Heapster/exponential code explosion

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