Adapt to GaloisInc/crucible#928

This bumps the `crucible` submodule to include GaloisInc/crucible#928. The `crucible` changes require adding some additional `?memOpts :: MemOptions` constraints to various functions.
GaloisInc · Dec 3, 2021 · acb7894 · acb7894
1 parent f4891a0
commit acb7894
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 4 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -936,7 +936,12 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs
 -- function spec, write the given value to the address of the given
 -- pointer.
 setupPrePointsTos :: forall arch.
-  (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts :: Crucible.MemOptions
+  , ?w4EvalTactic :: W4EvalTactic
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   MS.CrucibleMethodSpecIR (LLVM arch)       ->
   Options ->
   LLVMCrucibleContext arch       ->

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1625,6 +1625,7 @@ instantiateExtResolveSAWSymBV sc cc w tm = do
 -- Return a map containing the overwritten memory allocations.
 invalidateMutableAllocs ::
   ( ?lc :: Crucible.TypeContext
+  , ?memOpts :: Crucible.MemOptions
   , ?w4EvalTactic :: W4EvalTactic
   , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
   , Crucible.HasLLVMAnn Sym
@@ -1818,7 +1819,12 @@ executeGhost _sc _var (TypedTerm tp _) =
 -- the CrucibleSetup block. First we compute the value indicated by
 -- 'val', and then write it to the address indicated by 'ptr'.
 executePointsTo ::
-  (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts :: Crucible.MemOptions
+  , ?w4EvalTactic :: W4EvalTactic
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   Options                    ->
   SharedContext              ->
   LLVMCrucibleContext arch     ->
@@ -1849,7 +1855,11 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v
      writeGlobal memVar mem'
 
 storePointsToValue ::
-  (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ( ?memOpts :: Crucible.MemOptions
+  , ?w4EvalTactic :: W4EvalTactic
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   Options ->
   LLVMCrucibleContext arch ->
   Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) ->
+6 −3		crucible-concurrency/test/Main.hs
+2 −2		crucible-llvm/CHANGELOG.md
+3 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+54 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+29 −12		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+15 −5		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+66 −0		crucible-llvm/test/TestMemory.hs
+1 −0		crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+22 −0		crux-llvm/test-data/golden/isnan.c
+1 −0		crux-llvm/test-data/golden/isnan.config
+1 −0		crux-llvm/test-data/golden/isnan.good