From b39aa804c888827971f911ff95a705938184c12e Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 15 Nov 2021 10:56:20 -0800
Subject: [PATCH 01/10] added the command heapster_set_translation_checks to
 turn off the translation-time assertPermStack* and assertTopPermM checks used
 during translation

---
 .../Verifier/SAW/Heapster/IRTTranslation.hs   |  27 +--
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 155 ++++++++++--------
 src/SAWScript/HeapsterBuiltins.hs             |  31 ++--
 src/SAWScript/Interpreter.hs                  |   7 +
 src/SAWScript/Value.hs                        |   6 +-
 5 files changed, 136 insertions(+), 90 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
index f7b9e6a236..8ea6907157 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
@@ -186,7 +186,8 @@ runIRTTyVarsTransM :: PermEnv -> IRTRecName args -> CruCtx args ->
                       Either String a
 runIRTTyVarsTransM env n_rec argsCtx m = runReaderT m ctx
   where args_trans = RL.map (\tp -> Const $ typeTransTypes $
-                               runNilTypeTransM (translateClosed tp) env)
+                               runNilTypeTransM env noChecks $
+                               translateClosed tp)
                             (cruCtxToTypes argsCtx)
         ctx = IRTTyVarsTransCtx n_rec args_trans MNil env
 
@@ -274,8 +275,8 @@ translateCompletePermIRTTyVars sc env npn_rec args p =
     Left err -> fail err
     Right (tps, ixs) ->
       do tm <- completeOpenTermTyped sc $
-               runNilTypeTransM (lambdaExprCtx args $
-                                  listSortOpenTerm <$> sequence tps) env
+               runNilTypeTransM env noChecks (lambdaExprCtx args $
+                                              listSortOpenTerm <$> sequence tps)
          return (tm, setIRTVarIdxs ixs)
 
 -- | Given the a recursive shape being defined, translate the shape's body to
@@ -293,8 +294,8 @@ translateCompleteShapeIRTTyVars sc env nmsh_rec =
     Left err -> fail err
     Right (tps, ixs) ->
       do tm <- completeOpenTermTyped sc $
-               runNilTypeTransM (lambdaExprCtx args $
-                                  listSortOpenTerm <$> sequence tps) env
+               runNilTypeTransM env noChecks (lambdaExprCtx args $
+                                              listSortOpenTerm <$> sequence tps)
          return (tm, setIRTVarIdxs ixs)
 
 -- | Types from which we can get IRT type variables, e.g. ValuePerm
@@ -572,8 +573,8 @@ translateCompleteIRTDesc sc env tyVarsIdent args p ixs =
              [ applyOpenTermMulti (globalOpenTerm tyVarsIdent)
                                   (exprCtxToTerms ectx) ]
      tp <- completeOpenTerm sc $
-           runNilTypeTransM (translateClosed args >>= \tptrans ->
-                              piTransM "e" tptrans irtDescOpenTerm) env
+           runNilTypeTransM env noChecks (translateClosed args >>= \tptrans ->
+                                           piTransM "e" tptrans irtDescOpenTerm)
      return $ TypedTerm tm tp
 
 -- | Types from which we can get IRT type descriptions, e.g. ValuePerm
@@ -736,8 +737,8 @@ translateCompleteIRTDef :: SharedContext -> PermEnv ->
                            IO TypedTerm
 translateCompleteIRTDef sc env tyVarsIdent descIdent args =
   completeOpenTermTyped sc $
-  runNilTypeTransM (lambdaExprCtx args $
-                     irtDefinition tyVarsIdent descIdent) env
+  runNilTypeTransM env noChecks (lambdaExprCtx args $
+                                 irtDefinition tyVarsIdent descIdent)
 
 -- | Given identifiers whose definitions in the shared context are the results
 -- of corresponding calls to 'translateCompleteIRTDef',
@@ -749,8 +750,8 @@ translateCompleteIRTFoldFun :: SharedContext -> PermEnv ->
                                IO Term
 translateCompleteIRTFoldFun sc env tyVarsIdent descIdent _ args =
   completeOpenTerm sc $
-  runNilTypeTransM (lambdaExprCtx args $
-                     irtFoldFun tyVarsIdent descIdent) env
+  runNilTypeTransM env noChecks (lambdaExprCtx args $
+                                 irtFoldFun tyVarsIdent descIdent)
 
 -- | Given identifiers whose definitions in the shared context are the results
 -- of corresponding calls to 'translateCompleteIRTDef',
@@ -762,8 +763,8 @@ translateCompleteIRTUnfoldFun :: SharedContext -> PermEnv ->
                                  IO Term
 translateCompleteIRTUnfoldFun sc env tyVarsIdent descIdent _ args =
   completeOpenTerm sc $
-  runNilTypeTransM (lambdaExprCtx args $
-                     irtUnfoldFun tyVarsIdent descIdent) env
+  runNilTypeTransM env noChecks (lambdaExprCtx args $
+                                 irtUnfoldFun tyVarsIdent descIdent)
 
 -- | Get the terms for the arguments to @IRT@, @foldIRT@, and @unfoldIRT@
 -- given the appropriate identifiers
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index ab46c02027..323190aa28 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -609,30 +609,42 @@ instance (Translate info ctx a tr, NuMatching a) =>
 -- * Translating Types
 ----------------------------------------------------------------------
 
+-- | A flag for whether or not to perform checks in the translation. We use this
+-- type, rather than just 'Bool', for documentation purposes.
+newtype ChecksFlag = ChecksFlag { unChecksFlag :: Bool }
+
+-- | The 'ChecksFlag' specifying not to perform any translation checks
+noChecks :: ChecksFlag
+noChecks = ChecksFlag False
+
+-- | The 'ChecksFlag' specifying to perform all translation checks
+doChecks :: ChecksFlag
+doChecks = ChecksFlag True
+
 -- | Translation info for translating types and pure expressions
-data TypeTransInfo ctx = TypeTransInfo (ExprTransCtx ctx) PermEnv
+data TypeTransInfo ctx = TypeTransInfo (ExprTransCtx ctx) PermEnv ChecksFlag
 
 -- | Build an empty 'TypeTransInfo' from a 'PermEnv'
-emptyTypeTransInfo :: PermEnv -> TypeTransInfo RNil
+emptyTypeTransInfo :: PermEnv -> ChecksFlag -> TypeTransInfo RNil
 emptyTypeTransInfo = TypeTransInfo MNil
 
 instance TransInfo TypeTransInfo where
-  infoCtx (TypeTransInfo ctx _) = ctx
-  infoEnv (TypeTransInfo _ env) = env
-  extTransInfo etrans (TypeTransInfo ctx env) =
-    TypeTransInfo (ctx :>: etrans) env
+  infoCtx (TypeTransInfo ctx _ _) = ctx
+  infoEnv (TypeTransInfo _ env _) = env
+  extTransInfo etrans (TypeTransInfo ctx env checks) =
+    TypeTransInfo (ctx :>: etrans) env checks
 
 -- | The translation monad specific to translating types and pure expressions
 type TypeTransM = TransM TypeTransInfo
 
 -- | Run a 'TypeTransM' computation in the empty translation context
-runNilTypeTransM :: TypeTransM RNil a -> PermEnv -> a
-runNilTypeTransM m env = runTransM m (emptyTypeTransInfo env)
+runNilTypeTransM :: PermEnv -> ChecksFlag -> TypeTransM RNil a -> a
+runNilTypeTransM env checks m = runTransM m (emptyTypeTransInfo env checks)
 
 -- | Run a translation computation in an empty expression translation context
 inEmptyCtxTransM :: TypeTransM RNil a -> TypeTransM ctx a
 inEmptyCtxTransM =
-  withInfoM (\(TypeTransInfo _ env) -> TypeTransInfo MNil env)
+  withInfoM (\(TypeTransInfo _ env checks) -> TypeTransInfo MNil env checks)
 
 instance TransInfo info => Translate info ctx (NatRepr n) OpenTerm where
   translate mb_n = return $ natOpenTerm $ mbLift $ fmap natValue mb_n
@@ -1897,7 +1909,8 @@ data ImpTransInfo ext blocks tops ret ps ctx =
     itiPermStackVars :: RAssign (Member ctx) ps,
     itiPermEnv :: PermEnv,
     itiBlockMapTrans :: TypedBlockMapTrans ext blocks tops ret,
-    itiReturnType :: OpenTerm
+    itiReturnType :: OpenTerm,
+    itiChecksFlag :: ChecksFlag
   }
 
 instance TransInfo (ImpTransInfo ext blocks tops ret ps) where
@@ -1924,20 +1937,22 @@ impTransM :: forall ctx ps ext blocks tops ret a.
              OpenTerm -> ImpTransM ext blocks tops ret ps ctx a ->
              TypeTransM ctx a
 impTransM pvars pctx mapTrans retType =
