From aa4cc8d3121400e060bcbdc3ee1117c43273335e Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 27 Feb 2012 12:06:49 -0800 Subject: various fixes related to new error traces --- Source/Provers/SMTLib/ProverInterface.cs | 252 ++++++++++++++++++++----------- 1 file changed, 166 insertions(+), 86 deletions(-) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 4c0597f9..342a2b1b 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -380,9 +380,72 @@ namespace Microsoft.Boogie.SMTLib } } + public override ProverInterface.Outcome CheckOutcome(ProverInterface.ErrorHandler handler, IEnumerable controlFlowConstants) { + var result = Outcome.Undetermined; + if (Process == null) + return result; + + Contract.Assume(controlFlowConstants == null); + try { + currentErrorHandler = handler; + FlushProverWarnings(); + + var errorsLeft = CommandLineOptions.Clo.ProverCCLimit; + if (errorsLeft < 1) + errorsLeft = 1; + + var globalResult = Outcome.Undetermined; + + while (true) { + errorsLeft--; + Dictionary paths = null; + + result = GetResponse(); + if (globalResult == Outcome.Undetermined) + globalResult = result; + + if (result == Outcome.Invalid) { + paths = CalculatePath(controlFlowConstants); + ErrorModel errorModel = GetErrorModel(); + Dictionary> paths1 = new Dictionary>(); + foreach (int x in paths.Keys) { + paths1[x] = paths[x].ToList(); + } + handler.OnModel(paths1, errorModel); + } + + if (paths == null || errorsLeft == 0) break; + + string[] path = paths[0]; + string source = path[path.Length - 2]; + string target = path[path.Length - 1]; + SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + ")))"); + SendThisVC("(check-sat)"); + } + + if (CommandLineOptions.Clo.StratifiedInlining == 0) { + SendThisVC("(pop 1)"); + } + else if (CommandLineOptions.Clo.StratifiedInlining > 0 && pendingPop) { + pendingPop = false; + SendThisVC("(pop 1)"); + } + + FlushLogFile(); + + if (CommandLineOptions.Clo.RestartProverPerVC && Process != null) + Process.NeedsRestart = true; + + return globalResult; + } + finally { + currentErrorHandler = null; + } + } + [NoDefaultContract] public override Outcome CheckOutcome(ErrorHandler handler) - { //Contract.Requires(handler != null); + { Contract.EnsuresOnThrow(true); var result = Outcome.Undetermined; @@ -400,30 +463,47 @@ namespace Microsoft.Boogie.SMTLib var globalResult = Outcome.Undetermined; - while (errorsLeft-- > 0) { + while (true) { + errorsLeft--; string[] labels = null; result = GetResponse(); if (globalResult == Outcome.Undetermined) globalResult = result; - if (result == Outcome.Invalid && options.UseZ3) { - labels = GetLabelsInfo(handler); + if (result == Outcome.Invalid) { + IList xlabels; + if (CommandLineOptions.Clo.UseLabels) { + labels = GetLabelsInfo(); + xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); + } + else { + labels = CalculatePath(); + xlabels = labels; + } + ErrorModel errorModel = GetErrorModel(); + handler.OnModel(xlabels, errorModel); } - if (labels == null) break; + if (labels == null || errorsLeft == 0) break; - var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); - var posLabels = labels.Where(l => !l.StartsWith("@")); - Func lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s)); - if (!options.MultiTraces) - posLabels = Enumerable.Empty(); - var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray(); - var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); - if (errorsLeft > 0) { + if (CommandLineOptions.Clo.UseLabels) { + var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); + var posLabels = labels.Where(l => !l.StartsWith("@")); + Func lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s)); + if (!options.MultiTraces) + posLabels = Enumerable.Empty(); + var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray(); + var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); SendThisVC("(assert " + expr + ")"); SendThisVC("(check-sat)"); } + else { + string source = labels[labels.Length - 2]; + string target = labels[labels.Length - 1]; + SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") " + target + ")))"); + SendThisVC("(check-sat)"); + } } if (CommandLineOptions.Clo.StratifiedInlining == 0) @@ -449,99 +529,99 @@ namespace Microsoft.Boogie.SMTLib } private string[] CalculatePath() { - SendThisVC("(get-value ((ControlFlow 0 0)))"); - var path = new List(); + Dictionary dict = CalculatePath(new int[] { 0 }); + return dict[0]; + } + + private Dictionary CalculatePath(IEnumerable controlFlowConstants) { + Dictionary ret = new Dictionary(); + foreach (var controlFlowConstant in controlFlowConstants) { + SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))"); + var path = new List(); + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null) break; + if (!(resp.Name == "" && resp.ArgCount == 1)) break; + resp = resp.Arguments[0]; + if (!(resp.Name == "" && resp.ArgCount == 2)) break; + resp = resp.Arguments[1]; + var v = resp.Name; + if (v == "-" && resp.ArgCount == 1) { + v = resp.Arguments[0].Name; + path.Add(v); + break; + } + else if (resp.ArgCount != 0) + break; + path.Add(v); + SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))"); + } + ret[controlFlowConstant] = path.ToArray(); + } + return ret; + } + + private ErrorModel GetErrorModel() { + if (!options.ExpectingModel()) + return null; + SendThisVC("(get-model)"); + Process.Ping(); + Model theModel = null; while (true) { var resp = Process.GetProverResponse(); - if (resp == null) - break; - if (!(resp.Name == "" && resp.ArgCount == 1)) break; - resp = resp.Arguments[0]; - if (!(resp.Name == "" && resp.ArgCount == 2)) break; - resp = resp.Arguments[1]; - var v = resp.Name; - if (v == "-" && resp.ArgCount == 1) - v += resp.Arguments[0].Name; - else if (resp.ArgCount != 0) - break; - if (v.StartsWith("-")) { - path.Add("@" + v.Substring(1)); + if (resp == null || Process.IsPong(resp)) break; + if (theModel != null) + HandleProverError("Expecting only one model but got many"); + + string modelStr = null; + if (resp.Name == "model" && resp.ArgCount >= 1) { + modelStr = resp[0].Name; + } + else if (resp.ArgCount == 0 && resp.Name.Contains("->")) { + modelStr = resp.Name; } else { - path.Add("+" + v); + HandleProverError("Unexpected prover response getting model: " + resp.ToString()); + } + List models = null; + try { + models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr)); + } + catch (ArgumentException exn) { + HandleProverError("Model parsing error: " + exn.Message); } - SendThisVC("(get-value ((ControlFlow 0 " + v + ")))"); + if (models == null) + HandleProverError("Could not parse any models"); + else if (models.Count == 0) + HandleProverError("Could not parse any models"); + else if (models.Count > 1) + HandleProverError("Expecting only one model but got many"); + else + theModel = models[0]; } - return path.ToArray(); + return new ErrorModel(theModel); } - private string[] GetLabelsInfo(ErrorHandler handler) + private string[] GetLabelsInfo() { - if (CommandLineOptions.Clo.UseLabels) - SendThisVC("(labels)"); - if (options.ExpectingModel()) - SendThisVC("(get-model)"); + SendThisVC("(labels)"); Process.Ping(); - List labelNums = null; - Model theModel = null; string[] res = null; - while (true) { var resp = Process.GetProverResponse(); if (resp == null || Process.IsPong(resp)) break; + if (res != null) + HandleProverError("Expecting only one sequence of labels but got many"); if (resp.Name == "labels" && resp.ArgCount >= 1) { - var labels = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray(); - res = labels; - if (labelNums != null) HandleProverError("Got multiple :labels responses"); - labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); - } else { - string modelStr = null; - if (resp.Name == "model" && resp.ArgCount >= 1) { - modelStr = resp[0].Name; - } else if (resp.ArgCount == 0 && resp.Name.Contains("->")) { - modelStr = resp.Name; - } - - if (modelStr != null) { - List models = null; - try { - models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr)); - } catch (ArgumentException exn) { - HandleProverError("Model parsing error: " + exn.Message); - } - - if (models != null) { - if (models.Count == 0) HandleProverError("Could not parse any models"); - else { - if (models.Count > 1) HandleProverError("Expecting only one model, got multiple"); - if (theModel != null) HandleProverError("Got multiple :model responses"); - theModel = models[0]; - } - } - } else { - HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString()); - } + res = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray(); + } + else { + HandleProverError("Unexpected prover response getting labels: " + resp.ToString()); } } - - if (!CommandLineOptions.Clo.UseLabels) { - res = CalculatePath(); - if (res.Length == 0) - res = null; - else - labelNums = res.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); - } - - if (labelNums != null) { - ErrorModel m = null; - if (theModel != null) - m = new ErrorModel(theModel); - handler.OnModel(labelNums, m); - } - return res; } -- cgit v1.2.3