From d26d672bb7cfea66721d4a819477f3a7541d4631 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 20 Feb 2013 17:38:56 -0800 Subject: Added Equals method on Type Fixed some precondition violations Various improvements in Contracts --- Source/Dafny/Compiler.cs | 6 ++++- Source/Dafny/DafnyAst.cs | 41 +++++++++++++++++++++++++++++++++++ Source/Dafny/Printer.cs | 4 +++- Source/Dafny/RefinementTransformer.cs | 1 + Source/Dafny/Resolver.cs | 6 ++++- Source/Dafny/Translator.cs | 22 ++++++++++++------- Source/DafnyDriver/DafnyDriver.cs | 2 ++ Test/dafny0/Answer | 6 ++--- 8 files changed, 74 insertions(+), 14 deletions(-) diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d5bf1ecf..60084fb8 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -54,6 +54,7 @@ namespace Microsoft.Dafny { readonly int IndentAmount = 2; void Indent(int ind) { + Contract.Requires(0 <= ind); string spaces = " "; for (; spaces.Length < ind; ind -= spaces.Length) { wr.Write(spaces); @@ -61,7 +62,8 @@ namespace Microsoft.Dafny { wr.Write(spaces.Substring(0, ind)); } - public void Compile(Program program) {Contract.Requires(program != null); + public void Compile(Program program) { + Contract.Requires(program != null); wr.WriteLine("// Dafny program {0} compiled into C#", program.Name); wr.WriteLine(); ReadRuntimeSystem(); @@ -757,6 +759,7 @@ namespace Microsoft.Dafny { } void CompileReturnBody(Expression body, int indent) { + Contract.Requires(0 <= indent); body = body.Resolved; if (body is MatchExpr) { MatchExpr me = (MatchExpr)body; @@ -1693,6 +1696,7 @@ namespace Microsoft.Dafny { Contract.Requires(sourceType != null); Contract.Requires(ctor != null); Contract.Requires(cce.NonNullElements(arguments)); + Contract.Requires(0 <= indent); // if (source.is_Ctor0) { // FormalType f0 = ((Dt_Ctor0)source._D).a0; // ... diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index b4724d0c..1b9408a8 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -212,6 +212,8 @@ namespace Microsoft.Dafny { } } + public abstract bool Equals(Type that); + public bool IsSubrangeType { get { return this is NatType; } } @@ -321,6 +323,9 @@ namespace Microsoft.Dafny { public override string TypeName(ModuleDefinition context) { return "bool"; } + public override bool Equals(Type that) { + return that.Normalize() is BoolType; + } } public class IntType : BasicType { @@ -328,6 +333,9 @@ namespace Microsoft.Dafny { public override string TypeName(ModuleDefinition context) { return "int"; } + public override bool Equals(Type that) { + return that.Normalize() is IntType; + } } public class NatType : IntType @@ -344,6 +352,9 @@ namespace Microsoft.Dafny { public override string TypeName(ModuleDefinition context) { return "object"; } + public override bool Equals(Type that) { + return that.Normalize() is ObjectType; + } } public abstract class CollectionType : NonProxyType @@ -373,6 +384,10 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result() != null); return "set<" + base.Arg.TypeName(context) + ">"; } + public override bool Equals(Type that) { + var t = that.Normalize() as SetType; + return t != null && Arg.Equals(t.Arg); + } } public class MultiSetType : CollectionType @@ -385,6 +400,10 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result() != null); return "multiset<" + base.Arg.TypeName(context) + ">"; } + public override bool Equals(Type that) { + var t = that.Normalize() as MultiSetType; + return t != null && Arg.Equals(t.Arg); + } } public class SeqType : CollectionType { @@ -397,6 +416,10 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result() != null); return "seq<" + base.Arg.TypeName(context) + ">"; } + public override bool Equals(Type that) { + var t = that.Normalize() as SeqType; + return t != null && Arg.Equals(t.Arg); + } } public class MapType : CollectionType { @@ -413,6 +436,10 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result() != null); return "map<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">"; } + public override bool Equals(Type that) { + var t = that.Normalize() as MapType; + return t != null && Arg.Equals(t.Arg); + } } public class UserDefinedType : NonProxyType @@ -520,6 +547,11 @@ namespace Microsoft.Dafny { this.Path = new List(); } + public override bool Equals(Type that) { + var t = that.Normalize() as UserDefinedType; + return t != null && ResolvedClass == t.ResolvedClass && ResolvedParam == t.ResolvedParam; + } + /// /// If type denotes a resolved class type, then return that class type. /// Otherwise, return null. @@ -617,6 +649,15 @@ namespace Microsoft.Dafny { } } } + public override bool Equals(Type that) { + var i = Normalize(); + if (i is TypeProxy) { + var u = that.Normalize() as TypeProxy; + return u != null && object.ReferenceEquals(i, u); + } else { + return i.Equals(that); + } + } } public abstract class UnrestrictedTypeProxy : TypeProxy { diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index d3847f10..726b0e99 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -338,7 +338,8 @@ namespace Microsoft.Dafny { const int IndentAmount = 2; // The amount of indent for each new scope const string BunchaSpaces = " "; void Indent(int amount) - { Contract.Requires( 0 <= amount); + { + Contract.Requires(0 <= amount); while (0 < amount) { wr.Write(BunchaSpaces.Substring(0, amount)); @@ -807,6 +808,7 @@ namespace Microsoft.Dafny { } void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody) { + Contract.Requires(0 <= indent); if (omitGuard) { wr.WriteLine("while ..."); } else { diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index e1070dad..a49b3b42 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -462,6 +462,7 @@ namespace Microsoft.Dafny moduleUnderConstruction = null; } Function CloneFunction(IToken tok, Function f, bool isGhost, List moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions, Attributes moreAttributes) { + Contract.Requires(tok != null); Contract.Requires(moreBody == null || f is Predicate); Contract.Requires(moreBody == null || replacementBody == null); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 15652c60..2d847b1e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -421,6 +421,8 @@ namespace Microsoft.Dafny } private string ModuleNotFoundErrorMessage(int i, List path) { + Contract.Requires(path != null); + Contract.Requires(0 <= i && i < path.Count); return "module " + path[i].val + " does not exist" + (1 < path.Count ? " (position " + i.ToString() + " in path " + Util.Comma(".", path, x => x.val) + ")" : ""); } @@ -4768,6 +4770,8 @@ namespace Microsoft.Dafny /// "twoState" implies that "old" and "fresh" expressions are allowed. /// void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) { + Contract.Requires(expr != null); + Contract.Requires(codeContext != null); ResolveExpression(expr, twoState, codeContext, null); } @@ -5954,7 +5958,7 @@ namespace Microsoft.Dafny // - static function or method of sig. // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored. - Contract.Requires(p < e.Tokens.Count); + Contract.Requires(0 <= p && p < e.Tokens.Count); Expression r = null; // resolved version of e CallRhs call = null; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a6d5c2e9..f0d882af 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -139,6 +139,8 @@ namespace Microsoft.Dafny { Contract.Requires(tickType != null); Contract.Requires(setTypeCtor != null); Contract.Requires(multiSetTypeCtor != null); + Contract.Requires(mapTypeCtor != null); + Contract.Requires(arrayLength != null); Contract.Requires(seqTypeCtor != null); Contract.Requires(fieldNameType != null); Contract.Requires(heap != null); @@ -427,7 +429,7 @@ namespace Microsoft.Dafny { { var thVar = new Bpl.BoundVariable(ctor.tok, new TypedIdent(ctor.tok, "this", predef.DatatypeType)); var th = new Bpl.IdentifierExpr(ctor.tok, thVar); - var queryPredicate = FunctionCall(ctor.tok, fn.Name, null, th); + var queryPredicate = FunctionCall(ctor.tok, fn.Name, Bpl.Type.Bool, th); var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th); var rhs = Bpl.Expr.Eq(ctorId, new Bpl.IdentifierExpr(ctor.tok, cid)); // this uses the "cid" defined for the previous axiom var body = Bpl.Expr.Iff(queryPredicate, rhs); @@ -552,7 +554,7 @@ namespace Microsoft.Dafny { { var dVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType)); var d = new Bpl.IdentifierExpr(dt.tok, dVar); - var lhs = FunctionCall(dt.tok, cases_fn.Name, null, d); + var lhs = FunctionCall(dt.tok, cases_fn.Name, Bpl.Type.Bool, d); Bpl.Expr cases_body = Bpl.Expr.False; foreach (DatatypeCtor ctor in dt.Ctors) { var disj = FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, d); @@ -783,10 +785,10 @@ namespace Microsoft.Dafny { var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var); var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType)); var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var); - var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, k, d0, d1); + var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1); var body = Bpl.Expr.Imp(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), prefixEq); var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar), body); - var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, null, d0, d1); + var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, Bpl.Type.Bool, d0, d1); q = new Bpl.ForallExpr(dt.tok, new VariableSeq(d0Var, d1Var), Bpl.Expr.Iff(eqDt, q)); sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q)); } @@ -802,8 +804,8 @@ namespace Microsoft.Dafny { var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var); var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType)); var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var); - var prefixEqK = FunctionCall(dt.tok, CoPrefixName(codecl, 0), null, k, d0, d1); - var prefixEqM = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, m, d0, d1); + var prefixEqK = FunctionCall(dt.tok, CoPrefixName(codecl, 0), Bpl.Type.Bool, k, d0, d1); + var prefixEqM = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, m, d0, d1); var range = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), Bpl.Expr.Le(k, m)); var body = Bpl.Expr.Imp(BplAnd(range, prefixEqM), prefixEqK); var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, mVar, d0Var, d1Var), body); @@ -821,7 +823,7 @@ namespace Microsoft.Dafny { var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var); var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType)); var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var); - var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, k, d0, d1); + var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1); var body = Bpl.Expr.Imp(BplAnd(Bpl.Expr.Eq(d0, d1), Bpl.Expr.Le(Bpl.Expr.Literal(0), k)), prefixEq); var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, d0Var, d1Var), body); sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q)); @@ -3491,6 +3493,9 @@ namespace Microsoft.Dafny { public override string TypeName(ModuleDefinition context) { return "_increasingInt"; } + public override bool Equals(Type that) { + return that.Normalize() is EverIncreasingType; + } } Expression FrameToObjectSet(List fexprs) { @@ -8660,6 +8665,7 @@ namespace Microsoft.Dafny { { Contract.Requires(tok != null); Contract.Requires(function != null); + Contract.Requires(returnType != null); Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); @@ -8837,7 +8843,7 @@ namespace Microsoft.Dafny { // checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail)) // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr // free $PrefixEqual#Dt(k, A, B); var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k); - var prefixEqK = FunctionCall(expr.tok, CoPrefixName(codecl, 1), null, k, A, B); + var prefixEqK = FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B); var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1)); // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions) var etran2 = etran.LayerOffset(1); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index e7679a11..ecf2544c 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -124,6 +124,7 @@ namespace Microsoft.Dafny public static void ErrorWriteLine(string format, params object[] args) { Contract.Requires(format != null); + Contract.Requires(args != null); string s = string.Format(format, args); ErrorWriteLine(s); } @@ -192,6 +193,7 @@ namespace Microsoft.Dafny private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName) { + Contract.Requires(dafnyProgram != null); // Compile the Dafny program into a string that contains the C# program StringWriter sw = new StringWriter(); Dafny.Compiler compiler = new Dafny.Compiler(sw); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c738f058..879ee8af 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1786,15 +1786,15 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met Calculations.dfy(3,4): Error: index out of range Execution trace: (0,0): anon0 - (0,0): anon11_Then + (0,0): anon17_Then Calculations.dfy(8,13): Error: index out of range Execution trace: (0,0): anon0 - (0,0): anon13_Then + (0,0): anon19_Then Calculations.dfy(8,17): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon13_Then + (0,0): anon19_Then Calculations.dfy(42,11): Error: assertion violation Execution trace: (0,0): anon0 -- cgit v1.2.3