Redo Heapster Lifetime Subsumption (#1410)

* added ppInfoAddTypedExprNames to use a base name for each variable depending on its type; also removed old PPInfo-related code

* whoops, fixed an infinite loop

* implemented lifetime subsumption

* started adding a new version of lowned permissions that include a notion of contained lifetimes, along with an lfinished permission

* bugfix: there was an infinite loop that kept copying a block permission before eliminating it and would then go right back to trying to eliminate that same permission again...

* added debug output for return statements, which is long overdue

* changed implElimLLVMBlock to always only eliminate one step of a memblock permission; changed proveVarLLVMBlocks to focus first on eliminating memblock permissions on the left that overlap with but are not contained in memblock permissions on the right

* unfold defined shapes on the left when their ranges match a shape we are trying to prove on the right

* whoops, do not try to eliminate LHS block perms when we are proving an empty block perm on the right

* added a case to proveVarLLVMBlocks to detect if the right-hand side is a tagged union type where we already know from something on the left what the tag is, in which case we can avoid searching for proofs of all the disjuncts other than the one that matches that known tag

* added another special case to proveVarLLVMBlocks, to eliminate a sequence shape sh;emptysh with the empty shape when necessary

* finished updating Implication.hs with the new lowned permission form

* reorganized proveVarLLVMBlocks into two separate stages represented by two separate functions, all of which now take lists of multi-bindings instead of multi-bindings of lists

* whoops, forgot to change a shadowed variable...

* implemented a few more suggestions from Eric Mertens

* fixed an infinite loop in proving the new lowned permissions; also added helper function implPushCopyM

* updated the translation for the new lfinished permission and the modified lowned permission, along with all the new and modified rules; also removed a bunch of whitespace from a previous commit

* updated the remaining Heapster files to reflect the new form of the lowned permission

* added  parser support for lfinished perms and for lowned perms with non-empty contained lifetimes

* whoops, fixed the parser rules for an optional list of lifetimes

heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs

@@ -154,8 +154,9 @@ instance ContainsIRTRecName (AtomicPerm a) where
   containsIRTRecName n (Perm_NamedConj _ args _) = containsIRTRecName n args
   containsIRTRecName n (Perm_LLVMFrame fperm) =
     containsIRTRecName n (map fst fperm)
-  containsIRTRecName _ (Perm_LOwned _ _) = False
+  containsIRTRecName _ (Perm_LOwned _ _ _) = False
   containsIRTRecName _ (Perm_LCurrent _) = False
+  containsIRTRecName _ Perm_LFinished = False
   containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps
   containsIRTRecName _ (Perm_Fun _) = False
   containsIRTRecName _ (Perm_BVProp _) = False
@@ -414,9 +415,10 @@ instance IRTTyVars (AtomicPerm a) where
     [nuMP| Perm_NamedConj npn args off |] ->
       namedPermIRTTyVars mb_p npn args off
     [nuMP| Perm_LLVMFrame _ |] -> return ([], IRTVarsNil)
-    [nuMP| Perm_LOwned _ _ |] ->
+    [nuMP| Perm_LOwned _ _ _ |] ->
       throwError "lowned permission in an IRT definition!"
     [nuMP| Perm_LCurrent _ |] -> return ([], IRTVarsNil)
+    [nuMP| Perm_LFinished |] -> return ([], IRTVarsNil)
     [nuMP| Perm_Struct ps |] -> irtTyVars ps
     [nuMP| Perm_Fun _ |] ->
       throwError "fun perm in an IRT definition!"
@@ -660,9 +662,10 @@ instance IRTDescs (AtomicPerm a) where
     ([nuMP| Perm_NamedConj npn args off |], _) ->
       namedPermIRTDescs npn args off ixs
     ([nuMP| Perm_LLVMFrame _ |], _) -> return []
-    ([nuMP| Perm_LOwned _ _ |], _) ->
+    ([nuMP| Perm_LOwned _ _ _ |], _) ->
       error "lowned permission made it to IRTDesc translation"
     ([nuMP| Perm_LCurrent _ |], _) -> return []
+    ([nuMP| Perm_LFinished |], _) -> return []
     ([nuMP| Perm_Struct ps |], _) ->
       irtDescs ps ixs
     ([nuMP| Perm_Fun _ |], _) ->

heapster-saw/src/Verifier/SAW/Heapster/Parser.y

@@ -66,6 +66,7 @@ import Verifier.SAW.Heapster.UntypedAST
 'lifetime'      { Located $$ TLifetime                  }
 'lowned'        { Located $$ TLOwned                    }
 'lcurrent'      { Located $$ TLCurrent                  }
+'lfinished'     { Located $$ TLFinished                 }
 'rwmodality'    { Located $$ TRWModality                }
 'permlist'      { Located $$ TPermList                  }
 'struct'        { Located $$ TStruct                    }
@@ -179,9 +180,10 @@ expr ::                                         { AstExpr }
                                                 { ExPtr (pos $2) $1 $5 $7 Nothing $10 }
 
   | 'shape' '(' expr ')'                        { ExShape (pos $1) $3}
-  | 'lowned' '(' list(varExpr) '-o' list1(varExpr) ')'
-                                                { ExLOwned (pos $1) $3 $5}
+  | 'lowned' lifetimes '(' list(varExpr) '-o' list1(varExpr) ')'
+                                                { ExLOwned (pos $1) $2 $4 $6}
   | lifetime 'lcurrent'                         { ExLCurrent (pos $2) $1 }
+  | 'lfinished'                                 { ExLFinished (pos $1) }
 
 -- BV Props (Value Permissions)
 
@@ -223,6 +225,10 @@ lifetime ::                                     { Maybe AstExpr         }
   :                                             { Nothing               }
   | '[' expr ']'                                { Just $2               }
 
+lifetimes ::                                    { [AstExpr]             }
+  :                                             { []                    }
+  | '[' list(expr) ']'                          { $2                    }
+
 llvmFieldPermArray ::                           { ArrayPerm             }
   : lifetime '(' expr ',' expr ',' expr ')' '|->' expr
                                                 { ArrayPerm (pos $9) $1 $3 $5 (Just $7) $10 }

heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs

@@ -990,8 +990,6 @@ abstractMbLOPsModalities mb_lops = case mbMatch mb_lops of
                LOwnedPermBlock e (bp { llvmBlockRW = PExpr_Var rw,
                                        llvmBlockLifetime = PExpr_Var l }))
       mb_e mb_bp)
