Anonymous user
User:Realazthat/Projects wishlist/LLVM/SMT: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/SMT (view source)
Revision as of 02:34, 19 October 2010
, 13 years agono edit summary
(→Load) |
No edit summary |
||
Line 40:
'''Example:'''
<lang llvm>
%a = alloca i29, align 4 ; <i29*>
%b = alloca i35, align 4 ; <i35*>
</lang>
Line 72:
== Load ==
LLVM spec: See [http://llvm.org/docs/LangRef.html#i_load i_load].
'''Example:'''
Line 115 ⟶ 116:
</pre>
== 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>
| |||