Dafny:

* Added DeclType(f)==C axioms, which for each field f says which class declares it.

Boogie:
* Changed behavior of free loop invariants.  Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures.  The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE:  I did NOT yet make the corresponding change for loop unrolling, but it is needed.

4 files changed, 28 insertions, 6 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index fa0d1529..9ff60f1b 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -181,6 +181,8 @@ const unique #loc.$Heap: $token;
 

 const unique alloc: Field bool;

 

+function DeclType<T>(Field T) returns (ClassName);

+

 function $HeapSucc(HeapType, HeapType) returns (bool);

 axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

   $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 1a25e283..d215de0d 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -112,7 +112,8 @@ namespace Microsoft.Boogie
     public enum SubsumptionOption { Never, NotForQuantifiers, Always }

     public SubsumptionOption UseSubsumption = SubsumptionOption.Always;

 

-    public bool ShowTrace = false;

+    public bool AlwaysAssumeFreeLoopInvariants = false;

+

     public enum ShowEnvironment { Never, DuringPrint, Always }

     public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint;

     public bool DontShowLogo = false;

@@ -1106,6 +1107,7 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("noRemoveEmptyBlocks", ref RemoveEmptyBlocks, false) ||

               ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||

               ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) ||

+              ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||

               ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||

               ps.CheckBooleanFlag("noVerifyByDefault", ref NoVerifyByDefault) ||

               ps.CheckBooleanFlag("useUncheckedContracts", ref UseUncheckedContracts) ||

@@ -1799,6 +1801,10 @@ namespace Microsoft.Boogie
   /traceverify   : print debug output during verification condition generation

   /subsumption:<c> : apply subsumption to asserted conditions:

                     0 - never, 1 - not for quantifiers, 2 (default) - always

+  /alwaysAssumeFreeLoopInvariants : usually, a free loop invariant (or assume

+                   statement in that position) is ignored in checking contexts

+                   (like other free things); this option includes these free

+                   loop invariants as assumes in both contexts

   /bv:<bv>       : bitvector handling

                    n = none

                    z = native Z3 bitvectors (default)

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 15f208f0..1cac78af 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -909,7 +909,7 @@ namespace Microsoft.Dafny {
     }

     

     Bpl.Constant! GetField(Field! f)

-      requires predef != null;

+      requires sink != null && predef != null;

     {

       Bpl.Constant fc;

       if (fields.TryGetValue(f, out fc)) {

@@ -918,6 +918,9 @@ namespace Microsoft.Dafny {
         Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));

         fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);

         fields.Add(f, fc);

+        // axiom DeclType(f) == C;

+        Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass))));

+        sink.TopLevelDeclarations.Add(ax);

       }

       return fc;

     }

@@ -2243,6 +2246,7 @@ namespace Microsoft.Dafny {
       DynamicType,  // allocated type

       TypeParams,   // type parameters to allocated type

       TypeTuple,

+      DeclType,

       

       // CEV

       CevInit,

@@ -2364,6 +2368,10 @@ namespace Microsoft.Dafny {
           assert args.Length == 2;

           assert typeInstantiation == null;

           return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args);

+        case BuiltinFunction.DeclType:

+          assert args.Length == 1;

+          assert typeInstantiation != null;

+          return FunctionCall(tok, "DeclType", predef.ClassNameType, args);

           

         case BuiltinFunction.CevInit:

           assert args.Length == 1;

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index c0ebb933..a79e63eb 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1824,10 +1824,7 @@ namespace VC
           PredicateCmd a = header.Cmds[i] as PredicateCmd;

           if (a != null)

           {

-            if (a is AssumeCmd) {

-              prefixOfPredicateCmdsInit.Add(a);

-              prefixOfPredicateCmdsMaintained.Add(a);

-            } else {

+            if (a is AssertCmd) {

               Bpl.AssertCmd c = (AssertCmd) a;

               Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);

               b.ErrorData = c.ErrorData;

@@ -1836,6 +1833,15 @@ namespace VC
               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsMaintained.Add(b);

               header.Cmds[i] = new AssumeCmd(c.tok,c.Expr);

+            } else {

+              assert a is AssumeCmd;

+              if (Bpl.CommandLineOptions.Clo.AlwaysAssumeFreeLoopInvariants) {

+                // Usually, "free" stuff, like free loop invariants (and the assume statements

+                // that stand for such loop invariants) are ignored on the checking side.  This

+                // command-line option changes that behavior to always assume the conditions.

+                prefixOfPredicateCmdsInit.Add(a);

+                prefixOfPredicateCmdsMaintained.Add(a);

+              }

             }

           }

           else if ( header.Cmds[i] is CommentCmd )