Merge pull request #1521 from GaloisInc/crucible-submod-bump

Submodules: Adapt to GaloisInc/crucible#914, GaloisInc/crucible#906, and GaloisInc/crucible#928
GaloisInc · Dec 6, 2021 · 96272c0 · 96272c0
2 parents a648349 + acb7894
commit 96272c0
Show file tree

Hide file tree

Showing 8 changed files with 83 additions and 25 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/macaw b/deps/macaw
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -45,6 +45,7 @@ import Data.Parameterized.Context hiding ((:>), empty, take, view)
 import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.TraversableFC
 import Data.Parameterized.BoolRepr
+import Data.Parameterized.Nonce (Nonce)
 
 -- import qualified Text.PrettyPrint.ANSI.Leijen as PP
 import qualified Prettyprinter as PP
@@ -70,7 +71,7 @@ import Verifier.SAW.OpenTerm
 
 -- | The lens into an 'RAssign' associated with a 'Member' proof
 --
--- FIXME HERE: this should go into Hobbits, possibly using 
+-- FIXME HERE: this should go into Hobbits, possibly using
 member :: Member ctx a -> Lens' (RAssign f ctx) (f a)
 member memb = lens (RL.get memb) (flip (RL.set memb))
 
@@ -399,6 +400,17 @@ instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where
 $(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |])
 -}
 
+$(mkNuMatching [t| forall tp. GlobalVar tp |])
+
+instance NuMatching (Nonce s tp) where
+  nuMatchingProof = unsafeMbTypeRepr
+
+instance Closable (Nonce s tp) where
+  toClosed = unsafeClose
+
+instance Liftable (Nonce s tp) where
+  mbLift = unClosed . mbLift . fmap toClosed
+
 instance Closable (BV.BV w) where
   toClosed = unsafeClose
 
@@ -729,7 +741,7 @@ cruCtxLookup (CruCtxCons _ tp) Member_Base = tp
 cruCtxLookup (CruCtxCons ctx _) (Member_Step memb) = cruCtxLookup ctx memb
 
 -- | Build a 'CruCtx' of the given length.
-cruCtxReplicate :: NatRepr n -> TypeRepr a -> Some CruCtx 
+cruCtxReplicate :: NatRepr n -> TypeRepr a -> Some CruCtx
 cruCtxReplicate n tp =
   case isZeroNat n of
     ZeroNat -> Some CruCtxNil

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -470,7 +470,7 @@ data TypedLLVMStmt ret ps_in ps_out where
   -- Type:
   -- > ps, x:ptr((rw,0) |-> p), cur_ps
   -- > -o ps, x:ptr((rw,0) |-> eq(ret)), ret:p, cur_ps
-  TypedLLVMLoad :: 
+  TypedLLVMLoad ::
     (HasPtrWidth w, 1 <= sz, KnownNat sz) =>
     !(TypedReg (LLVMPointerType w)) ->
     !(LLVMFieldPerm w sz) ->
@@ -540,7 +540,7 @@ data TypedLLVMStmt ret ps_in ps_out where
   -- referred to by a function pointer, assuming we know it has one:
   --
   -- Type: @x:llvm_funptr(p) -o ret:p@
-  TypedLLVMLoadHandle :: 
+  TypedLLVMLoadHandle ::
     HasPtrWidth w =>
     !(TypedReg (LLVMPointerType w)) ->
     !(TypeRepr (FunctionHandleType cargs ret)) ->
@@ -1338,7 +1338,7 @@ entryByID entryID =
     over typedBlockEntries (replaceNth (blockEntryIx entryID blk) e) blk)
 
 
--- | Build an empty 'TypedBlock' 
+-- | Build an empty 'TypedBlock'
 emptyBlockOfSort ::
   [Maybe String] ->
   Assignment CtxRepr cblocks ->
