From 550caf7bc7e6427f26bfb3d24f224e12c6c1c318 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 1 Jul 2015 13:29:11 -0700
Subject: Fixed bug in BplImp! Improvements in encoding of reads of function
 values.

---
 Binaries/DafnyPrelude.bpl             |  8 ++++++++
 Source/Dafny/Translator.cs            | 16 +++++++---------
 Test/VerifyThis2015/Problem3.dfy      |  2 +-
 Test/dafny4/NumberRepresentations.dfy |  2 +-
 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
-- 
cgit v1.2.3