diff options
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 20 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 7 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 54 | ||||
-rw-r--r-- | 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<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;
|