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) |
||
| (2 intermediate revisions by the same user not shown) | |||
Line 13:
'''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 45:
'''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 82:
'''Translation:'''
<lang scheme>
:extrafuns ((memoryState0 bv[10240]))
:extrafuns ((stackPtr0 bv[16]))
Line 91:
;;%1 = load i29* %a, align 4 ;; <i29>
:extrafuns ((sym1 bv[
; Load sym1 from memory
Line 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
)
)
)
</
== Store ==
Line 168 ⟶ 185:
;store i29 %0, i29* %a
:extrafuns ((memoryState1 bv[10240]))
:assumption (= memoryState1
(bvor ; Combine the data in a with the old memory state
(bvshl ; Move the data in a to the corresponding position in memory
| |||