Merge branch 'heapster-lifetime-subsumption' into heapster-memblock-p…

…rover-improvements

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

@@ -180,7 +180,9 @@ expr ::                                         { AstExpr }
 
   | 'shape' '(' expr ')'                        { ExShape (pos $1) $3}
   | 'lowned' '(' list(varExpr) '-o' list1(varExpr) ')'
-                                                { ExLOwned (pos $1) $3 $5}
+                                                { ExLOwned (pos $1) [] $3 $5}
+  | 'lowned' '[' list(expr) ']' '(' list(varExpr) '-o' list1(varExpr) ')'
+                                                { ExLOwned (pos $1) $3 $6 $8}
   | lifetime 'lcurrent'                         { ExLCurrent (pos $2) $1 }
 
 -- BV Props (Value Permissions)

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

@@ -1408,12 +1408,18 @@ data AtomicPerm (a :: CrucibleType) where
   -- these are a form of permission implication, so we write lifetime ownership
   -- permissions as @lowned(Pin -o Pout)@. Intuitively, @Pin@ must be given back
   -- before the lifetime is ended, and @Pout@ is returned afterwards.
-  Perm_LOwned :: LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+  -- Additionally, a lifetime may contain some other lifetimes, meaning the all
+  -- must end before the current one can be ended.
+  Perm_LOwned :: [PermExpr LifetimeType] ->
+                 LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                  AtomicPerm LifetimeType
 
   -- | Assertion that a lifetime is current during another lifetime
   Perm_LCurrent :: PermExpr LifetimeType -> AtomicPerm LifetimeType
 
+  -- | Assertion that a lifetime has finished
+  Perm_LFinished :: AtomicPerm LifetimeType
+
   -- | A struct permission = a sequence of permissions for each field
   Perm_Struct :: RAssign ValuePerm (CtxToRList ctx) ->
                  AtomicPerm (StructType ctx)
@@ -1497,11 +1503,12 @@ pattern ValPerm_LLVMBlockShape sh <- ValPerm_Conj [Perm_LLVMBlockShape sh]
     ValPerm_LLVMBlockShape sh = ValPerm_Conj [Perm_LLVMBlockShape sh]
 
 -- | A single @lowned@ permission
-pattern ValPerm_LOwned :: () => (a ~ LifetimeType) =>
+pattern ValPerm_LOwned :: () => (a ~ LifetimeType) => [PermExpr LifetimeType] ->
                           LOwnedPerms ps_in -> LOwnedPerms ps_out -> ValuePerm a
-pattern ValPerm_LOwned ps_in ps_out <- ValPerm_Conj [Perm_LOwned ps_in ps_out]
+pattern ValPerm_LOwned ls ps_in ps_out <- ValPerm_Conj [Perm_LOwned
+                                                        ls ps_in ps_out]
   where
-    ValPerm_LOwned ps_in ps_out = ValPerm_Conj [Perm_LOwned ps_in ps_out]
+    ValPerm_LOwned ls ps_in ps_out = ValPerm_Conj [Perm_LOwned ls ps_in ps_out]
 
 -- | A single @lcurrent@ permission
 pattern ValPerm_LCurrent :: () => (a ~ LifetimeType) =>
@@ -1510,6 +1517,12 @@ pattern ValPerm_LCurrent l <- ValPerm_Conj [Perm_LCurrent l]
   where
     ValPerm_LCurrent l = ValPerm_Conj [Perm_LCurrent l]
 
+-- | A single @lfinished@ permission
+pattern ValPerm_LFinished :: () => (a ~ LifetimeType) => ValuePerm a
+pattern ValPerm_LFinished <- ValPerm_Conj [Perm_LFinished]
+  where
+    ValPerm_LFinished = ValPerm_Conj [Perm_LFinished]
+
 -- | A sequence of value permissions
 {-
 data ValuePerms as where
@@ -1695,9 +1708,6 @@ data LOwnedPerm a where
                      LOwnedPerm (LLVMPointerType w)
   LOwnedPermBlock :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) ->
                      LLVMBlockPerm w -> LOwnedPerm (LLVMPointerType w)
