feat: Implement assigned(e) expression (#5501)

Implements the `assigned(e)` expression, fixing #5251.

Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs

@@ -9,6 +9,7 @@ public enum Opcode {
  Fresh, // fresh also has a(n optional) second argument, namely the @-label
  Allocated,
  Lit, // there is no syntax for this operator, but it is sometimes introduced during translation
+ Assigned,
  }
  public readonly Opcode Op;
 
@@ -22,7 +23,8 @@ public enum ResolvedOpcode {
  MapCard,
  Fresh,
  Allocated,
- Lit
+ Lit,
+ Assigned,
  }
 
  private ResolvedOpcode _ResolvedOp = ResolvedOpcode.YetUndetermined;
@@ -42,6 +44,7 @@ public enum ResolvedOpcode {
  (Opcode.Fresh, _) => ResolvedOpcode.Fresh,
  (Opcode.Allocated, _) => ResolvedOpcode.Allocated,
  (Opcode.Lit, _) => ResolvedOpcode.Lit,
+ (Opcode.Assigned, _) => ResolvedOpcode.Assigned,
  _ => ResolvedOpcode.YetUndetermined // Unreachable
  };
  Contract.Assert(_ResolvedOp != ResolvedOpcode.YetUndetermined);

Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs

@@ -767,6 +767,10 @@ void PrintCasePattern<VT>(CasePattern<VT> pat)
  wr.Write("Lit(");
  PrintExpression(e.E, false);
  wr.Write(")");
+ } else if (e.Op == UnaryOpExpr.Opcode.Assigned) {
+ wr.Write("assigned(");
+ PrintExpression(e.E, false);
+ wr.Write(")");
  } else {
  Contract.Assert(e.Op != UnaryOpExpr.Opcode.Fresh); // this is handled is "is FreshExpr" case above
  // Prefix operator.

Source/DafnyCore/Dafny.atg

@@ -3682,6 +3682,8 @@ ConstAtomExpression<out Expression e>
  | "|" (. x = t; .)
  Expression<out e, true, true, false> (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e); .)
  "|"
+ | "assigned" (. x = t; .)
+ "(" NameSegment<out e> ")" (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Assigned, e); .)
  | ParensExpression<out e>
  ) (. if(x!= null) { e.RangeToken = new RangeToken(x, t); } .)
  .

Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs

@@ -63,6 +63,8 @@ public CheckDividedConstructorInit_Visitor(ErrorReporter reporter)
  if (e.Member.IsInstanceIndependentConstant && Expression.AsThis(e.Obj) != null) {
  return false; // don't continue the recursion
  }
+ } else if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) {
+ return false; // don't continue the recursion
  } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) {
  reporter.Error(MessageSource.Resolver, expr.tok, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields");
  }

Source/DafnyCore/Resolver/ExpressionTester.cs

@@ -562,7 +562,7 @@ public class ExpressionTester {
  return true;
  } else if (expr is UnaryExpr) {
  var e = (UnaryExpr)expr;
- if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Fresh or UnaryOpExpr.Opcode.Allocated }) {
+ if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Fresh or UnaryOpExpr.Opcode.Allocated or UnaryOpExpr.Opcode.Assigned }) {
  return true;
  }
  if (expr is TypeTestExpr tte && !IsTypeTestCompilable(tte)) {

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -758,6 +758,10 @@ public partial class ModuleResolver {
  reporter.Error(MessageSource.Resolver, expr, "a {0} definition is not allowed to depend on the set of allocated references", declKind);
  }
  break;
+ case UnaryOpExpr.Opcode.Assigned:
+ // the argument is allowed to have any type
+ expr.Type = Type.Bool;
+ break;
  default:
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
  }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -419,6 +419,10 @@ public partial class PreTypeResolver {
  ReportError(expr, "a {0} definition is not allowed to depend on the set of allocated references", declKind);
  }
  break;
+ case UnaryOpExpr.Opcode.Assigned:
+ // the argument is allowed to have any type at all
+ expr.PreType = ConstrainResultToBoolFamily(expr.tok, "assigned", "boolean literal used as if it had type {0}");
+ break;
  default:
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
  }

Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs

