summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs5
-rw-r--r--Source/Core/CommandLineOptions.cs5
-rw-r--r--Source/Houdini/Checker.cs20
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs16
-rw-r--r--Source/VCGeneration/StratifiedVC.cs4
-rw-r--r--Source/VCGeneration/Wlp.cs4
6 files changed, 47 insertions, 7 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index d5a98913..c2c09ded 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -443,6 +443,11 @@ namespace Microsoft.Boogie {
Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+ CommandLineOptions.Clo.UseLabels =
+ CommandLineOptions.Clo.UseLabels ||
+ CommandLineOptions.Clo.SoundnessSmokeTest ||
+ !(CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Dag ||
+ CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.DagIterative);
// ---------- Infer invariants --------------------------------------------------------
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 1a08cb54..e75fe867 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -447,7 +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 UseLabels = true;
public bool MonomorphicArrays {
get {
return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;
@@ -1224,7 +1224,8 @@ namespace Microsoft.Boogie {
ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
- ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)
+ ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
+ ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 40d54a49..3670c441 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -24,6 +24,8 @@ namespace Microsoft.Boogie.Houdini {
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
ConditionGeneration.CounterexampleCollector collector;
+ LocalVariable controlFlowVariable;
+ int entryBlockId;
public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl) {
descriptiveName = impl.Name;
@@ -37,8 +39,14 @@ namespace Microsoft.Boogie.Houdini {
ModelViewInfo mvInfo;
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo);
Hashtable/*<int, Absy!>*/ label2absy;
+
+ if (!CommandLineOptions.Clo.UseLabels) {
+ controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
+ impl.LocVars.Add(controlFlowVariable);
+ entryBlockId = impl.Blocks[0].UniqueId;
+ }
- conjecture = vcgen.GenerateVC(impl, null, out label2absy, checker);
+ conjecture = vcgen.GenerateVC(impl, controlFlowVariable, out label2absy, checker);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);
@@ -52,6 +60,16 @@ namespace Microsoft.Boogie.Houdini {
collector.examples.Clear();
VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);
+ if (!CommandLineOptions.Clo.UseLabels) {
+ var ctx = checker.TheoremProver.Context;
+ var bet = ctx.BoogieExprTranslator;
+ VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);
+ Contract.Assert(controlFlowVariableExpr != null);
+ VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(Microsoft.Basetypes.BigNum.ZERO));
+ Contract.Assert(controlFlowFunctionAppl != null);
+ vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(Microsoft.Basetypes.BigNum.FromInt(entryBlockId))), vc);
+ }
+
DateTime now = DateTime.UtcNow;
checker.BeginCheck(descriptiveName, vc, handler);
WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 7ffe8323..657603d0 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -285,6 +285,15 @@ namespace Microsoft.Boogie.SMTLib
Process.Close();
}
+ string controlFlowVariable;
+
+ private VCExpr ArgumentZero(VCExpr vc) {
+ VCExprNAry naryExpr = vc as VCExprNAry;
+ if (naryExpr == null)
+ return null;
+ return naryExpr[0];
+ }
+
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
//Contract.Requires(descriptiveName != null);
@@ -298,6 +307,9 @@ namespace Microsoft.Boogie.SMTLib
currentLogFile.Write(common.ToString());
}
+ if (!CommandLineOptions.Clo.UseLabels)
+ controlFlowVariable = VCExpr2String(ArgumentZero(ArgumentZero(ArgumentZero(vc))),1);
+
PrepareCommon();
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -450,7 +462,7 @@ namespace Microsoft.Boogie.SMTLib
}
private string[] CalculatePath() {
- SendThisVC("(get-value ((ControlFlow @cfc 0)))");
+ SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " 0)))");
var path = new List<string>();
while (true) {
var resp = Process.GetProverResponse();
@@ -472,7 +484,7 @@ namespace Microsoft.Boogie.SMTLib
else {
path.Add("+" + v);
}
- SendThisVC("(get-value ((ControlFlow @cfc " + v + ")))");
+ SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " " + v + ")))");
}
return path.ToArray();
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d13811e0..e0d7b4a7 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -208,8 +208,12 @@ namespace VC
Hashtable/*<int, Absy!>*/ label2absy;
VCExpressionGenerator gen = checker.VCExprGen;
Contract.Assert(gen != null);
+
+
VCExpr vcexpr = gen.Not(GenerateVC(impl, null, out label2absy, checker));
Contract.Assert(vcexpr != null);
+
+
info.label2absy = label2absy;
info.mvInfo = mvInfo;
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 6d4d8051..94892c29 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -136,9 +136,9 @@ namespace VC {
Contract.Assert(controlFlowFunctionAppl != null);
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));
+ return gen.AndSimp(gen.Implies(assertFailure, C), N);
} else {
- return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));
+ return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), N);
}
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 03:49:48 +0000