Coverage: add information from CFA for CounterexampleCoverageCollector

Druidos · Apr 16, 2021 · 953c051 · 953c051
1 parent 4eacf14
commit 953c051
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 17 deletions.
diff --git a/src/org/sosy_lab/cpachecker/cpa/arg/counterexamples/CEXExporter.java b/src/org/sosy_lab/cpachecker/cpa/arg/counterexamples/CEXExporter.java
@@ -100,12 +100,13 @@ enum CounterexampleExportType {
   private final ExtendedWitnessExporter extendedWitnessExporter;
   private final HarnessExporter harnessExporter;
   private TestCaseExporter testExporter;
+  private final CFA cfa;
 
   public CEXExporter(
       Configuration config,
       CEXExportOptions pOptions,
       LogManager pLogger,
-      CFA cfa,
+      CFA pCfa,
       ConfigurableProgramAnalysis cpa,
       WitnessExporter pWitnessExporter,
       ExtendedWitnessExporter pExtendedWitnessExporter)
@@ -115,12 +116,13 @@ public CEXExporter(
     logger = pLogger;
     witnessExporter = checkNotNull(pWitnessExporter);
     extendedWitnessExporter = checkNotNull(pExtendedWitnessExporter);
+    cfa = pCfa;
 
     if (!options.disabledCompletely()) {
       cexFilter =
           CounterexampleFilter.createCounterexampleFilter(config, pLogger, cpa, cexFilterClasses);
-      harnessExporter = new HarnessExporter(config, pLogger, cfa);
-      testExporter = new TestCaseExporter(cfa, logger, config);
+      harnessExporter = new HarnessExporter(config, pLogger, pCfa);
+      testExporter = new TestCaseExporter(pCfa, logger, config);
     } else {
       cexFilter = null;
       harnessExporter = null;
@@ -171,7 +173,7 @@ public void exportCounterexample(
     if (options.getCoveragePrefix() != null) {
       Path outputPath = options.getCoveragePrefix().getPath(counterexample.getUniqueId());
       try (Writer lcovFile = IO.openOutputFile(outputPath, Charset.defaultCharset())) {
-        CoverageReportLcov.write(CoverageCollector.fromCounterexample(targetPath), lcovFile);
+        CoverageReportLcov.write(CoverageCollector.fromCounterexample(targetPath, cfa), lcovFile);
       } catch (IOException e) {
         logger.logUserException(
             Level.WARNING, e, "Could not write coverage information for counterexample to file");
@@ -182,7 +184,7 @@ public void exportCounterexample(
       Path outputPath = options.getAdditionalCoveragePrefix().getPath(counterexample.getUniqueId());
       try (Writer additionalLcovFile = IO.openOutputFile(outputPath, Charset.defaultCharset())) {
         AdditionalCoverageReportLcov.write(
-            CoverageCollector.additionalInfoFromCounterexample(targetPath), additionalLcovFile);
+            CoverageCollector.additionalInfoFromCounterexample(targetPath, cfa), additionalLcovFile);
       } catch (IOException e) {
         logger.logUserException(
             Level.WARNING, e, "Could not write additional coverage information for counterexample to file");
@@ -193,7 +195,7 @@ public void exportCounterexample(
       Path outputPath = options.getGcovCoveragePrefix().getPath(counterexample.getUniqueId());
       try (Writer gcovFile = IO.openOutputFile(outputPath, Charset.defaultCharset())) {
         CoverageReportGcov.write(
-            CoverageCollector.additionalInfoFromCounterexample(targetPath), gcovFile);
+            CoverageCollector.additionalInfoFromCounterexample(targetPath, cfa), gcovFile);
       } catch (IOException e) {
         logger.logUserException(
             Level.WARNING, e, "Could not write coverage information for counterexample to gcov file");

diff --git a/src/org/sosy_lab/cpachecker/util/coverage/CoverageCollector.java b/src/org/sosy_lab/cpachecker/util/coverage/CoverageCollector.java
@@ -37,21 +37,21 @@
  */
 public abstract class CoverageCollector {
 
-  public static CoverageData fromReachedSet(Iterable<AbstractState> pReached, CFA cfa) {
-    return new ReachedSetCoverageCollector().collectFromReachedSet(pReached, cfa);
+  public static CoverageData fromReachedSet(Iterable<AbstractState> pReached, CFA pCfa) {
+    return new ReachedSetCoverageCollector().collectFromReachedSet(pReached, pCfa);
   }
 
-  public static CoverageData fromCounterexample(ARGPath pPath) {
-    return new CounterexampleCoverageCollector().collectFromCounterexample(pPath);
+  public static CoverageData fromCounterexample(ARGPath pPath, CFA pCfa) {
+    return new CounterexampleCoverageCollector().collectFromCounterexample(pPath, pCfa);
   }
 
   public static CoverageData additionalInfoFromReachedSet(
-      Iterable<AbstractState> pReached, CFA cfa) {
-    return new AdditionalCoverageCollector().collectFromReachedSet(pReached, cfa);
+      Iterable<AbstractState> pReached, CFA pCfa) {
+    return new AdditionalCoverageCollector().collectFromReachedSet(pReached, pCfa);
   }
 
-  public static CoverageData additionalInfoFromCounterexample(ARGPath pPath) {
-    return new CounterexampleAdditionalCoverageCollector().collectFromCounterexample(pPath);
+  public static CoverageData additionalInfoFromCounterexample(ARGPath pPath, CFA pCfa) {
+    return new CounterexampleAdditionalCoverageCollector().collectFromCounterexample(pPath, pCfa);
   }
 
   static CoverageData processStateForAdditionalInfo(AbstractState state, CoverageData pCov) {
@@ -82,8 +82,8 @@ static CoverageData processStateForAdditionalInfo(AbstractState state, CoverageD
 
 class CounterexampleAdditionalCoverageCollector extends CounterexampleCoverageCollector {
   @Override
-  CoverageData collectFromCounterexample(ARGPath cexPath) {
-    CoverageData cov = super.collectFromCounterexample(cexPath);
+  CoverageData collectFromCounterexample(ARGPath cexPath, CFA pCfa) {
+    CoverageData cov = super.collectFromCounterexample(cexPath, pCfa);
     PathIterator pathIterator = cexPath.fullPathIterator();
     while (pathIterator.hasNext()) {
       AbstractState state = pathIterator.getAbstractState().getWrappedState();
@@ -100,8 +100,9 @@ class CounterexampleCoverageCollector {
    * Coverage from a counterexample does not report all existing edges, but the set of existing
    * edges needs to contain all covered edges at the minimum.
    */
-  CoverageData collectFromCounterexample(ARGPath cexPath) {
+  CoverageData collectFromCounterexample(ARGPath cexPath, CFA pCfa) {
     CoverageData cov = new CoverageData();
+    cov.putCFA(pCfa);
     collectCoveredEdges(cexPath, cov);
     return cov;
   }
@@ -128,6 +129,17 @@ private void collectCoveredEdges(ARGPath cexPath, CoverageData cov) {
         break;
       }
       cov.addVisitedEdge(edge);
+
+      CFANode location = pathIterator.getLocation();
+      if (location != null && location instanceof FunctionEntryNode) {
+        FunctionEntryNode entryNode = (FunctionEntryNode) location;
+
+        final FileLocation loc = entryNode.getFileLocation();
+        if (loc.getStartingLineNumber() != 0) {
+          cov.addVisitedFunction(entryNode);
+        }
+      }
+
       pathIterator.advance();
     }
   }