/*-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
COMPILER Dafny
/*--------------------------------------------------------------------------*/
static List/*!*/ theModules = new List();
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope/*!*/ parseVarScope = new Scope();
static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
public bool IsUnlimited;
}
// helper routine for parsing call statements
private static void RecordCallLhs(IdentifierExpr/*!*/ e,
List/*!*/ lhs,
List/*!*/ newVars) {
Contract.Requires(e != null);
Contract.Requires(cce.NonNullElements(lhs));
Contract.Requires(cce.NonNullElements(newVars));
int index = lhs.Count;
lhs.Add(e);
if (parseVarScope.Find(e.Name) == null) {
AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index);
newVars.Add(d);
parseVarScope.Push(e.Name, e.Name);
}
}
// helper routine for parsing call statements
private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
{
Contract.Requires(e != null);
Contract.Ensures(Contract.Result() != null);
FieldSelectExpr fse = e as FieldSelectExpr;
if (fse != null && fse.Obj is ImplicitThisExpr) {
return new IdentifierExpr(fse.tok, fse.FieldName);
}
return e; // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
}
///
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ filename, List/*!*/ modules) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List());
return Parse(s, filename, modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List());
return Parse(s, filename, modules);
}
}
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
List oldModules = theModules;
theModules = modules;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
theModules = oldModules;
return parser.errors.count;
}
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
cr = '\r'.
lf = '\n'.
tab = '\t'.
space = ' '.
quote = '"'.
nondigit = letter + special.
nonquote = letter + digit + space + glyph.
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigit {nondigit | digit}.
digits = digit {digit}.
string = quote {nonquote} quote.
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List theImports;
List membersDefaultClass = new List();
ModuleDecl module;
// to support multiple files, create a default module only if theModules doesn't already contain one
DefaultModuleDecl defaultModule = null;
foreach (ModuleDecl mdecl in theModules) {
defaultModule = mdecl as DefaultModuleDecl;
if (defaultModule != null) { break; }
}
bool defaultModuleCreatedHere = false;
if (defaultModule == null) {
defaultModuleCreatedHere = true;
defaultModule = new DefaultModuleDecl();
}
.)
{ "module" (. attrs = null; theImports = new List(); .)
{ Attribute[ }
Ident
[ "imports" Idents ] (. module = new ModuleDecl(id, id.val, theImports, attrs); .)
"{"
{ ClassDecl (. module.TopLevelDecls.Add(c); .)
| DatatypeDecl (. module.TopLevelDecls.Add(dt); .)
} (. theModules.Add(module); .)
"}"
| ClassDecl (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .)
| ClassMemberDecl
}
(. if (defaultModuleCreatedHere) {
defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
theModules.Add(defaultModule);
} else {
// find the default class in the default module, then append membersDefaultClass to its member list
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
if (defaultClass != null) {
defaultClass.Members.AddRange(membersDefaultClass);
break;
}
}
}
.)
EOF
.
ClassDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List();
IToken/*!*/ idRefined;
IToken optionalId = null;
List members = new List();
.)
"class"
{ Attribute][ }
Ident
[ GenericParameters ]
[ "refines" Ident (. optionalId = idRefined; .)
]
"{"
{ ClassMemberDecl
}
"}"
(. if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
else
c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
.)
.
ClassMemberDecl<.List/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
.)
{ "ghost" (. mmod.IsGhost = true; .)
| "static" (. mmod.IsStatic = true; .)
| "unlimited" (. mmod.IsUnlimited = true; .)
}
( FieldDecl
| FunctionDecl (. mm.Add(f); .)
| MethodDecl (. mm.Add(m); .)
| CouplingInvDecl
)
.
DatatypeDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List();
List ctors = new List();
.)
"datatype"
{ Attribute][ }
Ident
[ GenericParameters ]
"{"
{ DatatypeMemberDecl
}
"}" (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)
.
DatatypeMemberDecl<.List/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
List typeArgs = new List();
List formals = new List();
.)
{ Attribute][ }
Ident
[ GenericParameters ]
(. parseVarScope.PushMarker(); .)
[ FormalsOptionalIds ]
(. parseVarScope.PopMarker();
ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
.)
";"
.
FieldDecl<.MemberModifiers mmod, List/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
.)
"var"
(. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute][ }
IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
";"
.
CouplingInvDecl<.MemberModifiers mmod, List/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
List ids = new List();;
IToken/*!*/ id;
Expression/*!*/ e;
parseVarScope.PushMarker();
.)
"replaces"
(. if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
.)
{ Attribute][ }
Ident (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
{ "," Ident (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
}
"by"
Expression
";"
(. mm.Add(new CouplingInvariant(ids, e, attrs));
parseVarScope.PopMarker();
.)
.
GIdentType
/* isGhost always returns as false if allowGhost is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false; .)
[ "ghost" (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
IdentType
.
IdentType
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
Ident
":"
Type
.
IdentTypeOptional
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
Ident
[ ":" Type (. optType = ty; .)
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
TypeIdentOptional
= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; isGhost = false; .)
[ "ghost" (. isGhost = true; .)
]
TypeAndToken
[ ":"
(. /* try to convert ty to an identifier */
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
name = udt.Name;
} else {
SemErr(id, "invalid formal-parameter name in datatype constructor");
}
.)
Type
]
(. if (name != null) {
identName = name;
} else {
identName = "#" + anonymousIds++;
}
.)
.
/*------------------------------------------------------------------------*/
GenericParameters<.List/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id; .)
"<"
Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .)
{ "," Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .)
}
">"
.
/*------------------------------------------------------------------------*/
MethodDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
Attributes attrs = null;
List/*!*/ typeArgs = new List();
List ins = new List();
List outs = new List();
List req = new List();
List mod = new List();
List ens = new List();
List dec = new List();
Statement/*!*/ bb; BlockStmt body = null;
bool isRefinement = false;
.)
( "method"
| "refines" (. isRefinement = true; .)
)
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
.)
{ Attribute][ }
Ident
[ GenericParameters ]
(. parseVarScope.PushMarker(); .)
Formals
[ "returns"
Formals
]
( ";" { MethodSpec }
| { MethodSpec } BlockStmt (. body = (BlockStmt)bb; .)
)
(. parseVarScope.PopMarker();
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
.)
.
MethodSpec<.List/*!*/ req, List/*!*/ mod, List/*!*/ ens,
List/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false;
.)
( "modifies" [ FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
] ";"
| [ "free" (. isFree = true; .)
]
( "requires" Expression ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures" Expression ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
)
| "decreases" Expressions ";"
)
.
Formals<.bool incoming, bool allowGhosts, List/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"("
[
GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
{ "," GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
}
]
")"
.
FormalsOptionalIds<.List/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
"("
[
TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
{ "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
}
]
")"
.
/*------------------------------------------------------------------------*/
Type
= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
TypeAndToken
.
TypeAndToken
= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List/*!*/ gt;
.)
( "bool" (. tok = t; .)
| "int" (. tok = t; ty = new IntType(); .)
| "set" (. tok = t; gt = new List(); .)
GenericInstantiation (. if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
}
ty = new SetType(gt[0]);
.)
| "seq" (. tok = t; gt = new List(); .)
GenericInstantiation (. if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
ty = new SeqType(gt[0]);
.)
| ReferenceType
)
.
ReferenceType
= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List/*!*/ gt;
.)
( "object" (. tok = t; ty = new ObjectType(); .)
| "array" (. tok = t; gt = new List(); .)
GenericInstantiation (. if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
ty = UserDefinedType.ArrayType(tok, gt[0]);
.)
| Ident (. gt = new List(); .)
[ GenericInstantiation ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
.
GenericInstantiation<.List/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
"<"
Type (. gt.Add(ty); .)
{ "," Type (. gt.Add(ty); .)
}
">"
.
/*------------------------------------------------------------------------*/
FunctionDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
Attributes attrs = null;
IToken/*!*/ id;
List typeArgs = new List();
List formals = new List();
Type/*!*/ returnType;
List reqs = new List();
List reads = new List();
List decreases = new List();
Expression/*!*/ bb; Expression body = null;
bool isFunctionMethod = false;
.)
"function"
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
Ident
[ GenericParameters ]
(. parseVarScope.PushMarker(); .)
Formals
":"
Type
( ";"
{ FunctionSpec }
| { FunctionSpec }
FunctionBody (. body = bb; .)
)
(. parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
.)
.
FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
( "requires" Expression ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression (. reads.Add(fe); .)
}
] ";"
| "decreases" Expressions ";"
)
.
PossiblyWildExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr; .)
/* A decreases clause on a loop asks that no termination check be performed.
* Use of this feature is sound only with respect to partial correctness.
*/
( "*" (. e = new WildcardExpr(t); .)
| Expression
)
.
PossiblyWildFrameExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
/* A reads clause can list a wildcard, which allows the enclosing function to
* read anything. In many cases, and in particular in all cases where
* the function is defined recursively, this makes it next to impossible to make
* any use of the function. Nevertheless, as an experimental feature, the
* language allows it (and it is sound).
*/
( "*" (. fe = new FrameExpression(new WildcardExpr(t), null); .)
| FrameExpression
)
.
FrameExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; .)
Expression
[ "`" Ident (. fieldName = id.val; .)
]
(. fe = new FrameExpression(e, fieldName); .)
.
FunctionBody
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
"{"
( MatchExpression
| Expression
)
"}"
.
MatchExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List cases = new List();
.)
"match" (. x = t; .)
Expression
{ CaseExpression (. cases.Add(c); .)
}
(. e = new MatchExpr(x, e, cases); .)
.
CaseExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
List arguments = new List();
Expression/*!*/ body;
.)
"case" (. x = t; parseVarScope.PushMarker(); .)
Ident
[ "("
Ident (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val); .)
{ "," Ident (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val); .)
}
")" ]
"=>"
Expression (. c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker(); .)
.
/*------------------------------------------------------------------------*/
BlockStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); IToken/*!*/ x;
List body = new List();
Statement/*!*/ s;
.)
(. parseVarScope.PushMarker(); .)
"{" (. x = t; .)
{ Stmt
}
"}" (. block = new BlockStmt(x, body); .)
(. parseVarScope.PopMarker(); .)
.
Stmt<.List/*!*/ ss.>
= (. Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s; .)
/* By first reading a sequence of block statements, we avoid problems in the generated parser, despite
the ambiguity in the grammar. See Note in ConstAtomExpression production.
*/
{ BlockStmt (. ss.Add(s); .)
}
( OneStmt (. ss.Add(s); .)
| VarDeclStmts
)
.
OneStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
( AssertStmt
| AssumeStmt
| UseStmt
| PrintStmt
| AssignStmt
| HavocStmt
| CallStmt
| IfStmt
| WhileStmt
| MatchStmt
| ForeachStmt
| "label" (. x = t; .)
Ident ":" (. s = new LabelStmt(x, id.val); .)
| "break" (. x = t; .)
[ Ident (. label = id.val; .)
] ";" (. s = new BreakStmt(x, label); .)
| "return" (. x = t; .)
";" (. s = new ReturnStmt(x); .)
)
.
AssignStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ lhs;
Expression rhs;
Type ty;
s = dummyStmt;
.)
LhsExpr
":=" (. x = t; .)
AssignRhs (. if (ty == null) {
Contract.Assert(rhs != null);
s = new AssignStmt(x, lhs, rhs);
} else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
s = new AssignStmt(x, lhs, ty, rhs);
}
.)
";"
.
AssignRhs
/* ensures e != null || ty != null; */
= (. IToken/*!*/ x; Expression/*!*/ ee; Type/*!*/ tt;
e = null; ty = null;
.)
( "new" TypeAndToken (. ty = tt; .)
[ "[" Expression "]" (. e = ee; .)
]
| Expression (. e = ee; .)
) (. if (e == null && ty == null) { e = dummyExpr; } .)
.
HavocStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs; .)
"havoc" (. x = t; .)
LhsExpr ";" (. s = new AssignStmt(x, lhs); .)
.
LhsExpr
= (.Contract.Ensures(Contract.ValueAtReturn(out e)!=null);.)
SelectExpression
.
VarDeclStmts<.List/*!*/ ss.>
= (. Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false; .)
[ "ghost" (. isGhost = true; .)
]
"var"
IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
{ "," IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
}
";"
.
IdentTypeRhs
= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty; Expression/*!*/ e;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
.)
Ident
[ ":" Type (. optionalType = ty; .)
]
[ ":="
AssignRhs
]
(. if (newType == null && rhs != null) {
optionalRhs = new ExprRhs(rhs);
} else if (newType != null) {
if (rhs == null) {
optionalRhs = new TypeRhs(newType);
} else {
optionalRhs = new TypeRhs(newType, rhs);
}
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
}
d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs);
.)
.
IfStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
Expression guard;
Statement/*!*/ thn;
Statement/*!*/ s;
Statement els = null;
.)
"if" (. x = t; .)
Guard
BlockStmt
[ "else"
( IfStmt (. els = s; .)
| BlockStmt (. els = s; .)
)
]
(. ifStmt = new IfStmt(x, guard, thn, els); .)
.
WhileStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard;
bool isFree; Expression/*!*/ e;
List invariants = new List();
List decreases = new List();
Statement/*!*/ body;
.)
"while" (. x = t; .)
Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
]
"invariant"
Expression (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
| "decreases"
PossiblyWildExpression (. decreases.Add(e); .)
{ "," PossiblyWildExpression (. decreases.Add(e); .)
}
";"
}
BlockStmt (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
.
Guard /* null represents demonic-choice */
= (. Expression/*!*/ ee; e = null; .)
"("
( "*" (. e = null; .)
| Expression (. e = ee; .)
)
")"
.
MatchStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List cases = new List(); .)
"match" (. x = t; .)
Expression
"{"
{ CaseStatement (. cases.Add(c); .)
}
"}"
(. s = new MatchStmt(x, e, cases); .)
.
CaseStatement
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id, arg;
List arguments = new List();
List body = new List();
.)
"case" (. x = t; parseVarScope.PushMarker(); .)
Ident
[ "("
Ident (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val); .)
{ "," Ident (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val); .)
}
")" ]
"=>"
(. parseVarScope.PushMarker(); .)
{ Stmt }
(. parseVarScope.PopMarker(); .)
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
(. parseVarScope.PopMarker(); .)
.
CallStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x, id;
Expression/*!*/ e;
List lhs = new List();
List newVars = new List();
.)
"call" (. x = t; .)
CallStmtSubExpr
[ "," /* call a,b,c,... := ... */
(. e = ConvertToLocal(e);
if (e is IdentifierExpr) {
RecordCallLhs((IdentifierExpr)e, lhs, newVars);
} else if (e is FieldSelectExpr) {
SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
} else {
SemErr(e.tok, "each LHS of call statement must be a variable");
}
.)
Ident (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
{ "," Ident (. RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); .)
}
":="
CallStmtSubExpr
| ":=" /* call a := ... */
(. e = ConvertToLocal(e);
if (e is IdentifierExpr) {
RecordCallLhs((IdentifierExpr)e, lhs, newVars);
} else if (e is FieldSelectExpr) {
SemErr(e.tok, "each LHS of call statement must be a variable, not a field");
} else {
SemErr(e.tok, "each LHS of call statement must be a variable");
}
.)
CallStmtSubExpr
]
";"
/* "e" has now been parsed as one of: IdentifierExpr, FunctionCallExpr, FieldSelectExpr.
It denotes the RHS, so to be legal it must be a FunctionCallExpr. */
(. if (e is FunctionCallExpr) {
FunctionCallExpr fce = (FunctionCallExpr)e;
s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args); // this actually does an ownership transfer of fce.Args
} else {
SemErr("RHS of call statement must denote a method invocation");
s = new CallStmt(x, newVars, lhs, dummyExpr, "dummyMethodName", new List());
}
.)
.
/*------------------------------------------------------------------------*/
ForeachStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x, boundVar;
Type/*!*/ ty;
Expression/*!*/ collection;
Expression/*!*/ range;
List bodyPrefix = new List();
AssignStmt bodyAssign = null;
.)
(. parseVarScope.PushMarker(); .)
"foreach" (. x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
.)
"(" Ident
[ ":" Type ]
"in" Expression
(. parseVarScope.Push(boundVar.val, boundVar.val); .)
[ "|" Expression ]
")"
"{"
{ AssertStmt (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
| AssumeStmt (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
| UseStmt (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
}
( AssignStmt (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
| HavocStmt (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
)
"}" (. if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
} else {
s = dummyStmt; // some error occurred in parsing the bodyAssign
}
.)
(. parseVarScope.PopMarker(); .)
.
AssertStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assert" (. x = t; .)
Expression ";" (. s = new AssertStmt(x, e); .)
.
AssumeStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assume" (. x = t; .)
Expression ";" (. s = new AssumeStmt(x, e); .)
.
UseStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"use" (. x = t; .)
Expression ";" (. s = new UseStmt(x, e); .)
.
PrintStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List args = new List();
.)
"print" (. x = t; .)
AttributeArg (. args.Add(arg); .)
{ "," AttributeArg (. args.Add(arg); .)
}
";" (. s = new PrintStmt(x, args); .)
.
/*------------------------------------------------------------------------*/
Expression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expression/*!*/ e0; Expression/*!*/ e1 = dummyExpr;
e = dummyExpr;
.)
( "if" (. x = t; .)
Expression
"then" Expression
"else" Expression (. e = new ITEExpr(x, e, e0, e1); .)
| EquivExpression
)
.
/*------------------------------------------------------------------------*/
EquivExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
ImpliesExpression
{ EquivOp (. x = t; .)
ImpliesExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
}
.
EquivOp = "<==>" | '\u21d4'.
/*------------------------------------------------------------------------*/
ImpliesExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
LogicalExpression
[ ImpliesOp (. x = t; .)
ImpliesExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
]
.
ImpliesOp = "==>" | '\u21d2'.
/*------------------------------------------------------------------------*/
LogicalExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
RelationalExpression
[ AndOp (. x = t; .)
RelationalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
{ AndOp (. x = t; .)
RelationalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
}
| OrOp (. x = t; .)
RelationalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
{ OrOp (. x = t; .)
RelationalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
}
]
.
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
/*------------------------------------------------------------------------*/
RelationalExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
Term
[ RelOp
Term (. e0 = new BinaryExpr(x, op, e0, e1); .)
]
.
RelOp
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
| "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
| ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
| "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
| ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
| "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
| "!!" (. x = t; op = BinaryExpr.Opcode.Disjoint; .)
| "in" (. x = t; op = BinaryExpr.Opcode.In; .)
| "!in" (. x = t; op = BinaryExpr.Opcode.NotIn; .)
| '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
| '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
| '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
)
.
/*------------------------------------------------------------------------*/
Term
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
Factor
{ AddOp
Factor (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
AddOp
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "+" (. x = t; op = BinaryExpr.Opcode.Add; .)
| "-" (. x = t; op = BinaryExpr.Opcode.Sub; .)
)
.
/*------------------------------------------------------------------------*/
Factor
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
UnaryExpression
{ MulOp
UnaryExpression (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
MulOp
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op = BinaryExpr.Opcode.Mul; .)
| "/" (. x = t; op = BinaryExpr.Opcode.Div; .)
| "%" (. x = t; op = BinaryExpr.Opcode.Mod; .)
)
.
/*------------------------------------------------------------------------*/
UnaryExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .)
( "-" (. x = t; .)
UnaryExpression (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
| NegOp (. x = t; .)
UnaryExpression (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
| SelectExpression
| ConstAtomExpression
)
.
NegOp = "!" | '\u00ac'.
ConstAtomExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x, dtName, id; BigInteger n; List/*!*/ elements;
e = dummyExpr;
.)
( "false" (. e = new LiteralExpr(t, false); .)
| "true" (. e = new LiteralExpr(t, true); .)
| "null" (. e = new LiteralExpr(t); .)
| Nat (. e = new LiteralExpr(t, n); .)
| "#" (. x = t; .)
Ident
"."
Ident (. elements = new List(); .)
[ "("
[ Expressions ]
")" ] (. e = new DatatypeValue(t, dtName.val, id.val, elements); .)
| "fresh" (. x = t; .)
"(" Expression ")" (. e = new FreshExpr(x, e); .)
| "|" (. x = t; .)
Expression (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
"|"
| "{" (. x = t; elements = new List(); .)
[ Expressions ] (. e = new SetDisplayExpr(x, elements); .)
"}"
| "[" (. x = t; elements = new List(); .)
[ Expressions ] (. e = new SeqDisplayExpr(x, elements); .)
"]"
)
.
/*------------------------------------------------------------------------*/
/* returns one of:
-- IdentifierExpr
-- FunctionCallExpr
-- FieldSelectExpr
*/
CallStmtSubExpr
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
( IdentOrFuncExpression
| ObjectExpression
SelectOrCallSuffix][
)
{ SelectOrCallSuffix][ }
.
SelectExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; .)
( IdentOrFuncExpression
| ObjectExpression
)
{ SelectOrCallSuffix][ }
.
IdentOrFuncExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List/*!*/ args; .)
Ident
[ "(" (. args = new List(); .)
[ Expressions ]
")" (. e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args); .)
] (. if (e == dummyExpr) {
if (parseVarScope.Find(id.val) != null) {
e = new IdentifierExpr(id, id.val);
} else {
e = new FieldSelectExpr(id, new ImplicitThisExpr(id), id.val);
}
}
.)
.
SelectOrCallSuffix][
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
bool func = false;
.)
( "."
Ident
[ "(" (. args = new List(); func = true; .)
[ Expressions ]
")" (. e = new FunctionCallExpr(id, id.val, e, args); .)
] (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
| "[" (. x = t; .)
( Expression]