No more assume 2 < 2; (#1354)

* Add test file

* Don't remove Lit brackets when assert/assume

By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`.

* Refactor Assert helper methods

This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway.

* Redo changes lost in the merge

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Remy Willems <rgv.willems@gmail.com>

Source/Dafny/Verifier/Translator.BoogieFactory.cs

@@ -185,8 +185,15 @@ private static Bpl.Expr GetLit(Bpl.Expr expr) {
  }
 
  public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {
- var lit = RemoveLit(expr);
- return attributes == null ? new Bpl.AssumeCmd(tok, lit) : new Bpl.AssumeCmd(tok, lit, attributes);
+ var litArgument = GetLit(expr);
+ if (litArgument is Bpl.LiteralExpr literalExpr && literalExpr.asBool) {
+ // In most cases, we leave any Lit brackets that "expr" may have. In the past, these brackets
+ // had always been removed here. Alas, some brittle test cases stopped verifying if we
+ // keep "assume Lit(true)" instead of simplifying it to "assume true". Therefore, as a
+ // special case, we remove the Lit brackets from the literal "true".
+ expr = litArgument;
+ }
+ return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes);
  }
 
  static Bpl.Expr RemoveLit(Bpl.Expr expr) {

Source/Dafny/Verifier/Translator.cs

@@ -10225,6 +10225,15 @@ Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)
  return Assert(tok, condition, errorMessage, tok);
  }
 
+ Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.QKeyValue kv) {
+ Contract.Requires(tok != null);
+ Contract.Requires(errorMessage != null);
+ Contract.Requires(condition != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
+
+ return Assert(tok, condition, errorMessage, tok, kv);
+ }
+
  Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesToken, Bpl.QKeyValue kv = null) {
  Contract.Requires(tok != null);
  Contract.Requires(condition != null);
@@ -10237,13 +10246,14 @@ Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage,
  } else {
  var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);
  cmd.ErrorData = "Error: " + errorMessage;
- this.assertionCount++;
  return cmd;
  }
  }
+
  Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage) {
  return AssertNS(tok, condition, errorMessage, tok, null);
  }
+
  Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesTok, Bpl.QKeyValue kv) {
  Contract.Requires(tok != null);
  Contract.Requires(errorMessage != null);
@@ -10263,22 +10273,6 @@ Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessag
  }
  }
 
- Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.QKeyValue kv) {
- Contract.Requires(tok != null);
- Contract.Requires(errorMessage != null);
- Contract.Requires(condition != null);
- Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
-
- if (assertAsAssume || (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
- // produce an assume instead
- return TrAssumeCmd(tok, condition, kv);
- } else {
- var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);
- cmd.ErrorData = "Error: " + errorMessage;
- return cmd;
- }
- }
-
  Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment) {
  Contract.Requires(tok != null);
  Contract.Requires(condition != null);
@@ -10707,8 +10701,13 @@ Expression Zero(IToken tok, Type typ) {
  delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);
 
  Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {
- var lit = RemoveLit(expr);
- return attributes == null ? new Bpl.AssertCmd(tok, lit) : new Bpl.AssertCmd(tok, lit, attributes);
+ // It may be that "expr" is a Lit expression. It might seem we don't need a Lit expression
+ // around the boolean expression that is being asserted. However, we keep it. For one,
+ // it doesn't change the semantics of the assert command. More importantly, leaving
+ // a Lit around the expression is useful to avoid sending an "assert false;" to Boogie--since
+ // Boogie looks especially for "assert false;" commands and processes them in such a way
+ // that loops no longer are loops (which is confusing for Dafny users).
+ return attributes == null ? new Bpl.AssertCmd(tok, expr) : new Bpl.AssertCmd(tok, expr, attributes);
  }
 
  delegate void BodyTranslator(BoogieStmtListBuilder builder, ExpressionTranslator etr);

Test/dafny0/NoMoreAssume2Less2.dfy

@@ -0,0 +1,199 @@
+// RUN: %dafny "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file tests various ways of writing the equivalent of "assume false;" or "assert false;" inside a loop.
+// It used to be that Dafny's translation of such statements into Boogie could cause Boogie to cut off the
+// loop back edge, which would turn a loop into something that wasn't a loop. In particular, it would cause
+// the expected "havoc loop_targets;" statement never to be generated, whose dramatic impact on what gets
+// verified would be both mysterious and surprising to most Dafny users.
+//
+// The equally mysterious workaround for this problem used to be for Dafny users to replace their "assume false;"
+// with something like "assume 2 < 2;", which Boogie wouldn't recognize in the same way.
+//
+// The current translation to Boogie makes sure that no user-supplied expression turns into exactly an
+// "assume false;" or "assert false;". This means that Dafny users can use a statement like "assume false;"
+// without chopping off back edges.
+//
+// It is still possible (in situations that would be rare in practice) to get some initially-surprising behavior
+// from Boogie, because it is possible to introduce a "false" condition that will be detected by the control-flow
+// handling in Boogie's abstract interpreter. Method Conjuncts4 below shows such an example.
+
+method M0(n: nat) {
+ var i := 0;
+ while i < n {
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method M1(n: nat) {
+ var i := 0;
+ while i < n {
+ assume false;
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method M2(n: nat) {
+ var i := 0;
+ while i < n {
+ assume 2 < 2;
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method M3(n: nat) {
+ var i := 0;
+ while i < n {
+ assert false; // error
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method M4(n: nat) {
+ var i := 0;
+ while i < n {
+ assert 2 < 2; // error
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method M5(n: nat) {
+ var i := 0;
+ while i < n {
+ assert false by { // error
+ }
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+predicate P() { true }
+predicate Q() { true }
+predicate R(n: nat) { true }
+predicate False() { false }
+
+method Conjuncts0(n: nat) {
+ var i := 0;
+ while i < n {
+ assume P() && false && Q();
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Conjuncts1(n: nat) {
+ var i := 0;
+ while i < n {
+ assert P() && false && Q(); // error
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Conjuncts2(n: nat) {
+ var i := 0;
+ while i < n {
+ assume False();
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Conjuncts3(n: nat) {
+ var i := 0;
+ while i < n {
+ assert False(); // error
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Conjuncts4(n: nat, m: nat) {
+ var i := 0;
+ while i < n {
+ assert R(m) && false; // error
+ i := i + 1;
+ }
+ // The following assertion is provable, because the "false" in the assertion above
+ // gets noticed by Boogie's abstract interpreter, which then (correctly) figures out
+ // that no control leads from inside the loop back to the loop head. Therefore, it
+ // infers the loop invariant i == 0.
+ // It takes a special (and unusual) condition to get this behavior. This example
+ // uses two conjuncts, one of which is "false" and one of which is a non-Lit expression.
+ assert n == 0;
+}
+
+method LoopInvariants(n: nat) {
+ var i := 0;
+ while i < n {
+ for j := 0 to 5
+ invariant false // error
+ {
+ }
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Calls0(n: nat) {
+ var i := 0;
+ while i < n {
+ FalsePre(); // error
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method Calls1(n: nat) {
+ var i := 0;
+ while i < n {
+ FalsePost();
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method FalsePre()
+ requires false
+
+method FalsePost()
+ ensures false
+
+method LabeledExpressions0(n: nat)
+ requires A: false
+{
+ var i := 0;
+ while i < n {
+ reveal A;
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method LabeledExpressions1(n: nat)
+{
+ assert A: false; // error
+ var i := 0;
+ while i < n {
+ reveal A;
+ i := i + 1;
+ }
+ assert n == 0; // error
+}
+
+method LabeledExpressions2(n: nat)
+{
+ assert A: false by { // error
+ }
+ var i := 0;
+ while i < n {
+ reveal A;
+ i := i + 1;
+ }
+ assert n == 0; // error
+}

Test/dafny0/NoMoreAssume2Less2.dfy.expect

@@ -0,0 +1,31 @@
+NoMoreAssume2Less2.dfy(26,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(35,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(44,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(50,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(53,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(59,13): Error: assertion violation
+NoMoreAssume2Less2.dfy(62,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(68,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(72,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(86,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(92,18): Error: assertion violation
+NoMoreAssume2Less2.dfy(95,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(104,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(110,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(78,20): Related location
+NoMoreAssume2Less2.dfy(113,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(119,19): Error: assertion violation
+NoMoreAssume2Less2.dfy(135,16): Error: This loop invariant might not hold on entry.
+NoMoreAssume2Less2.dfy(135,16): Related message: loop invariant violation
+NoMoreAssume2Less2.dfy(140,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(146,12): Error: A precondition for this call might not hold.
+NoMoreAssume2Less2.dfy(162,11): Related location: This is the precondition that might not hold.
+NoMoreAssume2Less2.dfy(149,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(158,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(175,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(180,12): Error: assertion violation
+NoMoreAssume2Less2.dfy(186,11): Error: assertion violation
+NoMoreAssume2Less2.dfy(191,12): Error: assertion violation
+NoMoreAssume2Less2.dfy(198,11): Error: assertion violation
+
+Dafny program verifier finished with 0 verified, 26 errors

Test/dafny0/snapshots/Snapshots0.run.dfy.expect

@@ -1,6 +1,6 @@
 Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
  >>> DoNothingToAssert
-Processing command (at Snapshots0.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
  >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
@@ -11,7 +11,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f
  >>> MarkAsFullyVerified
 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots0.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
  >>> MarkAsPartiallyVerified
 Snapshots0.v1.dfy(4,9): Error: assertion violation
 

Test/dafny0/snapshots/Snapshots1.run.dfy.expect

@@ -1,14 +1,14 @@
 Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
  >>> DoNothingToAssert
-Processing command (at Snapshots1.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
  >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
 Processing call to procedure Call$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
  >>> added after: a##cached##0 := a##cached##0 && false;
 Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
  >>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
  >>> DoNothingToAssert
 Snapshots1.v1.dfy(4,9): Error: assertion violation
 

Test/dafny0/snapshots/Snapshots2.run.dfy.expect

@@ -1,6 +1,6 @@
 Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
  >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(4,10)) assert false;
+Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
  >>> DoNothingToAssert
 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
  >>> DoNothingToAssert
@@ -20,7 +20,7 @@ Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1
  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
 Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
  >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(4,10)) assert false;
+Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
  >>> DoNothingToAssert
 Snapshots2.v1.dfy(4,9): Error: assertion violation
 Processing command (at Snapshots2.v1.dfy(11,11)) assert true;

Test/dafny0/snapshots/Snapshots3.run.dfy.expect

@@ -1,11 +1,11 @@
-Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0;
+Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
  >>> DoNothingToAssert
 Snapshots3.v0.dfy(9,13): Error: assertion violation
 
 Dafny program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots3.v1.dfy(5,12)) assert true;
+Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);
  >>> DoNothingToAssert
-Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0;
+Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
  >>> RecycleError
 Snapshots3.v0.dfy(9,13): Error: assertion violation