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
(→Load) |
(→Load) |
||
| (3 intermediate revisions by the same user not shown) | |||
Line 13:
'''Translation:'''
<lang scheme>
<pre>▼
;%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 40:
'''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]))
Line 65:
:extrafuns ((stackPtr2 bv[16])) ; New stack pointer state
:assumption (= stackPtr2 (bvadd stackPtr1 35)) ; Constrain new stack pointer
</
Assumptions:
Line 72:
== Load ==
LLVM spec: See [http://llvm.org/docs/LangRef.html#i_load i_load].
'''Example:'''
Line 81 ⟶ 82:
'''Translation:'''
<lang scheme>
:extrafuns ((memoryState0 bv[10240]))
:extrafuns ((stackPtr0 bv[16]))
Line 90 ⟶ 91:
;;%1 = load i29* %a, align 4 ;; <i29>
:extrafuns ((sym1 bv[
; Load sym1 from memory
Line 111 ⟶ 112:
;;%2 = load i35* %b, align 4 ;; <i35>
:extrafuns ((
; 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>
| |||