Boogie: Added stratified inlining. It is enabled using the flag /stratifiedInline:1.

16 files changed, 1256 insertions, 9 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index dda05546..e6b83a61 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -42,57 +42,133 @@ EndProject
 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

+		Debug|Any CPU = Debug|Any CPU

+		Debug|Mixed Platforms = Debug|Mixed Platforms

 		Release|.NET = Release|.NET

+		Release|Any CPU = Release|Any CPU

+		Release|Mixed Platforms = Release|Mixed Platforms

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET

 		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{F75666DE-CD56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET

 		{F75666DE-CD56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{F75666DE-CD56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET

 		{F75666DE-CD56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{F75666DE-CD56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.ActiveCfg = Debug|.NET

 		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.Build.0 = Debug|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|.NET.ActiveCfg = Release|.NET

 		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|.NET.Build.0 = Release|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Any CPU.ActiveCfg = Release|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{13C3A68C-462A-4CDA-A480-738046E37C5A}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Debug|.NET.ActiveCfg = Debug|.NET

 		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Debug|.NET.Build.0 = Debug|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Release|.NET.ActiveCfg = Release|.NET

 		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Release|.NET.Build.0 = Release|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Release|Any CPU.ActiveCfg = Release|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{11D06232-2039-4BCA-853B-C596E2A4EDB0}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.ActiveCfg = Debug|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.Build.0 = Debug|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Release|.NET.ActiveCfg = Release|.NET

 		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Release|.NET.Build.0 = Release|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Release|Any CPU.ActiveCfg = Release|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Debug|.NET.ActiveCfg = Debug|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Debug|.NET.Build.0 = Debug|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|.NET.ActiveCfg = Release|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|.NET.Build.0 = Release|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Any CPU.ActiveCfg = Release|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{47BC34F1-A173-40BE-84C2-9332B4418387}.Debug|.NET.ActiveCfg = Debug|.NET

 		{47BC34F1-A173-40BE-84C2-9332B4418387}.Debug|.NET.Build.0 = Debug|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{47BC34F1-A173-40BE-84C2-9332B4418387}.Release|.NET.ActiveCfg = Release|.NET

 		{47BC34F1-A173-40BE-84C2-9332B4418387}.Release|.NET.Build.0 = Release|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Release|Any CPU.ActiveCfg = Release|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{47BC34F1-A173-40BE-84C2-9332B4418387}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.ActiveCfg = Debug|.NET

 		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.Build.0 = Debug|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.ActiveCfg = Release|.NET

 		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.Build.0 = Release|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Any CPU.ActiveCfg = Release|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Debug|.NET.ActiveCfg = Debug|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Debug|.NET.Build.0 = Debug|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|.NET.ActiveCfg = Release|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|.NET.Build.0 = Release|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Any CPU.ActiveCfg = Release|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET

 		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET

 		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|.NET.ActiveCfg = Debug|.NET

 		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|.NET.Build.0 = Debug|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|.NET.ActiveCfg = Release|.NET

 		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|.NET.Build.0 = Release|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|Any CPU.ActiveCfg = Release|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|.NET.ActiveCfg = Debug|.NET

 		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|.NET.Build.0 = Debug|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|Any CPU.ActiveCfg = Debug|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|Mixed Platforms.Build.0 = Debug|.NET

 		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|.NET.ActiveCfg = Release|.NET

 		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|.NET.Build.0 = Release|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|Any CPU.ActiveCfg = Release|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|Mixed Platforms.ActiveCfg = Release|.NET

+		{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|Mixed Platforms.Build.0 = Release|.NET

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 62cd0593..ff901532 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -227,6 +227,7 @@ namespace Microsoft.Boogie
     public Inlining ProcedureInlining = Inlining.Assume;

     public bool PrintInlined = false;

     public int LazyInlining = 0;

+    public int StratifiedInlining = 0;

     

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

     public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;

@@ -974,6 +975,23 @@ namespace Microsoft.Boogie
               }

             }

             break;

+          case "-stratifiedInline":

+          case "/stratifiedInline":

+            if (ps.ConfirmArgumentCount(1)) {

+              switch (args[ps.i]) 

+              {

+                case "0":

+                  StratifiedInlining = 0;  

+                  break;

+                case "1":

+                  StratifiedInlining = 1;  

+                  break;

+                default:

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

+                  break;

+              }

+            }

+            break;            

           case "-typeEncoding":

           case "/typeEncoding":

             if (ps.ConfirmArgumentCount(1)) {

@@ -1323,6 +1341,12 @@ namespace Microsoft.Boogie
         UseArrayTheory = true;

         UseAbstractInterpretation = false;

       }

+      

+      if (StratifiedInlining > 0) {

+        TypeEncodingMethod = TypeEncoding.Monomorphic;

+        UseArrayTheory = true;

+        UseAbstractInterpretation = false;

+      }

     }

 

 

diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
index bd618c24..2a50adee 100644
--- a/Source/Provers/Simplify/ProverInterface.ssc
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -156,9 +156,11 @@ namespace Microsoft.Boogie.Simplify
 

     protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator();

 

-    protected void FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

+    // Return the number of axioms pushed to the theorem prover

+    protected int FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

       if (thmProver == null)

-        return;

+        return 0;

+      int ret = 0;

       foreach (string! s in vcExprTranslator.NewTypeDecls) {

         LogCommon(s);

         thmProver.Feed(s, 0);

@@ -166,7 +168,9 @@ namespace Microsoft.Boogie.Simplify
       foreach (string! s in vcExprTranslator.NewAxioms) {

         LogBgPush(s);

         thmProver.AddAxioms(s);

+        ret ++;

       }

+      return ret;

     }

 

     protected static string! CodebaseString() {

@@ -278,6 +282,32 @@ namespace Microsoft.Boogie.Simplify
     {

       vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) ); 

     }

+    

+    public override string! VCExpressionToString(VCExpr! vc)

+    {

+      return vcExprTranslator.translate(vc, 1);

+    }

+    

+    // Number of axioms pushed since the last call to Check

+    public override int NumAxiomsPushed() 

+    {

+       return vcExprTranslator.NewAxiomsCount;

+    }

+    

+    // Feed the axioms pushed since the last call to Check to the theorem prover

+    public override int FlushAxiomsToTheoremProver() 

+      throws UnexpectedProverOutputException;

+    {

+       return FeedNewAxiomsDecls2Prover();

+    }

+

+    public override void Pop() 

+      throws UnexpectedProverOutputException;

+    {

+       assert thmProver != null;

+       LogCommon("(BG_POP)");

+       thmProver.PopAxioms();

+    }

 

     [NoDefaultContract]  // important, since we have no idea what state the object might be in when this handler is invoked

     void ControlCHandler(object o, ConsoleCancelEventArgs a)

@@ -316,13 +346,24 @@ namespace Microsoft.Boogie.Simplify
 

         Helpers.ExtraTraceInformation("Sending data to theorem prover");

 

-        FeedNewAxiomsDecls2Prover();

+        int num_axioms_pushed = 

+           FeedNewAxiomsDecls2Prover();

+        

         string! prelude = ctx.GetProverCommands(false);

         vcString = prelude + vcString;

         LogActivity(vcString);

 

         assert thmProver != null;

         thmProver.BeginCheck(descriptiveName, vcString);

+        

+        if(CommandLineOptions.Clo.StratifiedInlining > 0) {

+			// Pop all the axioms that were pushed by FeedNewAxiomsDecls2Prover

+			for(int i = 0; i < num_axioms_pushed; i++) 

+			{

+			   LogBgPop();

+			   thmProver.PopAxioms();

+			}

+        }

 

         if (CommandLineOptions.Clo.RestartProverPerVC) {

           LogComment("Will restart the prover due to /restartProver option");

@@ -418,6 +459,10 @@ namespace Microsoft.Boogie.Simplify
       LogCommon(")");

     }

 

+    public void LogBgPop() {

+      LogCommon("(BG_POP)");

+    }

+    

     [NoDefaultContract]

     private void FireUpNewProver()

       requires IsExposed;

@@ -525,6 +570,11 @@ namespace Microsoft.Boogie.Simplify
     public readonly List<string!>! AllAxioms;

     private List<string!>! NewAxiomsAttr;

 

+    // The length of the list NewAxiomsAttr

+    public int NewAxiomsCount { get {

+      return NewAxiomsAttr.Count;

+    } }

+

     public List<string!>! NewAxioms { get {

       List<string!>! res = NewAxiomsAttr;

       NewAxiomsAttr = new List<string!> ();

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index 1278fc7d..dbf23a8a 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -116,7 +116,8 @@ namespace Microsoft.Boogie.Z3
       if (CommandLineOptions.Clo.PrintErrorModel >= 1 || 

           CommandLineOptions.Clo.EnhancedErrorMessages == 1 || 

           CommandLineOptions.Clo.ContractInfer ||

-          CommandLineOptions.Clo.LazyInlining > 0) {

+          CommandLineOptions.Clo.LazyInlining > 0 ||

+          CommandLineOptions.Clo.StratifiedInlining > 0) {

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

         expectingModel = true;

       }

diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc
index 0ccbd843..4bd6edea 100644
--- a/Source/VCGeneration/Check.ssc
+++ b/Source/VCGeneration/Check.ssc
@@ -469,7 +469,17 @@ namespace Microsoft.Boogie
     /// testing

     /// </summary>    

     public virtual void PushVCExpression(VCExpr! vc) {}

+    public virtual string! VCExpressionToString(VCExpr! vc) { return ""; }

+    public virtual void Pop() 

+      throws UnexpectedProverOutputException;

+    {}

+    public virtual int NumAxiomsPushed() 

+    { return 0; }

+    public virtual int FlushAxiomsToTheoremProver() 

+      throws UnexpectedProverOutputException;

+    { return 0; }

     

+        

     public abstract ProverContext! Context { get; }

     public abstract VCExpressionGenerator! VCExprGen { get; }

   }

diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index 6e87fd0e..a2db980d 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -253,10 +253,33 @@ namespace VC
       Helpers.ExtraTraceInformation("Finished implementation verification");

       return outcome;

     }

-  

+

+    public Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, out List<Counterexample!>? errors)

+      ensures result == Outcome.Errors ==> errors != null;

+      throws UnexpectedProverOutputException;

+    {

+      Helpers.ExtraTraceInformation("Starting implementation verification");

+

+      CounterexampleCollector collector = new CounterexampleCollector();

+      Outcome outcome = StratifiedVerifyImplementation(impl, program, collector);

+      if (outcome == Outcome.Errors) {

+        errors = collector.examples;

+      } else {

+        errors = null;

+      }

+

+      Helpers.ExtraTraceInformation("Finished implementation verification");

+      return outcome;

+    }

+      

     public abstract Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)

         throws UnexpectedProverOutputException;

