Anonymous user
User:Realazthat/Projects wishlist/LLVM/SMT: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/SMT (view source)
Revision as of 02:38, 19 October 2010
, 13 years ago→Load
No edit summary |
(→Load) |
||
| (8 intermediate revisions by the same user not shown) | |||
Line 8:
'''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]))
Line 21:
:extrafuns ((sym1 bv[1]))
:assumption (iff (= sym1 bv1[1]) (bvule bv8[32] sym0))
</
== Add ==
Line 31:
== Alloca ==
LLVM spec: See [http://llvm.org/docs/LangRef.html#i_alloca i_alloca].
Todo:
* Alignment
*: Necessary?
** Ignore for now
'''Example:'''
<lang llvm>
%a = alloca
%b = alloca
</lang>
'''Translation:'''
<lang scheme>
:extrafuns ((memoryState0 bv[10240]))
:extrafuns ((stackPtr0 bv[
;------^^^Initial state ^^^------
;%a = alloca
:extrafuns ((a bv[16])) ; Pointer
:assumption (= a
:extrafuns ((stackPtr1 bv[
:assumption (= stackPtr1 (bvadd stackPtr0
;%b = alloca
:extrafuns ((b bv[16])) ; Pointer
:assumption (= b
:extrafuns ((stackPtr2 bv[
:assumption (= stackPtr2 (bvadd stackPtr1
</lang>
Assumptions:
* Memory space is 10240
* Pointer size is 16
== Load ==
LLVM spec: See [http://llvm.org/docs/LangRef.html#i_load 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 [http://llvm.org/docs/LangRef.html#i_store i_store].
'''Algorithm:'''
<pre>
/*
101011011 buffer
001101000 store
001111000 mask
101101011 new buffer
--------------------
101011011 buffer
and
110000111 not(mask)
=
100000011
or
001101000 store
=
101101011 new buffer
*/
</pre>
'''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>
| |||