fix: Verify that all compilable expressions are compilable

RELEASE_NOTES.md

@@ -1,6 +1,7 @@
 # Upcoming
 
 - feat: Support for the `{:opaque}` attibute on `const`
+- fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 
 
 # 3.8.0

Source/Dafny/AST/DafnyAst.cs

@@ -4906,6 +4906,7 @@ public bool AllowsNontermination {
 
   public abstract class MemberDecl : Declaration {
     public abstract string WhatKind { get; }
+    public virtual string WhatKindMentionGhost => (IsGhost ? "ghost " : "") + WhatKind;
     public readonly bool HasStaticKeyword;
     public virtual bool IsStatic {
       get {
@@ -4991,7 +4992,7 @@ public virtual string FullSanitizedName {
   }
 
   public class Field : MemberDecl {
-    public override string WhatKind { get { return "field"; } }
+    public override string WhatKind => "field";
     public readonly bool IsMutable;  // says whether or not the field can ever change values
     public readonly bool IsUserMutable;  // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
     public readonly Type Type;
@@ -5052,15 +5053,17 @@ public enum ID {
     }
     public readonly ID SpecialId;
     public readonly object IdParam;
-    public SpecialField(IToken tok, string name, ID specialId, object idParam, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
+    public SpecialField(IToken tok, string name, ID specialId, object idParam,
+      bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
       : this(tok, name, specialId, idParam, false, isGhost, isMutable, isUserMutable, type, attributes) {
       Contract.Requires(tok != null);
       Contract.Requires(name != null);
       Contract.Requires(!isUserMutable || isMutable);
       Contract.Requires(type != null);
     }
 
-    public SpecialField(IToken tok, string name, ID specialId, object idParam, bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
+    public SpecialField(IToken tok, string name, ID specialId, object idParam,
+      bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes)
       : base(tok, name, hasStaticKeyword, isGhost, isMutable, isUserMutable, type, attributes) {
       Contract.Requires(tok != null);
       Contract.Requires(name != null);
@@ -5150,7 +5153,7 @@ static internal string PrintableCtorNameList(List<DatatypeCtor> ctors, string gr
   }
 
   public class ConstantField : SpecialField, ICallable {
-    public override string WhatKind { get { return "const field"; } }
+    public override string WhatKind => "const field";
     public readonly Expression Rhs;
     public ConstantField(IToken tok, string name, Expression/*?*/ rhs, bool hasStaticKeyword, bool isGhost, Type type, Attributes attributes)
       : base(tok, name, SpecialField.ID.UseIdParam, NonglobalVariable.SanitizeName(name), hasStaticKeyword, isGhost, false, false, type, attributes) {
@@ -5958,7 +5961,7 @@ public void AcceptArgumentExpressionsAsExactParameterList(List<Expression> args
   }
 
   public class Function : MemberDecl, TypeParameter.ParentType, ICallable {
-    public override string WhatKind { get { return "function"; } }
+    public override string WhatKind => "function";
 
     public string FunctionDeclarationKeywords {
       get {
@@ -6169,7 +6172,7 @@ bool ICallable.InferredDecreases {
   }
 
   public class Predicate : Function {
-    public override string WhatKind { get { return "predicate"; } }
+    public override string WhatKind => "predicate";
     public enum BodyOriginKind {
       OriginalOrInherited,  // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example)
       DelayedDefinition,  // this predicate declaration provides, for the first time, a body--the declaration refines a previously declared predicate, but the previous one had no body
@@ -6191,7 +6194,8 @@ public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isGhost,
   /// An PrefixPredicate is the inductive unrolling P# implicitly declared for every extreme predicate P.
   /// </summary>
   public class PrefixPredicate : Function {
-    public override string WhatKind { get { return "prefix predicate"; } }
+    public override string WhatKind => "prefix predicate";
+    public override string WhatKindMentionGhost => WhatKind;
     public readonly Formal K;
     public readonly ExtremePredicate ExtremePred;
     public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword,
@@ -6208,6 +6212,7 @@ public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword,
   }
 
   public abstract class ExtremePredicate : Function {
+    public override string WhatKindMentionGhost => WhatKind;
     public enum KType { Unspecified, Nat, ORDINAL }
     public readonly KType TypeOfK;
     public bool KNat {
@@ -6250,7 +6255,7 @@ public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Express
   }
 
   public class LeastPredicate : ExtremePredicate {
-    public override string WhatKind { get { return "least predicate"; } }
+    public override string WhatKind => "least predicate";
     public LeastPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK,
       List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
@@ -6261,7 +6266,7 @@ public LeastPredicate(IToken tok, string name, bool hasStaticKeyword, KType type
   }
 
   public class GreatestPredicate : ExtremePredicate {
-    public override string WhatKind { get { return "greatest predicate"; } }
+    public override string WhatKind => "greatest predicate";
     public GreatestPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK,
       List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
@@ -6272,7 +6277,8 @@ public GreatestPredicate(IToken tok, string name, bool hasStaticKeyword, KType t
   }
 
   public class TwoStateFunction : Function {
-    public override string WhatKind { get { return "twostate function"; } }
+    public override string WhatKind => "twostate function";
+    public override string WhatKindMentionGhost => WhatKind;
     public TwoStateFunction(IToken tok, string name, bool hasStaticKeyword,
                      List<TypeParameter> typeArgs, List<Formal> formals, Formal result, Type resultType,
                      List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
@@ -6292,7 +6298,7 @@ public TwoStateFunction(IToken tok, string name, bool hasStaticKeyword,
   }
 
   public class TwoStatePredicate : TwoStateFunction {
-    public override string WhatKind { get { return "twostate predicate"; } }
+    public override string WhatKind => "twostate predicate";
     public TwoStatePredicate(IToken tok, string name, bool hasStaticKeyword,
                      List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
                      List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
@@ -6310,7 +6316,7 @@ public TwoStatePredicate(IToken tok, string name, bool hasStaticKeyword,
   }
 
   public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext {
-    public override string WhatKind { get { return "method"; } }
+    public override string WhatKind => "method";
     public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } }
     public readonly IToken SignatureEllipsis;
     public readonly bool IsByMethod;
@@ -6472,7 +6478,8 @@ public BlockStmt BodyForRefinement {
   }
 
   public class Lemma : Method {
-    public override string WhatKind { get { return "lemma"; } }
+    public override string WhatKind => "lemma";
+    public override string WhatKindMentionGhost => WhatKind;
     public Lemma(IToken tok, string name,
                  bool hasStaticKeyword,
                  [Captured] List<TypeParameter> typeArgs,
@@ -6489,7 +6496,9 @@ public Lemma(IToken tok, string name,
   }
 
   public class TwoStateLemma : Method {
-    public override string WhatKind { get { return "twostate lemma"; } }
+    public override string WhatKind => "twostate lemma";
+    public override string WhatKindMentionGhost => WhatKind;
+
     public TwoStateLemma(IToken tok, string name,
                  bool hasStaticKeyword,
                  [Captured] List<TypeParameter> typeArgs,
@@ -6516,7 +6525,7 @@ public TwoStateLemma(IToken tok, string name,
   }
 
   public class Constructor : Method {
-    public override string WhatKind { get { return "constructor"; } }
+    public override string WhatKind => "constructor";
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(Body == null || Body is DividedBlockStmt);
@@ -6570,7 +6579,9 @@ public bool HasName {
   /// A PrefixLemma is the inductive unrolling M# implicitly declared for every extreme lemma M.
   /// </summary>
   public class PrefixLemma : Method {
-    public override string WhatKind { get { return "prefix lemma"; } }
+    public override string WhatKind => "prefix lemma";
+    public override string WhatKindMentionGhost => WhatKind;
+
     public readonly Formal K;
     public readonly ExtremeLemma ExtremeLemma;
     public PrefixLemma(IToken tok, string name, bool hasStaticKeyword,
@@ -6589,6 +6600,7 @@ public PrefixLemma(IToken tok, string name, bool hasStaticKeyword,
   }
 
   public abstract class ExtremeLemma : Method {
+    public override string WhatKindMentionGhost => WhatKind;
     public readonly ExtremePredicate.KType TypeOfK;
     public bool KNat {
       get {
@@ -6623,7 +6635,7 @@ public ExtremeLemma(IToken tok, string name,
   }
 
   public class LeastLemma : ExtremeLemma {
-    public override string WhatKind { get { return "least lemma"; } }
+    public override string WhatKind => "least lemma";
 
     public LeastLemma(IToken tok, string name,
                           bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
@@ -6648,7 +6660,7 @@ public LeastLemma(IToken tok, string name,
   }
 
   public class GreatestLemma : ExtremeLemma {
-    public override string WhatKind { get { return "greatest lemma"; } }
+    public override string WhatKind => "greatest lemma";
 
     public GreatestLemma(IToken tok, string name,
                    bool hasStaticKeyword, ExtremePredicate.KType typeOfK,

Source/Dafny/Resolver.cs

@@ -8508,6 +8508,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
           var s = (RevealStmt)stmt;
           s.ResolvedStatements.Iter(ss => Visit(ss, true, "a reveal statement"));
           s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost);
+
         } else if (stmt is BreakStmt) {
           var s = (BreakStmt)stmt;
           s.IsGhost = mustBeErasable;
@@ -8672,6 +8673,11 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
           }
           // if both branches were all ghost, then we can mark the enclosing statement as ghost as well
           s.IsGhost = s.IsGhost || (s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost));
+          if (!s.IsGhost && s.Guard != null) {
+            // If there were features in the guard that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            ExpressionTester.CheckIsCompilable(resolver, s.Guard, codeContext);
+          }
 
         } else if (stmt is AlternativeStmt) {
           var s = (AlternativeStmt)stmt;
@@ -8681,6 +8687,13 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
           }
           s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext)));
           s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));
+          if (!s.IsGhost) {
+            // If there were features in the guards that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            foreach (var alt in s.Alternatives) {
+              ExpressionTester.CheckIsCompilable(resolver, alt.Guard, codeContext);
+            }
+          }
 
         } else if (stmt is WhileStmt) {
           var s = (WhileStmt)stmt;
@@ -8704,6 +8717,11 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
               s.IsGhost = true;
             }
           }
+          if (!s.IsGhost && s.Guard != null) {
+            // If there were features in the guard that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            ExpressionTester.CheckIsCompilable(resolver, s.Guard, codeContext);
+          }
 
         } else if (stmt is AlternativeLoopStmt) {
           var s = (AlternativeLoopStmt)stmt;
@@ -8723,6 +8741,13 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
           }
           s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext)));
           s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)));
+          if (!s.IsGhost) {
+            // If there were features in the guards that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            foreach (var alt in s.Alternatives) {
+              ExpressionTester.CheckIsCompilable(resolver, alt.Guard, codeContext);
+            }
+          }
 
         } else if (stmt is ForLoopStmt) {
           var s = (ForLoopStmt)stmt;
@@ -8750,6 +8775,14 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
               s.IsGhost = true;
             }
           }
+          if (!s.IsGhost) {
+            // If there were features in the bounds that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            ExpressionTester.CheckIsCompilable(resolver, s.Start, codeContext);
+            if (s.End != null) {
+              ExpressionTester.CheckIsCompilable(resolver, s.End, codeContext);
+            }
+          }
 
         } else if (stmt is ForallStmt) {
           var s = (ForallStmt)stmt;
@@ -8769,6 +8802,10 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
                 Error(s, "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 '{0}'", bv.Name);
               }
             }
+
+            // If there were features in the range that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            ExpressionTester.CheckIsCompilable(resolver, s.Range, codeContext);
           }
 
         } else if (stmt is ModifyStmt) {
@@ -8800,10 +8837,17 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
           }
           s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext)));
           s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost));
+          if (!s.IsGhost) {
+            // If there were features in the source expression that are treated differently in ghost and non-ghost
+            // contexts, make sure they get treated for non-ghost use.
+            ExpressionTester.CheckIsCompilable(resolver, s.Source, codeContext);
+          }
+
         } else if (stmt is ConcreteSyntaxStatement) {
           var s = (ConcreteSyntaxStatement)stmt;
           Visit(s.ResolvedStatement, mustBeErasable, proofContext);
           s.IsGhost = s.IsGhost || s.ResolvedStatement.IsGhost;
+
         } else if (stmt is SkeletonStatement) {
           var s = (SkeletonStatement)stmt;
           s.IsGhost = mustBeErasable;

Source/Dafny/Util.cs

@@ -803,9 +803,10 @@ public static bool CheckIsCompilable(Resolver resolver, ErrorReporter reporter,
     }
 
     /// <summary>
-    /// Try to make "expr" compilable (in particular, mark LHSs of a let-expression as ghosts if
-    /// the corresponding RHS is ghost), and then report errors for every part that would prevent
-    /// compilation.
+    /// Checks that "expr" is compilable and reports an error if it is not.
+    /// Also, updates bookkeeping information for the verifier to record the fact that "expr" is to be compiled.
+    /// For example, this bookkeeping information keeps track of if the constraint of a let-such-that expression
+    /// must determine the value uniquely.
     /// Requires "expr" to have been successfully resolved.
     /// </summary>
     private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) {
@@ -817,13 +818,14 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) {
 
       if (expr is IdentifierExpr expression) {
         if (expression.Var != null && expression.Var.IsGhost) {
-          reporter?.Error(MessageSource.Resolver, expression, "ghost variables are allowed only in specification contexts");
+          reporter?.Error(MessageSource.Resolver, expression, "a ghost variable is allowed only in specification contexts");
           return false;
         }
 
       } else if (expr is MemberSelectExpr selectExpr) {
         if (selectExpr.Member != null && selectExpr.Member.IsGhost) {
-          reporter?.Error(MessageSource.Resolver, selectExpr, "ghost fields are allowed only in specification contexts");
+          var what = selectExpr.Member.WhatKindMentionGhost;
+          reporter?.Error(MessageSource.Resolver, selectExpr, $"a {what} is allowed only in specification contexts");
           return false;
         }
 
@@ -1047,6 +1049,14 @@ public static bool IsTypeTestCompilable(TypeTestExpr tte) {
     /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier)
     /// that is allowed only in specification contexts.
     /// Requires 'expr' to be a successfully resolved expression.
+    ///
+    /// Note, some expressions have different proof obligations in ghost and compiled contexts. For example,
+    /// a let-such-that expression in a compiled context is required to have a uniquely determined result.
+    /// For such an expression, "UsesSpecFeatures" returns "false", since the feature can be used in either ghost
+    /// or compiled contexts. Whenever "UsesSpecFeatures" returns "false", the caller has a choice about making
+    /// the expression ghost or making it compiled. If the caller chooses to make the expression compiled, the
+    /// caller must then call "CheckIsCompilable" to commit this choice, because "CheckIsCompilable" fills in
+    /// various bookkeeping information that the verifier will need.
     /// </summary>
     public static bool UsesSpecFeatures(Expression expr) {
       Contract.Requires(expr != null);