From 9c8ad44b64373fb9d85aef5a05809e8e25416684 Mon Sep 17 00:00:00 2001 From: leino Date: Fri, 3 Apr 2015 21:44:11 -0700 Subject: Added test cases and fixes for overrides termination checks Removed syntactic presence checks for specifications--these will be checked semantically by the verifier --- Source/Dafny/Resolver.cs | 43 ++------- Source/Dafny/Translator.cs | 87 ++++++++++++------ Test/dafny0/Trait/TraitSpecsOverride0.dfy | 19 +++- Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect | 7 +- Test/dafny0/Trait/TraitsDecreases.dfy | 108 +++++++++++++++++++++++ Test/dafny0/Trait/TraitsDecreases.dfy.expect | 17 ++++ 6 files changed, 210 insertions(+), 71 deletions(-) create mode 100644 Test/dafny0/Trait/TraitsDecreases.dfy create mode 100644 Test/dafny0/Trait/TraitsDecreases.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bf417de7..727011e8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2952,25 +2952,6 @@ namespace Microsoft.Dafny classMethod.OverriddenMethod = traitMethod; //adding a call graph edge from the trait method to that of class cl.Module.CallGraph.AddEdge(traitMethod, classMethod); - - //checking specifications - //class method must provide its own specifications in case the overriden method has provided any - if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req - { - Error(classMethod, "Method must provide its own Requires clauses anew"); - } - if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens - { - Error(classMethod, "Method must provide its own Ensures clauses anew"); - } - if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod - { - Error(classMethod, "Method must provide its own Modifies clauses anew"); - } - if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases - { - Error(classMethod, "Method must provide its own Decreases clauses anew"); - } } } else if (traitMem.Value is Function) @@ -2985,25 +2966,6 @@ namespace Microsoft.Dafny classFunction.OverriddenFunction = traitFunction; //adding a call graph edge from the trait function to that of class cl.Module.CallGraph.AddEdge(traitFunction, classFunction); - - //checking specifications - //class function must provide its own specifications in case the overriden function has provided any - if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req - { - Error(classFunction, "Function must provide its own Requires clauses anew"); - } - if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens - { - Error(classFunction, "Function must provide its own Ensures clauses anew"); - } - if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod - { - Error(classFunction, "Function must provide its own Reads clauses anew"); - } - if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases - { - Error(classFunction, "Function must provide its own Decreases clauses anew"); - } } } else if (traitMem.Value is Field) @@ -3058,6 +3020,11 @@ namespace Microsoft.Dafny { Method classMethod = (Method)classMem; refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod); + var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr); + var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr); + if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) { + Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name); + } } if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null) Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 96405daf..8678e2c3 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3405,33 +3405,68 @@ namespace Microsoft.Dafny { } } - private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary substMap) - { - var decrToks = new List(); - var decrTypes1 = new List(); - var decrTypes2 = new List(); - var decrClass = new List(); - var decrTrait = new List(); - if (m.Decreases != null) - { - foreach (var decC in m.Decreases.Expressions) - { - decrToks.Add(decC.tok); - decrTypes1.Add(decC.Type); - decrClass.Add(etran.TrExpr(decC)); - } - } - if (m.OverriddenMethod.Decreases != null) - { - foreach (var decT in m.OverriddenMethod.Decreases.Expressions) - { - var decCNew = Substitute(decT, null, substMap); - decrTypes2.Add(decCNew.Type); - decrTrait.Add(etran.TrExpr(decCNew)); - } + private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary substMap) { + Contract.Requires(m != null); + Contract.Requires(builder != null); + Contract.Requires(etran != null); + Contract.Requires(substMap != null); + // Note, it is as if the trait's method is calling the class's method. + var contextDecreases = m.OverriddenMethod.Decreases.Expressions; + var calleeDecreases = m.Decreases.Expressions; + // We want to check: calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches) + if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) { + // no check needed + return; + } + + int N = Math.Min(contextDecreases.Count, calleeDecreases.Count); + var toks = new List(); + var types0 = new List(); + var types1 = new List(); + var callee = new List(); + var caller = new List(); + + for (int i = 0; i < N; i++) { + Expression e0 = calleeDecreases[i]; + Expression e1 = Substitute(contextDecreases[i], null, substMap); + if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) { + N = i; + break; } - var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false); - builder.Add(new Bpl.AssertCmd(m.tok, decrChk)); + toks.Add(new NestedToken(m.tok, e1.tok)); + types0.Add(e0.Type.NormalizeExpand()); + types1.Add(e1.Type.NormalizeExpand()); + callee.Add(etran.TrExpr(e0)); + caller.Add(etran.TrExpr(e1)); + } + + var decrCountT = contextDecreases.Count; + var decrCountC = calleeDecreases.Count; + // Generally, we want to produce a check "decrClass <= decrTrait", allowing (the common case where) they are equal. + // * If N < decrCountC && N < decrCountT, then "decrClass <= decrTrait" if the comparison ever gets beyond the + // parts that survived truncation. Thus, we compare with "allowNoChange" set to "false". + // Otherwise: + // * If decrCountC == decrCountT, then the truncation we did above had no effect and we pass in "allowNoChange" as "true". + // * If decrCountC > decrCountT, then we will have truncated decrClass above. Let x,y and x' denote decrClass and + // decrTrait, respectively, where x and x' have the same length. Considering how Dafny in effect pads the end of + // decreases tuples with a \top, we were supposed to evaluate (x,(y,\top)) <= (x',\top), which by lexicographic pairs + // we can expand to: + // x <= x' && (x == x' ==> (y,\top) <= \top) + // which is equivalent to just x <= x'. Thus, we called DecreasesCheck to compare x and x' and we pass in "allowNoChange" + // as "true". + // * If decrCountC < decrCountT, then we will have truncated decrTrait above. Let x and x',y' denote decrClass and + // decrTrait, respectively, where x and x' have the same length. We then want to check (x,\top) <= (x',(y',\top)), which + // expands to: + // x <= x' && (x == x' ==> \top <= (y',\top)) + // = { \top is strictly larger than a pair } + // x <= x' && (x == x' ==> false) + // = + // x < x' + // So we perform our desired check by calling DecreasesCheck to strictly compare x and x', so we pass in "allowNoChange" + // as "false". + bool allowNoChange = N == decrCountT && decrCountT <= decrCountC; + var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false); + builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait")); } private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List localVariables, Dictionary substMap) diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy index 614adc2d..7e16c630 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -7,6 +7,7 @@ trait J function method F(k:int, y: array): int reads y; decreases k; + ensures F(k, y) < 100 function method G(y: int): int { @@ -36,12 +37,14 @@ trait J class C extends J { + // F's postcondition (true) is too weak, but that won't be detected until verification time function method F(kk:int, yy: array): int { 200 } - method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications + // M's postcondition (true) is too weak, but that won't be detected until verification time + method M(kk:int) returns (ksos:int) { ksos:=10; } @@ -56,4 +59,16 @@ class C extends J y1[0] := a1 + b1; c1 := a1 + b1; } -} \ No newline at end of file +} + +module BadNonTermination { + trait TT1 { + method N(x: int) + decreases x + } + class CC1 extends TT1 { + method N(x: int) + decreases * // error: can't override a terminating method with a possibly non-terminating method + { } + } +} diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect index 750e13e0..2281c604 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -1,5 +1,2 @@ -TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Reads clauses anew -TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Decreases clauses anew -TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Requires clauses anew -TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Ensures clauses anew -4 resolution/type errors detected in TraitSpecsOverride0.dfy +TraitSpecsOverride0.dfy(70,11): Error: not allowed to override a terminating method with a possibly non-terminating method ('N') +1 resolution/type errors detected in TraitSpecsOverride0.dfy diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy new file mode 100644 index 00000000..53ce28be --- /dev/null +++ b/Test/dafny0/Trait/TraitsDecreases.dfy @@ -0,0 +1,108 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +trait Trait { + // ----------------------- + method A0(x: nat) + // default decreases: x + method A1(x: nat) + // default decreases: x + method A2(x: nat) + decreases x + method A3(x: nat) + decreases x + // ----------------------- + method G0(x: nat, y: bool) + decreases x, y + method G1(x: nat, y: bool) + decreases x+1, y + method G2(x: nat, y: bool) + decreases x + method G3(x: nat, y: bool) + decreases x+1, y + method G4(x: nat, y: bool) + decreases y, x + method G5(x: nat, y: bool) + decreases y, x + method G6(x: nat, y: bool) + decreases true, x + method G7(x: nat, y: bool) + decreases false, x + method G8(x: nat, y: bool) + requires x < 100 + decreases 120, y + method G9(x: nat, y: bool) + requires x < 100 + decreases 120, y + method G10(x: nat, y: bool) + requires x < 100 + decreases x, y +} + +class Class extends Trait { + // ----------------------- + method A0(x: nat) + // default decreases: x + { } + method A1(x: nat) + decreases x + { } + method A2(x: nat) + // default decreases: x + { } + method A3(x: nat) + decreases x + { } + // ----------------------- + method G0(x: nat, y: bool) + decreases y, x // error: opposite order from default + { } + method G1(x: nat, y: bool) + decreases x, x // fine -- it's below the one in the trait + { } + method G2(x: nat, y: bool) // fine -- (x,y) is below the trait's (x,\top) + // default decreases: x, y + { } + method G3(x: nat, y: bool) + decreases x, y // fine -- trait decrease is above this one + { } + method G4(x: nat, y: bool) + decreases y, x+1 // error: this decreases is above the trait's decreases + { } + method G5(x: nat, y: bool) + decreases y // error: this is above the trait's decreases clause + { } + method G6(x: nat, y: bool) + decreases y, x // good -- this is the same or below the one in the trait + { } + method G7(x: nat, y: bool) + decreases y, x // error: this might be above the one in the trait + { } + method G8(x: nat, y: bool) + decreases x, y // fine -- given the precondition in the trait, this is below the one in the trait + { } + method G9(x: nat, y: bool) + requires x < 105 + decreases 120, y // fine -- given the precondition in the trait, this is below the one in the trait + { } + method G10(x: nat, y: bool) + requires x < 100 + decreases 120, y // error: this is above the one in the trait + { } +} + + +trait TT { + method M(x: int) + decreases * + method P(x: int) + decreases * +} +class CC extends TT { + method M(x: int) + decreases x + { } + method P(x: int) + decreases * + { } +} diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect new file mode 100644 index 00000000..6c76f9a8 --- /dev/null +++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect @@ -0,0 +1,17 @@ +TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait +Execution trace: + (0,0): anon0 +TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait +Execution trace: + (0,0): anon0 +TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait +Execution trace: + (0,0): anon0 +TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait +Execution trace: + (0,0): anon0 +TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 63 verified, 5 errors -- cgit v1.2.3