diff options
| author |  Jason Koenig <unknown> | 2012-07-29 12:24:02 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-29 12:24:02 -0700 |
| commit | 310521db71e18305b04f6a32ab753c87e30bfa19 (patch) | |
| tree | 7ccc36b76d4ee7a6fa259bc9853fecb5ec3cf1ad | |
| parent | 8a744c1edfbe715f3b19e9053646b0a6f812196f (diff) | |
Dafny: added structural refinement check
| -rw-r--r-- | Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 35 | ||||
| -rw-r--r-- | Dafny/RefinementTransformer.cs | 300 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 33 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 357 | ||||
| -rw-r--r-- | DafnyDriver/DafnyDriver.cs | 21 |
6 files changed, 690 insertions, 58 deletions
diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs index 3db69fba..aecb6fe7 100644 --- a/Dafny/Cloner.cs +++ b/Dafny/Cloner.cs @@ -125,7 +125,7 @@ namespace Microsoft.Dafny } else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
} else if (t is ParamTypeProxy) {
- return new ParamTypeProxy(((ParamTypeProxy)t).orig); // todo: this is not right, as when cloning the type parameter declartion changes.
+ return new ParamTypeProxy(CloneTypeParam(((ParamTypeProxy)t).orig));
} else {
Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
return null; // to please compiler
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 4a211aee..bf2c7492 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -28,6 +28,7 @@ namespace Microsoft.Dafny { public readonly ModuleDecl DefaultModule;
public readonly ModuleDefinition DefaultModuleDef;
public readonly BuiltIns BuiltIns;
+ public readonly List<TranslationTask> TranslationTasks;
public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns) {
Contract.Requires(name != null);
Contract.Requires(module != null);
@@ -38,6 +39,7 @@ namespace Microsoft.Dafny { BuiltIns = builtIns;
Modules = new List<ModuleDefinition>();
CompileModules = new List<ModuleDefinition>();
+ TranslationTasks = new List<TranslationTask>();
}
}
@@ -781,6 +783,14 @@ namespace Microsoft.Dafny { public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl
+ public bool IsAbstractTypeDeclaration { // true if this type parameter represents t in type t;
+ get { return parent == null; }
+ }
+ public bool IsToplevelScope { // true if this type parameter is on a toplevel (ie. class C<T>), and false if it is on a member (ie. method m<T>(...))
+ get { return parent is TopLevelDecl; }
+ }
+ public int PositionalIndex; // which type parameter this is (ie. in C<S, T, U>, S is 0, T is 1 and U is 2).
+
public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)
: base(tok, name, null) {
Contract.Requires(tok != null);
@@ -789,7 +799,7 @@ namespace Microsoft.Dafny { }
}
- // Represents a submodule declartion at module level scope
+ // Represents a submodule declaration at module level scope
abstract public class ModuleDecl : TopLevelDecl
{
public ModuleSignature Signature; // filled in by resolution, in topological order.
@@ -981,8 +991,6 @@ namespace Microsoft.Dafny { Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
-
-
Members = members;
}
public virtual bool IsDefaultClass {
@@ -4015,5 +4023,26 @@ namespace Microsoft.Dafny { return Attributes != null;
}
}
+ public abstract class TranslationTask
+ {
+ }
+ public class MethodCheck : TranslationTask
+ {
+ public readonly Method Refined;
+ public readonly Method Refining;
+ public MethodCheck(Method a, Method b) {
+ Refined = b;
+ Refining = a;
+ }
+ }
+ public class FunctionCheck : TranslationTask
+ {
+ public readonly Function Refined;
+ public readonly Function Refining;
+ public FunctionCheck(Function a, Function b) {
+ Refined = b;
+ Refining = a;
+ }
+ }
}
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index 56063442..008bf616 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -55,14 +55,17 @@ namespace Microsoft.Dafny ResolutionErrorReporter reporter;
Cloner rawCloner; // This cloner just gives exactly the same thing back.
RefinementCloner refinementCloner; // This cloner wraps things in a RefinementTransformer
- public RefinementTransformer(ResolutionErrorReporter reporter) {
+ Program program;
+ public RefinementTransformer(ResolutionErrorReporter reporter, Program p) {
Contract.Requires(reporter != null);
this.reporter = reporter;
rawCloner = new Cloner();
+ program = p;
}
private ModuleDefinition moduleUnderConstruction; // non-null for the duration of Construct calls
private Queue<Action> postTasks = new Queue<Action>(); // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
+ public Queue<Tuple<Method, Method>> translationMethodChecks = new Queue<Tuple<Method, Method>>(); // contains all the methods that need to be checked for structural refinement.
public void PreResolve(ModuleDefinition m) {
@@ -108,7 +111,8 @@ namespace Microsoft.Dafny }
if (derived != null) {
// check that the new module refines the previous declaration
- CheckIsRefinement(derived, original, nw.tok, "a module (" + d.Name + ") can only be replaced by a refinement of the original module");
+ if (!CheckIsRefinement(derived, original))
+ reporter.Error(nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);
}
}
} else if (d is ArbitraryTypeDecl) {
@@ -164,18 +168,280 @@ namespace Microsoft.Dafny Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method
}
- public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original, IToken errorTok, string errorMsg) {
- while (derived != null) {
- if (derived == original)
- break;
- derived = derived.Refines;
+ public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original) {
+ // Check refinement by construction.
+ var derivedPointer = derived;
+ while (derivedPointer != null) {
+ if (derivedPointer == original)
+ return true;
+ derivedPointer = derivedPointer.Refines;
}
- if (derived != original) {
- reporter.Error(errorTok, errorMsg);
- return false;
- } else return true;
+ // Check structural refinement. Note this involves several checks.
+ // First, we need to know if the two modules are signature compatible;
+ // this is determined immediately as it is necessary for determining
+ // whether resolution will succeed. This involves checking classes, datatypes,
+ // type declarations, and nested modules.
+ // Second, we need to determine whether the specifications will be compatible
+ // (i.e. substitutable), by translating to Boogie.
+
+ var errorCount = reporter.ErrorCount;
+ foreach (var kv in original.TopLevels) {
+ var d = kv.Value;
+ TopLevelDecl nw;
+ if (derived.TopLevels.TryGetValue(kv.Key, out nw)) {
+ if (d is ModuleDecl) {
+ if (!(nw is ModuleDecl)) {
+ reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);
+ } else {
+ CheckIsRefinement(((ModuleDecl)nw).Signature, ((ModuleDecl)d).Signature);
+ }
+ } else if (d is ArbitraryTypeDecl) {
+ if (nw is ModuleDecl) {
+ reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);
+ } else {
+ bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;
+ if (nw is ArbitraryTypeDecl) {
+ if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {
+ reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
+ }
+ } else if (dDemandsEqualitySupport) {
+ if (nw is ClassDecl) {
+ // fine, as long as "nw" does not take any type parameters
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);
+ }
+ } else if (nw is CoDatatypeDecl) {
+ reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
+ } else {
+ Contract.Assert(nw is IndDatatypeDecl);
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);
+ } else {
+ var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());
+ if (!(udt.SupportsEquality)) {
+ reporter.Error(nw.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", nw.Name);
+ }
+ }
+ }
+ }
+ }
+ } else if (d is DatatypeDecl) {
+ if (nw is DatatypeDecl) {
+ if (d is IndDatatypeDecl && !(nw is IndDatatypeDecl)) {
+ reporter.Error(nw, "a datatype ({0}) must be replaced by a datatype, not a codatatype", d.Name);
+ } else if (d is CoDatatypeDecl && !(nw is CoDatatypeDecl)) {
+ reporter.Error(nw, "a codatatype ({0}) must be replaced by a codatatype, not a datatype", d.Name);
+ }
+ // check constructors, formals, etc.
+ CheckDatatypesAreRefinements((DatatypeDecl)d, (DatatypeDecl)nw);
+ } else {
+ reporter.Error(nw, "a {0} ({1}) must be refined by a {0}", d is IndDatatypeDecl ? "datatype" : "codatatype", d.Name);
+ }
+ } else if (d is ClassDecl) {
+ if (!(nw is ClassDecl)) {
+ reporter.Error(nw, "a class declaration ({0}) must be refined by another class declaration", nw.Name);
+ } else {
+ CheckClassesAreRefinements((ClassDecl)nw, (ClassDecl)d);
+ }
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected toplevel
+ }
+ } else {
+ reporter.Error(d, "declaration {0} must have a matching declaration in the refining module", d.Name);
+ }
+ }
+ return errorCount == reporter.ErrorCount;
+ }
+
+ private void CheckClassesAreRefinements(ClassDecl nw, ClassDecl d) {
+ if (nw.TypeArgs.Count != d.TypeArgs.Count) {
+ reporter.Error(nw, "a refining class ({0}) must have the same number of type parameters", nw.Name);
+ } else {
+ var map = new Dictionary<string, MemberDecl>();
+ foreach (var mem in nw.Members) {
+ map.Add(mem.Name, mem);
+ }
+ foreach (var m in d.Members) {
+ MemberDecl newMem;
+ if (map.TryGetValue(m.Name, out newMem)) {
+ if (m.IsStatic != newMem.IsStatic) {
+ reporter.Error(newMem, "member {0} must {1}", m.Name, m.IsStatic? "be static" : "not be static");
+ }
+ if (m is Field) {
+ if (newMem is Field) {
+ var newField = (Field)newMem;
+ if (!ResolvedTypesAreTheSame(newField.Type, ((Field)m).Type))
+ reporter.Error(newMem, "field must be refined by a field with the same type (got {0}, expected {1})", newField.Type, ((Field)m).Type);
+ if (m.IsGhost || !newField.IsGhost)
+ reporter.Error(newField, "a field re-declaration ({0}) must be to ghostify the field", newField.Name, nw.Name);
+ } else {
+ reporter.Error(newMem, "a field declaration ({1}) must be replaced by a field in the refinement base (not {0})", newMem.Name, nw.Name);
+ }
+ } else if (m is Method) {
+ if (newMem is Method) {
+ CheckMethodsAreRefinements((Method)newMem, (Method)m);
+ } else {
+ reporter.Error(newMem, "method must be refined by a method");
+ }
+ } else if (m is Function) {
+ if (newMem is Function) {
+ CheckFunctionsAreRefinements((Function)newMem, (Function)m);
+ } else {
+ bool isPredicate = m is Predicate;
+ bool isCoPredicate = m is CoPredicate;
+ string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
+ reporter.Error(newMem, "{0} must be refined by a {0}", s);
+ }
+ }
+ } else {
+ reporter.Error(nw is DefaultClassDecl ? nw.Module.tok : nw.tok, "refining {0} must have member {1}", nw is DefaultClassDecl ? "module" : "class", m.Name);
+ }
+ }
+ }
+ }
+ void CheckAgreementResolvedParameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind) {
+ Contract.Requires(tok != null);
+ Contract.Requires(old != null);
+ Contract.Requires(nw != null);
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ Contract.Requires(parameterKind != null);
+ if (old.Count != nw.Count) {
+ reporter.Error(tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it refines", thing, name, parameterKind, nw.Count, old.Count);
+ } else {
+ for (int i = 0; i < old.Count; i++) {
+ var o = old[i];
+ var n = nw[i];
+ if (!o.IsGhost && n.IsGhost) {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-ghost to ghost", parameterKind, n.Name, thing, name);
+ } else if (o.IsGhost && !n.IsGhost) {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name);
+ } else if (!ResolvedTypesAreTheSame(o.Type, n.Type)) {
+ reporter.Error(n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);
+ }
+ }
+ }
+ }
+ private void CheckMethodsAreRefinements(Method nw, Method m) {
+ CheckAgreement_TypeParameters(nw.tok, m.TypeArgs, nw.TypeArgs, m.Name, "method", false);
+ CheckAgreementResolvedParameters(nw.tok, m.Ins, nw.Ins, m.Name, "method", "in-parameter");
+ CheckAgreementResolvedParameters(nw.tok, m.Outs, nw.Outs, m.Name, "method", "out-parameter");
+ program.TranslationTasks.Add(new MethodCheck(nw, m));
}
+ private void CheckFunctionsAreRefinements(Function nw, Function f) {
+ if (f is Predicate) {
+ if (!(nw is Predicate)) {
+ reporter.Error(nw, "a predicate declaration ({0}) can only be refined by a predicate", nw.Name);
+ } else {
+ CheckAgreement_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "predicate", false);
+ CheckAgreementResolvedParameters(nw.tok, f.Formals, nw.Formals, nw.Name, "predicate", "parameter");
+ }
+ } else if (f is CoPredicate) {
+ reporter.Error(nw, "refinement of co-predicates is not supported");
+ } else {
+ // f is a plain Function
+ if (nw is Predicate || nw is CoPredicate) {
+ reporter.Error(nw, "a {0} declaration ({1}) can only be refined by a function or function method", nw.IsGhost ? "function" : "function method", nw.Name);
+ } else {
+ CheckAgreement_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "function", false);
+ CheckAgreementResolvedParameters(nw.tok, f.Formals, nw.Formals, nw.Name, "function", "parameter");
+ if (!ResolvedTypesAreTheSame(nw.ResultType, f.ResultType)) {
+ reporter.Error(nw, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", nw.Name, nw.ResultType, f.ResultType);
+ }
+ }
+ }
+ program.TranslationTasks.Add(new FunctionCheck(nw, f));
+ }
+
+ private void CheckDatatypesAreRefinements(DatatypeDecl dd, DatatypeDecl nn) {
+ CheckAgreement_TypeParameters(nn.tok, dd.TypeArgs, nn.TypeArgs, dd.Name, "datatype", false);
+ if (dd.Ctors.Count != nn.Ctors.Count) {
+ reporter.Error(nn.tok, "a refining datatype must have the same number of constructors");
+ } else {
+ var map = new Dictionary<string, DatatypeCtor>();
+ foreach (var ctor in nn.Ctors) {
+ map.Add(ctor.Name, ctor);
+ }
+ foreach (var ctor in dd.Ctors) {
+ DatatypeCtor newCtor;
+ if (map.TryGetValue(ctor.Name, out newCtor)) {
+ if (newCtor.Formals.Count != ctor.Formals.Count) {
+ reporter.Error(newCtor, "the constructor ({0}) must have the same number of formals as in the refined module", newCtor.Name);
+ } else {
+ for (int i = 0; i < newCtor.Formals.Count; i++) {
+ var a = ctor.Formals[i]; var b = newCtor.Formals[i];
+ if (a.HasName) {
+ if (!b.HasName || a.Name != b.Name)
+ reporter.Error(b, "formal argument {0} in constructor {1} does not have the same name as in the refined module (should be {2})", i, ctor.Name, a.Name);
+ }
+ if (!ResolvedTypesAreTheSame(a.Type, b.Type)) {
+ reporter.Error(b, "formal argument {0} in constructor {1} does not have the same type as in the refined module (should be {2}, not {3})", i, ctor.Name, a.Type.ToString(), b.Type.ToString());
+ }
+ }
+ }
+ } else {
+ reporter.Error(nn, "the constructor {0} must be present in the refining datatype", ctor.Name);
+ }
+ }
+ }
+
+ }
+ // Check that two resolved types are the same in a similar context (the same type parameters, method, class, etc.)
+ // Assumes that a is in a previous refinement, and b is in a refinement.
+ public static bool ResolvedTypesAreTheSame(Type a, Type b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ if (a is TypeProxy || b is TypeProxy)
+ return false;
+
+ if (a is BoolType) {
+ return b is BoolType;
+ } else if (a is IntType) {
+ if (b is IntType) {
+ return (a is NatType) == (b is NatType);
+ } else return false;
+ } else if (a is ObjectType) {
+ return b is ObjectType;
+ } else if (a is SetType) {
+ return b is SetType && ResolvedTypesAreTheSame(((SetType)a).Arg, ((SetType)b).Arg);
+ } else if (a is MultiSetType) {
+ return b is MultiSetType && ResolvedTypesAreTheSame(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
+ } else if (a is MapType) {
+ return b is MapType && ResolvedTypesAreTheSame(((MapType)a).Domain, ((MapType)b).Domain) && ResolvedTypesAreTheSame(((MapType)a).Range, ((MapType)b).Range);
+ } else if (a is SeqType) {
+ return b is SeqType && ResolvedTypesAreTheSame(((SeqType)a).Arg, ((SeqType)b).Arg);
+ } else if (a is UserDefinedType) {
+ if (!(b is UserDefinedType)) {
+ return false;
+ }
+ UserDefinedType aa = (UserDefinedType)a;
+ UserDefinedType bb = (UserDefinedType)b;
+ if (aa.ResolvedClass != null && aa.ResolvedClass.Name == bb.ResolvedClass.Name) {
+ // these are both resolved class/datatype types
+ Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);
+ for (int i = 0; i < aa.TypeArgs.Count; i++)
+ if (!ResolvedTypesAreTheSame(aa.TypeArgs[i], bb.TypeArgs[i]))
+ return false;
+ return true;
+ } else if (aa.ResolvedParam != null && bb.ResolvedParam != null) {
+ // these are both resolved type parameters
+ Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);
+ // Note that this is only correct if the two types occur in the same context, ie. both from the same method
+ // or class field.
+ return aa.ResolvedParam.PositionalIndex == bb.ResolvedParam.PositionalIndex &&
+ aa.ResolvedParam.IsToplevelScope == bb.ResolvedParam.IsToplevelScope;
+ } else if (aa.ResolvedParam.IsAbstractTypeDeclaration && bb.ResolvedClass != null) {
+ return (aa.ResolvedParam.Name == bb.ResolvedClass.Name);
+ } else {
+ // something is wrong; either aa or bb wasn't properly resolved, or they aren't the same
+ return false;
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ }
public void PostResolve(ModuleDefinition m) {
if (m == moduleUnderConstruction) {
while (this.postTasks.Count != 0) {
@@ -279,7 +545,7 @@ namespace Microsoft.Dafny } else {
var nwMember = nw.Members[index];
if (nwMember is Field) {
- if (member is Field && TypesAreEqual(((Field)nwMember).Type, ((Field)member).Type)) {
+ if (member is Field && TypesAreSyntacticallyEqual(((Field)nwMember).Type, ((Field)member).Type)) {
if (member.IsGhost || !nwMember.IsGhost)
reporter.Error(nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name, nw.Name);
} else {
@@ -318,7 +584,7 @@ namespace Microsoft.Dafny } else {
CheckAgreement_TypeParameters(f.tok, prevFunction.TypeArgs, f.TypeArgs, f.Name, "function");
CheckAgreement_Parameters(f.tok, prevFunction.Formals, f.Formals, f.Name, "function", "parameter");
- if (!TypesAreEqual(prevFunction.ResultType, f.ResultType)) {
+ if (!TypesAreSyntacticallyEqual(prevFunction.ResultType, f.ResultType)) {
reporter.Error(f, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", f.Name, f.ResultType, prevFunction.ResultType);
}
}
@@ -385,7 +651,7 @@ namespace Microsoft.Dafny return nw;
}
- void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {
+ void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing, bool checkNames = true) {
Contract.Requires(tok != null);
Contract.Requires(old != null);
Contract.Requires(nw != null);
@@ -397,7 +663,7 @@ namespace Microsoft.Dafny for (int i = 0; i < old.Count; i++) {
var o = old[i];
var n = nw[i];
- if (o.Name != n.Name) {
+ if (o.Name != n.Name && checkNames) { // if checkNames is false, then just treat the parameters positionally.
reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);
} else {
// This explains what we want to do and why:
@@ -444,14 +710,14 @@ namespace Microsoft.Dafny reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-ghost to ghost", parameterKind, n.Name, thing, name);
} else if (o.IsGhost && !n.IsGhost) {
reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name);
- } else if (!TypesAreEqual(o.Type, n.Type)) {
+ } else if (!TypesAreSyntacticallyEqual(o.Type, n.Type)) {
reporter.Error(n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);
}
}
}
}
- bool TypesAreEqual(Type t, Type u) {
+ bool TypesAreSyntacticallyEqual(Type t, Type u) {
Contract.Requires(t != null);
Contract.Requires(u != null);
return t.ToString() == u.ToString();
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 8c14cb0c..0761d865 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -144,7 +144,7 @@ namespace Microsoft.Dafny h++;
}
- var refinementTransformer = new RefinementTransformer(this);
+ var refinementTransformer = new RefinementTransformer(this, prog);
IRewriter rewriter = new AutoContractsRewriter();
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
@@ -216,11 +216,14 @@ namespace Microsoft.Dafny ModuleSignature compileSig;
if (abs.CompilePath != null) {
if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig)) {
- if (refinementTransformer.CheckIsRefinement(compileSig, p, abs.CompilePath[0],
- "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val))) {
+ if (refinementTransformer.CheckIsRefinement(compileSig, p)) {
abs.Signature.CompileSignature = compileSig;
- abs.Signature.IsGhost = compileSig.IsGhost;
+ } else {
+ Error(abs.CompilePath[0],
+ "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val));
}
+ abs.Signature.IsGhost = compileSig.IsGhost;
+ // always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement
}
}
} else {
@@ -305,17 +308,17 @@ namespace Microsoft.Dafny var subdecl = (LiteralModuleDecl)tld;
var subBindings = BindModuleNames(subdecl.ModuleDef, bindings);
if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) {
- Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+ Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
} else if (tld is AbstractModuleDecl) {
var subdecl = (AbstractModuleDecl)tld;
if (!bindings.BindName(subdecl.Name, subdecl, null)) {
- Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+ Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
} else if (tld is AliasModuleDecl) {
var subdecl = (AliasModuleDecl)tld;
if (!bindings.BindName(subdecl.Name, subdecl, null)) {
- Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+ Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
}
}
@@ -853,7 +856,7 @@ namespace Microsoft.Dafny foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
- ResolveTypeParameters(d.TypeArgs, true, d);
+ ResolveTypeParameters(d.TypeArgs, true, d, true);
if (d is ArbitraryTypeDecl) {
// nothing to do
} else if (d is ClassDecl) {
@@ -889,7 +892,7 @@ namespace Microsoft.Dafny foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
- ResolveTypeParameters(d.TypeArgs, false, d);
+ ResolveTypeParameters(d.TypeArgs, false, d, true);
if (d is ClassDecl) {
ResolveClassMemberBodies((ClassDecl)d);
}
@@ -1520,14 +1523,14 @@ namespace Microsoft.Dafny } else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
- ResolveTypeParameters(f.TypeArgs, true, f);
+ ResolveTypeParameters(f.TypeArgs, true, f, false);
ResolveFunctionSignature(f);
allTypeParameters.PopMarker();
} else if (member is Method) {
Method m = (Method)member;
allTypeParameters.PushMarker();
- ResolveTypeParameters(m.TypeArgs, true, m);
+ ResolveTypeParameters(m.TypeArgs, true, m, false);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
@@ -1556,14 +1559,14 @@ namespace Microsoft.Dafny } else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
- ResolveTypeParameters(f.TypeArgs, false, f);
+ ResolveTypeParameters(f.TypeArgs, false, f, false);
ResolveFunction(f);
allTypeParameters.PopMarker();
} else if (member is Method) {
Method m = (Method)member;
allTypeParameters.PushMarker();
- ResolveTypeParameters(m.TypeArgs, false, m);
+ ResolveTypeParameters(m.TypeArgs, false, m, false);
ResolveMethod(m);
allTypeParameters.PopMarker();
} else {
@@ -1832,16 +1835,18 @@ namespace Microsoft.Dafny }
}
- void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
+ void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent, bool isToplevel) {
Contract.Requires(tparams != null);
Contract.Requires(parent != null);
// push non-duplicated type parameter names
+ int index = 0;
foreach (TypeParameter tp in tparams) {
Contract.Assert(tp != null);
if (emitErrors) {
// we're seeing this TypeParameter for the first time
tp.Parent = parent;
+ tp.PositionalIndex = index;
}
if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) {
Error(tp, "Duplicate type-parameter name: {0}", tp.Name);
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 7839c5ad..25524287 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -355,9 +355,30 @@ namespace Microsoft.Dafny { foreach(var c in fieldConstants.Values) {
sink.TopLevelDeclarations.Add(c);
}
+ HashSet<Tuple<string, string>> checkedMethods = new HashSet<Tuple<string, string>>();
+ HashSet<Tuple<string, string>> checkedFunctions = new HashSet<Tuple<string, string>>();
+ foreach (var t in program.TranslationTasks) {
+ if (t is MethodCheck) {
+ var m = (MethodCheck)t;
+ var id = new Tuple<string, string>(m.Refined.FullCompileName, m.Refining.FullCompileName);
+ if (!checkedMethods.Contains(id)) {
+ AddMethodRefinementCheck(m);
+ checkedMethods.Add(id);
+ }
+ } else if (t is FunctionCheck) {
+ var f = (FunctionCheck)t;
+ var id = new Tuple<string, string>(f.Refined.FullCompileName, f.Refining.FullCompileName);
+ if (!checkedFunctions.Contains(id)) {
+ AddFunctionRefinementCheck(f);
+ checkedFunctions.Add(id);
+ }
+ }
+ }
return sink;
}
+
+
void AddDatatype(DatatypeDecl dt)
{
Contract.Requires(dt != null);
@@ -3021,25 +3042,8 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
- Bpl.VariableSeq inParams = new Bpl.VariableSeq();
- Bpl.VariableSeq outParams = new Bpl.VariableSeq();
- if (!m.IsStatic) {
- Bpl.Expr wh = Bpl.Expr.And(
- Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),
- etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetReceiverType(m.tok, m)));
- Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);
- inParams.Add(thVar);
- }
- foreach (Formal p in m.Ins) {
- Bpl.Type varType = TrType(p.Type);
- Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
- inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
- }
- foreach (Formal p in m.Outs) {
- Bpl.Type varType = TrType(p.Type);
- Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
- outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
- }
+ Bpl.VariableSeq inParams, outParams;
+ GenerateMethodParameters(m, etran, out inParams, out outParams);
Bpl.RequiresSeq req = new Bpl.RequiresSeq();
Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
@@ -3110,6 +3114,293 @@ namespace Microsoft.Dafny { return proc;
}
+ private void AddMethodRefinementCheck(MethodCheck methodCheck) {
+
+ // First, we generate the declaration of the procedure. This procedure has the same
+ // pre and post conditions as the refined method. The body implementation will be a call
+ // to the refining method.
+ Method m = methodCheck.Refined;
+ currentModule = m.EnclosingClass.Module;
+ currentMethod = m;
+
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
+
+ Bpl.VariableSeq inParams, outParams;
+ GenerateMethodParameters(m, etran, out inParams, out outParams);
+
+ Bpl.RequiresSeq req = new Bpl.RequiresSeq();
+ Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
+ Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
+
+ Bpl.Expr context = Bpl.Expr.And(
+ Bpl.Expr.Eq(Bpl.Expr.Literal(m.EnclosingClass.Module.Height), etran.ModuleContextHeight()),
+ etran.InMethodContext());
+ req.Add(Requires(m.tok, true, context, null, null));
+
+ mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);
+ mod.Add(etran.Tick());
+
+ foreach (MaybeFreeExpression p in m.Req) {
+ if ((p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating)) {
+ req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, null));
+ } else {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
+ req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ }
+ }
+ }
+ foreach (MaybeFreeExpression p in m.Ens) {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
+ ens.Add(Ensures(s.E.tok, s.IsFree, s.E, "Error: postcondition of refined method may be violated", null));
+ }
+ }
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old)) {
+ ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
+ }
+
+ // Generate procedure, and then add it to the sink
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
+ string name = "CheckRefinement$$" + m.FullCompileName + "$" + methodCheck.Refining.FullCompileName;
+ Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, new Bpl.EnsuresSeq());
+
+ sink.TopLevelDeclarations.Add(proc);
+
+
+ // Generate the implementation
+ typeParams = TrTypeParamDecls(m.TypeArgs);
+ inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
+
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
+ GenerateImplPrelude(m, inParams, outParams, builder, localVariables);
+
+ // Generate the call to the refining method
+ Method method = methodCheck.Refining;
+ Expression receiver = new ThisExpr(Token.NoToken);
+ Bpl.ExprSeq ins = new Bpl.ExprSeq();
+ if (!method.IsStatic) {
+ ins.Add(etran.TrExpr(receiver));
+ }
+
+ // Ideally, the modifies and decreases checks would be done after the precondition check,
+ // but Boogie doesn't give us a hook for that. So, we set up our own local variables here to
+ // store the actual parameters.
+ // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < method.Ins.Count; i++) {
+ Formal p = method.Ins[i];
+ VarDecl local = new VarDecl(p.tok, p.Name + "#", p.Type, p.IsGhost);
+ local.type = local.OptionalType; // resolve local here
+ IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
+ ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(p, ie);
+ localVariables.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
+
+ Bpl.IdentifierExpr param = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
+ var bActual = new Bpl.IdentifierExpr(Token.NoToken, m.Ins[i].UniqueName, TrType(m.Ins[i].Type));
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, param, etran.CondApplyUnbox(Token.NoToken, bActual, cce.NonNull( m.Ins[i].Type),p.Type));
+ builder.Add(cmd);
+ ins.Add(param);
+ }
+
+ // Check modifies clause of a subcall is a subset of the current frame.
+ CheckFrameSubset(method.tok, method.Mod.Expressions, receiver, substMap, etran, builder, "call may modify locations not in the refined method's modifies clause", null);
+
+ // Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
+ Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
+ List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>();
+ for (int i = 0; i < m.Outs.Count; i++) {
+ var bLhs = m.Outs[i];
+ if (!ExpressionTranslator.ModeledAsBoxType(method.Outs[i].Type) && ExpressionTranslator.ModeledAsBoxType(bLhs.Type)) {
+ // we need an Box
+ Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + otherTmpVarCount, TrType(method.Outs[i].Type)));
+ otherTmpVarCount++;
+ localVariables.Add(var);
+ Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, TrType(method.Outs[i].Type));
+ tmpOuts.Add(varIdE);
+ outs.Add(varIdE);
+ } else {
+ tmpOuts.Add(null);
+ outs.Add(new Bpl.IdentifierExpr(Token.NoToken, bLhs.UniqueName, TrType(bLhs.Type)));
+ }
+ }
+
+ // Make the call
+ Bpl.CallCmd call = new Bpl.CallCmd(method.tok, method.FullCompileName, ins, outs);
+ builder.Add(call);
+
+ for (int i = 0; i < m.Outs.Count; i++) {
+ var bLhs = m.Outs[i];
+ var tmpVarIdE = tmpOuts[i];
+ if (tmpVarIdE != null) {
+ // e := Box(tmpVar);
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(Token.NoToken, new Bpl.IdentifierExpr(Token.NoToken, bLhs.UniqueName, TrType(bLhs.Type)), FunctionCall(Token.NoToken, BuiltinFunction.Box, null, tmpVarIdE));
+ builder.Add(cmd);
+ }
+ }
+
+ foreach (MaybeFreeExpression p in m.Ens) {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
+ var assert = new Bpl.AssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold."));
+ assert.ErrorData = "Error: A postcondition of the refined method may not hold.";
+ builder.Add(assert);
+ }
+ }
+ Bpl.StmtList stmts = builder.Collect(method.tok); // this token is for the implict return, which should be for the refining method,
+ // as this is where the error is.
+
+ Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
+ typeParams, inParams, outParams,
+ localVariables, stmts, etran.TrAttributes(m.Attributes, null));
+ sink.TopLevelDeclarations.Add(impl);
+
+ // Clean up
+ currentModule = null;
+ currentMethod = null;
+ otherTmpVarCount = 0;
+ _tmpIEs.Clear();
+ }
+
+ private static QKeyValue ErrorMessageAttribute(IToken t, string error) {
+ var l = new List<object>(1);
+ l.Add(error);
+ return new QKeyValue(t, "msg", l, null);
+ }
+ private static QKeyValue ErrorMessageAttribute(IToken t, string error, QKeyValue qv) {
+ var l = new List<object>(1);
+ l.Add(error);
+ return new QKeyValue(t, "msg", l, qv);
+ }
+
+ private void AddFunctionRefinementCheck(FunctionCheck functionCheck) {
+ Contract.Requires(sink != null && predef != null);
+ Contract.Requires(currentModule == null);
+ Contract.Ensures(currentModule == null);
+
+ Function f = functionCheck.Refined;
+ Function function = functionCheck.Refining;
+ currentModule = function.EnclosingClass.Module;
+
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
+ // parameters of the procedure
+ Bpl.VariableSeq inParams = new Bpl.VariableSeq();
+ if (!f.IsStatic) {
+ Bpl.Expr wh = Bpl.Expr.And(
+ Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),
+ etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetReceiverType(f.tok, f)));
+ Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);
+ inParams.Add(thVar);
+ }
+ foreach (Formal p in f.Formals) {
+ Bpl.Type varType = TrType(p.Type);
+ Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
+ inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
+ }
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
+ // the procedure itself
+ Bpl.RequiresSeq req = new Bpl.RequiresSeq();
+ // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
+ ModuleDefinition mod = function.EnclosingClass.Module;
+ Bpl.Expr context = Bpl.Expr.And(
+ Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
+ Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(function)), etran.FunctionContextHeight()));
+ req.Add(Requires(f.tok, true, context, null, null));
+
+ foreach (Expression p in f.Req) {
+ req.Add(Requires(p.tok, true, etran.TrExpr(p), null, null));
+ }
+
+ // check that postconditions hold
+ var ens = new Bpl.EnsuresSeq();
+ foreach (Expression p in f.Ens) {
+ bool splitHappened; // we actually don't care
+ foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {
+ if (!s.IsFree) {
+ ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
+ }
+ }
+ }
+ Bpl.Procedure proc = new Bpl.Procedure(function.tok, "CheckIsRefinement$$" + f.FullCompileName + "$" + functionCheck.Refining.FullCompileName, typeParams, inParams, new Bpl.VariableSeq(),
+ req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null));
+ sink.TopLevelDeclarations.Add(proc);
+
+ VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
+ Bpl.VariableSeq locals = new Bpl.VariableSeq();
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+
+ Bpl.FunctionCall funcOriginal = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));
+ Bpl.FunctionCall funcRefining = new Bpl.FunctionCall(new Bpl.IdentifierExpr(functionCheck.Refining.tok, functionCheck.Refining.FullCompileName, TrType(f.ResultType)));
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ args.Add(etran.HeapExpr);
+ foreach (Variable p in implInParams) {
+ args.Add(new Bpl.IdentifierExpr(f.tok, p));
+ }
+ Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcOriginal, args);
+ Bpl.Expr funcAppl2 = new Bpl.NAryExpr(f.tok, funcRefining, args);
+
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < function.Formals.Count; i++) {
+ Formal p = function.Formals[i];
+ IdentifierExpr ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].UniqueName);
+ ie.Var = f.Formals[i]; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(p, ie);
+ }
+ // add canCall
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(Token.NoToken, function.FullCompileName + "#canCall", Bpl.Type.Bool);
+ Bpl.Expr canCall = new Bpl.NAryExpr(Token.NoToken, new Bpl.FunctionCall(canCallFuncID), args);
+ builder.Add(new AssumeCmd(function.tok, canCall));
+
+ // check that the preconditions for the call hold
+ foreach (Expression p in function.Req) {
+ Expression precond = Substitute(p, new ThisExpr(Token.NoToken), substMap);
+ var assert = new AssertCmd(p.tok, etran.TrExpr(precond));
+ assert.ErrorData = "Error: the refining function is not allowed to add preconditions";
+ builder.Add(assert);
+ }
+ builder.Add(new AssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, funcAppl2)));
+
+ foreach (Expression p in f.Ens) {
+ var s = new FunctionCallSubstituter(new ThisExpr(Token.NoToken), substMap, f, function);
+ Expression precond = s.Substitute(p);
+ var assert = new AssertCmd(p.tok, etran.TrExpr(precond));
+ assert.ErrorData = "Error: A postcondition of the refined function may not hold";
+ builder.Add(assert);
+ }
+ Bpl.Implementation impl = new Bpl.Implementation(function.tok, proc.Name,
+ typeParams, implInParams, new Bpl.VariableSeq(),
+ locals, builder.Collect(function.tok));
+ sink.TopLevelDeclarations.Add(impl);
+
+ Contract.Assert(currentModule == function.EnclosingClass.Module);
+ currentModule = null;
+ }
+
+ private void GenerateMethodParameters(Method m, ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) {
+ inParams = new Bpl.VariableSeq();
+ outParams = new Bpl.VariableSeq();
+ if (!m.IsStatic) {
+ Bpl.Expr wh = Bpl.Expr.And(
+ Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),
+ etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetReceiverType(m.tok, m)));
+ Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);
+ inParams.Add(thVar);
+ }
+ foreach (Formal p in m.Ins) {
+ Bpl.Type varType = TrType(p.Type);
+ Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
+ inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
+ }
+ foreach (Formal p in m.Outs) {
+ Bpl.Type varType = TrType(p.Type);
+ Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
+ outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
+ }
+ }
+
class BoilerplateTriple { // a triple that is now a quintuple
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -5447,6 +5738,7 @@ namespace Microsoft.Dafny { void ObjectInvariant()
{
Contract.Invariant(HeapExpr != null);
+ Contract.Invariant(HeapExpr is Bpl.OldExpr || HeapExpr is Bpl.IdentifierExpr);
Contract.Invariant(predef != null);
Contract.Invariant(translator != null);
Contract.Invariant(This != null);
@@ -7963,7 +8255,32 @@ namespace Microsoft.Dafny { // TODO: in the following substitution, it may be that we also need to update the types of the resulting subexpressions (is this true for all Substitute calls?)
return Substitute(fce.Function.Body, fce.Receiver, substMap);
}
-
+ public class FunctionCallSubstituter : Substituter
+ {
+ public readonly Function A, B;
+ public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Function a, Function b)
+ : base(receiverReplacement, substMap) {
+ A = a;
+ B = b;
+ }
+ public override Expression Substitute(Expression expr) {
+ if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ Expression receiver = Substitute(e.Receiver);
+ List<Expression> newArgs = SubstituteExprList(e.Args);
+ FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
+ if (e.Function == A) {
+ newFce.Function = B;
+ newFce.Type = e.Type; // TODO: this may not work with type parameters.
+ } else {
+ newFce.Function = e.Function;
+ newFce.Type = e.Type;
+ }
+ return newFce;
+ }
+ return base.Substitute(expr);
+ }
+ }
public class Substituter
{
public readonly Expression receiverReplacement;
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 3534dcbf..82a0e8ed 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -677,8 +677,8 @@ namespace Microsoft.Dafny if (error is CallCounterexample)
{
CallCounterexample err = (CallCounterexample)error;
- ReportBplError(err.FailingCall.tok, "Error BP5002: A precondition for this call might not hold.", true);
- ReportBplError(err.FailingRequires.tok, "Related location: This is the precondition that might not hold.", false);
+ ReportBplError(err.FailingCall.tok, (err.FailingCall.ErrorData as string) ?? "Error BP5002: A precondition for this call might not hold.", true);
+ ReportBplError(err.FailingRequires.tok, (err.FailingRequires.ErrorData as string) ?? "Related location: This is the precondition that might not hold.", false);
if (CommandLineOptions.Clo.XmlSink != null)
{
CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);
@@ -688,7 +688,8 @@ namespace Microsoft.Dafny {
ReturnCounterexample err = (ReturnCounterexample)error;
ReportBplError(err.FailingReturn.tok, "Error BP5003: A postcondition might not hold on this return path.", true);
- ReportBplError(err.FailingEnsures.tok, "Related location: This is the postcondition that might not hold.", false);
+ ReportBplError(err.FailingEnsures.tok, (err.FailingEnsures.ErrorData as string) ?? "Related location: This is the postcondition that might not hold.", false);
+ ReportAllBplErrors(err.FailingEnsures.Attributes);
if (CommandLineOptions.Clo.XmlSink != null)
{
CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);
@@ -722,6 +723,8 @@ namespace Microsoft.Dafny msg = "Error BP5001: This assertion might not hold.";
}
ReportBplError(err.FailingAssert.tok, msg, true);
+ var attr = err.FailingAssert.Attributes;
+ ReportAllBplErrors(attr);
if (CommandLineOptions.Clo.XmlSink != null)
{
CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);
@@ -787,5 +790,17 @@ namespace Microsoft.Dafny return PipelineOutcome.VerificationCompleted;
}
+ private static void ReportAllBplErrors(QKeyValue attr) {
+ while (attr != null) {
+ if (attr.Key == "msg" && attr.Params.Count == 1) {
+ var str = attr.Params[0] as string;
+ if (str != null) {
+ ReportBplError(attr.tok, "Error: "+str, false);
+ }
+ }
+ attr = attr.Next;
+ }
+ }
+
}
}
|