From dc8e43c41b46e8d2ae9bc93caa97f7b7d891b5df Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 23 Feb 2012 13:52:02 -0800 Subject: using model instead of labels --- Source/Core/CommandLineOptions.cs | 1 + Source/Provers/SMTLib/ProverInterface.cs | 41 ++++++++++++++++++++++++++-- Source/Provers/SMTLib/SMTLibProverOptions.cs | 5 ++++ Source/VCGeneration/VC.cs | 17 +++++++++++- Source/VCGeneration/Wlp.cs | 2 +- 5 files changed, 62 insertions(+), 4 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index b478f11d..1a08cb54 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -447,6 +447,7 @@ namespace Microsoft.Boogie { public int EnhancedErrorMessages = 0; public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present public bool UseArrayTheory = false; + public bool UseLabels = false; public bool MonomorphicArrays { get { return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 40492ce4..7ffe8323 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -187,7 +187,7 @@ namespace Microsoft.Boogie.SMTLib if (common.Length == 0) { SendCommon("(set-option :print-success false)"); SendCommon("(set-info :smt-lib-version 2.0)"); - if (options.ExpectingModel()) + if (options.ProduceModel()) SendCommon("(set-option :produce-models true)"); foreach (var opt in options.SmtOptions) { SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); @@ -449,9 +449,38 @@ namespace Microsoft.Boogie.SMTLib } } + private string[] CalculatePath() { + SendThisVC("(get-value ((ControlFlow @cfc 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; + else if (resp.ArgCount != 0) + break; + if (v.StartsWith("-")) { + path.Add("@" + v.Substring(1)); + break; + } + else { + path.Add("+" + v); + } + SendThisVC("(get-value ((ControlFlow @cfc " + v + ")))"); + } + return path.ToArray(); + } + private string[] GetLabelsInfo(ErrorHandler handler) { - SendThisVC("(labels)"); + if (CommandLineOptions.Clo.UseLabels) + SendThisVC("(labels)"); if (options.ExpectingModel()) SendThisVC("(get-model)"); Process.Ping(); @@ -499,6 +528,14 @@ namespace Microsoft.Boogie.SMTLib } } + 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) diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index b7b7f24d..6fe025c0 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -41,6 +41,11 @@ namespace Microsoft.Boogie.SMTLib public string Inspector = null; public bool OptimizeForBv = false; + public bool ProduceModel() { + return !CommandLineOptions.Clo.UseLabels || + ExpectingModel(); + } + public bool ExpectingModel() { return CommandLineOptions.Clo.PrintErrorModel >= 1 || diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6026b862..49fa7144 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1536,9 +1536,24 @@ namespace VC { } )); - VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker); + LocalVariable controlFlowVariable = null; + + if (!CommandLineOptions.Clo.UseLabels) { + controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int)); + impl.LocVars.Add(controlFlowVariable); + } + + VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariable, label2absy, checker); Contract.Assert(vc != null); + if (!CommandLineOptions.Clo.UseLabels) { + VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable); + Contract.Assert(controlFlowVariableExpr != null); + VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO)); + Contract.Assert(controlFlowFunctionAppl != null); + vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))), vc); + } + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program); } else { diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index b84df433..6d4d8051 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -134,7 +134,7 @@ namespace VC { Contract.Assert(controlFlowVariableExpr != null); VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId))); Contract.Assert(controlFlowFunctionAppl != null); - VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId))); + VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-ac.UniqueId))); if (ctxt.Label2absy == null) { return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N)); } else { -- cgit v1.2.3