From 82a4acaec0c1474b46d0b0602fb3c98cff5f7cf3 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 23 Nov 2021 13:22:26 -0800
Subject: [PATCH 01/11] short-circut true `BVProp_Neq`s in the translation

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

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 72eb1af7d3..5dd818cdba 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -3606,6 +3606,13 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
          , applyMultiTransM (return $ globalOpenTerm "Prelude.bvEqWithProof")
            [ return (natOpenTerm $ natVal2 prop) , translate1 e1, translate1 e2]]
 
+  -- If e1 and e2 are already unequal, short-circuit and do nothing
+  ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) _ |], _)
+    | not $ mbLift (mbMap2 bvCouldEqual e1 e2) ->
+      translatePermImplUnary mb_impls $
+        withPermStackM (:>: translateVar x)
+          (:>: PTrans_Conj [APTrans_BVProp (BVPropTrans prop unitOpenTerm)])
+
   -- For an inequality test, we don't need a proof, so just insert an if
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->

From bc0fd6ea06a75da20d5b2b01b9d2e0e4f6f065fd Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 23 Nov 2021 15:36:46 -0800
Subject: [PATCH 02/11] fixed a bug in splitLLVMBlockPerm

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

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index eef99a5381..f7e605c410 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -3945,7 +3945,7 @@ splitLLVMBlockPerm off bp
 splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_EmptyShape) =
   Just (bp { llvmBlockLen = bvSub off (llvmBlockOffset bp) },
         bp { llvmBlockOffset = off,
-             llvmBlockLen = bvSub (llvmBlockLen bp) off })
+             llvmBlockLen = bvSub (llvmBlockEndOffset bp) off })
 splitLLVMBlockPerm off bp@(LLVMBlockPerm { llvmBlockShape = sh })
   | Just sh_len <- llvmShapeLength sh
   , bvLt sh_len (bvSub off (llvmBlockOffset bp)) =

From 0f4e55f28eb4014603d64710ef38d7cb9e7adf1b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 23 Nov 2021 15:37:31 -0800
Subject: [PATCH 03/11] small tweaks to the widening code to make the precise
 conditions of various cases more clear

---
 heapster-saw/src/Verifier/SAW/Heapster/Widening.hs | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
index 98c8606774..c0133094be 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
@@ -501,14 +501,12 @@ equalizeLLVMBlockRanges' bp1 bp2
   | bvEq (llvmBlockLen bp1) (llvmBlockLen bp2) =
     return (bp1, bp2, [], [])
 equalizeLLVMBlockRanges' bp1 bp2
