fix: Substitute for heap labels in TrSplitExpr (#2300)

This PR fixes two things related to heap labels. One gave rise to unsound verification, and the other to malformed Boogie code.

Fixes #2299

RELEASE_NOTES.md

@@ -1,5 +1,6 @@
 # Upcoming
 
+- fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300)
 - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302)
 
 # 3.7.1

Source/Dafny/AST/FreeVariablesUtil.cs

@@ -61,6 +61,9 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, re
  if (e.Obj.Type.IsRefType && !(e.Member is ConstantField)) {
  usesHeap = true;
  }
+ if (e.AtLabel != null) {
+ freeHeapAtVariables.Add(e.AtLabel);
+ }
  } else if (expr is SeqSelectExpr) {
  var e = (SeqSelectExpr)expr;
  if (e.Seq.Type.IsArrayType) {
@@ -74,10 +77,13 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, re
  } else if (expr is MultiSelectExpr) {
  usesHeap = true;
  } else if (expr is FunctionCallExpr) {
- Function f = ((FunctionCallExpr)expr).Function;
- if (Translator.AlwaysUseHeap || f == null || f.ReadsHeap) {
+ var e = (FunctionCallExpr)expr;
+ if (Translator.AlwaysUseHeap || e.Function == null || e.Function.ReadsHeap) {
  usesHeap = true;
  }
+ if (e.AtLabel != null) {
+ freeHeapAtVariables.Add(e.AtLabel);
+ }
  } else if (expr is UnchangedExpr) {
  var e = (UnchangedExpr)expr;
  // Note, we don't have to look out for const fields here, because const fields

Source/Dafny/Substituter.cs

@@ -9,18 +9,20 @@ namespace Microsoft.Dafny {
  /// particular, the substituter does not copy parts of an expression that are used only for well-formedness checks.
  /// </summary>
  public class Substituter {
- public readonly Expression receiverReplacement;
- public readonly Dictionary<IVariable, Expression/*!*/>/*!*/ substMap;
- public readonly Dictionary<TypeParameter, Type/*!*/>/*!*/ typeMap;
+ protected readonly Expression receiverReplacement;
+ protected readonly Dictionary<IVariable, Expression> substMap;
+ protected readonly Dictionary<TypeParameter, Type> typeMap;
+ protected readonly Label oldHeapLabel;
 
  public static readonly Substituter EMPTY = new Substituter(null, new Dictionary<IVariable, Expression>(), new Dictionary<TypeParameter, Type>());
 
- public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap) {
+ public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression> substMap, Dictionary<TypeParameter, Type> typeMap, Label oldHeapLabel = null) {
  Contract.Requires(substMap != null);
  Contract.Requires(typeMap != null);
  this.receiverReplacement = receiverReplacement;
  this.substMap = substMap;
  this.typeMap = typeMap;
+ this.oldHeapLabel = oldHeapLabel;
  }
  public virtual Expression Substitute(Expression expr) {
  Contract.Requires(expr != null);
@@ -84,13 +86,13 @@ public virtual Expression Substitute(Expression expr) {
  newExpr = new MapDisplayExpr(expr.tok, e.Finite, elmts);
  }
  } else if (expr is MemberSelectExpr) {
- MemberSelectExpr fse = (MemberSelectExpr)expr;
- Expression substE = Substitute(fse.Obj);
- MemberSelectExpr fseNew = new MemberSelectExpr(fse.tok, substE, fse.MemberName);
- fseNew.Member = fse.Member;
- fseNew.TypeApplication_AtEnclosingClass = fse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap));
- fseNew.TypeApplication_JustMember = fse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap));
- fseNew.AtLabel = fse.AtLabel;
+ var mse = (MemberSelectExpr)expr;
+ Expression substE = Substitute(mse.Obj);
+ MemberSelectExpr fseNew = new MemberSelectExpr(mse.tok, substE, mse.MemberName);
+ fseNew.Member = mse.Member;
+ fseNew.TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap));
+ fseNew.TypeApplication_JustMember = mse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap));
+ fseNew.AtLabel = mse.AtLabel ?? oldHeapLabel;
  newExpr = fseNew;
  } else if (expr is SeqSelectExpr) {
  SeqSelectExpr sse = (SeqSelectExpr)expr;
@@ -118,15 +120,15 @@ public virtual Expression Substitute(Expression expr) {
  }
 
  } else if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
+ var e = (FunctionCallExpr)expr;
  Expression receiver = Substitute(e.Receiver);
  List<Expression> newArgs = SubstituteExprList(e.Args);
  var newTypeApplicationAtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass);
  var newTypeApplicationJustFunction = SubstituteTypeList(e.TypeApplication_JustFunction);
  if (receiver != e.Receiver || newArgs != e.Args ||
  newTypeApplicationAtEnclosingClass != e.TypeApplication_AtEnclosingClass ||
  newTypeApplicationJustFunction != e.TypeApplication_JustFunction) {
- FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel);
+ FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel ?? oldHeapLabel);
  newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end)
  newFce.CoCall = e.CoCall; // also copy the co-call status
  newFce.CoCallHint = e.CoCallHint; // and any co-call hint
