( ";"
{ Spec }
| { Spec }
ImplBody
(.
// here we attach kv only to the Procedure, not its implementation
impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
.)
)
(. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
.
Implementation
= (. IToken! x;
TypeVariableSeq! typeParams;
VariableSeq! ins, outs;
VariableSeq! locals;
StmtList! stmtList;
QKeyValue kv;
.)
"implementation"
ProcSignature
ImplBody
(. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .)
.
ProcSignature
= (. IToken! typeParamTok; typeParams = new TypeVariableSeq();
outs = new VariableSeq(); kv = null; .)
{ Attribute[ }
Ident
[ TypeParams ]
ProcFormals
[ "returns" ProcFormals ]
.
Spec
= (. TokenSeq! ms; .)
( "modifies"
[ Idents (. foreach (IToken! m in ms) {
mods.Add(new IdentifierExpr(m, m.val));
}
.)
] ";"
| "free" SpecPrePost
| SpecPrePost
)
.
SpecPrePost
= (. Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; .)
( "requires" (. tok = t; .)
{ Attribute][ }
Proposition ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .)
| "ensures" (. tok = t; .)
{ Attribute][ }
Proposition ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .)
)
.
/*------------------------------------------------------------------------*/
ImplBody
= (. locals = new VariableSeq(); .)
"{"
{ LocalVars }
StmtList
.
/* the StmtList also reads the final curly brace */
StmtList
= (. List bigblocks = new List();
/* built-up state for the current BigBlock: */
IToken startToken = null; string currentLabel = null;
CmdSeq cs = null; /* invariant: startToken != null ==> cs != null */
/* temporary variables: */
IToken label; Cmd c; BigBlock b;
StructuredCmd ec = null; StructuredCmd! ecn;
TransferCmd tc = null; TransferCmd! tcn;
.)
{
( LabelOrCmd
(. if (c != null) {
// LabelOrCmd read a Cmd
assert label == null;
if (startToken == null) { startToken = c.tok; cs = new CmdSeq(); }
assert cs != null;
cs.Add(c);
} else {
// LabelOrCmd read a label
assert label != null;
if (startToken != null) {
assert cs != null;
// dump the built-up state into a BigBlock
b = new BigBlock(startToken, currentLabel, cs, null, null);
bigblocks.Add(b);
cs = null;
}
startToken = label;
currentLabel = label.val;
cs = new CmdSeq();
}
.)
| StructuredCmd
(. ec = ecn;
if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); }
assert cs != null;
b = new BigBlock(startToken, currentLabel, cs, ec, null);
bigblocks.Add(b);
startToken = null; currentLabel = null; cs = null;
.)
| TransferCmd
(. tc = tcn;
if (startToken == null) { startToken = tc.tok; cs = new CmdSeq(); }
assert cs != null;
b = new BigBlock(startToken, currentLabel, cs, null, tc);
bigblocks.Add(b);
startToken = null; currentLabel = null; cs = null;
.)
)
}
"}"
(. IToken! endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
startToken = t; cs = new CmdSeq();
}
if (startToken != null) {
assert cs != null;
b = new BigBlock(startToken, currentLabel, cs, null, null);
bigblocks.Add(b);
}
stmtList = new StmtList(bigblocks, endCurly);
.)
.
TransferCmd
= (. tc = dummyTransferCmd;
Token y; TokenSeq! xs;
StringSeq ss = new StringSeq();
.)
( "goto" (. y = t; .)
Idents (. foreach (IToken! s in xs) { ss.Add(s.val); }
tc = new GotoCmd(y, ss);
.)
| "return" (. tc = new ReturnCmd(t); .)
) ";"
.
StructuredCmd
= (. ec = dummyStructuredCmd; assume ec.IsPeerConsistent;
IfCmd! ifcmd; WhileCmd! wcmd; BreakCmd! bcmd;
.)
( IfCmd (. ec = ifcmd; .)
| WhileCmd (. ec = wcmd; .)
| BreakCmd (. ec = bcmd; .)
)
.
IfCmd
= (. IToken! x;
Expr guard;
StmtList! thn;
IfCmd! elseIf; IfCmd elseIfOption = null;
StmtList! els; StmtList elseOption = null;
.)
"if" (. x = t; .)
Guard
"{" StmtList
[ "else"
( IfCmd (. elseIfOption = elseIf; .)
| "{"
StmtList (. elseOption = els; .)
)
]
(. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .)
.
WhileCmd
= (. IToken! x; Token z;
Expr guard; Expr! e; bool isFree;
List invariants = new List();
StmtList! body;
.)
"while" (. x = t; .)
Guard (. assume guard == null || Owner.None(guard); .)
{ (. isFree = false; z = la/*lookahead token*/; .)
[ "free" (. isFree = true; .)
]
"invariant"
Expression (. if (isFree) {
invariants.Add(new AssumeCmd(z, e));
} else {
invariants.Add(new AssertCmd(z, e));
}
.)
";"
}
"{"
StmtList (. wcmd = new WhileCmd(x, guard, invariants, body); .)
.
Guard
= (. Expr! ee; e = null; .)
"("
( "*" (. e = null; .)
| Expression (. e = ee; .)
)
")"
.
BreakCmd
= (. IToken! x; IToken! y;
string breakLabel = null;
.)
"break" (. x = t; .)
[ Ident (. breakLabel = y.val; .)
] ";" (. bcmd = new BreakCmd(x, breakLabel); .)
.
/*------------------------------------------------------------------------*/
LabelOrCmd
/* ensures (c == null) != (label != null) */
= (. IToken! x; Expr! e;
TokenSeq! xs;
IdentifierExprSeq ids;
c = dummyCmd; label = null;
Cmd! cn;
QKeyValue kv = null;
.)
( LabelOrAssign
| "assert" (. x = t; .)
{ Attribute][ }
Proposition (. c = new AssertCmd(x,e, kv); .)
";"
| "assume" (. x = t; .)
Proposition (. c = new AssumeCmd(x,e); .)
";"
| "havoc" (. x = t; .)
Idents ";" (. ids = new IdentifierExprSeq();
foreach (IToken! y in xs) {
ids.Add(new IdentifierExpr(y, y.val));
}
c = new HavocCmd(x,ids);
.)
| CallCmd ";" (. c = cn; .)
)
.
/*------------------------------------------------------------------------*/
LabelOrAssign
/* ensures (c == null) != (label != null) */
= (. IToken! id; IToken! x, y; Expr! e, e0;
c = dummyCmd; label = null;
AssignLhs! lhs;
List! lhss;
List! rhss;
List! indexes;
.)
Ident (. x = t; .)
( ":" (. c = null; label = x; .)
| (. lhss = new List(); .)
(. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
{ MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
(. lhss.Add(lhs); .)
{ ","
Ident
(. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
{ MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
(. lhss.Add(lhs); .)
}
":=" (. x = t; /* use location of := */ .)
Expression (. rhss = new List ();
rhss.Add(e0); .)
{ ","
Expression (. rhss.Add(e0); .)
}
";" (. c = new AssignCmd(x, lhss, rhss); .)
)
.
MapAssignIndex<.out IToken! x, out List! indexes.>
= (. indexes = new List ();
Expr! e;
.)
"[" (. x = t; .)
[
Expression (. indexes.Add(e); .)
{ ","
Expression (. indexes.Add(e); .)
}
]
"]"
.
/*------------------------------------------------------------------------*/
CallCmd
= (. IToken! x; IToken! first; IToken p;
List! ids = new List();
List! es = new List();
QKeyValue kv = null;
Expr en; List args;
c = dummyCmd;
.)
"call" (. x = t; .)
{ Attribute][ }
( Ident
( "("
[ CallForallArg (. es.Add(en); .)
{ "," CallForallArg (. es.Add(en); .)
}
]
")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
|
(. ids.Add(new IdentifierExpr(first, first.val)); .)
[ "," CallOutIdent (.
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
.)
{ "," CallOutIdent (.
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
.)
}
] ":="
Ident "("
[ CallForallArg (. es.Add(en); .)
{ "," CallForallArg (. es.Add(en); .)
}
]
")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
)
| "forall"
Ident "(" (. args = new List(); .)
[ CallForallArg (. args.Add(en); .)
{ "," CallForallArg (. args.Add(en); .)
}
]
")" (. c = new CallForallCmd(x, first.val, args, kv); .)
| "*"
(. ids.Add(null); .)
[ "," CallOutIdent (.
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
.)
{ "," CallOutIdent (.
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
.)
}
] ":="
Ident "("
[ CallForallArg (. es.Add(en); .)
{ "," CallForallArg (. es.Add(en); .)
}
]
")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
)
.
CallOutIdent
= (. id = null;
IToken! p;
.)
( "*"
| Ident (. id = p; .)
)
.
CallForallArg
= (. exprOptional = null;
Expr! e;
.)
( "*"
| Expression (. exprOptional = e; .)
)
.
/*------------------------------------------------------------------------*/
Proposition
=
Expression
.
/*------------------------------------------------------------------------*/
Idents
= (. IToken! id; xs = new TokenSeq(); .)
Ident (. xs.Add(id); .)
{ "," Ident (. xs.Add(id); .)
}
.
/*------------------------------------------------------------------------*/
WhiteSpaceIdents
= (. IToken! id; xs = new TokenSeq(); .)
Ident (. xs.Add(id); .)
{ Ident (. xs.Add(id); .)
}
.
/*------------------------------------------------------------------------*/
Expressions
= (. Expr! e; es = new ExprSeq(); .)
Expression (. es.Add(e); .)
{ "," Expression (. es.Add(e); .)
}
.
/*------------------------------------------------------------------------*/
Expression
= (. IToken! x; Expr! e1; .)
ImpliesExpression
{ EquivOp (. x = t; .)
ImpliesExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .)
}
.
EquivOp = "<==>" | '\u21d4'.
/*------------------------------------------------------------------------*/
ImpliesExpression
= (. IToken! x; Expr! e1; .)
LogicalExpression
[
ImpliesOp (. x = t; .)
/* recurse because implication is right-associative */
ImpliesExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .)
|
ExpliesOp (. if (noExplies)
this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
x = t; .)
LogicalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
/* loop because explies is left-associative */
{
ExpliesOp (. x = t; .)
LogicalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
}
]
.
ImpliesOp = "==>" | '\u21d2'.
ExpliesOp = "<==" | '\u21d0'.
/*------------------------------------------------------------------------*/
LogicalExpression
= (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .)
RelationalExpression
[ AndOp (. x = t; .)
RelationalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
{ AndOp (. x = t; .)
RelationalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
}
| OrOp (. x = t; .)
RelationalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
{ OrOp (. x = t; .)
RelationalExpression
(. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
}
]
.
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
/*------------------------------------------------------------------------*/
RelationalExpression
= (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .)
BvTerm
[ RelOp
BvTerm (. e0 = Expr.Binary(x, op, e0, e1); .)
]
.
RelOp
= (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
( "==" (. x = t; op=BinaryOperator.Opcode.Eq; .)
| "<" (. x = t; op=BinaryOperator.Opcode.Lt; .)
| ">" (. x = t; op=BinaryOperator.Opcode.Gt; .)
| "<=" (. x = t; op=BinaryOperator.Opcode.Le; .)
| ">=" (. x = t; op=BinaryOperator.Opcode.Ge; .)
| "!=" (. x = t; op=BinaryOperator.Opcode.Neq; .)
| "<:" (. x = t; op=BinaryOperator.Opcode.Subtype; .)
| '\u2260' (. x = t; op=BinaryOperator.Opcode.Neq; .)
| '\u2264' (. x = t; op=BinaryOperator.Opcode.Le; .)
| '\u2265' (. x = t; op=BinaryOperator.Opcode.Ge; .)
)
.
/*------------------------------------------------------------------------*/
BvTerm
= (. IToken! x; Expr! e1; .)
Term
{ "++" (. x = t; .)
Term (. e0 = new BvConcatExpr(x, e0, e1); .)
}
.
/*------------------------------------------------------------------------*/
Term
= (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .)
Factor
{ AddOp
Factor (. e0 = Expr.Binary(x, op, e0, e1); .)
}
.
AddOp
= (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
( "+" (. x = t; op=BinaryOperator.Opcode.Add; .)
| "-" (. x = t; op=BinaryOperator.Opcode.Sub; .)
)
.
/*------------------------------------------------------------------------*/
Factor
= (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .)
UnaryExpression
{ MulOp
UnaryExpression (. e0 = Expr.Binary(x, op, e0, e1); .)
}
.
MulOp
= (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
| "/" (. x = t; op=BinaryOperator.Opcode.Div; .)
| "%" (. x = t; op=BinaryOperator.Opcode.Mod; .)
)
.
/*------------------------------------------------------------------------*/
UnaryExpression
= (. IToken! x;
e = dummyExpr;
.)
( "-" (. x = t; .)
UnaryExpression (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); .)
| NegOp (. x = t; .)
UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)
| CoercionExpression
)
.
NegOp = "!" | '\u00ac'.
/*------------------------------------------------------------------------*/
/* This production creates ambiguities, because types can start with "<"
(polymorphic map types), but can also be followed by "<" (inequalities).
Coco deals with these ambiguities in a reasonable way by preferring to read
further types (type arguments) over relational symbols. E.g., "5 : C < 0"
will cause a parse error because "<" is treated as the beginning of a
map type. */
CoercionExpression
= (. IToken! x;
Type! coercedTo;
BigNum bn;
.)
ArrayExpression
{ ":" (. x = t; .)
(
Type (. e = Expr.CoerceType(x, e, coercedTo); .)
|
Nat /* This means that we really look at a bitvector
expression t[a:b] */
(. if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
this.SemErr("arguments of extract need to be integer literals");
e = new BvBounds(x, bn, BigNum.ZERO);
} else {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
.)
)
}
.
/*------------------------------------------------------------------------*/
ArrayExpression
= (. IToken! x;
Expr! index0 = dummyExpr; Expr! e1;
bool store; bool bvExtract;
ExprSeq! allArgs = dummyExprSeq;
.)
AtomExpression
{ "[" (. x = t; allArgs = new ExprSeq ();
allArgs.Add(e);
store = false; bvExtract = false; .)
[
Expression
(. if (index0 is BvBounds)
bvExtract = true;
else
allArgs.Add(index0);
.)
{ "," Expression
(. if (bvExtract || e1 is BvBounds)
this.SemErr("bitvectors only have one dimension");
allArgs.Add(e1);
.)
}
[ ":=" Expression
(. if (bvExtract || e1 is BvBounds)
this.SemErr("assignment to bitvectors is not possible");
allArgs.Add(e1); store = true;
.)
]
| ":=" Expression (. allArgs.Add(e1); store = true; .)
]
"]"
(. if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
else if (bvExtract)
e = new BvExtractExpr(x, e,
((BvBounds)index0).Upper.ToIntSafe,
((BvBounds)index0).Lower.ToIntSafe);
else
e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
.)
}
.
/*------------------------------------------------------------------------*/
AtomExpression
= (. IToken! x; int n; BigNum bn;
ExprSeq! es; VariableSeq! ds; Trigger trig;
TypeVariableSeq! typeParams;
IdentifierExpr! id;
Bpl.Type! ty;
QKeyValue kv;
e = dummyExpr;
VariableSeq! locals;
List! blocks;
.)
( "false" (. e = new LiteralExpr(t, false); .)
| "true" (. e = new LiteralExpr(t, true); .)
| Nat (. e = new LiteralExpr(t, bn); .)
| BvLit (. e = new LiteralExpr(t, bn, n); .)
| Ident (. id = new IdentifierExpr(x, x.val); e = id; .)
[ "("
( Expressions (. e = new NAryExpr(x, new FunctionCall(id), es); .)
| /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); .)
)
")"
]
| "old" (. x = t; .)
"("
Expression]