-  withInfoM $ \(TypeTransInfo ectx env) ->
+  withInfoM $ \(TypeTransInfo ectx env checks) ->
   ImpTransInfo { itiExprCtx = ectx,
                  itiPermCtx = RL.map (const $ PTrans_True) ectx,
                  itiPermStack = pctx,
                  itiPermStackVars = pvars,
                  itiPermEnv = env,
                  itiBlockMapTrans = mapTrans,
-                 itiReturnType = retType }
+                 itiReturnType = retType,
+                 itiChecksFlag = checks }
 
 -- | Embed a type translation into an impure translation
 -- FIXME: should no longer need this...
 tpTransM :: TypeTransM ctx a -> ImpTransM ext blocks tops ret ps ctx a
 tpTransM =
-  withInfoM (\info -> TypeTransInfo (itiExprCtx info) (itiPermEnv info))
+  withInfoM (\(ImpTransInfo {..}) ->
+              TypeTransInfo itiExprCtx itiPermEnv itiChecksFlag)
 
 -- | Get most recently bound variable
 getTopVarM :: ImpTransM ext blocks tops ret ps (ctx :> tp) (ExprTrans tp)
@@ -1975,15 +1990,23 @@ getPermStackDistPerms =
        `mbApply`
        permTransCtxPerms prxs stack
 
+-- | Run a computation if the current 'ChecksFlag' is set
+ifChecksFlagM :: ImpTransM ext blocks tops ret ps ctx () ->
+                 ImpTransM ext blocks tops ret ps ctx ()
+ifChecksFlagM m =
+  (itiChecksFlag <$> ask) >>= \checks ->
+  if unChecksFlag checks then m else return ()
+
 -- | Assert a property of the current permission stack, raising an 'error' if it
 -- fails to hold. The 'String' names the construct being translated.
 assertPermStackM :: HasCallStack => String ->
                     (RAssign (Member ctx) ps -> PermTransCtx ctx ps -> Bool) ->
                     ImpTransM ext blocks tops ret ps ctx ()
 assertPermStackM nm f =
-  ask >>= \info ->
-  if f (itiPermStackVars info) (itiPermStack info) then return () else
-    error ("translate: " ++ nm ++ nlPrettyCallStack callStack)
+  ifChecksFlagM
+  (ask >>= \info ->
+   if f (itiPermStackVars info) (itiPermStack info) then return () else
+     error ("translate: " ++ nm ++ nlPrettyCallStack callStack))
 
 -- | Assert that the top portion of the current permission stack equals the
 -- given 'DistPerms'
@@ -1991,45 +2014,48 @@ assertPermStackTopEqM :: HasCallStack => ps ~ (ps1 :++: ps2) =>
                          String -> f ps1 -> Mb ctx (DistPerms ps2) ->
                          ImpTransM ext blocks tops ret ps ctx ()
 assertPermStackTopEqM nm prx expected =
-  getPermStackDistPerms >>= \perms ->
-  let actuals =
-        fmap (snd . splitDistPerms prx (mbDistPermsToProxies expected)) perms in
-  if expected == actuals then return () else
-    error ("assertPermStackEqM (" ++ nm ++ "): expected permission stack:\n" ++
-           permPrettyString emptyPPInfo expected ++
-           "\nFound permission stack:\n" ++
-           permPrettyString emptyPPInfo actuals ++
-           nlPrettyCallStack callStack)
+  ifChecksFlagM
+  (getPermStackDistPerms >>= \perms ->
+   let actuals =
+         fmap (snd . splitDistPerms prx (mbDistPermsToProxies expected)) perms in
+   if expected == actuals then return () else
+     error ("assertPermStackEqM (" ++ nm ++ "): expected permission stack:\n" ++
+            permPrettyString emptyPPInfo expected ++
+            "\nFound permission stack:\n" ++
+            permPrettyString emptyPPInfo actuals ++
+            nlPrettyCallStack callStack))
 
 -- | Assert that the current permission stack equals the given 'DistPerms'
 assertPermStackEqM :: HasCallStack => String -> Mb ctx (DistPerms ps) ->
                       ImpTransM ext blocks tops ret ps ctx ()
 assertPermStackEqM nm perms =
   -- FIXME: unify this function with assertPermStackTopEqM
-  getPermStackDistPerms >>= \stack_perms ->
-  if perms == stack_perms then return () else
-    error ("assertPermStackEqM (" ++ nm ++ "): expected permission stack:\n" ++
-           permPrettyString emptyPPInfo perms ++
-           "\nFound permission stack:\n" ++
-           permPrettyString emptyPPInfo stack_perms ++
-           nlPrettyCallStack callStack)
+  ifChecksFlagM
+  (getPermStackDistPerms >>= \stack_perms ->
+   if perms == stack_perms then return () else
+     error ("assertPermStackEqM (" ++ nm ++ "): expected permission stack:\n" ++
+            permPrettyString emptyPPInfo perms ++
+            "\nFound permission stack:\n" ++
+            permPrettyString emptyPPInfo stack_perms ++
+            nlPrettyCallStack callStack))
 
 -- | Assert that the top permission is as given by the arguments
 assertTopPermM :: HasCallStack => String -> Mb ctx (ExprVar a) ->
                   Mb ctx (ValuePerm a) ->
                   ImpTransM ext blocks tops ret (ps :> a) ctx ()
 assertTopPermM nm x p =
-  getPermStackDistPerms >>= \stack_perms ->
-  case mbMatch stack_perms of
-    [nuMP| DistPermsCons _ x' p' |] | x == x' && p == p' -> return ()
-    [nuMP| DistPermsCons _ x' p' |] ->
-      error ("assertTopPermM (" ++ nm ++ "): expected top permissions:\n" ++
-             permPrettyString emptyPPInfo (mbMap2 distPerms1 x p) ++
-             "\nFound top permissions:\n" ++
-             permPrettyString emptyPPInfo (mbMap2 distPerms1 x' p') ++
-             nlPrettyCallStack callStack ++
-             "\nCurrent perm stack:\n" ++
-             permPrettyString emptyPPInfo stack_perms)
+  ifChecksFlagM
+  (getPermStackDistPerms >>= \stack_perms ->
+   case mbMatch stack_perms of
+     [nuMP| DistPermsCons _ x' p' |] | x == x' && p == p' -> return ()
+     [nuMP| DistPermsCons _ x' p' |] ->
+       error ("assertTopPermM (" ++ nm ++ "): expected top permissions:\n" ++
+              permPrettyString emptyPPInfo (mbMap2 distPerms1 x p) ++
+              "\nFound top permissions:\n" ++
+              permPrettyString emptyPPInfo (mbMap2 distPerms1 x' p') ++
+              nlPrettyCallStack callStack ++
+              "\nCurrent perm stack:\n" ++
+              permPrettyString emptyPPInfo stack_perms))
 
 -- | Get the (translation of the) perms for a variable
 getVarPermM :: Mb ctx (ExprVar tp) ->
@@ -4352,10 +4378,10 @@ translateBlockMapBodies mapTrans =
 -- | Translate a typed CFG to a SAW term
 translateCFG ::
   PermCheckExtC ext =>
-  PermEnv ->
+  PermEnv -> ChecksFlag ->
   TypedCFG ext blocks ghosts inits ret ->
   OpenTerm
-translateCFG env (cfg :: TypedCFG ext blocks ghosts inits ret) =
+translateCFG env checks (cfg :: TypedCFG ext blocks ghosts inits ret) =
   let h = tpcfgHandle cfg
       fun_perm = tpcfgFunPerm cfg
       blkMap = tpcfgBlockMap cfg
@@ -4363,7 +4389,7 @@ translateCFG env (cfg :: TypedCFG ext blocks ghosts inits ret) =
       inits = typedFnHandleArgs h
       ghosts = typedFnHandleGhosts h
       retType = typedFnHandleRetType h in
-  flip runNilTypeTransM env $ lambdaExprCtx ctx $
+  runNilTypeTransM env checks $ lambdaExprCtx ctx $
 
   -- We translate retType before extending the expr context to contain another
   -- copy of inits, as it is easier to do it here
@@ -4441,7 +4467,7 @@ someCFGAndPermToName (SomeCFGAndPerm _ nm _ _) = nm
 someCFGAndPermLRT :: PermEnv -> SomeCFGAndPerm ext -> OpenTerm
 someCFGAndPermLRT env (SomeCFGAndPerm _ _ _
                        (FunPerm ghosts args ret perms_in perms_out)) =
-  flip runNilTypeTransM env $
+  runNilTypeTransM env noChecks $
   translateClosed (appendCruCtx ghosts args) >>= \ctx_trans ->
   piLRTTransM "arg" ctx_trans $ \ectx ->
   inCtxTransM ectx $
@@ -4470,9 +4496,9 @@ someCFGAndPermPtrPerm (SomeCFGAndPerm _ _ _ fun_perm) =
 -- each @tpi@ is the @i@th type in @lrts@
 tcTranslateCFGTupleFun ::
   HasPtrWidth w =>
-  PermEnv -> EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
+  PermEnv -> ChecksFlag -> EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
   (OpenTerm, OpenTerm)
-tcTranslateCFGTupleFun env endianness dlevel cfgs_and_perms =
+tcTranslateCFGTupleFun env checks endianness dlevel cfgs_and_perms =
   let lrts = map (someCFGAndPermLRT env) cfgs_and_perms in
   let lrts_tm =
         foldr (\lrt lrts' -> ctorOpenTerm "Prelude.LRT_Cons" [lrt,lrts'])
