Heapster/exponential code explosion (#1528)

NOTE: the heapster-tests tests succeeded last time through the CI, so I'm going to push this even though they haven't finished this time...

* short-circut true `BVProp_Neq`s in the translation

* fixed a bug in splitLLVMBlockPerm

* small tweaks to the widening code to make the precise conditions of various cases more clear

* added support for constant propagation through and, or, xor, and not of bitvectors

* optimized implGetLLVMPermForOffset so that it only returns permissions that could actually be used to prove a permission at the given offset

* 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

* removed no longer needed imports from SAWTranslation.hs

* added the OpenTerm combinator completeNormOpenTerm to beta-normalize an OpenTerm after it is completed

* changed the translation of TypedSetReg to let-bind its output expression translation, to avoid exponential code explosion

* 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

* added a dummy translation of BVUndef to the 0 bitvector value

Co-authored-by: Matthew Yacavone <[email protected]>

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 >>>= \_ ->

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,25 +203,39 @@ 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,
                                    llvmTransInfoDebugLevel = dlevel } in
   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]]

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
@@ -3958,7 +3990,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)) =
@@ -4563,21 +4595,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)

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
@@ -80,17 +77,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
 ----------------------------------------------------------------------
@@ -332,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 ->
@@ -429,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 =
@@ -3606,6 +3613,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' |]) ->
@@ -3864,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 |] ->
@@ -4140,10 +4158,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 |] ->
@@ -4683,24 +4702,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
@@ -4717,18 +4718,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
@@ -4748,21 +4749,21 @@ 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
 -- SAW core type it represents
 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
@@ -4776,7 +4777,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