diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 3 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 16 | ||||
| -rw-r--r-- | Test/AbsHoudini/Answer | 102 | ||||
| -rw-r--r-- | Test/AbsHoudini/fail1.bpl | 16 | ||||
| -rw-r--r-- | Test/AbsHoudini/runtest.bat | 8 |
5 files changed, 121 insertions, 24 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index bf60bcbf..3e2b83de 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -676,7 +676,8 @@ namespace Microsoft.Boogie { // Run Abstract Houdini
var abs = new Houdini.AbsHoudini(program, domain);
- abs.ComputeSummaries();
+ var absout = abs.ComputeSummaries();
+ ProcessOutcome(absout.outcome, absout.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
//Houdini.PredicateAbs.Initialize(program);
//var abs = new Houdini.AbstractHoudini(program);
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 91b89262..19969666 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -112,8 +112,10 @@ namespace Microsoft.Boogie.Houdini { name2Impl.Values.Iter(GenVC);
}
- public void ComputeSummaries()
+ public VCGenOutcome ComputeSummaries()
{
+ var overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Valid, new List<Counterexample>());
+
// Compute SCCs and determine a priority order for impls
var Succ = new Dictionary<string, HashSet<string>>();
var Pred = new Dictionary<string, HashSet<string>>();
@@ -206,7 +208,7 @@ namespace Microsoft.Boogie.Houdini { Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());
if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
- throw new AbsHoudiniInternalError("Timeout/Spaceout while verifying " + impl);
+ return new VCGenOutcome(proverOutcome, new List<Counterexample>());
if (CommandLineOptions.Clo.Trace)
Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT");
@@ -214,6 +216,11 @@ namespace Microsoft.Boogie.Houdini { if (collector.numErrors > 0)
{
var funcsChanged = collector.funcsChanged;
+ if (funcsChanged.Count == 0)
+ {
+ overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Invalid, collector.errors);
+ break;
+ }
// propagate dependent guys back into the worklist, including self
var deps = new HashSet<string>();
@@ -237,6 +244,8 @@ namespace Microsoft.Boogie.Houdini { // Print the answer
existentialFunctions.Values.Iter(PrintFunction);
}
+
+ return overallOutcome;
}
public IEnumerable<Function> GetAssignment()
@@ -369,6 +378,7 @@ namespace Microsoft.Boogie.Houdini { public HashSet<string> funcsChanged;
public string currImpl;
public int numErrors;
+ public List<Counterexample> errors;
AbsHoudini container;
@@ -383,11 +393,13 @@ namespace Microsoft.Boogie.Houdini { funcsChanged = new HashSet<string>();
currImpl = impl;
numErrors = 0;
+ errors = new List<Counterexample>();
}
public override void OnCounterexample(Counterexample ce, string reason)
{
numErrors++;
+ errors.Add(ce);
funcsChanged.UnionWith(
container.HandleCounterExample(currImpl, ce));
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index 2ba2eed3..58da416e 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -5,7 +5,7 @@ function {:existential true} {:inline} b1(x: bool) : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd2.bpl --------------------
function {:existential true} {:inline} Assert(x: bool) : bool
@@ -21,7 +21,7 @@ function {:existential true} {:inline} b2(x: bool) : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd3.bpl --------------------
function {:existential true} {:inline} Assert(x: bool) : bool
@@ -37,7 +37,7 @@ function {:existential true} {:inline} b2(x: bool) : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd4.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -61,7 +61,7 @@ function {:existential true} {:inline} b4(x: bool) : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd5.bpl --------------------
function {:existential true} {:inline} b1(x: bool) : bool
@@ -89,7 +89,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd6.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -129,7 +129,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd7.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -149,7 +149,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd8.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -165,10 +165,7 @@ function {:existential true} {:inline} b3() : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
-
--------------------- houd9.bpl --------------------
-Error opening file "houd9.bpl": Could not find file 'C:\Users\akashl\Documents\work\boogie\Test\AbsHoudini\houd9.bpl'.
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd10.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -188,7 +185,7 @@ function {:existential true} {:inline} Assert() : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd11.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -196,7 +193,7 @@ function {:existential true} {:inline} Assert() : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd12.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -232,7 +229,20 @@ function {:existential true} {:inline} b7() : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- fail1.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ false
+}
+fail1.bpl(14,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ fail1.bpl(9,3): anon0
+ fail1.bpl(10,11): anon4_Then
+ fail1.bpl(14,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
.
-------------------- test1.bpl --------------------
function {:existential true} {:inline} b0() : bool
@@ -252,7 +262,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test2.bpl --------------------
function {:existential true} {:inline} b0() : bool
@@ -272,7 +282,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test7.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -280,7 +290,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test8.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -288,7 +298,7 @@ function {:existential true} {:inline} Assert() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test9.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -356,7 +366,7 @@ function {:existential true} {:inline} b16() : bool true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test10.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -376,4 +386,56 @@ function {:existential true} {:inline} b4() : bool false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred1.bpl --------------------
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+ x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+ x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred2.bpl --------------------
+function {:existential true} {:inline} b0(x: bool) : bool
+{
+ x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred3.bpl --------------------
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+ x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+ x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred4.bpl --------------------
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool
+{
+ x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl new file mode 100644 index 00000000..abbd015b --- /dev/null +++ b/Test/AbsHoudini/fail1.bpl @@ -0,0 +1,16 @@ +function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+ assert false;
+}
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index 88ac1fd5..0bc74dfc 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -3,7 +3,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd10.bpl houd11.bpl houd12.bpl fail1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
@@ -14,3 +14,9 @@ for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do ( echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f
)
+
+for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:PredicateAbs %%f
+)
|