@@ -4497,7 +4523,8 @@ tcTranslateCFGTupleFun env endianness dlevel cfgs_and_perms =
   case cfg_and_perm of
     SomeCFGAndPerm sym _ cfg fun_perm ->
       debugTrace dlevel ("Type-checking " ++ show sym) $
-      translateCFG env' $ tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg
+      translateCFG env' checks $
+      tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg
 
 
 -- | Make a "coq-safe" identifier from a string that might contain
@@ -4525,13 +4552,12 @@ mkSafeIdent mnm nm =
 -- with the name @"n__tuple_fun"@ will also be added, where @n@ is the name
 -- associated with the first CFG in the list.
 tcTranslateAddCFGs ::
-  HasPtrWidth w =>
-  SharedContext -> ModuleName ->
-  PermEnv -> EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
+  HasPtrWidth w => SharedContext -> ModuleName -> PermEnv -> ChecksFlag ->
+  EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
   IO PermEnv
-tcTranslateAddCFGs sc mod_name env endianness dlevel cfgs_and_perms =
+tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
   do let (lrts, tup_fun) =
-           tcTranslateCFGTupleFun env endianness dlevel cfgs_and_perms
+           tcTranslateCFGTupleFun env checks endianness dlevel cfgs_and_perms
      let tup_fun_ident =
            mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms)
                                  ++ "__tuple_fun")
@@ -4567,15 +4593,13 @@ translateCompleteFunPerm :: SharedContext -> PermEnv ->
                             FunPerm ghosts args ret -> IO Term
 translateCompleteFunPerm sc env fun_perm =
   completeOpenTerm sc $
-  runNilTypeTransM (translate $ emptyMb fun_perm) env
+  runNilTypeTransM env noChecks (translate $ emptyMb fun_perm)
 
 -- | Translate a 'TypeRepr' to the SAW core type it represents
-translateCompleteType :: SharedContext -> PermEnv ->
-                         TypeRepr tp -> IO Term
+translateCompleteType :: SharedContext -> PermEnv -> TypeRepr tp -> IO Term
 translateCompleteType sc env typ_perm =
-  completeOpenTerm sc $
-  typeTransType1 $
-  runNilTypeTransM (translate $ emptyMb typ_perm) env
+  completeOpenTerm sc $ typeTransType1 $
+  runNilTypeTransM env noChecks $ translate $ emptyMb typ_perm
 
 -- | Translate a 'TypeRepr' within the given context of type arguments to the
 -- SAW core type it represents
@@ -4583,7 +4607,8 @@ translateCompleteTypeInCtx :: SharedContext -> PermEnv ->
                               CruCtx args -> Mb args (TypeRepr a) -> IO Term
 translateCompleteTypeInCtx sc env args ret =
   completeOpenTerm sc $
