diff options
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Dafny.atg | 48 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 38 | ||||
| -rw-r--r-- | Dafny/DafnyMain.ssc | 5 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 146 | ||||
| -rw-r--r-- | Dafny/Printer.ssc | 122 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 133 | ||||
| -rw-r--r-- | Dafny/SccGraph.ssc | 48 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 44 |
8 files changed, 366 insertions, 218 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 3ac46422..bd1e7d0f 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -19,7 +19,6 @@ COMPILER Dafny /*--------------------------------------------------------------------------*/
static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
-static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
@@ -58,37 +57,36 @@ private static Expression! ConvertToLocal(Expression! e) }
///<summary>
-/// Parses top level declarations from "filename" and appends them to "modules" and "classes".
+/// 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.
///</summary>
-public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {
if (filename == "stdin.dfy") {
BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
- return Parse(modules, classes);
+ return Parse(modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
- return Parse(modules, classes);
+ return Parse(modules);
}
}
}
///<summary>
-/// Parses top-level declarations and appends them to "classes" [sic].
+/// 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.
///</summary>
-public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {
+public static int Parse (List<ModuleDecl!>! modules) {
List<ModuleDecl!> oldModules = theModules;
- List<TopLevelDecl!> oldClasses = theClasses;
theModules = modules;
- theClasses = classes;
Parse();
theModules = oldModules;
- theClasses = oldClasses;
return Errors.count;
}
@@ -127,26 +125,32 @@ PRODUCTIONS Dafny
= (. ClassDecl! c; DatatypeDecl! dt;
- ModuleDecl m; Attributes attrs; Token! id; List<string!> theImports;
+ Attributes attrs; Token! id; List<string!> theImports;
+
+ List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
+ ModuleDecl module;
+ DefaultModuleDecl defaultModule = new DefaultModuleDecl();
.)
- { "module" (. attrs = null; theImports = new List<string!>(); .)
+ { "module" (. attrs = null; theImports = new List<string!>(); .)
{ Attribute<ref attrs> }
Ident<out id>
- [ "imports" Idents<theImports> ] (. m = new ModuleDecl(id, id.val, theImports, attrs);
- theModules.Add(m);
- .)
+ [ "imports" Idents<theImports> ] (. module = new ModuleDecl(id, id.val, theImports, attrs); .)
"{"
- { ClassDecl<m, out c> (. theClasses.Add(c); .)
- | DatatypeDecl<m, out dt> (. theClasses.Add(dt); .)
- }
+ { ClassDecl<module, out c> (. module.TopLevelDecls.Add(c); .)
+ | DatatypeDecl<module, out dt> (. module.TopLevelDecls.Add(dt); .)
+ } (. theModules.Add(module); .)
"}"
- | ClassDecl<null, out c> (. theClasses.Add(c); .)
- | DatatypeDecl<null, out dt> (. theClasses.Add(dt); .)
+ | ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
+ | DatatypeDecl<defaultModule, out dt> (. defaultModule.TopLevelDecls.Add(dt); .)
+ | ClassMemberDecl<membersDefaultClass>
}
+ (. defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
+ theModules.Add(defaultModule);
+ .)
EOF
.
-ClassDecl<ModuleDecl module, out ClassDecl! c>
+ClassDecl<ModuleDecl! module, out ClassDecl! c>
= (. Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
@@ -177,7 +181,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm> )
.
-DatatypeDecl<ModuleDecl module, out DatatypeDecl! dt>
+DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt>
= (. Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index 2e5bd893..9963ac2d 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -13,11 +13,9 @@ namespace Microsoft.Dafny public class Program {
public readonly string! Name;
public readonly List<ModuleDecl!>! Modules;
- public readonly List<TopLevelDecl!>! Classes;
- public Program(string! name, [Captured] List<ModuleDecl!>! modules, [Captured] List<TopLevelDecl!>! classes) {
+ public Program(string! name, [Captured] List<ModuleDecl!>! modules) {
Name = name;
Modules = modules;
- Classes = classes;
}
}
@@ -341,17 +339,31 @@ namespace Microsoft.Dafny public class ModuleDecl : Declaration {
public readonly List<string!>! Imports;
+ public readonly List<TopLevelDecl!>! TopLevelDecls = new List<TopLevelDecl!>(); // filled in by the parser; readonly after that
+ public readonly Graph<MemberDecl!>! CallGraph = new Graph<MemberDecl!>(); // filled in during resolution
public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {
Imports = imports;
base(tok, name, attributes);
}
+ public virtual bool IsDefaultModule {
+ get { return false; }
+ }
+ }
+
+ public class DefaultModuleDecl : ModuleDecl {
+ public DefaultModuleDecl() {
+ base(Token.NoToken, "$default", new List<string!>(), null);
+ }
+ public override bool IsDefaultModule {
+ get { return true; }
+ }
}
public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
- public readonly ModuleDecl Module;
+ public readonly ModuleDecl! Module;
public readonly List<TypeParameter!>! TypeArgs;
- public TopLevelDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, Attributes attributes) {
+ public TopLevelDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, Attributes attributes) {
Module = module;
TypeArgs = typeArgs;
base(tok, name, attributes);
@@ -361,16 +373,28 @@ namespace Microsoft.Dafny public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl!>! Members;
- public ClassDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
+ public ClassDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
Members = members;
base(tok, name, module, typeArgs, attributes);
}
+ public virtual bool IsDefaultClass {
+ get { return false; }
+ }
+ }
+
+ public class DefaultClassDecl : ClassDecl {
+ public DefaultClassDecl(DefaultModuleDecl! module, [Captured] List<MemberDecl!>! members) {
+ base(Token.NoToken, "$default", module, new List<TypeParameter!>(), members, null);
+ }
+ public override bool IsDefaultClass {
+ get { return true; }
+ }
}
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor!>! Ctors;
- public DatatypeDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
+ public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
Ctors = ctors;
base(tok, name, module, typeArgs, attributes);
}
diff --git a/Dafny/DafnyMain.ssc b/Dafny/DafnyMain.ssc index 36ca4191..a7d863fe 100644 --- a/Dafny/DafnyMain.ssc +++ b/Dafny/DafnyMain.ssc @@ -20,7 +20,6 @@ namespace Microsoft.Dafny { program = null;
Dafny.Errors.count = 0;
List<ModuleDecl!> modules = new List<ModuleDecl!>();
- List<TopLevelDecl!> classes = new List<TopLevelDecl!>();
foreach (string! dafnyFileName in fileNames){
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
@@ -33,7 +32,7 @@ namespace Microsoft.Dafny { int errorCount;
try
{
- errorCount = Dafny.Parser.Parse(dafnyFileName, modules, classes);
+ errorCount = Dafny.Parser.Parse(dafnyFileName, modules);
if (errorCount != 0)
{
return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);
@@ -45,7 +44,7 @@ namespace Microsoft.Dafny { }
}
- program = new Program(programName, modules, classes);
+ program = new Program(programName, modules);
if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {
string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index b76182e4..b2ec727f 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -17,7 +17,6 @@ public class Parser { static int errDist = minErrDist;
static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
-static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
@@ -56,37 +55,36 @@ private static Expression! ConvertToLocal(Expression! e) }
///<summary>
-/// Parses top level declarations from "filename" and appends them to "modules" and "classes".
+/// 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.
///</summary>
-public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {
if (filename == "stdin.dfy") {
BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
- return Parse(modules, classes);
+ return Parse(modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
- return Parse(modules, classes);
+ return Parse(modules);
}
}
}
///<summary>
-/// Parses top-level declarations and appends them to "classes" [sic].
+/// 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.
///</summary>
-public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {
+public static int Parse (List<ModuleDecl!>! modules) {
List<ModuleDecl!> oldModules = theModules;
- List<TopLevelDecl!> oldClasses = theClasses;
theModules = modules;
- theClasses = classes;
Parse();
theModules = oldModules;
- theClasses = oldClasses;
return Errors.count;
}
@@ -150,9 +148,12 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe static void Dafny() {
ClassDecl! c; DatatypeDecl! dt;
- ModuleDecl m; Attributes attrs; Token! id; List<string!> theImports;
+ Attributes attrs; Token! id; List<string!> theImports;
+ List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
+ ModuleDecl module;
+ DefaultModuleDecl defaultModule = new DefaultModuleDecl();
- while (t.kind == 4 || t.kind == 8 || t.kind == 12) {
+ while (StartOf(1)) {
if (t.kind == 4) {
Get();
attrs = null; theImports = new List<string!>();
@@ -164,28 +165,32 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe Get();
Idents(theImports);
}
- m = new ModuleDecl(id, id.val, theImports, attrs);
- theModules.Add(m);
-
+ module = new ModuleDecl(id, id.val, theImports, attrs);
Expect(6);
while (t.kind == 8 || t.kind == 12) {
if (t.kind == 8) {
- ClassDecl(m, out c);
- theClasses.Add(c);
+ ClassDecl(module, out c);
+ module.TopLevelDecls.Add(c);
} else {
- DatatypeDecl(m, out dt);
- theClasses.Add(dt);
+ DatatypeDecl(module, out dt);
+ module.TopLevelDecls.Add(dt);
}
}
+ theModules.Add(module);
Expect(7);
} else if (t.kind == 8) {
- ClassDecl(null, out c);
- theClasses.Add(c);
+ ClassDecl(defaultModule, out c);
+ defaultModule.TopLevelDecls.Add(c);
+ } else if (t.kind == 12) {
+ DatatypeDecl(defaultModule, out dt);
+ defaultModule.TopLevelDecls.Add(dt);
} else {
- DatatypeDecl(null, out dt);
- theClasses.Add(dt);
+ ClassMemberDecl(membersDefaultClass);
}
}
+ defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
+ theModules.Add(defaultModule);
+
Expect(0);
}
@@ -211,7 +216,7 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe }
}
- static void ClassDecl(ModuleDecl module, out ClassDecl! c) {
+ static void ClassDecl(ModuleDecl! module, out ClassDecl! c) {
Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
@@ -226,14 +231,14 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe GenericParameters(typeArgs);
}
Expect(6);
- while (StartOf(1)) {
+ while (StartOf(2)) {
ClassMemberDecl(members);
}
Expect(7);
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
}
- static void DatatypeDecl(ModuleDecl module, out DatatypeDecl! dt) {
+ static void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {
Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
@@ -255,19 +260,6 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
- static void GenericParameters(List<TypeParameter!>! typeArgs) {
- Token! id;
- Expect(17);
- Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
- while (t.kind == 15) {
- Get();
- Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
- }
- Expect(18);
- }
-
static void ClassMemberDecl(List<MemberDecl!>! mm) {
Method! m;
Function! f;
@@ -296,6 +288,19 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe } else Error(97);
}
+ static void GenericParameters(List<TypeParameter!>! typeArgs) {
+ Token! id;
+ Expect(17);
+ Ident(out id);
+ typeArgs.Add(new TypeParameter(id, id.val));
+ while (t.kind == 15) {
+ Get();
+ Ident(out id);
+ typeArgs.Add(new TypeParameter(id, id.val));
+ }
+ Expect(18);
+ }
+
static void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
Attributes attrs = null;
Token! id; Type! ty;
@@ -352,7 +357,7 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
FunctionSpec(reqs, reads, decreases);
}
- } else if (StartOf(2)) {
+ } else if (StartOf(3)) {
while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
FunctionSpec(reqs, reads, decreases);
}
@@ -394,11 +399,11 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe }
if (t.kind == 13) {
Get();
- while (StartOf(3)) {
+ while (StartOf(4)) {
MethodSpec(req, mod, ens, dec);
}
- } else if (StartOf(4)) {
- while (StartOf(3)) {
+ } else if (StartOf(5)) {
+ while (StartOf(4)) {
MethodSpec(req, mod, ens, dec);
}
BlockStmt(out bb);
@@ -435,7 +440,7 @@ public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classe static void FormalsOptionalIds(List<Formal!>! formals) {
Token! id; Type! ty; string! name;
Expect(26);
- if (StartOf(5)) {
+ if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty);
formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
while (t.kind == 15) {
@@ -555,7 +560,7 @@ List<Expression!>! decreases) { if (t.kind == 21) {
Get();
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expression(out e);
mod.Add(e);
while (t.kind == 15) {
@@ -596,7 +601,7 @@ List<Expression!>! decreases) { parseVarScope.PushMarker();
Expect(6);
x = token;
- while (StartOf(7)) {
+ while (StartOf(8)) {
Stmt(body);
}
Expect(7);
@@ -617,7 +622,7 @@ List<Expression!>! decreases) { Expect(46);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (StartOf(8)) {
+ } else if (StartOf(9)) {
EquivExpression(out e);
} else Error(103);
}
@@ -672,7 +677,7 @@ List<Expression!>! decreases) { reqs.Add(e);
} else if (t.kind == 34) {
Get();
- if (StartOf(9)) {
+ if (StartOf(10)) {
PossiblyWildExpressions(reads);
}
Expect(13);
@@ -688,7 +693,7 @@ List<Expression!>! decreases) { Expect(6);
if (t.kind == 36) {
MatchExpression(out e);
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out e);
} else Error(106);
Expect(7);
@@ -710,7 +715,7 @@ List<Expression!>! decreases) { if (t.kind == 35) {
Get();
e = new WildcardExpr(token);
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out e);
} else Error(107);
}
@@ -773,7 +778,7 @@ List<Expression!>! decreases) { BlockStmt(out s);
ss.Add(s);
}
- if (StartOf(10)) {
+ if (StartOf(11)) {
OneStmt(out s);
ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
@@ -1079,7 +1084,7 @@ List<Expression!>! decreases) { if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
}
}
- if (StartOf(11)) {
+ if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
} else if (t.kind == 44) {
@@ -1108,7 +1113,7 @@ List<Expression!>! decreases) { Get();
ReferenceType(out x, out tt);
ty = tt;
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out ee);
e = ee;
} else Error(113);
@@ -1160,7 +1165,7 @@ List<Expression!>! decreases) { if (t.kind == 35) {
Get();
e = null;
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out ee);
e = ee;
} else Error(115);
@@ -1213,7 +1218,7 @@ List<Expression!>! decreases) { static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
- if (StartOf(12)) {
+ if (StartOf(13)) {
if (t.kind == 60 || t.kind == 61) {
AndOp();
x = token;
@@ -1251,7 +1256,7 @@ List<Expression!>! decreases) { static void RelationalExpression(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Term(out e0);
- if (StartOf(13)) {
+ if (StartOf(14)) {
RelOp(out x, out op);
Term(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1384,9 +1389,9 @@ List<Expression!>! decreases) { x = token;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
- } else if (StartOf(11)) {
+ } else if (StartOf(12)) {
SelectExpression(out e);
- } else if (StartOf(14)) {
+ } else if (StartOf(15)) {
ConstAtomExpression(out e);
} else Error(123);
}
@@ -1447,7 +1452,7 @@ List<Expression!>! decreases) { elements = new List<Expression!>();
if (t.kind == 26) {
Get();
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expressions(elements);
}
Expect(27);
@@ -1475,7 +1480,7 @@ List<Expression!>! decreases) { case 6: {
Get();
x = token; elements = new List<Expression!>();
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
@@ -1485,7 +1490,7 @@ List<Expression!>! decreases) { case 85: {
Get();
x = token; elements = new List<Expression!>();
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
@@ -1513,7 +1518,7 @@ List<Expression!>! decreases) { if (t.kind == 26) {
Get();
args = new List<Expression!>();
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expressions(args);
}
Expect(27);
@@ -1543,9 +1548,9 @@ List<Expression!>! decreases) { e = new OldExpr(x, e);
} else if (t.kind == 26) {
Get();
- if (StartOf(15)) {
+ if (StartOf(16)) {
QuantifierGuts(out e);
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out e);
} else Error(127);
Expect(27);
@@ -1563,7 +1568,7 @@ List<Expression!>! decreases) { if (t.kind == 26) {
Get();
args = new List<Expression!>(); func = true;
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expressions(args);
}
Expect(27);
@@ -1573,14 +1578,14 @@ List<Expression!>! decreases) { } else if (t.kind == 85) {
Get();
x = token;
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expression(out ee);
e0 = ee;
if (t.kind == 42 || t.kind == 87) {
if (t.kind == 87) {
Get();
anyDots = true;
- if (StartOf(6)) {
+ if (StartOf(7)) {
Expression(out ee);
e1 = ee;
}
@@ -1672,7 +1677,7 @@ List<Expression!>! decreases) { Expect(6);
if (t.kind == 16) {
AttributeBody(ref attrs);
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
@@ -1696,7 +1701,7 @@ List<Expression!>! decreases) { Expect(16);
Expect(1);
aName = token.val;
- if (StartOf(16)) {
+ if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (t.kind == 15) {
@@ -1713,7 +1718,7 @@ List<Expression!>! decreases) { if (t.kind == 3) {
Get();
arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
- } else if (StartOf(6)) {
+ } else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
} else Error(136);
@@ -1880,6 +1885,7 @@ List<Expression!>! decreases) { static bool[,]! set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc index 88e9d5dc..1a242308 100644 --- a/Dafny/Printer.ssc +++ b/Dafny/Printer.ssc @@ -23,40 +23,51 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);
}
wr.WriteLine("// {0}", prog.Name);
- ModuleDecl currentModule = null;
- int indent = 0;
- foreach (TopLevelDecl d in prog.Classes) {
- if (d.Module != currentModule) {
- if (currentModule != null) {
- wr.WriteLine("}");
+ foreach (ModuleDecl module in prog.Modules) {
+ wr.WriteLine();
+ if (module.IsDefaultModule) {
+ PrintTopLevelDecls(module.TopLevelDecls, 0);
+ } else {
+ wr.Write("module ");
+ PrintAttributes(module.Attributes);
+ wr.Write("{0} ", module.Name);
+ if (module.Imports.Count != 0) {
+ string sep = "imports ";
+ foreach (string imp in module.Imports) {
+ wr.Write("{0}{1}", sep, imp);
+ sep = ", ";
+ }
}
- if (d.Module == null) {
- indent = 0;
+ if (module.TopLevelDecls.Count == 0) {
+ wr.WriteLine(" { }");
} else {
- wr.Write("module ");
- PrintAttributes(d.Module.Attributes);
- wr.Write("{0}", d.Module.Name);
- if (d.Module.Imports.Count != 0) {
- string sep = "imports ";
- foreach (string imp in d.Module.Imports) {
- wr.Write("{0}{1}", sep, imp);
- sep = ", ";
- }
- }
- wr.WriteLine("{");
- indent = IndentAmount;
+ wr.WriteLine(" {");
+ PrintTopLevelDecls(module.TopLevelDecls, IndentAmount);
+ wr.WriteLine("}");
}
}
- wr.WriteLine();
- if (d is ClassDecl) {
- PrintClass((ClassDecl)d, indent);
- } else {
+ }
+ }
+
+ public void PrintTopLevelDecls(List<TopLevelDecl!>! classes, int indent) {
+ int i = 0;
+ foreach (TopLevelDecl d in classes) {
+ if (d is DatatypeDecl) {
+ if (i++ != 0) { wr.WriteLine(); }
PrintDatatype((DatatypeDecl)d, indent);
+ } else {
+ ClassDecl cl = (ClassDecl)d;
+ if (!cl.IsDefaultClass) {
+ if (i++ != 0) { wr.WriteLine(); }
+ PrintClass(cl, indent);
+ } else if (cl.Members.Count == 0) {
+ // print nothing
+ } else {
+ if (i++ != 0) { wr.WriteLine(); }
+ PrintClass_Members(cl, indent);
+ }
}
}
- if (currentModule != null) {
- wr.WriteLine("}");
- }
}
public void PrintClass(ClassDecl! c, int indent) {
@@ -65,27 +76,33 @@ namespace Microsoft.Dafny { if (c.Members.Count == 0) {
wr.WriteLine(" { }");
} else {
- int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
wr.WriteLine(" {");
- int ind = indent + IndentAmount;
- foreach (MemberDecl m in c.Members) {
- if (m is Method) {
- if (state != 0) { wr.WriteLine(); }
- PrintMethod((Method)m, ind);
- state = 2;
- } else if (m is Field) {
- if (state == 2) { wr.WriteLine(); }
- PrintField((Field)m, ind);
- state = 1;
- } else if (m is Function) {
- if (state != 0) { wr.WriteLine(); }
- PrintFunction((Function)m, ind);
- state = 2;
- } else {
- assert false; // unexpected member
- }
+ PrintClass_Members(c, indent + IndentAmount);
+ Indent(indent);
+ wr.WriteLine("}");
+ }
+ }
+
+ public void PrintClass_Members(ClassDecl! c, int indent)
+ requires c.Members.Count != 0;
+ {
+ int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
+ foreach (MemberDecl m in c.Members) {
+ if (m is Method) {
+ if (state != 0) { wr.WriteLine(); }
+ PrintMethod((Method)m, indent);
+ state = 2;
+ } else if (m is Field) {
+ if (state == 2) { wr.WriteLine(); }
+ PrintField((Field)m, indent);
+ state = 1;
+ } else if (m is Function) {
+ if (state != 0) { wr.WriteLine(); }
+ PrintFunction((Function)m, indent);
+ state = 2;
+ } else {
+ assert false; // unexpected member
}
- Indent(indent); wr.WriteLine("}");
}
}
@@ -163,11 +180,8 @@ namespace Microsoft.Dafny { PrintFormals(f.Formals);
wr.Write(": ");
PrintType(f.ResultType);
- if (f.Body == null) {
- wr.WriteLine(";");
- } else {
- wr.WriteLine();
- }
+ wr.WriteLine(f.Body == null ? ";" : "");
+
int ind = indent + IndentAmount;
PrintSpec("requires", f.Req, ind);
PrintSpecLine("reads", f.Reads, ind);
@@ -220,7 +234,7 @@ namespace Microsoft.Dafny { }
PrintFormals(method.Outs);
}
- wr.WriteLine(method.Body == null ? ";" : ":");
+ wr.WriteLine(method.Body == null ? ";" : "");
int ind = indent + IndentAmount;
PrintSpec("requires", method.Req, ind);
@@ -230,7 +244,7 @@ namespace Microsoft.Dafny { if (method.Body != null) {
Indent(indent);
- PrintStatement(method.Body, ind);
+ PrintStatement(method.Body, indent);
wr.WriteLine();
}
}
@@ -309,7 +323,7 @@ namespace Microsoft.Dafny { } else if (stmt is UseStmt) {
wr.Write("use ");
- PrintExpression(((AssertStmt)stmt).Expr);
+ PrintExpression(((UseStmt)stmt).Expr);
wr.Write(";");
} else if (stmt is LabelStmt) {
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 235c9036..b3d5b2c3 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -48,17 +48,20 @@ namespace Microsoft.Dafny { modules.Add(m.Name, m);
}
}
- // resolve imports
+ // resolve imports and register top-level declarations
foreach (ModuleDecl m in prog.Modules) {
foreach (string imp in m.Imports) {
ModuleDecl other;
- if (modules.TryGetValue(imp, out other)) {
+ if (!modules.TryGetValue(imp, out other)) {
+ Error(m, "module {0} named among imports does not exist", imp);
+ } else if (other == m) {
+ Error(m, "module must not import itself: {0}", imp);
+ } else {
assert other != null; // follows from postcondition of TryGetValue
importGraph.AddEdge(m, other);
- } else {
- Error(m, "module {0} named among imports does not exist", imp);
}
}
+ RegisterTopLevelDecls(m.TopLevelDecls);
}
// check for cycles in the import graph
List<ModuleDecl!> cycle = importGraph.TryFindCycle();
@@ -71,10 +74,18 @@ namespace Microsoft.Dafny { }
Error(cycle[0], "import graph contains a cycle: {0}", cy);
}
-
- // Done with modules; now, do classes and datatypes
-
- foreach (TopLevelDecl d in prog.Classes) {
+ // resolve top-level declarations
+ Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();
+ foreach (ModuleDecl m in prog.Modules) {
+ ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
+ }
+ foreach (ModuleDecl m in prog.Modules) {
+ ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ }
+ }
+
+ public void RegisterTopLevelDecls(List<TopLevelDecl!>! declarations) {
+ foreach (TopLevelDecl d in declarations) {
// register the class/datatype name
if (classes.ContainsKey(d.Name)) {
Error(d, "Duplicate name of top-level declaration: {0}", d.Name);
@@ -112,10 +123,10 @@ namespace Microsoft.Dafny { }
}
}
+ }
- // resolve each class
- Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();
- foreach (TopLevelDecl d in prog.Classes) {
+ public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl!>! declarations, Graph<DatatypeDecl!>! datatypeDependencies) {
+ foreach (TopLevelDecl d in declarations) {
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, true, d);
if (d is ClassDecl) {
@@ -125,8 +136,10 @@ namespace Microsoft.Dafny { }
allTypeParameters.PopMarker();
}
-
- foreach (TopLevelDecl d in prog.Classes) {
+ }
+
+ public void ResolveTopLevelDecls_Meat(List<TopLevelDecl!>! declarations, Graph<DatatypeDecl!>! datatypeDependencies) {
+ foreach (TopLevelDecl d in declarations) {
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
if (d is ClassDecl) {
@@ -143,6 +156,7 @@ namespace Microsoft.Dafny { }
ClassDecl currentClass;
+ Function currentFunction;
readonly Scope<TypeParameter>! allTypeParameters = new Scope<TypeParameter>();
readonly Scope<IVariable>! scope = new Scope<IVariable>();
readonly Scope<Statement>! labeledStatements = new Scope<Statement>();
@@ -358,8 +372,12 @@ namespace Microsoft.Dafny { /// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
- void ResolveFunction(Function! f) {
+ void ResolveFunction(Function! f)
+ requires currentFunction == null;
+ ensures currentFunction == null;
+ {
scope.PushMarker();
+ currentFunction = f;
if (f.IsStatic) {
scope.AllowInstance = false;
}
@@ -399,6 +417,7 @@ namespace Microsoft.Dafny { Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
}
+ currentFunction = null;
scope.PopMarker();
}
@@ -481,7 +500,7 @@ namespace Microsoft.Dafny { // Resolve body
if (m.Body != null) {
- ResolveStatement(m.Body, m.IsGhost);
+ ResolveStatement(m.Body, m.IsGhost, m);
}
scope.PopMarker();
@@ -758,7 +777,7 @@ namespace Microsoft.Dafny { }
}
- public void ResolveStatement(Statement! stmt, bool specContextOnly)
+ public void ResolveStatement(Statement! stmt, bool specContextOnly, Method! method)
requires !(stmt is LabelStmt); // these should be handled inside lists of statements
{
if (stmt is UseStmt) {
@@ -904,15 +923,15 @@ namespace Microsoft.Dafny { // resolve the method name
UserDefinedType ctype;
MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype);
- Method method = null;
+ Method callee = null;
if (member == null) {
// error has already been reported by ResolveMember
} else if (!(member is Method)) {
Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name);
} else {
- method = (Method)member;
- s.Method = method;
- if (specContextOnly && !method.IsGhost) {
+ callee = (Method)member;
+ s.Method = callee;
+ if (specContextOnly && !callee.IsGhost) {
Error(s, "only ghost methods can be called from this context");
}
}
@@ -920,10 +939,10 @@ namespace Microsoft.Dafny { // resolve any local variables declared here
foreach (AutoVarDecl local in s.NewVars) {
// first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost
- if (method != null && local.Index < method.Outs.Count && method.Outs[local.Index].IsGhost) {
+ if (callee != null && local.Index < callee.Outs.Count && callee.Outs[local.Index].IsGhost) {
local.MakeGhost();
}
- ResolveStatement(local, specContextOnly);
+ ResolveStatement(local, specContextOnly, method);
}
// resolve left-hand side
@@ -939,20 +958,20 @@ namespace Microsoft.Dafny { // resolve arguments
int j = 0;
foreach (Expression e in s.Args) {
- bool allowGhost = method == null || method.Ins.Count <= j || method.Ins[j].IsGhost;
+ bool allowGhost = callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
ResolveExpression(e, true, allowGhost);
j++;
}
- if (method == null) {
+ if (callee == null) {
// error has been reported above
- } else if (method.Ins.Count != s.Args.Count) {
- Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count);
- } else if (method.Outs.Count != s.Lhs.Count) {
- Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count);
+ } else if (callee.Ins.Count != s.Args.Count) {
+ Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, callee.Ins.Count);
+ } else if (callee.Outs.Count != s.Lhs.Count) {
+ Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, callee.Outs.Count);
} else {
assert ctype != null; // follows from postcondition of ResolveMember above
- if (!scope.AllowInstance && !method.IsStatic && s.Receiver is ThisExpr) {
+ if (!scope.AllowInstance && !callee.IsStatic && s.Receiver is ThisExpr) {
// The call really needs an instance, but that instance is given as 'this', which is not
// available in this context. For more details, see comment in the resolution of a
// FunctionCallExpr.
@@ -963,25 +982,41 @@ namespace Microsoft.Dafny { for (int i = 0; i < ctype.TypeArgs.Count; i++) {
subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
- foreach (TypeParameter p in method.TypeArgs) {
+ foreach (TypeParameter p in callee.TypeArgs) {
subst.Add(p, new ParamTypeProxy(p));
}
// type check the arguments
- for (int i = 0; i < method.Ins.Count; i++) {
- Type st = SubstType(method.Ins[i].Type, subst);
+ for (int i = 0; i < callee.Ins.Count; i++) {
+ Type st = SubstType(callee.Ins[i].Type, subst);
if (!UnifyTypes((!)s.Args[i].Type, st)) {
Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
}
}
- for (int i = 0; i < method.Outs.Count; i++) {
- Type st = SubstType(method.Outs[i].Type, subst);
+ for (int i = 0; i < callee.Outs.Count; i++) {
+ Type st = SubstType(callee.Outs[i].Type, subst);
IdentifierExpr lhs = s.Lhs[i];
if (!UnifyTypes((!)lhs.Type, st)) {
Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
- } else if (!specContextOnly && !((!)lhs.Var).IsGhost && method.Outs[i].IsGhost) {
+ } else if (!specContextOnly && !((!)lhs.Var).IsGhost && callee.Outs[i].IsGhost) {
Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
}
}
+
+ // Resolution termination check
+ if (method.EnclosingClass != null && callee.EnclosingClass != null) {
+ ModuleDecl callerModule = method.EnclosingClass.Module;
+ ModuleDecl calleeModule = callee.EnclosingClass.Module;
+ if (callerModule == calleeModule) {
+ // intra-module call; this is allowed; add edge in module's call graph
+ callerModule.CallGraph.AddEdge(method, callee);
+ } else if (calleeModule.IsDefaultModule) {
+ // all is fine: everything implicitly imports the default module
+ } else if (importGraph.Reaches(callerModule, calleeModule)) {
+ // all is fine: the callee is downstream of the caller
+ } else {
+ Error(s, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name);
+ }
+ }
}
} else if (stmt is BlockStmt) {
@@ -995,7 +1030,7 @@ namespace Microsoft.Dafny { assert b; // since we just pushed a marker, we expect the Push to succeed
labelsToPop++;
} else {
- ResolveStatement(ss, specContextOnly);
+ ResolveStatement(ss, specContextOnly, method);
for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
}
}
@@ -1017,9 +1052,9 @@ namespace Microsoft.Dafny { branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
}
}
- ResolveStatement(s.Thn, branchesAreSpecOnly);
+ ResolveStatement(s.Thn, branchesAreSpecOnly, method);
if (s.Els != null) {
- ResolveStatement(s.Els, branchesAreSpecOnly);
+ ResolveStatement(s.Els, branchesAreSpecOnly, method);
}
} else if (stmt is WhileStmt) {
@@ -1048,7 +1083,7 @@ namespace Microsoft.Dafny { ResolveExpression(e, true, true);
// any type is fine
}
- ResolveStatement(s.Body, bodyIsSpecOnly);
+ ResolveStatement(s.Body, bodyIsSpecOnly, method);
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
@@ -1073,12 +1108,12 @@ namespace Microsoft.Dafny { bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;
foreach (PredicateStmt ss in s.BodyPrefix) {
- ResolveStatement(ss, specContextOnly);
+ ResolveStatement(ss, specContextOnly, method);
}
bool specOnly = specContextOnly ||
(successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
- ResolveStatement(s.BodyAssign, specOnly);
+ ResolveStatement(s.BodyAssign, specOnly, method);
// check for correct usage of BoundVar in LHS and RHS of this assignment
FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;
@@ -1429,6 +1464,22 @@ namespace Microsoft.Dafny { }
expr.Type = SubstType(function.ResultType, subst);
}
+
+ // Resolution termination check
+ if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {
+ ModuleDecl callerModule = currentFunction.EnclosingClass.Module;
+ ModuleDecl calleeModule = function.EnclosingClass.Module;
+ if (callerModule == calleeModule) {
+ // intra-module call; this is allowed; add edge in module's call graph
+ callerModule.CallGraph.AddEdge(currentFunction, function);
+ } else if (calleeModule.IsDefaultModule) {
+ // all is fine: everything implicitly imports the default module
+ } else if (importGraph.Reaches(callerModule, calleeModule)) {
+ // all is fine: the callee is downstream of the caller
+ } else {
+ Error(expr, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name);
+ }
+ }
}
} else if (expr is OldExpr) {
diff --git a/Dafny/SccGraph.ssc b/Dafny/SccGraph.ssc index e508d129..6a7983a6 100644 --- a/Dafny/SccGraph.ssc +++ b/Dafny/SccGraph.ssc @@ -10,12 +10,13 @@ namespace Microsoft.Dafny { public readonly List<Vertex!>! Successors = new List<Vertex!>();
public Vertex SccRepresentative; // null if not computed or if the vertex represents itself
public List<Vertex!> SccMembers; // non-null only for the representative of the SCC
- public Dictionary<Vertex,object> downwardClosure; // irrefexive, transitive closure; null if not computed
// the following field is used during the computation of SCCs and of reachability
public VisitedStatus Visited;
// the following fields are used during the computation of SCCs:
public int DfNumber;
public int LowLink;
+ // the following field is used during a Reaches computation
+ public int Gen; // generation <= Gen means this vertex has been visited in the current generation
public Vertex(Node n) {
N = n;
@@ -26,6 +27,7 @@ namespace Microsoft.Dafny { }
Dictionary<Node, Vertex!>! vertices = new Dictionary<Node, Vertex!>();
bool sccComputed = false;
+ int generation = 0;
public Graph()
{
@@ -42,14 +44,25 @@ namespace Microsoft.Dafny { /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.
/// </summary>
Vertex! GetVertex(Node n) {
+ Vertex v = FindVertex(n);
+ if (v == null) {
+ v = new Vertex(n);
+ vertices.Add(n, v);
+ }
+ return v;
+ }
+
+ /// <summary>
+ /// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null.
+ /// </summary>
+ Vertex FindVertex(Node n) {
Vertex v;
if (vertices.TryGetValue(n, out v)) {
assert v != null; // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!)
+ return v;
} else {
- v = new Vertex(n);
- vertices.Add(n, v);
+ return null;
}
- return v;
}
/// <summary>
@@ -234,5 +247,32 @@ namespace Microsoft.Dafny { v.Visited = VisitedStatus.Visited; // there are no cycles from here on
return null;
}
+
+ /// <summary>
+ /// Returns whether or not 'source' reaches 'sink' in the graph.
+ /// 'source' and 'sink' need not be in the graph; if neither is, the return value
+ /// is source==sink.
+ /// </summary>
+ public bool Reaches(Node source, Node sink) {
+ Vertex a = FindVertex(source);
+ Vertex b = FindVertex(sink);
+ if (a == null || b == null) {
+ return source.Equals(sink);
+ }
+ generation++;
+ return ReachSearch(a, b);
+ }
+
+ bool ReachSearch(Vertex! source, Vertex! sink) {
+ if (source == sink) {
+ return true;
+ } else if (source.Gen == generation) {
+ // already visited
+ return false;
+ } else {
+ source.Gen = generation;
+ return exists{Vertex succ in source.Successors; ReachSearch(succ, sink)};
+ }
+ }
}
}
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index fbf9c361..e6bed1b1 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -260,11 +260,13 @@ namespace Microsoft.Dafny { // already been printed, so just return an empty program here (which is non-null)
return new Bpl.Program();
}
- foreach (TopLevelDecl d in program.Classes) {
- if (d is DatatypeDecl) {
- AddDatatype((DatatypeDecl)d);
- } else {
- AddClassMembers((ClassDecl)d);
+ foreach (ModuleDecl m in program.Modules) {
+ foreach (TopLevelDecl d in m.TopLevelDecls) {
+ if (d is DatatypeDecl) {
+ AddDatatype((DatatypeDecl)d);
+ } else {
+ AddClassMembers((ClassDecl)d);
+ }
}
}
return sink;
@@ -1139,7 +1141,7 @@ namespace Microsoft.Dafny { void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.VariableSeq! locals, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
requires predef != null;
{
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr) {
+ if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
// always allowed
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -1218,16 +1220,19 @@ namespace Microsoft.Dafny { builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));
// finally, check that the decreases measure goes down
- if (((!)e.Function.EnclosingClass).Module == ((!)func.EnclosingClass).Module) {
- List<Expression!> contextDecreases = func.Decreases;
- if (contextDecreases.Count == 0) {
- contextDecreases = func.Reads; // use its reads clause instead
- }
- List<Expression!> calleeDecreases = e.Function.Decreases;
- if (calleeDecreases.Count == 0) {
- calleeDecreases = e.Function.Reads; // use its reads clause instead
+ ModuleDecl module = ((!)e.Function.EnclosingClass).Module;
+ if (module == ((!)func.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(func)) {
+ List<Expression!> contextDecreases = func.Decreases;
+ if (contextDecreases.Count == 0) {
+ contextDecreases = func.Reads; // use its reads clause instead
+ }
+ List<Expression!> calleeDecreases = e.Function.Decreases;
+ if (calleeDecreases.Count == 0) {
+ calleeDecreases = e.Function.Reads; // use its reads clause instead
+ }
+ CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
- CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
}
} else if (expr is DatatypeValue) {
@@ -1847,8 +1852,13 @@ namespace Microsoft.Dafny { // Check termination
if (exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
// omit termination checking for calls in this context
- } else if (((!)currentMethod.EnclosingClass).Module == ((!)s.Method.EnclosingClass).Module) {
- CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
+ } else {
+ ModuleDecl module = ((!)s.Method.EnclosingClass).Module;
+ if (module == ((!)currentMethod.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
+ CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
+ }
+ }
}
// Make the call
|