-        

+    

+    public virtual Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)

+        throws UnexpectedProverOutputException;

+    {

+       return VerifyImplementation(impl, program, callback);

+    }    

 

 /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////

 

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index f169e424..f5a57cf6 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -34,11 +34,16 @@ namespace VC
       this.appendLogFile = appendLogFile;

       this.logFilePath = logFilePath;

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

+      implName2StratifiedInliningInfo = new Dictionary<string!, StratifiedInliningInfo!>();

       base(program);

       if (CommandLineOptions.Clo.LazyInlining > 0)

       {

         this.GenerateVCsForLazyInlining(program);

       }

+      if (CommandLineOptions.Clo.StratifiedInlining > 0)

+      {

+        this.GenerateVCsForStratifiedInlining(program);

+      }

       // base();

     }

 

@@ -63,7 +68,7 @@ namespace VC
 

       return new AssumeCmd(assrt.tok, expr);

     }

-    

+        

     #region LazyInlining

     public class LazyInliningInfo {

       public Implementation! impl;

@@ -234,6 +239,140 @@ namespace VC
       checker.TheoremProver.PushVCExpression(vcexpr);

     }

     #endregion

+

+    #region StratifiedInlining

+    public class StratifiedInliningInfo : LazyInliningInfo 

+    {

+      public int inline_cnt;

+      public List<VCExprVar!>! privateVars;

+      public List<VCExprVar!>! interfaceExprVars;

+      public VCExpr funcExpr;

+      public VCExpr falseExpr;

+      

+      public StratifiedInliningInfo(Implementation! impl, Program! program, int uniqueid)

+        : base(impl, program, uniqueid)

+      {

+         inline_cnt = 0;

+         privateVars = new List<VCExprVar!>();

+         interfaceExprVars = new List<VCExprVar!>();

+      }

+    

+    }