-  runNilTypeTransM (piExprCtx args (typeTransType1 <$> translate ret')) env
+  runNilTypeTransM env noChecks (piExprCtx args (typeTransType1 <$>
+                                                 translate ret'))
   where ret' = mbCombine (cruCtxProxies args) . emptyMb $ ret
 
 -- | Translate an input list of 'ValuePerms' and an output 'ValuePerm' to a SAW
@@ -4595,9 +4620,9 @@ translateCompletePureFun :: SharedContext -> PermEnv
                          -> Mb ctx (ValuePerm ret) -- ^ Return type perm
                          -> IO Term
 translateCompletePureFun sc env ctx args ret =
-  completeOpenTerm sc $
-  runNilTypeTransM (piExprCtx ctx $ piPermCtx args' $ const $
-                    typeTransTupleType <$> translate ret') env
+  completeOpenTerm sc $ runNilTypeTransM env noChecks $
+  piExprCtx ctx $ piPermCtx args' $ const $
+  typeTransTupleType <$> translate ret'
   where args' = mbCombine pxys . emptyMb $ args
         ret'  = mbCombine pxys . emptyMb $ ret
         pxys  = cruCtxProxies ctx
diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index be40a69f86..b23469556e 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -50,6 +50,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_export_coq
        , heapster_parse_test
        , heapster_set_debug_level
+       , heapster_set_translation_checks
        ) where
 
 import Data.Maybe
@@ -280,11 +281,13 @@ mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) =
            heapster_default_env globals
      env_ref <- liftIO $ newIORef env
      dlevel_ref <- liftIO $ newIORef dlevel
+     checks_ref <- liftIO $ newIORef doChecks
      return $ HeapsterEnv {
        heapsterEnvSAWModule = saw_mod_name,
        heapsterEnvPermEnvRef = env_ref,
        heapsterEnvLLVMModules = llvm_mods,
-       heapsterEnvDebugLevel = dlevel_ref
+       heapsterEnvDebugLevel = dlevel_ref,
+       heapsterEnvChecksFlag = checks_ref
        }
 mkHeapsterEnv _ _ [] = fail "mkHeapsterEnv: empty list of LLVM modules!"
 
@@ -617,8 +620,8 @@ heapster_define_reachability_perm _bic _opts henv
        let args_ctx = appendParsedCtx pre_args_ctx last_args_ctx
        let args = parsedCtxCtx args_ctx
        trans_tp <- liftIO $ 
-         translateCompleteTypeInCtx sc env args (nus (cruCtxProxies args) $
-                                                 const $ ValuePermRepr tp)
+         translateCompleteTypeInCtx sc env args $
+         nus (cruCtxProxies args) $ const $ ValuePermRepr tp
        trans_tp_ident <- parseAndInsDef henv nm trans_tp trans_tp_str
 
        -- Use permEnvAddRecPermM to tie the knot of adding a recursive
@@ -642,12 +645,12 @@ heapster_define_reachability_perm _bic _opts henv
                     (\ns -> ValPerm_Named npn (namesToExprs ns) NoPermOffset)
               -- Typecheck fold against body -o P<args>
               fold_fun_tp <- liftIO $
-                translateCompletePureFun sc tmp_env args (singletonValuePerms
-                                                          <$> or_tp) nm_tp
+                translateCompletePureFun sc tmp_env args (singletonValuePerms <$>
+                                                          or_tp) nm_tp
               -- Typecheck fold against P<args> -o body
               unfold_fun_tp <- liftIO $
-                translateCompletePureFun sc tmp_env args (singletonValuePerms
-                                                          <$> nm_tp) or_tp
+                translateCompletePureFun sc tmp_env args (singletonValuePerms <$>
+                                                          nm_tp) or_tp
               -- Build identifiers foldXXX and unfoldXXX
               fold_ident <-
                 parseAndInsDef henv ("fold" ++ nm) fold_fun_tp fold_fun_str
@@ -717,9 +720,8 @@ heapster_define_opaque_llvmshape _bic _opts henv nm w_int args_str len_str tp_st
      mb_len <- parseExprInCtxString env (BVRepr w) args_ctx len_str
      sc <- getSharedContext
      tp_tp <- liftIO $
-       translateCompleteTypeInCtx sc env args (nus (cruCtxProxies args) $
-                                               const $ ValuePermRepr $
-                                               LLVMShapeRepr w)
+       translateCompleteTypeInCtx sc env args $
+       nus (cruCtxProxies args) $ const $ ValuePermRepr $ LLVMShapeRepr w
      tp_id <- parseAndInsDef henv nm tp_tp tp_str
      let env' = withKnownNat w $ permEnvAddOpaqueShape env nm args mb_len tp_id
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
@@ -1035,6 +1037,7 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms =
            llvmDataLayout (modTrans lm ^. transContext ^. llvmTypeCtx)
            ^. intLayout
      dlevel <- liftIO $ readIORef $ heapsterEnvDebugLevel henv
+     checks <- liftIO $ readIORef $ heapsterEnvChecksFlag henv
      LeqProof <- case decideLeq (knownNat @16) w of
        Left pf -> return pf
        Right _ -> fail "LLVM arch width is < 16!"
@@ -1059,7 +1062,8 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms =
      let saw_modname = heapsterEnvSAWModule henv
      env' <- liftIO $
        let ?ptrWidth = w in
-       tcTranslateAddCFGs sc saw_modname env endianness dlevel some_cfgs_and_perms
+       tcTranslateAddCFGs sc saw_modname env checks endianness dlevel
+       some_cfgs_and_perms
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
 
@@ -1115,6 +1119,11 @@ heapster_set_debug_level :: BuiltinContext -> Options -> HeapsterEnv ->
 heapster_set_debug_level _ _ env l =
   liftIO $ writeIORef (heapsterEnvDebugLevel env) (DebugLevel l)
 
+heapster_set_translation_checks :: BuiltinContext -> Options -> HeapsterEnv ->
+                                   Bool -> TopLevel ()
+heapster_set_translation_checks _ _ env f =
+  liftIO $ writeIORef (heapsterEnvChecksFlag env) (ChecksFlag f)
+
 heapster_parse_test :: BuiltinContext -> Options -> Some LLVMModule ->
                        String -> String ->  TopLevel ()
 heapster_parse_test _bic _opts _some_lm@(Some lm) fn_name perms_string =
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index feb91cf3b1..0d2d48c0a9 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3317,6 +3317,13 @@ primitives = Map.fromList
     Experimental
     [ "Set the debug level for Heapster; 0 = no debug output, 1 = debug output" ]
 
+  , prim "heapster_set_translation_checks"
+    "HeapsterEnv -> Bool -> TopLevel ()"
+    (bicVal heapster_set_translation_checks)
+    Experimental
+    [ "Tell Heapster whether to perform its translation-time checks of the "
+    , "well-formedness of type-checking proofs" ]
+
   , prim "heapster_parse_test"
     "LLVMModule -> String -> String -> TopLevel ()"
     (bicVal heapster_parse_test)
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 34e178a4d6..f53f096456 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -110,6 +110,7 @@ import Lang.Crucible.LLVM.ArraySizeProfile
 import           What4.ProgramLoc (ProgramLoc(..))
 
 import Verifier.SAW.Heapster.Permissions
+import Verifier.SAW.Heapster.SAWTranslation (ChecksFlag)
 
 -- Values ----------------------------------------------------------------------
 
@@ -184,7 +185,10 @@ data HeapsterEnv = HeapsterEnv {
   -- ^ The current permissions environment
   heapsterEnvLLVMModules :: [Some CMSLLVM.LLVMModule],
   -- ^ The list of underlying 'LLVMModule's that we are translating
-  heapsterEnvDebugLevel :: IORef DebugLevel
+  heapsterEnvDebugLevel :: IORef DebugLevel,
+  -- ^ The current debug level
+  heapsterEnvChecksFlag :: IORef ChecksFlag
+  -- ^ Whether translation checks are currently enabled
   }
 
 showHeapsterEnv :: HeapsterEnv -> String

From 620f34989b5655d9cb8b8b123f165ddfbdb610ea Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 15 Nov 2021 17:18:03 -0800
Subject: [PATCH 02/10] Replaced a number of uses of fmap and mbMap2 with
 mbMapCl, to try to reduce the number of times name-bindings are converted
 between fresh function and fresh pair representations

---
 .../src/Verifier/SAW/Heapster/Permissions.hs  |   4 +
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 288 ++++++++++--------
 2 files changed, 162 insertions(+), 130 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 27a885f4b5..99da63276a 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -2474,6 +2474,10 @@ data DefinedPerm b args a = DefinedPerm {
 -- make certain typeclass instances (like pretty-printing) specific to it
 data VarAndPerm a = VarAndPerm (ExprVar a) (ValuePerm a)
 
+-- | Extract the permissions from a 'VarAndPerm'
+varAndPermPerm :: VarAndPerm a -> ValuePerm a
+varAndPermPerm (VarAndPerm _ p) = p
+
 -- | A list of "distinguished" permissions to named variables
 -- FIXME: just call these VarsAndPerms or something like that...
 type DistPerms = RAssign VarAndPerm
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 323190aa28..ffed3f4937 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -1260,7 +1260,8 @@ class ExtPermTrans f where
 
 instance ExtPermTrans PermTrans where
   extPermTrans (PTrans_Eq e) = PTrans_Eq $ extMb e
-  extPermTrans (PTrans_Conj aps) = PTrans_Conj (map extPermTrans aps)
+  extPermTrans (PTrans_Conj aps) =
+    PTrans_Conj (map extPermTrans aps)
   extPermTrans (PTrans_Defined n args a ptrans) =
     PTrans_Defined n (extMb args) (extMb a) (extPermTrans ptrans)
   extPermTrans (PTrans_Term p t) = PTrans_Term (extMb p) t
@@ -1419,6 +1420,9 @@ getLLVMArrayTransCell :: (1 <= w, KnownNat w) => LLVMArrayPermTrans ctx w ->
 getLLVMArrayTransCell arr_trans mb_cell cell_tm (BVPropTrans _ in_rng_pf:_) =
   let w = fromInteger $ natVal arr_trans in
   fromJust $
+  -- FIXME: remove offsetLLVMAtomicPermTrans, as it requires changing all
+  -- name-bindings in the PermTrans it is applied to back to FreshFuns, i.e., it
+  -- substitutes for all the names
   offsetLLVMAtomicPermTrans (mbMap2 llvmArrayCellToOffset
                              (llvmArrayTransPerm arr_trans) mb_cell) $
   typeTransF (llvmArrayTransHeadCell arr_trans)
@@ -2132,7 +2136,15 @@ translateSimplImplOutHead :: Mb ctx (SimplImpl ps_in (ps_out :> a)) ->
                              ImpTransM ext blocks tops ret ps ctx
                              (TypeTrans (PermTrans ctx a))
 translateSimplImplOutHead =
-  fmap (fmap RL.head) . translate . mbSimplImplOut
+  translate . mbMapCl $(mkClosed [| varAndPermPerm . RL.head |]) . mbSimplImplOut
+
+-- | Translate the head of the tail of the output permission of a 'SimplImpl'
+translateSimplImplOutTailHead :: Mb ctx (SimplImpl ps_in (ps_out :> a :> b)) ->
+                                 ImpTransM ext blocks tops ret ps ctx
+                                 (TypeTrans (PermTrans ctx a))
+translateSimplImplOutTailHead =
+  translate . mbMapCl $(mkClosed [| varAndPermPerm . RL.head . RL.tail |])
+  . mbSimplImplOut
 
 -- | Translate a 'SimplImpl' to a function on translation computations
 translateSimplImpl :: Proxy ps -> Mb ctx (SimplImpl ps_in ps_out) ->
@@ -2190,27 +2202,30 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_IntroOrL _ p1 p2 |] ->
     do tp1 <- translate p1
        tp2 <- translate p2
+       tptrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(ps :>: p_top) ->
-           ps :>: PTrans_Term (mbMap2 ValPerm_Or p1 p2) (leftTrans tp1 tp2 p_top))
+           ps :>: typeTransF tptrans [leftTrans tp1 tp2 p_top])
          m
 
   [nuMP| SImpl_IntroOrR _ p1 p2 |] ->
     do tp1 <- translate p1
        tp2 <- translate p2
+       tptrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(ps :>: p_top) ->
-           ps :>: PTrans_Term (mbMap2 ValPerm_Or p1 p2) (rightTrans tp1 tp2 p_top))
+           ps :>: typeTransF tptrans [rightTrans tp1 tp2 p_top])
          m
 
   [nuMP| SImpl_IntroExists _ e p |] ->
     do let tp = mbExprType e
        tp_trans <- translateClosed tp
+       out_trans <- translateSimplImplOutHead mb_simpl
        etrans <- translate e
        trm <- sigmaPermTransM "x_ex" tp_trans (mbCombine RL.typeCtxProxies p)
                               etrans getTopPermM
        withPermStackM id
-         ((:>: PTrans_Term (fmap ValPerm_Exists p) trm) . RL.tail)
+         (\(pctx :>: _) -> pctx :>: typeTransF out_trans [trm])
          m
 
   [nuMP| SImpl_Cast _ _ _ |] ->
@@ -2221,7 +2236,8 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_CastPerm (x::ExprVar a) eqp |] ->
     do ttrans <- translateSimplImplOutHead mb_simpl
        let prxs_a = MNil :>: (Proxy :: Proxy a)
-       let prxs1 = mbLift $ fmap (distPermsToProxies . eqProofPerms) eqp
+       let prxs1 = mbLift $ mbMapCl $(mkClosed [| distPermsToProxies
+                                                . eqProofPerms |]) eqp
        let prxs = RL.append prxs_a prxs1
        withPermStackM
          (\vars -> fst (RL.split ps0 prxs vars) :>: translateVar x)
@@ -2232,17 +2248,19 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_IntroEqRefl x |] ->
-    withPermStackM (:>: translateVar x) (:>: PTrans_Eq (fmap PExpr_Var x)) m
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM (:>: translateVar x)
+         (\pctx -> pctx :>: typeTransF ttrans []) m
 