-  LOwnedPermLifetime :: PermExpr LifetimeType ->
-                        LOwnedPerms ps_in -> LOwnedPerms ps_out ->
-                        LOwnedPerm LifetimeType
 
 -- | A sequence of 'LOwnedPerm's
 type LOwnedPerms = RAssign LOwnedPerm
@@ -1714,13 +1724,6 @@ instance TestEquality LOwnedPerm where
     , e1 == e2 && bp1 == bp2
     = Just Refl
   testEquality (LOwnedPermBlock _ _) _ = Nothing
-  testEquality (LOwnedPermLifetime e1 ps_in1 ps_out1)
-    (LOwnedPermLifetime e2 ps_in2 ps_out2)
-    | Just Refl <- testEquality ps_in1 ps_in2
-    , Just Refl <- testEquality ps_out1 ps_out2
-    , e1 == e2
-    = Just Refl
-  testEquality (LOwnedPermLifetime _ _ _) _ = Nothing
 
 instance Eq (LOwnedPerm a) where
   lop1 == lop2 | Just Refl <- testEquality lop1 lop2 = True
@@ -1735,8 +1738,6 @@ lownedPermExprAndPerm (LOwnedPermField e fp) =
   ExprAndPerm e $ ValPerm_LLVMField fp
 lownedPermExprAndPerm (LOwnedPermBlock e bp) =
   ExprAndPerm e $ ValPerm_LLVMBlock bp
-lownedPermExprAndPerm (LOwnedPermLifetime e ps_in ps_out) =
-  ExprAndPerm e $ ValPerm_LOwned ps_in ps_out
 
 -- | Convert an 'LOwnedPerm' to a variable plus permission, if possible
 lownedPermVarAndPerm :: LOwnedPerm a -> Maybe (VarAndPerm a)
@@ -1751,8 +1752,6 @@ varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LLVMField fp)) =
   Just $ LOwnedPermField (PExpr_Var x) fp
 varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LLVMBlock bp)) =
   Just $ LOwnedPermBlock (PExpr_Var x) bp
-varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LOwned ps_in ps_out)) =
-  Just $ LOwnedPermLifetime (PExpr_Var x) ps_in ps_out
 varAndPermLOwnedPerm _ = Nothing
 
 -- | Get the expression part of an 'LOwnedPerm'
@@ -2342,8 +2341,8 @@ data LifetimeCurrentPerms ps_l where
   AlwaysCurrentPerms :: LifetimeCurrentPerms RNil
   -- | A variable @l@ that is @lowned@ is current, requiring perms
   --
-  -- > l:lowned(ps_in -o ps_out)
-  LOwnedCurrentPerms :: ExprVar LifetimeType ->
+  -- > l:lowned[ls](ps_in -o ps_out)
+  LOwnedCurrentPerms :: ExprVar LifetimeType -> [PermExpr LifetimeType] ->
                         LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                         LifetimeCurrentPerms (RNil :> LifetimeType)
 
@@ -2358,14 +2357,14 @@ data LifetimeCurrentPerms ps_l where
 lifetimeCurrentPermsLifetime :: LifetimeCurrentPerms ps_l ->
                                 PermExpr LifetimeType
 lifetimeCurrentPermsLifetime AlwaysCurrentPerms = PExpr_Always
-lifetimeCurrentPermsLifetime (LOwnedCurrentPerms l _ _) = PExpr_Var l
+lifetimeCurrentPermsLifetime (LOwnedCurrentPerms l _ _ _) = PExpr_Var l
 lifetimeCurrentPermsLifetime (CurrentTransPerms _ l) = PExpr_Var l
 
 -- | Convert a 'LifetimeCurrentPerms' to the 'DistPerms' it represent
 lifetimeCurrentPermsPerms :: LifetimeCurrentPerms ps_l -> DistPerms ps_l
 lifetimeCurrentPermsPerms AlwaysCurrentPerms = DistPermsNil
-lifetimeCurrentPermsPerms (LOwnedCurrentPerms l ps_in ps_out) =
-  DistPermsCons DistPermsNil l $ ValPerm_LOwned ps_in ps_out
+lifetimeCurrentPermsPerms (LOwnedCurrentPerms l ls ps_in ps_out) =
+  DistPermsCons DistPermsNil l $ ValPerm_LOwned ls ps_in ps_out
 lifetimeCurrentPermsPerms (CurrentTransPerms cur_ps l) =
   DistPermsCons (lifetimeCurrentPermsPerms cur_ps) l $
   ValPerm_Conj1 $ Perm_LCurrent $ lifetimeCurrentPermsLifetime cur_ps
