Added "free ensures" to procedures encoding the allocatedness

of references.

4 files changed, 77 insertions, 34 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 7a7e850b..d1b7f43c 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -1345,7 +1345,7 @@ namespace BytecodeTranslator
           List<Bpl.IdentifierExpr> outvars;

           Bpl.IdentifierExpr thisExpr;

           Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr, bool>> toBoxed;

-          var proc2 = TranslateArgumentsAndReturnProcedure(token, propertyDefinition.Getter, propertyDefinition.Getter.ResolvedMethod, target.Instance, IteratorHelper.GetEmptyEnumerable<IExpression>(), out inexpr, out outvars, out thisExpr, out toBoxed);

+          var proc2 = TranslateArgumentsAndReturnProcedure(token, propertyDefinition.Getter, propertyDefinition.Getter.ResolvedMethod, target.Instance, Enumerable<IExpression>.Empty, out inexpr, out outvars, out thisExpr, out toBoxed);

 

           EmitLineDirective(token);

 

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index d637586d..dd9aa62d 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -89,10 +89,10 @@ namespace BytecodeTranslator {
     [RepresentationFor("MultisetSingleton", "function {:inline true} MultisetSingleton(x: Delegate): DelegateMultiset { MultisetEmpty[x := 1] }")]

     public Bpl.Function MultisetSingleton = null;

 

-    [RepresentationFor("MultisetPlus", "function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { mapadd(x, y) }")]

+    [RepresentationFor("MultisetPlus", "function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { DelegateMapadd(x, y) }")]

     public  Bpl.Function MultisetPlus = null;

 

-    [RepresentationFor("MultisetMinus", "function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0)) }")]

+    [RepresentationFor("MultisetMinus", "function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0)) }")]

     public Bpl.Function MultisetMinus = null;

 

     [RepresentationFor("Field", "type Field;")]

@@ -364,8 +364,18 @@ namespace BytecodeTranslator {
     [RepresentationFor("$DisjointSubtree", "function $DisjointSubtree(Type, Type): bool;")]

     public Bpl.Function DisjointSubtree = null;

 

+    [RepresentationFor("$Alloc", "var $Alloc: [Ref] bool;")]

+    public Bpl.Variable AllocVariable = null;

+

+    [RepresentationFor("$allocImp", "function {:builtin \"MapImp\"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool;")]

+    public Bpl.Function AllocImplies = null;

+    [RepresentationFor("$allocConstBool", "function {:builtin \"MapConst\"} $allocConstBool(bool) : [Ref]bool;")]

+    public Bpl.Function AllocConstBool = null;

+

+

+

     protected readonly string CommonText =

-      @"var $Alloc: [Ref] bool;

+      @"//var $Alloc: [Ref] bool;

 

 procedure {:inline 1} Alloc() returns (x: Ref)

   modifies $Alloc;

@@ -374,26 +384,26 @@ procedure {:inline 1} Alloc() returns (x: Ref)
   $Alloc[x] := true;

 }

 

-function {:builtin ""MapAdd""} mapadd([Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapSub""} mapsub([Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapMul""} mapmul([Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapDiv""} mapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapMod""} mapmod([Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapConst""} mapconstint(int) : [Delegate]int;

-function {:builtin ""MapConst""} mapconstbool(bool) : [Delegate]bool;

-function {:builtin ""MapAnd""} mapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

-function {:builtin ""MapOr""} mapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

-function {:builtin ""MapNot""} mapnot([Delegate]bool) : [Delegate]bool;

-function {:builtin ""MapIte""} mapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

-function {:builtin ""MapIte""} mapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

-function {:builtin ""MapLe""} maple([Delegate]int, [Delegate]int) : [Delegate]bool;

-function {:builtin ""MapLt""} maplt([Delegate]int, [Delegate]int) : [Delegate]bool;

-function {:builtin ""MapGe""} mapge([Delegate]int, [Delegate]int) : [Delegate]bool;

-function {:builtin ""MapGt""} mapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

-function {:builtin ""MapEq""} mapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

-function {:builtin ""MapIff""} mapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

-function {:builtin ""MapImp""} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

-axiom MultisetEmpty == mapconstint(0);

+function {:builtin ""MapAdd""} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapSub""} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapMul""} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapDiv""} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapMod""} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapConst""} DelegateMapconstint(int) : [Delegate]int;

