Submodule updates

GaloisInc · Nov 19, 2021 · 952fe55 · 952fe55
1 parent c6eae87
commit 952fe55
Show file tree

Hide file tree

Showing 9 changed files with 11 additions and 10 deletions.
diff --git a/deps/asl-translator b/deps/asl-translator
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/semmc b/deps/semmc
diff --git a/deps/what4 b/deps/what4
diff --git 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
@@ -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
@@ -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
@@ -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