@@ -1943,7 +1943,7 @@ runPermCheckM names entryID args ghosts mb_perms_in m =
       (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args
       (arg_names, local_names) = initialNames args names
       st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names in
-  
+
   let go x = runGenStateContT x st (\_ () -> pure ()) in
   go $
   setVarTypes (Just "top") (noNames' stTopCtx) tops_ns stTopCtx >>>
@@ -1967,7 +1967,7 @@ initialNames CruCtxNil xs = (MNil, xs)
 initialNames (CruCtxCons ts _) xs =
   case initialNames ts xs of
     (ys, z:zs) -> (ys :>: Constant z, zs)
-    (ys, []  ) -> (ys :>: Constant Nothing, [])    
+    (ys, []  ) -> (ys :>: Constant Nothing, [])
 
 -- | Compute an empty debug name assignment from a known context
 noNames ::
@@ -2641,7 +2641,7 @@ ppCruRegAndPerms ctx r =
 -- their permissions, the variables in those permissions etc., as in
 -- 'varPermsTransFreeVars'
 getRelevantPerms :: [SomeName CrucibleType] ->
-                    PermCheckM ext cblocks blocks tops ret r ps r ps 
+                    PermCheckM ext cblocks blocks tops ret r ps r ps
                       (Some DistPerms)
 getRelevantPerms (namesListToNames -> SomeRAssign ns) =
   gets stCurPerms >>>= \perms ->
@@ -3121,7 +3121,7 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) =
     PExpr_Bool True ->
       dbgNames >>= \names ->
       emitStmt knownRepr names loc
-        (TypedSetRegPermExpr knownRepr $ 
+        (TypedSetRegPermExpr knownRepr $
           PExpr_Var $ typedRegVar tthen_reg) >>>= \(MNil :>: ret) ->
       stmtRecombinePerms >>>
       pure (addCtxName ctx ret)
@@ -3140,7 +3140,7 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) =
       pure (addCtxName ctx ret)
 
 -- For LLVM side conditions, treat each side condition as an assert
-tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) =
+tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions _ tp conds reg) =
   let treg = tcReg ctx reg in
   foldr
   (\(LLVMSideCondition cond_reg ub) rest_m ->

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -742,7 +742,11 @@ checkSpecReturnType cc mspec =
 -- Returns a tuple of (arguments, preconditions, pointer values,
 -- memory).
 verifyPrestate ::
-  (?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 ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
@@ -882,7 +886,11 @@ resolveArguments cc mem mspec env = mapM resolveArg [0..(nArgs-1)]
 -- | For each "llvm_global_alloc" in the method specification, allocate and
 -- register the appropriate memory.
 setupGlobalAllocs :: forall arch.
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  ( ?lc :: Crucible.TypeContext
+  , ?memOpts :: Crucible.MemOptions
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   LLVMCrucibleContext arch ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   MemImpl ->
@@ -928,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       ->
@@ -1010,7 +1023,11 @@ assertEqualVals cc v1 v2 =
 
 -- TODO(langston): combine with/move to executeAllocation
 doAlloc ::
-  (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
+  ( ?memOpts :: Crucible.MemOptions
+  , ?w4EvalTactic :: W4EvalTactic
+  , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym
+  ) =>
   LLVMCrucibleContext arch       ->
   AllocIndex ->
   LLVMAllocSpec ->
@@ -1390,7 +1407,7 @@ setupLLVMCrucibleContext pathSat lm action =
                           { Crucible.laxPointerOrdering = laxPointerOrdering
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
-          let ?recordLLVMAnnotation = \_ _ -> return ()
+          let ?recordLLVMAnnotation = \_ _ _ -> return ()
           let ?w4EvalTactic = W4EvalTactic { doW4Eval = what4Eval }
           let ?checkAllocSymInit = allocSymInitCheck
           cc <-

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -633,7 +633,12 @@ methodSpecHandler_prestate opts sc cc args cs =
 --   and computing postcondition predicates.
 methodSpecHandler_poststate ::
   forall arch ret.
-  (?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                  {- ^ output/verbosity options                     -} ->
   SharedContext            {- ^ context for constructing SAW terms           -} ->
   LLVMCrucibleContext arch     {- ^ context for interacting with Crucible        -} ->
@@ -706,7 +711,12 @@ enforceCompleteSubstitution loc ss =
 
 
 -- execute a pre/post condition
-executeCond :: (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym)
+executeCond :: ( ?lc :: Crucible.TypeContext
+               , ?memOpts :: Crucible.MemOptions
+               , ?w4EvalTactic :: W4EvalTactic
+               , Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+               , Crucible.HasLLVMAnn Sym
+               )
             => Options
             -> SharedContext
             -> LLVMCrucibleContext arch
@@ -1615,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
@@ -1707,7 +1718,12 @@ invalidateMutableAllocs opts sc cc cs = do
 -- | Perform an allocation as indicated by an @llvm_alloc@ or
 -- @llvm_fresh_pointer@ statement from the postcondition section.
 executeAllocation ::
-  (?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          ->
@@ -1734,7 +1750,11 @@ executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fres
      assignVar cc loc var ptr
 
 doAllocSymInit ::
-  (Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) =>
+  ( ?memOpts :: Crucible.MemOptions
+  , Crucible.IsSymInterface sym
+  , Crucible.HasPtrWidth wptr
+  , Crucible.HasLLVMAnn sym
+  ) =>
   sym ->
   Crucible.MemImpl sym ->
   Crucible.Mutability ->
@@ -1799,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     ->
@@ -1830,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)) ->

diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -299,7 +299,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       start <- io getCurrentTime
       let ?ptrWidth = knownNat @64
       let ?memOpts = C.LLVM.defaultMemOptions
-      let ?recordLLVMAnnotation = \_ _ -> return ()
+      let ?recordLLVMAnnotation = \_ _ _ -> return ()
       sc <- getSharedContext
       opts <- getOptions
       basic_ss <- getBasicSS

diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
@@ -401,7 +401,7 @@ translate opts elf fun =
      sayLn ("Translating function: " ++ BSC.unpack name)
 
      let ?memOpts = Crucible.defaultMemOptions
-     let ?recordLLVMAnnotation = \_ _ -> return ()
+     let ?recordLLVMAnnotation = \_ _ _ -> return ()
 
      let sym   = backend opts
          sopts = Opts { optsSym = sym, optsCry = cryEnv opts, optsMvar = memvar opts }