From ad46e191c60e4817f48d5c87894826d98d849697 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Sat, 8 Aug 2020 22:16:20 -0700 Subject: [PATCH 1/5] Update for addition of badBehaviorMap implicit for LLVM annotations. See https://github.com/GaloisInc/crucible/pull/453 --- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 07578d55..8d6f8181 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -117,6 +117,7 @@ import Control.Monad.IO.Class ( MonadIO, liftIO ) import qualified Data.BitVector.Sized as BV import qualified Data.ByteString as BS import qualified Data.Foldable as F +import Data.IORef ( newIORef ) import qualified Data.IntervalMap.Strict as IM import qualified Data.Parameterized.NatRepr as PN @@ -222,6 +223,8 @@ newGlobalMemory proxy sym endian mmc mem = do memImpl1 sizeBV CLD.noAlignment (symArray2, tbl) <- populateMemory proxy sym mmc mem symArray1 + bbmap <- liftIO $ newIORef mempty + let ?badBehaviorMap = bbmap memImpl3 <- liftIO $ CL.doArrayStore sym memImpl2 ptr CLD.noAlignment symArray2 sizeBV let ptrTable = MemPtrTable { memPtrTable = tbl, memPtr = ptr, memRepr = ?ptrWidth } @@ -479,6 +482,7 @@ mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do mapRegionPointers :: ( MC.MemWidth w , 16 <= w , CB.IsSymInterface sym + , CL.HasLLVMAnn sym ) => MemPtrTable sym w -> MS.GlobalMap sym CL.Mem w From 22f2a3122c2d957e8ddfc0ff9eae255260b09801 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 10 Aug 2020 09:48:50 -0700 Subject: [PATCH 2/5] [x86_symbolic] Create badBehaviorMap earlier in test. --- x86_symbolic/tests/Main.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs index f6ac59a1..b03045a3 100644 --- a/x86_symbolic/tests/Main.hs +++ b/x86_symbolic/tests/Main.hs @@ -117,12 +117,12 @@ main = do symFuns <- MX.newSymFuns sym - (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem - let globalMap = MSM.mapRegionPointers memPtrTbl - bbMapRef <- newIORef mempty let ?badBehaviorMap = bbMapRef + (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem + let globalMap = MSM.mapRegionPointers memPtrTbl + let lookupFn :: MS.LookupFunctionHandle sym MX.X86_64 lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> do fail "Could not find function handle." From fc419e4c1808154838d717a6b05685bb3d0e2e2a Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 10 Aug 2020 13:47:44 -0700 Subject: [PATCH 3/5] [refinement] update for badBehaviorMap implicit parameter. --- refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs | 1 + refinement/tests/RefinementTests.hs | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs index e1389108..6ec9e875 100644 --- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs +++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs @@ -508,6 +508,7 @@ initializeMemory :: forall arch sym m proxy . ( MS.SymArchConstraints arch , 16 <= M.ArchAddrWidth arch , CB.IsSymInterface sym + , LLVM.HasLLVMAnn sym , MonadIO m ) => proxy arch diff --git a/refinement/tests/RefinementTests.hs b/refinement/tests/RefinementTests.hs index b22c3d8e..813141f0 100644 --- a/refinement/tests/RefinementTests.hs +++ b/refinement/tests/RefinementTests.hs @@ -284,10 +284,10 @@ mkSymbolicTest testinp = do CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns) -- FIXME: We probably need to pull endianness from somewhere else - (initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem - let globalMap = MSM.mapRegionPointers memPtrTbl bbMapRef <- newIORef mempty let ?badBehaviorMap = bbMapRef + (initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem + let globalMap = MSM.mapRegionPointers memPtrTbl let lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> error "Could not find function handle" let validityCheck _ _ _ _ = return Nothing From 1db2d1669ca5c73b0c1f501018dcdd12bdabe33a Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 10 Aug 2020 14:50:45 -0700 Subject: [PATCH 4/5] [symbolic] Defer badBehaviorMap creation to caller instead. --- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 8d6f8181..7e2896fe 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -117,7 +117,6 @@ import Control.Monad.IO.Class ( MonadIO, liftIO ) import qualified Data.BitVector.Sized as BV import qualified Data.ByteString as BS import qualified Data.Foldable as F -import Data.IORef ( newIORef ) import qualified Data.IntervalMap.Strict as IM import qualified Data.Parameterized.NatRepr as PN @@ -197,6 +196,7 @@ newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch , KnownNat (MC.ArchAddrWidth arch) , CB.IsSymInterface sym , Ord (WI.SymExpr sym WI.BaseNatType) + , CL.HasLLVMAnn sym , MonadIO m ) => proxy arch @@ -223,8 +223,6 @@ newGlobalMemory proxy sym endian mmc mem = do memImpl1 sizeBV CLD.noAlignment (symArray2, tbl) <- populateMemory proxy sym mmc mem symArray1 - bbmap <- liftIO $ newIORef mempty - let ?badBehaviorMap = bbmap memImpl3 <- liftIO $ CL.doArrayStore sym memImpl2 ptr CLD.noAlignment symArray2 sizeBV let ptrTable = MemPtrTable { memPtrTable = tbl, memPtr = ptr, memRepr = ?ptrWidth } From de31610929bbf056a784e8eefe304fcc689558d8 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 10 Aug 2020 17:47:35 -0700 Subject: [PATCH 5/5] Update submodules. --- deps/asl-translator | 2 +- deps/crucible | 2 +- deps/dismantle | 2 +- deps/semmc | 2 +- deps/what4 | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/deps/asl-translator b/deps/asl-translator index d0bac677..a71409d4 160000 --- a/deps/asl-translator +++ b/deps/asl-translator @@ -1 +1 @@ -Subproject commit d0bac677e038a54f47af0467e68c4aab95a32d64 +Subproject commit a71409d4168fe7db912e85c9c53af550751a6adf diff --git a/deps/crucible b/deps/crucible index 5cb47b4f..996db66c 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 5cb47b4f77299b54b0ead3f93f25dc24447c80f3 +Subproject commit 996db66ca35950439282fc5724278dc5490ecd55 diff --git a/deps/dismantle b/deps/dismantle index 1f61d725..21c5d44d 160000 --- a/deps/dismantle +++ b/deps/dismantle @@ -1 +1 @@ -Subproject commit 1f61d7259228bbfb51053e7c990fac6d9228e154 +Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9 diff --git a/deps/semmc b/deps/semmc index 990ce7ab..08ff6f46 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 990ce7ab63dd67cf0f23876d5d4d93da507ec11e +Subproject commit 08ff6f46c68b0166784779744860d11d9c919f1f diff --git a/deps/what4 b/deps/what4 index f9a8f950..b66527ed 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit f9a8f950e7c66f0f04312ce3983a42f3facd576e +Subproject commit b66527eda1274d4f9d539d8c2956d9fe215c4aa2