+    

+    private Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;

+    

+    public void GenerateVCsForStratifiedInlining(Program! program)

+    {

+      Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

+      foreach (Declaration! decl in program.TopLevelDeclarations)

+      {

+        Implementation impl = decl as Implementation;

+        if (impl == null) continue;

+        Procedure! proc = (!)impl.Proc;

+        if (proc.FindExprAttribute("inline") != null) {

+          StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId());

+          implName2StratifiedInliningInfo[impl.Name] = info;

+          // We don't need controlFlowVariable for stratified Inlining

+          //impl.LocVars.Add(info.controlFlowVariable);

+          ExprSeq! exprs = new ExprSeq();

+          foreach (Variable! v in program.GlobalVariables())

+          {

+            exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

+          }

+          foreach (Variable! v in proc.InParams)

+          {

+            exprs.Add(new IdentifierExpr(Token.NoToken, v));

+          }

+          foreach (Variable! v in proc.OutParams)

+          {

+            exprs.Add(new IdentifierExpr(Token.NoToken, v)); 

+          }

+          foreach (IdentifierExpr! ie in proc.Modifies)

+          {

+            if (ie.Decl == null) continue;

+            exprs.Add(ie);

+          }

+          Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);

+          proc.Ensures.Add(new Ensures(true, freePostExpr));

+        }

+      }

+      

+      foreach (StratifiedInliningInfo! info in implName2StratifiedInliningInfo.Values)

+      {

+        GenerateVCForStratifiedInlining(program, info, checker);

+      }

+    }

+    

+    private void GenerateVCForStratifiedInlining(Program! program, StratifiedInliningInfo! info, Checker! checker)

+    requires info.impl != null;

+    requires info.impl.Proc != null;

+    {

+      Implementation! impl = info.impl;

+      ConvertCFG2DAG(impl, program);

+      info.gotoCmdOrigins = PassifyImpl(impl, program);

+      assert info.exitIncarnationMap != null;

+      Hashtable/*<int, Absy!>*/! label2absy;

+      VCExpressionGenerator! gen = checker.VCExprGen;

+      VCExpr! vcexpr = gen.Not(GenerateVC(impl, null, out label2absy, checker));

+      info.label2absy = label2absy;

+      

+      Boogie2VCExprTranslator! translator = checker.TheoremProver.Context.BoogieExprTranslator; 

+      info.privateVars = new List<VCExprVar!>();

+      foreach (Variable! v in impl.LocVars)

+      {

+        info.privateVars.Add(translator.LookupVariable(v));

+      }

+      foreach (Variable! v in impl.OutParams)

+      {

+        info.privateVars.Add(translator.LookupVariable(v));

+      }

+      

+      info.interfaceExprVars = new List<VCExprVar!>();

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

+      foreach (Variable! v in info.interfaceVars)

+      {

+        VCExprVar! ev = translator.LookupVariable(v);

+        info.interfaceExprVars.Add(ev);

+        interfaceExprs.Add(ev);

+      }

+      

+      Function! function = (!)info.function;

+      info.funcExpr = gen.Function(function, interfaceExprs);

+      info.vcexpr = vcexpr; 

+      

+      // Build the "false" expression: forall a b c: foo(a,b,c) <==> false

+      

+      info.falseExpr = gen.Eq(info.funcExpr, VCExpressionGenerator.False);

+      

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

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

+      exprs.Add(info.funcExpr);

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

+      triggers.Add(trigger);

+        

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

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

+      //info.interfaceExprVars.Reverse();

+      info.falseExpr = gen.Forall(new List<TypeVariable!>(), info.interfaceExprVars, triggers, 

+                                  new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), info.falseExpr);

+          

+      //checker.TheoremProver.PushVCExpression(vcexpr);

+      /*

+      Console.WriteLine("Procedure: {0}", info.impl.Name);

+      Console.Write("For all: ");

+      foreach(VCExprVar! v in info.interfaceExprVars) {

+         Console.Write(v.ToString() + " ");

+      }

+      Console.WriteLine();

+      Console.Write("There exists: ");

+      foreach(VCExprVar! v in info.privateVars) {

+         Console.Write(v.ToString() + " ");

+      }

+      Console.WriteLine();

+      Console.WriteLine(vcexpr.ToString());

+      */

+    }    

+    #endregion

     

     #region Soundness smoke tester

     class SmokeTester

@@ -1361,6 +1500,10 @@ namespace VC
       if (impl.SkipVerification) {

         return Outcome.Inconclusive; // not sure about this one

       } 

+      

+      if (CommandLineOptions.Clo.StratifiedInlining > 0) {

+        return StratifiedVerifyImplementation(impl, program, callback);

+      }

 

       callback.OnProgress("VCgen", 0, 0, 0.0);

 

@@ -1514,6 +1657,445 @@ namespace VC
       return outcome;

     }

 

+    public override Outcome StratifiedVerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)

+      throws UnexpectedProverOutputException;

