Bump submodules.

cabal.project

@@ -22,6 +22,7 @@ packages:
     deps/crucible/crucible-jvm
     deps/crucible/crucible-llvm
     deps/crucible/crucible-saw
+    deps/crucible/crucible-symio
     deps/crucible/crucible-syntax
     deps/crucible/crux
     deps/crucible/crux-mir

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -83,7 +83,7 @@ import qualified Cryptol.ModuleSystem.Renamer as MR
 
 import qualified Cryptol.Utils.Ident as C
 
-import Cryptol.Utils.PP
+import Cryptol.Utils.PP hiding ((</>))
 import Cryptol.Utils.Ident (Ident, preludeName, preludeReferenceName
                            , packIdent, interactiveName, identText
                            , packModName, textToModName, modNameChunks

saw/SAWScript/REPL/Command.hs

@@ -35,7 +35,7 @@ import SAWScript.REPL.Trie
 import SAWScript.Position (getPos)
 
 import Cryptol.Parser (ParseError())
-import Cryptol.Utils.PP
+import Cryptol.Utils.PP hiding ((</>))
 
 import Control.Monad (guard)
 import Data.Char (isSpace,isPunctuation,isSymbol)

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -153,6 +153,7 @@ import qualified Lang.Crucible.Simulator.PathSatisfiability as Crucible
 import qualified Lang.Crucible.LLVM.ArraySizeProfile as Crucible
 import qualified Lang.Crucible.LLVM.DataLayout as Crucible
 import qualified Lang.Crucible.LLVM.Bytes as Crucible
+import qualified Lang.Crucible.LLVM.Intrinsics as Crucible
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 import qualified Lang.Crucible.LLVM.MemType as Crucible
 import qualified Lang.Crucible.LLVM.Translation as Crucible
@@ -486,7 +487,7 @@ withMethodSpec ::
   LLVMModule arch ->
   String            {- ^ Name of the function -} ->
   LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
-  ((?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) =>
    LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> TopLevel a) ->
   TopLevel a
 withMethodSpec pathSat lm nm setup action =
@@ -530,7 +531,11 @@ withMethodSpec pathSat lm nm setup action =
               action cc methodSpec
 
 verifyMethodSpec ::
-  (?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
+  ) =>
   LLVMCrucibleContext arch ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   [MS.ProvedSpec (LLVM arch)] ->
@@ -1038,7 +1043,12 @@ ppGlobalPair cc gp =
 --------------------------------------------------------------------------------
 
 registerOverride ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch, Crucible.HasLLVMAnn Sym) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts::Crucible.MemOptions
+  , Crucible.HasPtrWidth wptr
+  , wptr ~ Crucible.ArchWidth arch
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   Options                    ->
   LLVMCrucibleContext arch       ->
   Crucible.SimContext (SAWCruciblePersonality Sym) Sym Crucible.LLVM ->
@@ -1075,7 +1085,11 @@ registerOverride opts cc sim_ctx top_loc cs =
               Crucible.writeGlobal mvar mem'
 
 registerInvariantOverride ::
-  (?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 ->
   LLVMCrucibleContext arch ->
   W4.ProgramLoc ->
@@ -1152,7 +1166,12 @@ withBreakpointCfgAndBlockId context name parent k =
          Nothing -> fail $ "Unexpected breakpoint name: " ++ name
 
 verifySimulate ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch, Crucible.HasLLVMAnn Sym) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts::Crucible.MemOptions
+  , Crucible.HasPtrWidth wptr
+  , wptr ~ Crucible.ArchWidth arch
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   Options ->
   LLVMCrucibleContext arch ->
   [Crucible.GenericExecutionFeature Sym] ->
@@ -1266,7 +1285,12 @@ scAndList sc = conj . filter nontrivial
 --------------------------------------------------------------------------------
 
 verifyPoststate ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch, Crucible.HasLLVMAnn Sym) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts::Crucible.MemOptions
+  , Crucible.HasPtrWidth wptr
+  , wptr ~ Crucible.ArchWidth arch
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   LLVMCrucibleContext arch              {- ^ crucible context                             -} ->
   MS.CrucibleMethodSpecIR (LLVM arch)              {- ^ specification                                -} ->
   Map AllocIndex (LLVMPtr wptr)     {- ^ allocation substitution                      -} ->
@@ -1331,7 +1355,7 @@ verifyPoststate cc mspec env0 globals ret =
 setupLLVMCrucibleContext ::
   Bool {- ^ enable path sat checking -} ->
   LLVMModule 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) =>
    LLVMCrucibleContext arch -> TopLevel a) ->
   TopLevel a
 setupLLVMCrucibleContext pathSat lm action =
@@ -1349,6 +1373,10 @@ setupLLVMCrucibleContext pathSat lm action =
      Crucible.llvmPtrWidth ctx $ \wptr ->
        Crucible.withPtrWidth wptr $
        do let ?lc = ctx^.Crucible.llvmTypeCtx
+          let ?memOpts = Crucible.defaultMemOptions
+                          { Crucible.laxPointerOrdering = laxPointerOrdering
+                          }
+          let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
           let ?recordLLVMAnnotation = \_ _ -> return ()
           cc <-
             io $
