From df1cd695daffb01a590a7310dbee1b6594de2ecd Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 23 Nov 2011 11:26:34 -0800 Subject: fixed bug in the inlineDepth option for houdini small clean up in the inlining implementation --- Source/BoogieDriver/BoogieDriver.cs | 3 +- Source/Core/Inline.cs | 64 ++++++------ Source/Houdini/Houdini.cs | 17 ++++ Test/houdini/Answer | 10 ++ Test/houdini/runtest.bat | 6 ++ Test/houdini/test7.bpl | 15 +++ Test/houdini/test8.bpl | 21 ++++ Test/inline/Answer | 191 ------------------------------------ Test/inline/runtest.bat | 5 - Test/inline/test7.bpl | 15 --- Test/inline/test8.bpl | 21 ---- 11 files changed, 100 insertions(+), 268 deletions(-) create mode 100644 Test/houdini/test7.bpl create mode 100644 Test/houdini/test8.bpl delete mode 100644 Test/inline/test7.bpl delete mode 100644 Test/inline/test8.bpl diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 4073c722..7e2ea87a 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -390,8 +390,7 @@ namespace Microsoft.Boogie { inline = true; } } - if ((inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) || - CommandLineOptions.Clo.InlineDepth >= 0) { + if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) { foreach (Declaration d in TopLevelDeclarations) { Implementation impl = d as Implementation; if (impl != null) { diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index c9f6445c..07a8e8a9 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -66,19 +66,18 @@ namespace Microsoft.Boogie { return prefix + "$" + formalName; } - protected Inliner(InlineCallback cb) { - inlinedProcLblMap = new Dictionary(); - recursiveProcUnrollMap = new Dictionary(); - inlineDepth = CommandLineOptions.Clo.InlineDepth; - codeCopier = new CodeCopier(); - inlineCallback = cb; + protected Inliner(InlineCallback cb, int inlineDepth) { + this.inlinedProcLblMap = new Dictionary(); + this.recursiveProcUnrollMap = new Dictionary(); + this.inlineDepth = inlineDepth; + this.codeCopier = new CodeCopier(); + this.inlineCallback = cb; } - public static void ProcessImplementation(Program program, Implementation impl, InlineCallback cb) { + private static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) { Contract.Requires(impl != null); Contract.Requires(program != null); Contract.Requires(impl.Proc != null); - Inliner inliner = new Inliner(cb); VariableSeq/*!*/ newInParams = new VariableSeq(impl.InParams); Contract.Assert(newInParams != null); @@ -90,7 +89,7 @@ namespace Microsoft.Boogie { Contract.Assert(newModifies != null); bool inlined = false; - List/*!*/ newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined); + List newBlocks = inliner.DoInlineBlocks(impl.Blocks, program, newLocalVars, newModifies, ref inlined); Contract.Assert(cce.NonNullElements(newBlocks)); if (!inlined) @@ -112,12 +111,18 @@ namespace Microsoft.Boogie { } } + public static void ProcessImplementationForHoudini(Program program, Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(program != null); + Contract.Requires(impl.Proc != null); + ProcessImplementation(program, impl, new Inliner(null, CommandLineOptions.Clo.InlineDepth)); + } public static void ProcessImplementation(Program program, Implementation impl) { Contract.Requires(impl != null); Contract.Requires(program != null); Contract.Requires(impl.Proc != null); - ProcessImplementation(program, impl, null); + ProcessImplementation(program, impl, new Inliner(null, -1)); } protected void EmitImpl(Implementation impl) { @@ -231,10 +236,10 @@ namespace Microsoft.Boogie { newCmds.Add(codeCopier.CopyCmd(cmd)); continue; } - - int inline = GetInlineCount(impl); - if (inline > 0 || (inline == -1 && inlineDepth > 0)) { // at least one block should exist + int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(impl); + + if (inline > 0) { // at least one block should exist Contract.Assume(impl != null); Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0); inlinedSomething = true; @@ -258,17 +263,22 @@ namespace Microsoft.Boogie { EndInline(); - if (inline > 0) - recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1; - else + if (inlineDepth >= 0) { + Debug.Assert(inlineDepth > 0); inlineDepth = inlineDepth - 1; + } + else { + recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1; + } inlinedBlocks = DoInlineBlocks(inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething); - if (inline > 0) - recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1; - else + if (inlineDepth >= 0) { inlineDepth = inlineDepth + 1; + } + else { + recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1; + } Block/*!*/ startBlock = inlinedBlocks[0]; Contract.Assert(startBlock != null); @@ -281,7 +291,7 @@ namespace Microsoft.Boogie { lblCount = nextlblCount; newCmds = new CmdSeq(); - } else if (inline == 0 || (inline == -1 && inlineDepth == 0)) { + } else if (inline == 0) { inlinedSomething = true; if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) { // add assert @@ -306,20 +316,6 @@ namespace Microsoft.Boogie { return newBlocks; } - protected List/*!*/ DoInline(List/*!*/ blocks, Program program, VariableSeq newLocalVars, IdentifierExprSeq newModifies, out bool inlined) { - Contract.Requires(newModifies != null); - Contract.Requires(newLocalVars != null); - Contract.Requires(program != null); - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - inlinedProcLblMap.Clear(); - recursiveProcUnrollMap.Clear(); - inlineDepth = CommandLineOptions.Clo.InlineDepth; - - inlined = false; - return DoInlineBlocks(blocks, program, newLocalVars, newModifies, ref inlined); - } - protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) { Contract.Requires(impl != null); Contract.Requires(impl.Proc != null); diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 2c202022..ed3d1afc 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -261,6 +261,7 @@ namespace Microsoft.Boogie.Houdini { this.callGraph = BuildCallGraph(); this.continueAtError = continueAtError; this.houdiniConstants = CollectExistentialConstants(); + Inline(); this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime); @@ -277,6 +278,22 @@ namespace Microsoft.Boogie.Houdini { this.houdiniSessions = new ReadOnlyDictionary(houdiniSessions); } + private void Inline() { + if (CommandLineOptions.Clo.InlineDepth < 0) + return; + foreach (Implementation impl in callGraph.Nodes) { + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; + } + foreach (Implementation impl in callGraph.Nodes) { + Inliner.ProcessImplementationForHoudini(program, impl); + } + foreach (Implementation impl in callGraph.Nodes) { + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; + } + } + private ReadOnlyDictionary CollectExistentialConstants() { Dictionary existentialConstants = new Dictionary(); foreach (Declaration decl in program.TopLevelDeclarations) { diff --git a/Test/houdini/Answer b/Test/houdini/Answer index 94ae7f04..60ae7d80 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -99,3 +99,13 @@ b6 = False b7 = False Boogie program verifier finished with 1 verified, 0 errors +. +-------------------- test7.bpl -------------------- +Assignment computed by Houdini: + +Boogie program verifier finished with 2 verified, 0 errors +. +-------------------- test8.bpl -------------------- +Assignment computed by Houdini: + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index d0e53b08..40f8cea0 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -8,3 +8,9 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp echo -------------------- %%f -------------------- %BGEXE% %* /nologo /noinfer /contractInfer %%f ) + +for %%f in (test7.bpl test8.bpl) do ( + echo . + echo -------------------- %%f -------------------- + %BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f +) diff --git a/Test/houdini/test7.bpl b/Test/houdini/test7.bpl new file mode 100644 index 00000000..b5c6a4c6 --- /dev/null +++ b/Test/houdini/test7.bpl @@ -0,0 +1,15 @@ +var g: int; + +procedure main() +modifies g; +{ + g := 0; + call foo(); + assert g == 1; +} + +procedure foo() +modifies g; +{ + g := g + 1; +} \ No newline at end of file diff --git a/Test/houdini/test8.bpl b/Test/houdini/test8.bpl new file mode 100644 index 00000000..12eab481 --- /dev/null +++ b/Test/houdini/test8.bpl @@ -0,0 +1,21 @@ +var g: int; + +procedure main() +modifies g; +{ + g := 0; + call foo(); + assert g == 1; +} + +procedure {:inline 1} foo() +modifies g; +{ + call bar(); +} + +procedure bar() +modifies g; +{ + g := g + 1; +} \ No newline at end of file diff --git a/Test/inline/Answer b/Test/inline/Answer index d7e7edbe..6f63f1e3 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1439,197 +1439,6 @@ implementation bar() Boogie program verifier finished with 5 verified, 0 errors --------------------- test7.bpl -------------------- - -var g: int; - -procedure main(); - modifies g; - - - -implementation main() -{ - - anon0: - g := 0; - call foo(); - assert g == 1; - return; -} - - - -procedure foo(); - modifies g; - - - -implementation foo() -{ - - anon0: - g := g + 1; - return; -} - - -after inlining procedure calls -procedure main(); - modifies g; - - -implementation main() -{ - var inline$foo$0$g: int; - - anon0: - g := 0; - goto inline$foo$0$Entry; - - inline$foo$0$Entry: - inline$foo$0$g := g; - goto inline$foo$0$anon0; - - inline$foo$0$anon0: - g := g + 1; - goto inline$foo$0$Return; - - inline$foo$0$Return: - goto anon0$1; - - anon0$1: - assert g == 1; - return; -} - - - -Boogie program verifier finished with 2 verified, 0 errors --------------------- test8.bpl -------------------- - -var g: int; - -procedure main(); - modifies g; - - - -implementation main() -{ - - anon0: - g := 0; - call foo(); - assert g == 1; - return; -} - - - -procedure {:inline 1} foo(); - modifies g; - - - -implementation {:inline 1} foo() -{ - - anon0: - call bar(); - return; -} - - - -procedure bar(); - modifies g; - - - -implementation bar() -{ - - anon0: - g := g + 1; - return; -} - - -after inlining procedure calls -procedure main(); - modifies g; - - -implementation main() -{ - var inline$foo$0$g: int; - var inline$bar$0$g: int; - - anon0: - g := 0; - goto inline$foo$0$Entry; - - inline$foo$0$Entry: - inline$foo$0$g := g; - goto inline$foo$0$anon0; - - inline$foo$0$anon0: - goto inline$bar$0$Entry; - - inline$bar$0$Entry: - inline$bar$0$g := g; - goto inline$bar$0$anon0; - - inline$bar$0$anon0: - g := g + 1; - goto inline$bar$0$Return; - - inline$bar$0$Return: - goto inline$foo$0$anon0$1; - - inline$foo$0$anon0$1: - goto inline$foo$0$Return; - - inline$foo$0$Return: - goto anon0$1; - - anon0$1: - assert g == 1; - return; -} - - -after inlining procedure calls -procedure {:inline 1} foo(); - modifies g; - - -implementation {:inline 1} foo() -{ - var inline$bar$0$g: int; - - anon0: - goto inline$bar$0$Entry; - - inline$bar$0$Entry: - inline$bar$0$g := g; - goto inline$bar$0$anon0; - - inline$bar$0$anon0: - g := g + 1; - goto inline$bar$0$Return; - - inline$bar$0$Return: - goto anon0$1; - - anon0$1: - return; -} - - - -Boogie program verifier finished with 3 verified, 0 errors -------------------- test5.bpl -------------------- test5.bpl(37,3): Error BP5001: This assertion might not hold. Execution trace: diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index 3a8b0a9d..f56d55a0 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -13,11 +13,6 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do ( %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f ) -for %%f in (test7.bpl test8.bpl) do ( - echo -------------------- %%f -------------------- - %BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f -) - for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do ( echo -------------------- %%f -------------------- %BGEXE% %* %%f diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl deleted file mode 100644 index b5c6a4c6..00000000 --- a/Test/inline/test7.bpl +++ /dev/null @@ -1,15 +0,0 @@ -var g: int; - -procedure main() -modifies g; -{ - g := 0; - call foo(); - assert g == 1; -} - -procedure foo() -modifies g; -{ - g := g + 1; -} \ No newline at end of file diff --git a/Test/inline/test8.bpl b/Test/inline/test8.bpl deleted file mode 100644 index 12eab481..00000000 --- a/Test/inline/test8.bpl +++ /dev/null @@ -1,21 +0,0 @@ -var g: int; - -procedure main() -modifies g; -{ - g := 0; - call foo(); - assert g == 1; -} - -procedure {:inline 1} foo() -modifies g; -{ - call bar(); -} - -procedure bar() -modifies g; -{ - g := g + 1; -} \ No newline at end of file -- cgit v1.2.3