Some simplifications to coverage reporting for StratifiedInlining.

2 files changed, 81 insertions, 51 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 3324d632..eadd8b97 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -351,6 +351,7 @@ namespace Microsoft.Boogie {
     public int StratifiedInliningOption = 0;

     public int RecursionBound = 500;

     public string CoverageReporterPath = null;

+    public Process coverageReporter = null; // used internally for debugging

 

     public enum TypeEncoding {

       None,

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 775a04cc..c6e77b67 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1921,27 +1921,40 @@ namespace VC {
        // create a process for displaying coverage information

        Process coverageProcess = null;

        ProcessStartInfo coverageProcessInfo = null;

+       bool stopCoverageProcess = true;

        #region Coverage reporter

-       if (CommandLineOptions.Clo.CoverageReporterPath != null)

+       coverageProcess = CommandLineOptions.Clo.coverageReporter;

+       if (coverageProcess != null)

        {

-           coverageProcess = new Process();

-           coverageProcessInfo = new ProcessStartInfo();

-           coverageProcessInfo.CreateNoWindow = true;

-           coverageProcessInfo.FileName = CommandLineOptions.Clo.CoverageReporterPath + @"\CoverageGraph.exe";

-           coverageProcessInfo.RedirectStandardInput = true;

-           coverageProcessInfo.RedirectStandardOutput = true;

-           coverageProcessInfo.RedirectStandardError = false;

-           coverageProcessInfo.UseShellExecute = false;

-

-           coverageProcess.StartInfo = coverageProcessInfo;

-           try

+           stopCoverageProcess = false;

+           if (!coverageProcess.StartInfo.RedirectStandardInput)

            {

-               coverageProcess.Start();

+               coverageProcess = null;

            }

-           catch (System.ComponentModel.Win32Exception e)

+       }

+       else

+       {

+           if (CommandLineOptions.Clo.CoverageReporterPath != null)

            {

-               coverageProcess.Dispose();

-               coverageProcess = null;

+               coverageProcess = new Process();

+               coverageProcessInfo = new ProcessStartInfo();

+               coverageProcessInfo.CreateNoWindow = true;

+               coverageProcessInfo.FileName = CommandLineOptions.Clo.CoverageReporterPath + @"\CoverageGraph.exe";

+               coverageProcessInfo.RedirectStandardInput = true;

+               coverageProcessInfo.RedirectStandardOutput = true;

+               coverageProcessInfo.RedirectStandardError = false;

+               coverageProcessInfo.UseShellExecute = false;

+

+               coverageProcess.StartInfo = coverageProcessInfo;

+               try

+               {

+                   coverageProcess.Start();

+               }

+               catch (System.ComponentModel.Win32Exception e)

+               {

+                   coverageProcess.Dispose();

+                   coverageProcess = null;

+               }

            }

        }

        #endregion

@@ -1973,20 +1986,20 @@ namespace VC {
        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);

+

        #region Coverage reporter

        if (coverageProcess != null)

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

+           coverageProcess.StandardInput.WriteLine("PROGRAM_ENTRY " + calls.getPersistentName(0));

 

        int vcSize = 0;

        vcSize += SizeComputingVisitor.ComputeSize(vc);

        #endregion

 

-       // 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;

@@ -2038,6 +2051,24 @@ namespace VC {
            {

                int axioms_pushed, prev_axioms_pushed;

 

+               #region Coverage reporter

+               if (coverageProcess != null)

+               {

+                   coverageProcess.StandardInput.WriteLine("reset_graph_round");

+                   // Go through the curr candidates and write down their parents (i.e.,

+                   // those procedures that have an assume false in them)

+                   foreach (var id in calls.currCandidates)

+                   {

+                       if (calls.candidateParent.ContainsKey(id))

+                       {

+                           var pid = calls.candidateParent[id];

+                           var str = calls.getPersistentName(pid);

+                           coverageProcess.StandardInput.WriteLine("color " + str);

+                       }

+                   }

+               }

+               #endregion

+

                // Underapprox query

                if (underApproxNeeded)

                {

@@ -2184,10 +2215,7 @@ namespace VC {
 

                expansionCount += reporter.candidatesToExpand.Count;

 

-               #region Coverage reporter

-               if (coverageProcess != null)

-                   coverageProcess.StandardInput.WriteLine("reset_graph_round");

-               #endregion

+

 

                if (incrementalSearch)

                {

@@ -2223,7 +2251,7 @@ namespace VC {
            Console.WriteLine("Stratified Inlining: VC Size: {0}", vcSize);

        }

 

-       if (coverageProcess != null)

+       if (coverageProcess != null && stopCoverageProcess)

        {

            coverageProcess.StandardInput.WriteLine("Done");

 

@@ -2273,17 +2301,8 @@ namespace VC {
             if (progress != null && calls.candidateParent.ContainsKey(id))

             {

                 var parentId = calls.candidateParent[id];

-                string str = "";

-                if (parentId == 0)

-                {

-                    str = "main";

-                }

-                else

-                {

-                    str = (calls.id2Candidate[parentId].Op as VCExprBoogieFunctionOp).Func.Name;

-                    str += "_" + parentId.ToString();

-                }

-                str = str + " " + procName + "_" + id.ToString();

+                string str =

+                 calls.getPersistentName(parentId) + " " + calls.getPersistentName(id);

                 progress.StandardInput.WriteLine(str);

             }

             #endregion

@@ -2379,17 +2398,8 @@ namespace VC {
             if (progress != null && calls.candidateParent.ContainsKey(id))

             {

                 var parentId = calls.candidateParent[id];

-                string str = "";

-                if (parentId == 0)

-                {

-                    str = "main";

-                }

-                else

-                {

-                    str = (calls.id2Candidate[parentId].Op as VCExprBoogieFunctionOp).Func.Name;

-                    str += "_" + parentId.ToString();

-                }

-                str = str + " " + procName + "_" + id.ToString();

+                string str =

+                 calls.getPersistentName(parentId) + " " + calls.getPersistentName(id);

                 progress.StandardInput.WriteLine(str);

             }

             #endregion

@@ -2654,7 +2664,26 @@ namespace VC {
 

           return (id2Candidate[id].Op as VCExprBoogieFunctionOp).Func.Name;

       }

-    

+

+      // Get a unique name for this candidate (dependent only on the Call

+      // graph of the program). This is used for reporting coverage only.

+      public string getPersistentName(int top_id)

+      {

+          string stack = "";

+          var id = top_id;

+          while (candidateParent.ContainsKey(id))

+          {

+              id = candidateParent[id];

+              var pname = getProc(id);

+              if (pname == "") pname = "main";

+              stack += "_" + getProc(id);

+          }

+

+          var n = getProc(top_id);

+          if (n == "") n = "main";

+          return n + "_cs=" + stack;

+      }

+

       private int GetNewId(VCExprNAry vc)

       {

           Contract.Requires(vc != null);