diff options
| author |  Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2011-11-21 08:56:29 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2011-11-21 08:56:29 +0000 |
| commit | fe2d0ea854d706d7839dd8ebb49ed3d7cb8ea466 (patch) | |
| tree | 6518fd0ebccb534bd935a05c4e8439bae76fe813 | |
| parent | 90dc2aab924b0404d8ff37e8d0184cf5af5e0b36 (diff) | |
| parent | eb67a2565b9d81e5272b4be57d4ed817b3fa9efd (diff) | |
Merge
28 files changed, 793 insertions, 358 deletions
@@ -9,3 +9,4 @@ e57f596b36edd27f66ff7400a6610034ce67d19d emicvccbld_build_2.1.30905.0 f59d45429b672bb429d26e1aff6e9df1d9def6b5 emicvccbld_build_2.1.31022.0 f3b3df39e9877fb2b3fde172f300f995689e6402 emicvccbld_build_2.1.31028.0 f5c14add09d2f57402c94574eeef490d900d58e8 emicvccbld_build_2.1.31109.0 +a25a1feb48848a6cac9ab0fd6480871ad5e9a881 emicvccbld_build_2.1.31116.0 diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index dd65a1f6..59b5d39f 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -318,20 +318,32 @@ namespace BytecodeTranslator /// <summary>
/// If the expression's type is a generic parameter (either method or type),
/// then this returns a "unboxed" expression, i.e., the value as a ref.
- /// Otherwise it just translates the expression and skips the address-of
- /// operation.
+ /// Otherwise it just translates the underlying expression and boxes it.
/// </summary>
public override void TraverseChildren(IAddressOf addressOf)
{
var t = addressOf.Expression.Type;
+ var boogieT = this.sink.CciTypeToBoogie(t);
+
if (t is IGenericParameterReference) {
- // then the expression will be represented by something of type Box
- // but the address of it must be a ref, so do the conversion
- this.Traverse(addressOf.Expression);
- var e = this.TranslatedExpressions.Pop();
- this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));
+ if (boogieT == this.sink.Heap.BoxType) {
+ // then the expression will be represented by something of type Box
+ // but the address of it must be a ref, so do the conversion
+ this.Traverse(addressOf.Expression);
+ var e = this.TranslatedExpressions.Pop();
+ this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));
+ } else {
+ this.Traverse(addressOf.Expression);
+ }
} else {
this.Traverse(addressOf.Expression);
+ var e = this.TranslatedExpressions.Pop();
+
+ Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type);
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
+ this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT));
+ this.TranslatedExpressions.Push(Bpl.Expr.Ident(a));
+
}
}
#endregion
@@ -676,6 +688,16 @@ namespace BytecodeTranslator #region Create the 'this' argument for the function call
thisExpr = null;
if (thisArg != null) {
+
+ // Special case! thisArg is going to be an AddressOf expression if the receiver is a value-type
+ // But if the method's containing type is something that doesn't get translated as a Ref, then
+ // the AddressOf node should be ignored.
+ var addrOf = thisArg as IAddressOf;
+ var boogieType = this.sink.CciTypeToBoogie(methodToCall.ContainingType);
+ if (addrOf != null && boogieType != this.sink.Heap.RefType) {
+ thisArg = addrOf.Expression;
+ }
+
this.Traverse(thisArg);
var e = this.TranslatedExpressions.Pop();
@@ -700,10 +722,27 @@ namespace BytecodeTranslator if (penum.Current == null) {
throw new TranslationException("More arguments than parameters in method call");
}
- this.Traverse(exp);
+
+ var expressionToTraverse = exp;
+ Bpl.Type boogieTypeOfExpression;
+
+ // Special case! exp can be an AddressOf expression if it is a value type being passed by reference.
+ // But since we pass reference parameters by in-out value passing, need to short-circuit the
+ // AddressOf node if the underlying type is not a Ref.
+ var addrOf = exp as IAddressOf;
+ if (addrOf != null) {
+ boogieTypeOfExpression = this.sink.CciTypeToBoogie(addrOf.Expression.Type);
+ if (boogieTypeOfExpression != this.sink.Heap.RefType) {
+ expressionToTraverse = addrOf.Expression;
+ }
+ }
+
+ boogieTypeOfExpression = this.sink.CciTypeToBoogie(expressionToTraverse.Type);
+ this.Traverse(expressionToTraverse);
+
Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter)
- inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(exp.Type), e));
+ if (penum.Current.Type is IGenericParameterReference && this.sink.CciTypeToBoogie(penum.Current.Type) == this.sink.Heap.BoxType)
+ inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e));
else
inexpr.Add(e);
if (penum.Current.IsByReference) {
@@ -711,7 +750,7 @@ namespace BytecodeTranslator if (unboxed == null) {
throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
}
- if (penum.Current.Type is IGenericParameter) {
+ if (penum.Current.Type is IGenericParameterReference) {
var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);
if (boogieType == this.sink.Heap.BoxType) {
Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
@@ -747,8 +786,8 @@ namespace BytecodeTranslator if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);
Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);
- if (resolvedMethod.Type is IGenericParameter) {
- var boogieType = this.sink.CciTypeToBoogie(methodToCall.Type);
+ if (resolvedMethod.Type is IGenericParameterReference) {
+ var boogieType = this.sink.CciTypeToBoogie(resolvedMethod.Type);
if (boogieType == this.sink.Heap.BoxType) {
Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
toBoxed[unboxed] = boxed;
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index c8300189..67fbfdb8 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -218,7 +218,7 @@ namespace BytecodeTranslator { }
var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;
// The decompiler does not turn calls to Assert/Assume into Code Model nodes
- m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);
+ m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);
decompiledModules.Add(m2);
host.RegisterAsLatest(m2);
contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index bcf3ce0b..612854d9 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -133,11 +133,12 @@ namespace BytecodeTranslator { return heap.RefType; // structs are kept on the heap with special rules about assignment
else if (type.IsEnum)
return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
- else if (type is IGenericParameter) {
- var gp = type as IGenericParameter;
- if (gp.MustBeReferenceType || gp.MustBeValueType)
+ else if (type is IGenericParameterReference) {
+ var gp = type.ResolvedType as IGenericParameter;
+ if (gp.MustBeReferenceType)// || gp.MustBeValueType)
return heap.RefType;
- foreach (var c in gp.Constraints){
+ foreach (var c in gp.Constraints) {
+ if (TypeHelper.TypesAreEquivalent(c, type.PlatformType.SystemValueType)) continue;
return CciTypeToBoogie(c);
}
return heap.BoxType;
@@ -214,7 +215,7 @@ namespace BytecodeTranslator { typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
var mangledName = String.Format("{0}_{1}", name, typeName);
if (!localVarMap.TryGetValue(mangledName, out v)) {
- v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));
+ v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, mangledName, t));
localVarMap.Add(mangledName, v);
}
return v;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 3284f217..f68465d1 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -499,38 +499,38 @@ const unique $real_literal_4_0: Real; implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
{
- var d: Real;
- var d2: Real;
+ var d_Real: Real;
+ var d2_Real: Real;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
- d := $real_literal_3_0;
+ d_Real := $real_literal_3_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
- d2 := $real_literal_4_0;
+ d2_Real := $real_literal_4_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
if ($Exception != null)
{
return;
@@ -667,27 +667,33 @@ const unique F$RegressionTestInput.S.b: Field; implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)
{
- var s: Ref;
+ var s_Ref: Ref;
var $tmp0: Ref;
var $tmp1: Ref;
+ var $tmp2: Ref;
+ var $tmp3: Ref;
var $localExc: Ref;
var $label: int;
call $tmp0 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp0);
assume $DynamicType($tmp0) == T$RegressionTestInput.S();
- s := $tmp0;
+ s_Ref := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
call $tmp1 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp1);
assume $DynamicType($tmp1) == T$RegressionTestInput.S();
- s := $tmp1;
+ s_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
- assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;
+ call $tmp2 := Alloc();
+ $Heap := Write($Heap, $tmp2, $BoxField, Ref2Box(s_Ref));
+ assert Box2Int(Read($Heap, $tmp2, F$RegressionTestInput.S.x)) == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
- assert !Box2Bool(Read($Heap, s, F$RegressionTestInput.S.b));
+ call $tmp3 := Alloc();
+ $Heap := Write($Heap, $tmp3, $BoxField, Ref2Box(s_Ref));
+ assert !Box2Bool(Read($Heap, $tmp3, F$RegressionTestInput.S.b));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
- $result := s;
+ $result := s_Ref;
return;
}
@@ -700,14 +706,20 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref)
{
var s: Ref;
+ var $tmp0: Ref;
+ var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
s := s$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
- $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));
+ call $tmp0 := Alloc();
+ $Heap := Write($Heap, $tmp0, $BoxField, Ref2Box(s));
+ $Heap := Write($Heap, $tmp0, F$RegressionTestInput.S.x, Int2Box(3));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
- assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
+ call $tmp1 := Alloc();
+ $Heap := Write($Heap, $tmp1, $BoxField, Ref2Box(s));
+ assert Box2Int(Read($Heap, $tmp1, F$RegressionTestInput.S.x)) == 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
@@ -761,9 +773,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
- var s: Ref;
+ var s_Ref: Ref;
var $tmp0: Ref;
- var t: Ref;
+ var t_Ref: Ref;
var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
@@ -771,21 +783,21 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
call $tmp0 := Alloc();
assume $ArrayLength($tmp0) == 1 * 5;
- s := $tmp0;
+ s_Ref := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
- $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];
+ $ArrayContents := $ArrayContents[s_Ref := $ArrayContents[s_Ref][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
- assert Box2Int($ArrayContents[s][0]) == 2;
+ assert Box2Int($ArrayContents[s_Ref][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
call $tmp1 := Alloc();
assume $ArrayLength($tmp1) == 1 * 4;
- t := $tmp1;
+ t_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
- $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];
+ $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
- assert Box2Int($ArrayContents[t][0]) == 1;
+ assert Box2Int($ArrayContents[t_Ref][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
- assert Box2Int($ArrayContents[s][0]) == 2;
+ assert Box2Int($ArrayContents[s_Ref][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
}
@@ -799,7 +811,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
var $tmp0: Ref;
- var t: Ref;
+ var t_Ref: Ref;
var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
@@ -815,11 +827,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp1 := Alloc();
assume $ArrayLength($tmp1) == 1 * 4;
- t := $tmp1;
+ t_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
- $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];
+ $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
- assert Box2Int($ArrayContents[t][0]) == 1;
+ assert Box2Int($ArrayContents[t_Ref][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
@@ -835,8 +847,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var _loc0: Ref;
- var _loc1: Ref;
+ var _loc0_Ref: Ref;
+ var _loc1_Ref: Ref;
var $localExc: Ref;
var $label: int;
@@ -846,9 +858,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
$ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
- _loc0 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
- _loc1 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
- assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
+ _loc0_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+ _loc1_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+ assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -1246,13 +1258,13 @@ procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var CS$0$0000: Box;
+ var CS$0$0000_Box: Box;
var $tmp0: Ref;
- var __temp_2: Box;
- var __temp_3: Box;
+ var __temp_2_Box: Box;
+ var __temp_3_Box: Box;
var $tmp1: Box;
var $tmp2: Box;
- var y: Box;
+ var y_Box: Box;
var $localExc: Ref;
var $label: int;
@@ -1265,13 +1277,13 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
- CS$0$0000 := $DefaultBox;
+ CS$0$0000_Box := $DefaultBox;
call $tmp0 := Alloc();
- $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000));
+ $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000_Box));
if ($tmp0 != null)
{
- CS$0$0000 := $DefaultBox;
- __temp_2 := CS$0$0000;
+ CS$0$0000_Box := $DefaultBox;
+ __temp_2_Box := CS$0$0000_Box;
}
else
{
@@ -1282,11 +1294,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: return;
}
- __temp_3 := $tmp1;
- __temp_2 := __temp_3;
+ __temp_3_Box := $tmp1;
+ __temp_2_Box := __temp_3_Box;
}
- y := __temp_2;
+ y_Box := __temp_2_Box;
return;
}
@@ -1414,15 +1426,15 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var __temp_1: int;
- var y: int;
+ var __temp_1_int: int;
+ var y_int: int;
var $localExc: Ref;
var $label: int;
x := x$in;
- __temp_1 := 5 / x;
+ __temp_1_int := 5 / x;
x := 3;
- y := __temp_1 + 3;
+ y_int := __temp_1_int + 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
if (x == 3)
{
@@ -1431,11 +1443,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) {
}
- assert (if x == 3 then y <= 8 else false);
+ assert (if x == 3 then y_int <= 8 else false);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
- F$RegressionTestInput.Class0.StaticInt := y;
+ F$RegressionTestInput.Class0.StaticInt := y_int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
- assert y == F$RegressionTestInput.Class0.StaticInt;
+ assert y_int == F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 83cc1869..9484ee38 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -485,38 +485,38 @@ const unique $real_literal_4_0: Real; implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
{
- var d: Real;
- var d2: Real;
+ var d_Real: Real;
+ var d2_Real: Real;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
- d := $real_literal_3_0;
+ d_Real := $real_literal_3_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
- d2 := $real_literal_4_0;
+ d2_Real := $real_literal_4_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
- call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
if ($Exception != null)
{
return;
@@ -653,27 +653,33 @@ var F$RegressionTestInput.S.b: [Ref]bool; implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)
{
- var s: Ref;
+ var s_Ref: Ref;
var $tmp0: Ref;
var $tmp1: Ref;
+ var $tmp2: Ref;
+ var $tmp3: Ref;
var $localExc: Ref;
var $label: int;
call $tmp0 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp0);
assume $DynamicType($tmp0) == T$RegressionTestInput.S();
- s := $tmp0;
+ s_Ref := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
call $tmp1 := Alloc();
call RegressionTestInput.S.#default_ctor($tmp1);
assume $DynamicType($tmp1) == T$RegressionTestInput.S();
- s := $tmp1;
+ s_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
- assert F$RegressionTestInput.S.x[s] == 0;
+ call $tmp2 := Alloc();
+ $BoxField[$tmp2] := Ref2Box(s_Ref);
+ assert F$RegressionTestInput.S.x[$tmp2] == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
- assert !F$RegressionTestInput.S.b[s];
+ call $tmp3 := Alloc();
+ $BoxField[$tmp3] := Ref2Box(s_Ref);
+ assert !F$RegressionTestInput.S.b[$tmp3];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
- $result := s;
+ $result := s_Ref;
return;
}
@@ -686,14 +692,20 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref)
{
var s: Ref;
+ var $tmp0: Ref;
+ var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
s := s$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
- F$RegressionTestInput.S.x[s] := 3;
+ call $tmp0 := Alloc();
+ $BoxField[$tmp0] := Ref2Box(s);
+ F$RegressionTestInput.S.x[$tmp0] := 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
- assert F$RegressionTestInput.S.x[s] == 3;
+ call $tmp1 := Alloc();
+ $BoxField[$tmp1] := Ref2Box(s);
+ assert F$RegressionTestInput.S.x[$tmp1] == 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
@@ -747,9 +759,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
- var s: Ref;
+ var s_Ref: Ref;
var $tmp0: Ref;
- var t: Ref;
+ var t_Ref: Ref;
var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
@@ -757,21 +769,21 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
call $tmp0 := Alloc();
assume $ArrayLength($tmp0) == 1 * 5;
- s := $tmp0;
+ s_Ref := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
- $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];
+ $ArrayContents := $ArrayContents[s_Ref := $ArrayContents[s_Ref][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
- assert Box2Int($ArrayContents[s][0]) == 2;
+ assert Box2Int($ArrayContents[s_Ref][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
call $tmp1 := Alloc();
assume $ArrayLength($tmp1) == 1 * 4;
- t := $tmp1;
+ t_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
- $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];
+ $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
- assert Box2Int($ArrayContents[t][0]) == 1;
+ assert Box2Int($ArrayContents[t_Ref][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
- assert Box2Int($ArrayContents[s][0]) == 2;
+ assert Box2Int($ArrayContents[s_Ref][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
}
@@ -785,7 +797,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
var $tmp0: Ref;
- var t: Ref;
+ var t_Ref: Ref;
var $tmp1: Ref;
var $localExc: Ref;
var $label: int;
@@ -801,11 +813,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp1 := Alloc();
assume $ArrayLength($tmp1) == 1 * 4;
- t := $tmp1;
+ t_Ref := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
- $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];
+ $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
- assert Box2Int($ArrayContents[t][0]) == 1;
+ assert Box2Int($ArrayContents[t_Ref][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
@@ -821,8 +833,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var _loc0: Ref;
- var _loc1: Ref;
+ var _loc0_Ref: Ref;
+ var _loc1_Ref: Ref;
var $localExc: Ref;
var $label: int;
@@ -832,9 +844,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
$ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Box(43)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
- _loc0 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
- _loc1 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
- assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
+ _loc0_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
+ _loc1_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
+ assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -1232,13 +1244,13 @@ procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var CS$0$0000: Box;
+ var CS$0$0000_Box: Box;
var $tmp0: Ref;
- var __temp_2: Box;
- var __temp_3: Box;
+ var __temp_2_Box: Box;
+ var __temp_3_Box: Box;
var $tmp1: Box;
var $tmp2: Box;
- var y: Box;
+ var y_Box: Box;
var $localExc: Ref;
var $label: int;
@@ -1251,13 +1263,13 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
- CS$0$0000 := $DefaultBox;
+ CS$0$0000_Box := $DefaultBox;
call $tmp0 := Alloc();
- $BoxField[$tmp0] := Box2Box(CS$0$0000);
+ $BoxField[$tmp0] := Box2Box(CS$0$0000_Box);
if ($tmp0 != null)
{
- CS$0$0000 := $DefaultBox;
- __temp_2 := CS$0$0000;
+ CS$0$0000_Box := $DefaultBox;
+ __temp_2_Box := CS$0$0000_Box;
}
else
{
@@ -1268,11 +1280,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: return;
}
- __temp_3 := $tmp1;
- __temp_2 := __temp_3;
+ __temp_3_Box := $tmp1;
+ __temp_2_Box := __temp_3_Box;
}
- y := __temp_2;
+ y_Box := __temp_2_Box;
return;
}
@@ -1400,15 +1412,15 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
{
var x: int;
- var __temp_1: int;
- var y: int;
+ var __temp_1_int: int;
+ var y_int: int;
var $localExc: Ref;
var $label: int;
x := x$in;
- __temp_1 := 5 / x;
+ __temp_1_int := 5 / x;
x := 3;
- y := __temp_1 + 3;
+ y_int := __temp_1_int + 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
if (x == 3)
{
@@ -1417,11 +1429,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) {
}
- assert (if x == 3 then y <= 8 else false);
+ assert (if x == 3 then y_int <= 8 else false);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
- F$RegressionTestInput.Class0.StaticInt := y;
+ F$RegressionTestInput.Class0.StaticInt := y_int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
- assert y == F$RegressionTestInput.Class0.StaticInt;
+ assert y_int == F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 028ff1dd..4073c722 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -440,11 +440,12 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
- }
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
}
errorCount = outcome.ErrorCount;
verified = outcome.Verified;
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index ae051b40..676ffd5a 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2161,6 +2161,11 @@ namespace Microsoft.Boogie { {
assume.Attributes = Attributes;
}
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))
+ {
+ assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List<object>(), assume.Attributes);
+ assume.Attributes.Params.Add(this.callee);
+ }
#endregion
newBlockBody.Add(assume);
}
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 0f29c9a0..cae8bd92 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -533,6 +533,13 @@ namespace Microsoft.Boogie { return l.asBigNum.ToIntSafe;
return defl;
}
+
+ public override Absy Clone() {
+ List<object> newParams = new List<object>();
+ foreach (object o in Params)
+ newParams.Add(o);
+ return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
+ }
}
public class Trigger : Absy {
@@ -546,7 +553,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Pos || Tr.Length == 1);
}
-
public Trigger Next;
public Trigger(IToken tok, bool pos, ExprSeq tr)
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 7519fb4c..c7950c9a 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -585,9 +585,8 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl> | { Spec<pre, mods, post> }
ImplBody<out locals, out stmtList>
(.
- // here we attach kv only to the Procedure, not its implementation
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
.)
)
(. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d2bdee62..a3bb44ba 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -264,7 +264,6 @@ namespace Microsoft.Boogie { /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>
public bool Parse([Captured] string[]/*!*/ args) {
Contract.Requires(cce.NonNullElements(args));
- Contract.Ensures(-2 <= Contract.Result<int>() && Contract.Result<int>() <= 2 && Contract.Result<int>() != 0);
// save the command line options for the log files
Environment += "Command Line Options: " + args.Concat(" ");
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index adc7e2f0..c9f6445c 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -388,6 +388,27 @@ namespace Microsoft.Boogie { codeCopier.OldSubst = null;
}
+ private Cmd InlinedRequires(Implementation impl, CallCmd callCmd, Requires req) {
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ if (req.Free)
+ reqCopy.Condition = Expr.True;
+ else
+ reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
+ AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ return a;
+ }
+
+ private Cmd InlinedEnsures(Implementation impl, CallCmd callCmd, Ensures ens) {
+ if (impl.FindExprAttribute("inline") != null && !ens.Free) {
+ Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
+ return new AssertEnsuresCmd(ensCopy);
+ }
+ else {
+ return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
+ }
+ }
// result[0] is the entry block
protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {
@@ -418,17 +439,20 @@ namespace Microsoft.Boogie { inCmds.Add(cmd);
}
- // inject non-free requires
+ // inject requires
for (int i = 0; i < proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
+ inCmds.Add(InlinedRequires(impl, callCmd, req));
+ /*
if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {
- Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ Requires reqCopy = (Requires)cce.NonNull(req.Clone());
reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);
Contract.Assert(a != null);
a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
inCmds.Add(a);
}
+ */
}
VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);
@@ -483,16 +507,19 @@ namespace Microsoft.Boogie { // create out block
CmdSeq outCmds = new CmdSeq();
- // inject non-free ensures
+ // inject ensures
for (int i = 0; i < proc.Ensures.Length; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
+ outCmds.Add(InlinedEnsures(impl, callCmd, ens));
+ /*
if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {
- Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);
+ AssertCmd a = new AssertEnsuresCmd(ensCopy);
Contract.Assert(a != null);
outCmds.Add(a);
}
+ */
}
// assign out params
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 34f43896..5bfbbfc2 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -503,7 +503,7 @@ private class BvBounds : Expr { }
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
} else SynErr(91);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 8c604b8a..745d50ef 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -33,8 +33,6 @@ namespace Microsoft.Dafny public bool ForceCompile = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
- Contract.Requires(name != null);
- Contract.Requires(ps != null);
var args = ps.args; // convenient synonym
switch (name) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 88f95f30..d1e41663 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5068,8 +5068,8 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
Contract.Requires(heap != null);
Contract.Requires(thisVar != null);
- Contract.Invariant(layerOffset == 0 || layerOffset == 1);
- Contract.Invariant(modifiesFrame != null);
+ Contract.Requires(layerOffset == 0 || layerOffset == 1);
+ Contract.Requires(modifiesFrame != null);
this.translator = translator;
this.predef = predef;
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 97c22cc9..b0c8fabf 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -17,60 +17,46 @@ using System.Threading; using VC;
namespace Microsoft.Boogie.Houdini {
- public class HoudiniVCGen : VCGen {
- private Checker checker;
+ public class HoudiniSession {
+ public static double proverTime = 0;
private string descriptiveName;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
- CounterexampleCollector collector;
+ ConditionGeneration.CounterexampleCollector collector;
- public VCExpressionGenerator VCExprGenerator {
- get {
- return checker.VCExprGen;
- }
- }
-
- public Boogie2VCExprTranslator BooogieExprTranslator {
- get {
- DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;
- return proverContext.BoogieExprTranslator;
- }
- }
-
- public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile) {
+ public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl, string logFilePath, bool appendLogFile) {
descriptiveName = impl.Name;
- collector = new CounterexampleCollector();
+ collector = new ConditionGeneration.CounterexampleCollector();
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
if (CommandLineOptions.Clo.SoundnessSmokeTest) {
throw new Exception("HoudiniVCGen does not support Soundness smoke test.");
}
- ConvertCFG2DAG(impl, program);
+ vcgen.ConvertCFG2DAG(impl, program);
ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo);
Hashtable/*<int, Absy!>*/ label2absy;
- checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
- if (!(checker.TheoremProver is Z3ProcessTheoremProver || checker.TheoremProver is SMTLibProcessTheoremProver)) {
- throw new Exception("HdnChecker only works with z3");
- }
- conjecture = GenerateVC(impl, null, out label2absy, checker);
+
+ conjecture = vcgen.GenerateVC(impl, null, out label2absy, checker);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
- handler = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);
}
else {
- handler = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);
}
}
- public ProverInterface.Outcome Verify(VCExpr axiom, out List<Counterexample> errors) {
+ public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {
collector.examples.Clear();
VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);
+
+ DateTime now = DateTime.Now;
checker.BeginCheck(descriptiveName, vc, handler);
WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
-
ProverInterface.Outcome proverOutcome = checker.ReadOutcome();
+ proverTime += (DateTime.Now - now).TotalSeconds;
+
if (proverOutcome == ProverInterface.Outcome.Invalid) {
Contract.Assume(collector.examples != null);
if (collector.examples.Count == 0) {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 7113293b..27b8d05f 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -193,7 +193,6 @@ namespace Microsoft.Boogie.Houdini { }
-
public abstract class ObservableHoudini {
private List<HoudiniObserver> observers = new List<HoudiniObserver>();
@@ -251,7 +250,9 @@ namespace Microsoft.Boogie.Houdini { public class Houdini : ObservableHoudini {
private Program program;
private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
- private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;
+ private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;
+ private VCGen vcgen;
+ private Checker checker;
private Graph<Implementation> callGraph;
private bool continueAtError;
@@ -260,21 +261,20 @@ namespace Microsoft.Boogie.Houdini { this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
this.houdiniConstants = CollectExistentialConstants();
- this.vcgenSessions = PrepareVCGenSessions();
- }
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
- private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {
- Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
+ Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
foreach (Implementation impl in callGraph.Nodes) {
// make a different simplify log file for each function
String simplifyLog = null;
if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
}
- HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- vcgenSessions.Add(impl, vcgen);
+ HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ houdiniSessions.Add(impl, session);
}
- return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);
+ this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
@@ -362,9 +362,10 @@ namespace Microsoft.Boogie.Houdini { return false;
}
- private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary<string, bool> currentAssignment) {
- Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;
- VCExpressionGenerator exprGen = vcgen.VCExprGenerator;
+ private VCExpr BuildAxiom(Dictionary<string, bool> currentAssignment) {
+ DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;
+ Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;
+ VCExpressionGenerator exprGen = checker.VCExprGen;
VCExpr expr = VCExpressionGenerator.True;
foreach (KeyValuePair<string, bool> kv in currentAssignment) {
@@ -389,46 +390,44 @@ namespace Microsoft.Boogie.Houdini { return initial;
}
- private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List<Counterexample> errors) {
- HoudiniVCGen vcgen;
- vcgenSessions.TryGetValue(implementation, out vcgen);
+ private ProverInterface.Outcome VerifyUsingAxiom(HoudiniSession session, Implementation implementation, VCExpr axiom, out List<Counterexample> errors) {
if (vcgen == null)
throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
- ProverInterface.Outcome outcome = TryCatchVerify(vcgen, axiom, out errors);
+ ProverInterface.Outcome outcome = TryCatchVerify(session, axiom, out errors);
return outcome;
}
// the main procedure that checks a procedure and updates the
// assignment and the worklist
- private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current,
+ private ProverInterface.Outcome HoudiniVerifyCurrent(
+ HoudiniSession session,
+ HoudiniState current,
Program program,
out List<Counterexample> errors,
out bool exc) {
- HoudiniVCGen vcgen;
if (current.Implementation == null)
throw new Exception("HoudiniVerifyCurrent has null implementation");
Implementation implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation, out vcgen);
if (vcgen == null)
throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
- ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
+ ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(session, current, program, out errors, out exc);
return outcome;
}
- private ProverInterface.Outcome VerifyCurrent(HoudiniState current,
+ private ProverInterface.Outcome VerifyCurrent(
+ HoudiniSession session,
+ HoudiniState current,
Program program,
out List<Counterexample> errors,
out bool exc) {
- HoudiniVCGen vcgen;
if (current.Implementation != null) {
Implementation implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation, out vcgen);
if (vcgen == null)
throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
- ProverInterface.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
+ ProverInterface.Outcome outcome = TrySpinSameFunc(session, current, program, out errors, out exc);
return outcome;
}
else {
@@ -494,17 +493,17 @@ namespace Microsoft.Boogie.Houdini { private void FlushWorkList(HoudiniState current) {
this.NotifyFlushStart();
- HoudiniVCGen vcgen;
- vcgenSessions.TryGetValue(current.Implementation, out vcgen);
- VCExpr axiom = BuildAxiom(vcgen, current.Assignment);
+ VCExpr axiom = BuildAxiom(current.Assignment);
while (current.WorkList.Count > 0) {
this.NotifyIteration();
current.Implementation = current.WorkList.Peek();
this.NotifyImplementation(current.Implementation);
+ HoudiniSession session;
+ houdiniSessions.TryGetValue(current.Implementation, out session);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
+ ProverInterface.Outcome outcome = VerifyUsingAxiom(session, current.Implementation, axiom, out errors);
UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
this.NotifyOutcome(outcome);
@@ -686,22 +685,20 @@ namespace Microsoft.Boogie.Houdini { HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
this.NotifyStart(program, houdiniConstants.Keys.Count);
-
-
while (current.WorkList.Count > 0) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
- HoudiniVCGen vcgen;
- vcgenSessions.TryGetValue(current.Implementation, out vcgen);
- VCExpr axiom = BuildAxiom(vcgen, current.Assignment);
+ VCExpr axiom = BuildAxiom(current.Assignment);
this.NotifyAssignment(current.Assignment);
current.Implementation = current.WorkList.Peek();
this.NotifyImplementation(current.Implementation);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
+ HoudiniSession session;
+ houdiniSessions.TryGetValue(current.Implementation, out session);
+ ProverInterface.Outcome outcome = VerifyUsingAxiom(session, current.Implementation, axiom, out errors);
this.NotifyOutcome(outcome);
UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
@@ -725,14 +722,16 @@ namespace Microsoft.Boogie.Houdini { while (current.WorkList.Count > 0) {
bool exceptional = false;
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
current.Implementation = current.WorkList.Peek();
this.NotifyImplementation(current.Implementation);
+ HoudiniSession session;
+ houdiniSessions.TryGetValue(current.Implementation, out session);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional);
+ ProverInterface.Outcome outcome = VerifyCurrent(session, current, program, out errors, out exceptional);
// updates to worklist already done in VerifyCurrent, unless there was an exception
if (exceptional) {
@@ -764,14 +763,16 @@ namespace Microsoft.Boogie.Houdini { while (current.WorkList.Count > 0) {
bool exceptional = false;
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
current.Implementation = current.WorkList.Peek();
this.NotifyImplementation(current.Implementation);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);
+ HoudiniSession session;
+ this.houdiniSessions.TryGetValue(current.Implementation, out session);
+ ProverInterface.Outcome outcome = HoudiniVerifyCurrent(session, current, program, out errors, out exceptional);
// updates to worklist already done in VerifyCurrent, unless there was an exception
if (exceptional) {
@@ -923,10 +924,10 @@ namespace Microsoft.Boogie.Houdini { return null;
}
- private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List<Counterexample> errors) {
+ private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, VCExpr axiom, out List<Counterexample> errors) {
ProverInterface.Outcome outcome;
try {
- outcome = vcgen.Verify(axiom, out errors);
+ outcome = session.Verify(checker, axiom, out errors);
}
catch (VCGenException e) {
Contract.Assume(e != null);
@@ -943,9 +944,10 @@ namespace Microsoft.Boogie.Houdini { //version of TryCatchVerify that spins on the same function
//as long as the current assignment is changing
- private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current,
+ private ProverInterface.Outcome TrySpinSameFunc(
+ HoudiniSession session,
+ HoudiniState current,
Program program,
- HoudiniVCGen vcgen,
out List<Counterexample> errors,
out bool exceptional) {
Contract.Assert(current.Implementation != null);
@@ -958,15 +960,14 @@ namespace Microsoft.Boogie.Houdini { do {
if (pastFirstIter) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
}
- this.vcgenSessions.TryGetValue(current.Implementation, out vcgen);
- VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);
+ VCExpr currentAx = BuildAxiom(current.Assignment);
this.NotifyAssignment(current.Assignment);
- outcome = vcgen.Verify(currentAx, out errors);
+ outcome = session.Verify(checker, currentAx, out errors);
this.NotifyOutcome(outcome);
DebugRefutedCandidates(current.Implementation, errors);
@@ -1004,30 +1005,37 @@ namespace Microsoft.Boogie.Houdini { }
//Similar to TrySpinSameFunc except no Candidate logic
- private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current,
+ private ProverInterface.Outcome HoudiniVerifyCurrentAux(
+ HoudiniSession session,
+ HoudiniState current,
Program program,
- HoudiniVCGen vcgen,
out List<Counterexample> errors,
out bool exceptional) {
Contract.Assert(current.Implementation != null);
ProverInterface.Outcome outcome;
+ // the following initialization is there just to satisfy the compiler
+ // which apparently does not understand the semantics of do-while statements
errors = null;
outcome = ProverInterface.Outcome.Undetermined;
+
try {
bool trySameFunc = true;
bool pastFirstIter = false; //see if this new loop is even helping
do {
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+
if (pastFirstIter) {
- System.GC.Collect();
+ //System.GC.Collect();
this.NotifyIteration();
}
- VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);
+ VCExpr currentAx = BuildAxiom(current.Assignment);
this.NotifyAssignment(current.Assignment);
//check the VC with the current assignment
- outcome = vcgen.Verify(currentAx, out errors);
+ outcome = session.Verify(checker, currentAx, out errors);
this.NotifyOutcome(outcome);
DebugRefutedCandidates(current.Implementation, errors);
@@ -1041,13 +1049,9 @@ namespace Microsoft.Boogie.Houdini { }
else { //continue
trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = ProverInterface.Outcome.Undetermined;
}
pastFirstIter = true;
} while (trySameFunc && current.WorkList.Count > 0);
-
}
catch (VCGenException e) {
Contract.Assume(e != null);
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 1d55fc13..e4dd3e46 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -444,7 +444,7 @@ namespace Microsoft.Boogie.ModelViewer private void ExpandParents(SkeletonItem item)
{
item = item.parent;
- while (item != null && !item.Expanded) {
+ while (item != null) {
item.Expanded = true;
item = item.parent;
}
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 10e4db10..6fd068a8 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -48,9 +48,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc public List<StateNode> states = new List<StateNode>();
public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();
+ Dictionary<Model.Element, string> datatypeLongName = new Dictionary<Model.Element, string>();
+
Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();
public const string selfMarker = "\\self";
+ public const int maxDatatypeNameLength = 5;
public VccModel(Model m, ViewOptions opts)
: base(m, opts)
@@ -422,6 +425,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return name.Substring(5);
}
+ if (name == "$result") {
+ kind = "function return value";
+ return "\\result";
+ }
+
if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {
kind = "call result";
return name;
@@ -686,7 +694,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var fldName = tpl.Func.Name.Substring(3);
var idx = fldName.LastIndexOf('.');
if (idx > 0) {
- return fldName.Substring(0, idx).Replace("_vcc_math_type_", ""); + return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
}
}
@@ -1197,7 +1205,58 @@ namespace Microsoft.Boogie.ModelViewer.Vcc }
}
- private string CanonicalBaseNameCore(string name, Model.Element elt)
+ private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)
+ {
+ Model.FuncTuple ctor = null;
+ int len = 1;
+ string dataTypeType = null;
+ foreach (var app in elt.References) {
+ var n = app.Func.Name;
+ if (app.Result == elt && n.StartsWith("DF#")) {
+ ctor = app;
+ }
+ var tmp = DataTypeName(elt, app);
+ if (tmp != null) dataTypeType = tmp;
+ }
+
+ if (dataTypeType != null) {
+ if (ctor != null)
+ sb.Append(ctor.Func.Name.Substring(3));
+ else
+ sb.Append(DataTypeShortName(elt, dataTypeType));
+ if (ctor != null && ctor.Args.Length > 0) {
+ if (level <= 0) sb.Append("(...)");
+ else {
+ sb.Append("(");
+ for (int i = 0; i < ctor.Args.Length; ++i) {
+ if (i != 0) sb.Append(", ");
+ len += DataTypeToString(sb, level - 1, ctor.Args[i]);
+ }
+ sb.Append(")");
+ }
+ }
+ } else {
+ sb.Append(CanonicalName(elt));
+ }
+ return len;
+ }
+
+ private string DataTypeShortName(Model.Element elt, string tp)
+ {
+ var baseName = tp;
+
+ var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);
+ if (hd != null) {
+ foreach (var nm in hd.References) {
+ if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
+ baseName = nm.Func.Name.Substring(3);
+ }
+ }
+
+ return baseName;
+ }
+
+ private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
{
var vm = this;
@@ -1229,18 +1288,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var dtpName = DataTypeName(elt, tpl);
if (dtpName != null) {
- var dgh = model.TryGetFunc("DGH#" + dtpName);
- if (dgh != null) {
- var hd = dgh.TryEval(elt);
- if (hd != null) {
- foreach (var nm in hd.References) {
- if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
- return nm.Func.Name.Substring(3);
- }
-
- }
+ var sb = new StringBuilder();
+ string prev = null;
+ datatypeLongName[elt] = "*SELF*"; // in case we recurse (but this shouldn't happen)
+ for (int lev = 0; lev < 10; lev++) {
+ sb.Length = 0;
+ var len = DataTypeToString(sb, lev, elt);
+ if (prev == null || len <= maxDatatypeNameLength)
+ prev = sb.ToString();
}
- return dtpName;
+
+ datatypeLongName[elt] = prev;
+ suff = NameSeqSuffix.WhenNonZero;
+ return prev;
}
}
@@ -1267,9 +1327,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc suff = NameSeqSuffix.None;
return lit;
}
+ if (datatypeLongName.TryGetValue(elt, out lit)) {
+ suff = NameSeqSuffix.WhenNonZero;
+ return lit;
+ }
var name = base.CanonicalBaseName(elt, out suff);
- name = CanonicalBaseNameCore(name, elt);
+ name = CanonicalBaseNameCore(name, elt, true, ref suff);
return name;
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 7b623bce..2f7267b1 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -101,7 +101,7 @@ namespace Microsoft.Boogie { /// <summary>
/// Constructor. Initialize a checker with the program and log file.
/// </summary>
- public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
@@ -158,7 +158,6 @@ namespace Microsoft.Boogie { }
foreach (Declaration decl in prog.TopLevelDeclarations) {
Contract.Assert(decl != null);
- bool expand = false;
Axiom ax = decl as Axiom;
if (ax != null) {
ctx.AddAxiom(ax, null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a52a7087..cb28cd7d 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -894,7 +894,7 @@ namespace VC { string log = logFilePath;
if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
log = log + "." + checkers.Count;
- Checker ch = new Checker(this, program, log, appendLogFile, impl, timeout);
+ Checker ch = new Checker(this, program, log, appendLogFile, timeout);
Contract.Assert(ch != null);
checkers.Add(ch);
return ch;
@@ -909,7 +909,7 @@ namespace VC { }
- protected class CounterexampleCollector : VerifierCallback {
+ public class CounterexampleCollector : VerifierCallback {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(examples));
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 0bcbad35..9ebc4fb3 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -27,6 +27,7 @@ namespace VC public static Dictionary<string, int> callTree = null;
public int numInlined = 0;
public readonly static string recordProcName = "boogie_si_record";
+ private bool useSummary;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -47,6 +48,7 @@ namespace VC this.GenerateVCsForStratifiedInlining(program);
PersistCallTree = false;
+ useSummary = false;
}
public static RECORD_TYPES getRecordType(Bpl.Type type)
@@ -1053,9 +1055,11 @@ namespace VC return checker.numQueries;
}
}
+ // For making summary queries on the side
+ public StratifiedCheckerInterface checker2;
public VerificationState(VCExpr vcMain, FCallHandler calls,
- ProverInterface.ErrorHandler reporter, Checker checker)
+ ProverInterface.ErrorHandler reporter, Checker checker, Checker checker2)
{
this.vcMain = vcMain;
this.calls = calls;
@@ -1063,13 +1067,18 @@ namespace VC if (checker.TheoremProver is ApiProverInterface)
{
this.checker = new ApiChecker(vcMain, reporter , checker);
+ if(checker2 != null)
+ this.checker2 = new ApiChecker(VCExpressionGenerator.False, new EmptyErrorHandler(), checker2);
}
else
{
this.checker = new NormalChecker(vcMain, reporter, checker);
+ if(checker2 != null)
+ this.checker2 = new NormalChecker(VCExpressionGenerator.False, new EmptyErrorHandler(), checker2);
}
vcSize = 0;
expansionCount = 0;
+
}
public void updateMainVC(VCExpr vcMain)
@@ -1121,7 +1130,7 @@ namespace VC vcMain = calls.Mutate(vcMain, true);
// Put all of the necessary state into one object
- var vState = new VerificationState(vcMain, calls, new EmptyErrorHandler(), checker);
+ var vState = new VerificationState(vcMain, calls, new EmptyErrorHandler(), checker, null);
vState.coverageManager = null;
// We'll restore the original state of the theorem prover at the end
@@ -1326,13 +1335,23 @@ namespace VC incrementalSearch = false;
createVConDemand = false;
break;
+ case 6:
+ incrementalSearch = true;
+ createVConDemand = true;
+ useSummary = true;
+ break;
}
#endregion
// Get the checker
Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
-
+ Checker checker2 = null;
+ if (useSummary)
+ {
+ checker2 = new Checker(this, program, "checker2.txt", true, CommandLineOptions.Clo.ProverKillTime);
+ }
+
// Record current time
var startTime = DateTime.Now;
@@ -1370,13 +1389,17 @@ namespace VC calls.setCurrProcAsMain();
vc = calls.Mutate(vc, true);
reporter.SetCandidateHandler(calls);
+ calls.id2VC.Add(0, vc);
+
+ // Identify summary candidates: Match ensure clauses with the appropriate call site
+ if (useSummary) calls.matchSummaries();
// create a process for displaying coverage information
var coverageManager = new CoverageGraphManager(calls);
coverageManager.addMain();
// Put all of the necessary state into one object
- var vState = new VerificationState(vc, calls, reporter, checker);
+ var vState = new VerificationState(vc, calls, reporter, checker, checker2);
vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
vState.coverageManager = coverageManager;
@@ -1441,6 +1464,9 @@ namespace VC int iters = 0;
+ // for blocking candidates (and focussing on a counterexample)
+ var block = new HashSet<int>();
+
// Process tasks while not done. We're done when:
// case 1: (correct) We didn't find a bug (either an over-approx query was valid
// or we reached the recursion bound) and the task is "step"
@@ -1487,10 +1513,22 @@ namespace VC break;
}
+ var summary = calls.getSummary();
+ if (useSummary && summary != null)
+ {
+ vState.checker.Push();
+ vState.checker.AddAxiom(summary);
+ }
+
// Stratified Step
- ret = stratifiedStep(bound, vState);
+ ret = stratifiedStep(bound, vState, block);
iters++;
+ if (useSummary && summary != null)
+ {
+ vState.checker.Pop();
+ }
+
// Sorry, out of luck (time/memory)
if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
{
@@ -1507,27 +1545,45 @@ namespace VC }
else if (ret == Outcome.Correct)
{
- // Correct
- done = 1;
- coverageManager.reportCorrect();
+ if (block.Count == 0)
+ {
+ // Correct
+ done = 1;
+ coverageManager.reportCorrect();
+ }
+ else
+ {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
+ }
}
else if (ret == Outcome.ReachedBound)
{
- // Increment bound
- var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
- foreach (var id in calls.currCandidates)
+ if (block.Count == 0)
{
- var rb = calls.getRecursionBound(id);
- if (rb <= bound) continue;
- if (rb < minRecReached) minRecReached = rb;
- }
- bound = minRecReached;
+ // Increment bound
+ var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
+ foreach (var id in calls.currCandidates)
+ {
+ var rb = calls.getRecursionBound(id);
+ if (rb <= bound) continue;
+ if (rb < minRecReached) minRecReached = rb;
+ }
+ bound = minRecReached;
- if (bound > CommandLineOptions.Clo.RecursionBound)
+ if (bound > CommandLineOptions.Clo.RecursionBound)
+ {
+ // Correct under bound
+ done = 1;
+ coverageManager.reportCorrect(bound);
+ }
+ }
+ else
{
- // Correct under bound
- done = 1;
- coverageManager.reportCorrect(bound);
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
}
}
else
@@ -1535,6 +1591,12 @@ namespace VC // Do inlining
Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
Contract.Assert(reporter.candidatesToExpand.Count != 0);
+ if (useSummary)
+ {
+ // compute candidates to block
+ block = new HashSet<int>(calls.currCandidates);
+ block.ExceptWith(reporter.candidatesToExpand);
+ }
#region expand call tree
@@ -1593,7 +1655,7 @@ namespace VC callTree.Add(calls.getPersistentId(id), 0);
}
}
-
+ if (checker2 != null) checker2.Close();
return ret;
}
@@ -1932,7 +1994,7 @@ namespace VC }
// A step of the stratified inlining algorithm: both under-approx and over-approx queries
- private Outcome stratifiedStep(int bound, VerificationState vState)
+ private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block)
{
Outcome ret;
List<int> unsatCore;
@@ -1959,7 +2021,6 @@ namespace VC assumptions.Add(calls.getFalseExpr(id));
ids.Add(id);
}
-
ret = checker.CheckAssumptions(assumptions, out unsatCore);
if (!CommandLineOptions.Clo.UseUnsatCoreForInlining) break;
if (ret != Outcome.Correct) break;
@@ -2016,8 +2077,18 @@ namespace VC {
if (calls.getRecursionBound(id) <= bound)
{
- //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id));
- allFalse = false;
+ if (block.Contains(id))
+ {
+ Contract.Assert(useSummary);
+ //checker.AddAxiom(calls.getFalseExpr(id));
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ else
+ {
+ //checker.TheoremProver.PushVCExpression(calls.getTrueExpr(id));
+ allFalse = false;
+ }
}
else
{
@@ -2053,6 +2124,41 @@ namespace VC return ret;
}
+ if (useSummary)
+ {
+ // Find the set of candidates with valid summaries
+ var assumeTrueCandidates = new HashSet<int>(vState.calls.currCandidates);
+ assumeTrueCandidates.ExceptWith(block);
+ // Find all nodes that have children only in assumeTrueCandidates
+ var overApproxNodes = FindNodes(vState.calls.candidateParent, vState.calls.currCandidates, assumeTrueCandidates);
+ overApproxNodes.IntersectWith(calls.summaryCandidates.Keys);
+ foreach (var id in overApproxNodes)
+ {
+ var post = getPostOrder(vState.calls.candidateParent, id);
+ var summary = calls.getSummary();
+ vState.checker2.Push();
+ vState.checker2.AddAxiom(summary);
+ foreach (var cid in post) vState.checker2.AddAxiom(calls.id2VC[cid]);
+ vState.checker2.AddAxiom(calls.id2ControlVar[id]);
+
+ foreach (var tup in calls.summaryCandidates[id])
+ {
+ Console.WriteLine("Going to try ({0} ==> {1}) on {2}", tup.Item1, tup.Item2, id);
+ Console.WriteLine("Call expr: {0}", calls.id2Candidate[id]);
+ vState.checker2.Push();
+ vState.checker2.AddAxiom(vState.checker2.underlyingChecker.VCExprGen.Not(tup.Item2));
+ var outcome = vState.checker2.CheckVC();
+ vState.checker2.Pop();
+ if (outcome == Outcome.Correct)
+ {
+ Console.WriteLine("Found summary: {0}", tup.Item1);
+ calls.trueSummaryConst.Add(tup.Item1);
+ }
+ }
+ vState.checker2.Pop();
+ }
+ }
+
// Nothing more can be done with current recursion bound.
return Outcome.ReachedBound;
}
@@ -2064,6 +2170,55 @@ namespace VC return ret;
}
+ // returns children of root in post order
+ static List<int> getPostOrder(Dictionary<int, int> parents, int root)
+ {
+ var children = new Dictionary<int, HashSet<int>>();
+ foreach (var id in parents.Keys) children.Add(id, new HashSet<int>());
+ children.Add(0, new HashSet<int>());
+ foreach (var kvp in parents) children[kvp.Value].Add(kvp.Key);
+ return getPostOrder(children, root);
+ }
+ static List<int> getPostOrder(Dictionary<int, HashSet<int>> children, int root)
+ {
+ var ret = new List<int>();
+ foreach (var ch in children[root]) ret.AddRange(getPostOrder(children, ch));
+ ret.Add(root);
+ return ret;
+ }
+
+ // Returns the set of candidates whose child leaves are all "good"
+ static HashSet<int> FindNodes(Dictionary<int, int> parents, HashSet<int> allLeaves,
+ HashSet<int> goodLeaves)
+ {
+ var ret = new HashSet<int>();
+ var leaves = new Dictionary<int, HashSet<int>>();
+ leaves.Add(0, new HashSet<int>());
+ parents.Keys.Iter(n => leaves.Add(n, new HashSet<int>()));
+ allLeaves.Iter(l => leaves[l].Add(l));
+
+ foreach (var l in allLeaves)
+ {
+ var curr = l;
+ leaves[curr].Add(l);
+ while (parents.ContainsKey(curr))
+ {
+ curr = parents[curr];
+ leaves[curr].Add(l);
+ }
+ }
+
+ foreach (var kvp in leaves)
+ {
+ if (kvp.Value.IsSubsetOf(goodLeaves))
+ {
+ ret.Add(kvp.Key);
+ }
+ }
+
+ return ret;
+ }
+
// A counter for adding new variables
static int newVarCnt = 0;
@@ -2149,9 +2304,11 @@ namespace VC calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
if(vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
-
+ if(useSummary) calls.matchSummaries();
+
//expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
expansion = checker.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
+ calls.id2VC.Add(id, expansion);
exprToPush = checker.VCExprGen.And(exprToPush, expansion);
}
@@ -2227,6 +2384,7 @@ namespace VC calls.currCandidates.Remove(id);
// Record the new set of candidates and rename absy labels
+
calls.currInlineCount = id;
calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
@@ -2321,6 +2479,7 @@ namespace VC public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
+ public Dictionary<int, VCExpr> id2VC;
public Dictionary<string/*!*/, int>/*!*/ label2Id;
// Stores the candidate from which this one originated
public Dictionary<int, int> candidateParent;
@@ -2340,6 +2499,14 @@ namespace VC // first argument (used for obtaining concrete values in error trace)
public Dictionary<int, VCExpr> argExprMap;
+ // map from candidate to summary candidates
+ public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
+ private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
+ // set of all boolean guards of summaries
+ public HashSet<VCExprVar> allSummaryConst;
+ // The summary: boolean guards that are true
+ public HashSet<VCExprVar> trueSummaryConst;
+
public HashSet<int> forcedCandidates;
////////////////////////////
@@ -2420,6 +2587,11 @@ namespace VC forcedCandidates = new HashSet<int>();
id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
+ summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
+ summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
+ allSummaryConst = new HashSet<VCExprVar>();
+ trueSummaryConst = new HashSet<VCExprVar>();
+ id2VC = new Dictionary<int, VCExpr>();
}
public void Clear()
@@ -2711,6 +2883,23 @@ namespace VC }
}
+ // summary candidate
+ if (lop.label.Substring(1).StartsWith("candidate_"))
+ {
+ var pname = lop.label.Substring("candidate_".Length + 1);
+
+ if (!summaryTemp.ContainsKey(pname))
+ summaryTemp.Add(pname, new List<Tuple<VCExprVar, VCExpr>>());
+
+ var expr = retnary[0] as VCExprNAry;
+ if (expr == null) return retnary[0];
+ if (expr.Op != VCExpressionGenerator.ImpliesOp) return retnary[0];
+ var tup = Tuple.Create(expr[0] as VCExprVar, expr[1]);
+ summaryTemp[pname].Add(tup);
+
+ return retnary[0];
+ }
+
// Else, rename label
string newLabel = RenameAbsyLabel(lop.label);
if (lop.pos)
@@ -2724,8 +2913,84 @@ namespace VC }
+ // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
+ // the appropriate candidate they came from
+ public void matchSummaries()
+ {
+ var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
+ foreach (var id in recentlyAddedCandidates)
+ {
+ var collect = new CollectVCVars();
+ var proc = getProc(id);
+ if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
+ id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
+ }
+
+ foreach (var kvp in summaryTemp)
+ {
+ Contract.Assert (id2Set.ContainsKey(kvp.Key));
+ var ls = id2Set[kvp.Key];
+ foreach (var tup in kvp.Value)
+ {
+ var collect = new CollectVCVars();
+ var s1 = collect.Collect(tup.Item2, true);
+ var found = false;
+ foreach (var t in ls)
+ {
+ var s2 = t.Item2;
+ if (s1.IsSubsetOf(s2))
+ {
+ if (!summaryCandidates.ContainsKey(t.Item1))
+ summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
+ summaryCandidates[t.Item1].Add(tup);
+ allSummaryConst.Add(tup.Item1);
+ found = true;
+ break;
+ }
+ }
+ Contract.Assert(found);
+ }
+ }
+ summaryTemp.Clear();
+ }
+
+ public VCExpr getSummary()
+ {
+ if (allSummaryConst.Count == 0) return null;
+
+ var ret = VCExpressionGenerator.True;
+ foreach (var c in allSummaryConst)
+ {
+ if (trueSummaryConst.Contains(c))
+ {
+ ret = Gen.And(ret, c);
+ }
+ else
+ {
+ ret = Gen.And(ret, Gen.Not(c));
+ }
+ }
+ return ret;
+ }
} // end FCallHandler
+ // Collects the set of all VCExprVar in a given VCExpr
+ class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool>
+ {
+ public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg)
+ {
+ var ret = new HashSet<VCExprVar>();
+ ret.Add(node);
+ return ret;
+ }
+
+ protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg)
+ {
+ var ret = new HashSet<VCExprVar>();
+ results.ForEach(s => ret.UnionWith(s));
+ return ret;
+ }
+ }
public class FCallInliner : MutatingVCExprVisitor<bool>
{
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 0a59555e..6ab86854 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -177,7 +177,7 @@ namespace VC { Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
}
- protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
+ public Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
protected GlobalVariable errorVariable;
public void GenerateVCsForLazyInlining(Program program) {
@@ -1611,7 +1611,7 @@ namespace VC { }
#endregion
- protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)
{
Contract.Requires(impl != null);
Contract.Requires(ch != null);
@@ -2059,7 +2059,7 @@ namespace VC { }
}
}
- protected void ConvertCFG2DAG(Implementation impl, Program program)
+ public void ConvertCFG2DAG(Implementation impl, Program program)
{
Contract.Requires(impl != null);
Contract.Requires(program != null);
@@ -2274,7 +2274,7 @@ namespace VC { #endregion
}
- protected Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)
+ public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
Contract.Requires(program != null);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index f5469ebf..c3134c09 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -149,6 +149,12 @@ namespace VC { AssumeCmd ac = (AssumeCmd)cmd;
if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
+ if(pname != null)
+ {
+ return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ }
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index d29caa5c..94ae7f04 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -1,48 +1,101 @@ -------------------- houd1.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd2.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
Boogie program verifier finished with 1 verified, 1 error
-------------------- houd3.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = False
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd4.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+b4 = True
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd5.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+b3 = False
+b4 = True
+b5 = True
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd6.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = False
+b3 = False
+b4 = False
+b5 = False
+b6 = False
+b7 = False
+b8 = False
Boogie program verifier finished with 3 verified, 0 errors
-------------------- houd7.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd8.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd9.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd10.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd11.bpl --------------------
+Assignment computed by Houdini:
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd12.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+b3 = True
+b4 = True
+b5 = True
+b6 = False
+b7 = False
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index 2a391b2c..d0e53b08 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -6,6 +6,5 @@ set BGEXE=..\..\Binaries\Boogie.exe for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /contractInfer %%f
-rem %BGEXE% %* /nologo /prover:z3api /Houdini:ci %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer %%f
)
diff --git a/Test/inline/Answer b/Test/inline/Answer index 2c29ab0b..d7e7edbe 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -32,7 +32,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); -implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
anon0:
@@ -49,7 +49,7 @@ procedure {:inline 1} inc(x: int, i: int) returns (y: int); -implementation inc(x: int, i: int) returns (y: int)
+implementation {:inline 1} inc(x: int, i: int) returns (y: int)
{
anon0:
@@ -65,7 +65,7 @@ procedure {:inline 1} dec(x: int, i: int) returns (y: int); -implementation dec(x: int, i: int) returns (y: int)
+implementation {:inline 1} dec(x: int, i: int) returns (y: int)
{
anon0:
@@ -160,7 +160,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); ensures z == x + 1 - y;
-implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
var inline$dec$0$x: int;
var inline$dec$0$i: int;
@@ -220,7 +220,7 @@ procedure {:inline 1} increase(i: int) returns (k: int); -implementation increase(i: int) returns (k: int)
+implementation {:inline 1} increase(i: int) returns (k: int)
{
var j: int;
@@ -298,7 +298,7 @@ procedure {:inline 3} recursive(x: int) returns (y: int); -implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
@@ -421,7 +421,7 @@ after inlining procedure calls procedure {:inline 3} recursive(x: int) returns (y: int);
-implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
var inline$recursive$0$k: int;
@@ -560,7 +560,7 @@ procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, fo -implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -606,7 +606,7 @@ procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool); -implementation check(A: [int]int, i: int, c: int) returns (ret: bool)
+implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
{
anon0:
@@ -746,7 +746,7 @@ after inlining procedure calls procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
-implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -866,7 +866,7 @@ procedure {:inline 2} foo(); -implementation foo()
+implementation {:inline 2} foo()
{
anon0:
@@ -882,7 +882,7 @@ procedure {:inline 2} foo1(); -implementation foo1()
+implementation {:inline 2} foo1()
{
anon0:
@@ -898,7 +898,7 @@ procedure {:inline 2} foo2(); -implementation foo2()
+implementation {:inline 2} foo2()
{
anon0:
@@ -914,7 +914,7 @@ procedure {:inline 2} foo3(); -implementation foo3()
+implementation {:inline 2} foo3()
{
anon0:
@@ -947,7 +947,7 @@ procedure {:inline 2} foo(); modifies x;
-implementation foo()
+implementation {:inline 2} foo()
{
var inline$foo$0$x: int;
var inline$foo$1$x: int;
@@ -992,7 +992,7 @@ procedure {:inline 2} foo1(); modifies x;
-implementation foo1()
+implementation {:inline 2} foo1()
{
var inline$foo2$0$x: int;
var inline$foo3$0$x: int;
@@ -1097,7 +1097,7 @@ procedure {:inline 2} foo2(); modifies x;
-implementation foo2()
+implementation {:inline 2} foo2()
{
var inline$foo3$0$x: int;
var inline$foo1$0$x: int;
@@ -1202,7 +1202,7 @@ procedure {:inline 2} foo3(); modifies x;
-implementation foo3()
+implementation {:inline 2} foo3()
{
var inline$foo1$0$x: int;
var inline$foo2$0$x: int;
@@ -1532,7 +1532,7 @@ procedure {:inline 1} foo(); -implementation foo()
+implementation {:inline 1} foo()
{
anon0:
@@ -1605,7 +1605,7 @@ procedure {:inline 1} foo(); modifies g;
-implementation foo()
+implementation {:inline 1} foo()
{
var inline$bar$0$g: int;
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 80aa8d7e..563f39d3 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,15 +1,15 @@ -# Aste started: 2011-11-16 07:00:04
+# Aste started: 2011-11-21 07:00:05
# Host id: Boogiebox
# Configuration: boogie.cfg
# Task: aste.tasks.boogie.FullBuild
-# [2011-11-16 07:03:29] SpecSharp revision: 441525d3599d
-# [2011-11-16 07:03:29] SscBoogie revision: 441525d3599d
-# [2011-11-16 07:05:22] Boogie revision: 2953138bd568
-[2011-11-16 07:06:54] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
+# [2011-11-21 07:03:42] SpecSharp revision: fcf3177ec66b
+# [2011-11-21 07:03:42] SscBoogie revision: fcf3177ec66b
+# [2011-11-21 07:05:30] Boogie revision: 1af8119efee0
+[2011-11-21 07:06:49] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
1>corflags : warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
-[2011-11-16 07:07:49] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+[2011-11-21 07:08:17] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
@@ -20,48 +20,11 @@ D:\Temp\aste\Boogie\Source\Core\Parser.cs(111,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(119,65): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.
- D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.
- D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.
- D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.
- C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(240,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite" "@Coreccrewrite.rsp"" exited with code 3.
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\TPTP\bin\Checked\Provers.TPTP.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Isabelle\bin\Checked\Provers.Isabelle.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Houdini\bin\Checked\Houdini.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found
- error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found
+ D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(247,7): warning CS0162: Unreachable code detected
+ D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(266,7): warning CS0162: Unreachable code detected
+ D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1695,11): warning CS0162: Unreachable code detected
+ D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1855,11): warning CS0162: Unreachable code detected
+ D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(852,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
warning CS0162: Unreachable code detected
@@ -71,14 +34,10 @@ warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.
warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.
warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.
- 1 error
- 1 error
- 2 error
- 3 error
- 3 error
- 4 error
- 4 error
- 5 error
- 6 error
- 9 error
- 11 failed
+ warning CS0162: Unreachable code detected
+ warning CS0162: Unreachable code detected
+ warning CS0162: Unreachable code detected
+ warning CS0162: Unreachable code detected
+ warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
+[2011-11-21 08:04:18] 0 out of 32 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2011-11-21 08:04:59] Released nightly of Boogie
|