fixed bug in the inlineDepth option for houdini

small clean up in the inlining implementation

9 files changed, 64 insertions, 232 deletions

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<string/*!*/, int>();

-      recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();

-      inlineDepth = CommandLineOptions.Clo.InlineDepth;

-      codeCopier = new CodeCopier();

-      inlineCallback = cb;

+    protected Inliner(InlineCallback cb, int inlineDepth) {

+      this.inlinedProcLblMap = new Dictionary<string/*!*/, int>();

+      this.recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();

+      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<Block/*!*/>/*!*/ newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);

+      List<Block> 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<Block/*!*/>/*!*/ DoInline(List<Block/*!*/>/*!*/ 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<List<Block>>()));

-      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<Implementation, HoudiniSession>(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<string, IdentifierExpr> CollectExistentialConstants() {

       Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();

       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/inline/test7.bpl b/Test/houdini/test7.bpl
index b5c6a4c6..b5c6a4c6 100644
--- a/Test/inline/test7.bpl
+++ b/Test/houdini/test7.bpl
diff --git a/Test/inline/test8.bpl b/Test/houdini/test8.bpl
index 12eab481..12eab481 100644
--- a/Test/inline/test8.bpl
+++ b/Test/houdini/test8.bpl
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