@@ -2375,7 +2374,7 @@ mbLifetimeCurrentPermsProxies :: Mb ctx (LifetimeCurrentPerms ps_l) ->
                                  RAssign Proxy ps_l
 mbLifetimeCurrentPermsProxies mb_l = case mbMatch mb_l of
   [nuMP| AlwaysCurrentPerms |] -> MNil
-  [nuMP| LOwnedCurrentPerms _ _ _ |] -> MNil :>: Proxy
+  [nuMP| LOwnedCurrentPerms _ _ _ _ |] -> MNil :>: Proxy
   [nuMP| CurrentTransPerms cur_ps _ |] ->
     mbLifetimeCurrentPermsProxies cur_ps :>: Proxy
 
@@ -2489,13 +2488,15 @@ instance Eq (AtomicPerm a) where
   (Perm_LLVMBlockShape _) == _ = False
   (Perm_LLVMFrame frame1) == (Perm_LLVMFrame frame2) = frame1 == frame2
   (Perm_LLVMFrame _) == _ = False
-  (Perm_LOwned ps_in1 ps_out1) == (Perm_LOwned ps_in2 ps_out2)
+  (Perm_LOwned ls1 ps_in1 ps_out1) == (Perm_LOwned ls2 ps_in2 ps_out2)
     | Just Refl <- testEquality ps_in1 ps_in2
     , Just Refl <- testEquality ps_out1 ps_out2
-    = True
-  (Perm_LOwned _ _) == _ = False
+    = ls1 == ls2
+  (Perm_LOwned _ _ _) == _ = False
   (Perm_LCurrent e1) == (Perm_LCurrent e2) = e1 == e2
   (Perm_LCurrent _) == _ = False
+  Perm_LFinished == Perm_LFinished = True
+  Perm_LFinished == _ = False
   (Perm_Struct ps1) == (Perm_Struct ps2) = ps1 == ps2
   (Perm_Struct _) == _ = False
   (Perm_Fun fperm1) == (Perm_Fun fperm2)
@@ -2645,12 +2646,16 @@ instance PermPretty (AtomicPerm a) where
   permPrettyM (Perm_LLVMFrame fperm) =
     do pps <- mapM (\(e,i) -> (<> (colon <> pretty i)) <$> permPrettyM e) fperm
        return (pretty "llvmframe" <+> ppEncList False pps)
-  permPrettyM (Perm_LOwned ps_in ps_out) =
+  permPrettyM (Perm_LOwned ls ps_in ps_out) =
     do pp_in <- permPrettyM ps_in
        pp_out <- permPrettyM ps_out
-       return (pretty "lowned" <+> parens (align $
-                                           sep [pp_in, pretty "-o", pp_out]))
+       ls_pp <- case ls of
+         [] -> return emptyDoc
+         _ -> ppEncList False <$> mapM permPrettyM ls
+       return (pretty "lowned" <> ls_pp <+>
+               parens (align $ sep [pp_in, pretty "-o", pp_out]))
   permPrettyM (Perm_LCurrent l) = (pretty "lcurrent" <+>) <$> permPrettyM l
+  permPrettyM Perm_LFinished = return (pretty "lfinished")
   permPrettyM (Perm_Struct ps) =
     ((pretty "struct" <+>) . parens) <$> permPrettyM ps
   permPrettyM (Perm_Fun fun_perm) = permPrettyM fun_perm
@@ -2915,8 +2920,9 @@ isLLVMBlockPerm _ = False
 
 -- | Test if an 'AtomicPerm' is a lifetime permission
 isLifetimePerm :: AtomicPerm a -> Maybe (a :~: LifetimeType)
-isLifetimePerm (Perm_LOwned _ _) = Just Refl
+isLifetimePerm (Perm_LOwned _ _ _) = Just Refl
 isLifetimePerm (Perm_LCurrent _) = Just Refl
+isLifetimePerm Perm_LFinished = Just Refl
 isLifetimePerm _ = Nothing
 
 -- | Test if an 'AtomicPerm' is a struct permission
