added the option /inlineDepth:n. This option defaults to -1. If the user provides a non-negative number then that number is used to inline

procedures not annotated by {:inline n} attribute.

7 files changed, 279 insertions, 29 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 5a1f8dc5..83e6009d 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -389,8 +389,8 @@ namespace Microsoft.Boogie {
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.LazyInlining == 0 &&

-          CommandLineOptions.Clo.StratifiedInlining == 0) {

+        if ((inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) ||

+            CommandLineOptions.Clo.InlineDepth >= 0) {

           foreach (Declaration d in TopLevelDeclarations) {

             Implementation impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ffccdc5..7d3fce84 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -143,6 +143,7 @@ namespace Microsoft.Boogie {
     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

+    public int InlineDepth = -1;

     public bool UseUncheckedContracts = false;

     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

@@ -949,7 +950,10 @@ namespace Microsoft.Boogie {
           case "/contractInfer":

             ContractInfer = true;

             break;

-

+          case "-inlineDepth":

+          case "/inlineDepth":

+            ps.GetNumericArgument(ref InlineDepth);

+            break;

           case "-subsumption":

           case "/subsumption": {

               int s = 0;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index d9c33bd4..a202bcfe 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -26,6 +26,8 @@ namespace Microsoft.Boogie {
 

     protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap;

 

+    protected int inlineDepth;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(codeCopier != null);

@@ -67,6 +69,7 @@ namespace Microsoft.Boogie {
     protected Inliner(InlineCallback cb) {

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

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

+      inlineDepth = CommandLineOptions.Clo.InlineDepth;

       codeCopier = new CodeCopier();

       inlineCallback = cb;

     }

@@ -159,6 +162,8 @@ namespace Microsoft.Boogie {
     // otherwise, the procedure is not inlined at the call site

     protected int GetInlineCount(Implementation impl) {

       Contract.Requires(impl != null);

+      Contract.Requires(impl.Proc != null);

+

       string/*!*/ procName = impl.Name;

       Contract.Assert(procName != null);

       int c;

@@ -169,9 +174,7 @@ namespace Microsoft.Boogie {
       c = -1; // TryGetValue above always overwrites c

       impl.CheckIntAttribute("inline", ref c);

       // procedure attribute overrides implementation

-      if (impl.Proc != null) {

-        impl.Proc.CheckIntAttribute("inline", ref c);

-      }

+      impl.Proc.CheckIntAttribute("inline", ref c);

 

       recursiveProcUnrollMap[procName] = c;

       return c;

@@ -194,9 +197,9 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private List<Block/*!*/>/*!*/ DoInlineBlocks(Stack<Procedure/*!*/>/*!*/ callStack, List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,

-                                         VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, ref bool inlinedSomething) {

-      Contract.Requires(cce.NonNullElements(callStack));

+    private List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,

+                                                 VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, 

+                                                 ref bool inlinedSomething) {

       Contract.Requires(cce.NonNullElements(blocks));

       Contract.Requires(program != null);

       Contract.Requires(newLocalVars != null);

@@ -204,7 +207,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>();

       

-

       foreach (Block block in blocks) {

         TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);

         CmdSeq cmds = block.Cmds;

@@ -223,14 +225,16 @@ namespace Microsoft.Boogie {
           } else {

             Contract.Assert(callCmd.Proc != null);

             Procedure proc = callCmd.Proc;

-            int inline = -1;

 

             Implementation impl = FindProcImpl(program, proc);

-            if (impl != null) {

-              inline = GetInlineCount(impl);

+            if (impl == null) {

+              newCmds.Add(codeCopier.CopyCmd(cmd));

+              continue;

             }

+          

+            int inline = GetInlineCount(impl);

 

-            if (inline > 0) { // at least one block should exist

+            if (inline > 0 || (inline == -1 && inlineDepth > 0)) { // at least one block should exist

               Contract.Assume(impl != null);

               Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);

               inlinedSomething = true;

@@ -247,18 +251,24 @@ namespace Microsoft.Boogie {
               // increment the counter for the procedure to be used in constructing the locals and formals

               NextInlinedProcLabel(proc.Name);

 

-              BeginInline(newLocalVars, newModifies, proc, impl);

+              BeginInline(newLocalVars, newModifies, impl);

 

-              List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);

+              List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel);

               Contract.Assert(cce.NonNullElements(inlinedBlocks));

 

               EndInline();

 

-              recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;

-              callStack.Push(cce.NonNull(impl.Proc));

-              inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);

-              callStack.Pop();

-              recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;

+              if (inline > 0)

+                recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;

+              else

+                inlineDepth = inlineDepth - 1;

+

+              inlinedBlocks = DoInlineBlocks(inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);

+

+              if (inline > 0)

+                recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;

+              else

+                inlineDepth = inlineDepth + 1;

 

               Block/*!*/ startBlock = inlinedBlocks[0];

               Contract.Assert(startBlock != null);

@@ -271,7 +281,7 @@ namespace Microsoft.Boogie {
 

               lblCount = nextlblCount;

               newCmds = new CmdSeq();

-            } else if (inline == 0) {

+            } else if (inline == 0 || (inline == -1 && inlineDepth == 0)) {

               inlinedSomething = true;

               if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {

                 // add assert

@@ -304,17 +314,20 @@ namespace Microsoft.Boogie {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       inlinedProcLblMap.Clear();

       recursiveProcUnrollMap.Clear();

+      inlineDepth = CommandLineOptions.Clo.InlineDepth;

 

       inlined = false;

-      return DoInlineBlocks(new Stack<Procedure/*!*/>(), blocks, program, newLocalVars, newModifies, ref inlined);

+      return DoInlineBlocks(blocks, program, newLocalVars, newModifies, ref inlined);

     }

 

-    protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Procedure proc, Implementation impl) {

+    protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) {

       Contract.Requires(impl != null);

-      Contract.Requires(proc != null);

+      Contract.Requires(impl.Proc != null);

       Contract.Requires(newModifies != null);

       Contract.Requires(newLocalVars != null);

+      

       Hashtable substMap = new Hashtable();

+      Procedure proc = impl.Proc;

 

       foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {

         Contract.Assert(locVar != null);

@@ -377,18 +390,19 @@ namespace Microsoft.Boogie {
 

 

     // result[0] is the entry block

-    protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Procedure proc, Implementation impl, string nextBlockLabel) {

+    protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {

       Contract.Requires(nextBlockLabel != null);

       Contract.Requires(impl != null);

-      Contract.Requires(proc != null);

+      Contract.Requires(impl.Proc != null);

       Contract.Requires(callCmd != null);

-      Contract.Requires(((codeCopier.Subst != null)));

+      Contract.Requires(codeCopier.Subst != null);

 

-      Contract.Requires((codeCopier.OldSubst != null));

+      Contract.Requires(codeCopier.OldSubst != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       List<Block/*!*/>/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);

       Contract.Assert(implBlocks.Count > 0);

 

+      Procedure proc = impl.Proc;

       string startLabel = implBlocks[0].Label;

 

       List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();

diff --git a/Test/inline/Answer b/Test/inline/Answer
index ae632f79..2c29ab0b 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1439,6 +1439,197 @@ 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 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 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 f56d55a0..3a8b0a9d 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -13,6 +13,11 @@ 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
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/inline/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/inline/test8.bpl b/Test/inline/test8.bpl
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/inline/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