+    {      

+       // Get the checker

+       Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

+

+       // Get the VC of the current procedure

+       VCExpr! vc;

+       StratifiedInliningErrorReporter! reporter;

+       Hashtable/*<int, Absy!>*/! mainLabel2absy;

+       GetVC(impl, program, callback, out vc, out mainLabel2absy, out reporter);

+       

+       // Find all procedure calls in vc and put labels on them      

+       FCallHandler calls = new FCallHandler(checker.VCExprGen, implName2StratifiedInliningInfo, mainLabel2absy);

+       calls.setCurrProcAsMain();

+       vc = calls.Mutate(vc, true);

+       reporter.SetCandidateHandler(calls);

+       

+       Outcome ret = Outcome.Correct;

+       

+       int expansionCount = 0;

+       int total_axioms_pushed = 0;

+       

+       /*

+       // Do eager inlining

+       while(calls.currCandidates.Count != 0) 

+       {

+          List<int>! toExpand = new List<int>();

+          foreach(int id in calls.currCandidates) {

+            toExpand.Add(id);

+          }

+          expansionCount += toExpand.Count;

+          total_axioms_pushed +=

+            DoExpansion(toExpand, calls, checker);

+       }

+       */

+       

+       int cnt = 0;

+       while(cnt < 500) {

+           cnt ++;

+

+		   // Push "false"

+		   checker.TheoremProver.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");

+		   

+		   int prev_axioms_pushed = checker.TheoremProver.NumAxiomsPushed();

+		   

+		   foreach(int id in calls.currCandidates) {

+		      VCExprNAry! vce = calls.id2Candidate[id];

+			  VCExpr! falseExpr = checker.VCExprGen.Eq(vce, VCExpressionGenerator.False);

+			  checker.TheoremProver.PushVCExpression(falseExpr);

+		   }

+	       int axioms_pushed = checker.TheoremProver.NumAxiomsPushed();

+	       

+	       // Note: axioms_pushed may not be the same as calls.currCandidates.Count 

+	       // because PushVCExpression pushes other stuff too (which always seems 

+	       // to be TRUE)

+	       

+		   reporter.underapproximationMode = true;

+	       

+	       // Check!

+		   //Console.Write("Checking with preds == false: "); Console.Out.Flush();

+		   ret = CheckVC(vc, reporter, checker, impl.Name);

+		   //Console.WriteLine(ret.ToString());

+	       

+		   // Pop

+		   for(int i = 0; i < axioms_pushed - prev_axioms_pushed; i++) {

+			  checker.TheoremProver.Pop();

+		   }

+		   	       

+	       checker.TheoremProver.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");

+		   

+		   if(ret == Outcome.Errors) {

+			 break;

+		   }	

+		          

+	       // If we didn't underapproximate, then we're done

+	       if(calls.currCandidates.Count == 0) {

+	          break;

+	       }

+	       

+	       checker.TheoremProver.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");

+		   // Push "true" (No-op)

+		   // Check

+		   reporter.underapproximationMode = false;

+	       

+		   //Console.Write("Checking with preds == true: "); Console.Out.Flush();

+		   ret = CheckVC(vc, reporter, checker, impl.Name);  

+		   //Console.WriteLine(ret.ToString());

+	       

+		   if(ret == Outcome.Correct) {

+			  break;

+		   }

+	       

+	       checker.TheoremProver.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");

+	       

+	       checker.TheoremProver.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");

+	       

+		   // Look at the errors to see what to inline

+		   assert reporter.candidatesToExpand.Count != 0;

+	       

+	       expansionCount += reporter.candidatesToExpand.Count;

+	       total_axioms_pushed +=

+	         DoExpansion(reporter.candidatesToExpand, calls, checker);

+

+		   checker.TheoremProver.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");

+	   }

+       

+       // Pop off everything that we pushed so that there are no side effects from

+       // this call to VerifyImplementation

+       for(int i = 0; i < total_axioms_pushed; i++) {

+	      checker.TheoremProver.Pop();

+	   }

+		   

+       if(cnt == 500) 

+       {

+          checker.TheoremProver.LogComment("Stratified Inlining: timeout");

+       }

+       

+       checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Calls to Z3: {0}", 2*cnt));

+       checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Expansions performed: {0}", expansionCount));

+       checker.TheoremProver.LogComment(string.Format("Stratified Inlining: Candidates left: {0}", calls.currCandidates.Count));

+       

+       return ret;

+    }

+    

+    // A counter for adding new variables

+    static int newVarCnt = 0;     

+    

+    // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.

+    // Returns the number of axioms pushed.

+    private int DoExpansion(List<int>! candidates,

+                             FCallHandler! calls, Checker! checker) 

+      throws UnexpectedProverOutputException;

+    {       

+       int old_axioms_pushed = checker.TheoremProver.NumAxiomsPushed();

+	   foreach(int id in candidates) {

+	      VCExprNAry! expr = calls.id2Candidate[id];

+		  string procName = ((!)(expr.Op as VCExprBoogieFunctionOp)).Func.Name;

+		  if(!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;

+          

+          //Console.WriteLine("Expanding: {0}", expr.ToString());

+          

+		  StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];

+		  VCExpr! expansion = (!)info.vcexpr;

+          

+		  // Instantiate the "forall" variables

+		  Dictionary<VCExprVar!, VCExpr!>! substForallDict = new Dictionary<VCExprVar!, VCExpr!>();

+		  assert info.interfaceExprVars.Count == expr.Length;

+		  for(int i = 0; i < info.interfaceExprVars.Count; i++) {

+			substForallDict.Add(info.interfaceExprVars[i], expr[i]);

+		  }

+		  VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable!, Microsoft.Boogie.Type!>());

+          

+		  SubstitutingVCExprVisitor! subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

+		  expansion = subst.Mutate(expansion, substForall);

+          

+		  // Instantiate and declare the "exists" variables

+		  Dictionary<VCExprVar!, VCExpr!>! substExistsDict = new Dictionary<VCExprVar!, VCExpr!>();

+		  for(int i = 0; i < info.privateVars.Count; i++) {

+		     VCExprVar! v = info.privateVars[i];

+		     string newName = v.Name + "_si_" + newVarCnt.ToString();

+		     newVarCnt ++;

+			 checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

+			 substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type));

+		  }

+		  VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable!, Microsoft.Boogie.Type!>());

+          

+		  subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

+		  expansion = subst.Mutate(expansion, substExists);

+

+		  if(!calls.currCandidates.Contains(id)) {

+		    Console.WriteLine("Don't know what we just expanded");

+		  }

+		  

+		  calls.currCandidates.Remove(id);

+		  

+		  // Record the new set of candidates and rename absy labels

+		  calls.currInlineCount = id;

+		  calls.setCurrProc(procName);

+		  expansion = calls.Mutate(expansion, true);

+		  

+		  expansion = checker.VCExprGen.Eq(expr, expansion);

+		  checker.TheoremProver.PushVCExpression(expansion);

+		  

+	    }

+	    int axioms_pushed = checker.TheoremProver.NumAxiomsPushed() - old_axioms_pushed;

+	    checker.TheoremProver.FlushAxiomsToTheoremProver();

+	    return axioms_pushed;