@@ -4400,8 +4406,9 @@ atomicPermIsCopyable (Perm_LLVMFunPtr _ _) = True
 atomicPermIsCopyable Perm_IsLLVMPtr = True
 atomicPermIsCopyable (Perm_LLVMBlockShape sh) = shapeIsCopyable PExpr_Write sh
 atomicPermIsCopyable (Perm_LLVMFrame _) = False
-atomicPermIsCopyable (Perm_LOwned _ _) = False
+atomicPermIsCopyable (Perm_LOwned _ _ _) = False
 atomicPermIsCopyable (Perm_LCurrent _) = True
+atomicPermIsCopyable Perm_LFinished = True
 atomicPermIsCopyable (Perm_Struct ps) = and $ RL.mapToList permIsCopyable ps
 atomicPermIsCopyable (Perm_Fun _) = True
 atomicPermIsCopyable (Perm_BVProp _) = True
@@ -4481,10 +4488,6 @@ lownedPermCouldProve (LOwnedPermBlock (PExpr_Var x) bp) ps =
                bvRangesCouldOverlap (llvmBlockRange bp) rng
              _ -> False) $
   varAtomicPermsInDistPerms x ps
-lownedPermCouldProve (LOwnedPermLifetime (PExpr_Var l) _ ps_out) ps =
-  any (\case Perm_LOwned _ _ -> True
-             _ -> False) (varAtomicPermsInDistPerms l ps) ||
-  lownedPermsCouldProve ps_out ps
 lownedPermCouldProve _ _ = False
 
 -- | Test if an 'LOwnedPerms' list could help prove any of a list of permissions
@@ -4647,9 +4650,10 @@ instance FreeVars (AtomicPerm tp) where
   freeVars Perm_IsLLVMPtr = NameSet.empty
   freeVars (Perm_LLVMBlockShape sh) = freeVars sh
   freeVars (Perm_LLVMFrame fperms) = freeVars $ map fst fperms
-  freeVars (Perm_LOwned ps_in ps_out) =
-    NameSet.union (freeVars ps_in) (freeVars ps_out)
+  freeVars (Perm_LOwned ls ps_in ps_out) =
+    NameSet.unions [freeVars ls, freeVars ps_in, freeVars ps_out]
   freeVars (Perm_LCurrent l) = freeVars l
+  freeVars Perm_LFinished = NameSet.empty
   freeVars (Perm_Struct ps) = NameSet.unions $ RL.mapToList freeVars ps
   freeVars (Perm_Fun fun_perm) = freeVars fun_perm
   freeVars (Perm_BVProp prop) = freeVars prop
@@ -4706,8 +4710,6 @@ instance FreeVars (LOwnedPerm a) where
     NameSet.unions [freeVars e, freeVars fp]
   freeVars (LOwnedPermBlock e bp) =
     NameSet.unions [freeVars e, freeVars bp]
-  freeVars (LOwnedPermLifetime e ps_in ps_out) =
-    NameSet.unions [freeVars e, freeVars ps_in, freeVars ps_out]
 
 instance FreeVars (LOwnedPerms ps) where
   freeVars = NameSet.unions . RL.mapToList freeVars
@@ -4770,7 +4772,7 @@ instance NeededVars (AtomicPerm a) where
   neededVars (Perm_LLVMArray ap) = neededVars ap
   neededVars (Perm_LLVMBlock bp) = neededVars bp
   neededVars (Perm_LLVMBlockShape _) = NameSet.empty
-  neededVars p@(Perm_LOwned _ _) = freeVars p
+  neededVars p@(Perm_LOwned _ _ _) = freeVars p
   neededVars p = freeVars p
 
 instance NeededVars (LLVMFieldPerm w sz) where
@@ -5033,9 +5035,10 @@ instance SubstVar s m => Substable s (AtomicPerm a) m where
     [nuMP| Perm_LLVMBlockShape sh |] ->
       Perm_LLVMBlockShape <$> genSubst s sh
     [nuMP| Perm_LLVMFrame fp |] -> Perm_LLVMFrame <$> genSubst s fp
