fix: A function with ghost parameters used as a value is ghost (#2847)

This PR fixes two issues: ghost parameters of function values and ghost parameters of arrow types. * Enforce that a non-ghost function with ghost parameters can be used as a value only in ghost contexts. For example, disallow `var f := F;` if `f` is compiled and `F` is a function with ghost parameters. * Disallow arrow types that look like they have ghost parameters. For example, disallow an attempted arrow type like `(ghost int) -> int`. Fixes #2843 <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>
dafny-lang · Oct 11, 2022 · 7c207ae · 7c207ae
1 parent 030cf95
commit 7c207ae
Show file tree

Hide file tree

Showing 7 changed files with 110 additions and 17 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -3,6 +3,7 @@
 - fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854)
 - fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)
 - fix: Handle sequence-to-string equality correctly in the JavaScript runtime (https://github.com/dafny-lang/dafny/pull/2877)
+- fix: A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (https://github.com/dafny-lang/dafny/pull/2847)
 
 # 3.9.0
 

diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
@@ -2108,7 +2108,7 @@ TypeAndToken<out IToken tok, out Type ty, bool inExpressionContext>
      ty = new BoolType();  /*keep compiler happy*/
      List<Type> gt;
      List<Type> tupleArgTypes = null;
-     List<bool> argumentGhostness = null;
+     List<IToken> argumentGhostTokens = null;
   .)
   ( "bool"                          (. tok = t; .)
   | "char"                          (. tok = t;  ty = new CharType(); .)
@@ -2182,7 +2182,7 @@ TypeAndToken<out IToken tok, out Type ty, bool inExpressionContext>
                                        int dims = StringToInt(dimString, 1, "arrays of that many dimensions");
                                        ty = theBuiltIns.ArrayType(tok, dims, gt, true, q);
                                     .)
-  | TupleType<out ty, out tok, out tupleArgTypes, out argumentGhostness>
+  | TupleType<out ty, out tok, out tupleArgTypes, out argumentGhostTokens>
   | NamedType<out ty, out tok, inExpressionContext>
   )
   [ (. int arrowKind = 0; /* 0: any, 1: partial, 2: total */
@@ -2193,10 +2193,14 @@ TypeAndToken<out IToken tok, out Type ty, bool inExpressionContext>
     | "->"           (. tok = t; arrowKind = 2; .)
     )
     Type<out t2>
-    (. if (tupleArgTypes != null) {
-         gt = tupleArgTypes;
-        } else {
+    (. if (tupleArgTypes == null) {
          gt = new List<Type>{ ty };
+       } else {
+         // make sure no "ghost" keyword was used in the tuple-looking type
+         foreach (var ghostToken in argumentGhostTokens.Where(ghostToken => ghostToken != null)) {
+           SemErr(ghostToken, $"arrow-type arguments may not be declared as 'ghost'");
+         }
+         gt = tupleArgTypes;
        }
        var arity = gt.Count;
        theBuiltIns.CreateArrowTypeDecl(arity);
@@ -2216,26 +2220,27 @@ TypeAndToken<out IToken tok, out Type ty, bool inExpressionContext>
 
 /*------------------------------------------------------------------------*/
 
-TupleType<.out Type ty, out IToken tok, out List<Type> tupleArgTypes, out List<bool> argumentGhostness.> =
+TupleType<.out Type ty, out IToken tok, out List<Type> tupleArgTypes, out List<IToken> argumentGhostTokens.> =
   "("                             (. tok = t;
                                      ty = null; // To keep compiler happy
                                      tupleArgTypes = new List<Type>();
-                                     var isGhost = false;
-                                     argumentGhostness = new List<bool>();
+                                     IToken ghostToken = null;
+                                     argumentGhostTokens = new List<IToken>();
                                   .)
-  [ [ "ghost"                     (. isGhost = true; .)
+  [ [ "ghost"                     (. ghostToken = t; .)
     ]
-    Type<out ty>                  (. tupleArgTypes.Add(ty); argumentGhostness.Add(isGhost); .)
-    { ","                         (. isGhost = false; .)
-      [ "ghost"                   (. isGhost = true; .)
+    Type<out ty>                  (. tupleArgTypes.Add(ty); argumentGhostTokens.Add(ghostToken); .)
+    { ","                         (. ghostToken = null; .)
+      [ "ghost"                   (. ghostToken = t; .)
       ]
-      Type<out ty>                (. tupleArgTypes.Add(ty); argumentGhostness.Add(isGhost); .)
+      Type<out ty>                (. tupleArgTypes.Add(ty); argumentGhostTokens.Add(ghostToken); .)
     }
   ]
-  ")"                             (. if (tupleArgTypes.Count == 1 && !isGhost) {
+  ")"                             (. if (tupleArgTypes.Count == 1 && argumentGhostTokens[0] == null) {
                                        // just return the type 'ty'
                                      } else {
                                        var dims = tupleArgTypes.Count;
+                                       var argumentGhostness = argumentGhostTokens.ConvertAll(tok => tok != null);
                                        var tmp = theBuiltIns.TupleType(tok, dims, true, argumentGhostness);  // make sure the tuple type exists
                                        ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(argumentGhostness), dims == 0 ? null : tupleArgTypes);
                                      }

diff --git a/Source/DafnyCore/Util.cs b/Source/DafnyCore/Util.cs
@@ -857,6 +857,10 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) {
           var what = selectExpr.Member.WhatKindMentionGhost;
           reporter?.Error(MessageSource.Resolver, selectExpr, $"a {what} is allowed only in specification contexts");
           return false;
+        } else if (selectExpr.Member is Function function && function.Formals.Any(formal => formal.IsGhost)) {
+          var what = selectExpr.Member.WhatKindMentionGhost;
+          reporter?.Error(MessageSource.Resolver, selectExpr, $"a {what} with ghost parameters can be used as a value only in specification contexts");
+          return false;
         } else if (selectExpr.Member is DatatypeDestructor dtor && dtor.EnclosingCtors.All(ctor => ctor.IsGhost)) {
           var what = selectExpr.Member.WhatKind;
           reporter?.Error(MessageSource.Resolver, selectExpr, $"{what} '{selectExpr.MemberName}' can be used only in specification contexts");
@@ -1167,6 +1171,8 @@ public static bool UsesSpecFeatures(Expression expr) {
           return true;
         } else if (e.Member != null && e.Member.IsGhost) {
           return true;
+        } else if (e.Member is Function function && function.Formals.Any(formal => formal.IsGhost)) {
+          return true;
         } else if (e.Member is DatatypeDestructor dtor) {
           return dtor.EnclosingCtors.All(ctor => ctor.IsGhost);
         } else {

diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
@@ -261,4 +261,18 @@ module Older {
   twostate lemma L(nameonly older nameonly c: C := "hello") // error: 'older' is an identifier here
 }
 
-newtype T {}
+// ---------------------- ghost arguments of arrow types -----------------------------------
+
+module ArrowTypes {
+  const f: (ghost int, int) -> int // error: arrow-type arguments are not allowed to be ghost
+
+  method M() {
+    var g: (real, (ghost int, int), bool) -> int;
+    var h: ((ghost int, int)) -> int;
+    var i: (bool, ghost real, int, ghost bv6) -> ORDINAL; // error (x2): ghost not allowed
+  }
+}
+
+// ---------------------- invalid newtype definition -----------------------------------
+
+newtype T {} // error: newtype is expected to have an '='
diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect
@@ -79,5 +79,8 @@ ParseErrors.dfy(255,32): Error: formal cannot be declared 'older' in this contex
 ParseErrors.dfy(256,11): Error: formal cannot be declared 'older' in this context
 ParseErrors.dfy(257,17): Error: formal cannot be declared 'older' in this context
 ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this context
-ParseErrors.dfy(264,10): Error: invalid NewtypeDecl
-77 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(267,12): Error: arrow-type arguments may not be declared as 'ghost'
+ParseErrors.dfy(272,18): Error: arrow-type arguments may not be declared as 'ghost'
+ParseErrors.dfy(272,35): Error: arrow-type arguments may not be declared as 'ghost'
+ParseErrors.dfy(278,10): Error: invalid NewtypeDecl
+80 parse errors detected in ParseErrors.dfy
diff --git a/Test/git-issues/git-issue-2843.dfy b/Test/git-issues/git-issue-2843.dfy
@@ -0,0 +1,54 @@
+// RUN: %dafny_0 /functionSyntax:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function F(ghost x: int, y: int): int {
+  y
+}
+
+ghost function G(x: int, y: int): int {
+  y
+}
+
+method M0() {
+  var f: (int, int) -> int;
+  f := F; // error: the expression `F` is ghost, since function F has a ghost parameter
+  print F(2, 3), " ", f(2, 3), "\n";
+}
+
+method M1() {
+  var g: (int, int) -> int;
+  g := G; // error: G is ghost
+  print g(2, 3), "\n";
+}
+
+method M2() {
+  ghost var f: (int, int) -> int;
+  f := F; // fine, since f is ghost
+  f := G; // fine
+}
+
+method M3() {
+  var f := F; // f is auto-ghost
+  var g := G; // g is auto-ghost
+  print f(2, 3), " ", g(2, 3), "\n"; // error (x2): f and g are ghost
+
+  var tuple0: (ghost (int, int) -> int, int, ghost (int, int) -> int);
+  tuple0 := (ghost F, 10, ghost G);
+  tuple0 := (ghost f, 10, ghost g);
+  print tuple0, "\n";
+
+  var tuple1; // type is inferred (same as for tuple0 above)
+  tuple1 := (ghost F, 10, ghost G);
+  tuple1 := (ghost f, 10, ghost g);
+  print tuple1, "\n";
+
+  var tuple2: ((int, int) -> int, int, (int, int) -> int);
+  tuple2 := (F, 10, G); // error (x2): F has ghost parameters and G is ghost
+  tuple2 := (f, 10, g); // error (x2): f and g are ghost variables
+  print tuple2, "\n";
+
+  ghost var tuple3: ((int, int) -> int, int, (int, int) -> int);
+  tuple3 := (F, 10, G);
+  tuple3 := (f, 10, g);
+  print tuple3, "\n"; // error: cannot print a ghost
+}
diff --git a/Test/git-issues/git-issue-2843.dfy.expect b/Test/git-issues/git-issue-2843.dfy.expect
@@ -0,0 +1,10 @@
+git-issue-2843.dfy(14,7): Error: a function with ghost parameters can be used as a value only in specification contexts
+git-issue-2843.dfy(20,7): Error: a ghost function is allowed only in specification contexts
+git-issue-2843.dfy(33,8): Error: a ghost variable is allowed only in specification contexts
+git-issue-2843.dfy(33,22): Error: a ghost variable is allowed only in specification contexts
+git-issue-2843.dfy(46,13): Error: a function with ghost parameters can be used as a value only in specification contexts
+git-issue-2843.dfy(46,20): Error: a ghost function is allowed only in specification contexts
+git-issue-2843.dfy(47,13): Error: a ghost variable is allowed only in specification contexts
+git-issue-2843.dfy(47,20): Error: a ghost variable is allowed only in specification contexts
+git-issue-2843.dfy(53,8): Error: a ghost variable is allowed only in specification contexts
+9 resolution/type errors detected in git-issue-2843.dfy