summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-03-16 08:53:22 +0000
committerGravatar rustanleino <unknown>2010-03-16 08:53:22 +0000
commit6766d9d3d836ca3d435ae87c4b3fe71a1741fcf4 (patch)
treefc1103759db2b9b5fe551564f050b7705f143fc0
parentcc63641cd0211b2f585330c9d65208665671991b (diff)
Dafny:
* Added modules with imports. These can be used to deal with termination checks without going into method/function implementations. Imports must be acyclic. * Added a default module. It contains all classes/datatypes defined outside the lexical scope of any other module. * Added a default class. It contains all class members defined outside the lexical scope of any module and class. This means that one can write small Dafny programs without any mention of a "class"! * Revised scheme for termination metrics. Inter-module calls are allowed iff they follow the import relation. Intra-module calls where the callee is in another strongly connected component of the call graph are always allowed. Intra-module calls in the same strongly connected component are verified to terminate via decreases clauses. * Removed previous hack that allowed methods with no decreases clauses not to be subjected to termination checking. * Removed or simplified decreases clauses in test suite, where possible. * Fixed error in Test/VSI-Benchmarks/b1.dfy
Diffstat
-rw-r--r--Dafny/Dafny.atg48
-rw-r--r--Dafny/DafnyAst.ssc38
-rw-r--r--Dafny/DafnyMain.ssc5
-rw-r--r--Dafny/Parser.ssc146
-rw-r--r--Dafny/Printer.ssc122
-rw-r--r--Dafny/Resolver.ssc133
-rw-r--r--Dafny/SccGraph.ssc48
-rw-r--r--Dafny/Translator.ssc44
-rw-r--r--Test/VSI-Benchmarks/b1.dfy5
-rw-r--r--Test/dafny0/Answer38
-rw-r--r--Test/dafny0/BinaryTree.dfy4
-rw-r--r--Test/dafny0/Modules0.dfy72
-rw-r--r--Test/dafny0/Modules1.dfy62
-rw-r--r--Test/dafny0/SchorrWaite.dfy6
-rw-r--r--Test/dafny0/SmallTests.dfy2
-rw-r--r--Test/dafny0/Use.dfy8
-rw-r--r--Test/dafny0/runtest.bat2
17 files changed, 540 insertions, 243 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
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index ba293008..70522aaf 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -35,8 +35,11 @@ class Benchmark1 {
method Mul(x: int, y: int) returns (r: int)
ensures r == x*y;
+ decreases x < 0, x;
{
- if (x < 0) {
+ if (x == 0) {
+ r := 0;
+ } else if (x < 0) {
call r := Mul(-x, y);
r := -r;
} else {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5dadda4b..ae2aa454 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -6,7 +6,7 @@ class MyClass<T, U> {
var x: int;
method M(s: bool, lotsaObjects: set<object>)
- returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):
+ returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
requires s;
modifies this, lotsaObjects;
ensures t == t;
@@ -266,10 +266,24 @@ Execution trace:
Dafny program verifier finished with 21 verified, 29 errors
-------------------- Modules0.dfy --------------------
+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
-Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
-3 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
+Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
+Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
+Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module $default must transitively import YY)
+7 resolution/type errors detected in Modules0.dfy
+
+-------------------- Modules1.dfy --------------------
+Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
+Execution trace:
+ (0,0): anon0
+Modules1.dfy(61,3): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 16 verified, 2 errors
-------------------- Queue.dfy --------------------
@@ -300,31 +314,31 @@ Dafny program verifier finished with 10 verified, 0 errors
Dafny program verifier finished with 13 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(15,18): Error: assertion violation
+Use.dfy(14,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(26,18): Error: assertion violation
+Use.dfy(24,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(35,18): Error: assertion violation
+Use.dfy(33,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(56,12): Error: assertion violation
+Use.dfy(52,12): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(88,17): Error: assertion violation
+Use.dfy(82,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(130,23): Error: assertion violation
+Use.dfy(124,23): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(144,5): Error: assertion violation
+Use.dfy(136,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(144,5): Error: assertion violation
+Use.dfy(136,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(215,19): Error: assertion violation
+Use.dfy(207,19): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 276b6c0e..714e9d58 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -55,6 +55,7 @@ class IntSet {
ensures n == null ==> fresh(m.footprint) && m.contents == {x};
ensures n != null ==> m == n && n.contents == old(n.contents) + {x};
ensures n != null ==> fresh(n.footprint - old(n.footprint));
+ decreases if n == null then {} else n.footprint;
{
if (n == null) {
m := new Node;
@@ -145,6 +146,7 @@ class Node {
method Find(x: int) returns (present: bool)
requires Valid();
ensures present <==> x in contents;
+ decreases footprint;
{
if (x == data) {
present := true;
@@ -164,6 +166,7 @@ class Node {
ensures node != null ==> node.Valid();
ensures node == null ==> old(contents) <= {x};
ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};
+ decreases footprint;
{
node := this;
if (left != null && x < data) {
@@ -201,6 +204,7 @@ class Node {
ensures node == null ==> old(contents) == {min};
ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};
ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);
+ decreases footprint;
{
if (left == null) {
min := data;
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cf616fba..0e0d3ab3 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -32,3 +32,75 @@ module I imports J {
module J imports G, M {
}
+
+// --------------- calls
+
+module X2 imports X1 {
+ class MyClass2 {
+ method Down(x1: MyClass1, x0: MyClass0) {
+ call x1.Down(x0);
+ }
+ method WayDown(x0: MyClass0, g: ClassG) {
+ call x0.Down();
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ method Up() {
+ }
+ method Somewhere(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+ }
+}
+
+module X1 imports X0 {
+ class MyClass1 {
+ method Down(x0: MyClass0) {
+ call x0.Down();
+ }
+ method Up(x2: MyClass2) {
+ call x2.Up(); // error: does not follow import relation
+ }
+ }
+}
+
+module X0 {
+ class MyClass0 {
+ method Down() {
+ }
+ method Up(x1: MyClass1, x2: MyClass2) {
+ call x1.Up(x2); // error: does not follow import relation
+ }
+ }
+}
+
+module YY {
+ class MyClassY {
+ method M() { }
+ method P(g: ClassG) {
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ }
+}
+
+class ClassG {
+ method T() { }
+ function method TFunc(): int { 10 }
+ method V(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+}
+
+method Ping() {
+ call Pong(); // allowed: intra-module call
+}
+
+method Pong() {
+ call Ping(); // allowed: intra-module call
+}
+
+method ProcG(g: ClassG) {
+ call g.T(); // allowed: intra-module call
+ var t := g.TFunc(); // allowed: intra-module call
+}
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
new file mode 100644
index 00000000..cfefa7fa
--- /dev/null
+++ b/Test/dafny0/Modules1.dfy
@@ -0,0 +1,62 @@
+module A imports B {
+ class X {
+ function Fx(z: Z): int
+ requires z != null;
+ decreases 5, 4, 3;
+ { z.G() } // fine; this goes to a different module
+ }
+ datatype Y {
+ Cons(int, Y);
+ Empty;
+ }
+}
+
+class C {
+ method M() { }
+ function F(): int { 818 }
+}
+
+method MyMethod() { }
+
+var MyField: int;
+
+module B {
+ class Z {
+ method K() { }
+ function G(): int
+ decreases 10, 8, 6;
+ { 25 }
+ }
+}
+
+static function MyFunction(): int { 5 }
+
+class D { }
+
+method Proc0(x: int)
+ decreases x;
+{
+ if (0 <= x) {
+ call Proc1(x - 1);
+ }
+}
+
+method Proc1(x: int)
+ decreases x;
+{
+ if (0 <= x) {
+ call Proc0(x - 1);
+ }
+}
+
+method Botch0(x: int)
+ decreases x;
+{
+ call Botch1(x - 1); // error: failure to keep termination metric bounded
+}
+
+method Botch1(x: int)
+ decreases x;
+{
+ call Botch0(x); // error: failure to decrease termination metric
+}
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index f429b9ed..97317792 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -36,6 +36,7 @@ class Main {
requires (forall n :: n in S && n.marked ==>
n in stackNodes ||
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ requires (forall n :: n in stackNodes ==> n != null && n.marked);
modifies S;
ensures root.marked;
// nodes reachable from 'root' are marked:
@@ -46,6 +47,7 @@ class Main {
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
+ decreases S - stackNodes;
{
if (! root.marked) {
root.marked := true;
@@ -66,6 +68,7 @@ class Main {
{
var c := root.children[i];
if (c != null) {
+ var D := S - stackNodes; assert root in D;
call RecursiveMarkWorker(c, S, stackNodes + {root});
}
i := i + 1;
@@ -146,7 +149,6 @@ class Main {
function Reachable(from: Node, to: Node, S: set<Node>): bool
requires null !in S;
reads S;
- decreases 1;
{
(exists via: Path :: ReachableVia(from, via, to, S))
}
@@ -154,7 +156,7 @@ class Main {
function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool
requires null !in S;
reads S;
- decreases 0, via;
+ decreases via;
{
match via
case Empty => from == to
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index b627df75..ba6c8e0c 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -2,7 +2,7 @@ class Node {
var next: Node;
function IsList(r: set<Node>): bool
- reads r;
+ reads r;
{
this in r &&
(next != null ==> next.IsList(r - {this}))
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index e006823e..58cb6bea 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -2,7 +2,6 @@ class T {
var x: int;
use function F(y: int): int
- decreases 0;
{
2*y
}
@@ -16,7 +15,6 @@ class T {
}
use function FF(y: int): int
- decreases 1;
{
F(y)
}
@@ -36,12 +34,10 @@ class T {
}
use function G(y: int): bool
- decreases 0;
{
0 <= y
}
use function GG(y: int): bool
- decreases 1;
{
G(y)
}
@@ -58,13 +54,11 @@ class T {
use function H(): int
reads this;
- decreases 0;
{
x
}
use function HH(): int
reads this;
- decreases 1;
{
H()
}
@@ -133,13 +127,11 @@ class T {
use function K(): bool
reads this;
- decreases 0;
{
x <= 100
}
use function KK(): bool
reads this;
- decreases 1;
{
K()
}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2bec0a4d..003566f3 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (BQueue.bpl) do (
)
for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
- Modules0.dfy Queue.dfy ListCopy.dfy
+ Modules0.dfy Modules1.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 04:40:15 +0000