Add options to control the emission of free ensures for

heap monotonicity (and allocatedness of references
returned from a method) as well as the assert/assume
checks that are generated for every object dereference.

4 files changed, 50 insertions, 36 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index acab17a1..b422e836 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -348,16 +348,18 @@ namespace BytecodeTranslator
       #endregion

     }

 

-    private void AssertOrAssumeNonNull(Bpl.IToken token, Bpl.Expr instance, bool assume = true) {

-      Bpl.Cmd c;

-      var n = Bpl.Expr.Ident(this.sink.Heap.NullRef);

-      var neq = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, instance, n);

-      if (assume) {

-        c = new Bpl.AssumeCmd(token, neq);

-      } else {

-        c = new Bpl.AssertCmd(token, neq);

+    private void AssertOrAssumeNonNull(Bpl.IToken token, Bpl.Expr instance) {

+      if (this.sink.Options.dereference != Options.Dereference.None) {

+        Bpl.Cmd c;

+        var n = Bpl.Expr.Ident(this.sink.Heap.NullRef);

+        var neq = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, instance, n);

+        if (this.sink.Options.dereference == Options.Dereference.Assume) {

+          c = new Bpl.AssumeCmd(token, neq);

+        } else {

+          c = new Bpl.AssertCmd(token, neq);

+        }

+        this.StmtTraverser.StmtBuilder.Add(c);

       }

-      this.StmtTraverser.StmtBuilder.Add(c);

     }

 

     internal static bool IsAtomicInstance(IExpression expression) {

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 22b64dca..cf758611 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -69,6 +69,13 @@ namespace BytecodeTranslator {
     [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]

     public bool instrumentBranches = false;

 

+    [OptionDescription("Add free ensures that express heap monotonicity", ShortForm = "heapM")]

+    public bool monotonicHeap = false;

+

+    public enum Dereference { Assert, Assume, None, }

+    [OptionDescription("Assert/Assume on all object dereferences", ShortForm = "deref")]

+    public Dereference dereference = Dereference.Assume;

+

   }

 

   public class BCT {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 8622c3a7..425a6b72 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -707,33 +707,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))

+        if (options.monotonicHeap) {

+          #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(preserveAlloc);

-        #endregion

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

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index bd400303..62ce9155 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,10 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, new Options(), null, false);

+      var options = new Options();

+      options.monotonicHeap = true;

+      options.dereference = Options.Dereference.Assume;

+      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, options, null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;