-  | bvLeq (llvmBlockLen bp1) (llvmBlockLen bp2) =
-    do (bp2', bp2'') <- splitLLVMBlockPerm (bvAdd (llvmBlockOffset bp1)
-                                            (llvmBlockLen bp1)) bp2
+  | bvLt (llvmBlockLen bp1) (llvmBlockLen bp2) =
+    do (bp2', bp2'') <- splitLLVMBlockPerm (llvmBlockEndOffset bp1) bp2
        return (bp1, bp2', [], [bp2''])
 equalizeLLVMBlockRanges' bp1 bp2
-  | bvLeq (llvmBlockLen bp2) (llvmBlockLen bp1) =
-    do (bp1', bp1'') <- splitLLVMBlockPerm (bvAdd (llvmBlockOffset bp2)
-                                            (llvmBlockLen bp2)) bp1
+  | bvLt (llvmBlockLen bp2) (llvmBlockLen bp1) =
+    do (bp1', bp1'') <- splitLLVMBlockPerm (llvmBlockEndOffset bp2) bp1
        return (bp1', bp2, [bp1''], [])
 equalizeLLVMBlockRanges' _ _ = Nothing
 
@@ -524,12 +522,12 @@ equalizeLLVMBlockRanges bp1 bp2
   | bvEq (llvmBlockOffset bp1) (llvmBlockOffset bp2) =
     equalizeLLVMBlockRanges' bp1 bp2
 equalizeLLVMBlockRanges bp1 bp2
-  | bvLeq (llvmBlockOffset bp1) (llvmBlockOffset bp2) =
+  | bvLt (llvmBlockOffset bp1) (llvmBlockOffset bp2) =
     do (bp1', bp1'') <- splitLLVMBlockPerm (llvmBlockOffset bp2) bp1
        (bp1_ret, bp2_ret, bps1, bps2) <- equalizeLLVMBlockRanges' bp1'' bp2
        return (bp1_ret, bp2_ret, bp1':bps1, bps2)
 equalizeLLVMBlockRanges bp1 bp2
-  | bvLeq (llvmBlockOffset bp2) (llvmBlockOffset bp1) =
+  | bvLt (llvmBlockOffset bp2) (llvmBlockOffset bp1) =
     do (bp2', bp2'') <- splitLLVMBlockPerm (llvmBlockOffset bp1) bp2
        (bp1_ret, bp2_ret, bps1, bps2) <- equalizeLLVMBlockRanges' bp1 bp2''
        return (bp1_ret, bp2_ret, bps1, bp2':bps2)

From 28da80d3bd242f8036aaa0f0c5300ae485c7da11 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 23 Nov 2021 15:38:22 -0800
Subject: [PATCH 04/11] added support for constant propagation through and, or,
 xor, and not of bitvectors

---
 .../src/Verifier/SAW/Heapster/TypedCrucible.hs    | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 3657d60986..2732956e47 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -2805,6 +2805,21 @@ tcExpr (BVZext w2 _ (RegWithVal _ (bvMatchConst -> Just bv))) =
 tcExpr (BVSext w2 w (RegWithVal _ (bvMatchConst -> Just bv))) =
   withKnownNat w2 $ pure $ Just $ bvBV $ BV.sext w w2 bv
 
+tcExpr (BVNot w (RegWithVal _ (bvMatchConst -> Just bv))) =
+  withKnownNat w $ pure $ Just $ bvBV $ BV.complement w bv
+tcExpr (BVAnd w (RegWithVal _ (bvMatchConst ->
+                               Just bv1)) (RegWithVal _
+                                           (bvMatchConst -> Just bv2))) =
+  withKnownNat w $ pure $ Just $ bvBV $ BV.and bv1 bv2
+tcExpr (BVOr w (RegWithVal _ (bvMatchConst ->
+                               Just bv1)) (RegWithVal _
+                                           (bvMatchConst -> Just bv2))) =
+  withKnownNat w $ pure $ Just $ bvBV $ BV.or bv1 bv2
+tcExpr (BVXor w (RegWithVal _ (bvMatchConst ->
+                               Just bv1)) (RegWithVal _
+                                           (bvMatchConst -> Just bv2))) =
+  withKnownNat w $ pure $ Just $ bvBV $ BV.xor bv1 bv2
+
 tcExpr (BVAdd w (RegWithVal _ e1) (RegWithVal _ e2)) =
   withKnownNat w $ pure $ Just $ bvAdd e1 e2
 

From 4edb06b170232c6ea1664bd067a68061e8003e37 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 23 Nov 2021 17:18:12 -0800
Subject: [PATCH 05/11] optimized implGetLLVMPermForOffset so that it only
 returns permissions that could actually be used to prove a permission at the
 given offset

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 21 ++++++++++++++++++-
 .../src/Verifier/SAW/Heapster/Permissions.hs  | 15 -------------
 2 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index bed740f0b4..158830cef3 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -4757,6 +4757,25 @@ implElimAppendIthLLVMBlock _ _ _ =
   error "implElimAppendIthLLVMBlock: malformed inputs"
 
 
+-- | Return the indices in a list of permissions for all of those that could be
+-- used to prove a permission containing the specified offset. Field and block
+-- permissions can only be used if they definitely (in the sense of
+-- 'bvPropHolds') contain the offset, while the 'Bool' flag indicates whether
+-- array permissions are allowed to only possibly contain (in the sense of
+-- 'bvPropCouldHold') the offset.
+permIndicesForProvingOffset :: (1 <= w, KnownNat w) =>
+                            [AtomicPerm (LLVMPointerType w)] -> Bool ->
+                            PermExpr (BVType w) -> [Int]
+permIndicesForProvingOffset ps imprecise_p off =
+  let ixs_holdss = flip findMaybeIndices ps $ \p ->
+        case llvmPermContainsOffset off p of
+          Just (_, True) -> Just True
+          Just _ | isLLVMArrayPerm p && imprecise_p -> Just False
+          _ -> Nothing in
+  case find (\(_,holds) -> holds) ixs_holdss of
+    Just (i,_) -> [i]
+    Nothing -> map fst ixs_holdss
+
 -- | Assume @x:p@ is on top of the stack, where @p@ is a @memblock@ permission
 -- that contains the supplied offset @off@, and repeatedly eliminate this
 -- @memblock@ permission until @p@ has been converted to a non-@memblock@
@@ -4818,7 +4837,7 @@ implGetLLVMPermForOffset ::
   (AtomicPerm (LLVMPointerType w))
 
 implGetLLVMPermForOffset x ps imprecise_p elim_blocks_p off mb_p =
-  case llvmPermIndicesForOffset ps imprecise_p off of
+  case permIndicesForProvingOffset ps imprecise_p off of
     -- If we didn't find any matches, try to unfold on the left
     [] ->
       implUnfoldOrFail x ps mb_p >>>= \_ ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index a0010423c6..d573fca350 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4550,21 +4550,6 @@ llvmAtomicPermOverlapsRange rng (Perm_LLVMBlock bp) =
   bvRangesOverlap rng (llvmBlockRange bp)
 llvmAtomicPermOverlapsRange _ _ = False
 
--- | Search through a list of permissions for either some permission that
--- definitely contains (as in 'bvPropHolds') the given offset or, failing that,
--- and if the supplied 'Bool' flag is 'True', for all permissions that could (as
--- in 'bvPropCouldHold') contain the given offset. Return the indices in the
--- list for the permissions that were found.
-llvmPermIndicesForOffset :: (1 <= w, KnownNat w) =>
-                            [AtomicPerm (LLVMPointerType w)] -> Bool ->
-                            PermExpr (BVType w) -> [Int]
-llvmPermIndicesForOffset ps imprecise_p off =
-  let ixs_props = findMaybeIndices (llvmPermContainsOffset off) ps in
-  case find (\(_,(_,holds)) -> holds) ixs_props of
-    Just (i,_) -> [i]
-    Nothing | imprecise_p -> map fst ixs_props
-    Nothing -> []
-
 -- | Return the total length of an LLVM array permission in bytes
 llvmArrayLengthBytes :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
                         PermExpr (BVType w)

From 5db8e70cd82e9d9d770ce0cf807f0f8994733b37 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 29 Nov 2021 06:36:27 -0800
Subject: [PATCH 06/11] changed the translation of LLVM globals so that each is
 translated to its own SAW core definition, rather than having the entire
 global be copied into each spec when it is used

---
 .../Verifier/SAW/Heapster/LLVMGlobalConst.hs  | 36 +++++++++++++------
 .../src/Verifier/SAW/Heapster/Permissions.hs  | 36 +++++++++++++++++--
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 29 ---------------
 .../Verifier/SAW/Heapster/TypedCrucible.hs    |  5 +--
 src/SAWScript/HeapsterBuiltins.hs             | 11 +++---
 5 files changed, 69 insertions(+), 48 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
index fcf6d75807..b5e431d2fd 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
@@ -29,6 +29,8 @@ import Lang.Crucible.LLVM.DataLayout
 import Lang.Crucible.LLVM.MemModel
 
 import Verifier.SAW.OpenTerm
+import Verifier.SAW.Term.Functor (ModuleName)
+import Verifier.SAW.SharedTerm
 import Verifier.SAW.Heapster.Permissions
 
 
@@ -201,11 +203,11 @@ llvmZeroInitValue tp =
   traceAndZeroM ("llvmZeroInitValue cannot handle type:\n"
                  ++ show (L.ppType tp))
 
--- | Add an LLVM global constant to a 'PermEnv', if the global has a type and
--- value we can translate to Heapster, otherwise silently ignore it
-permEnvAddGlobalConst :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm ->
-                         NatRepr w -> PermEnv -> L.Global -> PermEnv
-permEnvAddGlobalConst dlevel endianness w env global =
+-- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad
+translateLLVMValueTop :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm ->
+                         NatRepr w -> PermEnv -> L.Global ->
+                         Maybe (PermExpr (LLVMShapeType w), OpenTerm)
+translateLLVMValueTop dlevel endianness w env global =
   let sym = show (L.globalSym global) in
   let trans_info = LLVMTransInfo { llvmTransInfoEnv = env,
                                    llvmTransInfoEndianness = endianness,
@@ -213,13 +215,27 @@ permEnvAddGlobalConst dlevel endianness w env global =
   debugTrace dlevel ("Global: " ++ sym ++ "; value =\n" ++
                      maybe "None" ppLLVMValue
                      (L.globalValue global)) $
-  maybe env id $
   (\x -> case x of
       Just _ -> debugTrace dlevel (sym ++ " translated") x
       Nothing -> debugTrace dlevel (sym ++ " not translated") x) $
   flip runLLVMTransM trans_info $
   do val <- lift $ L.globalValue global
-     (sh, t) <- translateLLVMValue w (L.globalType global) val
-     let p = ValPerm_LLVMBlock $ llvmReadBlockOfShape sh
-     return $ permEnvAddGlobalSyms env
-       [PermEnvGlobalEntry (GlobalSymbol $ L.globalSym global) p [t]]
+     translateLLVMValue w (L.globalType global) val
+
+-- | Add an LLVM global constant to a 'PermEnv', if the global has a type and
+-- value we can translate to Heapster, otherwise silently ignore it
+permEnvAddGlobalConst :: (1 <= w, KnownNat w) => SharedContext -> ModuleName ->
+                         DebugLevel -> EndianForm -> NatRepr w -> PermEnv ->
+                         L.Global -> IO PermEnv
+permEnvAddGlobalConst sc mod_name dlevel endianness w env global =
+  case translateLLVMValueTop dlevel endianness w env global of
+    Nothing -> return env
+    Just (sh, t) ->
+      do let ident = mkSafeIdent mod_name $ show $ L.globalSym global
+         complete_t <- completeOpenTerm sc t
+         tp <- completeOpenTermType sc t
+         scInsertDef sc mod_name ident tp complete_t
+         let p = ValPerm_LLVMBlock $ llvmReadBlockOfShape sh
+         let t_ident = globalOpenTerm ident
+         return $ permEnvAddGlobalSyms env
+           [PermEnvGlobalEntry (GlobalSymbol $ L.globalSym global) p [t_ident]]
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index d573fca350..57dd9ee2c6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -29,7 +29,9 @@ module Verifier.SAW.Heapster.Permissions where
 
 import Prelude hiding (pred)
 
-import Data.Char (isDigit)
+import Numeric (showHex)
+import Data.Char
+import qualified Data.Text as Text
 import Data.Word
 import Data.Maybe
 import Data.Either
@@ -80,7 +82,9 @@ import Lang.Crucible.LLVM.DataLayout
 import Lang.Crucible.LLVM.MemModel
 import Lang.Crucible.LLVM.Bytes
 import Lang.Crucible.CFG.Core
-import Verifier.SAW.Term.Functor (Ident)
+import Verifier.SAW.Term.Functor (ModuleName)
+import Verifier.SAW.Module
+import Verifier.SAW.SharedTerm hiding (Constant)
 import Verifier.SAW.OpenTerm
 
 import Verifier.SAW.Heapster.CruUtil
@@ -193,6 +197,34 @@ nameSetFromFlags ns flags =
 data RecurseFlag = RecLeft | RecRight | RecNone
   deriving (Eq, Show, Read)
 
+-- | Make a "coq-safe" identifier from a string that might contain
+-- non-identifier characters, where we use the SAW core notion of identifier
+-- characters as letters, digits, underscore and primes. Any disallowed
+-- character is mapped to the string @__xNN@, where @NN@ is the hexadecimal code
+-- for that character. Additionally, a SAW core identifier is not allowed to
+-- start with a prime, so a leading underscore is added in such a case.
+mkSafeIdent :: ModuleName -> String -> Ident
+mkSafeIdent _ [] = fromString "_"
+mkSafeIdent mnm nm =
+  let is_safe_char c = isAlphaNum c || c == '_' || c == '\'' in
+  mkIdent mnm $ Text.pack $
+  (if nm!!0 == '\'' then ('_' :) else id) $
+  concatMap
+  (\c -> if is_safe_char c then [c] else
+           "__x" ++ showHex (ord c) "")
+  nm
+
+-- | Insert a definition into a SAW core module
+scInsertDef :: SharedContext -> ModuleName -> Ident -> Term -> Term -> IO ()
+scInsertDef sc mnm ident def_tp def_tm =
+  do t <- scConstant' sc (ModuleIdentifier ident) def_tm def_tp
+     scRegisterGlobal sc ident t
+     scModifyModule sc mnm $ \m ->
+       insDef m $ Def { defIdent = ident,
+                        defQualifier = NoQualifier,
+                        defType = def_tp,
+                        defBody = Just def_tm }
+
 
 ----------------------------------------------------------------------
 -- * Pretty-printing
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 5dd818cdba..6caea480c9 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -80,17 +80,6 @@ import Verifier.SAW.Heapster.TypedCrucible
 import GHC.Stack
 
 
-scInsertDef :: SharedContext -> ModuleName -> Ident -> Term -> Term -> IO ()
-scInsertDef sc mnm ident def_tp def_tm =
-  do t <- scConstant' sc (ModuleIdentifier ident) def_tm def_tp
-     scRegisterGlobal sc ident t
-     scModifyModule sc mnm $ \m ->
-       insDef m $ Def { defIdent = ident,
-                        defQualifier = NoQualifier,
-                        defType = def_tp,
-                        defBody = Just def_tm }
-
-
 ----------------------------------------------------------------------
 -- * Translation Monads
 ----------------------------------------------------------------------
@@ -4690,24 +4679,6 @@ tcTranslateCFGTupleFun env checks endianness dlevel cfgs_and_perms =
       tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg
 
 
--- | Make a "coq-safe" identifier from a string that might contain
--- non-identifier characters, where we use the SAW core notion of identifier
--- characters as letters, digits, underscore and primes. Any disallowed
--- character is mapped to the string @__xNN@, where @NN@ is the hexadecimal code
--- for that character. Additionally, a SAW core identifier is not allowed to
--- start with a prime, so a leading underscore is added in such a case.
-mkSafeIdent :: ModuleName -> String -> Ident
-mkSafeIdent _ [] = "_"
-mkSafeIdent mnm nm =
-  let is_safe_char c = isAlphaNum c || c == '_' || c == '\'' in
-  mkIdent mnm $ Data.Text.pack $
-  (if nm!!0 == '\'' then ('_' :) else id) $
-  concatMap
-  (\c -> if is_safe_char c then [c] else
-           "__x" ++ showHex (ord c) "")
-  nm
-
-
 -- | Type-check a set of CFGs against their function permissions, translate the
 -- results to SAW core functions, and add them as definitions to the SAW core
 -- module with the given module name. The name of each definition will be the
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 2732956e47..df49b4e60f 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -3891,7 +3891,7 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) =
       -- reflexivity.
       implWithoutTracingM (implPushOrReflMultiM perms_in) >>>
       pure (PermImpl_Done $
-               TypedJumpTarget siteID Proxy (mkCruCtx args_tps) perms_in)
+            TypedJumpTarget siteID Proxy (mkCruCtx args_tps) perms_in)
 
 
 -- | Type-check a termination statement
@@ -4027,7 +4027,8 @@ proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out =
         mbSeparate (cruCtxProxies ghosts) $
         mbValuePermsToDistPerms mb_perms_out in
   stmtTraceM (\i ->
-               pretty "proveCallSiteImpl:" <> line <>
+               pretty ("proveCallSiteImpl, src = " ++ show srcID ++
+                       ", dest = " ++ show destID) <> line <>
                indent 2 (permPretty i perms_in) <> line <>
                pretty "-o" <> line <>
                indent 2 (permPretty i perms_out)) >>>
diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index b23469556e..bbbc34563c 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -267,7 +267,8 @@ parseAndInsDef henv nm term_tp term_string =
 mkHeapsterEnv :: DebugLevel -> ModuleName -> [Some LLVMModule] ->
                  TopLevel HeapsterEnv
 mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) =
-  do let w = llvmModuleArchReprWidth first_mod
+  do sc <- getSharedContext
+     let w = llvmModuleArchReprWidth first_mod
      let endianness =
            llvmDataLayout (modTrans first_mod ^. transContext ^. llvmTypeCtx)
            ^. intLayout
@@ -275,10 +276,10 @@ mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) =
        Left pf -> return pf
        Right _ -> fail "LLVM arch width is 0!"
      let globals = concatMap (\(Some lm) -> L.modGlobals $ modAST lm) llvm_mods
-         env =
-           withKnownNat w $ withLeqProof leq_proof $
-           foldl (permEnvAddGlobalConst dlevel endianness w)
-           heapster_default_env globals
+     env <-
+       liftIO $ withKnownNat w $ withLeqProof leq_proof $
+       foldM (permEnvAddGlobalConst sc saw_mod_name dlevel endianness w)
+       heapster_default_env globals
      env_ref <- liftIO $ newIORef env
      dlevel_ref <- liftIO $ newIORef dlevel
      checks_ref <- liftIO $ newIORef doChecks

From a255e1554733ffd07dfc581cdccf394df00bee87 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 29 Nov 2021 07:30:59 -0800
Subject: [PATCH 07/11] removed no longer needed imports from SAWTranslation.hs

---
 heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 6caea480c9..bb996839bc 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -30,8 +30,6 @@ module Verifier.SAW.Heapster.SAWTranslation where
 
 import Prelude hiding (pi)
 
-import Numeric (showHex)
-import Data.Char
 import Data.Maybe
 import Numeric.Natural
 import Data.List hiding (inits)
@@ -69,7 +67,6 @@ import Lang.Crucible.CFG.Core
 
 import Verifier.SAW.OpenTerm
 import Verifier.SAW.Term.Functor
-import Verifier.SAW.Module
 import Verifier.SAW.SharedTerm
 
 import Verifier.SAW.Heapster.CruUtil

From d6c29b87e5fcd7d57bc25c178092e5c89674e361 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 29 Nov 2021 15:06:14 -0800
Subject: [PATCH 08/11] added the OpenTerm combinator completeNormOpenTerm to
 beta-normalize an OpenTerm after it is completed

---
 saw-core/src/Verifier/SAW/OpenTerm.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs
index a28c6b7e7f..afef3cb420 100644
--- a/saw-core/src/Verifier/SAW/OpenTerm.hs
+++ b/saw-core/src/Verifier/SAW/OpenTerm.hs
@@ -18,7 +18,7 @@ built.
 
 module Verifier.SAW.OpenTerm (
   -- * Open terms and converting to closed terms
-  OpenTerm(..), completeOpenTerm, completeOpenTermType,
+  OpenTerm(..), completeOpenTerm, completeNormOpenTerm, completeOpenTermType,
   -- * Basic operations for building open terms
   closedOpenTerm, flatOpenTerm, sortOpenTerm, natOpenTerm,
   unitOpenTerm, unitTypeOpenTerm,
@@ -59,6 +59,10 @@ completeOpenTerm sc (OpenTerm termM) =
   either (fail . show) return =<<
   runTCM (typedVal <$> termM) sc Nothing []
 
+-- | "Complete" an 'OpenTerm' to a closed term and 'betaNormalize' the result
+completeNormOpenTerm :: SharedContext -> OpenTerm -> IO Term
+completeNormOpenTerm sc m = completeOpenTerm sc m >>= betaNormalize sc
+
 -- | "Complete" an 'OpenTerm' to a closed term for its type
 completeOpenTermType :: SharedContext -> OpenTerm -> IO Term
 completeOpenTermType sc (OpenTerm termM) =

From db9dfe760cd5784e4efa3da643b62c7b1070cc02 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 29 Nov 2021 15:07:09 -0800
Subject: [PATCH 09/11] changed the translation of TypedSetReg to let-bind its
 output expression translation, to avoid exponential code explosion

---
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 44 ++++++++++++++-----
 1 file changed, 33 insertions(+), 11 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index bb996839bc..ece2f581c4 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -318,6 +318,15 @@ inExtMultiTransM MNil m = m
 inExtMultiTransM (ctx :>: etrans) m =
   inExtMultiTransM ctx $ inExtTransM etrans m
 
+-- | Run a translation computation in an extended context, where we let-bind any
+-- term in the supplied expression translation
+inExtTransLetBindM :: TransInfo info => TypeTrans (ExprTrans tp) ->
+                      ExprTrans tp -> TransM info (ctx :> tp) OpenTerm ->
+                      TransM info ctx OpenTerm
+inExtTransLetBindM tp_trans etrans m =
+  letTransMultiM "z" (typeTransTypes tp_trans) (transTerms etrans) $ \var_tms ->
+  inExtTransM (typeTransF tp_trans var_tms) m
+
 -- | Run a translation computation in context @(ctx1 :++: ctx2) :++: ctx2@ by
 -- copying the @ctx2@ portion of the current context
 inExtMultiTransCopyLastM :: TransInfo info => prx ctx1 -> RAssign any ctx2 ->
@@ -415,6 +424,18 @@ letTransM x tp rhs_m body_m =
      return $
        letOpenTerm (pack x) tp (runTransM rhs_m r) (\x' -> runTransM (body_m x') r)
 
+-- | Build 0 or more let-bindings in a translation monad, using the same
+-- variable name
+letTransMultiM :: String -> [OpenTerm] -> [OpenTerm] ->
+                  ([OpenTerm] -> TransM info ctx OpenTerm) ->
+                  TransM info ctx OpenTerm
+letTransMultiM _ [] [] f = f []
+letTransMultiM x (tp:tps) (rhs:rhss) f =
+  letTransM x tp (return rhs) $ \var_tm ->
+  letTransMultiM x tps rhss (\var_tms -> f (var_tm:var_tms))
+letTransMultiM _ _ _ _ =
+  error "letTransMultiM: numbers of types and right-hand sides disagree"
+
 -- | Build a bitvector type in a translation monad
 bitvectorTransM :: TransM info ctx OpenTerm -> TransM info ctx OpenTerm
 bitvectorTransM m =
@@ -4133,10 +4154,11 @@ translateStmt :: PermCheckExtC ext =>
                  ImpTransM ext blocks tops ret ps_out (ctx :++: rets) OpenTerm ->
                  ImpTransM ext blocks tops ret ps_in ctx OpenTerm
 translateStmt loc mb_stmt m = case mbMatch mb_stmt of
-  [nuMP| TypedSetReg _ e |] ->
-    do etrans <- tpTransM $ translate e
+  [nuMP| TypedSetReg tp e |] ->
+    do tp_trans <- translate tp
+       etrans <- tpTransM $ translate e
        let ptrans = exprOutPerm e
-       inExtTransM etrans $
+       inExtTransLetBindM tp_trans etrans $
          withPermStackM (:>: Member_Base) (:>: extPermTrans ptrans) m
 
   [nuMP| TypedSetRegPermExpr _ e |] ->
@@ -4692,18 +4714,18 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
      let tup_fun_ident =
            mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms)
                                  ++ "__tuple_fun")
-     tup_fun_tp <- completeOpenTerm sc $
+     tup_fun_tp <- completeNormOpenTerm sc $
        applyOpenTerm (globalOpenTerm "Prelude.lrtTupleType") lrts
-     tup_fun_tm <- completeOpenTerm sc $
+     tup_fun_tm <- completeNormOpenTerm sc $
        applyOpenTermMulti (globalOpenTerm "Prelude.multiFixM") [lrts, tup_fun]
      scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm 
      new_entries <-
        zipWithM
        (\cfg_and_perm i ->
-         do tp <- completeOpenTerm sc $
+         do tp <- completeNormOpenTerm sc $
               applyOpenTerm (globalOpenTerm "Prelude.lrtToType") $
               someCFGAndPermLRT env cfg_and_perm
-            tm <- completeOpenTerm sc $
+            tm <- completeNormOpenTerm sc $
               projTupleOpenTerm i (globalOpenTerm tup_fun_ident)
             let ident = mkSafeIdent mod_name (someCFGAndPermToName cfg_and_perm)
             scInsertDef sc mod_name ident tp tm
@@ -4723,13 +4745,13 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
 translateCompleteFunPerm :: SharedContext -> PermEnv ->
                             FunPerm ghosts args ret -> IO Term
 translateCompleteFunPerm sc env fun_perm =
-  completeOpenTerm sc $
+  completeNormOpenTerm sc $
   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 sc env typ_perm =
-  completeOpenTerm sc $ typeTransType1 $
+  completeNormOpenTerm sc $ typeTransType1 $
   runNilTypeTransM env noChecks $ translate $ emptyMb typ_perm
 
 -- | Translate a 'TypeRepr' within the given context of type arguments to the
@@ -4737,7 +4759,7 @@ translateCompleteType sc env typ_perm =
 translateCompleteTypeInCtx :: SharedContext -> PermEnv ->
                               CruCtx args -> Mb args (TypeRepr a) -> IO Term
 translateCompleteTypeInCtx sc env args ret =
-  completeOpenTerm sc $
+  completeNormOpenTerm sc $
   runNilTypeTransM env noChecks (piExprCtx args (typeTransType1 <$>
                                                  translate ret'))
   where ret' = mbCombine (cruCtxProxies args) . emptyMb $ ret
@@ -4751,7 +4773,7 @@ translateCompletePureFun :: SharedContext -> PermEnv
                          -> Mb ctx (ValuePerm ret) -- ^ Return type perm
                          -> IO Term
 translateCompletePureFun sc env ctx args ret =
-  completeOpenTerm sc $ runNilTypeTransM env noChecks $
+  completeNormOpenTerm sc $ runNilTypeTransM env noChecks $
   piExprCtx ctx $ piPermCtx args' $ const $
   typeTransTupleType <$> translate ret'
   where args' = mbCombine pxys . emptyMb $ args

From dd9aa834abaa88bf8dbc7c22310af11174db378b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 29 Nov 2021 15:27:08 -0800
Subject: [PATCH 10/11] changed the translation of lambdas so that their bodies
 have let-bindings for repeated terms; added a type ascription term to the Coq
 AST; changed the translation of the unit type to give it an explicit
 ascription to sort Type rather than Set

---
 saw-core-coq/src/Language/Coq/AST.hs                  | 2 ++
 saw-core-coq/src/Language/Coq/Pretty.hs               | 3 +++
 saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs | 7 +++++--
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/saw-core-coq/src/Language/Coq/AST.hs b/saw-core-coq/src/Language/Coq/AST.hs
index 740279bb35..052166ae2d 100644
--- a/saw-core-coq/src/Language/Coq/AST.hs
+++ b/saw-core-coq/src/Language/Coq/AST.hs
@@ -29,6 +29,8 @@ data Term
     -- | A variable that needs to be printed with a leading at sign in order to
     -- make all arguments explicit
   | ExplVar Ident
+    -- | A ascription @tm : tp@ of a type to a term
+  | Ascription Term Term
   | NatLit Integer
   | ZLit Integer
   | List [Term]
diff --git a/saw-core-coq/src/Language/Coq/Pretty.hs b/saw-core-coq/src/Language/Coq/Pretty.hs
index 9635ea920f..f78e86068e 100644
--- a/saw-core-coq/src/Language/Coq/Pretty.hs
+++ b/saw-core-coq/src/Language/Coq/Pretty.hs
@@ -129,6 +129,9 @@ ppTerm p e =
     ExplVar x ->
       parensIf (p > PrecApp) $
       string "@" <> ppIdent x
+    Ascription tm tp ->
+      parensIf (p > PrecLambda)
+      (ppTerm PrecApp tm <+> text ":" <+> ppTerm PrecApp tp)
     NatLit i ->
       integer i
     ZLit i ->
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index f9ff459198..f76f42ca60 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -226,7 +226,10 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
   case tf of
     Primitive pn  -> translateIdent (primName pn)
     UnitValue     -> pure (Coq.Var "tt")
-    UnitType      -> pure (Coq.Var "unit")
+    UnitType      ->
+      -- We need to explicitly tell Coq that we want unit to be a Type, since
+      -- all SAW core sorts are translated to Types
+      pure (Coq.Ascription (Coq.Var "unit") (Coq.Sort Coq.Type))
     PairValue x y -> Coq.App (Coq.Var "pair") <$> traverse translateTerm [x, y]
     PairType x y  -> Coq.App (Coq.Var "prod") <$> traverse translateTerm [x, y]
     PairLeft t    ->
@@ -537,7 +540,7 @@ translateTermUnshared t = withLocalTranslationState $ do
 
     Lambda {} -> do
       paramTerms <- translateParams params
-      e' <- translateTerm e
+      e' <- translateTermLet e
       pure (Coq.Lambda paramTerms e')
         where
           -- params are in normal, outermost first, order

From 27a845c2be9e78acb6eefd77e12c2b3bbcab685b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 30 Nov 2021 10:43:41 -0800
Subject: [PATCH 11/11] added a dummy translation of BVUndef to the 0 bitvector
 value

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

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index ece2f581c4..fa436b6397 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -3878,6 +3878,10 @@ instance (PermCheckExtC ext, TransInfo info) =>
     [nuMP| HandleLit _ |] -> return ETrans_Fun
 
     -- Bitvectors
+    [nuMP| BVUndef w |] ->
+      -- FIXME: we should really handle poison values; this translation just
+      -- treats them as if there were the bitvector 0 value
+      return $ ETrans_Term $ bvBVOpenTerm (mbLift w) $ BV.zero (mbLift w)
     [nuMP| BVLit w mb_bv |] ->
       return $ ETrans_Term $ bvBVOpenTerm (mbLift w) $ mbLift mb_bv
     [nuMP| BVConcat w1 w2 e1 e2 |] ->