SV-COMP: explorer-owned per-testcase stats.json + runs/ layout & analysis (#25)

.gitignore

@@ -13,6 +13,8 @@ targets/applications/openolat/libs/z3/
 **/logs/
 **/logs-debug/
 **/results/
+**/runs/
+**/runs-debug/
 **/*.class
 /build/
 **/build/

symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java

@@ -5,12 +5,9 @@
 import ch.qos.logback.core.FileAppender;
 import de.uzl.its.swat.common.exceptions.SWATException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.config.Config;
 import de.uzl.its.swat.thread.ThreadHandler;
 
-import java.util.Arrays;
-
 import static java.lang.Thread.currentThread;
 /**
  * ErrorHandler is responsible for handling exceptions throughout the application. It decides
@@ -73,14 +70,6 @@ public void handleException(String msg, Throwable t) {
             throw new RuntimeException(msg, t);
         }
         logger.error("Preparing to halt execution due to error...");
-        try {
-            if (ThreadHandler.hasThreadContext(currentThread().getId())) {
-                ThreadHandler.logStats(currentThread().getId());
-            }
-            ThreadHandler.logStats(-1);
-        } catch (Exception e) {
-            logger.error("Error while logging stats");
-        }
         logger.error("Halting...");
         if (!config.isLogShadowStateToConsole()) {
             logger.info("Flushing loggers...");
@@ -100,28 +89,6 @@ public void handleException(String msg, Throwable t) {
 
     public void logException(String msg, Throwable t){
         logger.error(msg, t);
-        long threadId = currentThread().getId();
-        String executionStage;
-        if(ThreadHandler.hasThreadContext(threadId)){
-            try {
-                executionStage = ThreadHandler.getCurrentInstruction(threadId).toString();
-            } catch (Exception e) {
-                logger.error("Error while getting current instruction", e);
-                executionStage = "Unknown";
-            }
-        }  else {
-            executionStage = "Main Thread";
-            threadId = -1;
-        }
-
-        // Record the error
-        ErrorRecord errorRecord = new ErrorRecord(msg, t.getClass().getSimpleName(),
-                Arrays.toString(t.getStackTrace()), t.getMessage(), executionStage);
-        try{
-            ThreadHandler.recordException(threadId, errorRecord);
-        } catch (Exception e) {
-            logger.error("Error while recording exception", e);
-        }
     }
 
 }

symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java

@@ -3,7 +3,6 @@
 import ch.qos.logback.classic.Logger;
 import de.uzl.its.swat.common.ErrorHandler;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.config.Config;
 import de.uzl.its.swat.symbolic.instruction.Instruction;
 import de.uzl.its.swat.thread.ThreadContext;

symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java

@@ -1,55 +1,32 @@
 package de.uzl.its.swat.common.logging;
 
-import com.fasterxml.jackson.core.JsonProcessingException;
-import com.fasterxml.jackson.databind.ObjectMapper;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import lombok.Getter;
 
-import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
+import java.util.HashSet;
+import java.util.Set;
+
+/**
+ * In-memory accumulator for per-execution statistics: the methods that could not be modelled
+ * symbolically ({@link #invocations}) and the subset of those that caused symbolic context loss
+ * ({@link #contextLossInvocations}). This data is attached to the trace and sent to the Symbolic
+ * Explorer (see {@code DTOBuilder}); the explorer owns the consolidated per-testcase output. The
+ * executor itself no longer writes any stats file.
+ */
 @Getter
 public class StatsStorage {
-    private String entrypoint;
     private final HashMap<InvocationEntry, Integer> invocations;
-    private final ArrayList<ErrorRecord> errors;
+    // Subset of invocations that received symbolic arguments and therefore caused context loss.
+    private final Set<InvocationEntry> contextLossInvocations;
 
     public StatsStorage() {
         this.invocations = new HashMap<>();
-        this.errors = new ArrayList<>();
+        this.contextLossInvocations = new HashSet<>();
     }
 
-    public String convertToJson() throws JsonProcessingException {
-        ObjectMapper mapper = new ObjectMapper();
-        List<Map<String, Object>> serializedList = new ArrayList<>();
-
-        invocations.forEach((entry, count) -> {
-            Map<String, Object> entryMap = new HashMap<>();
-            entryMap.put("owner", entry.owner());
-            entryMap.put("name", entry.name());
-            entryMap.put("desc", entry.desc());
-            entryMap.put("isInstance", entry.isInstance());
-            entryMap.put("invokeId", entry.invokeId());
-            entryMap.put("isSymbolic", entry.isSymbolic());
-            entryMap.put("count", count);  // Store the count as well
-
-            serializedList.add(entryMap);
-        });
-        errors.forEach(error -> {
-            Map<String, Object> errorMap = new HashMap<>();
-            errorMap.put("message", error.message());
-            errorMap.put("type", error.type());
-            errorMap.put("stackTrace", error.stackTrace());
-            errorMap.put("exceptionMessage", error.exceptionMessage());
-            errorMap.put("executionStage", error.executionStage());
-
-            serializedList.add(errorMap);
-        });
-
-        return mapper.writeValueAsString(serializedList);  // Convert the list of maps to JSON
+    /** Marks an already-recorded missing invocation as a context-loss culprit. */
+    public void recordContextLossInvocation(InvocationEntry entry) {
+        contextLossInvocations.add(entry);
     }
 }
-

symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java

@@ -108,8 +108,6 @@ public static void terminate() {
         try {
             Transformer.logMissedClasses();
             ThreadHandler.disableThreadContext(currentThread().getId());
-            ThreadHandler.logStats(currentThread().getId());
-            ThreadHandler.logStats(-1);
             logger.info(
                     new PrintBox(
                             60,
@@ -140,7 +138,7 @@ public static void terminate() {
                     break;
                 case PRINT:
                     if (!ThreadHandler.isThreadContextAborted(currentThread().getId())) {
-                        System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO());
+                        System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(currentThread().getId())));
                     }
                     break;
                 case NONE:

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java

@@ -96,13 +96,15 @@ public class InvocationHandler {
             }
 
 
-            ThreadHandler.recordMissingInvocation(Thread.currentThread().getId(),  new InvocationEntry(
+            long threadId = Thread.currentThread().getId();
+            InvocationEntry entry = new InvocationEntry(
                     owner,
                     name,
                     desc,
                     isInstance,
                     invokeId,
-                    containsSymbolicArgument));
+                    containsSymbolicArgument);
+            ThreadHandler.recordMissingInvocation(threadId, entry);
 
             if(
                     (retValue.equals(PlaceHolder.instance) // To detect a missing implementation
@@ -114,6 +116,9 @@ public class InvocationHandler {
                         owner,
                         desc);
                 symbolicTraceHandler.recordSymbolicContextLoss();
+                // Record the culprit so the explorer can compute the context-loss subset of the
+                // missing invocations without scraping logs.
+                ThreadHandler.recordContextLossInvocation(threadId, entry);
             }
 
         }

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java

@@ -11,12 +11,15 @@
 import de.uzl.its.swat.common.exceptions.NoThreadContextException;
 import de.uzl.its.swat.common.exceptions.NotImplementedException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.common.logging.StatsStorage;
+import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import de.uzl.its.swat.coverage.InstrCoverage;
 import de.uzl.its.swat.symbolic.trace.dto.*;
 import de.uzl.its.swat.thread.ThreadHandler;
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
 
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
@@ -34,8 +37,33 @@ class DTOBuilder {
      * @param symbolicTrace The symbolic trace to be encoded.
      * @return The symbolic trace encoded as a JSON string.
      */
-    protected static String encodeTrace(SymbolicTrace symbolicTrace) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return buildRequestBody(buildTraceDTO(symbolicTrace));
+    protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage));
+    }
+
+    /**
+     * Builds the list of missing-invocation DTOs from the per-execution statistics. The full set of
+     * missing invocations is the superset; entries present in the context-loss set are flagged so
+     * the explorer can compute the context-loss subset without log scraping.
+     *
+     * @param statsStorage The per-execution statistics accumulator.
+     * @return The missing invocations encoded as DTOs.
+     */
+    private static ArrayList<InvocationDTO> buildMissingInvocations(StatsStorage statsStorage) {
+        ArrayList<InvocationDTO> missingInvocations = new ArrayList<>();
+        for (Map.Entry<InvocationEntry, Integer> e : statsStorage.getInvocations().entrySet()) {
+            InvocationEntry entry = e.getKey();
+            missingInvocations.add(
+                    new InvocationDTO(
+                            entry.owner(),
+                            entry.name(),
+                            entry.desc(),
+                            entry.isInstance(),
+                            entry.isSymbolic(),
+                            statsStorage.getContextLossInvocations().contains(entry),
+                            e.getValue()));
+        }
+        return missingInvocations;
     }
 
     /**
@@ -46,7 +74,7 @@ protected static String encodeTrace(SymbolicTrace symbolicTrace) throws NoThread
      * @return A {@link TraceDTO ConstraintDTO} that contains relevant all relevant information
      *     to transfer symbolic traces
      */
-    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThreadContextException, NotImplementedException {
+    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, NotImplementedException {
         ArrayList<InputDTO> inputs = new ArrayList<>();
         ArrayList<UFDTO> ufs = new ArrayList<>();
         ArrayList<BranchDTO> trace = new ArrayList<>();
@@ -106,7 +134,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThre
                 trace.add(new BranchDTO(se.getIid(), se.getInst()));
             }
         }
-        return new TraceDTO(inputs, trace, ufs, symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange());
+        return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange());
     }
 
     protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException {

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java

@@ -6,6 +6,7 @@
 import de.uzl.its.swat.common.exceptions.NoThreadContextException;
 import de.uzl.its.swat.common.exceptions.NotImplementedException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.common.logging.StatsStorage;
 import de.uzl.its.swat.symbolic.value.Value;
 import de.uzl.its.swat.thread.ThreadHandler;
 import java.util.ArrayList;
@@ -108,8 +109,8 @@ public List<BooleanFormula> getConstraints() {
      *
      * @return The symbolic trace encoded as a JSON string.
      */
-    public String getTraceDTO() throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return DTOBuilder.encodeTrace(symbolicTrace);
+    public String getTraceDTO(StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return DTOBuilder.encodeTrace(symbolicTrace, statsStorage);
     }
 
     /**

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java

@@ -0,0 +1,55 @@
+package de.uzl.its.swat.symbolic.trace.dto;
+
+/**
+ * Describes a single method invocation that could not be modelled symbolically during execution
+ * (i.e. it returned a {@link de.uzl.its.swat.symbolic.value.PlaceHolder}). These are collected per
+ * execution and shipped to the Symbolic Explorer as part of the trace so that the explorer owns the
+ * consolidated per-testcase statistics instead of relying on log/stats-file scraping.
+ *
+ * <p>{@code contextLoss} marks the dangerous subset: invocations that received symbolic arguments
+ * and therefore caused symbolic context loss (see {@code InvocationHandler}). Missing invocations
+ * are the superset; context-loss invocations are the subset.
+ */
+public class InvocationDTO {
+    @SuppressWarnings("unused")
+    private String owner;
+
+    @SuppressWarnings("unused")
+    private String name;
+
+    @SuppressWarnings("unused")
+    private String desc;
+
+    @SuppressWarnings("unused")
+    private boolean isInstance;
+
+    @SuppressWarnings("unused")
+    private boolean isSymbolic;
+
+    @SuppressWarnings("unused")
+    private boolean contextLoss;
+
+    @SuppressWarnings("unused")
+    private int count;
+
+    public InvocationDTO(
+            String owner,
+            String name,
+            String desc,
+            boolean isInstance,
+            boolean isSymbolic,
+            boolean contextLoss,
+            int count) {
+        this.owner = owner;
+        this.name = name;
+        this.desc = desc;
+        this.isInstance = isInstance;
+        this.isSymbolic = isSymbolic;
+        this.contextLoss = contextLoss;
+        this.count = count;
+    }
+
+    /** Private default constructor for serialization */
+    @SuppressWarnings("unused")
+    private InvocationDTO() {}
+}

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java

@@ -12,17 +12,23 @@ public class TraceDTO {
     @SuppressWarnings("unused")
     private ArrayList<UFDTO> ufs;
 
+    // The methods encountered during execution that could not be modelled symbolically. The
+    // superset of all missing invocations; entries with contextLoss=true are the dangerous subset.
+    @SuppressWarnings("unused")
+    private ArrayList<InvocationDTO> missingInvocations;
+
     @SuppressWarnings("unused")
     private boolean symbolicContextLoss = false;
     @SuppressWarnings("unused")
     private boolean symbolicPrecisionLoss = false;
     @SuppressWarnings("unused")
     private boolean referenceSemanticChange = false;
 
-    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
+    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
         this.trace = trace;
         this.inputs = inputs;
         this.ufs = ufs;
+        this.missingInvocations = missingInvocations;
         this.symbolicContextLoss = symbolicContextLoss;
         this.symbolicPrecisionLoss = symbolicPrecisionLoss;
         this.referenceSemanticChange = referenceSemanticChange;