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.

1 files changed, 34 insertions, 6 deletions

diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc
index e70b332f..38aa6af8 100644
--- a/Source/VCGeneration/Wlp.ssc
+++ b/Source/VCGeneration/Wlp.ssc
@@ -8,12 +8,15 @@ using System.Collections;
 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Contracts;

+using System.Collections.Generic;

+using Microsoft.Basetypes;

 

 namespace VC {

   public class VCContext 

   {

     [Rep] public readonly Hashtable/*<int, Absy!>*/! Label2absy;

     [Rep] public readonly ProverContext! Ctxt;

+    public readonly Variable ControlFlowVariable;

     

     public VCContext(Hashtable/*<int, Absy!>*/! label2absy, ProverContext! ctxt)

     {

@@ -21,6 +24,13 @@ namespace VC {
       this.Ctxt = ctxt;

       // base();

     }

+    

+    public VCContext(Hashtable/*<int, Absy!>*/! label2absy, ProverContext! ctxt, Variable controlFlowVariable)

+    {

+      this.Label2absy = label2absy;

+      this.Ctxt = ctxt;

+      this.ControlFlowVariable = controlFlowVariable;

+    }

   }

 

   #region A class to compute wlp of a passive command program

@@ -41,7 +51,10 @@ namespace VC {
       int id = b.UniqueId;

       expose (ctxt) {

         ctxt.Label2absy[id] = b;

-        return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res);

+        if (ctxt.ControlFlowVariable != null)

+          return res;

+        else 

+          return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res);

       }

     }

 

@@ -73,11 +86,26 @@ namespace VC {
             default:

               assert false;  // unexpected case

           }

-// (MSchaef) Hack: This line might be useless, but at least it is not harmfull

-// need to test it

-        if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) return gen.Implies(C, N);

-      

-          return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N);

+          

+          // (MSchaef) Hack: This line might be useless, but at least it is not harmfull

+          // need to test it

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) 

+            return gen.Implies(C, N);

+          

+          if (ctxt.ControlFlowVariable != null)

+          {

+            VCExpr! controlFlowVariableExpr = 

+              ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

+            VCExpr! controlFlowFunctionAppl1 = 

+              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

+            VCExpr! controlFlowFunctionAppl2 = 

+              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

+            VCExpr! assertFailure = gen.Eq(controlFlowFunctionAppl1, gen.Integer(BigNum.FromInt(0)));

+            VCExpr! assertSuccess = gen.Neq(controlFlowFunctionAppl2, gen.Integer(BigNum.FromInt(0)));

+            return gen.And(gen.Implies(assertFailure, C), gen.Implies(assertSuccess, N));

+          }

+          else

+            return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N);

         }

 

       } else if (cmd is AssumeCmd) {