Fixed bug in BplImp!

Improvements in encoding of reads of function values.

4 files changed, 17 insertions, 11 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dbf9b76c..2ca10f73 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -273,6 +273,8 @@ const unique class._System.set: ClassName;
 const unique class._System.seq: ClassName;

 const unique class._System.multiset: ClassName;

 

+function Tclass._System.object(): Ty;

+

 function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty

 

 function TypeTuple(a: ClassName, b: ClassName): ClassName;

@@ -287,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type HandleType;

 

+function SetRef_to_SetBox(s: [ref]bool): Set Box;

+axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] }

+  SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);

+axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) }

+  $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));

+

 // ---------------------------------------------------------------

 // -- Datatypes --------------------------------------------------

 // ---------------------------------------------------------------

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c98bd203..78f5c89d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5713,11 +5713,9 @@ namespace Microsoft.Dafny {
 

       {

         // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box

-        //      :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN]

-        //

-        // no precondition for these, but:

-        // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN]

-        // for reads, we could:  ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't

+        //      :: ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == h[heap, b1, ..., bN]

+        //      :: RequiresN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) <== r[heap, b1, ..., bN]

+        //      :: ReadsN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == rd[heap, b1, ..., bN]

         Action<string, Bpl.Type, string, Bpl.Type, string, Bpl.Type> SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => {

           Contract.Assert((precond == null) == (precondTy == null));

           var bvars = new List<Bpl.Variable>();

@@ -5919,7 +5917,7 @@ namespace Microsoft.Dafny {
       var inner_name = GetClass(td).TypedIdent.Name;

       string name = "T" + inner_name;

       // Create the type constructor

-      {

+      if (td.Name != "object") {  // the type constructor for "object" is in DafnyPrelude.bpl

         Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false);

         List<Bpl.Variable> args = new List<Bpl.Variable>(

           Enumerable.Range(0, arity).Select(i =>

@@ -11462,10 +11460,10 @@ namespace Microsoft.Dafny {
         }

 

         var rdvars = new List<Bpl.Variable>();

-        var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType());

-

+        var o = BplBoundVar(varNameGen.FreshId("#o#"), predef.RefType, rdvars);

         Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

           translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null));

+        rdbody = translator.FunctionCall(e.tok, "SetRef_to_SetBox", predef.SetType(e.tok, true, predef.BoxType), rdbody);

 

         return translator.Lit(

           translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType,

@@ -14220,7 +14218,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(b != null);

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

 

-      if (a == Bpl.Expr.True || b == Bpl.Expr.True || b == Bpl.Expr.False) {

+      if (a == Bpl.Expr.True || b == Bpl.Expr.True) {

         return b;

       } else if (a == Bpl.Expr.False) {

         return Bpl.Expr.True;

diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 10ad2d3a..4205035d 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // Rustan Leino

diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 8a94505c..1ebdf64c 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // We consider a number representation that consists of a sequence of digits.  The least