-    [nuMP| Perm_LOwned ps_in ps_out |] ->
-      Perm_LOwned <$> genSubst s ps_in <*> genSubst s ps_out
+    [nuMP| Perm_LOwned ls ps_in ps_out |] ->
+      Perm_LOwned <$> genSubst s ls <*> genSubst s ps_in <*> genSubst s ps_out
     [nuMP| Perm_LCurrent e |] -> Perm_LCurrent <$> genSubst s e
+    [nuMP| Perm_LFinished |] -> return Perm_LFinished
     [nuMP| Perm_Struct tps |] -> Perm_Struct <$> genSubst s tps
     [nuMP| Perm_Fun fperm |] -> Perm_Fun <$> genSubst s fperm
     [nuMP| Perm_BVProp prop |] -> Perm_BVProp <$> genSubst s prop
@@ -5159,9 +5162,6 @@ instance SubstVar s m => Substable s (LOwnedPerm a) m where
       LOwnedPermField <$> genSubst s e <*> genSubst s fp
     [nuMP| LOwnedPermBlock e bp |] ->
       LOwnedPermBlock <$> genSubst s e <*> genSubst s bp
-    [nuMP| LOwnedPermLifetime e ps_in ps_out |] ->
-      LOwnedPermLifetime <$> genSubst s e <*> genSubst s ps_in
-                         <*> genSubst s ps_out
 
 instance SubstVar s m => Substable1 s LOwnedPerm m where
   genSubst1 = genSubst
@@ -5180,9 +5180,9 @@ instance SubstVar PermVarSubst m =>
          Substable PermVarSubst (LifetimeCurrentPerms ps) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| AlwaysCurrentPerms |] -> return AlwaysCurrentPerms
-    [nuMP| LOwnedCurrentPerms l ps_in ps_out |] ->
-      LOwnedCurrentPerms <$> genSubst s l <*> genSubst s ps_in
-                         <*> genSubst s ps_out
+    [nuMP| LOwnedCurrentPerms l ls ps_in ps_out |] ->
+      LOwnedCurrentPerms <$> genSubst s l <*> genSubst s ls
+      <*> genSubst s ps_in <*> genSubst s ps_out
     [nuMP| CurrentTransPerms ps l |] ->
       CurrentTransPerms <$> genSubst s ps <*> genSubst s l
 
@@ -5784,13 +5784,16 @@ instance AbstractVars (AtomicPerm a) where
   abstractPEVars ns1 ns2 (Perm_LLVMFrame fp) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LLVMFrame |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 fp
-  abstractPEVars ns1 ns2 (Perm_LOwned ps_in ps_out) =
+  abstractPEVars ns1 ns2 (Perm_LOwned ls ps_in ps_out) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LOwned |])
+    `clMbMbApplyM` abstractPEVars ns1 ns2 ls
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps_in
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps_out
   abstractPEVars ns1 ns2 (Perm_LCurrent e) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LCurrent |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 e
+  abstractPEVars ns1 ns2 Perm_LFinished =
+    absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LFinished |])
   abstractPEVars ns1 ns2 (Perm_Struct ps) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_Struct |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps
