diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs index bbf88f092e..94b18ac804 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs @@ -161,6 +161,7 @@ instance ContainsIRTRecName (AtomicPerm a) where containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps containsIRTRecName _ (Perm_Fun _) = False containsIRTRecName _ (Perm_BVProp _) = False + containsIRTRecName _ Perm_Any = False instance ContainsIRTRecName (LLVMFieldPerm w sz) where containsIRTRecName n fp = containsIRTRecName n $ llvmFieldContents fp @@ -425,6 +426,8 @@ instance IRTTyVars (AtomicPerm a) where throwError "fun perm in an IRT definition!" [nuMP| Perm_BVProp _ |] -> throwError "BVProp in an IRT definition!" + [nuMP| Perm_Any |] -> + throwError "any perm in an IRT definition!" -- | Get all IRT type variables in a shape expression instance IRTTyVars (PermExpr (LLVMShapeType w)) where @@ -676,6 +679,8 @@ instance IRTDescs (AtomicPerm a) where error "fun perm made it to IRTDesc translation" ([nuMP| Perm_BVProp _ |], _) -> error "BVProp made it to IRTDesc translation" + ([nuMP| Perm_Any |], _) -> + error "any perm made it to IRTDesc translation" -- | Get the IRTDescs associated to a shape expression instance IRTDescs (PermExpr (LLVMShapeType w)) where diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index d1608cef1a..8ad1593eea 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -1310,6 +1310,36 @@ data SimplImpl ps_in ps_out where PermExprs args -> PermOffset a -> ExprVar a -> PermExpr a -> SimplImpl (RNil :> a :> a) (RNil :> a) + -- | Two inconsistent equality permissions combine to an any: + -- + -- > x:eq(e1), x:eq(e2) -o x:any (when e1 /= e2) + SImpl_IntroAnyEqEq :: ExprVar a -> PermExpr a -> PermExpr a -> + SimplImpl (RNil :> a :> a) (RNil :> a) + + -- | Equality to a word along with a pointer permission combine to an any: + -- + -- > x:eq(llvmword(e)), x:p -o x:any (if p is a ptr, array, or block perm) + SImpl_IntroAnyWordPtr :: + (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) -> + PermExpr (BVType w) -> AtomicPerm (LLVMPointerType w) -> + SimplImpl (RNil :> LLVMPointerType w :> LLVMPointerType w) + (RNil :> LLVMPointerType w) + + -- | Eliminate an @any@ permission to an equality: + -- + -- > x:any -o x:eq(e) + SImpl_ElimAnyToEq :: ExprVar a -> PermExpr a -> + SimplImpl (RNil :> a) (RNil :> a) + + -- | Eliminate an @any@ permission to a pointer permission containing an @any@ + -- permission: + -- + -- > x:any -o x:[l]ptr((rw,off) |-> any) + SImpl_ElimAnyToPtr :: + (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => + ExprVar (LLVMPointerType w) -> LLVMFieldPerm w sz -> + SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w) + -- | A single step of permission implication. These can have multiple, -- disjunctive conclusions, each of which can bind some number of variables, and @@ -2143,7 +2173,19 @@ simplImplIn (SImpl_ReachabilityTrans x rp args off y e) = let npn = recPermName rp in distPerms2 x (ValPerm_Named npn (PExprs_Cons args (PExpr_Var y)) off) y (ValPerm_Named npn (PExprs_Cons args e) off) - +simplImplIn (SImpl_IntroAnyEqEq x e1 e2) = + if exprsUnequal e1 e2 then + distPerms2 x (ValPerm_Eq e1) x (ValPerm_Eq e2) + else + error "simplImplIn: SImpl_IntroAnyEqEq: expressions not unequal" +simplImplIn (SImpl_IntroAnyWordPtr x e p) = + if isLLVMPointerPerm p then + distPerms2 x (ValPerm_Eq $ PExpr_LLVMWord e) x (ValPerm_Conj1 p) + else + error "simplImplIn: SImpl_IntroAnyWordPtr: expressions not unequal" +simplImplIn (SImpl_ElimAnyToEq x _) = + distPerms1 x ValPerm_Any +simplImplIn (SImpl_ElimAnyToPtr x _) = distPerms1 x ValPerm_Any -- | Compute the output permissions of a 'SimplImpl' implication simplImplOut :: SimplImpl ps_in ps_out -> DistPerms ps_out @@ -2525,6 +2567,14 @@ simplImplOut (SImpl_NamedArgRead x npn args off memb) = off) simplImplOut (SImpl_ReachabilityTrans x rp args off _ e) = distPerms1 x (ValPerm_Named (recPermName rp) (PExprs_Cons args e) off) +simplImplOut (SImpl_IntroAnyEqEq x _ _) = distPerms1 x ValPerm_Any +simplImplOut (SImpl_IntroAnyWordPtr x _ _) = distPerms1 x ValPerm_Any +simplImplOut (SImpl_ElimAnyToEq x e) = distPerms1 x (ValPerm_Eq e) +simplImplOut (SImpl_ElimAnyToPtr x fp) = + if llvmFieldContents fp == ValPerm_Any then + distPerms1 x (ValPerm_LLVMField fp) + else + error "simplImplOut: SImpl_ElimAnyToPtr: non-any contents" -- | Compute the input permissions of a 'SimplImpl' implication in a binding mbSimplImplIn :: Mb ctx (SimplImpl ps_in ps_out) -> Mb ctx (DistPerms ps_in) @@ -3052,6 +3102,14 @@ instance SubstVar PermVarSubst m => SImpl_ReachabilityTrans <$> genSubst s x <*> genSubst s rp <*> genSubst s args <*> genSubst s off <*> genSubst s y <*> genSubst s e + [nuMP| SImpl_IntroAnyEqEq x e1 e2 |] -> + SImpl_IntroAnyEqEq <$> genSubst s x <*> genSubst s e1 <*> genSubst s e2 + [nuMP| SImpl_IntroAnyWordPtr x e p |] -> + SImpl_IntroAnyWordPtr <$> genSubst s x <*> genSubst s e <*> genSubst s p + [nuMP| SImpl_ElimAnyToEq x e |] -> + SImpl_ElimAnyToEq <$> genSubst s x <*> genSubst s e + [nuMP| SImpl_ElimAnyToPtr x fp |] -> + SImpl_ElimAnyToPtr <$> genSubst s x <*> genSubst s fp instance SubstVar PermVarSubst m => Substable PermVarSubst (PermImpl1 ps_in ps_out) m where @@ -3362,6 +3420,13 @@ setVarM memb e = pretty "=" <+> permPretty i e) modifyPSubst (psubstSet memb e) +-- | Set the value for an existential variable to the zero of its type if it has +-- not yet been set +zeroUnsetVarM :: Member vars (a :: CrucibleType) -> ImplM vars s r ps ps () +zeroUnsetVarM memb = + do tp <- RL.get memb <$> cruCtxToTypes <$> use implStateVars + setVarM memb (zeroOfType tp) + -- | Get a free variable that is provably equal to the value of an existential -- variable, let-binding a fresh variable if the evar is instantiated with a -- non-variable expression. It is an error if the evar has no instantiation in @@ -5294,6 +5359,9 @@ implElimAppendIthLLVMBlock _ _ _ = permIndicesForProvingOffset :: (1 <= w, KnownNat w) => [AtomicPerm (LLVMPointerType w)] -> Bool -> PermExpr (BVType w) -> [Int] +-- Special case: if we have an any permission, return just it +permIndicesForProvingOffset ps _ _ + | Just i <- findIndex (== Perm_Any) ps = [i] permIndicesForProvingOffset ps imprecise_p off = let ixs_holdss = flip findMaybeIndices ps $ \p -> case llvmPermContainsOffset off p of @@ -5532,6 +5600,17 @@ recombinePerm' x x_p@(ValPerm_Eq (PExpr_LLVMOffset y off)) p = recombinePerm' x _p p'@(ValPerm_Eq PExpr_Unit) = -- When trying to combine a permission x:eq(()), just drop this permission implDropM x p' +recombinePerm' x (ValPerm_Eq e1) (ValPerm_Eq e2) + | exprsUnequal e1 e2 = + implPushM x (ValPerm_Eq e1) >>> + implSimplM Proxy (SImpl_IntroAnyEqEq x e2 e1) >>> + implPopM x ValPerm_Any +recombinePerm' x (ValPerm_Conj ps) (ValPerm_Eq (PExpr_LLVMWord e)) + | Just i <- findIndex isLLVMPointerPerm ps = + implPushM x (ValPerm_Conj ps) >>> implGetConjM x ps i >>>= \ps' -> + implPopM x (ValPerm_Conj ps') >>> + implSimplM Proxy (SImpl_IntroAnyWordPtr x e (ps!!i)) >>> + recombinePerm x ValPerm_Any recombinePerm' x p p'@(ValPerm_Eq _) = -- NOTE: we could handle this by swapping the stack with the variable perm and -- calling recombinePerm again, but this could potentially create permission @@ -5891,8 +5970,17 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of proveVarEq :: NuMatchingAny1 r => ExprVar a -> Mb vars (PermExpr a) -> ImplM vars s r (ps :> a) ps () proveVarEq x mb_e = - proveEq (PExpr_Var x) mb_e >>>= \some_eqp -> - introEqReflM x >>> implCastPermM Proxy x (fmap ValPerm_Eq some_eqp) + getPerm x >>>= \case + p@(ValPerm_Conj ps) + | Just i <- findIndex (== Perm_Any) ps -> + implPushM x p >>> implCopyConjM x ps i >>> implPopM x p >>> + -- Zero out all bound variables in mb_e that have not yet been set + mapM_ (\(Some memb) -> zeroUnsetVarM memb) (boundVars mb_e) >>> + partialSubstForceM mb_e "proveVarEq" >>>= \e -> + implSimplM Proxy (SImpl_ElimAnyToEq x e) + _ -> + proveEq (PExpr_Var x) mb_e >>>= \some_eqp -> + introEqReflM x >>> implCastPermM Proxy x (fmap ValPerm_Eq some_eqp) -- | Build proofs that @x1:eq(e1),...,xn:eq(en)@ on top of the stack proveVarsEq :: NuMatchingAny1 r => RAssign ExprVar as -> @@ -6487,6 +6575,18 @@ proveVarLLVMFieldH2 x (Perm_LLVMArray ap) off mb_fp implSimplM Proxy (SImpl_LLVMArrayToField x sub_ap sz) >>> proveVarLLVMFieldH x (Perm_LLVMField fp) off mb_fp +-- If we have an any permission, eliminate it to a field and recurse +proveVarLLVMFieldH2 x Perm_Any off (mb_fp :: Mb vars (LLVMFieldPerm w sz)) = + getPSubst >>>= \psubst -> + let l = fromMaybe PExpr_Always (partialSubst psubst $ + mbLLVMFieldLifetime mb_fp) + rw = fromMaybe PExpr_Write $ partialSubst psubst $ mbLLVMFieldRW mb_fp + p = ValPerm_Any :: ValuePerm (LLVMPointerType sz) + fp = LLVMFieldPerm rw l off p in + implCopyM x ValPerm_Any >>> recombinePerm x ValPerm_Any >>> + implSimplM Proxy (SImpl_ElimAnyToPtr x fp) >>> + proveVarLLVMFieldH x (Perm_LLVMField fp) off mb_fp + -- If none of the above cases match, then fail proveVarLLVMFieldH2 x p _ mb_fp = implFailVarM "proveVarLLVMFieldH" x (ValPerm_Conj1 p) @@ -7478,7 +7578,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps implSwapInsertConjM x (Perm_LLVMBlock $ llvmFieldPermToBlock fp) ps' 0 --- If proving a field shape, prove the remaining blocks and then prove the +-- If proving an array shape, prove the remaining blocks and then prove the -- corresponding array permission -- -- FIXME: see above FIXME on proving field shapes @@ -7699,6 +7799,23 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps proveVarLLVMBlocks x ps psubst (mb_bp' : mb_bps) +-- If the shape of mb_bp is an unset variable z, mb_bp has a fixed constant +-- length, and there is an any permission on the left, recursively prove a +-- memblock permission with shape fieldsh(any) +proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps + | [nuMP| PExpr_Var mb_z |] <- mb_sh + , Left memb <- mbNameBoundP mb_z + , Nothing <- psubstLookup psubst memb + , elem Perm_Any ps + , Just len <- partialSubst psubst (mbLLVMBlockLen mb_bp) + , Just len_int <- bvMatchConstInt len + , Just (Some (sz :: NatRepr sz)) <- someNat (8 * len_int) + , Left LeqProof <- decideLeq (knownNat @1) sz + , p <- ValPerm_Any :: ValuePerm (LLVMPointerType sz) = + setVarM memb (withKnownNat sz $ PExpr_FieldShape $ LLVMFieldShape p) >>> + getPSubst >>>= \psubst' -> + proveVarLLVMBlocks2 x ps psubst' mb_bp mb_sh mb_bps + -- If the shape of mb_bp is an unset variable z and there is a field permission -- on the left that contains all the offsets of mb_bp, recursively prove a -- memblock permission with shape fieldsh(eq(y)) for fresh evar y, which is the @@ -8197,6 +8314,10 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of partialSubstForceM mb_prop "proveVarAtomicImpl" >>>= \prop -> implTryProveBVProp x prop + [nuMP| Perm_Any |] + | Just i <- findIndex (== Perm_Any) ps -> + implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps) + _ -> proveVarAtomicImplUnfoldOrFail x ps mb_p diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x b/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x index b5d24c8164..9d1d70e2f3 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x +++ b/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x @@ -38,6 +38,7 @@ $white+ ; "or" { token_ TOr } "true" { token_ TTrue } "false" { token_ TFalse } +"any" { token_ TAny } "empty" { token_ TEmpty } "exists" { token_ TExists } "eq" { token_ TEq } diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y index 1c6880dd8b..2a5af37e3b 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y +++ b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y @@ -48,6 +48,7 @@ import Verifier.SAW.Heapster.UntypedAST 'or' { Located $$ TOr } 'true' { Located $$ TTrue } 'false' { Located $$ TFalse } +'any' { Located $$ TAny } 'empty' { Located $$ TEmpty } 'exists' { Located $$ TExists } 'eq' { Located $$ TEq } @@ -171,6 +172,7 @@ expr :: { AstExpr } | 'true' { ExTrue (pos $1) } | 'false' { ExFalse (pos $1) } + | 'any' { ExAny (pos $1) } | expr 'or' expr { ExOr (pos $2) $1 $3 } | 'eq' '(' expr ')' { ExEq (pos $1) $3 } | 'exists' IDENT ':' type '.' expr { ExExists (pos $1) (locThing $2) $4 $6 } diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index c60bb5cfdb..ba1824c886 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -117,6 +117,12 @@ rlMapMWithAccum f accum (xs :>: x) = (y,accum'') <- f accum' x return (ys :>: y, accum'') +-- | Map a monomorphic binary function across a pair of 'RAssign's to create a +-- standard list, similarly to 'zipWith' +mapToList2 :: (forall a. f a -> g a -> b) -> + RAssign f tps -> RAssign g tps -> [b] +mapToList2 f fs gs = RL.toList $ RL.map2 (\x y -> Constant $ f x y) fs gs + ---------------------------------------------------------------------- -- * Data types and related types @@ -428,6 +434,13 @@ data AtomicPerm (a :: CrucibleType) where Perm_BVProp :: (1 <= w, KnownNat w) => BVProp w -> AtomicPerm (LLVMPointerType w) + -- | A false / unsatisfiable permission from which any permission can be + -- proved. This is different from the false permission because it translated + -- to the unit type instead of the empty type in specifications, and is used + -- in cases where the empty type cannot be proved in specifications + Perm_Any :: AtomicPerm a + + -- | A value permission is a permission to do something with a value, such as -- use it as a pointer. This also includes a limited set of predicates on values -- (you can think about this as "permission to assume the value satisfies this @@ -458,7 +471,7 @@ data ValuePerm (a :: CrucibleType) where -- permissions is the trivially true permission ValPerm_Conj :: [AtomicPerm a] -> ValuePerm a - -- | The false value permission + -- | The false / unsatisfiable permission ValPerm_False :: ValuePerm a -- | A sequence of value permissions @@ -2484,6 +2497,10 @@ pattern ValPerm_Struct ps <- ValPerm_Conj [Perm_Struct ps] where ValPerm_Struct ps = ValPerm_Conj [Perm_Struct ps] +-- | A single @any@ permission +pattern ValPerm_Any :: ValuePerm a +pattern ValPerm_Any = ValPerm_Conj [Perm_Any] + pattern ValPerms_Nil :: () => (tps ~ RNil) => ValuePerms tps pattern ValPerms_Nil = MNil @@ -3284,6 +3301,8 @@ instance Eq (AtomicPerm a) where (Perm_NamedConj _ _ _) == _ = False (Perm_BVProp p1) == (Perm_BVProp p2) = p1 == p2 (Perm_BVProp _) == _ = False + Perm_Any == Perm_Any = True + Perm_Any == _ = False instance Eq1 ValuePerm where eq1 = (==) @@ -3443,6 +3462,7 @@ instance PermPretty (AtomicPerm a) where ((pretty "struct" <+>) . parens) <$> permPrettyM ps permPrettyM (Perm_Fun fun_perm) = permPrettyM fun_perm permPrettyM (Perm_BVProp prop) = permPrettyM prop + permPrettyM Perm_Any = return $ pretty "any" permPrettyM (Perm_NamedConj n args off) = do n_pp <- permPrettyM n args_pp <- permPrettyM args @@ -4398,6 +4418,7 @@ instance Modalize (AtomicPerm a) where Perm_Struct <$> traverseRAssign (modalize rw l) ps modalize _ _ p@(Perm_Fun _) = Just p modalize _ _ p@(Perm_BVProp _) = Just p + modalize _ _ p@Perm_Any = Just p instance Modalize (ExprAndPerm a) where modalize rw l (ExprAndPerm e p) = @@ -4502,6 +4523,7 @@ instance AbstractModalities (AtomicPerm a) where Perm_Struct <$> traverseRAssign abstractModalities ps abstractModalities p@(Perm_Fun _) = pure p abstractModalities p@(Perm_BVProp _) = pure p + abstractModalities p@Perm_Any = pure p -- | Extract the shape-in-bindings for an unfoldable shape @@ -5527,6 +5549,7 @@ offsetLLVMAtomicPerm _ p@Perm_IsLLVMPtr = Just p offsetLLVMAtomicPerm off (Perm_NamedConj n args off') = Just $ Perm_NamedConj n args $ addPermOffsets off' (mkLLVMPermOffset off) offsetLLVMAtomicPerm _ p@(Perm_BVProp _) = Just p +offsetLLVMAtomicPerm _ p@Perm_Any = Just p -- | Add an offset to a field permission offsetLLVMFieldPerm :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> @@ -5806,6 +5829,7 @@ atomicPermIsCopyable Perm_LFinished = True atomicPermIsCopyable (Perm_Struct ps) = and $ RL.mapToList permIsCopyable ps atomicPermIsCopyable (Perm_Fun _) = True atomicPermIsCopyable (Perm_BVProp _) = True +atomicPermIsCopyable Perm_Any = True atomicPermIsCopyable (Perm_NamedConj n args _) = namedPermArgsAreCopyable (namedPermNameArgs n) args @@ -5965,6 +5989,22 @@ unfoldPerm :: NameSortCanFold ns ~ 'True => NamedPerm ns args a -> unfoldPerm (NamedPerm_Defined dp) = unfoldDefinedPerm dp unfoldPerm (NamedPerm_Rec rp) = unfoldRecPerm rp +-- | Test if two expressions are definitely unequal +exprsUnequal :: PermExpr a -> PermExpr a -> Bool +exprsUnequal (PExpr_Var _) _ = False +exprsUnequal (PExpr_Bool b1) (PExpr_Bool b2) = b1 /= b2 +exprsUnequal (PExpr_Nat n1) (PExpr_Nat n2) = n1 /= n2 +exprsUnequal (PExpr_String str1) (PExpr_String str2) = str1 /= str2 +exprsUnequal e1@(PExpr_BV _ _) e2 = not $ bvCouldEqual e1 e2 +{- FIXME: we need to prove the types are equal on both sides for this case: +exprsUnequal (PExpr_Struct es1) (PExpr_Struct es2) = + any $ mapToList2 exprsUnequal es1 es2 +-} +exprsUnequal _ _ = + -- FIXME: maybe we want more cases for shapes and even function handles, + -- though those shouldn't matter for the current uses of exprsUnequal + False + -- | Generic function to get free variables class FreeVars a where freeVars :: a -> NameSet CrucibleType @@ -5974,6 +6014,16 @@ freeVarsRAssign :: FreeVars a => a -> Some (RAssign ExprVar) freeVarsRAssign = foldl (\(Some ns) (SomeName n) -> Some (ns :>: n)) (Some MNil) . toList . freeVars +-- | Get the bound variables of an expression or permission +boundVars :: (NuMatching a, FreeVars a) => Mb (ctx :: RList CrucibleType) a -> + [Some @CrucibleType (Member ctx)] +boundVars mb_a = + mapMaybe (\case + [nuP| SomeName mb_n |] + | Left memb <- mbNameBoundP mb_n -> Just (Some memb) + _ -> Nothing) $ + mbList $ mbMapCl $(mkClosed [| toList . freeVars |]) mb_a + instance FreeVars a => FreeVars (Maybe a) where freeVars = maybe NameSet.empty freeVars @@ -6058,6 +6108,7 @@ instance FreeVars (AtomicPerm tp) where freeVars (Perm_Struct ps) = NameSet.unions $ RL.mapToList freeVars ps freeVars (Perm_Fun fun_perm) = freeVars fun_perm freeVars (Perm_BVProp prop) = freeVars prop + freeVars Perm_Any = NameSet.empty freeVars (Perm_NamedConj _ args off) = NameSet.union (freeVars args) (freeVars off) @@ -6484,6 +6535,7 @@ instance SubstVar s m => Substable s (AtomicPerm a) m where [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 + [nuMP| Perm_Any |] -> return Perm_Any [nuMP| Perm_NamedConj n args off |] -> Perm_NamedConj (mbLift n) <$> genSubst s args <*> genSubst s off @@ -7295,6 +7347,8 @@ instance AbstractVars (AtomicPerm a) where abstractPEVars ns1 ns2 (Perm_BVProp prop) = absVarsReturnH ns1 ns2 $(mkClosed [| Perm_BVProp |]) `clMbMbApplyM` abstractPEVars ns1 ns2 prop + abstractPEVars ns1 ns2 Perm_Any = + absVarsReturnH ns1 ns2 $(mkClosed [| Perm_Any |]) abstractPEVars ns1 ns2 (Perm_NamedConj n args off) = absVarsReturnH ns1 ns2 $(mkClosed [| Perm_NamedConj |]) `clMbMbApplyM` abstractPEVars ns1 ns2 n @@ -7592,6 +7646,7 @@ instance AbstractNamedShape w (AtomicPerm a) where 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) + abstractNSM Perm_Any = pureBindingM Perm_Any instance AbstractNamedShape w' (LLVMFieldPerm w sz) where abstractNSM (LLVMFieldPerm rw l off p) = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 2b6407d8dd..960f3094db 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -1098,6 +1098,9 @@ data AtomicPermTrans ctx a where APTrans_BVProp :: (1 <= w, KnownNat w) => BVPropTrans ctx w -> AtomicPermTrans ctx (LLVMPointerType w) + -- | Any permissions have no SAW terms + APTrans_Any :: AtomicPermTrans ctx a + -- | The translation of a proof of a 'BVProp' data BVPropTrans ctx w = BVPropTrans (Mb ctx (BVProp w)) OpenTerm @@ -1243,6 +1246,7 @@ instance IsTermTrans (AtomicPermTrans ctx a) where transTerms (APTrans_Struct pctx) = transTerms pctx transTerms (APTrans_Fun _ t) = [t] transTerms (APTrans_BVProp prop) = transTerms prop + transTerms APTrans_Any = [] instance IsTermTrans (BVPropTrans ctx w) where transTerms (BVPropTrans _ t) = [t] @@ -1304,6 +1308,7 @@ atomicPermTransPerm prxs (APTrans_Struct ps) = atomicPermTransPerm _ (APTrans_Fun fp _) = fmap Perm_Fun fp atomicPermTransPerm _ (APTrans_BVProp (BVPropTrans prop _)) = fmap Perm_BVProp prop +atomicPermTransPerm prxs APTrans_Any = nuMulti prxs $ const $ Perm_Any -- | Extract out the permissions from a context of permission translations permTransCtxPerms :: RAssign Proxy ctx -> PermTransCtx ctx ps -> @@ -1368,6 +1373,7 @@ instance ExtPermTrans AtomicPermTrans where extPermTrans (APTrans_Fun fp t) = APTrans_Fun (extMb fp) t extPermTrans (APTrans_BVProp prop_trans) = APTrans_BVProp $ extPermTrans prop_trans + extPermTrans APTrans_Any = APTrans_Any instance ExtPermTrans LLVMArrayPermTrans where extPermTrans (LLVMArrayPermTrans ap len sh {- bs -} t) = @@ -1790,6 +1796,7 @@ instance TransInfo info => return $ mkTypeTrans1 tp_term (APTrans_Fun fun_perm) [nuMP| Perm_BVProp prop |] -> fmap APTrans_BVProp <$> translate prop + [nuMP| Perm_Any |] -> return $ mkTypeTrans0 APTrans_Any -- | Translate an array permission to a 'TypeTrans' for an array permission -- translation, also returning the translations of the bitvector width as a @@ -3331,6 +3338,30 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of transTerm1 ptrans_y])]) m + [nuMP| SImpl_IntroAnyEqEq _ _ _ |] -> + do tp_trans <- translateSimplImplOutHead mb_simpl + withPermStackM RL.tail + (\(pctx :>: _ :>: _) -> + pctx :>: typeTransF tp_trans []) m + + [nuMP| SImpl_IntroAnyWordPtr _ _ _ |] -> + do tp_trans <- translateSimplImplOutHead mb_simpl + withPermStackM RL.tail + (\(pctx :>: _ :>: _) -> + pctx :>: typeTransF tp_trans []) m + + [nuMP| SImpl_ElimAnyToEq _ _ |] -> + do tp_trans <- translateSimplImplOutHead mb_simpl + withPermStackM id + (\(pctx :>: _) -> + pctx :>: typeTransF tp_trans []) m + + [nuMP| SImpl_ElimAnyToPtr _ _ |] -> + do tp_trans <- translateSimplImplOutHead mb_simpl + withPermStackM id + (\(pctx :>: _) -> + pctx :>: typeTransF tp_trans []) m + -- | A flag to indicate whether the translation of a permission implication -- contains any failures diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Token.hs b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs index aaca511b3c..b490184f3c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Token.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs @@ -33,6 +33,7 @@ data Token | TOr -- ^ keyword @or@ | TTrue -- ^ keyword @true@ | TFalse -- ^ keyword @false@ + | TAny -- ^ keyword @any@ | TEmpty -- ^ keyword @empty@ | TExists -- ^ keyword @exists@ | TEq -- ^ keyword @eq@ @@ -115,6 +116,7 @@ describeToken t = TOr -> "keyword 'or'" TTrue -> "keyword 'true'" TFalse -> "keyword 'false'" + TAny -> "keyword 'any'" TEmpty -> "keyword 'empty'" TExists -> "keyword 'exists'" TEq -> "keyword 'eq'" diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs index 3c52c1ef52..e1b7efacb0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs @@ -524,6 +524,7 @@ tcAtomicPerm (LLVMFrameRepr w) e = withKnownNat w (tcFrameAtomic e) tcAtomicPerm (LLVMBlockRepr w) e = withKnownNat w (tcBlockAtomic e) tcAtomicPerm (StructRepr tys) e = tcStructAtomic tys e tcAtomicPerm LifetimeRepr e = tcLifetimeAtomic e +tcAtomicPerm _ (ExAny _) = return Perm_Any tcAtomicPerm _ e = tcError (pos e) "Expected perm" -- | Build a field permission using an 'LLVMFieldShape' diff --git a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs index 96143e60de..c27e038667 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs @@ -53,6 +53,7 @@ data AstExpr | ExLlvmFrame Pos [(AstExpr, Natural)] -- ^ llvmframe literal | ExOr Pos AstExpr AstExpr -- ^ or permission | ExFalse Pos -- ^ false permission + | ExAny Pos -- ^ any permission | ExEmptySh Pos -- ^ empty shape | ExEqSh Pos AstExpr AstExpr -- ^ equal shape @@ -101,6 +102,7 @@ instance HasPos AstExpr where pos (ExOr p _ _ ) = p pos (ExFalse p ) = p pos (ExTrue p ) = p + pos (ExAny p ) = p pos (ExExists p _ _ _ ) = p pos (ExSeqSh p _ _ ) = p pos (ExOrSh p _ _ ) = p