User:Realazthat/Projects wishlist/LLVM/SMT

Documents conversions from LLVM IR to SMT

ICMP

LLVM spec: i_icmp.

TODO: vector comparison

Example: <lang llvm>

 %0 = add i32 10, 11
 %1 = icmp ule i32 8, %0

</lang>

Translation:

;%0 = add i32 10, 11
:extrafuns ((sym0 bv[32]))
:assumption (= sym0 (bvadd bv10[32] bv11[32]))

;%1 = icmp ule i32 8, %0
:extrafuns ((sym1 bv[1]))
:assumption (iff (= sym1 bv1[1]) (bvule bv8[32] sym0))

Add

LLVM spec: See i_add.

TODO: vector addition

Example: #ICMP

Alloca

LLVM spec: See i_alloca.

Todo:

Alignment
Necessary?
- Ignore for now

Example: <lang llvm>

 %a = alloca i29, align 4                        ; <i29*> [#uses=4]
 %b = alloca i35, align 4                        ; <i35*> [#uses=4]

</lang>

Translation:

:extrafuns ((memoryState0 bv[10240]))
:extrafuns ((stackPtr0 bv[16]))
;------^^^Initial state ^^^------

;%a = alloca i29, align 4                        ;; <i29*>
:extrafuns ((a bv[16]))                          ; Pointer
:assumption (= a stackPtr0))                     ; Constraint, related to last stack pointer state

:extrafuns ((stackPtr1 bv[16]))
:assumption (= stackPtr1 (bvadd stackPtr0 29))



;%b = alloca i35, align 4                        ;; <i35*>
:extrafuns ((b bv[16]))                          ; Pointer
:assumption (= b stackPtr1)                      ; Constraint, related to last stack pointer state

:extrafuns ((stackPtr2 bv[16]))                  ; New stack pointer state
:assumption (= stackPtr2 (bvadd stackPtr1 35))   ; Constrain new stack pointer

Assumptions:

Memory space is 10240
Pointer size is 16

Load

Example: <lang llvm>

 %1 = load i29* %a, align 4                      ;; <i29>
 %2 = load i35* %b, align 4                      ;; <i35>

</lang>

Translation:

:extrafuns ((memoryState0 bv[10240]))
:extrafuns ((stackPtr0 bv[16]))

:extrafuns ((a bv[16]))
:extrafuns ((b bv[16]))
;------^^^Initial state ^^^------

;;%1 = load i29* %a, align 4                     ;; <i29>
:extrafuns ((sym1 bv[32]))                       ; 
;TODO

;;%2 = load i35* %b, align 4                     ;; <i35>
:extrafuns ((sym1 bv[32]))                       ;
;TODO