Pass assert/assume attributes down to Boogie

3 files changed, 82 insertions, 38 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2e03dade..a2961174 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5002,7 +5002,7 @@ namespace Microsoft.Dafny {
       return Assert(tok, condition, errorMessage, tok);

     }

 

-    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesToken) {

+    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);

       Contract.Requires(errorMessage != null);

@@ -5010,17 +5010,17 @@ namespace Microsoft.Dafny {
 

       if (assertAsAssume || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {

         // produce an assume instead

-        return new Bpl.AssumeCmd(tok, condition);

+        return new Bpl.AssumeCmd(tok, condition, kv);

       } else {

-        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition);

+        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

     }

     Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage) {

-      return AssertNS(tok, condition, errorMessage, tok);

+      return AssertNS(tok, condition, errorMessage, tok, null);

     }

-    Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesTok)

+    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);

@@ -5029,13 +5029,12 @@ namespace Microsoft.Dafny {
 

       if (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {

         // produce a "skip" instead

-        return new Bpl.AssumeCmd(tok, Bpl.Expr.True);

+        return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

       } else {

         tok = ForceCheckToken.Unwrap(tok);

         var args = new List<object>();

         args.Add(Bpl.Expr.Literal(0));

-        Bpl.QKeyValue kv = new Bpl.QKeyValue(tok, "subsumption", args, null);

-        Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, kv);

+        Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, new Bpl.QKeyValue(tok, "subsumption", args, kv));

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -5114,12 +5113,12 @@ namespace Microsoft.Dafny {
           var ss = TrSplitExpr(s.Expr, etran, out splitHappened);

           if (!splitHappened) {

             var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok);

-            builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok));

+            builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null)));

           } else {

             foreach (var split in ss) {

               if (split.IsChecked) {

                 var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok);

-                builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok));

+                builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null)));  // attributes go on every split

               }

             }

             builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

@@ -5128,7 +5127,7 @@ namespace Microsoft.Dafny {
           AddComment(builder, stmt, "assume statement");

           AssumeStmt s = (AssumeStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

-          builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

+          builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null)));

         }

       } else if (stmt is PrintStmt) {

         AddComment(builder, stmt, "print statement");

@@ -5203,7 +5202,7 @@ namespace Microsoft.Dafny {
                 // this postcondition was inherited into this module, so just ignore it

               } else if (split.IsChecked) {

                 var yieldToken = new NestedToken(s.Tok, split.E.tok);

-                builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok));

+                builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok, null));

               }

             }

             builder.Add(new Bpl.AssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E)));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 424b83bb..676c0313 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -829,8 +829,22 @@ Execution trace:
 Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value

 Execution trace:

     (0,0): anon0

