First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.

4 files changed, 65 insertions, 13 deletions

diff --git a/Source/VCExpr/NameClashResolver.ssc b/Source/VCExpr/NameClashResolver.ssc
index 28a974a6..9c281bf8 100644
--- a/Source/VCExpr/NameClashResolver.ssc
+++ b/Source/VCExpr/NameClashResolver.ssc
@@ -27,6 +27,7 @@ namespace Microsoft.Boogie.VCExprAST {
                                          as IDictionary<Object!, string!>);

       UsedNames = new Dictionary<string!, bool> ();

       CurrentCounters = new Dictionary<string!, int> ();

+      GlobalPlusLocalNames = new Dictionary<Object!, string!> ();

     }

 

     private UniqueNamer(UniqueNamer! namer) {

@@ -41,6 +42,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

       UsedNames = new Dictionary<string!, bool> (namer.UsedNames);

       CurrentCounters = new Dictionary<string!, int> (namer.CurrentCounters);

+      GlobalPlusLocalNames = new Dictionary<Object!, string!>(namer.GlobalPlusLocalNames);

     }

 

     public Object! Clone() {

@@ -56,6 +58,7 @@ namespace Microsoft.Boogie.VCExprAST {
     // (locally or globally)

     private readonly IDictionary<string!, bool>! UsedNames;

     private readonly IDictionary<string!, int>! CurrentCounters;

+    private readonly IDictionary<Object!, string!>! GlobalPlusLocalNames;

 

     ////////////////////////////////////////////////////////////////////////////

 

@@ -69,7 +72,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     ////////////////////////////////////////////////////////////////////////////

 

-    private string! NextFreeName(string! baseName) {

+    private string! NextFreeName(Object! thingie, string! baseName) {

       string! candidate;

       int counter;

 

@@ -89,6 +92,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

       UsedNames.Add(candidate, true);

       CurrentCounters[baseName] = counter;

+      GlobalPlusLocalNames[thingie] = candidate;

       return candidate;

     }

 

@@ -102,7 +106,7 @@ namespace Microsoft.Boogie.VCExprAST {
         return res;

 

       // if the object is not yet registered, create a name for it

-      res = NextFreeName(inherentName);

+      res = NextFreeName(thingie, inherentName);

       GlobalNames.Add(thingie, res);

 

       return res;

@@ -121,9 +125,13 @@ namespace Microsoft.Boogie.VCExprAST {
     } }

 

     public string! GetLocalName(Object! thingie, string! inherentName) {

-      string! res = NextFreeName(inherentName);

+      string! res = NextFreeName(thingie, inherentName);

       LocalNames[LocalNames.Count - 1][thingie] = res;

       return res;

     }

+    

+    public string! Lookup(Object! thingie) {

+      return GlobalPlusLocalNames[thingie];

+    }

   }

 }

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 7085bffe..d3729ab1 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -197,6 +197,13 @@ namespace Microsoft.Boogie.VCExprAST
       }

     }

 

+    private static string! TypeToStringHelper(Type! t) {

+      System.IO.StringWriter buffer = new System.IO.StringWriter();

+      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+        t.Emit(stream);

+      }

+      return buffer.ToString();

+    }

     public static string! TypeToString(Type! t) {

       if (t.IsBool)

         return "$bool";

@@ -204,17 +211,14 @@ namespace Microsoft.Boogie.VCExprAST
         return "$int";

       else if (t.IsBv)

         return "$bv" + t.BvBits;

+      else if (t.IsMap)

+        return TypeToStringHelper(t);

       else {

         // at this point, only the types U, T, and bitvector types should be left

         if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)

           return "U";

-        else {

-          System.IO.StringWriter buffer = new System.IO.StringWriter();

-          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

-            t.Emit(stream);

-          }

-          return buffer.ToString();

-        }

+        else

+          return TypeToStringHelper(t);

       }

     }

 

@@ -231,6 +235,16 @@ namespace Microsoft.Boogie.VCExprAST
       return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";

     }

 

+    public static string! StoreOpName(VCExprNAry! node)

+      requires node.Op is VCExprStoreOp; {

+      return "Store_" + TypeToString(node[0].Type);

+    }

+

+    public static string! SelectOpName(VCExprNAry! node)

+      requires node.Op is VCExprSelectOp; {

+      return "Select_" + TypeToString(node[0].Type);

+    }

+    

     internal void WriteId(string! s) {

       wr.Write(MakeIdPrintable(s));

     }

@@ -679,11 +693,23 @@ namespace Microsoft.Boogie.VCExprAST
       }

 

       public bool VisitSelectOp   (VCExprNAry! node, LineariserOptions! options) {

-        assert false;      // should not occur in the output

+        wr.Write("(" + SelectOpName(node) + " ");

+        ExprLineariser.Linearise(node[0], options);

+        wr.Write(" ");

+        ExprLineariser.Linearise(node[1], options);

+        wr.Write(")");

+        return true;

       }

 

       public bool VisitStoreOp    (VCExprNAry! node, LineariserOptions! options) {

-        assert false;       // should not occur in the output

+        wr.Write("(" + StoreOpName(node) + " ");

+        ExprLineariser.Linearise(node[0], options);

+        wr.Write(" ");

+        ExprLineariser.Linearise(node[1], options);

+        wr.Write(" ");

+        ExprLineariser.Linearise(node[2], options);

+        wr.Write(")");

+        return true;

       }

 

       public bool VisitBvOp       (VCExprNAry! node, LineariserOptions! options) {

diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index d41cb887..bbf9d16e 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -805,7 +805,7 @@ namespace Microsoft.Boogie.TypeErasure
     public VCExpr! Erase(VCExpr! expr, int polarity)

       requires polarity >= -1 && polarity <= 1; {

       this.Polarity = polarity;

-      return Mutate(expr, new VariableBindings ());

+      return Mutate(expr, new VariableBindings());

     }

 

     internal int Polarity = 1;  // 1 for positive, -1 for negative, 0 for both

diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc
index e08e6138..2b5003a6 100644
--- a/Source/VCExpr/VCExprAST.ssc
+++ b/Source/VCExpr/VCExprAST.ssc
@@ -24,6 +24,24 @@ namespace Microsoft.Boogie
     public static readonly VCExpr! False = new VCExprLiteral (Type.Bool);

     public static readonly VCExpr! True  = new VCExprLiteral (Type.Bool);

 

+    private Function ControlFlowFunction = null;

+    public VCExpr! ControlFlowFunctionApplication(VCExpr! e1, VCExpr! e2)

+    {

+      if (ControlFlowFunction == null) {

+        Formal! first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

+        Formal! second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

+        VariableSeq! inputs = new VariableSeq();

+        inputs.Add(first);

+        inputs.Add(second);

+        Formal! returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);

+        ControlFlowFunction = new Function(Token.NoToken, "ControlFlow", inputs, returnVar);

+      }

+      List<VCExpr!> args = new List<VCExpr!>();

+      args.Add(e1);

+      args.Add(e2);

+      return Function(BoogieFunctionOp(ControlFlowFunction), args);

+    }

+    

     public VCExpr! Integer(BigNum x) {

       return new VCExprIntLit(x);

     }