From a64c0df2b7997da015072a31b4b8320f891d63c5 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Tue, 15 Nov 2011 13:08:02 -0800 Subject: VCC: Recognize $result --- Source/ModelViewer/VccProvider.cs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 10e4db10..4354ddc3 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -422,6 +422,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 +691,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_", ""); } } -- cgit v1.2.3 From 51bec918c61f056eb343faccceaa73d885549dde Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Tue, 15 Nov 2011 22:12:29 -0600 Subject: VCC: Better display of data type values --- Source/ModelViewer/VccProvider.cs | 91 +++++++++++++++++++++++++++++++++------ 1 file changed, 78 insertions(+), 13 deletions(-) diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 4354ddc3..27d6422b 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -48,9 +48,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc public List states = new List(); public Dictionary localVariableNames = new Dictionary(); + Dictionary datatypePrefixUse = new Dictionary(); + Dictionary datatypeShortName = new Dictionary(); + Dictionary datatypeLongName = new Dictionary(); + Dictionary fileNameMapping = new Dictionary(); public const string selfMarker = "\\self"; + public const int maxDatatypeNameLength = 5; public VccModel(Model m, ViewOptions opts) : base(m, opts) @@ -1202,7 +1207,63 @@ 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 && ctor.Args.Length == 0) + sb.Append(ctor.Func.Name.Substring(3)); + else + sb.Append(DataTypeShortName(elt, dataTypeType)); + if (level > 0 && ctor != null && ctor.Args.Length > 0) { + 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(")"); + } + } + return len; + } + + private string DataTypeShortName(Model.Element elt, string tp) + { + string res; + if (datatypeShortName.TryGetValue(elt, out res)) return res; + + 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); + } + } + + var useCnt = 0; + if (!datatypePrefixUse.TryGetValue(baseName, out useCnt)) + useCnt = -1; + useCnt++; + datatypePrefixUse[baseName] = useCnt; + res = baseName + "." + useCnt.ToString(); + datatypeShortName[elt] = res; + return res; + } + + private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff) { var vm = this; @@ -1234,18 +1295,18 @@ 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; + 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.None; + return prev; } } @@ -1272,9 +1333,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc suff = NameSeqSuffix.None; return lit; } + if (datatypeLongName.TryGetValue(elt, out lit)) { + suff = NameSeqSuffix.None; + return lit; + } var name = base.CanonicalBaseName(elt, out suff); - name = CanonicalBaseNameCore(name, elt); + name = CanonicalBaseNameCore(name, elt, true, ref suff); return name; } -- cgit v1.2.3 From 30f9cf0eed24a72102449c329b6eb2cfed5122d5 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Tue, 15 Nov 2011 22:24:58 -0600 Subject: VCC: Further data type improvements --- Source/ModelViewer/VccProvider.cs | 38 ++++++++++++++++---------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 27d6422b..6fd068a8 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -48,8 +48,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc public List states = new List(); public Dictionary localVariableNames = new Dictionary(); - Dictionary datatypePrefixUse = new Dictionary(); - Dictionary datatypeShortName = new Dictionary(); Dictionary datatypeLongName = new Dictionary(); Dictionary fileNameMapping = new Dictionary(); @@ -1222,27 +1220,29 @@ namespace Microsoft.Boogie.ModelViewer.Vcc } if (dataTypeType != null) { - if (ctor != null && ctor.Args.Length == 0) + if (ctor != null) sb.Append(ctor.Func.Name.Substring(3)); else sb.Append(DataTypeShortName(elt, dataTypeType)); - if (level > 0 && ctor != null && ctor.Args.Length > 0) { - sb.Append("("); - for (int i = 0; i < ctor.Args.Length; ++i) { - if (i != 0) sb.Append(", "); - len += DataTypeToString(sb, level - 1, ctor.Args[i]); + 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(")"); } - sb.Append(")"); } + } else { + sb.Append(CanonicalName(elt)); } return len; } private string DataTypeShortName(Model.Element elt, string tp) { - string res; - if (datatypeShortName.TryGetValue(elt, out res)) return res; - var baseName = tp; var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt); @@ -1253,14 +1253,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc } } - var useCnt = 0; - if (!datatypePrefixUse.TryGetValue(baseName, out useCnt)) - useCnt = -1; - useCnt++; - datatypePrefixUse[baseName] = useCnt; - res = baseName + "." + useCnt.ToString(); - datatypeShortName[elt] = res; - return res; + return baseName; } private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff) @@ -1297,6 +1290,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc if (dtpName != null) { 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); @@ -1305,7 +1299,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc } datatypeLongName[elt] = prev; - suff = NameSeqSuffix.None; + suff = NameSeqSuffix.WhenNonZero; return prev; } } @@ -1334,7 +1328,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return lit; } if (datatypeLongName.TryGetValue(elt, out lit)) { - suff = NameSeqSuffix.None; + suff = NameSeqSuffix.WhenNonZero; return lit; } -- cgit v1.2.3 From 5a76494853091329f2a50a1113ad77baef28dde5 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Tue, 15 Nov 2011 22:27:20 -0600 Subject: BVD: Fix display bug --- Source/ModelViewer/Main.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } -- cgit v1.2.3 From f93b56972e92b21490e00e886346e2af427fd22b Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 16 Nov 2011 09:36:25 -0800 Subject: simple fix in houdini --- Source/Houdini/Houdini.cs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 7113293b..09017d20 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1011,13 +1011,19 @@ namespace Microsoft.Boogie.Houdini { 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(); this.NotifyIteration(); @@ -1041,13 +1047,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); -- cgit v1.2.3 From 09f250265d20c322fd7c330b73a4a029f98b39b1 Mon Sep 17 00:00:00 2001 From: VccBuildServer Date: Wed, 16 Nov 2011 20:06:36 +0100 Subject: Tagging EMIC CC.NET build 2.1.31116.0 --- .hgtags | 1 + 1 file changed, 1 insertion(+) diff --git a/.hgtags b/.hgtags index 753b727a..f5160309 100644 --- a/.hgtags +++ b/.hgtags @@ -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 -- cgit v1.2.3 From f99b8c0a6af826c2b74f1b4143520e080453e033 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 16 Nov 2011 11:40:16 -0800 Subject: Eliminated unused argument in the constructor for Checker --- Source/Houdini/Checker.cs | 2 +- Source/VCGeneration/Check.cs | 2 +- Source/VCGeneration/ConditionGeneration.cs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 97c22cc9..519a01af 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -50,7 +50,7 @@ namespace Microsoft.Boogie.Houdini { ModelViewInfo mvInfo; Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo); Hashtable/**/ label2absy; - checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime); + checker = new Checker(this, program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime); if (!(checker.TheoremProver is Z3ProcessTheoremProver || checker.TheoremProver is SMTLibProcessTheoremProver)) { throw new Exception("HdnChecker only works with z3"); } diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 7b623bce..8e92c239 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -101,7 +101,7 @@ namespace Microsoft.Boogie { /// /// Constructor. Initialize a checker with the program and log file. /// - 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; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a52a7087..b8645cb0 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; -- cgit v1.2.3 From 8eb81c0042ba8969def9e4d2c69e1448e0aa40ec Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 16 Nov 2011 14:52:24 -0800 Subject: Boogie: fixed build error (incorrect type in Contract.Result) --- Source/Core/CommandLineOptions.cs | 1 - 1 file changed, 1 deletion(-) 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 { /// Consumed ("captured" and possibly modified) by the method. public bool Parse([Captured] string[]/*!*/ args) { Contract.Requires(cce.NonNullElements(args)); - Contract.Ensures(-2 <= Contract.Result() && Contract.Result() <= 2 && Contract.Result() != 0); // save the command line options for the log files Environment += "Command Line Options: " + args.Concat(" "); -- cgit v1.2.3 From fdb39e085355c4d647d9a54f58da18e2b2979462 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Wed, 16 Nov 2011 14:57:19 -0800 Subject: Translate AddressOf expressions correctly. Fixes for problems when translating generic type parameters. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 65 +++++++++--- BCT/BytecodeTranslator/Sink.cs | 11 +- .../TranslationTest/GeneralHeapInput.txt | 116 ++++++++++++--------- .../TranslationTest/SplitFieldsHeapInput.txt | 116 ++++++++++++--------- 4 files changed, 186 insertions(+), 122 deletions(-) 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 /// /// 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. /// 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/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; } -- cgit v1.2.3 From 7c4a89d9adbe8b8779d3691273ee407655754d3f Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 16 Nov 2011 15:33:36 -0800 Subject: refactoring houdini so that it creates only a single instance of z3 --- Source/Houdini/Checker.cs | 40 ++++--------- Source/Houdini/Houdini.cs | 96 +++++++++++++++--------------- Source/VCGeneration/ConditionGeneration.cs | 2 +- Source/VCGeneration/VC.cs | 8 +-- 4 files changed, 65 insertions(+), 81 deletions(-) diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 519a01af..3cb27e14 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -17,54 +17,36 @@ using System.Threading; using VC; namespace Microsoft.Boogie.Houdini { - public class HoudiniVCGen : VCGen { - private Checker checker; + public class HoudiniSession { 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/**/ label2absy; - checker = new Checker(this, program, logFilePath, appendLogFile, 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 errors) { + public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List errors) { collector.examples.Clear(); VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture); checker.BeginCheck(descriptiveName, vc, handler); diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 09017d20..06fd5502 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 observers = new List(); @@ -251,7 +250,9 @@ namespace Microsoft.Boogie.Houdini { public class Houdini : ObservableHoudini { private Program program; private ReadOnlyDictionary houdiniConstants; - private ReadOnlyDictionary vcgenSessions; + private ReadOnlyDictionary houdiniSessions; + private VCGen vcgen; + private Checker checker; private Graph 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 PrepareVCGenSessions() { - Dictionary vcgenSessions = new Dictionary(); + Dictionary houdiniSessions = new Dictionary(); 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(vcgenSessions); + this.houdiniSessions = new ReadOnlyDictionary(houdiniSessions); } private ReadOnlyDictionary CollectExistentialConstants() { @@ -362,9 +362,10 @@ namespace Microsoft.Boogie.Houdini { return false; } - private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary currentAssignment) { - Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator; - VCExpressionGenerator exprGen = vcgen.VCExprGenerator; + private VCExpr BuildAxiom(Dictionary currentAssignment) { + DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context; + Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator; + VCExpressionGenerator exprGen = checker.VCExprGen; VCExpr expr = VCExpressionGenerator.True; foreach (KeyValuePair kv in currentAssignment) { @@ -389,46 +390,44 @@ namespace Microsoft.Boogie.Houdini { return initial; } - private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List errors) { - HoudiniVCGen vcgen; - vcgenSessions.TryGetValue(implementation, out vcgen); + private ProverInterface.Outcome VerifyUsingAxiom(HoudiniSession session, Implementation implementation, VCExpr axiom, out List 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 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 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 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(); 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 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); @@ -731,8 +728,10 @@ namespace Microsoft.Boogie.Houdini { current.Implementation = current.WorkList.Peek(); this.NotifyImplementation(current.Implementation); + HoudiniSession session; + houdiniSessions.TryGetValue(current.Implementation, out session); List 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) { @@ -771,7 +770,9 @@ namespace Microsoft.Boogie.Houdini { this.NotifyImplementation(current.Implementation); List 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 errors) { + private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, VCExpr axiom, out List 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 errors, out bool exceptional) { Contract.Assert(current.Implementation != null); @@ -962,11 +964,10 @@ namespace Microsoft.Boogie.Houdini { 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,9 +1005,10 @@ 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 errors, out bool exceptional) { Contract.Assert(current.Implementation != null); @@ -1029,11 +1031,11 @@ namespace Microsoft.Boogie.Houdini { 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); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index b8645cb0..cb28cd7d 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -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/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 implName2LazyInliningInfo; + public Dictionary 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/**//*!*/ label2absy, Checker/*!*/ ch) + public VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/**//*!*/ 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); -- cgit v1.2.3 From e611277c4d889de2db5d27c54eb64e149c3f194d Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 16 Nov 2011 15:40:46 -0800 Subject: /contractInfer always prints the computed assignment now enabled the houdini regressions --- Source/BoogieDriver/BoogieDriver.cs | 8 +++--- Test/houdini/Answer | 53 +++++++++++++++++++++++++++++++++++++ Test/houdini/runtest.bat | 3 +-- 3 files changed, 57 insertions(+), 7 deletions(-) diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 028ff1dd..7b5576c1 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -440,11 +440,9 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) { Houdini.Houdini houdini = new Houdini.Houdini(program, true); Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Assignment computed by Houdini:"); - foreach (var x in outcome.assignment) { - Console.WriteLine(x.Key + " = " + x.Value); - } + Console.WriteLine("Assignment computed by Houdini:"); + foreach (var x in outcome.assignment) { + Console.WriteLine(x.Key + " = " + x.Value); } errorCount = outcome.ErrorCount; verified = outcome.Verified; 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 ) -- cgit v1.2.3 From 9cd8e65ea89d1eba89856903335fbf96775ca8f2 Mon Sep 17 00:00:00 2001 From: CodeplexBot Date: Thu, 17 Nov 2011 07:07:49 +0100 Subject: Boogie build failed --- _admin/Boogie/aste/summary.log | 85 ++++++++++++++---------------------------- 1 file changed, 27 insertions(+), 58 deletions(-) diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 80aa8d7e..80cb723d 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-17 07:00:04 # 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-17 07:03:22] SpecSharp revision: 441525d3599d +# [2011-11-17 07:03:22] SscBoogie revision: 441525d3599d +# [2011-11-17 07:05:04] Boogie revision: d837d1c8382c +[2011-11-17 07:06:14] 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-17 07:07:38] 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,12 @@ 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\Check.cs(161,16): warning CS0219: The variable 'expand' is assigned but its value is never used + D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(850,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 +35,19 @@ 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. + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0162: Unreachable code detected + warning CS0219: The variable 'expand' is assigned but its value is never used + warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires. +[2011-11-17 07:07:49] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Dafny.sln /Rebuild Checked + + D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5071,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)' + D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5072,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)' + D:\Temp\aste\Boogie\Source\Dafny\DafnyOptions.cs(36,7): warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', thus cannot add Requires. + 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" "@DafnyPipelineccrewrite.rsp"" exited with code 2. + error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Dafny\bin\Checked\DafnyPipeline.dll' could not be found + warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', 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 + 2 failed -- cgit v1.2.3 From 44fadfb3db027ce727ecf1d209c3a4a10036d521 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 16 Nov 2011 22:15:41 -0800 Subject: Dafny: fixed bad Code Contracts --- Source/Dafny/DafnyOptions.cs | 2 -- Source/Dafny/Translator.cs | 4 ++-- Source/VCGeneration/Check.cs | 1 - 3 files changed, 2 insertions(+), 5 deletions(-) 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/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 8e92c239..2f7267b1 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -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); -- cgit v1.2.3 From 0eb9ff4e155aa102d67b7dd3250831962d922886 Mon Sep 17 00:00:00 2001 From: CodeplexBot Date: Thu, 17 Nov 2011 11:30:16 +0100 Subject: Boogie build succeeded --- _admin/Boogie/aste/summary.log | 26 ++++++++------------------ 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 80cb723d..7f54bff2 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,15 +1,15 @@ -# Aste started: 2011-11-17 07:00:04 +# Aste started: 2011-11-17 10:26:12 # Host id: Boogiebox # Configuration: boogie.cfg # Task: aste.tasks.boogie.FullBuild -# [2011-11-17 07:03:22] SpecSharp revision: 441525d3599d -# [2011-11-17 07:03:22] SscBoogie revision: 441525d3599d -# [2011-11-17 07:05:04] Boogie revision: d837d1c8382c -[2011-11-17 07:06:14] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build +# [2011-11-17 10:29:20] SpecSharp revision: 441525d3599d +# [2011-11-17 10:29:20] SscBoogie revision: 441525d3599d +# [2011-11-17 10:30:59] Boogie revision: 31e905f5fadb +[2011-11-17 10:32:00] 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-17 07:07:38] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked +[2011-11-17 10:33:24] 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() @@ -24,7 +24,6 @@ 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\Check.cs(161,16): warning CS0219: The variable 'expand' is assigned but its value is never used D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(850,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() @@ -39,15 +38,6 @@ warning CS0162: Unreachable code detected warning CS0162: Unreachable code detected warning CS0162: Unreachable code detected - warning CS0219: The variable 'expand' is assigned but its value is never used warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires. -[2011-11-17 07:07:49] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Dafny.sln /Rebuild Checked - - D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5071,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)' - D:\Temp\aste\Boogie\Source\Dafny\Translator.cs(5072,9): error CC1022: Bad use of method 'Contract.Invariant' in method body 'Microsoft.Dafny.Translator+ExpressionTranslator.#ctor(Microsoft.Dafny.Translator,Microsoft.Dafny.Translator+PredefinedDecls,Microsoft.Boogie.Expr,System.String,Microsoft.Dafny.Function,System.Int32,System.String)' - D:\Temp\aste\Boogie\Source\Dafny\DafnyOptions.cs(36,7): warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', thus cannot add Requires. - 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" "@DafnyPipelineccrewrite.rsp"" exited with code 2. - error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Dafny\bin\Checked\DafnyPipeline.dll' could not be found - warning CC1032: Method 'Microsoft.Dafny.DafnyOptions.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)' overrides 'Microsoft.Boogie.CommandLineOptionEngine.ParseOption(System.String,Microsoft.Boogie.CommandLineOptionEngine+CommandLineParseState)', thus cannot add Requires. - 1 error - 2 failed +[2011-11-17 11:29:34] 0 out of 32 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed +# [2011-11-17 11:30:16] Released nightly of Boogie -- cgit v1.2.3 From 915225c14ba71e94ed0f43fef8aaeb4dfbf49e71 Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 17 Nov 2011 14:14:43 -0800 Subject: changed the semantics of requires and ensures for inlined procedures --- Source/Core/AbsyQuant.cs | 8 +++++++- Source/Core/BoogiePL.atg | 2 +- Source/Core/Inline.cs | 39 +++++++++++++++++++++++++++++++++------ Source/Core/Parser.cs | 2 +- Test/inline/Answer | 40 ++++++++++++++++++++-------------------- 5 files changed, 62 insertions(+), 29 deletions(-) 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 newParams = new List(); + 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..645cdee5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -587,7 +587,7 @@ Procedure (. // 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/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/*!*/ 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/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; -- cgit v1.2.3 From 924a89f9022f0d4fa7201376eff55c0294cd4a72 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 18 Nov 2011 14:56:07 -0800 Subject: commented calls to GC.Collect() --- BCT/BytecodeTranslator/Program.cs | 2 +- Source/BoogieDriver/BoogieDriver.cs | 3 +++ Source/Core/BoogiePL.atg | 1 - Source/Houdini/Checker.cs | 6 +++++- Source/Houdini/Houdini.cs | 10 +++++----- 5 files changed, 14 insertions(+), 8 deletions(-) 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/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 7b5576c1..4073c722 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -444,6 +444,9 @@ namespace Microsoft.Boogie { foreach (var x in outcome.assignment) { Console.WriteLine(x.Key + " = " + x.Value); } + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime); + } errorCount = outcome.ErrorCount; verified = outcome.Verified; inconclusives = outcome.Inconclusives; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 645cdee5..c7950c9a 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -585,7 +585,6 @@ Procedure | { Spec } ImplBody (. - // 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, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); .) diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 3cb27e14..b0c8fabf 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -18,6 +18,7 @@ using VC; namespace Microsoft.Boogie.Houdini { public class HoudiniSession { + public static double proverTime = 0; private string descriptiveName; private VCExpr conjecture; private ProverInterface.ErrorHandler handler; @@ -49,10 +50,13 @@ namespace Microsoft.Boogie.Houdini { public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List 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 06fd5502..27b8d05f 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -686,7 +686,7 @@ namespace Microsoft.Boogie.Houdini { this.NotifyStart(program, houdiniConstants.Keys.Count); while (current.WorkList.Count > 0) { - System.GC.Collect(); + //System.GC.Collect(); this.NotifyIteration(); VCExpr axiom = BuildAxiom(current.Assignment); @@ -722,7 +722,7 @@ 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(); @@ -763,7 +763,7 @@ 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(); @@ -960,7 +960,7 @@ namespace Microsoft.Boogie.Houdini { do { if (pastFirstIter) { - System.GC.Collect(); + //System.GC.Collect(); this.NotifyIteration(); } @@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.Houdini { outcome = ProverInterface.Outcome.Undetermined; if (pastFirstIter) { - System.GC.Collect(); + //System.GC.Collect(); this.NotifyIteration(); } -- cgit v1.2.3 From 50ebdd01228234e2311b61e59972519af3d512dc Mon Sep 17 00:00:00 2001 From: akashlal Date: Sun, 20 Nov 2011 22:44:42 +0530 Subject: Added lazy summary computation to stratified inlining (not finished yet) --- Source/Core/AbsyCmd.cs | 5 + Source/VCGeneration/StratifiedVC.cs | 317 +++++++++++++++++++++++++++++++++--- Source/VCGeneration/Wlp.cs | 6 + 3 files changed, 302 insertions(+), 26 deletions(-) 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(), assume.Attributes); + assume.Attributes.Params.Add(this.callee); + } #endregion newBlockBody.Add(assume); } 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 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(); + // 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(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 block) { Outcome ret; List 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(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 getPostOrder(Dictionary parents, int root) + { + var children = new Dictionary>(); + foreach (var id in parents.Keys) children.Add(id, new HashSet()); + children.Add(0, new HashSet()); + foreach (var kvp in parents) children[kvp.Value].Add(kvp.Key); + return getPostOrder(children, root); + } + static List getPostOrder(Dictionary> children, int root) + { + var ret = new List(); + 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 FindNodes(Dictionary parents, HashSet allLeaves, + HashSet goodLeaves) + { + var ret = new HashSet(); + var leaves = new Dictionary>(); + leaves.Add(0, new HashSet()); + parents.Keys.Iter(n => leaves.Add(n, new HashSet())); + 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/*!*/ recordExpr2Var; public Dictionary/*!*/ id2Candidate; public Dictionary/*!*/ id2ControlVar; + public Dictionary id2VC; public Dictionary/*!*/ label2Id; // Stores the candidate from which this one originated public Dictionary candidateParent; @@ -2340,6 +2499,14 @@ namespace VC // first argument (used for obtaining concrete values in error trace) public Dictionary argExprMap; + // map from candidate to summary candidates + public Dictionary>> summaryCandidates; + private Dictionary>> summaryTemp; + // set of all boolean guards of summaries + public HashSet allSummaryConst; + // The summary: boolean guards that are true + public HashSet trueSummaryConst; + public HashSet forcedCandidates; //////////////////////////// @@ -2420,6 +2587,11 @@ namespace VC forcedCandidates = new HashSet(); id2Vars = new Dictionary>(); + summaryCandidates = new Dictionary>>(); + summaryTemp = new Dictionary>>(); + allSummaryConst = new HashSet(); + trueSummaryConst = new HashSet(); + id2VC = new Dictionary(); } 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>()); + + 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>>>(); + foreach (var id in recentlyAddedCandidates) + { + var collect = new CollectVCVars(); + var proc = getProc(id); + if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List>>()); + 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>()); + 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, bool> + { + public override HashSet Visit(VCExprVar node, bool arg) + { + var ret = new HashSet(); + ret.Add(node); + return ret; + } + + protected override HashSet CombineResults(List> results, bool arg) + { + var ret = new HashSet(); + results.ForEach(s => ret.UnionWith(s)); + return ret; + } + } public class FCallInliner : MutatingVCExprVisitor { 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) { -- cgit v1.2.3 From eb67a2565b9d81e5272b4be57d4ed817b3fa9efd Mon Sep 17 00:00:00 2001 From: CodeplexBot Date: Mon, 21 Nov 2011 08:05:00 +0100 Subject: Boogie build succeeded --- _admin/Boogie/aste/summary.log | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 7f54bff2..563f39d3 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,15 +1,15 @@ -# Aste started: 2011-11-17 10:26:12 +# Aste started: 2011-11-21 07:00:05 # Host id: Boogiebox # Configuration: boogie.cfg # Task: aste.tasks.boogie.FullBuild -# [2011-11-17 10:29:20] SpecSharp revision: 441525d3599d -# [2011-11-17 10:29:20] SscBoogie revision: 441525d3599d -# [2011-11-17 10:30:59] Boogie revision: 31e905f5fadb -[2011-11-17 10:32:00] 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-17 10:33:24] 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() @@ -24,7 +24,7 @@ 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(850,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires. + 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 @@ -39,5 +39,5 @@ 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-17 11:29:34] 0 out of 32 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed -# [2011-11-17 11:30:16] Released nightly of Boogie +[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 -- cgit v1.2.3