/*-----------------------------------------------------------------------------
//
// 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
/*--------------------------------------------------------------------------*/
readonly Expression/*!*/ dummyExpr;
readonly AssignmentRhs/*!*/ dummyRhs;
readonly FrameExpression/*!*/ dummyFrameExpr;
readonly Statement/*!*/ dummyStmt;
readonly ModuleDecl theModule;
readonly BuiltIns theBuiltIns;
readonly bool theVerifyThisFile;
int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
}
///
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(module != null);
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List());
return Parse(s, filename, module, builtIns, errors, verifyThisFile);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List());
return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);
}
}
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Errors errors = new Errors();
return Parse(s, filename, module, builtIns, errors, verifyThisFile);
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// 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, ModuleDecl module, BuiltIns builtIns,
Errors/*!*/ errors, bool verifyThisFile=true) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Contract.Requires(errors != null);
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, module, builtIns, verifyThisFile);
parser.Parse();
return parser.errors.count;
}
public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
: this(scanner, errors) // the real work
{
// initialize readonly fields
dummyExpr = new LiteralExpr(Token.NoToken);
dummyRhs = new ExprRhs(dummyExpr, null);
dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
theModule = module;
theBuiltIns = builtIns;
theVerifyThisFile = verifyThisFile;
}
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
}
bool IsAlternative() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.val == "case";
}
bool IsLoopSpec() {
return la.val == "invariant" | la.val == "decreases" | la.val == "modifies";
}
bool IsLoopSpecOrAlternative() {
Token x = scanner.Peek();
return IsLoopSpec() || (la.kind == _lbrace && x.val == "case");
}
bool IsParenStar() {
scanner.ResetPeek();
Token x = scanner.Peek();
return la.kind == _openparen && x.kind == _star;
}
string UnwildIdent(string x, bool allowWildcardId) {
if (x.StartsWith("_")) {
if (allowWildcardId && x.Length == 1) {
return "_v" + anonymousIds++;
} else {
SemErr("cannot declare identifier beginning with underscore");
}
}
return x;
}
bool IsLambda(bool allowLambda)
{
return allowLambda &&
(la.kind == _darrow || la.kind == _arrow
|| la.kind == _reads || la.kind == _requires);
}
bool IsIdentParen() {
Token x = scanner.Peek();
return la.kind == _ident && x.kind == _openparen;
}
bool IsIdentColonOrBar() {
Token x = scanner.Peek();
return la.kind == _ident && (x.kind == _colon || x.kind == _verticalbar);
}
bool SemiFollowsCall(bool allowSemi, Expression e) {
return allowSemi && la.kind == _semi &&
(e is FunctionCallExpr || e is ApplyExpr ||
(e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
}
bool CloseOptionalParen(bool usesOptionalParen) {
return usesOptionalParen && la.kind == _closeparen;
}
bool CloseOptionalBrace(bool usesOptionalBrace) {
return usesOptionalBrace && la.kind == _rbrace;
}
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
posDigit = "123456789".
hexdigit = "0123456789ABCDEFabcdef".
special = "'_?".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
cr = '\r'.
lf = '\n'.
tab = '\t'.
space = ' '.
nondigit = letter + special.
idchar = nondigit + digit.
nonidchar = ANY - idchar.
/* exclude the characters in 'array' and '\'' */
nondigitMinusATick = nondigit - 'a' - '\''.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
idcharMinusTick = idchar - '\''.
/* string literals */
charChar = ANY - '\'' - '\\' - cr - lf.
stringChar = ANY - '"' - '\\' - cr - lf.
verbatimStringChar = ANY - '"'.
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusATick {idchar} /* if char 0 is not an 'a' or '\'', 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}
| "'" [ idchar ] /* if char 0 is a '\'' and length is 1 or 2, then it is an identifier */
| "'" idchar idcharMinusTick /* if char 0 is '\'' and length is 3, then it is an identifier provided char 2 is not '\'' */
| "'" idchar idchar idchar { idchar } /* if char 0 is '\'' and length exceeds 3, then it is an identifier */
.
digits = digit {['_'] digit}.
hexdigits = "0x" hexdigit {['_'] hexdigit}.
decimaldigits = digit {['_'] digit} '.' digit {['_'] digit}.
arrayToken = "array" [posDigit {digit}].
charToken =
"'"
( charChar
| "\\\'" | "\\\"" | "\\\\" | "\\0" | "\\n" | "\\r" | "\\t"
| "\\u" hexdigit hexdigit hexdigit hexdigit
)
"'".
stringToken =
'"'
{ stringChar
| "\\\'" | "\\\"" | "\\\\" | "\\0" | "\\n" | "\\r" | "\\t"
| "\\u" hexdigit hexdigit hexdigit hexdigit
}
'"'
| '@' '"' { verbatimStringChar | "\"\"" } '"'.
colon = ':'.
verticalbar = '|'.
semi = ';'.
darrow = "=>".
arrow = "->".
reads = "reads".
requires = "requires".
lbrace = '{'.
rbrace = '}'.
openparen = '('.
closeparen = ')'.
star = '*'.
notIn = "!in" CONTEXT (nonidchar).
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
List membersDefaultClass = new List();
ModuleDecl submodule;
// to support multiple files, create a default module only if theModule is null
DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
.)
{ "include" stringToken (. {
string parsedFile = t.filename;
bool isVerbatimString;
string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);
string fullPath = includedFile;
if (!Path.IsPathRooted(includedFile)) {
string basePath = Path.GetDirectoryName(parsedFile);
includedFile = Path.Combine(basePath, includedFile);
fullPath = Path.GetFullPath(includedFile);
}
defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
}
.)
}
{ SubModuleDecl (. defaultModule.TopLevelDecls.Add(submodule); .)
| ClassDecl (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .)
| NewtypeDecl (. defaultModule.TopLevelDecls.Add(td); .)
| OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .)
| IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .)
| TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .)
| ClassMemberDecl
}
(. // find the default class in the default module, then append membersDefaultClass to its member list
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
defaultClass = topleveldecl as DefaultClassDecl;
if (defaultClass != null) {
defaultClass.Members.AddRange(membersDefaultClass);
break;
}
}
if (defaultClass == null) { // create the default class here, because it wasn't found
defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
defaultModule.TopLevelDecls.Add(defaultClass);
} .)
EOF
.
SubModuleDecl
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
Attributes attrs = null; IToken/*!*/ id;
TraitDecl/*!*/ trait;
List namedModuleDefaultClassMembers = new List();;
List idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
ModuleDecl sm;
submodule = null; // appease compiler
bool isAbstract = false;
bool opened = false;
.)
( [ "abstract" (. isAbstract = true; .) ]
"module"
{ Attribute[ }
NoUSIdent
[ "refines" QualifiedName ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
"{" (. module.BodyStartTok = t; .)
{ SubModuleDecl (. module.TopLevelDecls.Add(sm); .)
| ClassDecl (. module.TopLevelDecls.Add(c); .)
| TraitDecl (. module.TopLevelDecls.Add(trait); .)
| DatatypeDecl (. module.TopLevelDecls.Add(dt); .)
| NewtypeDecl (. module.TopLevelDecls.Add(td); .)
| OtherTypeDecl (. module.TopLevelDecls.Add(td); .)
| IteratorDecl (. module.TopLevelDecls.Add(iter); .)
| ClassMemberDecl
}
"}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent); .)
|
"import" ["opened" (.opened = true;.)]
NoUSIdent
[ "=" QualifiedName
(. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
| "as" QualifiedName ["default" QualifiedName ]
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
]
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
// (. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
// And in a version after that, don't allow the semi-colon at all.
]
(. if (submodule == null) {
idPath = new List();
idPath.Add(id);
submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
.)
)
.
QualifiedName<.out List ids.>
= (. IToken id; IToken idPrime; ids = new List(); .)
Ident (. ids.Add(id); .)
{ IdentOrDigitsSuffix (. ids.Add(id);
if (idPrime != null) { ids.Add(idPrime); }
.)
}
.
ClassDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
List/*!*/ traitId=null;
Attributes attrs = null;
List typeArgs = new List();
List members = new List();
IToken bodyStart;
.)
SYNC
"class"
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
["extends" QualifiedName]
"{" (. bodyStart = t; .)
{ ClassMemberDecl
}
"}"
(. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
TraitDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out trait) != null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List(); //traits should not support type parameters at the moment
List members = new List();
IToken bodyStart;
.)
SYNC
"trait"
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
"{" (. bodyStart = t; .)
{ ClassMemberDecl
}
"}"
(. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
trait.BodyStartTok = bodyStart;
trait.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; .)
}
( 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
bool co = false;
.)
SYNC
( "datatype"
| "codatatype" (. co = true; .)
)
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
"=" (. bodyStart = t; .)
DatatypeMemberDecl
{ "|" DatatypeMemberDecl }
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
// (. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
// And in a version after that, don't allow the semi-colon at all.
]
(. if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
dt = new IndDatatypeDecl(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][ }
NoUSIdent
[ 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.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute][ }
FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
OldSemi
.
NewtypeDecl
= (. IToken id, bvId;
Attributes attrs = null;
td = null;
Type baseType = null;
Expression wh;
.)
"newtype"
{ Attribute][ }
NoUSIdent
"="
( IF(IsIdentColonOrBar())
NoUSIdent
[ ":" Type ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .)
"|"
Expression (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
| Type (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
)
.
OtherTypeDecl
= (. IToken id;
Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
var typeArgs = new List();
td = null;
Type ty;
.)
"type"
{ Attribute][ }
NoUSIdent
( "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
[ GenericParameters ]
|
[ GenericParameters ]
[ "="
Type (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
]
) (. if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
.)
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
// (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
// And in a version after that, don't allow the semi-colon at all.
]
.
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
.
FIdentType
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
id = Token.NoToken;
.)
( WildIdent
| digits (. id = t; .)
)
":"
Type
.
IdentType
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
WildIdent
":"
Type
.
LocalIdentTypeOptional
= (. IToken id; Type ty; Type optType = null;
.)
WildIdent
[ ":" Type (. optType = ty; .)
]
(. var = new LocalVariable(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
IdentTypeOptional
= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);
IToken id; Type ty; Type optType = null;
.)
WildIdent
[ ":" 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; id = Token.NoToken; ty = new BoolType()/*dummy*/; 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
]
| digits (. id = t; name = id.val;.)
":"
Type
)
(. if (name != null) {
identName = name;
} else {
identName = "#" + anonymousIds++;
}
.)
.
/*------------------------------------------------------------------------*/
IteratorDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null);
IToken/*!*/ id;
Attributes attrs = null;
List/*!*/ typeArgs = new List();
List ins = new List();
List outs = new List();
List reads = new List();
List mod = new List();
List decreases = new List();
List req = new List();
List ens = new List();
List yieldReq = new List();
List yieldEns = new List();
List dec = new List();
Attributes readsAttrs = null;
Attributes modAttrs = null;
Attributes decrAttrs = null;
BlockStmt body = null;
IToken signatureEllipsis = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
"iterator"
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
[ ( "yields"
| "returns" (. SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); .)
)
Formals
]
| "..." (. signatureEllipsis = t; .)
)
{ IteratorSpec }
[ BlockStmt
]
(. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
new Specification(reads, readsAttrs),
new Specification(mod, modAttrs),
new Specification(decreases, decrAttrs),
req, ens, yieldReq, yieldEns,
body, attrs, signatureEllipsis);
iter.BodyStartTok = bodyStart;
iter.BodyEndTok = bodyEnd;
.)
.
/*------------------------------------------------------------------------*/
GenericParameters<.List/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
.)
"<"
NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
{ "," NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
">"
.
/*------------------------------------------------------------------------*/
MethodDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id = Token.NoToken;
bool hasName = false; IToken keywordToken;
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();
Attributes decAttrs = null;
Attributes modAttrs = null;
BlockStmt body = null;
bool isLemma = false;
bool isConstructor = false;
bool isCoLemma = false;
IToken signatureEllipsis = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
( "method"
| "lemma" (. isLemma = true; .)
| "colemma" (. isCoLemma = true; .)
| "comethod" (. isCoLemma = true;
errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
.)
| "constructor" (. if (allowConstructor) {
isConstructor = true;
} else {
SemErr(t, "constructors are allowed only in classes");
}
.)
) (. keywordToken = t; .)
(. if (isLemma) {
if (mmod.IsGhost) {
SemErr(t, "lemmas cannot be declared 'ghost' (they are automatically 'ghost')");
}
} else if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
}
if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
} else if (isCoLemma) {
if (mmod.IsGhost) {
SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')");
}
}
.)
{ Attribute][ }
[ NoUSIdent (. hasName = true; .)
]
(. if (!hasName) {
id = keywordToken;
if (!isConstructor) {
SemErr(la, "a method must be given a name (expecting identifier)");
}
}
.)
(
[ GenericParameters ]
Formals
[ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals
]
| "..." (. signatureEllipsis = t; .)
)
{ MethodSpec }
[ BlockStmt
]
(.
if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {
SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
}
IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
if (isConstructor) {
m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isCoLemma) {
m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isLemma) {
m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else {
m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
}
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); .)
}
] OldSemi
| [ "free" (. isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
.)
]
( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures"
{ IF(IsAttribute()) Attribute][ }
Expression OldSemi (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
)
| "decreases" { IF(IsAttribute()) Attribute][ } DecreasesList OldSemi
)
.
IteratorSpec<.List/*!*/ reads, List/*!*/ mod, List decreases,
List/*!*/ req, List/*!*/ ens,
List/*!*/ yieldReq, List/*!*/ yieldEns,
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.>
= (. Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
.)
SYNC
( "reads" { IF(IsAttribute()) Attribute][ }
[ FrameExpression (. reads.Add(fe); .)
{ "," FrameExpression (. reads.Add(fe); .)
}
] OldSemi
| "modifies" { IF(IsAttribute()) Attribute][ }
[ FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
] OldSemi
| [ "free" (. isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
.)
]
[ "yield" (. isYield = true; .)
]
( "requires" Expression OldSemi (. if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
} else {
req.Add(new MaybeFreeExpression(e, isFree));
}
.)
| "ensures" { IF(IsAttribute()) Attribute][ }
Expression OldSemi (. if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
.)
)
| "decreases" { IF(IsAttribute()) Attribute][ } DecreasesList OldSemi
)
.
Formals<.bool incoming, bool allowGhostKeyword, List formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; .)
"("
[
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 = null;
.)
( "bool" (. tok = t; .)
| "char" (. tok = t; ty = new CharType(); .)
| "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
| "real" (. tok = t; ty = new RealType(); .)
| "set" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("set type expects only one type argument");
}
ty = new SetType(gt.Count == 1 ? gt[0] : null);
.)
| "multiset" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("multiset type expects only one type argument");
}
ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);
.)
| "seq" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("seq type expects only one type argument");
}
ty = new SeqType(gt.Count == 1 ? gt[0] : null);
.)
| "string" (. tok = t; ty = new UserDefinedType(tok, tok.val, new List(), new List()); .)
| "map" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count == 0) {
ty = new MapType(null, null);
} else if (gt.Count != 2) {
SemErr("map type expects two type arguments");
ty = new MapType(gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);
} else {
ty = new MapType(gt[0], gt[1]);
}
.)
| "(" (. tok = t; gt = new List(); .)
[ Type (. gt.Add(ty); .)
{ "," Type (. gt.Add(ty); .)
}
]
")" (. if (gt.Count == 1) {
// just return the type 'ty'
} else {
// make sure the nullary tuple type exists
var dims = gt.Count;
var tmp = theBuiltIns.TupleType(tok, dims, true);
ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List());
}
.)
| ReferenceType
)
[ (. Type t2; .)
"->" (. tok = t; .)
Type
(. if (gt == null) {
gt = new List{ ty };
}
ty = new ArrowType(tok, gt, t2);
theBuiltIns.CreateArrowTypeDecl(gt.Count);
.)
]
.
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;
List path;
.)
( "object" (. tok = t; ty = new ObjectType(); .)
| arrayToken (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
ty = theBuiltIns.ArrayType(tok, dims, gt, true);
.)
| Ident (. gt = new List();
path = new List(); .)
{ (. path.Add(tok); .)
"." Ident
}
[ GenericInstantiation ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
)
.
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;
Expression body = null;
bool isPredicate = false; bool isCoPredicate = false;
bool isFunctionMethod = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
IToken signatureEllipsis = null;
bool missingOpenParen;
.)
/* ----- function ----- */
( "function"
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
":"
Type
| "..." (. signatureEllipsis = t; .)
)
/* ----- predicate ----- */
| "predicate" (. isPredicate = true; .)
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ] (. missingOpenParen = true; .)
[ Formals (. missingOpenParen = false; .)
] (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the predicate takes no additional arguments"); } .)
[ ":" (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
/* ----- copredicate ----- */
| "copredicate" (. isCoPredicate = true; .)
(. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ] (. missingOpenParen = true; .)
[ Formals (. missingOpenParen = false; .)
] (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less co-predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the co-predicate takes no additional arguments"); } .)
[ ":" (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
)
(. decreases = isCoPredicate ? null : new List(); .)
{ FunctionSpec }
[ FunctionBody
]
(. if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {
SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");
}
IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
if (isPredicate) {
f = new Predicate(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals,
reqs, reads, ens, new Specification(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);
} else if (isCoPredicate) {
f = new CoPredicate(tok, id.val, mmod.IsStatic, typeArgs, formals,
reqs, reads, ens, body, attrs, signatureEllipsis);
} else {
f = new Function(tok, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, formals, returnType,
reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis);
}
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
theBuiltIns.CreateArrowTypeDecl(formals.Count);
if (isCoPredicate) {
// also create an arrow type for the corresponding prefix predicate
theBuiltIns.CreateArrowTypeDecl(formals.Count);
}
.)
.
FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs));
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
(
SYNC
"requires" Expression OldSemi (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression (. reads.Add(fe); .)
}
] OldSemi
| "ensures" Expression OldSemi (. ens.Add(e); .)
| "decreases" (. if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
decreases = new List();
}
.)
DecreasesList OldSemi
)
.
LambdaSpec<.out Expression req, List reads.>
= (. Contract.Requires(reads != null);
Expression e; req = null; FrameExpression fe; .)
{ ( "requires" Expression
(. if (req == null) {
req = e;
} else {
req = new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, e);
}
.)
| "reads" PossiblyWildFrameExpression (. reads.Add(fe); .)
)
}
.
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(t, new WildcardExpr(t), null); .)
| FrameExpression
)
.
FrameExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
Expression/*!*/ e;
IToken/*!*/ id;
string fieldName = null; IToken feTok = null;
fe = null;
.)
(( Expression (. feTok = e.tok; .)
[ "`" Ident (. fieldName = id.val; feTok = id; .)
]
(. fe = new FrameExpression(feTok, e, fieldName); .)
)
|
( "`" Ident (. fieldName = id.val; .)
(. fe = new FrameExpression(id, new ImplicitThisExpr(id), 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, bodyEnd, 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 */
BlockStmt bs;
IToken bodyStart, bodyEnd;
int breakCount;
.)
SYNC
( BlockStmt (. s = bs; .)
| AssertStmt
| AssumeStmt
| PrintStmt
| UpdateStmt
| VarDeclStatement
| IfStmt
| WhileStmt
| MatchStmt
| ForallStmt
| CalcStmt
| ModifyStmt
| "label" (. x = t; .)
NoUSIdent ":"
OneStmt (. s.Labels = new LList]