+    }

+    

+    // Return the VC for the impl (don't pass it to the theorem prover).

+    // GetVC is a cheap imitation of VerifyImplementatio, except that the VC is not passed to the theorem prover.

+    private void GetVC(Implementation! impl, Program! program, VerifierCallback! callback, out VCExpr! vc, out Hashtable/*<int, Absy!>*/! label2absy, out StratifiedInliningErrorReporter! reporter) 

+    {

+      ConvertCFG2DAG(impl, program);

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);

+      Checker! checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime);

+      

+      vc = GenerateVC(impl, null, out label2absy, checker);

+      

+      /*

+      ErrorReporter errReporter;

+      if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

+        errReporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);

+      } else {

+        errReporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, (DeclFreeProverContext!) checker.TheoremProver.Context, program);

+      }

+      */

+      

+      reporter = new StratifiedInliningErrorReporter(

+         (!)implName2StratifiedInliningInfo, checker.TheoremProver, callback, 

+         (DeclFreeProverContext)checker.TheoremProver.Context, gotoCmdOrigins, program, impl);

+

+    }

+    

+    private Outcome CheckVC(VCExpr! vc, StratifiedInliningErrorReporter! reporter, Checker! checker, string! implName)

+      throws UnexpectedProverOutputException;

+    {

+       checker.TheoremProver.FlushAxiomsToTheoremProver();

+       checker.BeginCheck(implName, vc, reporter);

+       checker.ProverDone.WaitOne();

+

+       ProverInterface.Outcome outcome = (checker).ReadOutcome();

+       

+       switch (outcome) {

+         case ProverInterface.Outcome.Valid:

+            return Outcome.Correct;

+         case ProverInterface.Outcome.Invalid:

+            return Outcome.Errors;

+         case ProverInterface.Outcome.OutOfMemory:

+            return Outcome.OutOfMemory;

+         case ProverInterface.Outcome.TimeOut:

+            return Outcome.TimedOut;

+         case ProverInterface.Outcome.Undetermined:

+            return Outcome.Inconclusive;

+          default:

+            assert false;

+        }

+       

+    }

+

+    /*

+    // Collects all function calls in the VCExpr

+    public class FCallCollector : TraversingVCExprVisitor<bool, bool> {

+      Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;

+      public List<VCExprNAry!>! fcalls;

+      

+      public FCallCollector(Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo) {

+        this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;

+        fcalls = new List<VCExprNAry!>();

+      }

+      

+      protected override bool StandardResult(VCExpr! node, bool arg) {

+        VCExprNAry vnary = node as VCExprNAry;

+        if(vnary == null) return true;

+        VCExprBoogieFunctionOp bop = vnary.Op as VCExprBoogieFunctionOp;

+        if(bop == null) return true;  

+        if(implName2StratifiedInliningInfo.ContainsKey(bop.Func.Name)) {

+           fcalls.Add(vnary);

+        }

+        return true;

+      }

+      

+    }

+    */

+

+    // This class is used to traverse VCs and do the following:

+    // -- collect the set of FunctionCall nodes and label them with a unique string

+    // -- Rename all other labels (so that calling this on the same VC results in 

+    //    VCs with different labels each time)

+    public class FCallHandler : MutatingVCExprVisitor<bool> {

+      Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;

+      public readonly Hashtable/*<int, Absy!>*/! mainLabel2absy;

+      public Dictionary<NAryExpr!, int>! boogieExpr2Id;

+      public Dictionary<int, VCExprNAry!>! id2Candidate;

+      public Dictionary<VCExprNAry!, int>! candidate2Id;

+      public Dictionary<string!, int>! label2Id;

+      public Microsoft.SpecSharp.Collections.Set<int> currCandidates;

+

+      // Name of the procedure who's VC we're mutating

+      string currProc;

+      

+      // The 0^th candidate is main

+      static int candidateCount = 1;

+      public int currInlineCount;

+      

+      public FCallHandler(VCExpressionGenerator! gen, 

+                            Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo,

+                            Hashtable/*<int, Absy!>*/! mainLabel2absy) 

+        : base(gen) 

+      {

+        this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;

+        this.mainLabel2absy = mainLabel2absy;

+        id2Candidate = new Dictionary<int, VCExprNAry!>();

+        candidate2Id = new Dictionary<VCExprNAry!, int>();

+        boogieExpr2Id = new Dictionary<NAryExpr!, int>();

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

+        currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();

+        currInlineCount = 0;

+        currProc = null;

+      }

+      

+      public void Clear() 

+      {

+        currCandidates = new Microsoft.SpecSharp.Collections.Set<int>();

+      }

+      

+      private int GetId(VCExprNAry! vc) 

+      {

+         if(candidate2Id.ContainsKey(vc))

+           return candidate2Id[vc];

+         

+         

+         int id = candidateCount;

+         candidate2Id[vc] = id;

+         id2Candidate[id] = vc;

+         

+         candidateCount ++;

+         currCandidates.Add(id);

+         

+         return id;

+      }

+      

+      private string! GetLabel(int id) 

+      {

+         string! ret = "si_fcall_" + id.ToString();

+         if(!label2Id.ContainsKey(ret))

+           label2Id[ret] = id;

+         

+         return ret;

+      }

+      

+      public int GetId(string! label) 

+      {

+         if(!label2Id.ContainsKey(label)) return -1;

+         return label2Id[label];

+      }

+      

+      public string! RenameAbsyLabel(string !label) 

+        requires label.Length >= 1;

+      {

+         // Remove the sign from the label

+         string! nosign = label.Substring(1);

+         return "si_inline_" + currInlineCount.ToString() + "_" + nosign;

+      }

+      

+      public string ParseRenamedAbsyLabel(string! label)

+      {

+         string! prefix = RenameAbsyLabel("+");

+         if(!label.StartsWith(prefix))

+           return null;

+         return label.Substring(prefix.Length);

+      }

+      

+      public void setCurrProc(string! name) 

+      {

+        currProc = name;

+        assert implName2StratifiedInliningInfo.ContainsKey(name);

+      }

+      

+      public void setCurrProcAsMain() 

+      {

+        currProc = "";

+      }

+      

+      private Hashtable/*<int,absy>*/! getLabel2absy() 

+      {

+         assert currProc != null;

+         if(currProc == "") {

+            return mainLabel2absy;

+         }

+         return (!)implName2StratifiedInliningInfo[currProc].label2absy;

+      }

+      

+      // Finds labels and changes them:

+      //   si_fcall_id:  if "id" corresponds to a tracked procedure call, then

+      //                 si_fcall_candidateId

+      //   si_fcall_id:  if "id" does not corresponds to a tracked procedure call, then

+      //                 delete

+      //   num:          si_inline_num

+      //  

+      protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,

+                                                    List<VCExpr!>! newSubExprs,

+                                                    // has any of the subexpressions changed?

+                                                    bool changed,

+                                                    bool arg) 