@@ -161,7 +163,7 @@ public virtual Expression Substitute(Expression expr) {
  // BoogieWrapper before calling Substitute.
  Expression se = Substitute(e.E);
  if (se != e.E) {
- newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel };
+ newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel ?? oldHeapLabel };
  }
  } else if (expr is UnchangedExpr) {
  var e = (UnchangedExpr)expr;
@@ -175,7 +177,7 @@ public virtual Expression Substitute(Expression expr) {
  fr.Add(fefe);
  }
  if (anythingChanged) {
- newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel };
+ newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel ?? oldHeapLabel };
  }
  } else if (expr is SeqConstructionExpr) {
  var e = (SeqConstructionExpr)expr;
@@ -202,7 +204,7 @@ public virtual Expression Substitute(Expression expr) {
  if (se != e.E) {
  if (e is FreshExpr) {
  var ee = (FreshExpr)e;
- newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel };
+ newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldHeapLabel };
  } else if (e is UnaryOpExpr) {
  var ee = (UnaryOpExpr)e;
  newExpr = new UnaryOpExpr(expr.tok, ee.Op, se);

Source/Dafny/Verifier/Translator.cs

@@ -11675,7 +11675,7 @@ private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) {
  var pp = (PrefixPredicate)f;
  body = PrefixSubstitution(pp, body);
  }
- body = Substitute(body, fexp.Receiver, substMap, fexp.GetTypeArgumentSubstitutions());
+ body = Substitute(body, fexp.Receiver, substMap, fexp.GetTypeArgumentSubstitutions(), fexp.AtLabel);
  return body;
  }
 
@@ -11822,11 +11822,12 @@ public static Expression Substitute(Expression expr, IVariable v, Expression e)
  return Substitute(expr, null, substMap);
  }
 
- public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type>/*?*/ typeMap = null) {
+ public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap,
+ Dictionary<TypeParameter, Type> typeMap = null, Label oldLabel = null) {
  Contract.Requires(expr != null);
  Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
  Contract.Ensures(Contract.Result<Expression>() != null);
- var s = new Substituter(receiverReplacement, substMap, typeMap ?? new Dictionary<TypeParameter, Type>());
+ var s = new Substituter(receiverReplacement, substMap, typeMap ?? new Dictionary<TypeParameter, Type>(), oldLabel);
  return s.Substitute(expr);
  }
 

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

@@ -0,0 +1,135 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class Twostate {
+ var z: int
+
+ twostate predicate Increase()
+ reads this
+ {
+ old(z) <= z
+ }
+
+ twostate predicate NoChange()
+ reads this
+ {
+ unchanged(this)
+ }
+
+ static twostate predicate IsFresh(new c: Twostate)
+ {
+ fresh(c)
+ }
+
+ twostate predicate All(new c: Twostate)
+ reads this
+ {
+ Increase() && NoChange() && IsFresh(c)
+ }
+
+ method Test0()
+ modifies this
+ {
+ z := z + 1;
+ label L:
+ z := z - 1;
+ // the following line was once translated incorrectly without the @L
+ assert Increase@L(); // error: does not hold
+ assert false;
+ }
+
+ method Test1()
+ modifies this
+ {
+ z := z + 1;
+ label L:
+ z := z - 1;
+ // the following line was once translated incorrectly without the @L
+ assert NoChange@L(); // error: does not hold
+ }
+
+ method Test2()
+ modifies this
+ {
+ z := z + 1;
+ label L:
+ z := z - 1;
+ // the following line was once translated incorrectly without the @L
+ assert IsFresh@L(this); // error: does not hold
+ }
+
+ method Test3()
+ {
+ var c := new Twostate;
+ label L:
+ if * {
+ // the following line was once translated incorrectly without the @L
+ assert IsFresh@L(c); // error: does not hold
+ } else {
+ assert IsFresh(c);
+ }
+ }
+
+ method Test4()
+ modifies this
+ {
+ var c := new Twostate;
+ z := z + 1;
+ label L:
+ z := z - 1;
+ // the following line was once translated incorrectly without the @L
+ assert All@L(c); // error: does not hold
+ }
+
+ method Test5(k: nat)
+ modifies this
+ {
+ z := z + k;
+ label L:
+ var c := new Twostate;
+
+ assert Increase@L();
+ assert NoChange@L();
+ assert IsFresh@L(c);
+
+ assert Increase();
+ if k == 0 {
+ assert NoChange();
+ }
+ assert IsFresh(c);
+ }
+
+ method Test6()
+ modifies this
+ {
+ z := z + 1;
+ var c := new Twostate;
+ label L:
+ z := z - 1;
+
+ assert Increase();
+ assert NoChange();
+ assert IsFresh(c);
+ }
+
+ method Test7()
+ modifies this
+ {
+ z := z + 1;
+ label L:
+ var c := new Twostate;
+ assert All@L(c);
+ }
+
+ method FreeHeapAtVariables()
+ modifies this
+ {
+ z := z + 1;
+ label L:
+ z := z - 1;
+ ghost var x;
+ // regression: the following line once led to malformed Boogie
+ x := var u :| u == Increase@L(); !u;
+ assert x;
+ }
+}

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

@@ -0,0 +1,19 @@
+git-issue-2299.dfy(37,11): Error: assertion might not hold
+git-issue-2299.dfy(10,11): Related location
+git-issue-2299.dfy(48,11): Error: assertion might not hold
+git-issue-2299.dfy(16,4): Related location
+git-issue-2299.dfy(58,11): Error: assertion might not hold
+git-issue-2299.dfy(21,4): Related location
+git-issue-2299.dfy(67,13): Error: assertion might not hold
+git-issue-2299.dfy(21,4): Related location
+git-issue-2299.dfy(81,11): Error: assertion might not hold
+git-issue-2299.dfy(27,4): Related location
+git-issue-2299.dfy(10,11): Related location
+git-issue-2299.dfy(81,11): Error: assertion might not hold
+git-issue-2299.dfy(27,18): Related location
+git-issue-2299.dfy(16,4): Related location
+git-issue-2299.dfy(81,11): Error: assertion might not hold
+git-issue-2299.dfy(27,32): Related location
+git-issue-2299.dfy(21,4): Related location
+
+Dafny program verifier finished with 7 verified, 7 errors