Fix: Support for opaque function handles (#4203)

This PR fixes #4202
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.cs

@@ -5764,6 +5764,7 @@ public string FunctionHandle(Function f) {
  functionHandles[f] = name;
  var args = new List<Bpl.Expr>();
  var vars = MkTyParamBinders(GetTypeParams(f), out args);
+ var argsRequires = new List<Bpl.Expr>(args); // Requires don't have reveal parameters
  var formals = MkTyParamFormals(GetTypeParams(f), false, true);
  var tyargs = new List<Bpl.Expr>();
  foreach (var fm in f.Formals) {
@@ -5773,9 +5774,15 @@ public string FunctionHandle(Function f) {
  if (f.IsFuelAware()) {
  vars.Add(BplBoundVar("$ly", predef.LayerType, out var ly));
  args.Add(ly);
+ argsRequires.Add(ly);
  formals.Add(BplFormalVar("$fuel", predef.LayerType, true));
  AddFuelSuccSynonymAxiom(f, true);
  }
+ if (f.IsOpaque) {
+ vars.Add(BplBoundVar("$reveal", Boogie.Type.Bool, out var reveal));
+ args.Add(reveal);
+ formals.Add(BplFormalVar("$reveal", Boogie.Type.Bool, true));
+ }
 
  Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocSelf = x => x;
  Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocPrevH = x => x;
@@ -5817,6 +5824,7 @@ public string FunctionHandle(Function f) {
  lhs_args.Add(fe);
  var be = UnboxIfBoxed(fe, fm.Type);
  rhs_args.Add(be);
+
  rhs_dict[fm] = new BoogieWrapper(be, fm.Type);
  // args and its [Box]args
  var arg = BplBoundVar(fm_name, TrType(fm.Type), func_vars);
@@ -5845,7 +5853,7 @@ public string FunctionHandle(Function f) {
  }
 
  {
- // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)
+ // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, reveal, self), Heap, arg1, ..., argN)
  // = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)
 
  var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args)));
@@ -5855,7 +5863,7 @@ public string FunctionHandle(Function f) {
  // In case this is the /requires/ or /reads/ function, then there is no precondition
  rhs = Bpl.Expr.True;
  } else {
- var args_h = f.ReadsHeap ? Snoc(SnocPrevH(args), h) : args;
+ var args_h = f.ReadsHeap ? Snoc(SnocPrevH(argsRequires), h) : argsRequires;
  rhs = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(args_h), rhs_args));
  }
 

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

@@ -0,0 +1,16 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+opaque function F(x: int): char
+{ 'D' }
+
+function InitArray<D>(f: int -> D): (a: D)
+{
+ f(44)
+}
+
+method Main() {
+ reveal F();
+ var c := InitArray(F);
+ assert c == 'D';
+}

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

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

docs/dev/news/4202.fix

@@ -0,0 +1 @@
+Support for opaque function handles