diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 143 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 6 |
2 files changed, 86 insertions, 63 deletions
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 58992dea..18160f39 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -38,10 +38,12 @@ namespace Microsoft.Dafny { readonly Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>! classMembers = new Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>();
readonly Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>! datatypeCtors = new Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>();
readonly Graph<ModuleDecl!>! importGraph = new Graph<ModuleDecl!>();
-
+
+ bool checkRefinements = true;
+
public void ResolveProgram(Program! prog) {
// register modules
- Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();
+ Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();
foreach (ModuleDecl m in prog.Modules) {
if (modules.ContainsKey(m.Name)) {
Error(m, "Duplicate module name: {0}", m.Name);
@@ -50,6 +52,7 @@ namespace Microsoft.Dafny { }
}
// resolve imports and register top-level declarations
+ Graph<TopLevelDecl!>! refines = new Graph<TopLevelDecl!>();
foreach (ModuleDecl m in prog.Modules) {
importGraph.AddVertex(m);
foreach (string imp in m.Imports) {
@@ -64,6 +67,7 @@ namespace Microsoft.Dafny { }
}
RegisterTopLevelDecls(m.TopLevelDecls);
+ foreach (TopLevelDecl! decl in m.TopLevelDecls) refines.AddVertex(decl);
}
// check for cycles in the import graph
List<ModuleDecl!> cycle = importGraph.TryFindCycle();
@@ -86,11 +90,27 @@ namespace Microsoft.Dafny { }
}
- // resolve top-level declarations of refinements
+ // resolve top-level declarations of refinements
foreach (ModuleDecl m in prog.Modules)
foreach (TopLevelDecl decl in m.TopLevelDecls)
- if (decl is ClassRefinementDecl)
- ResolveTopLevelRefinement((ClassRefinementDecl) decl);
+ if (decl is ClassRefinementDecl) {
+ ClassRefinementDecl! rdecl = (ClassRefinementDecl) decl;
+ ResolveTopLevelRefinement(rdecl);
+ if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);
+ }
+
+ // attempt finding refinement cycles
+ List<TopLevelDecl!> refinesCycle = refines.TryFindCycle();
+ if (refinesCycle != null) {
+ string cy = "";
+ string sep = "";
+ foreach (TopLevelDecl decl in refinesCycle) {
+ cy = decl + sep + cy;
+ sep = " -> ";
+ }
+ Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);
+ checkRefinements = false;
+ }
// resolve top-level declarations
Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();
@@ -162,7 +182,6 @@ namespace Microsoft.Dafny { }
public void ResolveTopLevelRefinement(ClassRefinementDecl! decl) {
- // TODO: check for loops in refinement
if (!classes.ContainsKey(decl.RefinedClass.val)) {
Error(decl.RefinedClass, "Refined class declaration is missing: {0}", decl.RefinedClass.val);
} else {
@@ -243,26 +262,28 @@ namespace Microsoft.Dafny { CouplingInvariant inv = (CouplingInvariant)member;
if (currentClass is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
- assert refined != null;
- assert classMembers.ContainsKey(refined);
- Dictionary<string!,MemberDecl!> members = classMembers[refined];
+ if (refined != null) {
+ assert classMembers.ContainsKey(refined);
+ Dictionary<string!,MemberDecl!> members = classMembers[refined];
+
+ // resolve abstracted fields in the refined class
+ List<Field!> fields = new List<Field!>();
+ foreach (IToken tok in inv.Toks) {
+ if (!members.ContainsKey(tok.val))
+ Error(tok, "Refined class does not declare a field: {0}", tok.val);
+ else {
+ MemberDecl! field = members[tok.val];
+ if (!(field is Field))
+ Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
+ else if (fields.Contains((Field!)field))
+ Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
+ else
+ fields.Add((Field!)field);
+ }
+ }
+ inv.Refined = fields;
+ }
- // resolve abstracted fields in the refined class
- List<Field!> fields = new List<Field!>();
- foreach (IToken tok in inv.Toks) {
- if (!members.ContainsKey(tok.val))
- Error(tok, "Refined class does not declare a field: {0}", tok.val);
- else {
- MemberDecl! field = members[tok.val];
- if (!(field is Field))
- Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
- else if (fields.Contains((Field!)field))
- Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
- else
- fields.Add((Field!)field);
- }
- }
- inv.Refined = fields;
} else {
Error(member, "Coupling invariants can only be declared in refinement classes");
}
@@ -272,12 +293,13 @@ namespace Microsoft.Dafny { if (currentClass is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
- assert refined != null;
- assert classMembers.ContainsKey(refined);
+ if (refined != null) {
+ assert classMembers.ContainsKey(refined);
- // there is a member with the same name in refined class if and only if the member is a refined method
- if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
- Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);
+ // there is a member with the same name in refined class if and only if the member is a refined method
+ if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
+ Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);
+ }
}
}
currentClass = null;
@@ -314,36 +336,41 @@ namespace Microsoft.Dafny { // check if signature of the refined method matches the refinement method
if (member is MethodRefinement) {
MethodRefinement mf = (MethodRefinement)member;
- assert currentClass is ClassRefinementDecl;
- assert ((ClassRefinementDecl)currentClass).Refined != null; // should have already been resolved
- MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];
- if (d is Method) {
- mf.Refined = (Method)d;
- if (mf.Ins.Count != mf.Refined.Ins.Count)
- Error(mf, "Different number of input variables");
- if (mf.Outs.Count != mf.Refined.Outs.Count)
- Error(mf, "Different number of output variables");
- if (mf.IsStatic || mf.Refined.IsStatic)
- Error(mf, "Refined methods cannot be static");
+ if (currentClass is ClassRefinementDecl) {
+ // should have already been resolved
+ if (((ClassRefinementDecl)currentClass).Refined != null) {
+ MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];
+ if (d is Method) {
+ mf.Refined = (Method)d;
+ if (mf.Ins.Count != mf.Refined.Ins.Count)
+ Error(mf, "Different number of input variables");
+ if (mf.Outs.Count != mf.Refined.Outs.Count)
+ Error(mf, "Different number of output variables");
+ if (mf.IsStatic || mf.Refined.IsStatic)
+ Error(mf, "Refined methods cannot be static");
+ } else {
+ Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);
+ }
+ }
} else {
- Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);
- }
+ Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
+ }
}
} else if (member is CouplingInvariant) {
CouplingInvariant inv = (CouplingInvariant)member;
- assert inv.Refined != null;
- inv.Formals = new List<Formal!>();
- scope.PushMarker();
- for (int i = 0; i < inv.Refined.Count; i++) {
- Field! field = inv.Refined[i];
- Formal! formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);
- inv.Formals.Add(formal);
- scope.Push(inv.Toks[i].val, formal);
- }
- ResolveExpression(inv.Expr, false, true);
- scope.PopMarker();
-
+ if (inv.Refined != null) {
+ inv.Formals = new List<Formal!>();
+ scope.PushMarker();
+ for (int i = 0; i < inv.Refined.Count; i++) {
+ Field! field = inv.Refined[i];
+ Formal! formal = new Formal(inv.Toks[i], field.Name, field.Type, true, field.IsGhost);
+ inv.Formals.Add(formal);
+ scope.Push(inv.Toks[i].val, formal);
+ }
+ ResolveExpression(inv.Expr, false, true);
+ scope.PopMarker();
+ }
} else {
assert false; // unexpected member type
}
@@ -469,10 +496,10 @@ namespace Microsoft.Dafny { void ResolveTypeParameters(List<TypeParameter!>! tparams, bool emitErrors, TypeParameter.ParentType! parent) {
// push type arguments of the refined class
- if (parent is ClassRefinementDecl) {
+ if (checkRefinements && parent is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)parent).Refined;
- assert refined != null;
- ResolveTypeParameters(refined.TypeArgs, false, refined);
+ if (refined != null)
+ ResolveTypeParameters(refined.TypeArgs, false, refined);
}
// push non-duplicated type parameter names
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 5a762ef6..dcd1b60f 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1747,12 +1747,8 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);
- // for now, refinement is local -- if A.f is refined by B.g then f is shadowed by g in B.
- // therefore, the abstract and concrete programs operate on different receivers thisA and thisB.
- // there is still a possibility of A events polluting the heap that's used by B events, e.g. if another object is referenced by both thisA and thisB.
-
// TODO: this straight inlining does not handle recursive calls
- // TODO: we assume frame allows anything to be changed
+ // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure
// generate procedure declaration with pre-condition wp(r, true)
Bpl.Procedure! proc = AddMethod(r, false, true);
|