User:Realazthat/Projects wishlist/LLVM/SMT: Difference between revisions
Content added Content deleted
(→Load) |
No edit summary |
||
Line 40: | Line 40: | ||
'''Example:''' |
'''Example:''' |
||
<lang llvm> |
<lang llvm> |
||
%a = alloca i29, align 4 ; <i29*> |
%a = alloca i29, align 4 ; <i29*> |
||
%b = alloca i35, align 4 ; <i35*> |
%b = alloca i35, align 4 ; <i35*> |
||
</lang> |
</lang> |
||
Line 72: | Line 72: | ||
== Load == |
== Load == |
||
LLVM spec: See [http://llvm.org/docs/LangRef.html#i_load i_load]. |
|||
'''Example:''' |
'''Example:''' |
||
Line 115: | Line 116: | ||
</pre> |
</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> |