@@ -163,7 +163,8 @@ public partial class BoogieGenerator {
 
  Bpl.IdentifierExpr ie;
  if (definiteAssignmentTrackers.TryGetValue(expr.Var.UniqueName, out ie)) {
- builder.Add(Assert(GetToken(expr), ie, new PODesc.DefiniteAssignment($"variable '{expr.Var.Name}'", "here")));
+ builder.Add(Assert(GetToken(expr), ie,
+ new PODesc.DefiniteAssignment("variable", expr.Var.Name, "here")));
  }
  }
 
@@ -187,8 +188,8 @@ public partial class BoogieGenerator {
  var nm = SurrogateName(field);
  Bpl.IdentifierExpr ie;
  if (definiteAssignmentTrackers.TryGetValue(nm, out ie)) {
- var desc = new PODesc.DefiniteAssignment($"field '{field.Name}'",
- atNew ? "at this point in the constructor body" : "here");
+ var desc = new PODesc.DefiniteAssignment(
+ "field", field.Name, atNew ? "at this point in the constructor body" : "here");
  builder.Add(Assert(tok, ie, desc));
  }
  }
@@ -230,7 +231,7 @@ public partial class BoogieGenerator {
 
  Bpl.IdentifierExpr ie;
  if (definiteAssignmentTrackers.TryGetValue(p.UniqueName, out ie)) {
- var desc = new PODesc.DefiniteAssignment($"out-parameter '{p.Name}'", "at this return point");
+ var desc = new PODesc.DefiniteAssignment("out-parameter", p.Name, "at this return point");
  builder.Add(Assert(tok, ie, desc));
  }
  }

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -832,6 +832,26 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  // both the $IsAllocBox and $IsAlloc forms, because the axioms that connects these two is triggered
  // by $IsAllocBox.
  return BoogieGenerator.MkIsAllocBox(BoxIfNecessary(e.E.tok, TrExpr(e.E), e.E.Type), e.E.Type, HeapExpr);
