From 94087bfa24bd34a5cfcb6c8b361439c6de3135a9 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Thu, 16 Sep 2010 22:13:18 +0000
Subject: Added more stat printing

---
 Source/VCGeneration/VC.cs | 72 +++++++++++++++++++++++++++++++++++++++++------
 1 file 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
-- 
cgit v1.2.3