From a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 18 Apr 2013 17:50:18 +0530 Subject: Nice clean re-implementation of AbstractHoudini. And tests --- Source/BoogieDriver/BoogieDriver.cs | 38 +++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9d1038f5..9b31c31e 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -639,15 +639,45 @@ namespace Microsoft.Boogie { { if (CommandLineOptions.Clo.AbstractHoudini != null) { - CommandLineOptions.Clo.PrintErrorModel = 1; + //CommandLineOptions.Clo.PrintErrorModel = 1; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; CommandLineOptions.Clo.ProverCCLimit = 1; + CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never; + + // Declare abstract domains + var domains = new List>(new System.Tuple[] { + System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), + System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) + }); + + domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2)); + + // Find the abstract domain + Houdini.IAbstractDomain domain = null; + foreach (var tup in domains) + { + if (tup.Item1 == CommandLineOptions.Clo.AbstractHoudini) + { + domain = tup.Item2; + break; + } + } + if (domain == null) + { + Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini); + Console.WriteLine("Supported domains are:"); + domains.Iter(tup => Console.WriteLine(" {0}", tup.Item1)); + throw new Houdini.AbsHoudiniInternalError("Domain not found"); + } // Run Abstract Houdini - Houdini.PredicateAbs.Initialize(program); - var abs = new Houdini.AbstractHoudini(program); - abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType().First().Name)); + var abs = new Houdini.AbsHoudini(program, domain); + abs.ComputeSummaries(); + + //Houdini.PredicateAbs.Initialize(program); + //var abs = new Houdini.AbstractHoudini(program); + //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType().First().Name)); return PipelineOutcome.Done; } -- cgit v1.2.3 From 2afe289c11d78711d4483e1ed36346998689668c Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 18 Apr 2013 22:29:51 +0530 Subject: AbsHoudini: Added support for /inlineDepth, and fixed the regression tests (all pass) --- Source/BoogieDriver/BoogieDriver.cs | 2 + Source/Houdini/AbstractHoudini.cs | 110 +++++++++++ Test/AbsHoudini/Answer | 384 +++++++++++++++++++++++++++++++++++- Test/AbsHoudini/houd1.bpl | 3 +- Test/AbsHoudini/runtest.bat | 4 +- Test/AbsHoudini/test1.bpl | 16 +- Test/AbsHoudini/test10.bpl | 19 +- Test/AbsHoudini/test2.bpl | 16 +- Test/AbsHoudini/test7.bpl | 8 +- Test/AbsHoudini/test8.bpl | 8 +- Test/AbsHoudini/test9.bpl | 81 +++++--- 11 files changed, 581 insertions(+), 70 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9b31c31e..9ef365c0 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -640,6 +640,8 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.AbstractHoudini != null) { //CommandLineOptions.Clo.PrintErrorModel = 1; + CommandLineOptions.Clo.UseProverEvaluate = true; + CommandLineOptions.Clo.ModelViewFile = "z3model"; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; CommandLineOptions.Clo.ProverCCLimit = 1; diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index e35e4a5c..3c649ed5 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -82,6 +82,8 @@ namespace Microsoft.Boogie.Houdini { if (CommandLineOptions.Clo.ProverKillTime > 0) CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); + Inline(); + this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1); @@ -337,6 +339,114 @@ namespace Microsoft.Boogie.Houdini { impl2VC.Add(impl.Name, gen.Function(macro)); } + private void Inline() + { + if (CommandLineOptions.Clo.InlineDepth < 0) + return; + + var callGraph = BuildCallGraph(); + + foreach (Implementation impl in callGraph.Nodes) + { + InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor(); + inlineRequiresVisitor.Visit(impl); + } + + foreach (Implementation impl in callGraph.Nodes) + { + FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor(); + freeRequiresVisitor.Visit(impl); + } + + foreach (Implementation impl in callGraph.Nodes) + { + InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor(); + inlineEnsuresVisitor.Visit(impl); + } + + foreach (Implementation impl in callGraph.Nodes) + { + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; + } + foreach (Implementation impl in callGraph.Nodes) + { + CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining; + CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec; + Inliner.ProcessImplementationForHoudini(program, impl); + CommandLineOptions.Clo.ProcedureInlining = savedOption; + } + foreach (Implementation impl in callGraph.Nodes) + { + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; + } + + Graph oldCallGraph = callGraph; + callGraph = new Graph(); + foreach (Implementation impl in oldCallGraph.Nodes) + { + callGraph.AddSource(impl); + } + foreach (Tuple edge in oldCallGraph.Edges) + { + callGraph.AddEdge(edge.Item1, edge.Item2); + } + int count = CommandLineOptions.Clo.InlineDepth; + while (count > 0) + { + foreach (Implementation impl in oldCallGraph.Nodes) + { + List newNodes = new List(); + foreach (Implementation succ in callGraph.Successors(impl)) + { + newNodes.AddRange(oldCallGraph.Successors(succ)); + } + foreach (Implementation newNode in newNodes) + { + callGraph.AddEdge(impl, newNode); + } + } + count--; + } + } + + private Graph BuildCallGraph() + { + Graph callGraph = new Graph(); + Dictionary> procToImpls = new Dictionary>(); + foreach (Declaration decl in program.TopLevelDeclarations) + { + Procedure proc = decl as Procedure; + if (proc == null) continue; + procToImpls[proc] = new HashSet(); + } + foreach (Declaration decl in program.TopLevelDeclarations) + { + Implementation impl = decl as Implementation; + if (impl == null || impl.SkipVerification) continue; + callGraph.AddSource(impl); + procToImpls[impl.Proc].Add(impl); + } + foreach (Declaration decl in program.TopLevelDeclarations) + { + Implementation impl = decl as Implementation; + if (impl == null || impl.SkipVerification) continue; + foreach (Block b in impl.Blocks) + { + foreach (Cmd c in b.Cmds) + { + CallCmd cc = c as CallCmd; + if (cc == null) continue; + foreach (Implementation callee in procToImpls[cc.Proc]) + { + callGraph.AddEdge(impl, callee); + } + } + } + } + return callGraph; + } } diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index d2418bd4..2ba2eed3 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -1,11 +1,379 @@ --------------------- f1.bpl -------------------- -Summary of foo: -g == old(g) + 1 -Summary of main: -(old(g) == 0 ==> g == old(g) + 1) -Prover time = 0.0260026 -Number of prover queries = 6 -Witness written to absHoudiniWitness.bpl +-------------------- houd1.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd2.bpl -------------------- +function {:existential true} {:inline} Assert(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd3.bpl -------------------- +function {:existential true} {:inline} Assert(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b1(x: bool) : bool +{ + true +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd4.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + false +} +function {:existential true} {:inline} b3(x: bool) : bool +{ + false +} +function {:existential true} {:inline} b4(x: bool) : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd5.bpl -------------------- +function {:existential true} {:inline} b1(x: bool) : bool +{ + !x +} +function {:existential true} {:inline} b2(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b3(x: bool) : bool +{ + !x +} +function {:existential true} {:inline} b4(x: bool) : bool +{ + x +} +function {:existential true} {:inline} b5() : bool +{ + false +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd6.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} b4() : bool +{ + true +} +function {:existential true} {:inline} b5() : bool +{ + true +} +function {:existential true} {:inline} b6() : bool +{ + true +} +function {:existential true} {:inline} b7() : bool +{ + true +} +function {:existential true} {:inline} b8() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd7.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd8.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + true +} +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'. + +-------------------- houd10.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd11.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors + +-------------------- houd12.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + false +} +function {:existential true} {:inline} b4() : bool +{ + false +} +function {:existential true} {:inline} b5() : bool +{ + false +} +function {:existential true} {:inline} b6() : bool +{ + true +} +function {:existential true} {:inline} b7() : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test1.bpl -------------------- +function {:existential true} {:inline} b0() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test2.bpl -------------------- +function {:existential true} {:inline} b0() : bool +{ + false +} +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test7.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test8.bpl -------------------- +function {:existential true} {:inline} Assert() : bool +{ + false +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test9.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + true +} +function {:existential true} {:inline} b2() : bool +{ + true +} +function {:existential true} {:inline} b3() : bool +{ + true +} +function {:existential true} {:inline} b4() : bool +{ + false +} +function {:existential true} {:inline} b5() : bool +{ + true +} +function {:existential true} {:inline} b6() : bool +{ + false +} +function {:existential true} {:inline} b7() : bool +{ + true +} +function {:existential true} {:inline} b8() : bool +{ + true +} +function {:existential true} {:inline} b9() : bool +{ + true +} +function {:existential true} {:inline} b10() : bool +{ + false +} +function {:existential true} {:inline} b11() : bool +{ + true +} +function {:existential true} {:inline} b12() : bool +{ + false +} +function {:existential true} {:inline} b13() : bool +{ + true +} +function {:existential true} {:inline} b14() : bool +{ + true +} +function {:existential true} {:inline} b15() : bool +{ + true +} +function {:existential true} {:inline} b16() : bool +{ + true +} + +Boogie program verifier finished with 0 verified, 0 errors +. +-------------------- test10.bpl -------------------- +function {:existential true} {:inline} b1() : bool +{ + false +} +function {:existential true} {:inline} b2() : bool +{ + false +} +function {:existential true} {:inline} b3() : bool +{ + false +} +function {:existential true} {:inline} b4() : bool +{ + false +} Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl index 099c6f09..fc3d5713 100644 --- a/Test/AbsHoudini/houd1.bpl +++ b/Test/AbsHoudini/houd1.bpl @@ -14,5 +14,4 @@ ensures b1(myVar>0); } } -// expected output: Correct -// expected end assigment: b1(x) = x +// expected end assigment: b1(x) = true diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index b9816bb9..88ac1fd5 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -6,11 +6,11 @@ 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 ( echo. echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f ) for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do ( echo . echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f + %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f ) diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl index e6ce06c9..5884cf7b 100644 --- a/Test/AbsHoudini/test1.bpl +++ b/Test/AbsHoudini/test1.bpl @@ -2,7 +2,7 @@ var g: bool; procedure foo() modifies g; -ensures b0 ==> (!old(g) ==> old(g) == g); +ensures b0() || (!old(g) ==> old(g) == g); { call AcquireLock(); call ReleaseLock(); @@ -10,14 +10,14 @@ ensures b0 ==> (!old(g) ==> old(g) == g); procedure AcquireLock() modifies g; -ensures b1 ==> old(g) == g; +ensures b1() || old(g) == g; { g := true; } procedure ReleaseLock() modifies g; -ensures b2 ==> old(g) == g; +ensures b2() || old(g) == g; { g := false; } @@ -27,10 +27,12 @@ modifies g; { g := false; call foo(); - assert !g; + assert Assert() || !g; } -const {:existential true} b0: bool; -const {:existential true} b1: bool; -const {:existential true } b2: bool; +function {:existential true} b0(): bool; +function {:existential true} b1(): bool; +function {:existential true } b2(): bool; +function {:existential true} Assert(): bool; +// Expected: b0 = false, b1 = true, b2 = true, Assert = false diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl index abb993f7..a30c3159 100644 --- a/Test/AbsHoudini/test10.bpl +++ b/Test/AbsHoudini/test10.bpl @@ -1,9 +1,9 @@ var sdv_7: int; var sdv_21: int; -const {:existential true} b1: bool; -const{:existential true} b2: bool; -const{:existential true} b3: bool; -const{:existential true} b4: bool; +function {:existential true} b1(): bool; +function{:existential true} b2(): bool; +function{:existential true} b3(): bool; +function{:existential true} b4(): bool; procedure push(a:int) modifies sdv_7, sdv_21; @@ -21,8 +21,8 @@ modifies sdv_7, sdv_21; procedure foo() modifies sdv_7, sdv_21; -requires {:candidate} b1 ==> (sdv_7 == 0); -ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7)); +requires {:candidate} b1() || (sdv_7 == 0); +ensures{:candidate} b2() || (sdv_7 == old(sdv_7)); { call push(2); call pop(); @@ -30,8 +30,8 @@ ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7)); } procedure bar() -requires{:candidate} b3 ==> (sdv_7 == 0); -ensures{:candidate} b4 ==> (sdv_7 == old(sdv_7)); +requires{:candidate} b3() || (sdv_7 == 0); +ensures{:candidate} b4() || (sdv_7 == old(sdv_7)); modifies sdv_7, sdv_21; { call push(1); @@ -45,3 +45,6 @@ modifies sdv_7, sdv_21; call foo(); } +// Expected: All false + + diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl index febb28e6..bfd78363 100644 --- a/Test/AbsHoudini/test2.bpl +++ b/Test/AbsHoudini/test2.bpl @@ -3,7 +3,7 @@ var h: int; procedure foo() modifies g, h; -ensures b0 ==> old(g) == g; +ensures b0() || old(g) == g; { call AcquireLock(); call ReleaseLock(); @@ -11,7 +11,7 @@ ensures b0 ==> old(g) == g; procedure AcquireLock() modifies g, h; -ensures b1 ==> old(g) == g; +ensures b1() || old(g) == g; { h := g; g := 1; @@ -19,7 +19,7 @@ ensures b1 ==> old(g) == g; procedure ReleaseLock() modifies g, h; -ensures b2 ==> old(g) == g; +ensures b2() || old(g) == g; { g := h; } @@ -29,10 +29,12 @@ modifies g, h; { g := 0; call foo(); - assert g == 0; + assert Assert() || g == 0; } -const {:existential true} b0: bool; -const {:existential true} b1: bool; -const {:existential true } b2: bool; +function {:existential true} b0(): bool; +function {:existential true} b1(): bool; +function {:existential true} b2(): bool; +function {:existential true} Assert(): bool; +// Expected: Assert = false, b0 = false, b1 = true, b2 = true diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl index b5c6a4c6..bfe8a32d 100644 --- a/Test/AbsHoudini/test7.bpl +++ b/Test/AbsHoudini/test7.bpl @@ -1,3 +1,5 @@ +function {:existential true} Assert() : bool; + var g: int; procedure main() @@ -5,11 +7,13 @@ modifies g; { g := 0; call foo(); - assert g == 1; + assert Assert() || g == 1; } procedure foo() modifies g; { g := g + 1; -} \ No newline at end of file +} + +// Expected: Assert = false diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl index 12eab481..6c55016a 100644 --- a/Test/AbsHoudini/test8.bpl +++ b/Test/AbsHoudini/test8.bpl @@ -1,3 +1,5 @@ +function {:existential true} Assert(): bool; + var g: int; procedure main() @@ -5,7 +7,7 @@ modifies g; { g := 0; call foo(); - assert g == 1; + assert Assert() || g == 1; } procedure {:inline 1} foo() @@ -18,4 +20,6 @@ procedure bar() modifies g; { g := g + 1; -} \ No newline at end of file +} + +// Expected: Assert = false diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl index 24eb66e8..c08edf6b 100644 --- a/Test/AbsHoudini/test9.bpl +++ b/Test/AbsHoudini/test9.bpl @@ -1,28 +1,28 @@ var v1: int; var v2: int; var v3: int; -const{:existential true} b1: bool; -const{:existential true} b2: bool; -const{:existential true} b3: bool; -const{:existential true} b4: bool; -const{:existential true} b5: bool; -const{:existential true} b6: bool; -const{:existential true} b7: bool; -const{:existential true} b8: bool; -const{:existential true} b9: bool; -const{:existential true} b10: bool; -const{:existential true} b11: bool; -const{:existential true} b12: bool; -const{:existential true} b13: bool; -const{:existential true} b14: bool; -const{:existential true} b15: bool; -const{:existential true} b16: bool; +function{:existential true} b1(): bool; +function{:existential true} b2(): bool; +function{:existential true} b3(): bool; +function{:existential true} b4(): bool; +function{:existential true} b5(): bool; +function{:existential true} b6(): bool; +function{:existential true} b7(): bool; +function{:existential true} b8(): bool; +function{:existential true} b9(): bool; +function{:existential true} b10(): bool; +function{:existential true} b11(): bool; +function{:existential true} b12(): bool; +function{:existential true} b13(): bool; +function{:existential true} b14(): bool; +function{:existential true} b15(): bool; +function{:existential true} b16(): bool; procedure push() -requires {:candidate} b1 ==> v1 == 0; -requires {:candidate} b2 ==> v1 == 1; -ensures {:candidate} b3 ==> v1 == 0; -ensures {:candidate} b4 ==> v1 == 1; +requires {:candidate} b1() || v1 == 0; +requires {:candidate} b2() || v1 == 1; +ensures {:candidate} b3() || v1 == 0; +ensures {:candidate} b4() || v1 == 1; modifies v1,v2; { v2 := v1; @@ -31,10 +31,10 @@ modifies v1,v2; procedure pop() modifies v1,v2; -requires {:candidate} b5 ==> v1 == 0; -requires {:candidate} b6 ==> v1 == 1; -ensures {:candidate} b7 ==> v1 == 0; -ensures {:candidate} b8 ==> v1 == 1; +requires {:candidate} b5() || v1 == 0; +requires {:candidate} b6() || v1 == 1; +ensures {:candidate} b7() || v1 == 0; +ensures {:candidate} b8() || v1 == 1; { v1 := v2; havoc v2; @@ -42,10 +42,10 @@ ensures {:candidate} b8 ==> v1 == 1; procedure foo() modifies v1,v2; -requires {:candidate} b9 ==> v1 == 0; -requires {:candidate} b10 ==> v1 == 1; -ensures {:candidate} b11 ==> v1 == 0; -ensures {:candidate} b12 ==> v1 == 1; +requires {:candidate} b9() || v1 == 0; +requires {:candidate} b10() || v1 == 1; +ensures {:candidate} b11() || v1 == 0; +ensures {:candidate} b12() || v1 == 1; { call push(); call pop(); @@ -53,10 +53,10 @@ ensures {:candidate} b12 ==> v1 == 1; procedure bar() modifies v1,v2; -requires {:candidate} b13 ==> v1 == 0; -requires {:candidate} b14 ==> v1 == 1; -ensures {:candidate} b15 ==> v1 == 0; -ensures {:candidate} b16 ==> v1 == 1; +requires {:candidate} b13() || v1 == 0; +requires {:candidate} b14() || v1 == 1; +ensures {:candidate} b15() || v1 == 0; +ensures {:candidate} b16() || v1 == 1; { call push(); call pop(); @@ -71,3 +71,20 @@ modifies v1,v2; call bar(); } +// Expected: +//b1 = true +//b2 = true +//b3 = true +//b4 = false +//b5 = true +//b6 = false +//b7 = true +//b8 = true +//b9 = true +//b10 = false +//b11 = true +//b12 = false +//b13 = true +//b14 = true +//b15 = true +//b16 = true -- cgit v1.2.3 From 93e49749af27e816a6924e74cff620e589412c7b Mon Sep 17 00:00:00 2001 From: akashlal Date: Fri, 19 Apr 2013 11:02:07 +0530 Subject: AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, intervals domain --- Source/BoogieDriver/BoogieDriver.cs | 8 +- Source/Houdini/AbstractHoudini.cs | 160 ++++++++++++++++++++++++++++++++---- 2 files changed, 148 insertions(+), 20 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9ef365c0..0ffa5619 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -644,13 +644,15 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ModelViewFile = "z3model"; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; + // Because we use ProverEvaluate, we need to restrict counterexamples to 1 otherwise the model + // goes away for UseProverEvaluate CommandLineOptions.Clo.ProverCCLimit = 1; - CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never; - // Declare abstract domains var domains = new List>(new System.Tuple[] { + System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain), System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), - System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) + System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), + System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) }); domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2)); diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 3c649ed5..23ebeb20 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -79,8 +79,8 @@ namespace Microsoft.Boogie.Houdini { throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name)); }); - if (CommandLineOptions.Clo.ProverKillTime > 0) - CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); + //if (CommandLineOptions.Clo.ProverKillTime > 0) + // CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); Inline(); @@ -91,6 +91,7 @@ namespace Microsoft.Boogie.Houdini { this.numProverQueries = 0; program.TopLevelDeclarations.OfType() + .Where(impl => !impl.SkipVerification) .Iter(impl => name2Impl.Add(impl.Name, impl)); // Let's do VC Gen (and also build dependencies) @@ -99,12 +100,47 @@ namespace Microsoft.Boogie.Houdini { public void ComputeSummaries() { - var worklist = new Queue(); - name2Impl.Keys.Iter(k => worklist.Enqueue(k)); + // Compute SCCs and determine a priority order for impls + var Succ = new Dictionary>(); + var Pred = new Dictionary>(); + name2Impl.Keys.Iter(s => Succ[s] = new HashSet()); + name2Impl.Keys.Iter(s => Pred[s] = new HashSet()); + + foreach(var impl in name2Impl.Keys) { + Succ[impl] = new HashSet(); + impl2functionsAsserted[impl].Iter(f => + function2implAssumed[f].Iter(succ => + { + Succ[impl].Add(succ); + Pred[succ].Add(impl); + })); + } + + var sccs = new StronglyConnectedComponents(name2Impl.Keys, + new Adjacency(n => Pred[n]), + new Adjacency(n => Succ[n])); + sccs.Compute(); + + // impl -> priority + var impl2Priority = new Dictionary(); + int p = 0; + foreach (var scc in sccs) + { + foreach (var impl in scc) + { + impl2Priority.Add(impl, p); + p++; + } + } + + var worklist = new SortedSet>(); + name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k))); while (worklist.Any()) { - var impl = worklist.Dequeue(); + var impl = worklist.First().Item2; + worklist.Remove(worklist.First()); + var gen = prover.VCExprGen; Expr env = Expr.True; @@ -121,12 +157,14 @@ namespace Microsoft.Boogie.Houdini { env.Typecheck(new TypecheckingContext((IErrorSink)null)); var envVC = prover.Context.BoogieExprTranslator.Translate(env); - //Console.WriteLine("env: {0}", envVC); var vc = gen.Implies(envVC, impl2VC[impl]); if (CommandLineOptions.Clo.Trace) - Console.Write("Verifying {0}: ", impl); + { + Console.WriteLine("Verifying {0}: ", impl); + Console.WriteLine("env: {0}", envVC); + } var handler = impl2ErrorHandler[impl].Item1; var collector = impl2ErrorHandler[impl].Item2; @@ -162,16 +200,17 @@ namespace Microsoft.Boogie.Houdini { } if (CommandLineOptions.Clo.Trace) Console.WriteLine("SAT"); - Debug.Assert(collector.examples.Count == 1); - var error = collector.examples[0]; - // Find the failing assert -- need to do a join there - var cex = ExtractState(impl, error); var funcsChanged = new HashSet(); - foreach (var tup in cex) + foreach (var error in collector.examples) { - function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2); - funcsChanged.Add(tup.Item1); + // Find the failing assert -- need to do a join there + var cex = ExtractState(impl, error); + foreach (var tup in cex) + { + function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2); + funcsChanged.Add(tup.Item1); + } } // propagate dependent guys back into the worklist, including self @@ -179,12 +218,16 @@ namespace Microsoft.Boogie.Houdini { deps.Add(impl); funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f])); - deps.RemoveWhere(s => worklist.Contains(s)); - deps.Iter(s => worklist.Enqueue(s)); - + deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s))); prover.Pop(); } + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2")); + Console.WriteLine("Number of prover queries = " + numProverQueries); + } + if (CommandLineOptions.Clo.PrintAssignment) { // Print the answer @@ -525,6 +568,89 @@ namespace Microsoft.Boogie.Houdini { } + public class Intervals : IAbstractDomain + { + // [lower, upper] + int upper; + int lower; + // or: \bot + bool isBottom; + // number of times join has been performed + int nJoin; + // number of times before we widen + readonly static int maxJoin = 5; + + public Intervals() + { + this.upper = 0; + this.lower = 0; + this.nJoin = 0; + this.isBottom = true; + } + + private Intervals(int lower, int upper, int nJoin) + { + this.upper = upper; + this.lower = lower; + this.nJoin = nJoin; + } + + public IAbstractDomain Bottom() + { + return new Intervals(); + } + + public IAbstractDomain Join(List states) + { + Debug.Assert(states.Count == 1); + var state = states[0] as Model.Integer; + if (state == null) + throw new AbsHoudiniInternalError("Incorrect type, expected int"); + var intval = state.AsInt(); + + if (isBottom) + { + return new Intervals(intval, intval, 1); + } + + if(intval >= lower && intval <= upper) + return this; + + if (nJoin > maxJoin) + { + // widen + if (intval > upper) + return new Intervals(lower, Int32.MaxValue, 1); + if(intval < lower) + return new Intervals(Int32.MinValue, upper, 1); + + Debug.Assert(false); + } + + if (intval > upper) + return new Intervals(lower, intval, nJoin + 1); + if (intval < lower) + return new Intervals(intval, upper, nJoin + 1); + + Debug.Assert(false); + return null; + } + + public Expr Gamma(List vars) + { + Debug.Assert(vars.Count == 1); + var v = vars[0]; + if (isBottom) return Expr.False; + Expr ret = Expr.True; + if (lower != Int32.MinValue) + ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower))); + if (upper != Int32.MaxValue) + ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper))); + return ret; + } + + } + public class ConstantProp : IAbstractDomain { object val; -- cgit v1.2.3 From 410f9a6ade1e16402e283e39bb68e21bb9a8c10b Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 25 Apr 2013 13:51:18 +0530 Subject: AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini, few bug fixes, hack to support missing prover declarations. --- Source/BoogieDriver/BoogieDriver.cs | 2 + Source/Houdini/AbstractHoudini.cs | 83 ++++++++++++++++++++++++++++++++++++- 2 files changed, 83 insertions(+), 2 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 0ffa5619..f3194256 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -649,8 +649,10 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ProverCCLimit = 1; // Declare abstract domains var domains = new List>(new System.Tuple[] { + System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain), System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain), System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), + System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) }); diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 23ebeb20..d1e9ba96 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -320,7 +320,7 @@ namespace Microsoft.Boogie.Houdini { else { var val = prover.Evaluate(arg); - if (val is int || val is bool) + if (val is int || val is bool || val is Microsoft.Basetypes.BigNum) { return model.MkElement(val.ToString()); } @@ -362,7 +362,15 @@ namespace Microsoft.Boogie.Houdini { fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3)); var gen = prover.VCExprGen; - var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context); + VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO); + + var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context); + if (!CommandLineOptions.Clo.UseLabels) + { + VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO)); + VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId))); + vcexpr = gen.Implies(eqExpr, vcexpr); + } ProverInterface.ErrorHandler handler = null; if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) @@ -380,6 +388,19 @@ namespace Microsoft.Boogie.Houdini { // Store VC impl2VC.Add(impl.Name, gen.Function(macro)); + + // HACK: push the definitions of constants involved in function calls + // It is possible that some constants only appear in function calls. Thus, when + // they are replaced by Boolean constants, it is possible that (get-value) will + // fail if the expression involves such constants. All we need to do is make sure + // these constants are declared, because otherwise, semantically we are doing + // the right thing. + foreach (var tup in fv.functionsUsed) + { + var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3); + tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt); + prover.Assert(tt, true); + } } private void Inline() @@ -651,6 +672,64 @@ namespace Microsoft.Boogie.Houdini { } + // [false -- (x == true) -- true] + public class HoudiniConst : IAbstractDomain + { + bool isBottom; + bool isTop; + + private HoudiniConst(bool isTop, bool isBottom) + { + this.isBottom = isBottom; + this.isTop = isTop; + Debug.Assert(!(isTop && isBottom)); + } + + public static HoudiniConst GetExtObj() + { + return new HoudiniConst(false, false); + } + + public static HoudiniConst GetTop() + { + return new HoudiniConst(true, false); + } + + public static HoudiniConst GetBottom() + { + return new HoudiniConst(false, true); + } + + public IAbstractDomain Bottom() + { + return GetBottom(); + } + + public IAbstractDomain Join(List states) + { + Debug.Assert(states.Count == 1); + var state = states[0]; + + if (state is Model.Boolean) + { + if ((state as Model.Boolean).Value) + return GetExtObj(); + } + + return GetTop(); + } + + public Expr Gamma(List vars) + { + Debug.Assert(vars.Count == 1); + var v = vars[0]; + if (isBottom) return Expr.False; + if (isTop) return Expr.True; + return v; + } + } + + public class ConstantProp : IAbstractDomain { object val; -- cgit v1.2.3 From d1b98641093f94f76c74bdf477f2bfeeea3ad945 Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 25 Apr 2013 14:13:16 +0530 Subject: AbsHoudini: Added predicate-abstraction domain and some examples. --- Source/BoogieDriver/BoogieDriver.cs | 1 + Source/Houdini/AbstractHoudini.cs | 158 ++++++++++++++++++++++++++++++++++++ Test/AbsHoudini/pred1.bpl | 23 ++++++ Test/AbsHoudini/pred2.bpl | 12 +++ Test/AbsHoudini/pred3.bpl | 24 ++++++ 5 files changed, 218 insertions(+) create mode 100644 Test/AbsHoudini/pred1.bpl create mode 100644 Test/AbsHoudini/pred2.bpl create mode 100644 Test/AbsHoudini/pred3.bpl (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index f3194256..afc1a098 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -652,6 +652,7 @@ namespace Microsoft.Boogie { System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain), System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain), System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), + System.Tuple.Create("PredicateAbs", new Houdini.PredicateAbsElem() as Houdini.IAbstractDomain), System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index d1e9ba96..a0797308 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -347,6 +347,11 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl); var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo); + //CommandLineOptions.Clo.PrintInstrumented = true; + //var tt = new TokenTextWriter(Console.Out); + //impl.Emit(tt, 0); + //tt.Close(); + // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants var existentialFunctionNames = new HashSet(existentialFunctions.Keys); var fv = new ReplaceFunctionCalls(existentialFunctionNames); @@ -672,6 +677,159 @@ namespace Microsoft.Boogie.Houdini { } + public class PredicateAbsElem : IAbstractDomain + { + public static class ExprExt + { + public static Expr AndSimp(Expr e1, Expr e2) + { + if (e1 == Expr.True) return e2; + if (e2 == Expr.True) return e1; + if (e1 == Expr.False || e2 == Expr.False) return Expr.False; + return Expr.And(e1, e2); + } + + public static Expr OrSimp(Expr e1, Expr e2) + { + if (e1 == Expr.False) return e2; + if (e2 == Expr.False) return e1; + if (e1 == Expr.True || e2 == Expr.True) return Expr.True; + return Expr.Or(e1, e2); + } + } + + class Disjunct + { + public static int DisjunctBound = 3; + HashSet pos; + HashSet neg; + bool isTrue; + + public Disjunct() + { + isTrue = true; + pos = new HashSet(); + neg = new HashSet(); + } + + public Disjunct(IEnumerable pos, IEnumerable neg) + { + this.isTrue = false; + this.pos = new HashSet(pos); + this.neg = new HashSet(neg); + if (this.pos.Overlaps(this.neg)) + { + this.isTrue = true; + this.pos = new HashSet(); + this.neg = new HashSet(); + } + if (this.pos.Count + this.neg.Count > DisjunctBound) + { + // Set to true + this.isTrue = true; + this.pos = new HashSet(); + this.neg = new HashSet(); + } + + } + + public Disjunct OR(Disjunct that) + { + if (isTrue) + return this; + if (that.isTrue) + return that; + + return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg)); + } + + public bool Implies(Disjunct that) + { + if (isTrue) return that.isTrue; + if (that.isTrue) return true; + + return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg); + } + + public Expr Gamma(List vars) + { + if (isTrue) return Expr.True; + Expr ret = Expr.False; + pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i])); + neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i]))); + return ret; + } + } + + // Conjunction of Disjuncts + List conjuncts; + bool isFalse; + + public PredicateAbsElem() + { + this.conjuncts = new List(); + this.isFalse = true; + } + + public IAbstractDomain Bottom() + { + return new PredicateAbsElem(); + } + + public IAbstractDomain Join(List state) + { + if (state.Any(me => !(me is Model.Boolean))) + throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool"); + + // quick return if this == true + if (!this.isFalse && conjuncts.Count == 0) + return this; + + var ret = new PredicateAbsElem(); + ret.isFalse = false; + + for (int i = 0; i < state.Count; i++) + { + var b = (state[i] as Model.Boolean).Value; + Disjunct d = null; + if (b) d = new Disjunct(new int[] { i }, new int[] { }); + else d = new Disjunct(new int[] { }, new int[] { i }); + + if (isFalse) + ret.AddDisjunct(d); + else + { + conjuncts.Iter(c => ret.AddDisjunct(c.OR(d))); + } + } + + return ret; + + } + + public Expr Gamma(List vars) + { + if (isFalse) return Expr.False; + Expr ret = Expr.True; + + foreach (var c in conjuncts) + { + ret = ExprExt.AndSimp(ret, c.Gamma(vars)); + } + + return ret; + } + + private void AddDisjunct(Disjunct d) + { + if (conjuncts.Any(c => c.Implies(d))) + return; + + conjuncts.RemoveAll(c => d.Implies(c)); + conjuncts.Add(d); + } + } + // [false -- (x == true) -- true] public class HoudiniConst : IAbstractDomain { diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl new file mode 100644 index 00000000..fc37a15b --- /dev/null +++ b/Test/AbsHoudini/pred1.bpl @@ -0,0 +1,23 @@ +function {:existential true} b0(x:bool, y:bool): bool; +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} b2(x:bool, y:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == 0, g == 5); +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b2(g == 0, g == 5); +{ + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl new file mode 100644 index 00000000..3ce948ce --- /dev/null +++ b/Test/AbsHoudini/pred2.bpl @@ -0,0 +1,12 @@ +function {:existential true} b0(x:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == old(g)); +{ + if(*) { g := 5; } + assume g != 5; +} + diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl new file mode 100644 index 00000000..450efde4 --- /dev/null +++ b/Test/AbsHoudini/pred3.bpl @@ -0,0 +1,24 @@ +function {:existential true} b0(x:bool, y:bool): bool; +function {:existential true} b1(x:bool, y:bool): bool; +function {:existential true} b2(x:bool, y:bool): bool; + +var g: int; + +procedure main() +modifies g; +ensures b0(g == 0, g == 5); +{ + assume 0 == old(g) || 1 == old(g); + g := 0; + if(*) { g := 5; } + call foo(); +} + +procedure foo() + modifies g; + requires b1(g == 0, g == 5); + ensures b2(old(g) == 0, old(g) == 5); +{ + assume g != 5; +} + -- cgit v1.2.3 From e71b77d2c0d7d5c7bbb05ad58eaae96cd24a6d55 Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 25 Apr 2013 15:20:56 +0530 Subject: AbsHoudini: Added support for /errorLimit:n, n > 1 --- Source/BoogieDriver/BoogieDriver.cs | 3 -- Source/Houdini/AbstractHoudini.cs | 87 +++++++++++++++++++++++++------------ 2 files changed, 59 insertions(+), 31 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index afc1a098..6a141fac 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -644,9 +644,6 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ModelViewFile = "z3model"; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; - // Because we use ProverEvaluate, we need to restrict counterexamples to 1 otherwise the model - // goes away for UseProverEvaluate - CommandLineOptions.Clo.ProverCCLimit = 1; // Declare abstract domains var domains = new List>(new System.Tuple[] { System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain), diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index a0797308..8998d22c 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -35,7 +35,7 @@ namespace Microsoft.Boogie.Houdini { Dictionary> function2implAssumed, function2implAsserted; // impl -> handler, collector - Dictionary> impl2ErrorHandler; + Dictionary> impl2ErrorHandler; // Essentials: VCGen, Prover VCGen vcgen; @@ -57,7 +57,7 @@ namespace Microsoft.Boogie.Houdini { this.impl2functionsAssumed = new Dictionary>(); this.function2implAsserted = new Dictionary>(); this.function2implAssumed = new Dictionary>(); - this.impl2ErrorHandler = new Dictionary>(); + this.impl2ErrorHandler = new Dictionary>(); this.constant2FuncCall = new Dictionary(); // Find the existential functions @@ -168,7 +168,7 @@ namespace Microsoft.Boogie.Houdini { var handler = impl2ErrorHandler[impl].Item1; var collector = impl2ErrorHandler[impl].Item2; - collector.examples.Clear(); + collector.Reset(impl); var start = DateTime.Now; @@ -190,35 +190,22 @@ namespace Microsoft.Boogie.Houdini { if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory) throw new AbsHoudiniInternalError("Timeout/Spaceout while verifying " + impl); - - - if (collector.examples.Count == 0) - { - if (CommandLineOptions.Clo.Trace) Console.WriteLine("UNSAT"); - prover.Pop(); - continue; - } - if (CommandLineOptions.Clo.Trace) Console.WriteLine("SAT"); + if (CommandLineOptions.Clo.Trace) + Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT"); - var funcsChanged = new HashSet(); - foreach (var error in collector.examples) + if (collector.numErrors > 0) { - // Find the failing assert -- need to do a join there - var cex = ExtractState(impl, error); - foreach (var tup in cex) - { - function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2); - funcsChanged.Add(tup.Item1); - } - } + var funcsChanged = collector.funcsChanged; + + // propagate dependent guys back into the worklist, including self + var deps = new HashSet(); + deps.Add(impl); + funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f])); - // propagate dependent guys back into the worklist, including self - var deps = new HashSet(); - deps.Add(impl); - funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f])); + deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s))); + } - deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s))); prover.Pop(); } @@ -242,6 +229,20 @@ namespace Microsoft.Boogie.Houdini { } } + public HashSet HandleCounterExample(string impl, Counterexample error) + { + var funcsChanged = new HashSet(); + // Find the failing assert -- need to do a join there + // return the set of functions whose definition has changed + var cex = ExtractState(impl, error); + foreach (var tup in cex) + { + function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2); + funcsChanged.Add(tup.Item1); + } + return funcsChanged; + } + private List>> ExtractState(string impl, Counterexample error) { var lastBlock = error.Trace.Last() as Block; @@ -332,11 +333,41 @@ namespace Microsoft.Boogie.Houdini { } } + class AbsHoudiniCounterexampleCollector : VerifierCallback + { + public HashSet funcsChanged; + public string currImpl; + public int numErrors; + + AbsHoudini container; + + public AbsHoudiniCounterexampleCollector(AbsHoudini container) + { + this.container = container; + Reset(null); + } + + public void Reset(string impl) + { + funcsChanged = new HashSet(); + currImpl = impl; + numErrors = 0; + } + + public override void OnCounterexample(Counterexample ce, string reason) + { + numErrors++; + + funcsChanged.UnionWith( + container.HandleCounterExample(currImpl, ce)); + } + } + private void GenVC(Implementation impl) { ModelViewInfo mvInfo; System.Collections.Hashtable label2absy; - var collector = new ConditionGeneration.CounterexampleCollector(); + var collector = new AbsHoudiniCounterexampleCollector(this); collector.OnProgress("HdnVCGen", 0, 0, 0.0); if (CommandLineOptions.Clo.Trace) -- cgit v1.2.3