diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 1 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 41 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 17 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 2 |
5 files changed, 62 insertions, 4 deletions
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<string>();
+ 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 {
|