From 4565192f11ae26c0d6ca5e343644661c713381e6 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Thu, 18 Nov 2021 20:05:22 -0800 Subject: [PATCH] Submodule updates --- deps/asl-translator | 2 +- deps/crucible | 2 +- deps/llvm-pretty | 2 +- deps/semmc | 2 +- deps/what4 | 2 +- refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs | 2 +- refinement/tests/RefinementTests.hs | 2 +- symbolic/src/Data/Macaw/Symbolic.hs | 5 +++-- symbolic/src/Data/Macaw/Symbolic/Testing.hs | 2 +- 9 files changed, 11 insertions(+), 10 deletions(-) diff --git a/deps/asl-translator b/deps/asl-translator index 9906e850..6b9bcb4d 160000 --- a/deps/asl-translator +++ b/deps/asl-translator @@ -1 +1 @@ -Subproject commit 9906e850cd93cace9cd4fc2288b92c4b0822bdc0 +Subproject commit 6b9bcb4d0a1d64910438c2faff37fd1905dd9591 diff --git a/deps/crucible b/deps/crucible index 01154760..f7fa4d20 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 011547602d8fe40a22434b460038e0021e0b216a +Subproject commit f7fa4d20ce1248861a41b4e758b49ea9cbc99fdc diff --git a/deps/llvm-pretty b/deps/llvm-pretty index 8456623f..7ab7ac98 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit 8456623f243a47aa42693617fa22abbfac22a528 +Subproject commit 7ab7ac98eab93b6a84472fb040621adf0b150297 diff --git a/deps/semmc b/deps/semmc index 034e28b6..87782b4d 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 034e28b61afc69c17cd8ae99e374ad5a8329e17d +Subproject commit 87782b4d9f21ec24b576170bd0892cdee11a89bc diff --git a/deps/what4 b/deps/what4 index ce5c0aa9..042a8112 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit ce5c0aa937286932f792fe33ad7692495cdd54a6 +Subproject commit 042a8112b1d2b97b91e3399bb976eebe33fc60b8 diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs index 6a4d4f36..412692cf 100644 --- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs +++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs @@ -184,7 +184,7 @@ smtSolveTransfer ctx slice case some_cfg of C.SomeCFG cfg -> do let executionFeatures = [] - let ?recordLLVMAnnotation = \_ _ -> pure () + let ?recordLLVMAnnotation = \_ _ _ -> pure () initialState <- initializeSimulator ctx sym archVals halloc cfg entryBlock -- Symbolically execute the relevant code in a fresh assumption diff --git a/refinement/tests/RefinementTests.hs b/refinement/tests/RefinementTests.hs index a5a16f48..4f12c5b0 100644 --- a/refinement/tests/RefinementTests.hs +++ b/refinement/tests/RefinementTests.hs @@ -282,7 +282,7 @@ mkSymbolicTest testinp = do printf "External resolutions of %s: %s\n" (show funcName) (show (MD.discoveredClassifyFailureResolutions dfi)) CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns) - let ?recordLLVMAnnotation = \_ _ -> pure () + let ?recordLLVMAnnotation = \_ _ _ -> pure () -- 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 diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 112f6fc7..fc3fe3fe 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -1044,15 +1044,16 @@ termStmtToBlockEnd tm0 = -- * Symbolic simulation -evalMacawExprExtension :: forall sym arch f tp +evalMacawExprExtension :: forall sym arch f tp p rtp blocks r ctx ext . IsSymInterface sym => sym -> C.IntrinsicTypes sym -> (Int -> String -> IO ()) + -> C.CrucibleState p sym ext rtp blocks r ctx -> (forall utp . f utp -> IO (C.RegValue sym utp)) -> MacawExprExtension arch f tp -> IO (C.RegValue sym tp) -evalMacawExprExtension sym _iTypes _logFn f e0 = +evalMacawExprExtension sym _iTypes _logFn _cst f e0 = case e0 of MacawOverflows op w xv yv cv -> do diff --git a/symbolic/src/Data/Macaw/Symbolic/Testing.hs b/symbolic/src/Data/Macaw/Symbolic/Testing.hs index 5f7cd544..87e9d954 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Testing.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Testing.hs @@ -234,7 +234,7 @@ simulateAndVerify goalSolver logger sym execFeatures archInfo archVals mem (Resu CCC.SomeCFG g <- MS.mkFunCFG (MS.archFunctions archVals) halloc funName posFn dfi let endianness = toCrucibleEndian (MAI.archEndianness archInfo) - let ?recordLLVMAnnotation = \_ _ -> return () + let ?recordLLVMAnnotation = \_ _ _ -> return () (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @arch) sym endianness MSM.ConcreteMutable mem let globalMap = MSM.mapRegionPointers memPtrTbl (memVar, stackPointer, execResult) <- simulateFunction sym execFeatures archVals halloc initMem globalMap g