+      {

+        VCExpr! ret;

+        if (changed)

+          ret = Gen.Function(originalNode.Op,

+                             newSubExprs, originalNode.TypeArguments);

+        else

+          ret = originalNode;

+                                                      

+        VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;

+        if(lop == null) return ret;

+        if(!(ret is VCExprNAry!)) return ret;

+        

+        VCExprNAry! retnary = (VCExprNAry!)ret;

+        string! prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)

+        if(lop.label.Substring(1).StartsWith(prefix)) {

+           int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));

+           Hashtable! label2absy = getLabel2absy();

+           Absy cmd = label2absy[id] as Absy;

+           label2absy.Remove(id);

+           

+           assert cmd != null;

+           AssumeCmd acmd = cmd as AssumeCmd;

+           assert acmd != null;

+           NAryExpr naryExpr  = acmd.Expr as NAryExpr;

+           assert naryExpr != null;

+           

+           string! calleeName = naryExpr.Fun.FunctionName;

+           

+           VCExprNAry callExpr = retnary[0] as VCExprNAry;

+           assert callExpr != null;

+             

+           if(implName2StratifiedInliningInfo.ContainsKey(calleeName)) {

+             int candidateId = GetId(callExpr);

+             boogieExpr2Id[naryExpr] = candidateId;

+             string! label = GetLabel(candidateId);

+             return Gen.LabelPos(label, callExpr);

+           } else {

+             return callExpr;

+           }

+        }

+        

+        // Else, rename label

+        string! newLabel = RenameAbsyLabel(lop.label);

+        if(lop.pos) {

+           return Gen.LabelPos(newLabel, retnary[0]);

+        } else {

+           return Gen.LabelNeg(newLabel, retnary[0]);

+        }

+        

+      }

+      

+    } // end FCallHandler

+    

     public class ErrorReporter : ProverInterface.ErrorHandler {

       Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins;

       Hashtable/*<int, Absy!>*/! label2absy;

@@ -1668,6 +2250,206 @@ namespace VC
       }

     }

 

+    public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {

+      Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo;

+      ProverInterface! theoremProver;

+      VerifierCallback! callback;

+      FCallHandler calls;

+      Program! program;

+      Implementation! mainImpl;

+      DeclFreeProverContext! context;

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

+      

+      public bool underapproximationMode;

+      public List<int>! candidatesToExpand;

+      

+      public StratifiedInliningErrorReporter(Dictionary<string!, StratifiedInliningInfo!>! implName2StratifiedInliningInfo,

+                                             ProverInterface! theoremProver, VerifierCallback! callback, DeclFreeProverContext! context,

+                                             Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

+                                             Program! program, Implementation! mainImpl) {

+        this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;

+        this.theoremProver = theoremProver;

+        this.callback = callback;

+        this.context = context;

+        this.program = program;

+        this.mainImpl = mainImpl;

+        this.underapproximationMode = false;

+        this.calls = null;

+        this.candidatesToExpand = new List<int>();

+        this.gotoCmdOrigins = gotoCmdOrigins;

+      }

+

+      public void SetCandidateHandler(FCallHandler! calls) 

+      {

+        this.calls = calls;

+      }

+      

+      public override void OnModel(IList<string!>! labels, ErrorModel errModel) {

+        if(underapproximationMode) {

+          if(errModel == null) return;

+          GenerateTraceMain(labels, errModel);

+          return;

+        }

+        

+        assert calls != null;

+        assert errModel != null;

+        

+        candidatesToExpand = new List<int>();

+        foreach(string! lab in labels) 

+        {

+           int id = calls.GetId(lab);

+           if(id < 0) continue;

+           if(!calls.currCandidates.Contains(id)) continue;

+           candidatesToExpand.Add(id);

+        }

+        

+      }

+      

+      // Construct the interprocedural trace

+      private void GenerateTraceMain(IList<string!>! labels, ErrorModel! errModel) {

+        if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

+            errModel.Print(ErrorReporter.ModelWriter);

+            ErrorReporter.ModelWriter.Flush();

+        }

+        

+        Counterexample newCounterexample = 

+          GenerateTrace(labels, errModel, 0, mainImpl);

+

+        if(newCounterexample == null) return;

+        

+        #region Map passive program errors back to original program errors

+        ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;

+        if (returnExample != null && gotoCmdOrigins != null)

+        {

+          foreach (Block! b in returnExample.Trace) {

+            assume b.TransferCmd != null;

+            ReturnCmd cmd = (ReturnCmd) gotoCmdOrigins[b.TransferCmd];

+            if (cmd != null)

+            {

+              returnExample.FailingReturn = cmd;

+              break;

+            }

+          }

+        }

+        #endregion

+        

+        callback.OnCounterexample(newCounterexample, null);

+      }

+      

+      private Counterexample GenerateTrace(IList<string!>! labels, ErrorModel! errModel,

+                                           int candidateId, Implementation! procImpl) {

+

+        Hashtable traceNodes = new Hashtable();

+        foreach (string! s in labels) {

+          string! procPrefix = "si_inline_" + candidateId.ToString() + "_";

+          if(!s.StartsWith(procPrefix))

+            continue;

+            

+          Absy! absy;

+          

+          if(candidateId == 0) {

+            absy = Label2Absy(s.Substring(procPrefix.Length)); 

+          } else {

+            absy = Label2Absy(procImpl.Name, s.Substring(procPrefix.Length)); 

+          }

+          

+          if (traceNodes.ContainsKey(absy))

+            System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");

+          else

+            traceNodes.Add(absy, null);

+        }

+

+        BlockSeq! trace = new BlockSeq();

+        Block! entryBlock = (!) procImpl.Blocks[0];

+        assert traceNodes.Contains(entryBlock);

+        trace.Add(entryBlock);

+

+        Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples = new Dictionary<Absy!, CalleeCounterexampleInfo!>();

+        Counterexample newCounterexample = GenerateTraceRec(labels, errModel, entryBlock, traceNodes, trace, calleeCounterexamples);

+

+        return newCounterexample;

+

+      }

