From 379f89ee781943e650bce55dc7434b55e6080ee1 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Fri, 11 Jan 2019 23:01:07 -0800 Subject: [PATCH] Update to the latest crucible version The llvm memory model was extended with better diagnostics and configurable handling of undefined behavior. macaw-symbolic uses no undefined behavior checking, as those operations are only undefined in C. --- deps/crucible | 2 +- deps/flexdis86 | 2 +- deps/llvm-pretty | 2 +- deps/parameterized-utils | 2 +- symbolic/src/Data/Macaw/Symbolic/MemOps.hs | 4 +++- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 5 +++-- 6 files changed, 10 insertions(+), 7 deletions(-) diff --git a/deps/crucible b/deps/crucible index ca9173d2..284cda6b 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit ca9173d2ca5ffdf55750d676e9e67c297b38d377 +Subproject commit 284cda6bf9f85ae2df30cdf41099948504c34463 diff --git a/deps/flexdis86 b/deps/flexdis86 index 5c4453b0..2ac3d616 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 5c4453b0b2c89af2267174bf06b486a9dd6c57a2 +Subproject commit 2ac3d616996885f93b66c870520381cb09e783ca diff --git a/deps/llvm-pretty b/deps/llvm-pretty index e05cf319..4690fa10 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit e05cf3195b0938961cb0d8ecf4b7a4821f0d2673 +Subproject commit 4690fa103c6ce4d13fb659f0ac76b6c059157280 diff --git a/deps/parameterized-utils b/deps/parameterized-utils index 045e90c5..fac47a2a 160000 --- a/deps/parameterized-utils +++ b/deps/parameterized-utils @@ -1 +1 @@ -Subproject commit 045e90c564c7839667ff92274d442a343b76d168 +Subproject commit fac47a2a783cd885bdabfce026a5e7880be11537 diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs index d43d6f56..4f399b99 100644 --- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs +++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs @@ -396,7 +396,9 @@ doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y -> do okP1 <- isValidPtr sym mem w x okP2 <- isValidPtr sym mem w y ok <- andPred sym okP1 okP2 - endCaseCheck ok "Comparing invalid pointers" =<< ptrEq sym nw x y + (p1, p2) <- ptrEq sym nw x y + ps <- andPred sym p1 p2 + endCaseCheck ok "Comparing invalid pointers" ps ] doReadMem :: diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index eb9b1375..00b2d34c 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -110,6 +110,7 @@ import qualified Data.Macaw.Memory.Permissions as MMP import qualified Lang.Crucible.Backend as CB import qualified Lang.Crucible.LLVM.DataLayout as CLD import qualified Lang.Crucible.LLVM.MemModel as CL +import qualified Lang.Crucible.LLVM.UndefinedBehavior as UB import qualified Lang.Crucible.Simulator as CS import qualified Lang.Crucible.Types as CT import qualified What4.Interface as WI @@ -365,7 +366,7 @@ mapBitvectorToLLVMPointer mpt@(MemPtrTable im _) sym mem offsetVal = allocBase <- WI.bvLit sym wrep (MC.memWordToUnsigned (allocationBase alloc)) allocationOffset <- WI.bvSub sym offsetVal allocBase let ?ptrWidth = wrep - Just <$> CL.doPtrAddOffset sym mem (allocationPtr alloc) allocationOffset + Just <$> CL.doPtrAddOffset sym (Just UB.laxConfig) mem (allocationPtr alloc) allocationOffset [] -> return Nothing _ -> error ("Overlapping allocations for pointer: " ++ show (WI.printSymExpr offsetVal)) Nothing -> do @@ -416,7 +417,7 @@ staticRegionMuxTree (MemPtrTable im _) sym mem offsetVal = do allocBase <- WI.bvLit sym rep (MC.memWordToUnsigned (allocationBase alloc)) allocationOffset <- WI.bvSub sym offsetVal allocBase let ?ptrWidth = rep - thisPtr <- CL.doPtrAddOffset sym mem (allocationPtr alloc) allocationOffset + thisPtr <- CL.doPtrAddOffset sym (Just UB.laxConfig) mem (allocationPtr alloc) allocationOffset CL.muxLLVMPtr sym p thisPtr f addMuxForRegion f (interval, alloc) = do case interval of