From 25f34505bf610f41586ed77c2db97e7b8cd52114 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 29 Nov 2021 16:05:22 -0500 Subject: [PATCH] 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. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 6 +++++- src/SAWScript/Crucible/LLVM/Override.hs | 9 +++++++-- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 26870cdde8..673cbbb11e 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -932,7 +932,11 @@ 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, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , 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 index 6255ddc9a4..08cda081a2 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1526,6 +1526,7 @@ instantiateExtResolveSAWSymBV sc cc w tm = do -- Return a map containing the overwritten memory allocations. invalidateMutableAllocs :: ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1692,7 +1693,11 @@ 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, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1723,7 +1728,7 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v writeGlobal memVar mem' storePointsToValue :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?memOpts :: Crucible.MemOptions, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> LLVMCrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) ->