+ case UnaryOpExpr.ResolvedOpcode.Assigned:
+ var ns = e.E as NameSegment;
+ Contract.Assert(ns != null);
+ string name = null;
+ switch (ns.Resolved) {
+ case IdentifierExpr ie:
+ name = ie.Var.UniqueName;
+ break;
+ case MemberSelectExpr mse:
+ if (BoogieGenerator.inBodyInitContext && Expression.AsThis(mse.Obj) != null) {
+ name = BoogieGenerator.SurrogateName(mse.Member as Field);
+ }
+ break;
+ }
+
+ if (name == null) {
+ return Expr.True;
+ }
+ BoogieGenerator.definiteAssignmentTrackers.TryGetValue(name, out var defass);
+ return defass;
  default:
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
  }

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -921,7 +921,12 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
  }
  case UnaryExpr unaryExpr: {
  UnaryExpr e = unaryExpr;
- CheckWellformed(e.E, wfOptions, locals, builder, etran);
+ if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) {
+ CheckWellformed(e.E.Resolved, wfOptions.WithLValueContext(true), locals, builder, etran);
+ } else {
+ CheckWellformed(e.E, wfOptions, locals, builder, etran);
+ }
+
  if (e is ConversionExpr ee) {
  CheckResultToBeInType(unaryExpr.tok, ee.E, ee.ToType, locals, builder, etran, ee.messagePrefix);
  }

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -1426,20 +1426,26 @@ public class ElementInDomain : ProofObligationDescription {
 
 public class DefiniteAssignment : ProofObligationDescription {
  public override string SuccessDescription =>
- $"{what}, which is subject to definite-assignment rules, is always initialized {where}";
+ $"{kind} '{name}', which is subject to definite-assignment rules, is always initialized {where}";
 
  public override string FailureDescription =>
- $"{what}, which is subject to definite-assignment rules, might be uninitialized {where}";
+ $"{kind} '{name}', which is subject to definite-assignment rules, might be uninitialized {where}";
 
  public override string ShortDescription => "definite assignment";
 
- private readonly string what;
+ private readonly string kind;
+ private readonly string name;
  private readonly string where;
 
- public DefiniteAssignment(string what, string where) {
- this.what = what;
+ public DefiniteAssignment(string kind, string name, string where) {
+ this.kind = kind;
+ this.name = name;
  this.where = where;
  }
+
+ public override Expression GetAssertedExpr(DafnyOptions options) {
+ return new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Assigned, new IdentifierExpr(Token.NoToken, name));
+ }
 }
 
 public class InRange : ProofObligationDescription {

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

@@ -0,0 +1,42 @@
+// RUN: %verify --relax-definite-assignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C<G>
+{
+ var x: G
+ const y: G
+
+ constructor Con0(i: int, a: G, b: G)
+ {
+ x := a;
+ y := b;
+ assert assigned(x);
+ assert assigned(y);
+ new;
+ if i > 0 {
+ x := y;
+ }
+ }
+
+ constructor Con1(i: int, a: G, b: G)
+ {
+ x := a;
+ assert assigned(x);
+ assume {:axiom} assigned(y);
+ new;
+ if i > 0 {
+ x := y;
+ }
+ }
+}
+
+method M0<G>(x: int, a: G, b: G) returns (y: G)
+{
+ if x < 10 {
+ y := a;
+ } else if x < 20 {
+ return b;
+ } else {
+ assume {:axiom} assigned(y);
+ }
+}

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

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy

@@ -0,0 +1,89 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C<G>
+{
+ var x: G
+ const y: G
+
+ constructor Con0(i: int, a: G, b: G)
+ {
+ if i > 0 {
+ x := a;
+ } else {
+ y := b;
+ }
+ new;
+ if i > 10 {
+ x := y;
+ }
+ }
+}
+
+method M0<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x := a;
+ } else if i < 10 {
+ y := b;
+ } else if i < 20 {
+ x := a;
+ y := x;
+ } else if i < 30 {
+ x := y;
+ y := b;
+ }
+}
+
+method M1<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ return x, y;
+ }
+ return a, b;
+}
+
+method M2<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x := a;
+ return x, y;
+ }
+ return a, b;
+}
+
+method M3<G>(i: int, a: G, b: G, c: G) returns (x: G, y: G, z: G)
+{
+ if i < 0 {
+ x := y;
+ return x, y, z;
+ }
+ return a, b, c;
+}
+
+method M4<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x := a;
+ return;
+ }
+ return a, b;
+}
+
+method M5<G>(i: int, a: G, b: G, c: G) returns (x: G, y: G, z: G)
+{
+ if i < 0 {
+ x := y;
+ return;
+ }
+ return a, b, c;
+}
+
+method M6<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x, y := y, x;
+ return;
+ }
+ return a, b;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect

@@ -0,0 +1,32 @@
+definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
+ Asserted expression: assigned(x)
+definite-assignment.dfy(16,4): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
+ Asserted expression: assigned(y)
+definite-assignment.dfy(33,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(36,0): Error: out-parameter 'x', which is subject to definite-assignment rules, might be uninitialized at this return point
+ Asserted expression: assigned(x)
+definite-assignment.dfy(36,0): Error: out-parameter 'y', which is subject to definite-assignment rules, might be uninitialized at this return point
+ Asserted expression: assigned(y)
+definite-assignment.dfy(41,11): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(x)
+definite-assignment.dfy(41,14): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(50,14): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(58,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(59,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(z)
+definite-assignment.dfy(68,4): Error: out-parameter 'y', which is subject to definite-assignment rules, might be uninitialized at this return point
+ Asserted expression: assigned(y)
+definite-assignment.dfy(76,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(77,4): Error: out-parameter 'z', which is subject to definite-assignment rules, might be uninitialized at this return point
+ Asserted expression: assigned(z)
+definite-assignment.dfy(85,12): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(y)
+definite-assignment.dfy(85,15): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here
+ Asserted expression: assigned(x)
+
+Dafny program verifier finished with 0 verified, 15 errors