fix: Improve ghost detection in comprehensions (#5041)

Fixes #5033
Fixes #5034
Fixes #5035

This PR allows more expressions as compiled (from issues #5033 and
#5034) and also adds some missing restrictions on uses of ghosts
(#5035), all having to do with set/iset/map/imap comprehensions.

### How has this been tested?

The tests from these Issues have been added to `DiscoverBounds.dfy` and
`DiscoverBoundsErrors.dfy`.

<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/AST/Expressions/Comprehensions/ComprehensionExpr.cs

@@ -266,9 +266,9 @@ public override PoolVirtues Virtues {
  var v = PoolVirtues.IndependentOfAlloc | PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc;
  if (IsFiniteCollection) {
  v |= PoolVirtues.Finite;
-  if (CollectionElementType.IsTestableToBe(BoundVariableType)) {
-  v |= PoolVirtues.Enumerable;
- }
+ }
+ if (CollectionElementType.IsTestableToBe(BoundVariableType)) {
+ v |= PoolVirtues.Enumerable;
  }
  return v;
  }

Source/DafnyCore/Resolver/ExpressionTester.cs

@@ -279,6 +279,9 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext, bool i
  if (comprehensionExpr.Range != null) {
  isCompilable = CheckIsCompilable(comprehensionExpr.Range, codeContext) && isCompilable;
  }
+ if (comprehensionExpr is MapComprehension { TermLeft: { } termLeft }) {
+ isCompilable = CheckIsCompilable(termLeft, codeContext) && isCompilable;
+ }
  isCompilable = CheckIsCompilable(comprehensionExpr.Term, codeContext) && isCompilable;
  return isCompilable;
 
@@ -546,10 +549,10 @@ public static bool UsesSpecFeatures(Expression expr) {
  return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody());
  } else if (expr is SetComprehension) {
  var e = (SetComprehension)expr;
- return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
+ return e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
  } else if (expr is MapComprehension) {
  var e = (MapComprehension)expr;
- return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || (e.TermLeft != null && UsesSpecFeatures(e.TermLeft)) || UsesSpecFeatures(e.Term);
+ return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || (e.TermLeft != null && UsesSpecFeatures(e.TermLeft)) || UsesSpecFeatures(e.Term);
  } else if (expr is LambdaExpr) {
  var e = (LambdaExpr)expr;
  return UsesSpecFeatures(e.Term);

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy

@@ -38,6 +38,8 @@ method Main()
  print x0, " ", x1, " ", x2, " ", x3, " ", x4, " ", x5, "\n";
  x0, x1, x2, x3, x4, x5 := OtherEq(true, {}, [], map[198 := 200], multiset{}, iset{}, imap[]);
  print x0, " ", x1, " ", x2, " ", x3, " ", x4, " ", x5, "\n";
+
+ EnumerateOverInfiniteCollections();
 }
 
 predicate P(x: int)
@@ -69,3 +71,35 @@ method OtherEq<U,V(==)>(b: bool, s: set<int>, t: seq<real>, u: map<U,V>, v: mult
  x' := var x'' :| x'' == x; x'';
  }
 }
+
+predicate LessThanFour(x: int) {
+ x < 4
+}
+
+method EnumerateOverInfiniteCollections() {
+ // ===== iset
+
+ var s := {3, 3, 3, 5};
+
+ // Once, the following RHS caused "u" to be auto-ghost. (Oddly enough, when using the same RHS as a
+ // separate assignment, the RHS was not considered to be ghost. So, we test both here.)
+ var u := iset x | x in s;
+ u := iset x | x in s;
+
+ // Once, the compilation of the following was rejected, because an iset was not considered enumerable. But it is.
+ var y :| y in u && LessThanFour(y); // an iset is enumerable, so it's compilable
+ print y, "\n"; // 3
+
+ // ===== imap
+
+ var m := map[3 := true, 5 := false];
+
+ // Once, the following RHS caused "u" to be auto-ghost. (Oddly enough, when using the same RHS as a
+ // separate assignment, the RHS was not considered to be ghost. So, we test both here.)
+ var w := imap x | x in m :: true;
+ w := imap x | x in m :: true;
+
+ // Once, the compilation of the following was rejected, because an imap was not considered enumerable. But it is.
+ var z :| z in w && LessThanFour(z); // an imap is enumerable, so it's compilable
+ print z, "\n"; // 3
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.expect

@@ -5,3 +5,5 @@
 -2
 {} [] map[198 := 200] multiset{} {} map[]
 {} [] map[198 := 200] multiset{} {} map[]
+3
+3

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBoundsErrors.dfy

@@ -77,3 +77,22 @@ lemma MaxExists(ks: set<K>)
  MaxExists(ks - {k});
  }
 }
+
+predicate LessThanFour(x: int) {
+ x < 4
+}
+
+ghost function PlusOne(x: int): int {
+ x + 1
+}
+
+method EnumerateOverInfiniteCollections() {
+ var s := {3, 3, 3, 5};
+ var l;
+ // Once, the TermLeft of map comprehensions was not checked for ghost-ness. Thus, the following assignment
+ // had been allowed by the resolver, which caused the compiler to emit malformed target code. (Oddly enough,
+ // when using the same RHS as an initializing assignment, the ghost-ness was detected and caused the variable
+ // to become auto-ghost which means an error is reported about the print statement not being compilable.)
+ l := map x | x in s && LessThanFour(x) :: PlusOne(x) := x;
+ print l, "\n"; // map[3 := 3]
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBoundsErrors.dfy.expect

@@ -4,4 +4,5 @@ DiscoverBoundsErrors.dfy(13,7): Error: quantifiers in non-ghost contexts must be
 DiscoverBoundsErrors.dfy(31,2): Error: forall statements in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'
 DiscoverBoundsErrors.dfy(34,2): Error: forall statements in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'
 DiscoverBoundsErrors.dfy(52,2): Error: forall statements in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'k'
-6 resolution/type errors detected in DiscoverBoundsErrors.dfy
+DiscoverBoundsErrors.dfy(96,44): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+7 resolution/type errors detected in DiscoverBoundsErrors.dfy

docs/dev/news/5041.fix

@@ -0,0 +1,3 @@
+Detect the same ghost usage in initializing assignments as in other expressions. The effect of this fix is to allow more iset/imap comprehensions to be compiled.
+
+Also, report errors if the LHS of `:=` in compiled `map`/`imap` comprehensions contains ghosts.