From 938998b5af3c49654b2e018c4a77ebc95dd0d85f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 20 Apr 2022 06:41:36 -0700 Subject: [PATCH 1/2] added syntax for the false permission and the false shape --- heapster-saw/src/Verifier/SAW/Heapster/Parser.y | 4 ++++ heapster-saw/src/Verifier/SAW/Heapster/Token.hs | 4 ++++ heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs | 2 ++ heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs | 6 +++++- 4 files changed, 15 insertions(+), 1 deletion(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y index 000ab3bc6c..1c6880dd8b 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y +++ b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y @@ -47,6 +47,7 @@ import Verifier.SAW.Heapster.UntypedAST '<=u' { Located $$ TUnsignedLe } 'or' { Located $$ TOr } 'true' { Located $$ TTrue } +'false' { Located $$ TFalse } 'empty' { Located $$ TEmpty } 'exists' { Located $$ TExists } 'eq' { Located $$ TEq } @@ -72,6 +73,7 @@ import Verifier.SAW.Heapster.UntypedAST 'struct' { Located $$ TStruct } 'shape' { Located $$ TShape } 'emptysh' { Located $$ TEmptySh } +'falsesh' { Located $$ TFalseSh } 'eqsh' { Located $$ TEqSh } 'ptrsh' { Located $$ TPtrSh } 'fieldsh' { Located $$ TFieldSh } @@ -153,6 +155,7 @@ expr :: { AstExpr } -- Shapes | 'emptysh' { ExEmptySh (pos $1) } + | 'falsesh' { ExFalseSh (pos $1) } | expr 'orsh' expr { ExOrSh (pos $2) $1 $3 } | expr ';' expr { ExSeqSh (pos $2) $1 $3 } | 'eqsh' '(' expr ',' expr ')' { ExEqSh (pos $1) $3 $5 } @@ -167,6 +170,7 @@ expr :: { AstExpr } -- Value Permissions | 'true' { ExTrue (pos $1) } + | 'false' { ExFalse (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/Token.hs b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs index 4f342923cf..aaca511b3c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Token.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs @@ -32,6 +32,7 @@ data Token | TUnsignedLe -- ^ symbol @<=u@ | TOr -- ^ keyword @or@ | TTrue -- ^ keyword @true@ + | TFalse -- ^ keyword @false@ | TEmpty -- ^ keyword @empty@ | TExists -- ^ keyword @exists@ | TEq -- ^ keyword @eq@ @@ -57,6 +58,7 @@ data Token | TStruct -- ^ keyword @struct@ | TShape -- ^ keyword @shape@ | TEmptySh -- ^ keyword @emptysh@ + | TFalseSh -- ^ keyword @falsesh@ | TEqSh -- ^ keyword @eqsh@ | TPtrSh -- ^ keyword @ptrsh@ | TFieldSh -- ^ keyword @fieldsh@ @@ -112,6 +114,7 @@ describeToken t = TUnsignedLe -> "'<=u'" TOr -> "keyword 'or'" TTrue -> "keyword 'true'" + TFalse -> "keyword 'false'" TEmpty -> "keyword 'empty'" TExists -> "keyword 'exists'" TEq -> "keyword 'eq'" @@ -137,6 +140,7 @@ describeToken t = TStruct -> "keyword 'struct'" TShape -> "keyword 'shape'" TEmptySh -> "keyword 'emptysh'" + TFalseSh -> "keyword 'falsesh'" TEqSh -> "keyword 'eqsh'" TPtrSh -> "keyword 'ptrsh'" TFieldSh -> "keyword 'fieldsh'" diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs index 51a0c87531..2fc64dfa66 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs @@ -436,6 +436,7 @@ tcLLVMShape (ExArraySh _ len stride sh) = <$> tcKExpr len <*> (Bytes . fromIntegral <$> tcNatural stride) <*> tcKExpr sh +tcLLVMShape (ExFalseSh _) = pure PExpr_FalseShape tcLLVMShape e = tcError (pos e) "Expected shape" -- | Field and array helper for 'tcLLVMShape' @@ -466,6 +467,7 @@ tcValPermInCtx ctx tp = inParsedCtxM ctx . const . tcValPerm tp -- | Parse a value permission of a known type tcValPerm :: TypeRepr a -> AstExpr -> Tc (ValuePerm a) tcValPerm _ ExTrue{} = pure ValPerm_True +tcValPerm _ ExFalse{} = pure ValPerm_False tcValPerm ty (ExOr _ x y) = ValPerm_Or <$> tcValPerm ty x <*> tcValPerm ty y tcValPerm ty (ExEq _ e) = ValPerm_Eq <$> tcExpr ty e tcValPerm ty (ExExists _ var vartype e) = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs index 125bff3355..96143e60de 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs @@ -51,7 +51,8 @@ data AstExpr | ExStruct Pos [AstExpr] -- ^ struct literal with field expressions | ExLlvmWord Pos AstExpr -- ^ llvmword with value | ExLlvmFrame Pos [(AstExpr, Natural)] -- ^ llvmframe literal - | ExOr Pos AstExpr AstExpr + | ExOr Pos AstExpr AstExpr -- ^ or permission + | ExFalse Pos -- ^ false permission | ExEmptySh Pos -- ^ empty shape | ExEqSh Pos AstExpr AstExpr -- ^ equal shape @@ -63,6 +64,7 @@ data AstExpr | ExFieldSh Pos (Maybe AstExpr) AstExpr -- ^ field shape | ExPtrSh Pos (Maybe AstExpr) (Maybe AstExpr) AstExpr -- ^ pointer shape | ExArraySh Pos AstExpr AstExpr AstExpr -- ^ array shape + | ExFalseSh Pos -- ^ false shape | ExEqual Pos AstExpr AstExpr -- ^ equal bitvector proposition | ExNotEqual Pos AstExpr AstExpr -- ^ not-equal bitvector proposition @@ -97,6 +99,7 @@ instance HasPos AstExpr where pos (ExEqSh p _ _ ) = p pos (ExEq p _ ) = p pos (ExOr p _ _ ) = p + pos (ExFalse p ) = p pos (ExTrue p ) = p pos (ExExists p _ _ _ ) = p pos (ExSeqSh p _ _ ) = p @@ -119,6 +122,7 @@ instance HasPos AstExpr where pos (ExLlvmFrame p _ ) = p pos (ExArray p _ _ _ _ _ _) = p pos (ExArraySh p _ _ _ ) = p + pos (ExFalseSh p ) = p -- | Returns outermost position instance HasPos AstType where From eee5159f8b20a05f434b13a5d63d89706840a4f5 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 20 Apr 2022 06:47:15 -0700 Subject: [PATCH 2/2] whoops, forgot to add support for the false permission and false shape to the lexer --- heapster-saw/src/Verifier/SAW/Heapster/Lexer.x | 2 ++ 1 file changed, 2 insertions(+) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x b/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x index f4a63c97fa..b5d24c8164 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x +++ b/heapster-saw/src/Verifier/SAW/Heapster/Lexer.x @@ -37,6 +37,7 @@ $white+ ; "<=u" { token_ TUnsignedLe } "or" { token_ TOr } "true" { token_ TTrue } +"false" { token_ TFalse } "empty" { token_ TEmpty } "exists" { token_ TExists } "eq" { token_ TEq } @@ -61,6 +62,7 @@ $white+ ; "struct" { token_ TStruct } "shape" { token_ TShape } "emptysh" { token_ TEmptySh } +"falsesh" { token_ TFalseSh } "eqsh" { token_ TEqSh } "ptrsh" { token_ TPtrSh } "fieldsh" { token_ TFieldSh }