diff --git a/acsl-parser/Makefile b/acsl-parser/Makefile index 19b0e11..e0b13c6 100644 --- a/acsl-parser/Makefile +++ b/acsl-parser/Makefile @@ -1,7 +1,7 @@ CUP = java_cup.Main -CUPFLAGS = -expect 400 -locations +CUPFLAGS = -expect 7 -locations JLEX = JLex.Main diff --git a/acsl-parser/acsl-parser.jar b/acsl-parser/acsl-parser.jar index 825570f..6d8b6cd 100644 Binary files a/acsl-parser/acsl-parser.jar and b/acsl-parser/acsl-parser.jar differ diff --git a/acsl-parser/acsl.cf b/acsl-parser/acsl.cf index d212877..21a0f19 100644 --- a/acsl-parser/acsl.cf +++ b/acsl-parser/acsl.cf @@ -30,14 +30,18 @@ -- Figure references are to ACSL Manual: -- https://frama-c.com/download/acsl.pdf +-- This grammar merges Predicate and Term into Expr to avoid conflicts. + --- Annotation --------------------------------------------- AnnotContract. Annotation ::= "/*@" FunctionContract "*/"; AnnotAssertion. Annotation ::= "/*@" Assertion "*/"; LoopAnnot. Annotation ::= "/*@" LoopInvariant "*/"; +entrypoints Annotation, FunctionContract, Assertion, LoopInvariant; + ---- Assertions -------------------------------------------- -RegularAssertion1. Assertion ::= AssertionKind Predicate ";" ; -RegularAssertion2. Assertion ::= AssertionKind Predicate ; +RegularAssertion. Assertion ::= AssertionKind Expr ; +_. Assertion ::= Assertion ";" ; -- BehaviourAssertion. Assertion ::= for id ... (see Figure 2.9 in the ACSL standard) ---- Contracts (2.6) --------------------------------------- @@ -51,16 +55,16 @@ SomeClauseKind. MaybeClauseKind ::= ClauseKind ; ClauseKindCheck. ClauseKind ::= "check" ; ClauseKindAdmit. ClauseKind ::= "admit" ; -ARequiresClause. RequiresClause ::= MaybeClauseKind "requires" Predicate ; +ARequiresClause. RequiresClause ::= MaybeClauseKind "requires" Expr ; terminator RequiresClause ";" ; NoTerminatesClause. MaybeTerminatesClause ::= ; SomeTerminatesClause. MaybeTerminatesClause ::= TerminatesClause ; -ATerminatesClause. TerminatesClause ::= "terminates" Predicate ";" ; +ATerminatesClause. TerminatesClause ::= "terminates" Expr ";" ; NoDecreasesClause. MaybeDecreasesClause ::= ; SomeDecreasesClause. MaybeDecreasesClause ::= DecreasesClause ; -ADecreasesClause. DecreasesClause ::= "decreases" Term ";" ; -- TODO: ("for" ident)? +ADecreasesClause. DecreasesClause ::= "decreases" Expr ";" ; -- Term -- TODO: ("for" ident)? SimpleClauseAssigns. SimpleClause ::= AssignsClause ; SimpleClauseEnsures. SimpleClause ::= EnsuresClause ; @@ -78,14 +82,14 @@ LocationsNothing. Locations ::= "\\nothing" ; ALocation. Location ::= TSet ; separator nonempty Location "," ; -AnEnsuresClause. EnsuresClause ::= MaybeClauseKind "ensures" Predicate ";" ; +AnEnsuresClause. EnsuresClause ::= MaybeClauseKind "ensures" Expr ";" ; ANamedBehavior. NamedBehavior ::= "behavior" Id ":" BehaviorBody ; terminator NamedBehavior "" ; ABehaviorBody. BehaviorBody ::= [AssumesClause] [RequiresClause] [SimpleClause] ; -AnAssumesClause. AssumesClause ::= "assumes" Predicate ; +AnAssumesClause. AssumesClause ::= "assumes" Expr ; separator AssumesClause ";" ; CompletenessClauseComplete. CompletenessClause ::= "complete" "behaviors" [Id] ; @@ -94,151 +98,208 @@ terminator CompletenessClause ";" ; ---- Loops ------------------------------------------------- -- This is a bit simplified -LoopInvSimple. LoopInvariant ::= "loop" "invariant" Predicate ";" ; - ----- Predicates (2.2) -------------------------------------- -RelOpEQ. RelOp ::= "==" ; -RelOpNEQ. RelOp ::= "!=" ; -RelOpLEQ. RelOp ::= "<=" ; -RelOpGEQ. RelOp ::= ">=" ; -RelOpGT. RelOp ::= ">" ; -RelOpLT. RelOp ::= "<" ; - -PredTrue. Predicate ::= "\\true" ; -PredFalse. Predicate ::= "\\false" ; -PredRelOp. Predicate ::= Term RelOp Term; -- FIXME: Chained relops allowed. -PredApplication. Predicate ::= Id "(" [Term] ")" ; -PredParentheses. Predicate ::= "(" Predicate ")" ; -PredConjunction. Predicate ::= Predicate "&&" Predicate ; -PredDisjunction. Predicate ::= Predicate "||" Predicate ; -PredImplication. Predicate ::= Predicate "==>" Predicate ; -PredEquivalence. Predicate ::= Predicate "<==>" Predicate ; -PredNegation. Predicate ::= "!" Predicate ; -PredXOr. Predicate ::= Predicate "^^" Predicate ; -PredTernaryCond. Predicate ::= Term "?" Predicate ":" Predicate ; -PredTernaryCond2. Predicate ::= Predicate "?" Predicate ":" Predicate ; -PredLocalBinding. Predicate ::= "\\let" Id "=" Term ";" Predicate ; -PredLocalBinding2. Predicate ::= "\\let" Id "=" Predicate ";" Predicate ; -PredForAll. Predicate ::= "\\forall" [Binder] ";" Predicate ; -PredExists. Predicate ::= "\\exists" [Binder] ";" Predicate ; -PredSyntacticNaming. Predicate ::= Id ":" Predicate ; -PredSyntacticNaming2. Predicate ::= String ":" Predicate ; --- PredicateOld is extension for contracts. --- Maybe want separate `ContractPredicate` for this? -PredOld. Predicate ::= "\\old" "(" Predicate ")" ; -PredValid. Predicate ::= "\\valid" "(" [Location] ")" ; - ----- Terms (2.1) ------------------------------------------- -LiteralTrue. Literal ::= "\\true" ; -LiteralFalse. Literal ::= "\\false" ; --- FIXME: Use C-specific literals. -LiteralInt. Literal ::= UnboundedInteger ; -LiteralReal. Literal ::= Double ; -LiteralString. Literal ::= String ; -LiteralChar. Literal ::= Char ; - -BinOpPlus. BinOp ::= "+" ; -BinOpMinus. BinOp ::= "-" ; -BinOpMult. BinOp ::= "*" ; -BinOpDiv. BinOp ::= "/" ; -BinOpMod. BinOp ::= "%" ; -BinOpEQ. BinOp ::= "==" ; -BinOpNEQ. BinOp ::= "!=" ; -BinOpLEQ. BinOp ::= "<=" ; -BinOpGEQ. BinOp ::= ">=" ; -BinOpGT. BinOp ::= ">" ; -BinOpLT. BinOp ::= "<" ; -BinOpAnd. BinOp ::= "&&" ; -BinOpOr. BinOp ::= "||" ; -BinOpXOr. BinOp ::= "^^" ; -BinOpLShift. BinOp ::= "<<" ; -BinOpRShift. BinOp ::= ">>" ; -BinOpBitwiseAnd. BinOp ::= "&" ; -BinOpBitwiseOr. BinOp ::= "|" ; -BinOpBitwiseImpl. BinOp ::= "-->" ; -BinOpBitwiseEquiv. BinOp ::= "<-->" ; -BinOpBitwiseXOr. BinOp ::= "^" ; - -UnaryOpPlus. UnaryOp ::= "+" ; -UnaryOpMinus. UnaryOp ::= "-" ; -UnaryOpNegation. UnaryOp ::= "!" ; -UnaryOpComplementation. UnaryOp ::= "~" ; -UnaryOpPtrDeref. UnaryOp ::= "*" ; -UnaryOpAddressOf. UnaryOp ::= "&" ; - -TermLiteral. Term ::= Literal ; -TermIdent. Term ::= Id ; -TermUnaryOp. Term ::= UnaryOp Term ; -TermBinOp. Term ::= Term BinOp Term ; -TermArrayAccess. Term ::= Term "[" Term "]" ; -TermArrayFunctionalModifier. Term ::= "{" Term "\\with" "[" Term "]" "=" Term "}" ; -TermStructFieldAccess. Term ::= Term "." Id ; -TermFieldFunctionalModifier. Term ::= "{" Term "\\with" "." Id "=" Term "}" ; -TermStructPtrFieldAccess. Term ::= Term "->" Id ; -TermTypeCast. Term ::= "(" TypeExpr ")" Term ; -TermFuncAppl. Term ::= Id "(" [Term] ")" ; -TermParentheses. Term ::= "(" Term ")" ; -TermTernaryCond. Term ::= Term "?" Term ":" Term ; -TermLocalBinding. Term ::= "\\let" Id "=" Term ";" Term ; -TermSizeOfTerm. Term ::= "sizeof" "(" Term ")" ; -TermSizeOfType. Term ::= "sizeof" "(" CTypeSpecifier ")" ; -- FIXME: Should be CTypeExpr -TermSyntacticNaming. Term ::= Id ":" Term ; -TermSyntacticNaming2. Term ::= String ":" Term ; --- TermOld and TermResult are extensions for contracts. --- Maybe want separate `ContractTerm` for this? -TermOld. Term ::= "\\old" "(" Term ")" ; -TermResult. Term ::= "\\result" ; -separator nonempty Term "," ; +LoopInvSimple. LoopInvariant ::= "loop" "invariant" Expr ";" ; + +---- Expressions (Predicates and Terms) (2.2) --------------------------------- + +-- Literals +LitTrue. Lit ::= "\\true" ; +LitFalse. Lit ::= "\\false" ; +LitInt. Lit ::= UnboundedInteger ; +LitReal. Lit ::= Double ; +LitString. Lit ::= String ; +LitChar. Lit ::= Char ; + +-- In increasing order of precedence. +-- Associtivities are given in parentheses. +-- See the ACSL standard for precedence and associativity. + +-- naming (right) +ENaming1. Expr ::= Id ":" Expr ; +ENaming2. Expr ::= String ":" Expr ; + +-- binding (left) +EForAll. Expr2 ::= "\\forall" [Binder] ";" Expr2 ; +EExists. Expr2 ::= "\\exists" [Binder] ";" Expr2 ; +EBinding. Expr2 ::= "\\let" Id "=" Expr2 ";" Expr ; + +-- ternary connective (right) +ETernary. Expr3 ::= Expr3 "?" Expr4 ":" Expr5 ; + +-- logical connectives +EEquiv. Expr4 ::= Expr5 "<==>" Expr4 ; -- (left) +EImplies. Expr5 ::= Expr5 "==>" Expr6 ; -- (right) +EOr. Expr6 ::= Expr7 "||" Expr6 ; -- (left) +EXOr. Expr7 ::= Expr8 "^^" Expr7 ; -- (left) +EAnd. Expr8 ::= Expr9 "&&" Expr8 ; -- (left) + +-- bitwise operators +EBitEquiv. Expr9 ::= Expr10 "<-->" Expr9 ; -- (left) +EBitImplies. Expr10 ::= Expr10 "-->" Expr11 ; -- (right) +EBitOr. Expr11 ::= Expr12 "|" Expr11 ; -- (left) +EBitXOr. Expr12 ::= Expr13 "^" Expr12 ; -- (left) +EBitAnd. Expr13 ::= Expr14 "&" Expr13 ; -- (left) + +-- Comparison (associativity -) +EEq. Expr14 ::= Expr14 "==" Expr15 ; +ENeq. Expr14 ::= Expr14 "!=" Expr15 ; +ERelOp. Expr15 ::= Expr15 RelOp Expr16; -- FIXME: Chained relops allowed. + +-- Shift (left) +ELeftShift. Expr16 ::= Expr17 "<<" Expr16; +ERightShift. Expr16 ::= Expr17 ">>" Expr16; + +-- Additive (left) +EPlus. Expr17 ::= Expr18 "+" Expr17; +EMinus. Expr17 ::= Expr18 "-" Expr17; + +-- Multiplicative (left) +EMult. Expr18 ::= Expr19 "*" Expr18; +EDiv. Expr18 ::= Expr19 "/" Expr18; +EMod. Expr18 ::= Expr19 "%" Expr18; + +-- Unary (right) +EUnary. Expr19 ::= UnaryOp Expr19 ; + +-- FIXME: Test that sizeof can also take a term as argument. +ETypeCast. Expr19 ::= "(" TypeExpr ")" Expr19 ; +ESizeOfTerm. Expr19 ::= "sizeof" "(" Expr19 ")" ; +ESizeOfType. Expr19 ::= "sizeof" "(" CTypeExpr ")" ; + +-- Selection (left) +EArrayAccess. Expr20 ::= Expr20 "[" Expr19 "]" ; -- Term[Term] +EStructFieldAccess. Expr20 ::= Expr20 "." Id ; -- Term.Term +EStructPtrFieldAccess. Expr20 ::= Expr20 "->" Id ; + +EArrayFunMod. Expr21 ::= "{" Expr21 "\\with" "[" Expr22 "]" "=" Expr23 "}" ; +EFieldFunMod. Expr21 ::= "{" Expr21 "\\with" "." Id "=" Expr22 "}" ; + +EApplication. Expr22 ::= Id "(" [Expr2] ")" ; +EOld. Expr22 ::= "\\old" "(" Expr2 ")" ; +EValid. Expr22 ::= "\\valid" "(" [Location] ")" ; + +ELit. Expr23 ::= Lit ; +EIdent. Expr23 ::= Id ; +EResult. Expr23 ::= "\\result" ; + +separator nonempty Expr2 "," ; +coercions Expr 23; + +UnaryPlus. UnaryOp ::= "+" ; +UnaryMinus. UnaryOp ::= "-" ; +UnaryNegation. UnaryOp ::= "!" ; +UnaryComplementation. UnaryOp ::= "~" ; +UnaryPtrDeref. UnaryOp ::= "*" ; +UnaryAddressOf. UnaryOp ::= "&" ; + +RelOpLEQ. RelOp ::= "<=" ; +RelOpGEQ. RelOp ::= ">=" ; +RelOpGT. RelOp ::= ">" ; +RelOpLT. RelOp ::= "<" ; -- Binders (2.4) ------------------------------------------- -ABinder. Binder ::= TypeName [VariableIdent] ; +ABinder. Binder ::= TypeName [VarIdent] ; separator nonempty Binder "," ; TypeNameLogic. TypeName ::= LogicTypeName ; -TypeNameC. TypeName ::= CTypeSpecifier ; -- FIXME: Should be CTypeName +TypeNameC. TypeName ::= CTypeName ; -- NOTE: Referenced but not used in 2.4 TypeExprLogic. TypeExpr ::= LogicTypeName ; -TypeExprC. TypeExpr ::= CTypeSpecifier ; -- FIXME: Should be CTypeExpr +TypeExprC. TypeExpr ::= CTypeExpr ; LogicTypeNameBuiltIn. LogicTypeName ::= BuiltInLogicType ; -LogicTypeNameId. LogicTypeName ::= Id ; BuiltInLogicTypeBoolean. BuiltInLogicType ::= "boolean" ; BuiltInLogicTypeInteger. BuiltInLogicType ::= "integer" ; BuiltInLogicTypeReal. BuiltInLogicType ::= "real" ; -VariableIdentId. VariableIdent ::= Id ; -VariableIdentPtrDeref. VariableIdent ::= "*" VariableIdent ; -VariableIdentArray. VariableIdent ::= VariableIdent "[]"; -VariableIdentParentheses. VariableIdent ::= "(" VariableIdent ")"; +VarIdentId. VarIdent3 ::= Id ; +VarIdentArray. VarIdent2 ::= VarIdent3 "[" "]"; +VarIdentPtrDeref. VarIdent ::= "*" VarIdent2 ; -separator nonempty VariableIdent "," ; +coercions VarIdent 3 ; +separator nonempty VarIdent "," ; -- Memory Location Sets (2.8) ------------------------------ -- TODO: Missing a lot. TSetEmpty. TSet ::= "\\empty" ; -TSetTerm. TSet ::= Term ; - --- C Type Expressions (A.1) -------------------------------- --- TODO: Missing a lot. -CTypeSpecifierVoid. CTypeSpecifier ::= "void" ; -CTypeSpecifierChar. CTypeSpecifier ::= "char" ; -CTypeSpecifierShort. CTypeSpecifier ::= "short" ; -CTypeSpecifierInt. CTypeSpecifier ::= "int" ; -CTypeSpecifierLong. CTypeSpecifier ::= "long" ; -CTypeSpecifierFloat. CTypeSpecifier ::= "float" ; -CTypeSpecifierDouble. CTypeSpecifier ::= "double" ; -CTypeSpecifierSigned. CTypeSpecifier ::= "signed" ; -CTypeSpecifierUnsigned. CTypeSpecifier ::= "unsigned" ; -CTypeSpecifierStruct. CTypeSpecifier ::= "struct" Id ; -CTypeSpecifierUnion. CTypeSpecifier ::= "union" Id ; -CTypeSpecifierEnum. CTypeSpecifier ::= "enum" Id ; -CTypeSpecifierId. CTypeSpecifier ::= Id ; - +TSetTerm. TSet ::= Expr ; + +-- C types +ACTypeExpr. CTypeExpr ::= [CSpecQual] CMaybeAbsDec ; +separator nonempty CSpecQual "" ; + +NoAbsDec. CMaybeAbsDec ::= ; +SomeAbsDec. CMaybeAbsDec ::= CAbsDec ; + +ACTypeName. CTypeName ::= [CDeclSpec] ; +separator nonempty CDeclSpec "" ; + +CSpecQualTypeSpec. CSpecQual ::= CTypeSpec ; +CSpecQualTypeQual. CSpecQual ::= CTypeQual ; + +CTypeQualConst. CTypeQual ::= "const" ; +CTypeQualVolat. CTypeQual ::= "volatile" ; + +CStruct. CCollection ::= "struct" ; +CUnion. CCollection ::= "union" ; +CEnum. CCollection ::= "enum" ; + +Tvoid. CTypeSpec ::= "void"; +Tchar. CTypeSpec ::= "char"; +Tshort. CTypeSpec ::= "short"; +Tint. CTypeSpec ::= "int"; +Tlong. CTypeSpec ::= "long"; +Tfloat. CTypeSpec ::= "float"; +Tdouble. CTypeSpec ::= "double"; +Tsigned. CTypeSpec ::= "signed"; +Tunsigned. CTypeSpec ::= "unsigned"; +Tcollection. CTypeSpec ::= CCollection Id; + +PointerStart. CAbsDec ::= CPointer ; +Advanced. CAbsDec ::= CDirAbsDec ; +PointAdvanced. CAbsDec ::= CPointer CDirAbsDec ; + +ACSinglePointer. CSinglePointer ::= "*" [CTypeQual] ; +separator CTypeQual "" ; + +ACPointer. CPointer ::= [CSinglePointer] ; +separator nonempty CSinglePointer "" ; + +WithinParentes. CDirAbsDec ::= "(" CAbsDec ")" ; +Array. CDirAbsDec ::= "[" "]" ; +InitiatedArray. CDirAbsDec ::= "[" Expr "]" ; +UnInitiated. CDirAbsDec ::= CDirAbsDec "[" "]" ; +Initiated. CDirAbsDec ::= CDirAbsDec "[" Expr "]" ; +OldFunction. CDirAbsDec ::= "(" ")" ; +NewFunction. CDirAbsDec ::= "(" CParamType ")" ; +OldFuncExpr. CDirAbsDec ::= CDirAbsDec "(" ")" ; +NewFuncExpr. CDirAbsDec ::= CDirAbsDec "(" CParamType ")" ; + +AllSpec. CParamType ::= [CParamDecl] ; +separator nonempty CParamDecl "," ; + +COnlyType. CParamDecl ::= [CDeclSpec] ; +CTypeAndParam. CParamDecl ::= [CDeclSpec] CDeclarator ; +CAbstract. CParamDecl ::= [CDeclSpec] CAbsDec ; + +CType. CDeclSpec ::= CTypeSpec ; +CSpecProp. CDeclSpec ::= CTypeQual; + +BeginPointer. CDeclarator ::= CPointer CDirectDeclarator ; +NoPointer. CDeclarator ::= CDirectDeclarator ; + +Name. CDirectDeclarator ::= Id ; +ParenDecl. CDirectDeclarator ::= "(" CDeclarator ")" ; +InitArray. CDirectDeclarator ::= CDirectDeclarator "[" Expr "]" ; +Incomplete. CDirectDeclarator ::= CDirectDeclarator "[" "]" ; +MathArray. CDirectDeclarator ::= CDirectDeclarator "[" "_" "]" ; +NewFuncDec. CDirectDeclarator ::= CDirectDeclarator "(" CParamType ")" ; +OldFuncDec. CDirectDeclarator ::= CDirectDeclarator "(" ")" ; ---- Tokens ------------------------------------------------ --- Taken from concorrentC.cf -token Id (letter | '_' | '$') (letter | digit | '_' | '$')*; -token UnboundedInteger ('0' | (["123456789"] digit *)); +position token Id (letter | '_' | '$') (letter | digit | '_' | '$')*; separator Id "," ; + +token UnboundedInteger ('0' | (["123456789"] digit *)); diff --git a/regression-tests/acsl-contracts/contract11.hcc b/regression-tests/acsl-contracts/contract11.hcc index 5a410df..8626e4e 100644 --- a/regression-tests/acsl-contracts/contract11.hcc +++ b/regression-tests/acsl-contracts/contract11.hcc @@ -1,7 +1,7 @@ /*@ requires \valid(p, q); - ensures ((\result == *p) || (\result == *q)); - ensures \result >= (*p); + ensures \result == *p || \result == *q; + ensures \result >= *p; ensures \result >= (*q); */ int max(int* p, int* q) { diff --git a/regression-tests/acsl-contracts/contract13.hcc b/regression-tests/acsl-contracts/contract13.hcc index 23f9378..7f607ab 100644 --- a/regression-tests/acsl-contracts/contract13.hcc +++ b/regression-tests/acsl-contracts/contract13.hcc @@ -1,7 +1,7 @@ /*@ requires \valid(p, q); - ensures ((\result == *p) || (\result == *q)); - ensures \result >= (*p); + ensures \result == *p || \result == *q; + ensures \result >= *p; ensures \result >= (*q); */ int max(int* p, int* q) { diff --git a/regression-tests/acsl-contracts/contract14.hcc b/regression-tests/acsl-contracts/contract14.hcc index dd533c6..fd422bf 100644 --- a/regression-tests/acsl-contracts/contract14.hcc +++ b/regression-tests/acsl-contracts/contract14.hcc @@ -1,5 +1,5 @@ /*@ - ensures \forall int i; (i >= 0) ==> (i > \result); + ensures \forall int i; i >= 0 ==> i > \result; */ int getNeg() { return -1; diff --git a/regression-tests/acsl-contracts/contract2.hcc b/regression-tests/acsl-contracts/contract2.hcc index 308d0b9..f214477 100644 --- a/regression-tests/acsl-contracts/contract2.hcc +++ b/regression-tests/acsl-contracts/contract2.hcc @@ -1,6 +1,6 @@ /*@ - requires (x >= 0) && (x <= 4); - ensures (\result >= 10) && (\result <= 14); + requires x >= 0 && x <= 4; + ensures \result >= 10 && \result <= 14; */ int foo(int x) { return 12; diff --git a/regression-tests/acsl-contracts/contract27.hcc b/regression-tests/acsl-contracts/contract27.hcc index 995b419..68ca4e5 100644 --- a/regression-tests/acsl-contracts/contract27.hcc +++ b/regression-tests/acsl-contracts/contract27.hcc @@ -3,7 +3,7 @@ /*@ requires \valid(a) && \valid(b); assigns *a, *b; - ensures (*a) == \old(*b); + ensures *a == \old(*b); ensures (*b) == \old(*a); */ void swap(int* a, int* b) { diff --git a/regression-tests/acsl-standalone/maxptr_unsafe.c b/regression-tests/acsl-standalone/maxptr_unsafe.c index 72135c2..6d0f4a1 100644 --- a/regression-tests/acsl-standalone/maxptr_unsafe.c +++ b/regression-tests/acsl-standalone/maxptr_unsafe.c @@ -1,7 +1,7 @@ /*@ requires \valid(p, q); - ensures ((\result == *p) || (\result == *q)); - ensures \result >= (*p); + ensures \result == *p || \result == *q; + ensures \result >= *p; ensures \result >= (*q); */ int foo(int* p, int* q) { diff --git a/regression-tests/acsl-standalone/mc91_safe.c b/regression-tests/acsl-standalone/mc91_safe.c index 5050e9a..defac58 100644 --- a/regression-tests/acsl-standalone/mc91_safe.c +++ b/regression-tests/acsl-standalone/mc91_safe.c @@ -1,6 +1,6 @@ /*@ - ensures ((n <= 100) ==> (\result == 91)); - ensures ((n > 100) ==> (\result == (n-10))); + ensures n <= 100 ==> \result == 91; + ensures n > 100 ==> \result == n-10; */ int foo(int n) { if (n > 100) { diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs index b8f02b7..ae0b8b9 100755 --- a/regression-tests/runalldirs +++ b/regression-tests/runalldirs @@ -1,7 +1,5 @@ #!/bin/sh -set -e - ./rundir horn-hcc-heap "" -assertNoVerify -dev -t:60 ./rundir horn-hcc-array "" -assertNoVerify -dev -t:60 ./rundir horn-bv "" -assert -dev -t:60 diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 399ea3f..5e86363 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -498,8 +498,7 @@ class Main (args: Array[String]) { processor(processedSolution)() // will process all predicates } - println("\nInferred ACSL annotations") - println("="*80) + var printedACSLHeader = false // line numbers in contract vars (e.g. x/1) are due to CCVar.toString for ((fun, ctx) <- contexts if maybeEnc.isEmpty || @@ -515,6 +514,11 @@ class Main (args: Array[String]) { val fPostWithArgs = replaceArgs(fPost, ctx.postPredACSLArgNames) + if (!printedACSLHeader) { + println("\nInferred ACSL annotations") + println("=" * 80) + printedACSLHeader = true + } println("/* contracts for " + fun + " */") println("/*@") print( " requires "); println(fPreWithArgs + ";") @@ -528,6 +532,11 @@ class Main (args: Array[String]) { p._1.name.stripPrefix("inv_") == inv.pred.name).get._2 val fInvWithArgs = replaceArgs(fInv, inv.argVars.map(_.name)) + if (!printedACSLHeader) { + println("\nInferred ACSL annotations") + println("=" * 80) + printedACSLHeader = true + } println("\n/* loop invariant for the loop at line " + srcInfo.line + " */") println("/*@") @@ -535,7 +544,9 @@ class Main (args: Array[String]) { println("*/") } } - println("="*80 + "\n") + if (printedACSLHeader) { + println("=" * 80 + "\n") + } } case None => } diff --git a/src/tricera/acsl/ACSLTranslator.scala b/src/tricera/acsl/ACSLTranslator.scala index ee00e63..b0e9e82 100644 --- a/src/tricera/acsl/ACSLTranslator.scala +++ b/src/tricera/acsl/ACSLTranslator.scala @@ -33,13 +33,11 @@ package tricera.acsl import tricera.acsl.{Absyn => AST} import collection.JavaConverters._ -import ap.parser.IExpression -import ap.parser.{IBoolLit, IConstant, IFormula, IFormulaITE, IFunApp, IFunction, ISortedQuantified, ISortedVariable, ITerm} +import ap.parser._ import ap.theories.nia.GroebnerMultiplication._ import ap.types.{Sort, SortedConstantTerm} import ap.theories.Heap import tricera.Util.{SourceInfo, getSourceInfo} -import tricera.acsl.Absyn.LoopInvSimple import tricera.concurrency.ccreader._ import CCExceptions._ @@ -144,6 +142,8 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { import scala.collection.mutable.{HashMap => MHashMap} import ACSLTranslator._ + private val printer = new tricera.acsl.PrettyPrinterNonStatic + val locals = new MHashMap[String, CCTerm] var vars: Map[String, CCVar] = Map() var inPostCond = false @@ -152,14 +152,12 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { // ---- Statement annotations (e.g., assertions) ----------- def translate(assertAnnotation : AST.Assertion, - stmCtx : StatementAnnotationContext) : StatementAnnotation = { + stmCtx : StatementAnnotationContext) + : StatementAnnotation = { assertAnnotation match { - case regularAssertion : AST.RegularAssertion1 => - val f = translate(regularAssertion.predicate_) - StatementAnnotation(f, isAssert = true) - case regularAssertion: AST.RegularAssertion2 => - val f = translate(regularAssertion.predicate_) - StatementAnnotation(f, isAssert = true) + case regularAssertion : AST.RegularAssertion => + val f = translate(regularAssertion.expr_) + StatementAnnotation(f.toFormula, isAssert = true) case _ => throw new ACSLParseException("Behaviour assertions are " + "currently unsupported.") @@ -171,9 +169,9 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { stmCtx : StatementAnnotationContext) : LoopAnnotation = { loopInvariantAnnotation match { - case inv : LoopInvSimple => - val f = translate(inv.predicate_) - LoopAnnotation(f) + case inv : AST.LoopInvSimple => + val f = translate(inv.expr_) + LoopAnnotation(f.toFormula) } } @@ -192,11 +190,12 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { case _ => throw new ACSLParseException("Unsupported simple clause.") } + // TODO: do not use "and" and "toFormula" below,losing source information! // NOTE: `pre` and `post` defaults to true given usage of `and`. useOldHeap = true - val pre : IFormula = IExpression.and(rcs.map(f => translate(f))) + val pre : IFormula = IExpression.and(rcs.map(f => translate(f).toFormula)) useOldHeap = false - val post : IFormula = IExpression.and(ecs.map(f => translate(f))) + val post : IFormula = IExpression.and(ecs.map(f => translate(f).toFormula)) // FIXME: Refactor and break out in functions! val assigns : (IFormula, IFormula) = acs match { @@ -325,12 +324,12 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { val nils = (Nil : List[CCExpr], Nil : List[CCExpr]) val terms : (List[CCExpr], List[CCExpr]) = tSets.foldRight(nils) ({ case (t : AST.TSetTerm, (idents, ptrDerefs)) => - t.term_ match { - case i : AST.TermIdent => (translate(i) :: idents, ptrDerefs) - case p : AST.TermUnaryOp - if p.unaryop_.isInstanceOf[AST.UnaryOpPtrDeref] => { + t.expr_ match { + case i : AST.EIdent => (translate(i) :: idents, ptrDerefs) + case p : AST.EUnary + if p.unaryop_.isInstanceOf[AST.UnaryPtrDeref] => { useOldHeap = true - val res = (idents, translate(p.term_) :: ptrDerefs) + val res = (idents, translateTerm(p.expr_) :: ptrDerefs) useOldHeap = false res } @@ -350,132 +349,264 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { /** * Translates assigns / ensures clauses. */ - def translate(clause : AST.SimpleClause) : IFormula = clause match { + def translate(clause : AST.SimpleClause) : CCFormula = clause match { case ac : AST.SimpleClauseAssigns => throwNotImpl(ac) case ec : AST.SimpleClauseEnsures => translate(ec.ensuresclause_) } - - def translate(clause : AST.EnsuresClause) : IFormula = { + def translate(clause : AST.EnsuresClause) : CCFormula = { val funCtx = ctx.asInstanceOf[FunctionContext] inPostCond = true vars = (funCtx.getParams.map(v => (v.name, funCtx.getOldVar(v.name).get)) ++ ctx.getGlobals.map(v => (v.name, v))).toMap - val res = translate(clause.asInstanceOf[AST.AnEnsuresClause].predicate_) + val res = translatePred(clause.asInstanceOf[AST.AnEnsuresClause].expr_) inPostCond = false res } - def translate(clause : AST.RequiresClause) : IFormula = { + def translate(clause : AST.RequiresClause) : CCFormula = { val funCtx = ctx.asInstanceOf[FunctionContext] vars = (funCtx.getParams ++ ctx.getGlobals).map(v => (v.name, funCtx.getOldVar(v.name).get)).toMap - translate(clause.asInstanceOf[AST.ARequiresClause].predicate_) - } - - // ---- Predicates ----------------------------------------- - def translate(pred : AST.Predicate) : IFormula = pred match { - case p : AST.PredTrue => translate(p) - case p : AST.PredFalse => translate(p) - case p : AST.PredRelOp => translate(p) - case p : AST.PredApplication => throwNotImpl(p) // Redundant for now. - case p : AST.PredParentheses => translate(p) - case p : AST.PredConjunction => translate(p) - case p : AST.PredDisjunction => translate(p) - case p : AST.PredImplication => translate(p) - case p : AST.PredEquivalence => translate(p) - case p : AST.PredNegation => translate(p) - case p : AST.PredXOr => translate(p) - case p : AST.PredTernaryCond => throwNotImpl(p) - case p : AST.PredTernaryCond2 => translate(p) - case p : AST.PredLocalBinding => translate(p) - case p : AST.PredLocalBinding2 => throwNotImpl(p) - case p : AST.PredForAll => translate(p) - case p : AST.PredExists => translate(p) - case p : AST.PredSyntacticNaming => translate(p) - case p : AST.PredSyntacticNaming2 => translate(p) - case p : AST.PredOld => throwNotImpl(p) - case p : AST.PredValid => translate(p) - } - - def translate(pred : AST.PredTrue) : IFormula = { - IBoolLit(true) - } - - def translate(pred : AST.PredFalse) : IFormula = { - IBoolLit(false) - } - - def translate(pred : AST.PredRelOp) : IFormula = { - val left : ITerm = translate(pred.term_1).toTerm - val right : ITerm = translate(pred.term_2).toTerm - pred.relop_ match { - case op : AST.RelOpEQ => left === right - case op : AST.RelOpNEQ => left =/= right - case op : AST.RelOpLEQ => left <= right - case op : AST.RelOpGEQ => left >= right - case op : AST.RelOpGT => left > right - case op : AST.RelOpLT => left < right + translatePred(clause.asInstanceOf[AST.ARequiresClause].expr_) + } + + def translate(expr : AST.Expr) : CCExpr = expr match { + case e : AST.ENaming1 => ??? + case e : AST.ENaming2 => ??? + case _ : AST.EForAll + | _ : AST.EExists => translateQuantified(expr) + case e : AST.EBinding => ??? + case e : AST.ETernary => translateTernary(e) + case _ : AST.EEquiv + | _ : AST.EImplies + | _ : AST.EOr + | _ : AST.EXOr + | _ : AST.EAnd => translateBinaryLogicOp(expr) + case e : AST.EBitEquiv => ??? + case e : AST.EBitImplies => ??? + case e : AST.EBitOr => ??? + case e : AST.EBitXOr => ??? + case e : AST.EBitAnd => ??? + case e : AST.EEq => translateEqNeq(e) + case e : AST.ENeq => translateEqNeq(e) + case e : AST.ERelOp => translateRelOp(e) + case e : AST.ELeftShift => ??? + case e : AST.ERightShift => ??? + case _ : AST.EPlus + | _ : AST.EMinus + | _ : AST.EMult + | _ : AST.EDiv + | _ : AST.EMod => translateArith(expr) + case e : AST.EUnary => translateUnary(e) + case e : AST.ETypeCast => ??? + case e : AST.ESizeOfTerm => ??? + case e : AST.ESizeOfType => ??? + case e : AST.EArrayAccess => translateArrayAccessExpr(e) + case e : AST.EStructFieldAccess => ??? + case e : AST.EStructPtrFieldAccess => ??? + case e : AST.EArrayFunMod => ??? + case e : AST.EFieldFunMod => ??? + case e : AST.EApplication => ??? + case e : AST.EOld => translateOldExpr(e) + case e : AST.EValid => translateValidExpr(e) + case e : AST.ELit => translateLitExpr(e.lit_) + case e : AST.EIdent => translateIdentExpr(e) + case e : AST.EResult => translateResultExpr + } + + def translateLitExpr(lit : AST.Lit) : CCExpr = { + import IExpression._ + import ap.basetypes.IdealInt + val srcInfo = Some(getSourceInfo(lit)) + lit match { + case t : AST.LitTrue =>CCFormula(IBoolLit(true), CCBool, srcInfo) + case t : AST.LitFalse => CCFormula(IBoolLit(false), CCBool, srcInfo) + case t : AST.LitInt => + CCTerm(i(IdealInt(t.unboundedinteger_)), CCInt, srcInfo) + case t : AST.LitReal => ??? + case t : AST.LitString => ??? + case t : AST.LitChar => ??? } } - def translate(pred : AST.PredParentheses) : IFormula = { - translate(pred.predicate_) - } - - // NOTE: Might wanna simplify directly with e.g. &&&. - def translate(pred : AST.PredConjunction) : IFormula = { - val left : IFormula = translate(pred.predicate_1) - val right : IFormula = translate(pred.predicate_2) - left & right - } - - def translate(pred : AST.PredDisjunction) : IFormula = { - val left : IFormula = translate(pred.predicate_1) - val right : IFormula = translate(pred.predicate_2) - left | right + /** + * term x term -> predicate + * In the ACSL grammar the return type of rel ops is ambiguous: it can be + * a term or a predicate. Here we disambiguate by picking the latter. + * TODO: support chained applications + */ + def translateRelOp(relOp : AST.ERelOp) : CCFormula = { + val lhs : ITerm = translate(relOp.expr_1).toTerm + val rhs : ITerm = translate(relOp.expr_2).toTerm + val srcInfo = Some(getSourceInfo(relOp)) + CCFormula(relOp.relop_ match { + case _ : AST.RelOpLEQ => lhs <= rhs + case _ : AST.RelOpGEQ => lhs >= rhs + case _ : AST.RelOpGT => lhs > rhs + case _ : AST.RelOpLT => lhs < rhs + }, CCBool, srcInfo) } - def translate(pred : AST.PredImplication) : IFormula = { - val left : IFormula = translate(pred.predicate_1) - val right : IFormula = translate(pred.predicate_2) - left ==> right + /** + * term x term -> predicate + * In the ACSL grammar the return type of rel ops is ambiguous: it can be + * a term or a predicate. Here we disambiguate by picking the latter. + * TODO: support chained applications + */ + def translateEqNeq(expr : AST.Expr) : CCFormula = { + CCFormula( + expr match { + case eq : AST.EEq => + val lhs : ITerm = translateTerm(eq.expr_1).toTerm + val rhs : ITerm = translateTerm(eq.expr_2).toTerm + lhs === rhs + case neq : AST.ENeq => + val lhs : ITerm = translateTerm(neq.expr_1).toTerm + val rhs : ITerm = translateTerm(neq.expr_2).toTerm + lhs =/= rhs + case _ => + throw new ACSLParseException(s"Op must be '==' or '!=', got " + + s"${printer print expr}.") + }, CCBool, Some(getSourceInfo(expr))) + } + + def translateArith(expr : AST.Expr) : CCTerm = { + CCTerm( + expr match { + case eq : AST.EPlus => + val lhs : ITerm = translateTerm(eq.expr_1).toTerm + val rhs : ITerm = translateTerm(eq.expr_2).toTerm + lhs + rhs + case neq : AST.EMinus => + val lhs : ITerm = translateTerm(neq.expr_1).toTerm + val rhs : ITerm = translateTerm(neq.expr_2).toTerm + lhs - rhs + case neq : AST.EMult => + val lhs : ITerm = translateTerm(neq.expr_1).toTerm + val rhs : ITerm = translateTerm(neq.expr_2).toTerm + lhs * rhs + case neq : AST.EDiv => + val lhs : ITerm = translateTerm(neq.expr_1).toTerm + val rhs : ITerm = translateTerm(neq.expr_2).toTerm + lhs / rhs + case neq : AST.EMod => + val lhs : ITerm = translateTerm(neq.expr_1).toTerm + val rhs : ITerm = translateTerm(neq.expr_2).toTerm + lhs % rhs + case _ => + throw new ACSLParseException( + "Op is recognized, got " + (printer print expr)) + }, CCBool, Some(getSourceInfo(expr))) } - def translate(pred : AST.PredEquivalence) : IFormula = { - val left : IFormula = translate(pred.predicate_1) - val right : IFormula = translate(pred.predicate_2) - left <=> right + /** + * Helper function to translate expressions into predicates. + * Throws an error if the expression is not an actual predicate. + */ + def translatePred(expr : AST.Expr) : CCFormula = { + val t = translate(expr) + t match { + case pred : CCFormula => pred + case _ => + throw new ACSLParseException( + "Expected a predicate, but got " + (printer print expr)) + } } - def translate(pred : AST.PredNegation) : IFormula = { - val right : IFormula = translate(pred.predicate_) - !right + /** + * Helper function to translate expressions into terms. + * Throws an error if the expression is not an actual term. + */ + def translateTerm(expr : AST.Expr) : CCTerm = { + val t = translate(expr) + t match { + case term : CCTerm => term + case _ => + throw new ACSLParseException( + "Expected a term, but got " + (printer print expr)) + } } - def translate(pred : AST.PredXOr) : IFormula = { - val left : IFormula = translate(pred.predicate_1) - val right : IFormula = translate(pred.predicate_2) - left right + /** + * Translate logical operators that are only applicable to predicates. + * I.e.,: "&&" | "||" | "==>" | "<==>" | "^^" + */ + def translateBinaryLogicOp(expr : AST.Expr) : CCFormula = { + val srcInfo = Some(getSourceInfo(expr)) + expr match { + case e : AST.EEquiv => // <==> + val lhs = translatePred(e.expr_1) + val rhs = translatePred(e.expr_2) + CCFormula(lhs.toFormula <=> rhs.toFormula, CCBool, srcInfo) + case e : AST.EImplies => // ==> + val lhs = translatePred(e.expr_1) + val rhs = translatePred(e.expr_2) + CCFormula(lhs.toFormula ==> rhs.toFormula, CCBool, srcInfo) + case e : AST.EOr => // || + val lhs = translatePred(e.expr_1) + val rhs = translatePred(e.expr_2) + CCFormula(lhs.toFormula ||| rhs.toFormula, CCBool, srcInfo) + case e : AST.EXOr => // ^^ + val lhs = translatePred(e.expr_1) + val rhs = translatePred(e.expr_2) + CCFormula(lhs.toFormula rhs.toFormula, CCBool, srcInfo) + case e : AST.EAnd => // && + val lhs = translatePred(e.expr_1) + val rhs = translatePred(e.expr_2) + CCFormula(lhs.toFormula &&& rhs.toFormula, CCBool, srcInfo) + case _ => + throw new ACSLTranslateException( + "Not a logical operator: " + (printer print expr)) + } } - // How will this clash with `PredTernaryCond`? - def translate(pred : AST.PredTernaryCond2) : IFormula = { - val cond : IFormula = translate(pred.predicate_1) - val left : IFormula = translate(pred.predicate_2) - val right : IFormula = translate(pred.predicate_3) - IFormulaITE(cond, left, right) + /** + * There are three cases in the ACSL grammar: + * term ? term : term -> term + * term ? pred : pred -> pred + * pred ? pred : pred -> pred + */ + def translateTernary(expr : AST.ETernary) : CCExpr = { + val cond : CCExpr = translate(expr.expr_1) + val left : CCExpr = translate(expr.expr_2) + val right : CCExpr = translate(expr.expr_3) + val srcInfo = Some(getSourceInfo(expr)) + + (cond, left, right) match { + case (c@CCTerm(_, _, _), l@CCTerm(_,lType,_), r@CCTerm(_,rType,_)) => + if (lType != rType) { + // TODO: support implicit type casts. + throw new ParseException(s"Type mismatch in $expr: $lType vs $rType." + + "(Implicit casts are currently unsupported.)") + } + CCTerm(ITermITE(cond.toFormula, left.toTerm, right.toTerm), + lType, srcInfo) + case (c@CCTerm(_, _, _), l@CCFormula(_,_,_), r@CCFormula(_,_,_)) => + CCFormula(IFormulaITE(c.toFormula, l.toFormula, right.toFormula), + CCBool, srcInfo) + case (c@CCFormula(_, _, _), l@CCFormula(_,_,_), r@CCFormula(_,_,_)) => + CCFormula(IFormulaITE(c.toFormula, l.toFormula, right.toFormula), + CCBool, srcInfo) + case _ => + throw new ACSLParseException( + s"""Do not know how to parse ${printer print expr}. + | Ternary expression must be in one of the following forms: + | term ? term : term -> term + | term ? pred : pred -> pred + | pred ? pred : pred -> pred""".stripMargin) + } } - def translate(pred : AST.PredLocalBinding) : IFormula = { - val ident : String = pred.id_ - val boundTo : CCExpr = translate(pred.term_) - - locals.put(ident, CCTerm(boundTo.toTerm, boundTo.typ, boundTo.srcInfo)) - val inner : IFormula = translate(pred.predicate_) - locals.remove(ident) - inner - } +// def translate(pred : AST.PredLocalBinding) : IFormula = { +// val ident : String = pred.id_ +// val boundTo : CCExpr = translate(pred.term_) +// +// locals.put(ident, CCTerm(boundTo.toTerm, boundTo.typ, boundTo.srcInfo)) +// val inner : IFormula = translate(pred.predicate_) +// locals.remove(ident) +// inner +// } /* TODO: Requires all translate to just return IExpression - desired? Alternative approach could be preprocessing/replacement. @@ -489,96 +620,135 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { }*/ // TODO: Not tested. Unsure if correct. - def translate(pred : AST.PredForAll) : IFormula = { - val binders : Seq[AST.ABinder] = - pred.listbinder_.asScala.toList.map(_.asInstanceOf[AST.ABinder]) + def translateQuantified(pred : AST.Expr) : CCFormula = { + val (binders, bodyExpr, quantifier) = pred match { + case expr : AST.EForAll => + (expr.listbinder_, expr.expr_, IExpression.Quantifier.ALL) + case expr : AST.EExists => + (expr.listbinder_, expr.expr_, IExpression.Quantifier.EX) + case _ => + throw new ACSLTranslateException( + "Not a quantified expression: " + (printer print pred)) + } + val namedTerms : Seq[(String, CCTerm)] = bindersToConstants(binders) namedTerms.map(t => locals.put(t._1, t._2)) - val inner : IFormula = translate(pred.predicate_) + val inner : CCFormula = translatePred(bodyExpr) val (names, terms) : (Seq[String], Seq[CCTerm]) = namedTerms.unzip // FIXME: If v is shadowed, this will remove the shadowed term. names.map(locals.remove) // FIXME: Look over order of creation here. - // FIXME: Use IExpression.all? - terms.foldLeft(inner)((formula, term) => { + CCFormula(terms.foldLeft(inner.toFormula)((formula, term) => { val sort : Sort = term.typ.toSort - ISortedQuantified(IExpression.Quantifier.ALL, sort, formula) - }) - } - - def translate(pred: AST.PredExists): IFormula = { - val binders: Seq[AST.ABinder] = - pred.listbinder_.asScala.toList.map(_.asInstanceOf[AST.ABinder]) - val namedTerms: Seq[(String, CCTerm)] = bindersToConstants(binders) - - namedTerms.map(t => locals.put(t._1, t._2)) - val inner: IFormula = translate(pred.predicate_) - val (names, terms): (Seq[String], Seq[CCTerm]) = namedTerms.unzip - // FIXME: If v is shadowed, this will remove the shadowed term. - names.map(locals.remove) - - // FIXME: Look over order of creation here. - // FIXME: Use IExpression.all? - terms.foldLeft(inner)((formula, term) => { - val sort: Sort = term.typ.toSort - ISortedQuantified(IExpression.Quantifier.EX, sort, formula) - }) - } - - private def bindersToConstants(binders : Seq[AST.ABinder]) : Seq[(String, CCTerm)] = { - binders.flatMap(b => { - val typ : AST.CTypeSpecifier = - b.typename_.asInstanceOf[AST.TypeNameC].ctypespecifier_ - val ctyp : CCType = toCCType(typ) - val idents : Seq[AST.VariableIdent] = b.listvariableident_.asScala.toList + ISortedQuantified(quantifier, sort, formula) + }), CCBool, Some(getSourceInfo(pred))) + } + +// def translate(pred: AST.PredExists): IFormula = { +// val binders: Seq[AST.ABinder] = +// pred.listbinder_.asScala.toList.map(_.asInstanceOf[AST.ABinder]) +// val namedTerms: Seq[(String, CCTerm)] = bindersToConstants(binders) +// +// namedTerms.map(t => locals.put(t._1, t._2)) +// val inner: IFormula = translate(pred.predicate_) +// val (names, terms): (Seq[String], Seq[CCTerm]) = namedTerms.unzip +// // FIXME: If v is shadowed, this will remove the shadowed term. +// names.map(locals.remove) +// +// // FIXME: Look over order of creation here. +// // FIXME: Use IExpression.all? +// terms.foldLeft(inner)((formula, term) => { +// val sort: Sort = term.typ.toSort +// ISortedQuantified(IExpression.Quantifier.EX, sort, formula) +// }) +// } + + private def bindersToConstants(binders : AST.ListBinder) : Seq[(String, CCTerm)] = { + binders.asScala.toList.map(_.asInstanceOf[AST.ABinder]).flatMap(b => { + val ctyp : CCType = getType(b.typename_) + val idents : Seq[AST.VarIdent] = b.listvarident_.asScala.toList idents.map { - case v: AST.VariableIdentId => + case v: AST.VarIdentId => (v.id_, CCTerm(ISortedVariable(0, ctyp.toSort), ctyp, None)) // todo: line no? - case v: AST.VariableIdentPtrDeref => throwNotImpl(v) - case v: AST.VariableIdentArray => throwNotImpl(v) - case v: AST.VariableIdentParentheses => throwNotImpl(v) + case v: AST.VarIdentPtrDeref => throwNotImpl(v) + case v: AST.VarIdentArray => throwNotImpl(v) } }) } - private def toCCType(typ : AST.CTypeSpecifier) : CCType = typ match { - case t : AST.CTypeSpecifierVoid => throwNotImpl(t) - case t : AST.CTypeSpecifierChar => throwNotImpl(t) - case t : AST.CTypeSpecifierShort => throwNotImpl(t) - case t : AST.CTypeSpecifierInt => CCInt - case t : AST.CTypeSpecifierLong => throwNotImpl(t) - case t : AST.CTypeSpecifierFloat => throwNotImpl(t) - case t : AST.CTypeSpecifierDouble => throwNotImpl(t) - case t : AST.CTypeSpecifierSigned => throwNotImpl(t) - case t : AST.CTypeSpecifierUnsigned => throwNotImpl(t) - case t : AST.CTypeSpecifierStruct => throwNotImpl(t) - case t : AST.CTypeSpecifierUnion => throwNotImpl(t) - case t : AST.CTypeSpecifierEnum => throwNotImpl(t) - case t : AST.CTypeSpecifierId => throwNotImpl(t) + private def getType(typ : AST.TypeName) : CCType = typ match { + case typ : AST.TypeNameLogic => getType(typ.logictypename_) + case typ : AST.TypeNameC => getType(typ.ctypename_) + } + + private def getType(typ : AST.LogicTypeName) : CCType = typ + .asInstanceOf[AST.LogicTypeNameBuiltIn].builtinlogictype_ match { + case _ : AST.BuiltInLogicTypeBoolean => CCBool + case _ : AST.BuiltInLogicTypeInteger => CCMathInt + case _ : AST.BuiltInLogicTypeReal => throwNotImpl("real") + } + + private def getType(typ : AST.CTypeName) : CCType = { + val declSpecs = typ.asInstanceOf[AST.ACTypeName].listcdeclspec_.asScala.toList + getType(for (specifier <- declSpecs.iterator; + if (specifier.isInstanceOf[AST.CType])) + yield specifier.asInstanceOf[AST.CType].ctypespec_) + } + + private def getType(specs : Iterator[AST.CTypeSpec]) : CCType = { + // by default assume that the type is int + var typ : CCType = CCInt + + for (specifier <- specs) + specifier match { + case _ : AST.Tvoid => typ = CCVoid + case _ : AST.Tint =>// ignore + case _ : AST.Tchar =>// ignore + case _ : AST.Tsigned => typ = CCInt + case _ : AST.Tunsigned => typ = CCUInt + case _ : AST.Tlong if typ == CCInt => typ = CCLong + case _ : AST.Tlong if typ == CCUInt => typ = CCULong + case _ : AST.Tlong if typ == CCLong => typ = CCLongLong + case _ : AST.Tlong if typ == CCULong => typ = CCULongLong + case e : AST.Tcollection => + throw new ACSLParseException(s"type ${printer print e} is currently" + + "not supported in ACSL contracts.") +// val structName = getStructName(structOrUnion) +// typ = structDefs get structName match { +// case None => throw new TranslationException( +// "struct " + structName + " not found!") +// case Some(structType) => structType +// } +// case enum : AST.Tenum => +// typ = getEnumType(enum) + case x => throw new ACSLParseException( + s"type ${printer print x} not supported.") + } + typ } // `INamedPart` relevant? - def translate(pred : AST.PredSyntacticNaming) : IFormula = { - translate(pred.predicate_) - } +// def translate(pred : AST.PredSyntacticNaming) : IFormula = { +// translate(pred.predicate_) +// } - def translate(pred : AST.PredSyntacticNaming2) : IFormula = { - translate(pred.predicate_) - } +// def translate(pred : AST.PredSyntacticNaming2) : IFormula = { +// translate(pred.predicate_) +// } // todo: this probably should work for statement annotations too - def translate(pred : AST.PredValid) : IFormula = { + def translateValidExpr(expr : AST.EValid) : CCFormula = { val tSets : List[AST.TSet] = - pred.listlocation_.asScala.toList.map(_.asInstanceOf[AST.ALocation].tset_) + expr.listlocation_.asScala.toList.map(_.asInstanceOf[AST.ALocation].tset_) val terms : List[CCExpr] = tSets.collect({ - case t : AST.TSetTerm => translate(t.term_) + case t : AST.TSetTerm => translateTerm(t.expr_) case t => throwNotImpl(t) }) // FIXME: Typecheck terms? - terms.foldLeft(IBoolLit(true) : IFormula)((formula, term) => + val res = terms.foldLeft(IBoolLit(true) : IFormula)((formula, term) => term.typ match { // FIXME: Handle CCPointer in general? (Need access to field `typ`) case p : CCHeapPointer => @@ -591,40 +761,14 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { ctx.getHeap.heapADTs.hasCtor(readObj, ctx.getCtor(sort)) formula &&& valid & corrSort case t => - throw new ACSLParseException(s"$t in \\valid not a heap pointer.") + throw new ACSLParseException( + s"$t in \\valid not a heap pointer.") } ) + CCFormula(res, CCBool, Some(getSourceInfo(expr))) } - // ---- Terms ---------------------------------------------- - def translate(term : AST.Term) : CCExpr = term match { - case t : AST.TermLiteral => translate(t) - case t : AST.TermIdent => translate(t) - case t : AST.TermUnaryOp => translate(t) - case t : AST.TermBinOp => translate(t) - case t : AST.TermArrayAccess => translate(t) - case t : AST.TermArrayFunctionalModifier => throwNotImpl(t) - case t : AST.TermStructFieldAccess => throwNotImpl(t) - case t : AST.TermFieldFunctionalModifier => throwNotImpl(t) - case t : AST.TermStructPtrFieldAccess => throwNotImpl(t) - case t : AST.TermTypeCast => throwNotImpl(t) - case t : AST.TermFuncAppl => throwNotImpl(t) - case t : AST.TermParentheses => translate(t) - case t : AST.TermTernaryCond => throwNotImpl(t) - case t : AST.TermLocalBinding => throwNotImpl(t) - case t : AST.TermSizeOfTerm => throwNotImpl(t) - case t : AST.TermSizeOfType => throwNotImpl(t) - case t : AST.TermSyntacticNaming => throwNotImpl(t) - case t : AST.TermSyntacticNaming2 => throwNotImpl(t) - case t : AST.TermOld => translate(t) - case t : AST.TermResult => translate(t) - } - - def translate(term : AST.TermLiteral) : CCTerm = { - translate(term.literal_) - } - - def translate(t : AST.TermIdent) : CCTerm = { + def translateIdentExpr(t : AST.EIdent) : CCTerm = { val ident = t.id_ // TODO: Lookup if var exists as as local binding. // FIXME: Order of lookups (priority)? @@ -649,91 +793,51 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { } } - def translate(term : AST.TermUnaryOp) : CCExpr = { - val right : CCExpr = translate(term.term_) + def translateUnary(expr : AST.EUnary) : CCExpr = { // FIXME: Probably needs type conversions. - term.unaryop_ match { - case op : AST.UnaryOpPlus => throwNotImpl(op) - case op : AST.UnaryOpMinus => - CCTerm(right.toTerm.unary_-, right.typ, right.srcInfo) - case op : AST.UnaryOpNegation => - CCTerm(right.toTerm.unary_-, right.typ, right.srcInfo) - case op : AST.UnaryOpComplementation => throwNotImpl(op) - case op : AST.UnaryOpPtrDeref => - right.typ match { + val srcInfo = Some(getSourceInfo(expr)) + expr.unaryop_ match { + case _ : AST.UnaryPlus => + translateTerm(expr.expr_) + case _ : AST.UnaryMinus => + val t = translateTerm(expr.expr_) + CCTerm(- t.toTerm, t.typ, t.srcInfo) + case _ : AST.UnaryNegation => + translate(expr.expr_) match { + case term : CCTerm => + CCTerm(- term.toTerm, term.typ, term.srcInfo) + case pred : CCFormula => + CCFormula(!pred.toFormula, pred.typ, pred.srcInfo) + } + case op : AST.UnaryComplementation => throwNotImpl(op) + case _ : AST.UnaryPtrDeref => + val t = translateTerm(expr.expr_) + t.typ match { case p : CCHeapPointer => import ap.parser.IExpression.toFunApplier val heap : ITerm = if (useOldHeap) ctx.getOldHeapTerm else ctx.getHeapTerm - val readObj : IFunApp = ctx.getHeap.read(heap, right.toTerm) + val readObj : IFunApp = ctx.getHeap.read(heap, t.toTerm) val getObj : IFunction = ctx.sortGetter(p.typ.toSort).getOrElse( throw new ACSLParseException( s"Cannot dereference pointer of type ${p.typ}." ) ) - CCTerm(getObj(readObj), p.typ, right.srcInfo) - // FIXME: Handle stackptr - case p => throwNotImpl(p) + CCTerm(getObj(readObj), p.typ, t.srcInfo) + case p => throwNotImpl(p) // FIXME: Handle stackptr } - case op : AST.UnaryOpAddressOf => throwNotImpl(op) + case op : AST.UnaryAddressOf => throwNotImpl(op) //IFunApp(ctx.getHeap.nthAddr, Seq(ctx.getHeapTerm, right)) } } - def translate(term : AST.TermBinOp) : CCExpr = { - val left : CCExpr = translate(term.term_1) - val right : CCExpr = translate(term.term_2) - // FIXME: Type promotion? - //assert(left.typ == right.typ) - val typ : CCType = left.typ - val srcInfo = left.srcInfo - term.binop_ match { - case op : AST.BinOpPlus => - CCTerm(left.toTerm + right.toTerm, typ, srcInfo) - case op : AST.BinOpMinus => - CCTerm(left.toTerm - right.toTerm, typ, srcInfo) - case op : AST.BinOpMult => - CCTerm(mult(left.toTerm, right.toTerm), typ, srcInfo) - case op : AST.BinOpDiv => - CCTerm(tDiv(left.toTerm, right.toTerm), typ, srcInfo) - case op : AST.BinOpMod => - CCTerm(tMod(left.toTerm, right.toTerm), typ, srcInfo) - case _ : AST.BinOpEQ => - CCFormula(left.toTerm === right.toTerm, typ, srcInfo) - case _ : AST.BinOpNEQ => - CCFormula(left.toTerm =/= right.toTerm, typ, srcInfo) - case _ : AST.BinOpLEQ => // todo: this mixes and matches terms and formulas right now! needs parentheses everywhere to work correctly - CCFormula(left.toTerm <= right.toTerm, typ, srcInfo) - case _ : AST.BinOpGEQ => - CCFormula(left.toTerm >= right.toTerm, typ, srcInfo) - case op : AST.BinOpGT => - CCFormula(left.toTerm > right.toTerm, typ, srcInfo) - case op : AST.BinOpLT => - CCFormula(left.toTerm < right.toTerm, typ, srcInfo) - case op : AST.BinOpAnd => - CCFormula(left.toFormula &&& right.toFormula, typ, srcInfo) - case op : AST.BinOpOr => - CCFormula(left.toFormula ||| right.toFormula, typ, srcInfo) - case op : AST.BinOpXOr => - CCFormula((left.toFormula &&& !right.toFormula) ||| - (!left.toFormula &&& right.toFormula), typ, srcInfo) - case op : AST.BinOpLShift => throwNotImpl(op) - case op : AST.BinOpRShift => throwNotImpl(op) - case op : AST.BinOpBitwiseAnd => throwNotImpl(op) - case op : AST.BinOpBitwiseOr => throwNotImpl(op) - case op : AST.BinOpBitwiseImpl => throwNotImpl(op) - case op : AST.BinOpBitwiseEquiv => throwNotImpl(op) - case op : AST.BinOpBitwiseXOr => throwNotImpl(op) - } - } - // todo: move heap getters to Context from FunctionContext, these should be usable from statement annoations too // otherwise we cannot use array accesses inside assertions. - def translate(term : AST.TermArrayAccess) : CCExpr = { + def translateArrayAccessExpr(term : AST.EArrayAccess) : CCTerm = { import ap.parser.IExpression.toFunApplier - // TODO: Unsure if working. - val array : CCExpr = translate(term.term_1) - val index : CCExpr = translate(term.term_2) + // TODO: Untested + val array = translateTerm(term.expr_1) + val index = translateTerm(term.expr_2) array.typ match { case p : CCHeapPointer => val heap: ITerm = if (useOldHeap) ctx.getOldHeapTerm else ctx.getHeapTerm @@ -763,23 +867,19 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { } } - def translate(term : AST.TermParentheses) : CCExpr = { - translate(term.term_) - } - - def translate(term : AST.TermOld) : CCExpr = { + def translateOldExpr(expr : AST.EOld) : CCTerm = { val old = vars val funCtx = ctx.asInstanceOf[FunctionContext] vars = (funCtx.getParams.map(v => (v.name, funCtx.getOldVar(v.name).get)) ++ funCtx.getGlobals.map(v => (v.name, funCtx.getOldVar(v.name).get))).toMap useOldHeap = true - val res = translate(term.term_) + val res = translateTerm(expr.expr_) useOldHeap = false vars = old res } - def translate(term : AST.TermResult) : CCExpr = { + def translateResultExpr : CCTerm = { val funCtx = ctx.asInstanceOf[FunctionContext] if (!inPostCond) { throw new ACSLParseException("\\result has no meaning.") @@ -791,21 +891,7 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { ) } - // ---- Literals ------------------------------------------- - def translate(literal : AST.Literal) : CCTerm = literal match { - // Do we want to use CCTypes here or what? - case l : AST.LiteralTrue => throwNotImpl(l) // IBoolLit(true) - case l : AST.LiteralFalse => throwNotImpl(l) // IBoolLit(false) - case l : AST.LiteralInt => - import ap.basetypes.IdealInt - val term : ITerm = IExpression.i(IdealInt(l.unboundedinteger_)) - CCTerm(term, CCInt, None) // todo; line no? - case l : AST.LiteralReal => throwNotImpl(l) - case l : AST.LiteralString => throwNotImpl(l) // ap.theories.string.StringTheory? - case l : AST.LiteralChar => throwNotImpl(l) - } - private def throwNotImpl[T](obj : T) = { - throw new NotImplementedError(s"Support missing for ${obj.getClass}.") + throw new NotImplementedError(s"ACSL support missing for ${obj.getClass}.") } } diff --git a/src/tricera/acsl/FunctionContract.scala b/src/tricera/acsl/FunctionContract.scala index 75b851c..567524f 100644 --- a/src/tricera/acsl/FunctionContract.scala +++ b/src/tricera/acsl/FunctionContract.scala @@ -44,12 +44,12 @@ class FunctionContract( val srcInfo : SourceInfo, val postSrcInfo : SourceInfo) extends ParsedAnnotation { override def toString : String = { - s"Pre: $pre\n" + - s"Post: $post\n" + - s"Assigns (in asserts): $assignsAssert\n" + - s"Assigns (in assumes): $assignsAssume" + s"""|requires ${ap.SimpleAPI.pp(pre)} + |ensures ${ap.SimpleAPI.pp(post)} + |assigns (in asserts) ${ap.SimpleAPI.pp(assignsAssert)} + |assigns (in assumes) ${ap.SimpleAPI.pp(assignsAssume)} + |""".stripMargin } - } case class StatementAnnotation(f : IFormula, diff --git a/src/tricera/concurrency/ccreader/CCExpr.scala b/src/tricera/concurrency/ccreader/CCExpr.scala index 76d81fa..5031b3f 100644 --- a/src/tricera/concurrency/ccreader/CCExpr.scala +++ b/src/tricera/concurrency/ccreader/CCExpr.scala @@ -92,6 +92,7 @@ case class CCTerm(t: ITerm, _typ: CCType, _srcInfo: Option[SourceInfo]) .asInstanceOf[CCHeapPointer] .heap .nullAddr()) + case t if _typ == CCBool => t === ap.theories.ADT.BoolADT.True case t => !IExpression.eqZero(t) } def occurringConstants: Seq[IExpression.ConstantTerm] = diff --git a/src/tricera/concurrency/ccreader/CCType.scala b/src/tricera/concurrency/ccreader/CCType.scala index 955f5a8..d857e0b 100644 --- a/src/tricera/concurrency/ccreader/CCType.scala +++ b/src/tricera/concurrency/ccreader/CCType.scala @@ -51,6 +51,8 @@ abstract sealed class CCType { def toSort: Sort = tricera.params.TriCeraParameters.get.arithMode match { case ArithmeticMode.Mathematical => this match { + case CCBool => Sort.Bool + case CCMathInt => Sort.Integer case typ: CCArithType if typ.isUnsigned => Sort.Nat case CCDuration => Sort.Nat case CCHeap(heap) => heap.HeapSort @@ -65,7 +67,9 @@ abstract sealed class CCType { } case ArithmeticMode.ILP32 => this match { + case CCBool => Sort.Bool case CCInt => SignedBVSort(32) + case CCMathInt => Sort.Integer case CCUInt => UnsignedBVSort(32) case CCLong => SignedBVSort(32) case CCULong => UnsignedBVSort(32) @@ -84,7 +88,9 @@ abstract sealed class CCType { } case ArithmeticMode.LP64 => this match { + case CCBool => Sort.Bool case CCInt => SignedBVSort(32) + case CCMathInt => Sort.Integer case CCUInt => UnsignedBVSort(32) case CCLong => SignedBVSort(64) case CCULong => UnsignedBVSort(64) @@ -103,7 +109,9 @@ abstract sealed class CCType { } case ArithmeticMode.LLP64 => this match { + case CCBool => Sort.Bool case CCInt => SignedBVSort(32) + case CCMathInt => Sort.Integer case CCUInt => UnsignedBVSort(32) case CCLong => SignedBVSort(32) case CCULong => UnsignedBVSort(32) @@ -195,6 +203,12 @@ case object CCVoid extends CCType { def shortName = "void" } +// Logical type - only to be used in ghost code & annotations +case object CCBool extends CCType { + override def toString: String = "boolean" + def shortName = "boolean" +} + case object CCInt extends CCArithType { override def toString: String = "int" def shortName = "int" @@ -202,6 +216,12 @@ case object CCInt extends CCArithType { val isUnsigned: Boolean = false } +// Logical type - only to be used in ghost code & annotations +case object CCMathInt extends CCType { + override def toString: String = "integer" + def shortName = "integer" +} + case object CCUInt extends CCArithType { override def toString: String = "unsigned int" def shortName = "uint"