Adapt to GaloisInc/crucible#914

This bumps the `crucible` submodule to include GaloisInc/crucible#914. This
also bumps the `macaw` submodule to include GaloisInc/macaw#244, which adapts
`macaw-symbolic` to the `crucible` changes. These `crucible` changes require
some tweaks in the following libraries:

* In `heapster-saw`, we need to add a `NuMatching1` instance for `GlobalVar`
  now that `LLVM_SideConditions` has a field of type `GlobalVar Mem`. This
  also requires defining an opaque `NuMatching` instance for `Nonce` to support
  the `NuMatching1` instance for `GlobalVar`.

  Elsewhere in `heapster-saw`, we need to adapt a pattern match on
  `LLVM_SideConditions` to accommodate its new field.
* In `saw-script`, we need to make sure that `?recordLLVMAnnotation` is given
  three arguments, not two, so that its type matches what `HasLLVMAnn` expects.

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

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 ->
@@ -3106,7 +3106,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)
@@ -3125,7 +3125,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 ->

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1377,7 +1377,7 @@ setupLLVMCrucibleContext pathSat lm action =
                           { Crucible.laxPointerOrdering = laxPointerOrdering
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
-          let ?recordLLVMAnnotation = \_ _ -> return ()
+          let ?recordLLVMAnnotation = \_ _ _ -> return ()
           cc <-
             io $
             do let verbosity = simVerbose opts

src/SAWScript/Crucible/LLVM/X86.hs

@@ -297,7 +297,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

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 }