@@ -5920,11 +5923,6 @@ instance AbstractVars (LOwnedPerm a) where
     absVarsReturnH ns1 ns2 $(mkClosed [| LOwnedPermBlock |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 e
     `clMbMbApplyM` abstractPEVars ns1 ns2 bp
-  abstractPEVars ns1 ns2 (LOwnedPermLifetime e ps_in ps_out) =
-    absVarsReturnH ns1 ns2 $(mkClosed [| LOwnedPermLifetime |])
-    `clMbMbApplyM` abstractPEVars ns1 ns2 e
-    `clMbMbApplyM` abstractPEVars ns1 ns2 ps_in
-    `clMbMbApplyM` abstractPEVars ns1 ns2 ps_out
 
 instance AbstractVars (LOwnedPerms ps) where
   abstractPEVars ns1 ns2 MNil =
@@ -6095,9 +6093,11 @@ instance AbstractNamedShape w (AtomicPerm a) where
   abstractNSM (Perm_NamedConj n args off) = 
     mbMap2 (Perm_NamedConj n) <$> abstractNSM args <*> abstractNSM off
   abstractNSM (Perm_LLVMFrame fp) = fmap Perm_LLVMFrame <$> abstractNSM fp
-  abstractNSM (Perm_LOwned ps_in ps_out) =
-    mbMap2 Perm_LOwned <$> abstractNSM ps_in <*> abstractNSM ps_out
+  abstractNSM (Perm_LOwned ls ps_in ps_out) =
+    mbMap3 Perm_LOwned <$> abstractNSM ls <*> abstractNSM ps_in <*>
+    abstractNSM ps_out
   abstractNSM (Perm_LCurrent e) = fmap Perm_LCurrent <$> abstractNSM e
+  abstractNSM Perm_LFinished = pureBindingM Perm_LFinished
   abstractNSM (Perm_Struct ps) = fmap Perm_Struct <$> abstractNSM ps
   abstractNSM (Perm_Fun fp) = fmap Perm_Fun <$> abstractNSM fp
   abstractNSM (Perm_BVProp prop) = pureBindingM (Perm_BVProp prop)
@@ -6136,9 +6136,6 @@ instance AbstractNamedShape w (LOwnedPerm a) where
     mbMap2 LOwnedPermField <$> abstractNSM e <*> abstractNSM fp
   abstractNSM (LOwnedPermBlock e bp) =
     mbMap2 LOwnedPermBlock <$> abstractNSM e <*> abstractNSM bp
-  abstractNSM (LOwnedPermLifetime e ps_in ps_out) =
-    mbMap3 LOwnedPermLifetime <$> abstractNSM e <*> abstractNSM ps_in
-                              <*> abstractNSM ps_out
 
 instance AbstractNamedShape w (ValuePerms as) where
   abstractNSM ValPerms_Nil = pureBindingM ValPerms_Nil
@@ -6627,7 +6624,7 @@ instance GetDetVarsClauses (AtomicPerm a) where
   getDetVarsClauses (Perm_LLVMBlockShape sh) = getDetVarsClauses sh
   getDetVarsClauses (Perm_LLVMFrame frame_perm) =
     concat <$> mapM (getDetVarsClauses . fst) frame_perm
-  getDetVarsClauses (Perm_LOwned _ _) = return []
+  getDetVarsClauses (Perm_LOwned _ _ _) = return []
   getDetVarsClauses _ = return []
 
 instance (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>

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

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

@@ -603,9 +603,10 @@ tcBlockAtomic e = tcError (pos e) "Expected llvmblock perm"
 
 -- | Check a lifetime permission literal
 tcLifetimeAtomic :: AstExpr -> Tc (AtomicPerm LifetimeType)
-tcLifetimeAtomic (ExLOwned _ x y) =
+tcLifetimeAtomic (ExLOwned _ ls x y) =
   do Some x' <- tcLOwnedPerms x
      Some y' <- tcLOwnedPerms y
+     ls' <- mapM tcKExpr ls
      pure (Perm_LOwned x' y')
 tcLifetimeAtomic (ExLCurrent _ l) = Perm_LCurrent <$> tcOptLifetime l
 tcLifetimeAtomic e = tcError (pos e) "Expected lifetime perm"

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

@@ -69,7 +69,7 @@ data AstExpr
   | ExLessEqual Pos AstExpr AstExpr -- ^ less-than or equal-to bitvector proposition
 
   | ExEq Pos AstExpr            -- ^ equal permission
-  | ExLOwned Pos [(Located String, AstExpr)] [(Located String, AstExpr)] -- ^ owned permission
+  | ExLOwned Pos [AstExpr] [(Located String, AstExpr)] [(Located String, AstExpr)] -- ^ owned permission
   | ExLCurrent Pos (Maybe AstExpr) -- ^ current permission
   | ExShape Pos AstExpr -- ^ shape literal
   | ExFree Pos AstExpr -- ^ free literal
@@ -106,7 +106,7 @@ instance HasPos AstExpr where
   pos (ExNotEqual   p _ _      ) = p
   pos (ExLessThan   p _ _      ) = p
   pos (ExLessEqual  p _ _      ) = p
-  pos (ExLOwned     p _ _      ) = p
+  pos (ExLOwned     p _ _ _    ) = p
   pos (ExLCurrent   p _        ) = p
   pos (ExShape      p _        ) = p
   pos (ExFree       p _        ) = p