+function {:builtin ""MapConst""} DelegateMapconstbool(bool) : [Delegate]bool;

+function {:builtin ""MapAnd""} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin ""MapOr""} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin ""MapNot""} DelegateMapnot([Delegate]bool) : [Delegate]bool;

+function {:builtin ""MapIte""} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

+function {:builtin ""MapIte""} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin ""MapLe""} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin ""MapLt""} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin ""MapGe""} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin ""MapGt""} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin ""MapEq""} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

+function {:builtin ""MapIff""} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+function {:builtin ""MapImp""} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

+axiom MultisetEmpty == DelegateMapconstint(0);

 

 function IsRef(u: Union) : (bool);

 axiom (forall x: bool :: {Bool2Union(x)} Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x)));

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b1a8f1a4..8622c3a7 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -55,6 +55,7 @@ namespace BytecodeTranslator {
           }

         }

       }

+      this.uniqueNumberSeed = 0;

     }

 

     public Options Options { get { return this.options; } }

@@ -705,6 +706,35 @@ namespace BytecodeTranslator {
           }

         }

         #endregion

+

+        #region Add free ensures for allocatedness of result (for methods that return references)

+        if (retVariable != null && retVariable.TypedIdent.Type == this.Heap.RefType) {

+          var ens = new Bpl.Ensures(true,

+            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or,

+              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+                Bpl.Expr.Ident(retVariable), Bpl.Expr.Ident(this.Heap.NullRef)),

+              Bpl.Expr.Select(Bpl.Expr.Ident(this.Heap.AllocVariable), Bpl.Expr.Ident(retVariable))

+              ));

+          boogiePostcondition.Add(ens);

+        }

+        #endregion

+        #region Add free ensures for preservation of allocatedness: AllocMapImplies(old($Alloc), $Alloc) == AllocMapConst(true)

+        var preserveAlloc = new Bpl.Ensures(true,

+          Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+            new Bpl.NAryExpr(

+              Bpl.Token.NoToken,

+              new Bpl.FunctionCall(this.Heap.AllocImplies),

+                new Bpl.ExprSeq(

+                  new Bpl.OldExpr(Bpl.Token.NoToken, Bpl.Expr.Ident(this.Heap.AllocVariable)),

+                  Bpl.Expr.Ident(this.Heap.AllocVariable))),

+            new Bpl.NAryExpr(

+              Bpl.Token.NoToken,

+              new Bpl.FunctionCall(this.Heap.AllocConstBool),

+                new Bpl.ExprSeq(Bpl.Expr.True))

+                ));

+        boogiePostcondition.Add(preserveAlloc);

+        #endregion

+

       }

       return procInfo;

     }

@@ -1380,5 +1410,14 @@ namespace BytecodeTranslator {
         }

       }

     }

+

+    private int uniqueNumberSeed;

+    public int UniqueNumberAcrossAllAssemblies {

+      get {

+        return uniqueNumberSeed++;

+      }

+    }

+

+

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 9005b43a..49f932ec 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -56,6 +56,7 @@ namespace BytecodeTranslator
     internal readonly Stack<Bpl.Expr> operandStack = new Stack<Bpl.Expr>();

     private bool captureState;

     private static int captureStateCounter = 0;

+    public IPrimarySourceLocation lastSourceLocation;

 

     #region Constructors

     public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, TraverserFactory factory) {

@@ -88,7 +89,7 @@ namespace BytecodeTranslator
         var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);

         newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);

       }

-      StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null)));

+      StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.sink.UniqueNumberAcrossAllAssemblies) }, null)));

       this.Traverse(methodBody);

       return newTypes;

     }

@@ -206,10 +207,10 @@ namespace BytecodeTranslator
       if (this.sink.Options.instrumentBranches) {

         var tok = conditionalStatement.Token();

         thenTraverser.StmtBuilder.Add(

-          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))

+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.sink.UniqueNumberAcrossAllAssemblies) }, null))

           );

         elseTraverser.StmtBuilder.Add(

-          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))

+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.sink.UniqueNumberAcrossAllAssemblies) }, null))

           );

       }

 

@@ -240,13 +241,6 @@ namespace BytecodeTranslator
 

     }

 

-    private static int counter = 0;

-    public IPrimarySourceLocation lastSourceLocation;

-    internal int NextUniqueNumber() {

-      return counter++;

-    }

-

-

     /// <summary>

     /// 

     /// </summary>