From cbf9ade2c3839f303da41681d40067c28d703072 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 16 Apr 2012 08:45:50 -0700 Subject: 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. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 20 +++++---- BCT/BytecodeTranslator/Program.cs | 7 +++ BCT/BytecodeTranslator/Sink.cs | 54 ++++++++++++------------ BCT/RegressionTests/TranslationTest/UnitTest0.cs | 5 ++- 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 { assemblyName }, heapFactory, new Options(), null, false); + var options = new Options(); + options.monotonicHeap = true; + options.dereference = Options.Dereference.Assume; + BCT.TranslateAssemblyAndWriteOutput(new List { assemblyName }, heapFactory, options, null, false); var fileName = Path.ChangeExtension(assemblyName, "bpl"); var s = File.ReadAllText(fileName); return s; -- cgit v1.2.3