Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heapster false permission and shape syntax #1630

Merged
merged 3 commits into from
Apr 20, 2022
Merged

Heapster false permission and shape syntax #1630

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
938998b
added syntax for the false permission and the false shape
Apr 20, 2022
eee5159
whoops, forgot to add support for the false permission and false shap…
Apr 20, 2022
8612646
Merge branch 'master' into heapster/false-perm-syntax
mergify[bot] Apr 20, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Lexer.x
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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 }
Expand Down
4 changes: 4 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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 }
Expand Down Expand Up @@ -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 }
Expand All @@ -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 }
Expand Down
4 changes: 4 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Token.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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@
Expand All @@ -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@
Expand Down Expand Up @@ -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'"
Expand All @@ -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'"
Expand Down
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down Expand Up @@ -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) =
Expand Down
6 changes: 5 additions & 1 deletion heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down