diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 13 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 60 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar7.bpl | 43 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar8.bpl | 42 |
7 files changed, 152 insertions, 19 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 6aed82cc..5425f6c0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -348,6 +348,7 @@ namespace Microsoft.Boogie { public int LazyInlining = 0;
public int StratifiedInlining = 0;
public int StratifiedInliningOption = 0;
+ public bool UseUnsatCoreForInlining = false;
public int RecursionBound = 500;
public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
@@ -1152,12 +1153,16 @@ namespace Microsoft.Boogie { CoverageReporterPath = args[ps.i];
}
break;
- case "-stratifiedInilneOption":
+ case "-stratifiedInlineOption":
case "/stratifiedInlineOption":
if (ps.ConfirmArgumentCount(1)) {
StratifiedInliningOption=Int32.Parse(cce.NonNull(args[ps.i]));
}
break;
+ case "-useUnsatCoreForInlining":
+ case "/useUnsatCoreForInlining":
+ UseUnsatCoreForInlining = true;
+ break;
case "-typeEncoding":
case "/typeEncoding":
if (ps.ConfirmArgumentCount(1)) {
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 2f2f03ce..5f776bff 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -99,11 +99,11 @@ namespace Microsoft.Boogie.Z3 outcome = cm.Check(out z3LabelModels);
}
- public override void CheckAssumptions(List<VCExpr> assumptions)
+ public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
Z3SafeContext cm = context.cm;
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels);
+ outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index f3a42670..97ff41c5 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -388,10 +388,13 @@ namespace Microsoft.Boogie.Z3 }
}
- public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions, out List<Z3ErrorModelAndLabels> boogieErrors)
+ public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
+ out List<Z3ErrorModelAndLabels> boogieErrors,
+ out List<int> unsatCore)
{
Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
boogieErrors = new List<Z3ErrorModelAndLabels>();
+ unsatCore = new List<int>();
LBool outcome = LBool.Undef;
Model z3Model;
@@ -440,6 +443,14 @@ namespace Microsoft.Boogie.Z3 }
else if (outcome == LBool.False)
{
+ foreach (Term t in core)
+ {
+ for (int i = 0; i < assumption_terms.Length; i++)
+ {
+ if (t.Equals(assumption_terms[i]))
+ unsatCore.Add(i);
+ }
+ }
return ProverInterface.Outcome.Valid;
}
else
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 54a8823f..eeaab21d 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -671,7 +671,7 @@ namespace Microsoft.Boogie { public abstract void Assert(VCExpr vc, bool polarity);
public abstract void AssertAxioms();
public abstract void Check();
- public abstract void CheckAssumptions(List<VCExpr> assumptions);
+ public abstract void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore);
public abstract void Push();
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 2be23c41..134dbd04 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -548,10 +548,14 @@ namespace VC abstract public void Pop();
abstract public void AddAxiom(VCExpr vc);
abstract public void LogComment(string str);
- virtual public Outcome CheckAssumptions(List<VCExpr> assumptions)
+ virtual public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
Outcome ret;
+ unsatCore = new List<int>();
+ for (int i = 0; i < assumptions.Count; i++)
+ unsatCore.Add(i);
+
if (assumptions.Count == 0)
{
return CheckVC();
@@ -742,21 +746,22 @@ namespace VC checker.TheoremProver.LogComment(str);
}
- public override Outcome CheckAssumptions(List<VCExpr> assumptions)
+ public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
if (!UseCheckAssumptions)
{
- return base.CheckAssumptions(assumptions);
+ return base.CheckAssumptions(assumptions, out unsatCore);
}
if (assumptions.Count == 0)
{
+ unsatCore = new List<int>();
return CheckVC();
}
//TheoremProver.Push();
TheoremProver.AssertAxioms();
- TheoremProver.CheckAssumptions(assumptions);
+ TheoremProver.CheckAssumptions(assumptions, out unsatCore);
ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);
//TheoremProver.Pop();
numQueries++;
@@ -1036,7 +1041,6 @@ namespace VC done = 1;
coverageManager.reportCorrect(bound);
}
-
}
else
{
@@ -1107,21 +1111,45 @@ namespace VC private Outcome stratifiedStep(int bound, VerificationState vState)
{
Outcome ret;
-
+ List<int> unsatCore;
+
var reporter = vState.reporter;
var calls = vState.calls;
var checker = vState.checker;
reporter.underapproximationMode = true;
checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
+ List<VCExpr> assumptions;
+ List<int> ids;
- var assumptions = new List<VCExpr>();
- foreach (int id in calls.currCandidates)
+ while (true)
{
- assumptions.Add(calls.getFalseExpr(id));
- }
+ assumptions = new List<VCExpr>();
+ ids = new List<int>();
+ foreach (int id in calls.currCandidates)
+ {
+ assumptions.Add(calls.getFalseExpr(id));
+ ids.Add(id);
+ }
+
+ ret = checker.CheckAssumptions(assumptions, out unsatCore);
+ if (!CommandLineOptions.Clo.UseUnsatCoreForInlining) break;
+ if (ret != Outcome.Correct) break;
+ Debug.Assert(unsatCore.Count <= assumptions.Count);
+ if (unsatCore.Count == assumptions.Count)
+ break;
- ret = checker.CheckAssumptions(assumptions);
+ var unsatCoreIds = new List<int>();
+ foreach (int i in unsatCore)
+ unsatCoreIds.Add(ids[i]);
+ vState.checker.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
+ bool incrementalSearch =
+ CommandLineOptions.Clo.StratifiedInliningOption == 0 ||
+ CommandLineOptions.Clo.StratifiedInliningOption == 2;
+ DoExpansion(incrementalSearch, unsatCoreIds, vState);
+ vState.calls.forcedCandidates.UnionWith(unsatCoreIds);
+ vState.checker.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
+ }
checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
@@ -1182,7 +1210,7 @@ namespace VC }
else
{
- ret = checker.CheckAssumptions(assumptions);
+ ret = checker.CheckAssumptions(assumptions, out unsatCore);
}
if (ret != Outcome.Correct && ret != Outcome.Errors)
@@ -1474,7 +1502,9 @@ namespace VC // Name of main procedure
private string mainProcName;
- // User info -- to decrease/increase calculcation of recursion bound
+ public HashSet<int> forcedCandidates;
+
+ // User info -- to decrease/increase calculation of recursion bound
public Dictionary<int, int> recursionIncrement;
public HashSet<int> currCandidates;
@@ -1525,6 +1555,8 @@ namespace VC persistentNameCache[0] = "0";
persistentNameInv["0"] = 0;
recentlyAddedCandidates = new HashSet<int>();
+
+ forcedCandidates = new HashSet<int>();
}
public void Clear()
@@ -1546,7 +1578,7 @@ namespace VC {
if (recursionIncrement.ContainsKey(id)) ret += recursionIncrement[id];
id = candidateParent[id];
- if (getProc(id) == str) ret++;
+ if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
}
return ret;
}
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl new file mode 100644 index 00000000..747510de --- /dev/null +++ b/Test/stratifiedinline/bar7.bpl @@ -0,0 +1,43 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 80) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo();
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl new file mode 100644 index 00000000..d447e3a7 --- /dev/null +++ b/Test/stratifiedinline/bar8.bpl @@ -0,0 +1,42 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 80) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m) {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 2;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo();
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file |