Added another option for lazy inlining based on macro expansion. This option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.

4 files changed, 43 insertions, 14 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 286f1036..179cba3c 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -439,7 +439,7 @@ namespace Microsoft.Boogie
             inline = true;

           }

         }

-        if (inline && !CommandLineOptions.Clo.LazyInlining) {

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

           foreach (Declaration d in TopLevelDeclarations) {

             Implementation impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 39ba0fb8..3645e7a3 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -225,7 +225,7 @@ namespace Microsoft.Boogie
     public enum Inlining { None, Assert, Assume, Spec };

     public Inlining ProcedureInlining = Inlining.Assume;

     public bool PrintInlined = false;

-    public bool LazyInlining = false;

+    public int LazyInlining = 0;

     

     public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };

     public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;

@@ -950,10 +950,16 @@ namespace Microsoft.Boogie
               switch (args[ps.i]) 

               {

                 case "0":

-                  LazyInlining = false;  

+                  LazyInlining = 0;  

                   break;

                 case "1":

-                  LazyInlining = true;  

+                  LazyInlining = 1;  

+                  break;

+                case "2":

+                  LazyInlining = 2;

+                  break;

+                default:

+                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

                   break;

               }

             }

@@ -1302,7 +1308,7 @@ namespace Microsoft.Boogie
         Monomorphize = true;

       }

       

-      if (LazyInlining) {

+      if (LazyInlining > 0) {

         TypeEncodingMethod = TypeEncoding.Monomorphic;

         UseArrayTheory = true;

         UseAbstractInterpretation = false;

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index f453d71d..b7f70145 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -113,10 +113,15 @@ namespace Microsoft.Boogie.Z3
       if (CommandLineOptions.Clo.PrintErrorModel >= 1 || 

           CommandLineOptions.Clo.EnhancedErrorMessages == 1 || 

           CommandLineOptions.Clo.ContractInfer ||

-          CommandLineOptions.Clo.LazyInlining) {

+          CommandLineOptions.Clo.LazyInlining > 0) {

         z3args += " " + OptionChar() + "m";

         expectingModel = true;

       }

+      if (CommandLineOptions.Clo.LazyInlining == 2) {

+        z3args += " " + OptionChar() + "nw";

+        AddOption(parms, "MACRO_EXPANSION", "true");

+      }

+      

       // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args

       if (opts.V1) {

         foreach (OptionValue opt in parms) {

@@ -595,7 +600,20 @@ namespace Microsoft.Boogie.Z3
         assume 0 <= j;

         string id = s.Substring(0, j);

         // id is stored into definedFunctions once the function definition for it has 

-        // been completely parsed, 

+        // been completely parsed. 

+        

+        if (s.IndexOf("-> {") < 0) 

+        {

+          // This function was a macro and we are not parsing its definition currently.

+          // Just move on to the next function.

+          while (true) 

+          {

+            s = FromReadLine();

+            if (0 <= s.IndexOf("{" + id + "}"))

+              break;

+          }

+          continue;

+        }

         

         // just ignore the "-> {" by dropping string s

         string zIDstring;

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index a866d047..f169e424 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -35,7 +35,7 @@ namespace VC
       this.logFilePath = logFilePath;

       implName2LazyInliningInfo = new Dictionary<string!, LazyInliningInfo!>();

       base(program);

-      if (CommandLineOptions.Clo.LazyInlining)

+      if (CommandLineOptions.Clo.LazyInlining > 0)

       {

         this.GenerateVCsForLazyInlining(program);

       }

@@ -211,22 +211,27 @@ namespace VC
       

       Function! function = (!)info.function;

       VCExpr! expr = gen.Function(function, interfaceExprs);

-      vcexpr = gen.Implies(expr, vcexpr);

+      if (CommandLineOptions.Clo.LazyInlining == 1) {

+        vcexpr = gen.Implies(expr, vcexpr);

+      } else {

+        assert CommandLineOptions.Clo.LazyInlining == 2;

+        vcexpr = gen.Eq(expr, vcexpr);

+      }

       

+      List<VCTrigger!> triggers = new List<VCTrigger!>();

       List<VCExpr!> exprs = new List<VCExpr!>();

       exprs.Add(expr);

       VCTrigger! trigger = new VCTrigger(true, exprs);

-      List<VCTrigger!> triggers = new List<VCTrigger!>();

       triggers.Add(trigger);

-      

-      interfaceExprVars.Reverse();

+        

       Expr e = new LiteralExpr(Token.NoToken, BigNum.FromInt(1));

       QKeyValue q = new QKeyValue(Token.NoToken, "weight", new List<object!>(new object![] { e }), null);

+      interfaceExprVars.Reverse();

       vcexpr = gen.Forall(new List<TypeVariable!>(), interfaceExprVars, triggers, 

                           new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);

-      checker.TheoremProver.PushVCExpression(vcexpr);

       

-      info.vcexpr = vcexpr;

+      info.vcexpr = vcexpr;     

+      checker.TheoremProver.PushVCExpression(vcexpr);

     }

     #endregion