Added more stat printing

1 files changed, 63 insertions, 9 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 8a7edc75..31bcef54 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1976,6 +1976,9 @@ namespace VC {
        #region Coverage reporter

        if (coverageProcess != null)

             coverageProcess.StandardInput.WriteLine(impl.Name + " main");

+

+       int vcSize = 0;

+       vcSize += SizeComputingVisitor.ComputeSize(vc);

        #endregion

 

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

@@ -1993,20 +1996,31 @@ namespace VC {
        for(int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i ++) 

        {

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

-          foreach(int id in calls.currCandidates) {

-            toExpand.Add(id);

+          foreach (int id in calls.currCandidates)

+          {

+              if (calls.isNonTrivialCandidate(id))

+              {

+                  toExpand.Add(id);

+              }

           }

           expansionCount += toExpand.Count;

           if(incrementalSearch) 

           {

             total_axioms_pushed +=

-              DoExpansion(toExpand, calls, checker, coverageProcess);

+              DoExpansion(toExpand, calls, checker, coverageProcess, ref vcSize);

           } else 

           {

-            vc = DoExpansionAndInline(vc, toExpand, calls, checker, coverageProcess);

+              vc = DoExpansionAndInline(vc, toExpand, calls, checker, coverageProcess, ref vcSize);

           }

        }

 

+       #region Coverage reporter

+       if (CommandLineOptions.Clo.CoverageReporterPath == "Console")

+       {

+           Console.WriteLine("Stratified Inlining: Size of VC after eager inlining: {0}", vcSize);

+       }

+       #endregion

+

        // Number of Z3 queries

        int numqueries = 0;

 

@@ -2178,11 +2192,11 @@ namespace VC {
                if (incrementalSearch)

                {

                    total_axioms_pushed +=

-                     DoExpansion(reporter.candidatesToExpand, calls, checker, coverageProcess);

+                     DoExpansion(reporter.candidatesToExpand, calls, checker, coverageProcess, ref vcSize);

                }

                else

                {

-                   vc = DoExpansionAndInline(vc, reporter.candidatesToExpand, calls, checker, coverageProcess);

+                   vc = DoExpansionAndInline(vc, reporter.candidatesToExpand, calls, checker, coverageProcess, ref vcSize);

                }

 

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

@@ -2205,6 +2219,8 @@ namespace VC {
            Console.WriteLine("Stratified Inlining: Calls to Z3: {0}", numqueries);

            Console.WriteLine("Stratified Inlining: Expansions performed: {0}", expansionCount);

            Console.WriteLine("Stratified Inlining: Candidates left: {0}", calls.currCandidates.Count);

+           Console.WriteLine("Stratified Inlining: Nontrivial Candidates left: {0}", calls.numNonTrivialCandidates());

+           Console.WriteLine("Stratified Inlining: VC Size: {0}", vcSize);

        }

 

        if (coverageProcess != null)

@@ -2233,7 +2249,8 @@ namespace VC {
     // 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, Process progress)

+                             FCallHandler/*!*/ calls, Checker/*!*/ checker, Process progress,

+                             ref int vcSize)

     {

         Contract.Requires(candidates != null);

         Contract.Requires(calls != null);

@@ -2326,6 +2343,7 @@ namespace VC {
             exprToPush = checker.VCExprGen.And(exprToPush, expansion);

         }

         checker.TheoremProver.PushVCExpression(exprToPush);

+        vcSize += SizeComputingVisitor.ComputeSize(exprToPush);

 

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

         checker.TheoremProver.FlushAxiomsToTheoremProver();

@@ -2337,7 +2355,7 @@ namespace VC {
     private VCExpr DoExpansionAndInline(

                                 VCExpr/*!*/ mainVC, List<int>/*!*/ candidates,

                                 FCallHandler/*!*/ calls, Checker/*!*/ checker,

-                                Process progress)

+                                Process progress, ref int vcSize)

     {

         Contract.Requires(mainVC != null);

         Contract.Requires(candidates != null);

@@ -2427,7 +2445,10 @@ namespace VC {
 

         }

 

-        return inliner.Mutate(mainVC, true);

+        var ret = inliner.Mutate(mainVC, true);

+        vcSize = SizeComputingVisitor.ComputeSize(ret);

+

+        return ret;

     }

 

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

@@ -2731,6 +2752,39 @@ namespace VC {
         return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);

       }

 

+      // How many of the current candidates represent calls to procedures

+      // with non-trivial mod sets.

+      // This is only used for statistic purposes

+      public bool isNonTrivialCandidate(int id)

+      {

+          string proc = getProc(id);

+          if (proc == "") return false;

+          if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;

+          var info = implName2StratifiedInliningInfo[proc];

+          if (info.impl.Proc.Modifies.Length != 0) return true;

+          return false;

+          /*

+          foreach (IdentifierExpr ie in info.impl.Proc.Modifies)

+          {

+              if (ie.Decl.Name.StartsWith("Mem_") || ie.Decl.Name.StartsWith("Res_"))

+              {

+                  return true;

+              }

+          }

+          return false;

+           */

+      }

+

+      public int numNonTrivialCandidates()

+      {

+          int ret = 0;

+          foreach (int id in currCandidates)

+          {

+              if(isNonTrivialCandidate(id)) ret++;

+          }

+          return ret;

+      }

+

       // Finds labels and changes them:

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

       //                 si_control_var_candidateId