User:Realazthat/Projects wishlist/LLVM/SMT: Difference between revisions

Content added Content deleted
No edit summary
Line 90: Line 90:


;;%1 = load i29* %a, align 4 ;; <i29>
;;%1 = load i29* %a, align 4 ;; <i29>
:extrafuns ((sym1 bv[32])) ;
:extrafuns ((sym1 bv[32])) ;

;TODO
; 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>
;;%2 = load i35* %b, align 4 ;; <i35>
Retrieved from "https://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/SMT"