GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-26 09:22:20 +03:00
Code Issues Projects Releases Wiki Activity

Bugfix and show more info when failing.

Browse Source
This commit is contained in:
Iavor Diatchki 2018-02-21 15:06:18 -08:00
parent 8bf523f8b1
commit e3f4e0875b
1 changed files with 18 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
symbolic/src/Data/Macaw/Symbolic/MemOps.hs
View File

@ -50,6 +50,7 @@ import Lang.Crucible.LLVM.MemModel.Pointer
, pattern LLVMPointer , pattern LLVMPointer
) )
import Lang.Crucible.LLVM.MemModel.Type(bitvectorType) import Lang.Crucible.LLVM.MemModel.Type(bitvectorType)
import Lang.Crucible.LLVM.MemModel.Generic(ppPtr)
import Lang.Crucible.LLVM.DataLayout(EndianForm(..)) import Lang.Crucible.LLVM.DataLayout(EndianForm(..))
import Lang.Crucible.LLVM.Bytes(toBytes) import Lang.Crucible.LLVM.Bytes(toBytes)
@ -71,12 +72,20 @@ type PtrOp sym w a =
RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} -> RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} ->
IO (a, CrucibleState s sym ext rtp blocks r ctx) IO (a, CrucibleState s sym ext rtp blocks r ctx)
binOpLabel :: IsSymInterface sym =>
String -> LLVMPtr sym w -> LLVMPtr sym w -> String
binOpLabel lab x y =
unlines [ "{ instruction: " ++ lab
, ", operand 1: " ++ show (ppPtr x)
, ", operand 2: " ++ show (ppPtr y)
, "}"
]
doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w) doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w)
doPtrMux c = ptrOp $ \sym _ _ xPtr xBits yPtr yBits x y -> doPtrMux c = ptrOp $ \sym _ _ xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
cases sym "ptr_mux" muxLLVMPtr cases sym (binOpLabel "ptr_mux" x y) muxLLVMPtr
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvIte sym c (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvIte sym c (asBits x) (asBits y)
, both_ptrs ~> , both_ptrs ~>
@ -89,7 +98,7 @@ doPtrAdd = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
ptr_bits <- andPred sym xPtr yBits ptr_bits <- andPred sym xPtr yBits
bits_ptr <- andPred sym xBits yPtr bits_ptr <- andPred sym xBits yPtr
cases sym "ptr_add" muxLLVMPtr cases sym (binOpLabel "ptr_add" x y) muxLLVMPtr
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvAdd sym (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvAdd sym (asBits x) (asBits y)
@ -111,7 +120,7 @@ doPtrSub = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
ptr_bits <- andPred sym xPtr yBits ptr_bits <- andPred sym xPtr yBits
ptr_ptr <- andPred sym xPtr yPtr ptr_ptr <- andPred sym xPtr yPtr
cases sym "ptr_sub" muxLLVMPtr cases sym (binOpLabel "ptr_sub" x y) muxLLVMPtr
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvSub sym (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvSub sym (asBits x) (asBits y)
@ -133,7 +142,8 @@ doPtrLt = ptrOp $ \sym _ _ xPtr xBits yPtr yBits x y ->
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
sameRegion <- natEq sym (ptrBase x) (ptrBase y) sameRegion <- natEq sym (ptrBase x) (ptrBase y)
ok <- andPred sym sameRegion =<< orPred sym both_bits both_ptrs ok <- andPred sym sameRegion =<< orPred sym both_bits both_ptrs
addAssertion sym ok (AssertFailureSimError "[ptr_lt] Invalid arguments") addAssertion sym ok
(AssertFailureSimError (binOpLabel "ptr_lt" x y ++ " Invalid arguments"))
bvUlt sym (asBits x) (asBits y) bvUlt sym (asBits x) (asBits y)
@ -143,7 +153,9 @@ doPtrLeq = ptrOp $ \sym _ _ xPtr xBits yPtr yBits x y ->
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
sameRegion <- natEq sym (ptrBase x) (ptrBase y) sameRegion <- natEq sym (ptrBase x) (ptrBase y)
ok <- andPred sym sameRegion =<< orPred sym both_bits both_ptrs ok <- andPred sym sameRegion =<< orPred sym both_bits both_ptrs
addAssertion sym ok (AssertFailureSimError "[ptr_leq] Invalid arguments") addAssertion sym ok
(AssertFailureSimError
(binOpLabel "ptr_leq" x y ++ " Invalid arguments"))
bvUle sym (asBits x) (asBits y) bvUle sym (asBits x) (asBits y)
@ -151,7 +163,7 @@ doPtrEq :: PtrOp sym w (RegValue sym BoolType)
doPtrEq = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y -> doPtrEq = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
cases sym "ptr_eq" itePred cases sym (binOpLabel "ptr_eq" x y) itePred
[ both_bits ~> endCase =<< bvEq sym (asBits x) (asBits y) [ both_bits ~> endCase =<< bvEq sym (asBits x) (asBits y)
, both_ptrs ~> endCase =<< ptrEq sym w x y , both_ptrs ~> endCase =<< ptrEq sym w x y
] ]