+      

+    private Counterexample GenerateTraceRec(

+                          IList<string!>! labels, ErrorModel! errModel,

+                          Block! b, Hashtable! traceNodes, BlockSeq! trace,  

+                          Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples)

+    {

+      // After translation, all potential errors come from asserts.

+      CmdSeq! cmds = b.Cmds;

+      TransferCmd! transferCmd = (!)b.TransferCmd;

+      for (int i = 0; i < cmds.Length; i++)

+      {

+        Cmd! cmd = (!) cmds[i];

+            

+        // Skip if 'cmd' not contained in the trace or not an assert

+        if (cmd is AssertCmd && traceNodes.Contains(cmd))

+        {

+          Counterexample! newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, new Dictionary<Incarnation, Absy!>());

+          newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

+          return newCounterexample;

+        }

+        

+        // Counterexample generation for inlined procedures

+        AssumeCmd assumeCmd = cmd as AssumeCmd;

+        if (assumeCmd == null) continue;

+        NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+        if (naryExpr == null) continue;

+        string! calleeName = naryExpr.Fun.FunctionName;

+        if (!implName2StratifiedInliningInfo.ContainsKey(calleeName)) continue;

+        

+        assert calls != null;

+        int calleeId = calls.boogieExpr2Id[naryExpr];

+        

+        calleeCounterexamples[assumeCmd] = 

+            new CalleeCounterexampleInfo(

+                (!)GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl),

+                new List<object!>());

+

+      }

+      

+      GotoCmd gotoCmd = transferCmd as GotoCmd;

+      if (gotoCmd != null)

+      {

+        foreach (Block! bb in (!)gotoCmd.labelTargets)

+        {

+          if (traceNodes.Contains(bb)){

+            trace.Add(bb);

+            return GenerateTraceRec(labels, errModel, bb, traceNodes, trace, calleeCounterexamples);

+          }

+        }

+      }

+

+      return null;

+

+    }

+          

+      public override Absy! Label2Absy(string! label)

+      {

+        int id = int.Parse(label);

+        assert calls != null;

+        return (Absy!) calls.mainLabel2absy[id];

+      }

+

+      public Absy! Label2Absy(string! procName, string! label)

+      {

+        int id = int.Parse(label);

+        Hashtable! l2a = (!)implName2StratifiedInliningInfo[procName].label2absy;

+        return (Absy!) l2a[id];

+      }

+            

+      public override void OnResourceExceeded(string! msg)

+      {

+        //resourceExceededMessage = msg;

+      }

+      

+      public override void OnProverWarning(string! msg)

+      {

+        callback.OnWarning(msg);

+      }

+    }

+

     protected void ConvertCFG2DAG(Implementation! impl, Program! program)

     {

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1922,7 +2704,15 @@ namespace VC
         exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

       }

       #endregion

-      

+

+      #region Support for stratified lazy inlining

+      if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(impl.Name))

+      {

+        Expr! assertExpr = implName2StratifiedInliningInfo[impl.Name].assertExpr;

+        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

+      }

+      #endregion

+            

       #region Debug Tracing

       if (CommandLineOptions.Clo.TraceVerify) 

       {

@@ -1952,7 +2742,13 @@ namespace VC
         info.exitIncarnationMap = exitIncarnationMap;

         info.incarnationOriginMap = this.incarnationOriginMap;

       }

-      

+      if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(impl.Name))

+      {

+        StratifiedInliningInfo! info = implName2StratifiedInliningInfo[impl.Name];

+        info.exitIncarnationMap = exitIncarnationMap;

+        info.incarnationOriginMap = this.incarnationOriginMap;

+      }

+            

       if (CommandLineOptions.Clo.LiveVariableAnalysis) {

         Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

       }

@@ -2971,6 +3767,7 @@ namespace VC
           SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

         }

 

+        

         VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

         

diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc
index 38aa6af8..be99dd6d 100644
--- a/Source/VCGeneration/Wlp.ssc
+++ b/Source/VCGeneration/Wlp.ssc
@@ -31,6 +31,7 @@ namespace VC {
       this.Ctxt = ctxt;

       this.ControlFlowVariable = controlFlowVariable;

     }

+    

   }

 

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