-  [nuMP| SImpl_InvertEq x y |] ->
-    withPermStackM ((:>: translateVar y) . RL.tail)
-    ((:>: PTrans_Eq (fmap PExpr_Var x)) . RL.tail)
-    m
+  [nuMP| SImpl_InvertEq _ y |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM ((:>: translateVar y) . RL.tail)
+         (\(pctx :>: _) -> pctx :>: typeTransF ttrans []) m
 
-  [nuMP| SImpl_InvTransEq _ mb_y _ |] ->
-    withPermStackM RL.tail
-    ((:>: PTrans_Eq (fmap PExpr_Var mb_y)) . RL.tail . RL.tail)
-    m
+  [nuMP| SImpl_InvTransEq _ _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail
+         (\(pctx :>: _ :>: _) -> pctx :>: typeTransF ttrans []) m
 
   [nuMP| SImpl_CopyEq _ _ |] ->
     withPermStackM
@@ -2250,15 +2268,15 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     (\(pctx :>: ptrans) -> (pctx :>: ptrans :>: ptrans))
     m
 
-  [nuMP| SImpl_LLVMWordEq _ _ e |] ->
-    withPermStackM RL.tail
-    (\(pctx :>: _ :>: _) -> (pctx :>: PTrans_Eq (fmap PExpr_LLVMWord e)))
-    m
+  [nuMP| SImpl_LLVMWordEq _ _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail (\(pctx :>: _ :>: _) ->
+                                pctx :>: typeTransF ttrans []) m
 
   [nuMP| SImpl_LLVMOffsetZeroEq x |] ->
-    let bvZero = zeroOfType (BVRepr knownNat) in
-    withPermStackM (:>: translateVar x)
-                   (:>: PTrans_Eq (fmap (flip PExpr_LLVMOffset bvZero) x)) m
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM (:>: translateVar x)
+         (\pctx -> pctx :>: typeTransF ttrans []) m
 
   [nuMP| SImpl_IntroConj x |] ->
     withPermStackM (:>: translateVar x) (:>: PTrans_True) m
@@ -2308,81 +2326,78 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
       pctx :>: PTrans_Conj (take i ps) :>: PTrans_Conj (drop i ps))
     m
 
-  [nuMP| SImpl_IntroStructTrue x prxs |] ->
-    withPermStackM (:>: translateVar x)
-    (\pctx -> pctx :>: PTrans_Conj [APTrans_Struct $
-                                    RL.map (const PTrans_True) (mbRAssign prxs)])
-    m
+  [nuMP| SImpl_IntroStructTrue x _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM (:>: translateVar x)
+         (\pctx -> pctx :>: typeTransF tptrans [])
+         m
 
-  [nuMP| SImpl_StructEqToPerm _ exprs |] ->
-    withPermStackM id
-    (\(pctx :>: _) ->
-      pctx :>: PTrans_Conj [APTrans_Struct $
-                            RL.map (PTrans_Eq . getCompose)
-                            (mbRAssign $ fmap exprsToRAssign exprs)])
-    m
+  [nuMP| SImpl_StructEqToPerm _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM id
+         (\(pctx :>: _) -> pctx :>: typeTransF tptrans [])
+         m
 
-  [nuMP| SImpl_StructPermToEq _ exprs |] ->
-    withPermStackM id
-    (\(pctx :>: _) -> pctx :>: PTrans_Eq (fmap PExpr_Struct exprs))
-    m
+  [nuMP| SImpl_StructPermToEq _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM id
+         (\(pctx :>: _) -> pctx :>: typeTransF tptrans [])
+         m
 
   [nuMP| SImpl_IntroStructField _ _ memb _ |] ->
-    withPermStackM RL.tail
-    (\(pctx :>: PTrans_Conj [APTrans_Struct pctx_str] :>: ptrans) ->
-      pctx :>: PTrans_Conj [APTrans_Struct $
-                            RL.set (mbLift memb) ptrans pctx_str])
-    m
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail
+         (\(pctx :>: PTrans_Conj [APTrans_Struct pctx_str] :>: ptrans) ->
+           pctx :>: typeTransF tptrans (transTerms $
+                                        RL.set (mbLift memb) ptrans pctx_str))
+         m
 
-  [nuMP| SImpl_ConstFunPerm x _ mb_fun_perm ident |] ->
-    withPermStackM ((:>: translateVar x) . RL.tail)
-    ((:>: PTrans_Term (fmap (ValPerm_Conj1
-                             . Perm_Fun) mb_fun_perm) (globalOpenTerm $
-                                                       mbLift ident))
-     . RL.tail)
-    m
+  [nuMP| SImpl_ConstFunPerm _ _ _ ident |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM id
+         (\(pctx :>: _) ->
+           pctx :>: typeTransF tptrans [globalOpenTerm $ mbLift ident])
+         m
 
-  [nuMP| SImpl_CastLLVMWord _ _ e2 |] ->
-    withPermStackM RL.tail
-    ((:>: PTrans_Eq (fmap PExpr_LLVMWord e2)) . RL.tail . RL.tail)
-    m
+  [nuMP| SImpl_CastLLVMWord _ _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail
+         (\(pctx :>: _ :>: _) ->
+           pctx :>: typeTransF tptrans [])
+         m
 
-  [nuMP| SImpl_InvertLLVMOffsetEq mb_x mb_off mb_y |] ->
-    withPermStackM
-    ((:>: translateVar mb_y) . RL.tail)
-    ((:>: PTrans_Eq (mbMap2 (\x off -> PExpr_LLVMOffset x $
-                                       bvNegate off) mb_x mb_off)) . RL.tail)
-    m
+  [nuMP| SImpl_InvertLLVMOffsetEq _ _ mb_y |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM
+         (\(vars :>: _) -> (vars :>: translateVar mb_y))
+         (\(pctx :>: _) -> pctx :>: typeTransF tptrans [])
+         m
 
-  [nuMP| SImpl_OffsetLLVMWord _ mb_e mb_off mb_x |] ->
-    withPermStackM
-    ((:>: translateVar mb_x) . RL.tail . RL.tail)
-    ((:>: PTrans_Eq (mbMap2 (\e off -> PExpr_LLVMWord $ bvAdd e off)
-                     mb_e mb_off)) . RL.tail . RL.tail)
-    m
+  [nuMP| SImpl_OffsetLLVMWord _ _ _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM
+         (\(vars :>: _ :>: x_var) -> vars :>: x_var)
+         (\(pctx :>: _ :>: _) -> pctx :>: typeTransF tptrans [])
+         m
 
-  [nuMP| SImpl_CastLLVMPtr _ _ off _ |] ->
-    withPermStackM RL.tail
-    (\(pctx :>: _ :>: ptrans) ->
-      pctx :>: offsetLLVMPermTrans (fmap bvNegate off) ptrans)
-    m
+  [nuMP| SImpl_CastLLVMPtr _ _ _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail
+         (\(pctx :>: _ :>: ptrans) ->
+           pctx :>: typeTransF tptrans (transTerms ptrans))
+         m
 
   [nuMP| SImpl_CastLLVMFree _ _ e2 |] ->
     withPermStackM RL.tail
     ((:>: PTrans_Conj [APTrans_LLVMFree e2]) . RL.tail . RL.tail)
     m
 
-  [nuMP| SImpl_CastLLVMFieldOffset _ mb_fld mb_off |] ->
-    withPermStackM RL.tail
-    (\(pctx :>: _ :>: ptrans) ->
-      let (_,ptrans') =
-            unPTransLLVMField "translateSimplImpl: SImpl_CastLLVMFieldOffset"
-            knownNat ptrans in
-      pctx :>: PTrans_Conj [APTrans_LLVMField
-                            (mbMap2 (\fld off -> fld { llvmFieldOffset = off })
-                             mb_fld mb_off)
-                            ptrans'])
-    m
+  [nuMP| SImpl_CastLLVMFieldOffset _ _ _ |] ->
+    do tptrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail
+         (\(pctx :>: ptrans :>: _) ->
+           pctx :>: typeTransF tptrans (transTerms ptrans))
+         m
 
   [nuMP| SImpl_IntroLLVMFieldContents x _ mb_fld |] ->
     withPermStackM ((:>: translateVar x) . RL.tail . RL.tail)
@@ -2397,9 +2412,10 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
             unPTransLLVMField
             "translateSimplImpl: SImpl_DemoteLLVMFieldRW"
             knownNat ptrans in
-      pctx :>: PTrans_Conj [APTrans_LLVMField
-                            (fmap (\fld -> fld { llvmFieldRW = PExpr_Read }) mb_fld)
-                            ptrans'])
+      pctx :>: PTrans_Conj [
+        APTrans_LLVMField
+        (mbMapCl $(mkClosed [| \fld -> fld { llvmFieldRW = PExpr_Read } |]) mb_fld)
+        ptrans'])
     m
 
   [nuMP| SImpl_SplitLLVMWordField x _ _ _ _ |] ->
@@ -2705,6 +2721,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     do pctx_out_trans <- translateSimplImplOut mb_simpl
        ps_in_trans <- translate ps_in
        ps_out_trans <- translate ps_out
+       -- FIXME: write a fun to translate-and-apply a lifetimefunctor
        x_tp_trans <- translate (mbMap3 ltFuncApply f args l)
        withPermStackM
          (\(ns :>: x :>: _ :>: l2) -> ns :>: x :>: l2)
@@ -2848,15 +2865,13 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            m]
 
   [nuMP| SImpl_LCurrentRefl l |] ->
-    withPermStackM (:>: translateVar l)
-    (:>: PTrans_Conj [APTrans_LCurrent $ fmap PExpr_Var l])
-    m
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM (:>: translateVar l) (:>: typeTransF ttrans []) m
 
-  [nuMP| SImpl_LCurrentTrans _l1 _l2 l3 |] ->
-    withPermStackM RL.tail
-    ((:>: PTrans_Conj [APTrans_LCurrent l3]) .
-     RL.tail . RL.tail)
-    m
+  [nuMP| SImpl_LCurrentTrans _ _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
+       withPermStackM RL.tail (\(pctx :>: _ :>: _) ->
+                                (pctx :>: typeTransF ttrans [])) m
 
   [nuMP| SImpl_DemoteLLVMBlockRW _ _ |] ->
     do ttrans <- translateSimplImplOutHead mb_simpl
@@ -3086,21 +3101,18 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                                                 ++ [transTerm1 ptrans_x])])
          m
 
-  [nuMP| SImpl_FoldNamed _ (NamedPerm_Defined dp) args off |] ->
-    do folded_trans <-
-         translate (mbMap2 ValPerm_Named (fmap definedPermName dp) args
-                    `mbApply` off)
+  [nuMP| SImpl_FoldNamed _ (NamedPerm_Defined _) _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
-           pctx :>: typeTransF folded_trans (transTerms ptrans))
+           pctx :>: typeTransF ttrans (transTerms ptrans))
          m
 
-  [nuMP| SImpl_UnfoldNamed _ (NamedPerm_Defined dp) args off |] ->
-    do unfolded_trans <-
-         translate (mbMap2 unfoldDefinedPerm dp args `mbApply` off)
+  [nuMP| SImpl_UnfoldNamed _ (NamedPerm_Defined _) _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
-           pctx :>: typeTransF unfolded_trans (transTerms ptrans))
+           pctx :>: typeTransF ttrans (transTerms ptrans))
          m
 
   {-
@@ -3145,7 +3157,8 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
 
   [nuMP| SImpl_ReachabilityTrans _ rp args _ y e |] ->
-    do args_trans <- translate $ mbMap2 PExprs_Cons args e
+    do args_trans <- translate args
+       e_trans <- translate e
        y_trans <- translate y
        e_trans <- translate e
        ttrans <- translateSimplImplOutHead mb_simpl
@@ -3156,6 +3169,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            typeTransF (tupleTypeTrans ttrans) [applyOpenTermMulti
                                                (globalOpenTerm trans_ident)
                                                (transTerms args_trans
+                                                ++ transTerms e_trans
                                                 ++ transTerms y_trans
                                                 ++ transTerms e_trans
                                                 ++ [transTerm1 ptrans_x,
@@ -3315,7 +3329,11 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
       (Nothing, Nothing) -> mzero
       _ ->
         return $ \k ->
-        do () <- assertTopPermM "Impl1_ElimOr" x (mbMap2 ValPerm_Or p1 p2)
+        do let mb_p1_or_p2 =
+                 mbMapCl $(mkClosed
+                           [| \(Impl1_ElimOr _ p1 p2) -> ValPerm_Or p1 p2 |])
+                 mb_impl
+           () <- assertTopPermM "Impl1_ElimOr" x mb_p1_or_p2
            tp1 <- translate p1
            tp2 <- translate p2
            tp_ret <- compReturnTypeTransM
@@ -3366,7 +3384,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
        let etrans_y = case etrans_x of
              ETrans_Struct flds -> RL.get (mbLift memb) flds
              _ -> error "translatePermImpl1: Impl1_ElimStructField"
-       let mb_y = mbCombine RL.typeCtxProxies $ fmap (const $ nu $ \y -> PExpr_Var y) x
+       let mb_y = mbCombine RL.typeCtxProxies $ fmap (const $ nu $ \y ->
+                                                       PExpr_Var y) x
        inExtTransM etrans_y $
          withPermStackM (:>: Member_Base)
          (\(pctx :>: PTrans_Conj [APTrans_Struct pctx_str]) ->
@@ -3383,29 +3402,33 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
       let (_,ptrans') =
             unPTransLLVMField "translatePermImpl1: Impl1_ElimLLVMFieldContents"
             knownNat ptrans_x in
-      pctx :>: PTrans_Conj [APTrans_LLVMField
-                            (mbCombine RL.typeCtxProxies $
-                             fmap (\fld -> nu $ \y ->
-                                    fld { llvmFieldContents =
-                                            ValPerm_Eq (PExpr_Var y)})
-                             mb_fld) $
-                            PTrans_Eq (mbCombine RL.typeCtxProxies $
-                                       fmap (const $ nu PExpr_Var) mb_fld)]
+      pctx :>: PTrans_Conj [
+        APTrans_LLVMField
+        (mbCombine RL.typeCtxProxies $
+         mbMapCl $(mkClosed [| \fld -> nu $ \y ->
+                              llvmFieldSetEqVar fld y |]) mb_fld) $
+        PTrans_Eq (mbCombine RL.typeCtxProxies $
+                   fmap (const $ nu PExpr_Var) mb_fld)]
       :>: ptrans')
     m
 
   ([nuMP| Impl1_ElimLLVMBlockToEq _ mb_bp |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     inExtTransM ETrans_LLVMBlock $
-    do tp_trans1 <-
-         translate (mbMap2 (\bp y ->
-                             ValPerm_Conj1 $ Perm_LLVMBlock $
-                             bp { llvmBlockShape = PExpr_EqShape $ PExpr_Var y })
-                    (extMb mb_bp) $
-                    nuMulti (mbToProxy mb_bp :>: Proxy) (\(_ :>: y) -> y))
-       tp_trans2 <-
-         translate $ fmap (ValPerm_Conj1 .
-                           Perm_LLVMBlockShape . modalizeBlockShape) (extMb mb_bp)
+    do let mb_p_out1 =
+             mbCombine RL.typeCtxProxies $
+             mbMapCl $(mkClosed
+                       [| \bp -> nu $ \y ->
+                         ValPerm_Conj1 $ Perm_LLVMBlock $
+                         bp { llvmBlockShape = PExpr_EqShape $ PExpr_Var y } |])
+             mb_bp
+       tp_trans1 <- translate mb_p_out1
+       let mb_p_out2 =
+             mbMapCl $(mkClosed
+                       [| ValPerm_Conj1
+                        . Perm_LLVMBlockShape . modalizeBlockShape |]) $
+             extMb mb_bp
+       tp_trans2 <- translate mb_p_out2
        withPermStackM (:>: Member_Base)
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans1 [unitOpenTerm] :>:
@@ -4074,10 +4097,12 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
     m
 
   [nuMP| OffsetLLVMValue x off |] ->
+    let mb_x_off =
+          mbMapCl $(mkClosed [| \(OffsetLLVMValue x off) ->
+                               PExpr_LLVMOffset (typedRegVar x) off |])
+          mb_stmt in
     inExtTransM ETrans_LLVM $
-    withPermStackM (:>: Member_Base)
-    (:>: (PTrans_Eq $ extMb $
-          mbMap2 PExpr_LLVMOffset (fmap typedRegVar x) off))
+    withPermStackM (:>: Member_Base) (:>: (PTrans_Eq $ extMb $ mb_x_off))
     m
 
   [nuMP| TypedLLVMLoad _ (mb_fp :: LLVMFieldPerm w sz)
@@ -4096,9 +4121,9 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
       RL.append
       (pctx :>: PTrans_Conj [APTrans_LLVMField
                              (mbCombine RL.typeCtxProxies $
-                              fmap (\fp -> nu $ \ret ->
-                                     fp { llvmFieldContents =
-                                            ValPerm_Eq (PExpr_Var ret)}) mb_fp)
+                              mbMapCl $(mkClosed
+                                        [| \fp -> nu $ \ret ->
+                                          llvmFieldSetEqVar fp ret |]) mb_fp)
                              (PTrans_Eq $ mbCombine RL.typeCtxProxies $
                               fmap (const $ nu $ \ret -> PExpr_Var ret) mb_fp)]
        :>: p_ret) pctx_l)
@@ -4177,8 +4202,11 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
     inExtTransM ETrans_LLVM $
     do b <- translate1 $ extMb mb_r1
        tptrans <-
-         translate $ mbCombine RL.typeCtxProxies $ flip fmap mb_stmt $ \stmt -> nu $ \ret ->
-         distPermsHeadPerm $ typedLLVMStmtOut stmt ret
+         translate $ mbCombine RL.typeCtxProxies $
+         mbMapCl $(mkClosed
+                   [| \stmt -> nu $ \ret ->
+                     distPermsHeadPerm $ typedLLVMStmtOut stmt ret |])
+         mb_stmt
        let t = applyOpenTerm (globalOpenTerm "Prelude.boolToEither") b
        withPermStackM (:>: Member_Base) (:>: typeTransF tptrans [t]) m
 

From 4835d6dcc7d7135e676604653085b5864eeff99a Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 15 Nov 2021 17:23:49 -0800
Subject: [PATCH 03/10] updated CruUtil.hs to handle a recent change to
 Crucible

---
 heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
index b4cfb28551..20983505bb 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -288,7 +288,7 @@ instance NuMatching ByteString where
 instance NuMatching (MemoryError sym) where
   nuMatchingProof = unsafeMbTypeRepr
 
-instance NuMatching MemoryErrorReason where
+instance NuMatching (MemoryErrorReason a b) where
   nuMatchingProof = unsafeMbTypeRepr
 
 instance NuMatching (FnHandle args ret) where

From 6bfc52a34985aca5c31bf79e66b8ee38c373085b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 15 Nov 2021 17:24:00 -0800
Subject: [PATCH 04/10] removed unused variables

---
 heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index ffed3f4937..78707e0300 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -3160,7 +3160,6 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     do args_trans <- translate args
        e_trans <- translate e
        y_trans <- translate y
-       e_trans <- translate e
        ttrans <- translateSimplImplOutHead mb_simpl
        let trans_ident = mbLift $ fmap recPermTransMethod rp
        withPermStackM RL.tail
@@ -3318,7 +3317,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
 
   -- If both branches of an or elimination fail, the whole thing fails; otherwise,
   -- an or elimination performs a pattern-match on an Either
-  ([nuMP| Impl1_ElimOr x p1 p2 |],
+  ([nuMP| Impl1_ElimOr x mb_p1 mb_p2 |],
    [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
     pitmCatching (translatePermImpl prx $
                   mbCombine RL.typeCtxProxies mb_impl1) >>= \(mtrans1,hasf1) ->
@@ -3334,8 +3333,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                            [| \(Impl1_ElimOr _ p1 p2) -> ValPerm_Or p1 p2 |])
                  mb_impl
            () <- assertTopPermM "Impl1_ElimOr" x mb_p1_or_p2
-           tp1 <- translate p1
-           tp2 <- translate p2
+           tp1 <- translate mb_p1
+           tp2 <- translate mb_p2
            tp_ret <- compReturnTypeTransM
            top_ptrans <- getTopPermM
            eitherElimTransM tp1 tp2 tp_ret
@@ -4096,7 +4095,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
     ((:>: (PTrans_Eq $ extMb e)) . RL.tail)
     m
 
-  [nuMP| OffsetLLVMValue x off |] ->
+  [nuMP| OffsetLLVMValue _ _ |] ->
     let mb_x_off =
           mbMapCl $(mkClosed [| \(OffsetLLVMValue x off) ->
                                PExpr_LLVMOffset (typedRegVar x) off |])

From 6d3bf5bb85442c593691c31208b1360d3c21a562 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 16 Nov 2021 06:09:11 -0800
Subject: [PATCH 05/10] whoops, undid that recent change to CruUtil.hs because
 it looks like that was for an older version of Crucible...

---
 heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
index 20983505bb..b4cfb28551 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -288,7 +288,7 @@ instance NuMatching ByteString where
 instance NuMatching (MemoryError sym) where
   nuMatchingProof = unsafeMbTypeRepr
 
-instance NuMatching (MemoryErrorReason a b) where
+instance NuMatching MemoryErrorReason where
   nuMatchingProof = unsafeMbTypeRepr
 
 instance NuMatching (FnHandle args ret) where

From 98fb656e2131fe1e8366901e94e0b35a42618041 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 16 Nov 2021 06:37:03 -0800
Subject: [PATCH 06/10] changed the translation of the catch rule to not
 translate the second branch if the first one succeeds

---
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 43 ++++++++++++-------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 78707e0300..bc18d7f25e 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -3281,22 +3281,33 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
   ([nuMP| Impl1_Catch |],
    [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
     pitmCatching (translatePermImpl prx $
-                  mbCombine RL.typeCtxProxies mb_impl1) >>= \(mtrans1,hasf1) ->
-    pitmCatching (translatePermImpl prx $
-                  mbCombine RL.typeCtxProxies mb_impl2) >>= \(mtrans2,hasf2) ->
-    (if hasf1 == HasFailures && hasf2 == HasFailures then tell ([],HasFailures)
-     else return ()) >>
-    case (mtrans1, hasf1, mtrans2, hasf2) of
-      (Just trans, NoFailures, _, _) -> return trans
-      (_, _, Just trans, NoFailures) -> return trans
-      (Just trans1, _, Just trans2, _) ->
-        return $ \k ->
-        compReturnTypeM >>= \ret_tp ->
-        letTransM "catchpoint" ret_tp (trans2 k)
-        (\catchpoint -> trans1 $ ImplFailContTerm catchpoint)
-      (Just trans, _, Nothing, _) -> return trans
-      (Nothing, _, Just trans, _) -> return trans
-      (Nothing, _, Nothing, _) -> mzero
+                  mbCombine RL.typeCtxProxies mb_impl1) >>= \case
+    -- Short-circuit: if mb_impl1 succeeds, don't translate mb_impl2
+    (Just trans, NoFailures) -> return trans
+    (mtrans1, hasf1) ->
+      pitmCatching (translatePermImpl prx $
+                    mbCombine RL.typeCtxProxies mb_impl2) >>= \(mtrans2,
+                                                                hasf2) ->
+
+      -- Only report the possibility of failures if both branches have them
+      (if hasf1 == HasFailures && hasf2 == HasFailures
+       then tell ([],HasFailures)
+       else return ()) >>
+
+      -- Combine the two continuations
+      case (mtrans1, hasf1, mtrans2, hasf2) of
+        -- If mb_impl2 has no failures, drop mb_impl1
+        (_, _, Just trans, NoFailures) -> return trans
+        -- If both sides are defined but have failures, insert a catchpoint
+        (Just trans1, _, Just trans2, _) ->
+          return $ \k ->
+          compReturnTypeM >>= \ret_tp ->
+          letTransM "catchpoint" ret_tp (trans2 k)
+          (\catchpoint -> trans1 $ ImplFailContTerm catchpoint)
+        -- Otherwise, use whichever side is defined
+        (Just trans, _, Nothing, _) -> return trans
+        (Nothing, _, Just trans, _) -> return trans
+        (Nothing, _, Nothing, _) -> mzero
 
   -- A push moves the given permission from x to the top of the perm stack
   ([nuMP| Impl1_Push x p |], _) ->

From 78d6ee32917e0fe11bed25efebd0458c86db124d Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 16 Nov 2021 08:55:03 -0800
Subject: [PATCH 07/10] added tracing information to implCatchM, to see where
 catches and backtracking happen

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 54 +++++++++++++------
 .../src/Verifier/SAW/Heapster/Permissions.hs  |  8 +++
 .../Verifier/SAW/Heapster/TypedCrucible.hs    |  3 +-
 3 files changed, 48 insertions(+), 17 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 16914f0f5e..30e1c4faaf 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -2989,15 +2989,18 @@ withExtVarsMultiM (ctx :>: KnownReprObj) m =
   withExtVarsMultiM ctx (withExtVarsM m >>>= \(a,_) -> return a)
 
 -- | Perform either the first, second, or both computations with an 'implCatchM'
--- between, depending on the recursion flag
-implRecFlagCaseM :: NuMatchingAny1 r => ImplM vars s r ps_out ps_in a ->
+-- between, depending on the recursion flag. The 'String' names the function
+-- that is calling 'implCatchM', while the @p@ argument states what we are
+-- trying to prove; both of these are used for debug tracing.
+implRecFlagCaseM :: NuMatchingAny1 r => PermPretty p => String -> p ->
+                    ImplM vars s r ps_out ps_in a ->
                     ImplM vars s r ps_out ps_in a ->
                     ImplM vars s r ps_out ps_in a
-implRecFlagCaseM m1 m2 =
+implRecFlagCaseM f p m1 m2 =
   use implStateRecRecurseFlag >>>= \case
     RecLeft  -> m1
     RecRight -> m2
-    RecNone  -> implCatchM m1 m2
+    RecNone  -> implCatchM f p m1 m2
 
 -- | Set the recursive permission recursion flag to indicate recursion on the
 -- right, or fail if we are already recursing on the left
@@ -3186,14 +3189,27 @@ implFailVarM f x p mb_p =
   implFailM
 
 -- | Produce a branching proof tree that performs the first implication and, if
--- that one fails, falls back on the second. If 'pruneFailingBranches' is set,
--- failing branches are pruned.
-implCatchM :: NuMatchingAny1 r =>
+-- that one fails, falls back on the second. The supplied 'String' says what
+-- proof-search function is performing the catch, while the @p@ argument says
+-- what we are trying to prove; both of these are for debugging purposes, and
+-- are used in the debug trace.
+implCatchM :: NuMatchingAny1 r => PermPretty p => String -> p ->
               ImplM vars s r ps1 ps2 a -> ImplM vars s r ps1 ps2 a ->
               ImplM vars s r ps1 ps2 a
-implCatchM m1 m2 =
-  implApplyImpl1 Impl1_Catch (MNil :>: Impl1Cont (const m1)
-                              :>: Impl1Cont (const m2))
+implCatchM f p m1 m2 =
+  implApplyImpl1
+    Impl1_Catch
+    (MNil
+     :>: Impl1Cont (const $
+                    implTraceM (\i -> pretty ("Inserting catch in " ++ f
+                                              ++ " for proving:")
+                                      <> line <> permPretty i p) >>>
+                    m1)
+     :>: Impl1Cont (const $
+                    implTraceM (\i -> pretty ("Backtracking to catch in " ++ f
+                                              ++ " for proving:")
+                                      <> line <> permPretty i p) >>>
+                    m2))
 
 -- | "Push" all of the permissions in the permission set for a variable, which
 -- should be equal to the supplied permission, after deleting those permissions
@@ -4624,7 +4640,8 @@ implGetLLVMPermForOffset x ps imprecise_p elim_blocks_p off mb_p =
           -- FIXME: handle eq perms here
           _ -> implFailVarM "implGetLLVMPermForOffset" x (ValPerm_Conj ps) mb_p)
     ixs ->
-      foldr1 implCatchM $ flip map ixs $ \i ->
+      foldr1 (implCatchM "implGetLLVMPermForOffset" (ColonPair x mb_p)) $
+      flip map ixs $ \i ->
       implExtractConjM x ps i >>>
       let ps' = deleteNth i ps in
       recombinePerm x (ValPerm_Conj ps') >>>
@@ -6558,7 +6575,9 @@ proveVarLLVMBlocks2 x ps psubst mb_bp _ mb_bps
           let len =
                 mbLift $ mbMapCl $(mkClosed [| length .
                                              taggedUnionDisjs |]) mb_tag_u in
-          foldr1 implCatchM $ map return [0..len-1]) >>>= \i ->
+          foldr1 (implCatchM "proveVarLLVMBlocks2"
+                  (ColonPair x (mb_bp:mb_bps))) $
+          map return [0..len-1]) >>>= \i ->
 
     -- Get the permissions we now have for x and push them back to the top of
     -- the stack
@@ -6588,7 +6607,8 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
 
     -- Build a computation that tries returning True here, and if that fails
     -- returns False; True is used for sh1 while False is used for sh2
-    implCatchM (pure True) (pure False) >>>= \is_case1 ->
+    implCatchM "proveVarLLVMBlocks2" (ColonPair x (mb_bp:mb_bps))
+               (pure True) (pure False) >>>= \is_case1 ->
 
     -- Prove the chosen shape by recursively calling proveVarLLVMBlocks
     let mb_sh' = if is_case1 then mb_sh1 else mb_sh2 in
@@ -7220,7 +7240,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
   -- Prove x:(p1 \/ p2) by trying to prove x:p1 and x:p2 in two branches
   (_, [nuMP| ValPerm_Or mb_p1 mb_p2 |]) ->
     implPopM x p >>>
-    implCatchM
+    implCatchM "proveVarImplH" (ColonPair x mb_p)
     (proveVarImplInt x mb_p1 >>>
      partialSubstForceM mb_p1 "proveVarImpl" >>>= \p1 ->
      partialSubstForceM mb_p2 "proveVarImpl" >>>= \p2 ->
@@ -7246,7 +7266,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
     , NameReachConstr <- namedPermNameReachConstr npn
     , PExprs_Cons args1_pre e1 <- args1
     , [nuMP| PExprs_Cons mb_args2_pre mb_e2 |] <- mbMatch mb_args2 ->
-      implCatchM
+      implCatchM "proveVarImplH" (ColonPair x mb_p)
 
       -- Reflexivity branch: pop x:P<...>, prove x:eq(e), and use reflexivity
       (implPopM x p >>> proveVarImplInt x (fmap ValPerm_Eq mb_e2) >>>
@@ -7324,6 +7344,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
     | RecursiveSortRepr _ _ <- namedPermNameSort npn1
     , RecursiveSortRepr _ _ <- namedPermNameSort $ mbLift mb_npn2 ->
       implRecFlagCaseM
+      "proveVarImplH" (ColonPair x mb_p)
       (proveVarImplFoldRight x p mb_p)
       (proveVarImplUnfoldLeft x p mb_p Nothing)
 
@@ -7335,6 +7356,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
     | Just i <- findIndex isRecursiveConjPerm ps
     , RecursiveSortRepr _ _ <- namedPermNameSort $ mbLift mb_npn ->
       implRecFlagCaseM
+      "proveVarImplH" (ColonPair x mb_p)
       (proveVarImplUnfoldLeft x p mb_p (Just i))
       (proveVarImplFoldRight x p mb_p)
 
@@ -7730,7 +7752,7 @@ proveVarsImplAppend :: NuMatchingAny1 r => ExDistPerms vars ps ->
 proveVarsImplAppend mb_ps =
   use implStatePerms >>>= \(_ :: PermSet ps_in) ->
   lifetimesThatCouldProve mb_ps >>>= \ls_ps ->
-  foldr1 implCatchM
+  foldr1 (implCatchM "proveVarsImplAppend" mb_ps)
   ((proveVarsImplAppendInt mb_ps)
    :
    flip map ls_ps
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 99da63276a..7f7066474c 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -2478,6 +2478,9 @@ data VarAndPerm a = VarAndPerm (ExprVar a) (ValuePerm a)
 varAndPermPerm :: VarAndPerm a -> ValuePerm a
 varAndPermPerm (VarAndPerm _ p) = p
 
+-- | A pair that is specifically pretty-printing with a colon
+data ColonPair a b = ColonPair a b
+
 -- | A list of "distinguished" permissions to named variables
 -- FIXME: just call these VarsAndPerms or something like that...
 type DistPerms = RAssign VarAndPerm
@@ -3061,6 +3064,11 @@ instance PermPretty (VarAndPerm a) where
 instance PermPrettyF VarAndPerm where
   permPrettyMF = permPrettyM
 
+instance (PermPretty a, PermPretty b) => PermPretty (ColonPair a b) where
+  permPrettyM (ColonPair a b) =
+    (\pp1 pp2 -> pp1 <> colon <> pp2) <$> permPrettyM a <*> permPrettyM b
+
+
 {-
 instance PermPretty (DistPerms ps) where
   permPrettyM ps = ppCommaSep <$> helper ps where
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 55451b73b5..c94d803119 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -2970,7 +2970,8 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) =
           pure (if could then Just (SomeFunPerm fun_perm) else Nothing)
         _ -> pure Nothing
       _ -> pure []) >>>= \maybe_fun_perms ->
-  (stmtEmbedImplM $ foldr1WithDefault implCatchM
+  (stmtEmbedImplM $ foldr1WithDefault (implCatchM "tcEmitStmt (fun perm)" $
+                                       typedRegVar freg)
    (implFailMsgM "Could not find function permission")
    (mapMaybe (fmap pure) maybe_fun_perms)) >>>= \some_fun_perm ->
   case some_fun_perm of

From 97027a3d36db34e92a128e7c17d4981c5f141d02 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Tue, 16 Nov 2021 09:05:35 -0800
Subject: [PATCH 08/10] Update opam install arguments to support v2.1 or later.

---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 88198aeaab..5f287f180b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -226,7 +226,7 @@ jobs:
 
       - run: opam repo add coq-released https://coq.inria.fr/opam/released
 
-      - run: opam install --unlock-base -y coq=8.12.2 coq-bits=1.0.0
+      - run: opam install --update-invariant -y coq=8.12.2 coq-bits=1.0.0
 
       # FIXME: the following builds the Coq libraries for the SAW core
       # to Coq translator; if we do other Coq tests, this should become

From a7ae7bdb214bb3fb24e731dea847ed95a0f13008 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 16 Nov 2021 11:07:54 -0800
Subject: [PATCH 09/10] tweaked the tracing messages in implCatchM

---
 heapster-saw/src/Verifier/SAW/Heapster/Implication.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 30e1c4faaf..c2c9888ece 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -3197,16 +3197,18 @@ implCatchM :: NuMatchingAny1 r => PermPretty p => String -> p ->
               ImplM vars s r ps1 ps2 a -> ImplM vars s r ps1 ps2 a ->
               ImplM vars s r ps1 ps2 a
 implCatchM f p m1 m2 =
+  implTraceM (\i -> pretty ("Inserting catch in " ++ f ++ " for proving:")
+                    <> line <> permPretty i p) >>>
   implApplyImpl1
     Impl1_Catch
     (MNil
      :>: Impl1Cont (const $
-                    implTraceM (\i -> pretty ("Inserting catch in " ++ f
+                    implTraceM (\i -> pretty ("Case 1 of catch in " ++ f
                                               ++ " for proving:")
                                       <> line <> permPretty i p) >>>
                     m1)
      :>: Impl1Cont (const $
-                    implTraceM (\i -> pretty ("Backtracking to catch in " ++ f
+                    implTraceM (\i -> pretty ("Case 2 of catch in " ++ f
                                               ++ " for proving:")
                                       <> line <> permPretty i p) >>>
                     m2))

From e547a6cfcfcecbae34090138f1255413d84198fb Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 16 Nov 2021 12:29:15 -0800
Subject: [PATCH 10/10] renamed unChecksFlag to checksFlagSet

---
 heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index bc18d7f25e..79e2b3aff3 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -611,7 +611,7 @@ instance (Translate info ctx a tr, NuMatching a) =>
 
 -- | A flag for whether or not to perform checks in the translation. We use this
 -- type, rather than just 'Bool', for documentation purposes.
-newtype ChecksFlag = ChecksFlag { unChecksFlag :: Bool }
+newtype ChecksFlag = ChecksFlag { checksFlagSet :: Bool }
 
 -- | The 'ChecksFlag' specifying not to perform any translation checks
 noChecks :: ChecksFlag
@@ -1999,7 +1999,7 @@ ifChecksFlagM :: ImpTransM ext blocks tops ret ps ctx () ->
                  ImpTransM ext blocks tops ret ps ctx ()
 ifChecksFlagM m =
   (itiChecksFlag <$> ask) >>= \checks ->
-  if unChecksFlag checks then m else return ()
+  if checksFlagSet checks then m else return ()
 
 -- | Assert a property of the current permission stack, raising an 'error' if it
 -- fails to hold. The 'String' names the construct being translated.