fix: Check well-definedness of forall-ensures

Fixes dafny-lang#2605
RustanLeino · Aug 17, 2022 · 2dae005 · 2dae005
1 parent 6ea3725
commit 2dae005
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 3 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -16,6 +16,7 @@
   (https://github.com/dafny-lang/dafny/pull/2522)
 - feat: `predicate P(x: int): (y: bool) ...` is now valid syntax (https://github.com/dafny-lang/dafny/pull/2454)
 - fix: Improve the performance of proofs involving bit vector shifts (https://github.com/dafny-lang/dafny/pull/2520)
+- fix: Perform well-definedness checks for ensures clauses of forall statements (https://github.com/dafny-lang/dafny/issues/2605)
 
 # 3.7.3
 

diff --git a/Source/Dafny/Verifier/Translator.TrStatement.cs b/Source/Dafny/Verifier/Translator.TrStatement.cs
@@ -993,9 +993,9 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi
       //     havoc x,y;
       //     CheckWellformed( Range );
       //     assume Range(x,y);
-      //     Tr( Body );
       //     CheckWellformed( Post );
-      //     assert Post;
+      //     Tr( Body );       // include only if there is a Body
+      //     assert Post;      // include only if there is a Body
       //     assume false;
       //   } else {
       //     assume (forall x,y :: Range(x,y) ==> Post(x,y));
@@ -1022,12 +1022,18 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi
       TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
       definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
 
+      var ensuresDefinedness = new BoogieStmtListBuilder(this);
+      foreach (var ens in s.Ens) {
+        TrStmt_CheckWellformed(ens.E, ensuresDefinedness, locals, etran, false);
+        ensuresDefinedness.Add(TrAssumeCmd(ens.E.tok, etran.TrExpr(ens.E)));
+      }
+      PathAsideBlock(s.Tok, ensuresDefinedness, definedness);
+
       if (s.Body != null) {
         TrStmt(s.Body, definedness, locals, etran);
 
         // check that postconditions hold
         foreach (var ens in s.Ens) {
-
           bool splitHappened;  // we actually don't care
           foreach (var split in TrSplitExpr(ens.E, etran, true, out splitHappened)) {
             if (split.IsChecked) {

diff --git a/Test/git-issues/git-issue-2605.dfy b/Test/git-issues/git-issue-2605.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M(a: array<int>, j: int) {
+  forall n | 0 <= n < 100
+    ensures n / 0 == n / 0 // error (x2): division by zero
+    ensures a[j] == a[j] // error (x2): array index out of bounds    
+  {
+    assert false; // error
+  }
+  assert false; // error
+}
diff --git a/Test/git-issues/git-issue-2605.dfy.expect b/Test/git-issues/git-issue-2605.dfy.expect
@@ -0,0 +1,7 @@
+git-issue-2605.dfy(6,14): Error: possible division by zero
+git-issue-2605.dfy(6,23): Error: possible division by zero
+git-issue-2605.dfy(7,13): Error: index out of range
+git-issue-2605.dfy(7,21): Error: index out of range
+git-issue-2605.dfy(9,11): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 5 errors