+Basics.dfy(426,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

+Basics.dfy(437,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+Basics.dfy(439,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

 

-Dafny program verifier finished with 59 verified, 11 errors

+Dafny program verifier finished with 61 verified, 14 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index cdeae046..8f036349 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -382,28 +382,59 @@ module SetCardinality {
 

 method HexTest()

 {

-	var first16lower := [ 0x0, 0x1, 0x2, 0x3, 0x4, 0x5, 0x6, 0x7, 0x8, 0x9, 0xa, 0xb, 0xc, 0xd, 0xe, 0xf ];

-	var first16upper := [ 0x0, 0x1, 0x2, 0x3, 0x4, 0x5, 0x6, 0x7, 0x8, 0x9, 0xA, 0xB, 0xC, 0xD, 0xE, 0xF ];

-	assert forall i :: 0 <= i < |first16lower| ==> first16lower[i] == i;

-	assert forall i :: 0 <= i < |first16upper| ==> first16upper[i] == i;

-

-	var randomHex := [ 0xCF4458F2, 0x9A5C5BAF, 0x26A6ABD6, 0x00EB3933, 0x9123D2CF, 0xBE040001, 0x5AD038FA, 0xC75597A6, 0x7CF821A7, 0xCDEFB617, 0x4889D968, 0xB05F896A,

-					   0x75B18DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, 

-					   0x610D0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, 

-					   0x02FBF254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, 

-					   0x730D85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, 

-					   0xc95f056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, 

-					   0x1520b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, 

-					   0xbfcd3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, 

-					   0xcd85f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd8C6FAF7 ];

-	var randomDec := [ 3477362930, 2589744047, 648457174, 15415603, 2435044047, 3187933185, 1523595514, 3344275366, 2096636327, 3455038999, 1216993640, 2959051114, 

-					   1974570418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, 

-					   1628242745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, 

-					   50066004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, 

-					   1930266087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,

-					   3378447726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,

-					   354465647, 2080258281, 2351471473, 1736439093, 196693838, 4215372800, 2714419258, 1581046514, 1981216564, 3042395387, 660877099, 2707539070,

-					   3217899519, 2788029817, 1050875824, 3362808767,  3721613, 2510678132, 1993876726, 409501246, 1273417770, 741130572, 1855051115, 1994570544,

-					   3448107468, 1645859758, 3193559252, 3636919031 ];

-	assert forall i :: 0 <= i < |randomHex| ==> randomHex[i] == randomDec[i];

-}
\ No newline at end of file
+  var first16lower := [ 0x0, 0x1, 0x2, 0x3, 0x4, 0x5, 0x6, 0x7, 0x8, 0x9, 0xa, 0xb, 0xc, 0xd, 0xe, 0xf ];

+  var first16upper := [ 0x0, 0x1, 0x2, 0x3, 0x4, 0x5, 0x6, 0x7, 0x8, 0x9, 0xA, 0xB, 0xC, 0xD, 0xE, 0xF ];

+  assert forall i :: 0 <= i < |first16lower| ==> first16lower[i] == i;

+  assert forall i :: 0 <= i < |first16upper| ==> first16upper[i] == i;

+

+  var randomHex := [ 0xCF4458F2, 0x9A5C5BAF, 0x26A6ABD6, 0x00EB3933, 0x9123D2CF, 0xBE040001, 0x5AD038FA, 0xC75597A6, 0x7CF821A7, 0xCDEFB617, 0x4889D968, 0xB05F896A,

+             0x75B18DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, 

+             0x610D0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, 

+             0x02FBF254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, 

+             0x730D85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, 

+             0xc95f056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, 

+             0x1520b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, 

+             0xbfcd3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, 

+             0xcd85f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd8C6FAF7 ];

+  var randomDec := [ 3477362930, 2589744047, 648457174, 15415603, 2435044047, 3187933185, 1523595514, 3344275366, 2096636327, 3455038999, 1216993640, 2959051114, 

+             1974570418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, 

+             1628242745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, 

+             50066004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, 

+             1930266087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,

+             3378447726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,

+             354465647, 2080258281, 2351471473, 1736439093, 196693838, 4215372800, 2714419258, 1581046514, 1981216564, 3042395387, 660877099, 2707539070,

+             3217899519, 2788029817, 1050875824, 3362808767,  3721613, 2510678132, 1993876726, 409501246, 1273417770, 741130572, 1855051115, 1994570544,

+             3448107468, 1645859758, 3193559252, 3636919031 ];

+  assert forall i :: 0 <= i < |randomHex| ==> randomHex[i] == randomDec[i];

+}

+

+// ------------------------ attributes on assert/assume and methods are passed down -----

+

+// To test this in Dafny, we're using Boogie's :selective_checking and :start_checking_here

+// attributes.  This also tests the useful mode of using these attributes in Dafny programs.

+method {:selective_checking} MySelectiveChecking0(x: int, y: int, z: int)

+{

+  if * {

+    // this is another branch

+    assert y + 129 == z;  // no complaint, since we're using :selective_checking

+  } else {

+    assert x < y;  // no complaint

+    assert y < z;  // ditto

+    assume {:start_checking_here} true;

+    assert x < z;  // this holds, so there's no complaint here, either

+  }

+  assert x < z;  // error (this doesn't hold if we take the 'then' branch)

+}

+method {:selective_checking} MySelectiveChecking1(x: int, y: int, z: int)

+{

+  if * {

+    // this is another branch

+    assert y + 129 == z;  // no complaint, since we're using :selective_checking

+  } else {

+    assert x < y;  // no complaint

+    assert y < z;  // ditto

+    assert {:start_checking_here} true;

+    assert x + 10 < z;  // error

+  }

+  assert x < z;  // error (this doesn't hold if we take the 'then' branch)

+}