From 1996182214a0f2516045c41b845867f4ac410977 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 29 May 2013 18:40:04 -0700 Subject: Adding background model to fixedpoint counterexamples and small code contracts fixes --- Source/Provers/SMTLib/ProverInterface.cs | 21 +++++++++++++++++++++ Source/VCGeneration/ConditionGeneration.cs | 4 +++- Source/VCGeneration/FixedpointVC.cs | 14 ++++++++------ Source/VCGeneration/RPFP.cs | 13 ++++++++++++- 4 files changed, 44 insertions(+), 8 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index be98eb5b..d91ca010 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -510,6 +510,19 @@ namespace Microsoft.Boogie.SMTLib return topnode; } + private Model SExprToModel(SExpr resp, ErrorHandler handler) + { + // Concatenate all the arguments + string modelString = resp[0].Name; + // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")" + var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString)); + if (models == null || models.Count == 0) + { + HandleProverError("no model from prover: " + resp.ToString()); + } + return models[0]; + } + private string QuantifiedVCExpr2String(VCExpr x) { return VCExpr2String(x, 1); @@ -632,6 +645,14 @@ namespace Microsoft.Boogie.SMTLib { cex = SExprToCex(resp, handler,varSubst); } + else + HandleProverError("Unexpected prover response: " + resp.ToString()); + resp = Process.GetProverResponse(); + if (resp.Name == "model") + { + var model = SExprToModel(resp, handler); + cex.owner.SetBackgroundModel(model); + } else HandleProverError("Unexpected prover response: " + resp.ToString()); break; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 092d12d2..cabc9d9e 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -188,12 +188,14 @@ namespace Microsoft.Boogie { public static bool firstModelFile = true; + public bool ModelHasStatesAlready = false; + public void PrintModel() { var filename = CommandLineOptions.Clo.ModelViewFile; if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return; - var m = this.GetModelWithStates(); + var m = ModelHasStatesAlready ? Model : this.GetModelWithStates(); if (filename == "-") { m.Write(Console.Out); diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index bc6a7ce0..e96499fe 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -52,7 +52,7 @@ namespace Microsoft.Boogie Context ctx; RPFP rpfp; - Program program; + // Program program; Microsoft.Boogie.ProverContext boogieContext; Microsoft.Boogie.VCExpressionGenerator gen; public readonly static string recordProcName = "boogie_si_record"; // TODO: this really needed? @@ -515,7 +515,7 @@ namespace Microsoft.Boogie public List interfaceExprVars; - public List privateVars; + // public List privateVars; public VCExpr funcExpr; public VCExpr falseExpr; public RPFP.Transformer F; @@ -1004,7 +1004,7 @@ namespace Microsoft.Boogie Contract.Assert(gen != null); VCExpr vcexpr; if(NoLabels){ - int assertionCount = 0; + // int assertionCount = 0; VCExpr startCorrect = null; /* VC.VCGen.LetVC(cce.NonNull(impl.Blocks[0]), null, null, info.blockVariables, info.bindings, info.ctxt, out assertionCount); */ vcexpr = gen.Let(info.bindings, startCorrect); @@ -1017,7 +1017,7 @@ namespace Microsoft.Boogie info.mvInfo = mvInfo; List interfaceExprs = new List(); - if (true || !info.isMain) + if (true /* was: !info.isMain */) { Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator; Contract.Assert(translator != null); @@ -1129,7 +1129,7 @@ namespace Microsoft.Boogie public class CyclicLiveVariableAnalysis : Microsoft.Boogie.LiveVariableAnalysis { - public static void ComputeLiveVariables(Implementation impl) + public new static void ComputeLiveVariables(Implementation impl) { bool some_change = true; @@ -1538,6 +1538,7 @@ namespace Microsoft.Boogie } } + public Counterexample CreateBoogieCounterExample(RPFP rpfp, RPFP.Node root, Implementation mainImpl) { FindLabels(); @@ -1546,10 +1547,11 @@ namespace Microsoft.Boogie GenerateTrace(rpfp, root, orderedStateIds, mainImpl,true); if (CommandLineOptions.Clo.ModelViewFile != null) { - Model m = new Model(); + Model m = root.owner.GetBackgroundModel(); GetModelWithStates(m, root, implName2StratifiedInliningInfo[mainImpl.Name], orderedStateIds, varSubst); newCounterexample.Model = m; + newCounterexample.ModelHasStatesAlready = true; } return newCounterexample; } diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs index 9048f0f5..f6a42a43 100644 --- a/Source/VCGeneration/RPFP.cs +++ b/Source/VCGeneration/RPFP.cs @@ -566,10 +566,21 @@ namespace Microsoft.Boogie public List nodes = new List(); }; + /** Set the model of the background theory used in a counterexample. */ + public void SetBackgroundModel(Model m) + { + dualModel = m; + } + + /** Set the model of the background theory used in a counterexample. */ + public Model GetBackgroundModel() + { + return dualModel; + } private int nodeCount = 0; private int edgeCount = 0; - // private Model dualModel; + private Model dualModel; // private LabeledLiterals dualLabels; private Stack stack; public List nodes = new List(); -- cgit v1.2.3