@@ -1382,11 +1410,8 @@ setupLLVMCrucibleContext pathSat lm action =
                  crucible_assert_then_assume_enabled
 
                let bindings = Crucible.fnBindingsFromList []
-               let memOpts  = Crucible.defaultMemOptions
-                                { Crucible.laxPointerOrdering = laxPointerOrdering
-                                }
                let simctx   = Crucible.initSimContext sym intrinsics halloc stdout
-                                 bindings (Crucible.llvmExtensionImpl memOpts)
+                                 bindings (Crucible.llvmExtensionImpl ?memOpts)
                                  Common.SAWCruciblePersonality
                mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans)
                         =<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod

src/SAWScript/Crucible/LLVM/Override.hs

@@ -368,7 +368,11 @@ ppArgs sym cc cs (Crucible.RegMap args) = do
 --   predicates.
 methodSpecHandler ::
   forall arch rtp args ret.
-  (?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                  {- ^ output/verbosity options                     -} ->
   SharedContext            {- ^ context for constructing SAW terms           -} ->
   LLVMCrucibleContext arch     {- ^ context for interacting with Crucible        -} ->
@@ -586,7 +590,11 @@ methodSpecHandler opts sc cc top_loc css h = do
 --   predicates.
 methodSpecHandler_prestate ::
   forall arch ctx.
-  (?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                  {- ^ output/verbosity options                     -} ->
   SharedContext            {- ^ context for constructing SAW terms           -} ->
   LLVMCrucibleContext arch     {- ^ context for interacting with Crucible        -} ->
@@ -630,16 +638,21 @@ methodSpecHandler_poststate opts sc cc retTy cs =
      computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue)
 
 -- learn pre/post condition
-learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym)
-          => Options
-          -> SharedContext
-          -> LLVMCrucibleContext arch
-          -> MS.CrucibleMethodSpecIR (LLVM arch)
-          -> PrePost
-          -> [MS.AllocGlobal (LLVM arch)]
-          -> Map AllocIndex (MS.AllocSpec (LLVM arch))
-          -> MS.StateSpec (LLVM arch)
-          -> OverrideMatcher (LLVM arch) md ()
+learnCond ::
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts::Crucible.MemOptions
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
+  Options ->
+  SharedContext ->
+  LLVMCrucibleContext arch ->
+  MS.CrucibleMethodSpecIR (LLVM arch) ->
+  PrePost ->
+  [MS.AllocGlobal (LLVM arch)] ->
+  Map AllocIndex (MS.AllocSpec (LLVM arch)) ->
+  MS.StateSpec (LLVM arch) ->
+  OverrideMatcher (LLVM arch) md ()
 learnCond opts sc cc cs prepost globals extras ss =
   do let loc = cs ^. MS.csLoc
      matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos)
@@ -870,7 +883,11 @@ ppProgramLoc loc =
 -- statement cannot be executed until bindings for any/all lhs
 -- variables exist.
 matchPointsTos :: forall arch md.
-  (?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          {- ^ saw script print out opts -} ->
   SharedContext    {- ^ term construction context -} ->
   LLVMCrucibleContext arch {- ^ simulator context     -} ->
@@ -1334,7 +1351,11 @@ learnGhost _sc _cc _loc _prepost _var (TypedTerm tp _)
 -- Returns a string on failure describing a concrete memory load failure.
 learnPointsTo ::
   forall arch md ann.
-  (?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      ->

src/SAWScript/Crucible/LLVM/X86.hs

@@ -139,6 +139,7 @@ type Ptr = C.LLVM.LLVMPtr Sym 64
 type X86Constraints =
   ( C.LLVM.HasPtrWidth (C.LLVM.ArchWidth LLVMArch)
   , C.LLVM.HasLLVMAnn Sym
+  , ?memOpts :: C.LLVM.MemOptions
   , ?lc :: C.LLVM.TypeContext
   )
 
@@ -295,6 +296,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
                  $ modTrans llvmModule ^. C.LLVM.transContext = do
       start <- io getCurrentTime
       let ?ptrWidth = knownNat @64
+      let ?memOpts = C.LLVM.defaultMemOptions
       let ?recordLLVMAnnotation = \_ _ -> return ()
       sc <- getSharedContext
       opts <- getOptions

src/SAWScript/X86.hs

@@ -398,6 +398,7 @@ translate opts elf fun =
   do let name = funName fun
      sayLn ("Translating function: " ++ BSC.unpack name)
 
+     let ?memOpts = Crucible.defaultMemOptions
      let ?recordLLVMAnnotation = \_ _ -> return ()
 
      let sym   = backend opts
@@ -431,7 +432,7 @@ setSimulatorVerbosity verbosity sym = do
 
 
 doSim ::
-  Crucible.HasLLVMAnn Sym =>
+  (?memOpts::Crucible.MemOptions, Crucible.HasLLVMAnn Sym) =>
   Options ->
   RelevantElf ->
   SymFuns Sym ->