From 45fb2f73118bf4010ad08757122d829c76e676d3 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Tue, 12 Oct 2010 01:18:45 +0000 Subject: Make the -mv option use the new Model class. --- .gitignore | 6 +----- Source/BoogieDriver/BoogieDriver.cs | 2 +- Source/Core/CommandLineOptions.cs | 7 ++++--- Source/Provers/Z3/Prover.cs | 2 +- Source/VCGeneration/Check.cs | 7 +++++-- Source/VCGeneration/ConditionGeneration.cs | 31 +++++++++++++++++++++++++++--- Source/VCGeneration/Model.cs | 10 +++++----- Source/VCGeneration/VC.cs | 1 + 8 files changed, 46 insertions(+), 20 deletions(-) diff --git a/.gitignore b/.gitignore index c6ee95ca..3ac7f5b0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,4 @@ -Source/AIFramework/bin/ -Source/AIFramework/obj/ -Source/AbsInt/bin/ -Source/AbsInt/obj/ -Source/Basetypes/bin/ +Source/t Source/_ReSharper.Boogie Source/Provers/*/*.user Source/*/*.user diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 33b9146c..0fc67e15 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -642,7 +642,7 @@ namespace Microsoft.Boogie { Console.WriteLine("Execution trace:"); error.Print(4); } - if (CommandLineOptions.Clo.ModelView == 1) { + if (CommandLineOptions.Clo.ModelViewFile != null) { error.PrintModel(); } errorCount++; diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 4196670f..b63b82cc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -192,7 +192,6 @@ namespace Microsoft.Boogie { Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3); Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7); Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4); - Contract.Invariant(0 <= ModelView && ModelView < 2); Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2); Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9); Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1); @@ -230,7 +229,7 @@ namespace Microsoft.Boogie { public int PrintErrorModel = 0; public string PrintErrorModelFile = null; public bool CEVPrint = false; - public int ModelView = 1; + public string/*?*/ ModelViewFile = null; public int EnhancedErrorMessages = 0; public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present public enum BvHandling { @@ -922,7 +921,9 @@ namespace Microsoft.Boogie { case "-mv": case "/mv": - ps.GetNumericArgument(ref ModelView, 2); + if (ps.ConfirmArgumentCount(1)) { + ModelViewFile = args[ps.i]; + } break; case "-printModelToFile": diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 33e622ba..f218d3b6 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -70,7 +70,7 @@ namespace Microsoft.Boogie.Z3 { return CommandLineOptions.Clo.PrintErrorModel >= 1 || CommandLineOptions.Clo.EnhancedErrorMessages == 1 || - CommandLineOptions.Clo.ModelView > 0 || + CommandLineOptions.Clo.ModelViewFile != null || CommandLineOptions.Clo.ContractInfer || CommandLineOptions.Clo.LazyInlining > 0 || CommandLineOptions.Clo.StratifiedInlining > 0; diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index c128bec8..ef2501de 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -374,9 +374,12 @@ namespace Microsoft.Boogie { } foreach (var t in definedFunctions) { - var f = m.MkFunc(t.Key, t.Value.Count - 1); + var tuples = t.Value; + if (tuples.Count == 0) continue; + + var f = m.MkFunc(t.Key, tuples[0].Count - 1); var args = new Model.Element[f.Arity]; - foreach (var l in t.Value) { + foreach (var l in tuples) { if (l.Count == 1) continue; for (int i = 0; i < f.Arity; ++i) args[i] = elts[l[i]]; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 55cfa650..eda5cfda 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -177,7 +177,26 @@ namespace Microsoft.Boogie { } } - public void PrintModel() { + static bool firstModelFile = true; + + public void PrintModel() + { + var filename = CommandLineOptions.Clo.ModelViewFile; + if (Model == null || filename == null) return; + + var m = this.GetModelWithStates(); + + if (filename == "-") { + m.Write(Console.Out); + Console.Out.Flush(); + } else { + using (var wr = new StreamWriter(filename, !firstModelFile)) { + firstModelFile = false; + m.Write(wr); + } + } + + /* if (Model == null || MvInfo == null) { return; } @@ -267,6 +286,7 @@ namespace Microsoft.Boogie { Console.WriteLine(" undefined captured-state ID {0}", s); } } + */ } public Model GetModelWithStates() @@ -307,7 +327,12 @@ namespace Microsoft.Boogie { if (e is IdentifierExpr) { IdentifierExpr ide = (IdentifierExpr)e; - elt = m.GetFunc(ide.Decl.Name).GetConstant(); + + var f = m.TryGetFunc(ide.Decl.Name); + if (f == null) { + f = m.MkFunc(ide.Decl.Name, 0); + } + elt = f.GetConstant(); } else if (e is LiteralExpr) { LiteralExpr lit = (LiteralExpr)e; elt = m.MkElement(lit.Val.ToString()); @@ -1397,7 +1422,7 @@ namespace VC { Contract.Assert(pc != null); Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); - if (0 < CommandLineOptions.Clo.ModelView && pc is AssumeCmd) { + if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) { string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); if (description != null) { Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Literal(mvInfo.CapturePoints.Count))); diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs index 331d287a..d2d9cc24 100644 --- a/Source/VCGeneration/Model.cs +++ b/Source/VCGeneration/Model.cs @@ -21,7 +21,7 @@ namespace Microsoft.Boogie abstract public class Element { - protected readonly Model parent; + public readonly Model Model; internal List references = new List(); public readonly int Id; @@ -48,7 +48,7 @@ namespace Microsoft.Boogie } } - protected Element(Model p) { parent = p; } + protected Element(Model p) { Model = p; } public abstract ElementKind Kind { get; } public virtual int AsInt() { throw new NotImplementedException(); } } @@ -94,13 +94,13 @@ namespace Microsoft.Boogie public class Func { - private readonly Model Parent; + public readonly Model Model; public readonly string Name; public readonly int Arity; internal readonly List apps = new List(); public IEnumerable Apps { get { return apps; } } - internal Func(Model p, string n, int a) { Parent = p; Name = n; Arity = a; } + internal Func(Model p, string n, int a) { Model = p; Name = n; Arity = a; } public void SetConstant(Element res) { @@ -116,7 +116,7 @@ namespace Microsoft.Boogie if (Arity != 0) throw new ArgumentException(); if (apps.Count == 0) - SetConstant(Parent.MkElement("**" + Name)); + SetConstant(Model.MkElement("**" + Name)); return apps[0].Result; } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 304130ef..9e8b2dc8 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -3021,6 +3021,7 @@ namespace VC { errModel.Print(ErrorReporter.ModelWriter); ErrorReporter.ModelWriter.Flush(); } + Hashtable traceNodes = new Hashtable(); foreach (string s in labels) { Contract.Assert(s != null); -- cgit v1.2.3