From 73fcdf32d81ab61a8262cbf62a4b59f7fc95747d Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 15 Feb 2024 00:35:19 +0100 Subject: [PATCH] fix: Termination override check for certain non-reference trait implementations (#5087) --- .../Verifier/BoogieGenerator.Methods.cs | 11 +++- .../Verifier/FunctionCallSubstituter.cs | 14 ++--- .../LitTest/git-issues/git-issue-4982.dfy | 55 +++++++++++++++++++ .../git-issues/git-issue-4982.dfy.expect | 2 + docs/dev/news/5087.fix | 1 + 5 files changed, 75 insertions(+), 8 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect create mode 100644 docs/dev/news/5087.fix diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index d8320ac1ff..36d88d7a24 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -1461,6 +1461,9 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo // Note, it is as if the trait's method is calling the class's method. var contextDecreases = overryd.Decreases.Expressions; var calleeDecreases = original.Decreases.Expressions; + var T = (TraitDecl)((MemberDecl)overryd).EnclosingClass; + var I = (TopLevelDeclWithMembers)((MemberDecl)original).EnclosingClass; + // 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 @@ -1473,10 +1476,12 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo var types1 = new List(); var callee = new List(); var caller = new List(); + FunctionCallSubstituter sub = null; for (int i = 0; i < N; i++) { Expression e0 = calleeDecreases[i]; - Expression e1 = Substitute(contextDecreases[i], null, substMap, typeMap); + sub ??= new FunctionCallSubstituter(substMap, typeMap, T, I); + Expression e1 = sub.Substitute(contextDecreases[i]); if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) { N = i; break; @@ -1486,6 +1491,10 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo types1.Add(e1.Type.NormalizeExpand()); callee.Add(etran.TrExpr(e0)); caller.Add(etran.TrExpr(e1)); + var canCall = etran.CanCallAssumption(e1); + if (canCall != Bpl.Expr.True) { + builder.Add(new Bpl.AssumeCmd(e1.tok, canCall)); + } } var decrCountT = contextDecreases.Count; diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index 3f4c147f95..0e6d06f40f 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -4,16 +4,16 @@ namespace Microsoft.Dafny { public class FunctionCallSubstituter : Substituter { public readonly TraitDecl Tr; - public readonly TopLevelDeclWithMembers Cl; + public readonly TopLevelDeclWithMembers Impl; // We replace all occurrences of the trait version of the function with the class version. This is only allowed if // the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex // expressions that evaluate to one. public FunctionCallSubstituter(Dictionary /*!*/ substMap, Dictionary typeMap, - TraitDecl parentTrait, TopLevelDeclWithMembers cl) - : base(new ThisExpr(cl.tok) { Type = UserDefinedType.FromTopLevelDecl(cl.tok, cl) }, substMap, typeMap) { - this.Tr = parentTrait; - this.Cl = cl; + TraitDecl parentTrait, TopLevelDeclWithMembers impl) + : base(new ThisExpr(impl.tok) { Type = UserDefinedType.FromTopLevelDecl(impl.tok, impl) }, substMap, typeMap) { + Tr = parentTrait; + Impl = impl; } public override Expression Substitute(Expression expr) { @@ -24,10 +24,10 @@ public override Expression Substitute(Expression expr) { Function function; if ((e.Function.EnclosingClass == Tr || Tr.InheritedMembers.Contains(e.Function)) && e.Receiver.Resolved is ThisExpr && receiver.Resolved is ThisExpr && - Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) { + Impl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) { receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass); function = (Function)f; - typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Cl).TypeArgs.ToList(); + typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Impl).TypeArgs.ToList(); } else { function = e.Function; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy new file mode 100644 index 0000000000..18c2730a91 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy @@ -0,0 +1,55 @@ +// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype + +trait Tr1 { + function Decrease(): nat { + 0 + } + + function F(): nat + decreases Decrease() +} + +datatype Dt1 extends Tr1 = Dt { + function F(): nat + decreases 0 + { + 0 + } +} + +trait Tr2 { + function Decrease(): nat { + 0 + } + + function F(): A + decreases Decrease() +} + +datatype Dt2 extends Tr2 = Dt { + function F(): nat + decreases 0 + { + 0 + } +} + +trait ProgramTrait { + function Rank(): nat + + method Compute() returns (r: Result) + decreases Rank() +} + +datatype Result = Bounce(next: ProgramTrait) | Done + +datatype Trivial extends ProgramTrait = Trivial +{ + function Rank(): nat { 0 } + + method Compute() returns (r: Result) + decreases Rank() + { + return Done(); + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect new file mode 100644 index 0000000000..1981561ca0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 10 verified, 0 errors diff --git a/docs/dev/news/5087.fix b/docs/dev/news/5087.fix new file mode 100644 index 0000000000..1003d396e5 --- /dev/null +++ b/docs/dev/news/5087.fix @@ -0,0 +1 @@ +Termination override check for certain non-reference trait implementations \ No newline at end of file