@@ -110,6 +111,19 @@ namespace VC {
 

       } else if (cmd is AssumeCmd) {

         AssumeCmd ac = (AssumeCmd)cmd;

+

+        if(CommandLineOptions.Clo.StratifiedInlining > 0) {

+          // Label the assume if it is a procedure call

+          NAryExpr naryExpr = ac.Expr as NAryExpr;

+          if (naryExpr != null) {

+            if (naryExpr.Fun is FunctionCall) {

+              int id = ac.UniqueId;

+              ctxt.Label2absy[id] = ac;

+              return gen.ImpliesSimp(gen.LabelPos((!)"si_fcall_" + id.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);

+            }

+          }

+        }

+        

         return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

 

       } else {

diff --git a/Test/alltests.txt b/Test/alltests.txt
index e5f91e61..b566d8af 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -25,3 +25,4 @@ VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification c
 vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks

 livevars	 Use	STORM benchmarks for testing correctness of live variable analysis

 lazyinline	 Use	Lazy inlining benchmarks

+stratifiedinline	 Use	Stratified inlining benchmarks

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
new file mode 100644
index 00000000..aa83b37c
--- /dev/null
+++ b/Test/stratifiedinline/Answer
@@ -0,0 +1,64 @@
+----- Running regression test bar1.bpl

+bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.

+bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

+Execution trace:

+        bar1.bpl(24,3): anon0

+        Inlined call to procedure foo begins

+            bar1.bpl(13,5): anon0

+            Inlined call to procedure bar begins

+                bar1.bpl(7,5): anon0

+            Inlined call to procedure bar ends

+            Inlined call to procedure bar begins

+                bar1.bpl(7,5): anon0

+            Inlined call to procedure bar ends

+        Inlined call to procedure foo ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

+----- Running regression test bar2.bpl

+bar2.bpl(21,3): Error BP5001: This assertion might not hold.

+Execution trace:

+        bar2.bpl(19,3): anon0

+        Inlined call to procedure foo begins

+            bar2.bpl(5,3): anon0

+            bar2.bpl(6,7): anon3_Then

+        Inlined call to procedure foo ends

+        Inlined call to procedure foo begins

+            bar2.bpl(5,3): anon0

+            bar2.bpl(9,7): anon3_Else

+        Inlined call to procedure foo ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

+----- Running regression test bar3.bpl

+bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.

+bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

+Execution trace:

+        bar3.bpl(38,3): anon0

+        Inlined call to procedure foo begins

+            bar3.bpl(18,3): anon0

+            bar3.bpl(19,7): anon3_Then

+            Inlined call to procedure bar begins

+                bar3.bpl(7,3): anon0

+                bar3.bpl(8,7): anon3_Then

+            Inlined call to procedure bar ends

+            Inlined call to procedure bar begins

+                bar3.bpl(7,3): anon0

+                bar3.bpl(8,7): anon3_Then

+            Inlined call to procedure bar ends

+        Inlined call to procedure foo ends

+        Inlined call to procedure bar begins

+            bar3.bpl(7,3): anon0

+            bar3.bpl(10,7): anon3_Else

+        Inlined call to procedure bar ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

+----- Running regression test bar4.bpl

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

+----- Running regression test bar6.bpl

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl
new file mode 100644
index 00000000..845954d5
--- /dev/null
+++ b/Test/stratifiedinline/bar1.bpl
@@ -0,0 +1,26 @@
+var x: int;

+var y: int;

+

+procedure {:inline 1} bar()

+modifies y;

+{

+  y := y + 1;

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  x := x + 1;

+  call bar();

+  call bar();

+  x := x + 1;

+}

+

+procedure main()

+requires x == y;

+ensures x != y;

+modifies x, y;

+{

+  call foo();

+}

+

diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl
new file mode 100644
index 00000000..76991a8f
--- /dev/null
+++ b/Test/stratifiedinline/bar2.bpl
@@ -0,0 +1,24 @@
+

+procedure {:inline 1} foo() returns (x: bool)

+{

+  var b: bool;

+  if (b) {

+    x := false;

+    return;

+  } else {

+    x := true;

+    return;

+  }

+}

+

+procedure main()

+{

+  var b1: bool;

+  var b2: bool;

+

+  call b1 := foo();

+  call b2 := foo();

+  assert b1 == b2;

+}

+

+

diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl
new file mode 100644
index 00000000..7bd91184
--- /dev/null
+++ b/Test/stratifiedinline/bar3.bpl
@@ -0,0 +1,41 @@
+var y: int;

+var x: int;

+

+procedure {:inline 1} bar(b: bool)

+modifies y;

+{

+  if (b) {

+    y := y + 1;

+  } else {

+    y := y - 1;

+  }

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  var b: bool;

+  if (b) {

+    x := x + 1;

+    call bar(true);

+    call bar(true);

+    x := x + 1;

+  } else {

+    x := x - 1;

+    call bar(false);

+    call bar(false);

+    x := x - 1;  

+  }

+}

+

+

+procedure main()

+requires x == y;

+ensures x == y;

+modifies x, y;

+modifies y;

+{

+  call foo();

+  assert x == y;

+  call bar(false);

+}

diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl
new file mode 100644
index 00000000..84640811
--- /dev/null
+++ b/Test/stratifiedinline/bar4.bpl
@@ -0,0 +1,38 @@
+var y: int;

+var x: int;

+

+procedure {:inline 1} bar() returns (b: bool)

+modifies y;

+{

+  if (b) {

+    y := y + 1;

+  } else {

+    y := y - 1;

+  }

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  var b: bool;

+

+  call b := bar();

+  if (b) {

+    x := x + 1;

+  } else {

+    x := x - 1;

+  }

+}

+

+

+procedure main() returns (b: bool)

+requires x == y;

+ensures !b ==> x == y+1;

+ensures b ==> x+1 == y;

+modifies x, y;

+modifies y;

+{

+  call foo();

+  assert x == y;

+  call b := bar();

+}

diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl
new file mode 100644
index 00000000..e133aef7
--- /dev/null
+++ b/Test/stratifiedinline/bar6.bpl
@@ -0,0 +1,36 @@
+var M: [int]int;

+

+procedure {:inline 1} bar(y: int) returns (b: bool)

+modifies M;

+{

+  if (b) {

+    M[y] := M[y] + 1;

+  } else {

+    M[y] := M[y] - 1;

+  }

+}

+

+procedure {:inline 1} foo(x: int, y: int) 

+modifies M;

+{

+  var b: bool;

+

+  call b := bar(y);

+  if (b) {

+    M[x] := M[x] + 1;

+  } else {

+    M[x] := M[x] - 1;

+  }

+}

+

+procedure main(x: int, y: int) returns (b: bool)

+requires x != y;

+requires M[x] == M[y];

+ensures !b ==> M[x] == M[y]+1;

+ensures b ==> M[x]+1 == M[y];

+modifies M;

+{

+  call foo(x, y);

+  assert M[x] == M[y];

+  call b := bar(y);

+}

diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
new file mode 100644
index 00000000..194570d0
--- /dev/null
+++ b/Test/stratifiedinline/runtest.bat
@@ -0,0 +1,22 @@
+@echo off

+setlocal

+

+set BGEXE=..\..\Binaries\Boogie.exe

+rem set BGEXE=mono ..\..\Binaries\Boogie.exe

+

+echo ----- Running regression test bar1.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar1.bpl

+echo -----

+echo ----- Running regression test bar2.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar2.bpl

+echo -----

+echo ----- Running regression test bar3.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar3.bpl

+echo -----

+echo ----- Running regression test bar4.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar4.bpl

+echo -----

+echo ----- Running regression test bar6.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl

+echo -----

+