/*-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/
using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
COMPILER Dafny
/*--------------------------------------------------------------------------*/
static List theModules;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
public bool IsUnlimited;
}
// helper routine for parsing call statements
///
/// 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, BuiltIns builtIns) /* 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, builtIns);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List());
return Parse(s, filename, modules, builtIns);
}
}
}
///
/// 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, BuiltIns builtIns) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
Errors errors = new Errors();
return Parse(s, filename, modules, builtIns, errors);
}
///
/// 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 with the given Errors sink.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns,
Errors/*!*/ errors) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
Contract.Requires(errors != null);
List oldModules = theModules;
theModules = modules;
BuiltIns oldBuiltIns = builtIns;
theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
theModules = oldModules;
theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
}
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
posDigit = "123456789".
special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
cr = '\r'.
lf = '\n'.
tab = '\t'.
space = ' '.
quote = '"'.
nondigit = letter + special.
idchar = nondigit + digit.
nonquote = letter + digit + space + glyph.
/* exclude the characters in 'array' */
nondigitMinusA = nondigit - 'a'.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
| 'a' [ idcharMinusR {idchar} ] /* if char 0 is an 'a', then either there is no char 1 or char 1 is not an 'r' */
| 'a' 'r' [ idcharMinusR {idchar} ] /* etc. */
| 'a' 'r' 'r' [ idcharMinusA {idchar} ]
| 'a' 'r' 'r' 'a' [ idcharMinusY {idchar} ]
| 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
| 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}.
digits = digit {digit}.
arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
string = quote {nonquote} quote.
colon = ':'.
lbrace = '{'.
rbrace = '}'.
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
Attributes attrs; IToken/*!*/ id; List theImports;
List membersDefaultClass = new List();
List namedModuleDefaultClassMembers;
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();
}
IToken idRefined;
.)
{ "module" (. attrs = null; idRefined = null; theImports = new List();
namedModuleDefaultClassMembers = new List();
.)
{ Attribute[ }
Ident (. defaultModule.ImportNames.Add(id.val); .)
[ "refines" Ident ]
[ "imports" Idents ] (. module = new ModuleDecl(id, id.val, idRefined == null ? null : idRefined.val, theImports, attrs); .)
"{" (. module.BodyStartTok = t; .)
{ ClassDecl (. module.TopLevelDecls.Add(c); .)
| DatatypeDecl (. module.TopLevelDecls.Add(dt); .)
| ArbitraryTypeDecl(. module.TopLevelDecls.Add(at); .)
| ClassMemberDecl
}
"}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
theModules.Add(module); .)
| ClassDecl (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .)
| ArbitraryTypeDecl (. defaultModule.TopLevelDecls.Add(at); .)
| 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();
List members = new List();
IToken bodyStart;
.)
SYNC
"class"
{ Attribute][ }
Ident
[ GenericParameters ]
"{" (. bodyStart = t; .)
{ ClassMemberDecl
}
"}"
(. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
ClassMemberDecl<.List/*!*/ mm, bool allowConstructors.>
= (. 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); .)
)
.
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();
IToken bodyStart = Token.NoToken; // dummy assignment
.)
SYNC
"datatype"
{ Attribute][ }
Ident
[ GenericParameters ]
"=" (. bodyStart = t; .)
DatatypeMemberDecl
{ "|" DatatypeMemberDecl }
SYNC ";"
(. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
.)
.
DatatypeMemberDecl<.List/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
List formals = new List();
.)
{ Attribute][ }
Ident
[ FormalsOptionalIds ]
(. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
FieldDecl<.MemberModifiers mmod, List/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
.)
SYNC
"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)); .)
}
SYNC ";"
.
ArbitraryTypeDecl
= (. IToken/*!*/ id;
Attributes attrs = null;
.)
"type"
{ Attribute][ }
Ident (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)
SYNC ";"
.
GIdentType
/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false; .)
[ "ghost" (. if (allowGhostKeyword) { 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
.
LocalIdentTypeOptional
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
Ident
[ ":" Type (. optType = ty; .)
]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
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();
IToken openParen;
List ins = new List();
List outs = new List();
List req = new List();
List mod = new List();
List ens = new List();
List dec = new List();
Attributes decAttrs = null;
Attributes modAttrs = null;
Statement/*!*/ bb; BlockStmt body = null;
bool isConstructor = false;
bool signatureOmitted = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
( "method"
| "constructor" (. if (allowConstructor) {
isConstructor = true;
} else {
SemErr(t, "constructors are only allowed in classes");
}
.)
)
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
}
if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
}
.)
{ Attribute][ }
Ident
(
[ GenericParameters ]
Formals
[ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals
]
| "..." (. signatureOmitted = true; openParen = Token.NoToken; .)
)
{ MethodSpec }
[ BlockStmt (. body = (BlockStmt)bb; .)
]
(. if (isConstructor) {
m = new Constructor(id, id.val, typeArgs, ins,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureOmitted);
} else {
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureOmitted);
}
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
.)
.
MethodSpec<.List/*!*/ req, List/*!*/ mod, List/*!*/ ens,
List/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs.>
= (. 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; Attributes ensAttrs = null;
.)
SYNC
( "modifies" { IF(IsAttribute()) Attribute][ }
[ FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
] SYNC ";"
| [ "free" (. isFree = true; .)
]
( "requires" Expression SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures" { IF(IsAttribute()) Attribute][ } Expression SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
)
| "decreases" { IF(IsAttribute()) Attribute][ } DecreasesList SYNC ";"
)
.
Formals<.bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"(" (. openParen = t; .)
[
GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
{ "," GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
}
]
")"
.
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)); .)
{ "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
}
]
")"
.
/*------------------------------------------------------------------------*/
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; .)
| "nat" (. tok = t; ty = new NatType(); .)
| "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]);
.)
| "multiset" (. tok = t; gt = new List(); .)
GenericInstantiation (. if (gt.Count != 1) {
SemErr("multiset type expects exactly one type argument");
}
ty = new MultiSetType(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(); .)
| arrayToken (. tok = t; gt = new List(); .)
GenericInstantiation (. if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
int dims = 1;
if (tok.val.Length != 5) {
dims = int.Parse(tok.val.Substring(5));
}
ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
.)
| 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 = Token.NoToken; // to please compiler
List typeArgs = new List();
List formals = new List();
Type/*!*/ returnType = new BoolType();
List reqs = new List();
List ens = new List();
List reads = new List();
List decreases = new List();
Expression/*!*/ bb; Expression body = null;
bool isPredicate = false;
bool isFunctionMethod = false;
IToken openParen = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
.)
/* ----- function ----- */
( "function"
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
Ident
(
[ GenericParameters ]
Formals
":"
Type
| "..." (. signatureOmitted = true;
openParen = Token.NoToken; .)
)
/* ----- predicate ----- */
| "predicate" (. isPredicate = true; .)
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
Ident
(
[ GenericParameters ]
[ Formals
[ ":" (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
]
]
| "..." (. signatureOmitted = true;
openParen = Token.NoToken; .)
)
)
{ FunctionSpec }
[ FunctionBody (. body = bb; .)
]
(. if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals,
reqs, reads, ens, new Specification(decreases, null), body, false, attrs, signatureOmitted);
} else {
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, openParen, formals, returnType,
reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureOmitted);
}
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
.)
.
FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
(
SYNC
"requires" Expression SYNC ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression (. reads.Add(fe); .)
}
] SYNC ";"
| "ensures" Expression SYNC ";" (. ens.Add(e); .)
| "decreases" DecreasesList SYNC ";"
)
.
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; .)
"{" (. bodyStart = t; .)
Expression
"}" (. bodyEnd = t; .)
.
/*------------------------------------------------------------------------*/
BlockStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List body = new List();
.)
"{" (. bodyStart = t; .)
{ Stmt
}
"}" (. bodyEnd = t;
block = new BlockStmt(bodyStart, body); .)
.
Stmt<.List/*!*/ ss.>
= (. Statement/*!*/ s;
.)
OneStmt (. ss.Add(s); .)
.
OneStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
IToken bodyStart, bodyEnd;
int breakCount;
.)
SYNC
( BlockStmt
| AssertStmt
| AssumeStmt
| PrintStmt
| UpdateStmt
| VarDeclStatement
| IfStmt
| WhileStmt
| MatchStmt
| ParallelStmt
| "label" (. x = t; .)
Ident ":"
OneStmt (. s.Labels = new LabelNode(x, id.val, s.Labels); .)
| "break" (. x = t; breakCount = 1; label = null; .)
( Ident (. label = id.val; .)
| { "break" (. breakCount++; .)
}
)
SYNC
";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| ReturnStmt
| "..." (. s = new SkeletonStatement(t); .)
";"
)
.
ReturnStmt
= (.
IToken returnTok = null;
List rhss = null;
AssignmentRhs r;
.)
"return" (. returnTok = t; .)
[
Rhs (. rhss = new List(); rhss.Add(r); .)
{ "," Rhs (. rhss.Add(r); .)
}
]
";" (. s = new ReturnStmt(returnTok, rhss); .)
.
UpdateStmt
= (. List lhss = new List();
List rhss = new List();
Expression e; AssignmentRhs r;
Expression lhs0;
IToken x;
Attributes attrs = null;
.)
Lhs (. x = e.tok; .)
( { Attribute][ }
";" (. rhss.Add(new ExprRhs(e, attrs)); .)
| (. lhss.Add(e); lhs0 = e; .)
{ "," Lhs (. lhss.Add(e); .)
}
":=" (. x = t; .)
Rhs (. rhss.Add(r); .)
{ "," Rhs (. rhss.Add(r); .)
}
";"
| ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. s = new UpdateStmt(x, lhss, rhss); .)
.
Rhs
= (. IToken/*!*/ x, newToken; Expression/*!*/ e;
List ee = null;
Type ty = null;
CallStmt initCall = null;
List args;
r = null; // to please compiler
Attributes attrs = null;
.)
( "new" (. newToken = t; .)
TypeAndToken
[ "[" (. ee = new List(); .)
Expressions
"]" (. // make sure an array class with this dimensionality exists
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
.)
| "." Ident
"(" (. args = new List(); .)
[ Expressions ]
")" (. initCall = new CallStmt(x, new List(),
receiverForInitCall, x.val, args); .)
]
(. if (ee != null) {
r = new TypeRhs(newToken, ty, ee);
} else {
r = new TypeRhs(newToken, ty, initCall);
}
.)
/* One day, the choose expression should be treated just as a special case of a method call. */
| "choose" (. x = t; .)
Expression (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
| "*" (. r = new HavocRhs(t); .)
| Expression (. r = new ExprRhs(e); .)
)
{ Attribute][ } (. r.Attributes = attrs; .)
.
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null; bool isGhost = false;
VarDecl/*!*/ d;
AssignmentRhs r; IdentifierExpr lhs0;
List lhss = new List();
List rhss = new List();
.)
[ "ghost" (. isGhost = true; x = t; .)
]
"var" (. if (!isGhost) { x = t; } .)
LocalIdentTypeOptional (. lhss.Add(d); .)
{ ","
LocalIdentTypeOptional (. lhss.Add(d); .)
}
[ ":=" (. assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here
.)
Rhs (. rhss.Add(r); .)
{ "," Rhs (. rhss.Add(r); .)
}
]
";"
(. UpdateStmt update;
if (rhss.Count == 0) {
update = null;
} else {
var ies = new List();
foreach (var lhs in lhss) {
ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
}
update = new UpdateStmt(assignTok, ies, rhss);
}
s = new VarDeclStmt(x, lhss, update);
.)
.
IfStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
Expression guard = null; bool guardOmitted = false;
Statement/*!*/ thn;
Statement/*!*/ s;
Statement els = null;
IToken bodyStart, bodyEnd;
List alternatives;
ifStmt = dummyStmt; // to please the compiler
.)
"if" (. x = t; .)
(
( Guard
| "..." (. guardOmitted = true; .)
)
BlockStmt
[ "else"
( IfStmt (. els = s; .)
| BlockStmt (. els = s; .)
)
]
(. if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
} else {
ifStmt = new IfStmt(x, guard, thn, els);
}
.)
|
AlternativeBlock
(. ifStmt = new AlternativeStmt(x, alternatives); .)
)
.
AlternativeBlock<.out List alternatives.>
= (. alternatives = new List();
IToken x;
Expression e;
List body;
.)
"{"
{ "case" (. x = t; .)
Expression
"=>"
(. body = new List(); .)
{ Stmt }
(. alternatives.Add(new GuardedAlternative(x, e, body)); .)
}
"}"
.
WhileStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard = null; bool guardOmitted = false;
List invariants = new List();
List decreases = new List();
Attributes decAttrs = null;
Attributes modAttrs = null;
List mod = null;
Statement/*!*/ body = null; bool bodyOmitted = false;
IToken bodyStart = null, bodyEnd = null;
List alternatives;
stmt = dummyStmt; // to please the compiler
.)
"while" (. x = t; .)
(
( Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
| "..." (. guardOmitted = true; .)
)
LoopSpec
( BlockStmt
| "..." (. bodyOmitted = true; .)
)
(.
if (guardOmitted || bodyOmitted) {
if (decreases.Count != 0) {
SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");
}
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
}
if (body == null) {
body = new AssertStmt(x, new LiteralExpr(x, true), null);
}
stmt = new WhileStmt(x, guard, invariants, new Specification(null, null), new Specification(null, null), body);
stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);
} else {
stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body);
}
.)
|
LoopSpec
AlternativeBlock
(. stmt = new AlternativeLoopStmt(x, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives); .)
)
.
LoopSpec<.out List invariants, out List decreases, out List mod, ref Attributes decAttrs, ref Attributes modAttrs.>
= (. FrameExpression/*!*/ fe;
invariants = new List();
MaybeFreeExpression invariant = null;
decreases = new List();
mod = null;
.)
{
Invariant SYNC ";" (. invariants.Add(invariant); .)
| SYNC "decreases"
{ IF(IsAttribute()) Attribute][ }
DecreasesList SYNC ";"
| SYNC "modifies"
{ IF(IsAttribute()) Attribute][ } (. mod = mod ?? new List(); .)
[ FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
] SYNC ";"
}
.
Invariant
= (. bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; .)
SYNC
["free" (. isFree = true; .)
]
"invariant" { IF(IsAttribute()) Attribute][ } Expression (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)
.
DecreasesList<.List decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
decreases.Add(e);
}
.)
{ "," PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
decreases.Add(e);
}
.)
}
.
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;
List arguments = new List();
BoundVar/*!*/ bv;
List body = new List();
.)
"case" (. x = t; .)
Ident
[ "("
IdentTypeOptional (. arguments.Add(bv); .)
{ "," IdentTypeOptional (. arguments.Add(bv); .)
}
")" ]
"=>"
{ Stmt }
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
/*------------------------------------------------------------------------*/
AssertStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ e = null; Attributes attrs = null;
.)
"assert" (. x = t; s = null;.)
{ IF(IsAttribute()) Attribute][ }
( Expression
| "..."
)
";"
(. if (e == null) {
s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
s = new AssertStmt(x, e, attrs);
}
.)
.
AssumeStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assume" (. x = t; .)
Expression ";" (. s = new AssumeStmt(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); .)
.
ParallelStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x;
List bvars = null;
Attributes attrs = null;
Expression range = null;
var ens = new List();
bool isFree;
Expression/*!*/ e;
Statement/*!*/ block;
IToken bodyStart, bodyEnd;
.)
"parallel" (. x = t; .)
"("
[ (. List bvarsX; Attributes attrsX; Expression rangeX; .)
QuantifierDomain
(. bvars = bvarsX; attrs = attrsX; range = rangeX;
.)
]
(. if (bvars == null) { bvars = new List(); }
if (range == null) { range = new LiteralExpr(x, true); }
.)
")"
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
]
"ensures" Expression ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
}
BlockStmt
(. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
.
/*------------------------------------------------------------------------*/
Expression
=
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 e) != null);
IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
List chain = null;
List ops = null;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
// 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
// 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
// 3 ("illegal") indicates illegal chain
// 4 ("disjoint") indicates chain of disjoint set operators
bool hasSeenNeq = false;
.)
Term (. e = e0; .)
[ RelOp (. firstOpTok = x; .)
Term (. e = new BinaryExpr(x, op, e0, e1);
if (op == BinaryExpr.Opcode.Disjoint)
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
.)
{ (. if (chain == null) {
chain = new List();
ops = new List]