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: <lang scheme>
- %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))
</lang>
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*> %b = alloca i35, align 4 ; <i35*>
</lang>
Translation: <lang scheme>
- 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
</lang>
Assumptions:
- Memory space is 10240
- Pointer size is 16
Load
LLVM spec: See i_load.
Example: <lang llvm>
%1 = load i29* %a, align 4 ;; <i29> %2 = load i35* %b, align 4 ;; <i35>
</lang>
Translation:
<lang scheme>
- 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[29])) ;
- Load sym1 from memory
- assumption(
(extract[29:0] ; Extract the information from the huge resulting bit vector
(bvlshr ; Move the info back to rightmost position
(bvand ; Extract the masked bits
(bvshl ; Move the mask to the correct position
(zero_extend[10211] ; Extend the mask bitvector over the memory
(repeat[29] bv1[1]) ; Mask for sym1's corresponding bits
)
(zero_extend[10224] a) ; Move the mask by the value of the pointer a
)
memoryState0 ; Extract the mask bits from the last memory state
)
(zero_extend[10224] a) ; Move the info back to the right by the value of the pointer a
)
)
)
- %2 = load i35* %b, align 4 ;; <i35>
- extrafuns ((sym2 bv[35])) ;
- Load sym2 from memory
- assumption(
(extract[35:0] ; Extract the information from the huge resulting bit vector
(bvlshr ; Move the info back to rightmost position
(bvand ; Extract the masked bits
(bvshl ; Move the mask to the correct position
(zero_extend[10205] ; Extend the mask bitvector over the memory
(repeat[35] bv1[1]) ; Mask for sym1's corresponding bits
)
(zero_extend[10224] b) ; Move the mask by the value of the pointer b
)
memoryState0 ; Extract the mask bits from the last memory state
)
(zero_extend[10224] b) ; Move the info back to the right by the value of the pointer b
)
)
)
</lang>
Store
LLVM spec: See i_store.
Algorithm:
/* 101011011 buffer 001101000 store 001111000 mask 101101011 new buffer -------------------- 101011011 buffer and 110000111 not(mask) = 100000011 or 001101000 store = 101101011 new buffer */
Example: <lang llvm>
%a = alloca i29, align 4 ; <i29*> ; Deliberately not optimized out to keep things interesting %0 = add i29 0, 15 ; <i29> store i29 %0, i29* %a
</lang>
Translation: <lang scheme>
- 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))
- %0 = add i29 0, 15
- extrafuns ((sym0 bv[29]))
- assumption (= sym0 (bvadd bv0[29] bv15[29]))
- store i29 %0, i29* %a
- extrafuns ((memoryState1 bv[10240]))
- assumption (= memoryState1 ; The new memory state
(bvor ; Combine the data in a with the old memory state
(bvshl ; Move the data in a to the corresponding position in memory
(zero_extend[10211] sym0) ; The bits to be written
(zero_extend[10224] a) ; Move the bits over to the position pointed to by a
)
(bvand ; All data in the memorystate will still be there,
; except the part that needs to be overwritten
(bvnot ; Inverse the mask to create a zero'd mask to erase
; the bits that need to be overwritten
(bvshl ; Move the 1 bits to the correct position
(zero_extend[10211] (repeat[29] bv1[1])) ; Create a mask of 1 bits
(zero_extend[10224] a) ; Move the mask to the position pointed to by a
)
)
memoryState0 ; The old memory state
)
)
)
</lang>