Fix: Handling of opaque methods in traits overriding check (#4207)

This PR fixes #4205
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -1058,6 +1058,7 @@ public partial class Translator {
 
  var moreArgsCF = new List<Boogie.Expr>();
  Expr layer = null;
+ Expr reveal = null;
 
  // Add the fuel argument
  if (f.IsFuelAware()) {
@@ -1072,6 +1073,18 @@ public partial class Translator {
  layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
  }
 
+ if (f.IsOpaque) {
+ Contract.Assert(overridingFunction.IsOpaque);
+ var revealVar = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "reveal", Boogie.Type.Bool));
+ forallFormals.Add(revealVar);
+ reveal = new Boogie.IdentifierExpr(f.tok, revealVar);
+ argsJF.Add(reveal);
+ } else if (overridingFunction.IsOpaque) {
+ // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel.
+ // Instead, we do the next best thing: use the literal false.
+ reveal = new Boogie.LiteralExpr(f.tok, false);
+ }
+
  // Add heap arguments
  if (f is TwoStateFunction) {
  Contract.Assert(bvPrevHeap != null);
@@ -1127,6 +1140,10 @@ public partial class Translator {
  argsCF.Add(layer);
  }
 
+ if (reveal != null) {
+ argsCF.Add(reveal);
+ }
+
  argsCF = Concat(argsCF, moreArgsCF);
 
  // ante := useViaCanCall || (useViaContext && this != null && $Is(this, C))

Source/DafnyCore/Verifier/Translator.cs

@@ -3580,6 +3580,10 @@ public enum StmtType { NONE, ASSERT, ASSUME };
  argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
  }
 
+ if (f.IsOpaque) {
+ argsC.Add(GetRevealConstant(f));
+ }
+
  // add heap arguments
  if (f is TwoStateFunction) {
  argsC.Add(etran.Old.HeapExpr);

Test/git-issues/git-issue-4205.dfy

@@ -0,0 +1,12 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+ opaque function bar(): int
+}
+
+class F extends T {
+ opaque function bar(): int {
+ 1
+ }
+}

Test/git-issues/git-issue-4205.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Test/git-issues/git-issue-4205a.dfy

@@ -0,0 +1,13 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+ opaque function bar(): (r: int)
+}
+
+class F extends T {
+ constructor() {}
+ opaque function bar(): (r: int) {
+ 1
+ }
+}

Test/git-issues/git-issue-4205a.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/4205.fix

@@ -0,0 +1 @@
+Traits with opaque functions can now be extended without errors