-  [nuMP| lops :>: lop@(LOwnedPermLifetime _ _ _) |] ->
-    liftA2 (mbMap2 (:>:)) (abstractMbLOPsModalities lops) (pure lop)
 
 
 -- | Find all field or block permissions containing lifetime @l@ and return them
@@ -1058,11 +1056,11 @@ mbLifetimeFunPerm (LifetimeDef _ _ [] _)
          Some3FunPerm $ FunPerm (appendCruCtx
                                  (singletonCruCtx LifetimeRepr) ghosts) args ret
          (mbMap3 (\ps_in lops_in lops_in_abs ->
-                   assocAppend (MNil :>: ValPerm_LOwned lops_in lops_in_abs)
+                   assocAppend (MNil :>: ValPerm_LOwned [] lops_in lops_in_abs)
                    ghosts args_prxs $ distPermsToValuePerms ps_in)
           mb_ps_in mb_lops_in mb_lops_in_abs)
          (mbMap3 (\ps_out lops_out lops_in_abs ->
-                   assocAppend (MNil :>: ValPerm_LOwned lops_out lops_in_abs)
+                   assocAppend (MNil :>: ValPerm_LOwned [] lops_out lops_in_abs)
                    ghosts (args_prxs :>: Proxy) $ distPermsToValuePerms ps_out)
           mb_ps_out mb_lops_out (extMb mb_lops_in_abs))
 mbLifetimeFunPerm (LifetimeDef _ _ _bounds _) _ =