From 550d304756eb6d859e289ec52160bccb6890d145 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Tue, 16 Jun 2026 16:21:49 +0000 Subject: [PATCH 1/2] feat(sv-comp): explorer-owned per-testcase stats.json via trace metadata MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The executor no longer writes stats_.json. Instead it accumulates missing invocations (each flagged when it caused symbolic context loss) in StatsStorage and ships them with the trace (TraceDTO.missingInvocations / new InvocationDTO). The explorer accumulates this per testcase on the Tree and, at testcase completion, writes a single consolidated stats.json to the log dir — mirroring the existing timing_data.json write. It holds the verdict, soundness flags, the missing-invocation superset and the explicit context-loss subset, so the analysis can rely on authoritative structured data instead of scraping logs. Execution errors cannot ride the trace: in sv-comp every error path halts the JVM before the trace is sent. They are instead surfaced from the executor stdout markers the explorer already scans in determine_next_step ([SWAT Exception] / internal SWAT AssertionError), recorded on the Tree and included in stats.json. Removes the now-dead executor error chain (StatsStorage.errors, ThreadContext/ThreadHandler.recordException, ErrorRecord) and the unused StatsStorage.entrypoint. Part of #25. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../de/uzl/its/swat/common/ErrorHandler.java | 33 -------- .../swat/common/exceptions/SWATAssert.java | 1 - .../its/swat/common/logging/StatsStorage.java | 55 ++++--------- .../common/logging/records/ErrorRecord.java | 4 - .../uzl/its/swat/instrument/Intrinsics.java | 4 +- .../symbolic/invoke/InvocationHandler.java | 9 ++- .../its/swat/symbolic/trace/DTOBuilder.java | 36 ++++++++- .../symbolic/trace/SymbolicTraceHandler.java | 5 +- .../symbolic/trace/dto/InvocationDTO.java | 55 +++++++++++++ .../its/swat/symbolic/trace/dto/TraceDTO.java | 8 +- .../de/uzl/its/swat/thread/ThreadContext.java | 29 +------ .../de/uzl/its/swat/thread/ThreadHandler.java | 32 +++----- .../constraint/ConstraintController.py | 2 + .../constraint/ConstraintService.py | 11 ++- .../data/BinaryExecutionTree/Tree.py | 53 ++++++++++++ symbolic-explorer/data/Database.py | 9 ++- symbolic-explorer/driver/SVCompDriver.py | 10 ++- .../parse/DataTransferObjects.py | 16 ++++ symbolic-explorer/svcomp/TestcaseStats.py | 81 +++++++++++++++++++ 19 files changed, 315 insertions(+), 138 deletions(-) delete mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java create mode 100644 symbolic-explorer/svcomp/TestcaseStats.py diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java index 7f89493..18a888a 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java +++ b/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); - } } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java index ee4c341..e8859b9 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java +++ b/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; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java index 6c6cfd3..cbf961c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java +++ b/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 invocations; - private final ArrayList errors; + // Subset of invocations that received symbolic arguments and therefore caused context loss. + private final Set 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> serializedList = new ArrayList<>(); - - invocations.forEach((entry, count) -> { - Map 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 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); } } - diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java deleted file mode 100644 index 0322708..0000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java +++ /dev/null @@ -1,4 +0,0 @@ -package de.uzl.its.swat.common.logging.records; - -public record ErrorRecord(String message, String type, String stackTrace, String exceptionMessage, String executionStage) { -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java index 0561ae1..48061c8 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java +++ b/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: diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java index d1c465b..2150713 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java +++ b/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); } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index 8fa442e..e1156b9 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/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 buildMissingInvocations(StatsStorage statsStorage) { + ArrayList missingInvocations = new ArrayList<>(); + for (Map.Entry 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 inputs = new ArrayList<>(); ArrayList ufs = new ArrayList<>(); ArrayList 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 { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index 6d99da5..0211915 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/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 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); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java new file mode 100644 index 0000000..1ecef89 --- /dev/null +++ b/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. + * + *

{@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() {} +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java index 2f8b394..75eaf69 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java @@ -12,6 +12,11 @@ public class TraceDTO { @SuppressWarnings("unused") private ArrayList 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 missingInvocations; + @SuppressWarnings("unused") private boolean symbolicContextLoss = false; @SuppressWarnings("unused") @@ -19,10 +24,11 @@ public class TraceDTO { @SuppressWarnings("unused") private boolean referenceSemanticChange = false; - public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) { + public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, ArrayList 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; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java index 25fb19f..38c571d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java @@ -8,7 +8,6 @@ import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException; import de.uzl.its.swat.common.exceptions.ThreadAlreadyEnabledException; import de.uzl.its.swat.common.logging.GlobalLogger; -import de.uzl.its.swat.common.logging.records.ErrorRecord; import de.uzl.its.swat.common.logging.records.InvocationEntry; import de.uzl.its.swat.common.logging.LoggerUtils; import de.uzl.its.swat.common.logging.StatsStorage; @@ -23,9 +22,6 @@ import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; -import java.io.FileNotFoundException; -import java.io.FileOutputStream; -import java.io.PrintStream; import java.util.HashMap; import java.util.concurrent.TimeUnit; @@ -53,7 +49,6 @@ public class ThreadContext { @Getter @Setter private Instruction current; @Getter @Setter private Long instCnt = 0L; @Getter private Instruction next; - @Getter private PrintStream statsStream; @Getter private boolean disabled; @Getter private boolean aborted; Config config = Config.instance(); @@ -136,17 +131,6 @@ public ThreadContext(long id, String endpointName, int endpointID) throws Invali this.coverageTraceHandler = new CoverageTraceHandler(); - - try { - - this.statsStream = - new PrintStream( - new FileOutputStream( - config.getLoggingDirectory() + "/stats_" + id + ".json", - true)); - } catch (FileNotFoundException e) { - this.statsStream = System.out; - } } void checkAbortTimerExpiration() { @@ -236,6 +220,10 @@ public void recordMissingInvocation(InvocationEntry entry) { statsStorage.getInvocations().merge(entry, 1, Integer::sum); } + public void recordContextLossInvocation(InvocationEntry entry) { + statsStorage.recordContextLossInvocation(entry); + } + public long getNextSubUid(String symbolicVar) { long next = SubUid.getOrDefault(symbolicVar, 0L); @@ -244,13 +232,4 @@ public long getNextSubUid(String symbolicVar) { return next; } - /** - * Records an exception that occurred during the execution of the symbolic execution. This includes swallowed - * assertions. - * - * @param record The error record - */ - public void recordException(ErrorRecord record) { - statsStorage.getErrors().add(record); - } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java index 1aab04e..2ecdbac 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java @@ -4,7 +4,6 @@ import com.fasterxml.jackson.core.JsonProcessingException; import de.uzl.its.swat.common.exceptions.*; import de.uzl.its.swat.common.logging.GlobalLogger; -import de.uzl.its.swat.common.logging.records.ErrorRecord; import de.uzl.its.swat.common.logging.records.InvocationEntry; import de.uzl.its.swat.config.Config; import de.uzl.its.swat.coverage.CoverageRequest; @@ -18,7 +17,6 @@ import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.Value; -import java.io.PrintStream; import java.util.HashMap; import java.util.concurrent.ThreadLocalRandom; import java.util.logging.LogRecord; @@ -139,6 +137,15 @@ public static UFHandler getUFHandler(long id) throws NoThreadContextException { } } + public static de.uzl.its.swat.common.logging.StatsStorage getStatsStorage(long id) throws NoThreadContextException { + ThreadContext context = threadContextHashMap.get(id); + if (context != null) { + return context.getStatsStorage(); + } else { + throw new NoThreadContextException(id); + } + } + public static void sendData(long id) throws NoThreadContextException, JsonProcessingException, NotImplementedException { ThreadContext context = threadContextHashMap.get(id); if (context != null) { @@ -156,7 +163,7 @@ public static void sendData(long id) throws NoThreadContextException, JsonProces } if(!config.isCoverageOnly()) { ConstraintRequest.sendConstraints( - symbolicStateHandler.getTraceDTO(), endpointID, traceID); + symbolicStateHandler.getTraceDTO(context.getStatsStorage()), endpointID, traceID); } } else { @@ -273,25 +280,12 @@ public static void recordMissingInvocation( } } - public static void recordException(long id, ErrorRecord er) throws NoThreadContextException { - ThreadContext context = threadContextHashMap.get(id); - if (context != null) { - context.recordException(er); - } else { - throw new NoThreadContextException(id); - } - } - - public static void logStats(long id) throws NoThreadContextException { + public static void recordContextLossInvocation( + long id, InvocationEntry entry) throws NoThreadContextException { if (!config.isLoggingStats()) return; ThreadContext context = threadContextHashMap.get(id); if (context != null) { - PrintStream ps = context.getStatsStream(); - try { - ps.println(context.getStatsStorage().convertToJson()); - } catch (JsonProcessingException e) { - logger.warn("Error logging missing invocation context."); - } + context.recordContextLossInvocation(entry); } else { throw new NoThreadContextException(id); } diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py index afe20f7..7b205a0 100755 --- a/symbolic-explorer/constraint/ConstraintController.py +++ b/symbolic-explorer/constraint/ConstraintController.py @@ -38,6 +38,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str trace = request.trace inputs = request.inputs ufs = request.ufs + missingInvocations = request.missingInvocations symbolicContextLoss = request.symbolicContextLoss symbolicPrecisionLoss = request.symbolicPrecisionLoss referenceSemanticChange = request.referenceSemanticChange @@ -49,6 +50,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str 'trace': trace, 'inputs': inputs, 'ufs': ufs, + 'missing_invocations': missingInvocations, 'symbolic_context_loss': symbolicContextLoss, 'symbolic_precision_loss': symbolicPrecisionLoss, 'reference_semantic_change': referenceSemanticChange}) diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py index 89831e6..14cee24 100755 --- a/symbolic-explorer/constraint/ConstraintService.py +++ b/symbolic-explorer/constraint/ConstraintService.py @@ -4,7 +4,7 @@ from data.trace.Input import Input from data.trace.UF import UF -from parse.DataTransferObjects import TraceItem, InputItem, UFItem +from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem from data.trace.Special import Special from data.trace.Branch import Branch @@ -23,7 +23,8 @@ class ConstraintService: @staticmethod def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inputs: List[InputItem], ufs: List[UFItem], symbolic_context_loss: bool, symbolic_precision_loss: bool, - reference_semantic_change: bool = False): + reference_semantic_change: bool = False, + missing_invocations: List[InvocationItem] = None): """ Adds constraints to the database. @@ -40,6 +41,7 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp symbolic_context_loss (bool): A flag indicating whether the symbolic context was lost. symbolic_precision_loss (bool): A flag indicating whether the symbolic precision was lost (UFs introduced). reference_semantic_change (bool): A flag indicating whether reference equality semantics changed. + missing_invocations (list): Methods that could not be modelled symbolically during this trace. Returns: None: The result is the side effect of adding data to the database. @@ -50,6 +52,9 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp # logger.info(f'[CONSTRAINT SERVICE] Parsed trace: {[t.__str__() for t in trace_parsed]}') inputs_parsed: List[Input] = Parser.parse_inputs(inputs) ufs_parsed: List[UF] = Parser.parse_ufs(ufs) + # Flatten the missing-invocation DTOs into plain dicts so the Database/Tree stay decoupled + # from the pydantic request models. + missing_invocations_data = [item.model_dump() for item in (missing_invocations or [])] # Adding the trace and inputs to the database for the specified endpoint. - Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change) + Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data) logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}') diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py index 6636395..20f8d48 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -37,6 +37,13 @@ def __init__(self, endpoint_id: Union[str, int]): self.uncaught_exceptions: int = 0 self.symbolic_vars: Set = set() self.ufs: Set = set() + # Missing invocations accumulated across all traces of this testcase, keyed by + # (owner, name, desc, isInstance, isSymbolic). Each value aggregates count and context_loss. + self.missing_invocations: dict = {} + # Execution errors detected in the executor's stdout (internal SWAT assertions or + # [SWAT Exception]s) that make the verdict untrustworthy. These cannot ride the trace + # because they halt the executor JVM before it sends one, so they are surfaced here. + self.execution_errors: list = [] def record_inputs(self, inputs: List[Input]): @@ -60,6 +67,52 @@ def record_ufs(self, ufs: List[UF]): self.ufs.add(uf.definition) + def record_missing_invocations(self, invocations: Optional[List[dict]]): + """ + Accumulates missing invocations across all traces of this testcase. + + Args: + invocations (list): Dicts with keys owner, name, desc, isInstance, isSymbolic, + contextLoss, count. Entries are deduped by + (owner, name, desc, isInstance, isSymbolic); counts are summed and contextLoss + is OR-ed across traces. The full set is the superset of missing invocations; + entries with context_loss=True form the context-loss subset. + """ + if not invocations: + return + for inv in invocations: + key = (inv['owner'], inv['name'], inv['desc'], inv['isInstance'], inv['isSymbolic']) + count = int(inv.get('count', 1)) + context_loss = bool(inv.get('contextLoss', False)) + existing = self.missing_invocations.get(key) + if existing is None: + self.missing_invocations[key] = { + 'owner': inv['owner'], + 'name': inv['name'], + 'desc': inv['desc'], + 'isInstance': inv['isInstance'], + 'isSymbolic': inv['isSymbolic'], + 'context_loss': context_loss, + 'count': count, + } + else: + existing['count'] += count + existing['context_loss'] = existing['context_loss'] or context_loss + + def record_execution_error(self, kind: str, message: str): + """ + Records an execution error surfaced from the executor's stdout. + + Deduplicated by (kind, message) so repeated exploration rounds don't inflate the list. + + Args: + kind (str): A short category, e.g. "swat_assertion" or "swat_exception". + message (str): The offending output line. + """ + entry = {'kind': kind, 'message': message} + if entry not in self.execution_errors: + self.execution_errors.append(entry) + def record_context_loss(self): logger.warning("Context loss recorded!") self.symbolic_context_loss = True diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index e4866a8..489190b 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -114,7 +114,7 @@ def get_endpoints(self): def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF], symbolic_context_loss: bool, symbolic_precision_loss: bool, - reference_semantic_change: bool = False): + reference_semantic_change: bool = False, missing_invocations: list = None): endpoint_id = str(endpoint_id) lock.acquire() @@ -124,6 +124,7 @@ def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Bra self.tree[endpoint_id].add(trace, inputs, ufs) self.tree[endpoint_id].record_inputs(inputs) self.tree[endpoint_id].record_ufs(ufs) + self.tree[endpoint_id].record_missing_invocations(missing_invocations) self.tree[endpoint_id].record_context_loss() if symbolic_context_loss else None self.tree[endpoint_id].record_precision_loss() if symbolic_precision_loss else None self.tree[endpoint_id].record_reference_semantic_change() if reference_semantic_change else None @@ -155,6 +156,12 @@ def record_uncaught_exception(self, endpoint_id: Union[str, int]): self.tree[endpoint_id].uncaught_exceptions += 1 lock.release() + def record_execution_error(self, endpoint_id: Union[str, int], kind: str, message: str): + endpoint_id = str(endpoint_id) + lock.acquire() + self.tree[endpoint_id].record_execution_error(kind, message) + lock.release() + def add_solution(self, branch_id: int, sol: Any, inputs: List[Input], endpoint_id: Union[str, int]): lock.acquire() self.solutions[branch_id] = Solution(sol=sol, inputs=inputs, endpoint_id=endpoint_id) diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a0081e8..0fec004 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -17,6 +17,7 @@ from enum import Enum from svcomp.SymbolicStorage import SymbolicStorage +from svcomp.TestcaseStats import write_testcase_stats from timing.TimingManager import TimingManager @@ -139,8 +140,9 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac for l in output: if "java.lang.AssertionError: [SWAT]" in l: - # Internal assertion error in the DSE + # Internal assertion error in the DSE logger.critical(f'[SVCOMP] SWAT Assertion failed: {l}') + Database.instance().record_execution_error(ENDPOINT_ID, 'swat_assertion', l.strip()) self.state.verdict = Verdict.UNKNOWN return Action.REPORTVERDICT if "java.lang.AssertionError" in l and self.verification_category == VerificationCategory.VALID_ASSERT_PRP: @@ -156,6 +158,7 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac Database.instance().record_uncaught_exception(ENDPOINT_ID) if "[SWAT Exception]:" in l: logger.info(f'[SVCOMP] SWAT Exception: {l}') + Database.instance().record_execution_error(ENDPOINT_ID, 'swat_exception', l.strip()) self.state.verdict = Verdict.UNKNOWN return Action.REPORTVERDICT @@ -329,6 +332,11 @@ def run(self): timing_file = os.path.join(log_dir, 'timing_data.json') TimingManager.instance().save_to_file(Path(timing_file)) + # Write the consolidated per-testcase statistics (verdict, soundness flags, missing + # invocations and the context-loss subset) so the analysis can rely on structured data. + stats_file = os.path.join(log_dir, 'stats.json') + write_testcase_stats(Path(stats_file), verdict, self.verification_category, Database.instance().get_tree(ENDPOINT_ID)) + self.kill_current_process() diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index be30d85..4d46be7 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -22,10 +22,26 @@ class InputItem(BaseModel): upperBound: str +class InvocationItem(BaseModel): + """A method invocation that could not be modelled symbolically during execution. + + The full list is the superset of missing invocations; entries with ``contextLoss`` set are the + dangerous subset that received symbolic arguments and caused symbolic context loss. + """ + owner: str + name: str + desc: str + isInstance: bool + isSymbolic: bool + contextLoss: bool + count: int + + class ConstraintRequest(BaseModel): trace: List[TraceItem] inputs: List[InputItem] ufs: List[UFItem] + missingInvocations: List[InvocationItem] = [] symbolicContextLoss: bool symbolicPrecisionLoss: bool referenceSemanticChange: bool = False diff --git a/symbolic-explorer/svcomp/TestcaseStats.py b/symbolic-explorer/svcomp/TestcaseStats.py new file mode 100644 index 0000000..830f042 --- /dev/null +++ b/symbolic-explorer/svcomp/TestcaseStats.py @@ -0,0 +1,81 @@ +""" +Consolidated per-testcase statistics for SV-COMP runs. + +The Symbolic Explorer owns the per-testcase output: after a testcase completes it writes a single +``stats.json`` into the log directory containing the verdict, the soundness-relevant flags, and the +methods that could not be modelled symbolically. This replaces the executor-written ``stats_*.json`` +files and lets the analysis rely on authoritative structured data instead of scraping logs. + +The missing-invocation list is the superset; entries with ``context_loss=True`` are the dangerous +subset that received symbolic arguments and caused symbolic context loss. This makes the +superset/subset relationship explicit (see issue #25), rather than inferring it from regexes. +""" + +import json +from pathlib import Path + +import log + +logger = log.get_logger() + + +def _signature(inv: dict) -> str: + """Render a missing invocation as a stable ``owner/name:desc`` signature.""" + return f"{inv['owner']}/{inv['name']}:{inv['desc']}" + + +def build_testcase_stats(verdict, category, tree) -> dict: + """ + Assemble the consolidated per-testcase statistics dictionary. + + Args: + verdict: The final (post-downgrade) Verdict enum for the testcase. + category: The VerificationCategory enum for the property. + tree: The per-endpoint Tree holding accumulated metadata for the testcase. + + Returns: + A JSON-serializable dict describing the testcase outcome. + """ + # Order: context-loss culprits first, then by signature, for readable output. + missing = sorted( + tree.missing_invocations.values(), + key=lambda i: (not i['context_loss'], i['owner'], i['name'], i['desc']), + ) + context_loss_methods = sorted({_signature(i) for i in missing if i['context_loss']}) + + return { + 'property': category.value, + 'verdict': verdict.name, + 'verdict_raw': verdict.value, + 'soundness': { + 'symbolic_context_loss': tree.symbolic_context_loss, + 'symbolic_precision_loss': tree.symbolic_precision_loss, + 'reference_semantic_change': tree.reference_semantic_change, + 'uncaught_exceptions': tree.uncaught_exceptions, + }, + 'symbolic_vars': sorted(tree.symbolic_vars), + 'missing_invocations': missing, + 'context_loss_methods': context_loss_methods, + 'execution_errors': list(tree.execution_errors), + 'counts': { + 'missing_invocations': len(missing), + 'context_loss_invocations': sum(1 for i in missing if i['context_loss']), + 'execution_errors': len(tree.execution_errors), + }, + } + + +def write_testcase_stats(filepath: Path, verdict, category, tree): + """Write the consolidated per-testcase statistics to ``filepath`` as JSON.""" + data = build_testcase_stats(verdict, category, tree) + + filepath.parent.mkdir(parents=True, exist_ok=True) + with open(filepath, 'w') as f: + json.dump(data, f, indent=2) + + logger.info( + f"[STATS] Saved testcase stats to {filepath} " + f"({data['counts']['missing_invocations']} missing invocations, " + f"{data['counts']['context_loss_invocations']} context-loss, " + f"{data['counts']['execution_errors']} execution errors)" + ) From d2c67084533f5a7190b40e636814c9dfa2512889 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Tue, 16 Jun 2026 16:43:59 +0000 Subject: [PATCH 2/2] feat(sv-comp): runs/run_/ layout, stats.json analysis, CLI consolidation Implements the remaining issue #25 parts in the svcomp CLI (lib/ + commands/): - Run folder structure: each `svcomp test run` writes its per-testcase logs and aggregated results under one timestamped runs/run_/{logs,results} dir (runs-debug//run_/logs for debug configs). Previous runs are kept; a single run timestamp is threaded through command generation and result writing. - Analysis on stats.json: rewrote lib/analysis/context_loss.py to read each testcase's consolidated stats.json instead of scraping explorer.log / stats_*.json. It pairs a run's results with its logs and reports the missing-invocation superset and its authoritative context-loss subset, fixing the old regex inconsistency. - Scoring summary: `svcomp analyze results` prints a Correct/Failed/Unk/Error/Timeout table per category and overall. - Consolidation: run_locally.sh and ci_run.sh now invoke `./svcomp test run`; the dead legacy top-level duplicates are removed (target_execution.py, command_generation.py, analyse_ctx_loss.py, analyze_by_correctness.py, compare_results.py, target_selection.py, witness_validation.py, util.py, dtypes.py). README and .gitignore updated. Closes #25. Co-Authored-By: Claude Opus 4.8 (1M context) --- .gitignore | 2 + targets/sv-comp/scripts/README.md | 64 +- targets/sv-comp/scripts/analyse_ctx_loss.py | 399 ---------- .../sv-comp/scripts/analyze_by_correctness.py | 211 ------ targets/sv-comp/scripts/ci_run.sh | 7 +- targets/sv-comp/scripts/command_generation.py | 115 --- targets/sv-comp/scripts/commands/analyze.py | 57 +- targets/sv-comp/scripts/commands/test.py | 9 +- targets/sv-comp/scripts/commands/util.py | 22 +- targets/sv-comp/scripts/compare_results.py | 56 -- targets/sv-comp/scripts/dtypes.py | 38 - .../scripts/lib/analysis/context_loss.py | 552 +++++--------- targets/sv-comp/scripts/lib/command_gen.py | 31 +- targets/sv-comp/scripts/lib/execution.py | 47 +- targets/sv-comp/scripts/run_locally.sh | 2 +- targets/sv-comp/scripts/target_execution.py | 703 ------------------ targets/sv-comp/scripts/target_selection.py | 90 --- targets/sv-comp/scripts/util.py | 10 - targets/sv-comp/scripts/witness_validation.py | 187 ----- 19 files changed, 321 insertions(+), 2281 deletions(-) delete mode 100644 targets/sv-comp/scripts/analyse_ctx_loss.py delete mode 100644 targets/sv-comp/scripts/analyze_by_correctness.py delete mode 100644 targets/sv-comp/scripts/command_generation.py delete mode 100644 targets/sv-comp/scripts/compare_results.py delete mode 100644 targets/sv-comp/scripts/dtypes.py delete mode 100644 targets/sv-comp/scripts/target_execution.py delete mode 100644 targets/sv-comp/scripts/target_selection.py delete mode 100644 targets/sv-comp/scripts/util.py delete mode 100644 targets/sv-comp/scripts/witness_validation.py diff --git a/.gitignore b/.gitignore index 761ca1c..57b3d54 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,8 @@ targets/applications/openolat/libs/z3/ **/logs/ **/logs-debug/ **/results/ +**/runs/ +**/runs-debug/ **/*.class /build/ **/build/ diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md index 5992b85..22ce37c 100644 --- a/targets/sv-comp/scripts/README.md +++ b/targets/sv-comp/scripts/README.md @@ -27,7 +27,7 @@ scripts/ ├── svcomp.py # Main CLI entry point ├── lib/ # Library modules (refactored from original scripts) │ ├── __init__.py -│ ├── analysis.py # (was analyse_ctx_loss.py) +│ ├── analysis/ # context_loss.py (was analyse_ctx_loss.py) + timing/failures/performance │ ├── command_gen.py # (was command_generation.py) │ ├── comparison.py # (was compare_results.py) │ ├── dtypes.py # (unchanged) @@ -86,19 +86,35 @@ scripts/ ### Analysis Commands ```bash -# Analyze latest results for context losses +# Analyze the latest run: scoring summary (Correct/Failed/Unk/Error/Timeout) plus +# the missing-invocation superset and its context-loss subset, read from each +# testcase's stats.json (no log scraping) ./svcomp analyze results -# Analyze specific results file -./svcomp analyze results path/to/results.json +# Analyze a specific run directory +./svcomp analyze results runs/run_20260101_120000 # Compare two result files -./svcomp analyze compare results/old.json results/new.json +./svcomp analyze compare runs/run_A/results/results_valid-assert.prp_*.json \ + runs/run_B/results/results_valid-assert.prp_*.json # Show test case statistics ./svcomp analyze stats ``` +### Run output + +Each `./svcomp test run` writes everything for that run under one timestamped directory, +so previous runs are preserved: + +``` +runs/run_/ +├── logs//_/ # explorer.log, stats.json, timing_data.json, ... +└── results/ # results__.json, stage_timing.csv, histograms +``` + +Debug runs (a `*-debug.cfg`) are grouped per target instead: `runs-debug///run_/logs/`. + ### Utility Commands ```bash @@ -127,17 +143,18 @@ scripts/ ## Migration Notes -### Old Scripts (Still Available) +### Old Scripts (Removed) -The original Python scripts are still in the `scripts/` directory and can be used directly if needed: -- `target_selection.py` -- `command_generation.py` -- `target_execution.py` -- `witness_validation.py` -- `analyse_ctx_loss.py` -- `compare_results.py` +The original top-level scripts have been removed; their functionality lives in `lib/` and is driven through the `./svcomp` CLI: +- `target_selection.py` → `lib/selection.py` +- `command_generation.py` → `lib/command_gen.py` +- `target_execution.py` → `lib/execution.py` +- `witness_validation.py` → `lib/witness.py` +- `analyse_ctx_loss.py` → `lib/analysis/context_loss.py` +- `compare_results.py` → `lib/comparison.py` +- `util.py` → `lib/utils.py`, `dtypes.py` → `lib/dtypes.py` -However, **it's recommended to use the new CLI** for better user experience. +`run_locally.sh` and `ci_run.sh` now invoke `./svcomp test run`. ### Key Changes @@ -147,11 +164,9 @@ However, **it's recommended to use the new CLI** for better user experience. 4. **Relative Imports**: Library modules use relative imports for better packaging 5. **Wrapper Script**: `svcomp` wrapper automatically uses the venv Python -### Backwards Compatibility +### Programmatic Use -- Old scripts still work as before -- Library functions are exposed through `lib/__init__.py` -- Can import and use functions programmatically: +- Library functions are exposed through `lib/__init__.py`: ```python from lib import extract_testcases, generate_commands, run_parallel ``` @@ -171,10 +186,10 @@ However, **it's recommended to use the new CLI** for better user experience. - [ ] Improve error messages and validation - [ ] Add shell completion support -**Phase 3: 🔜 Future** -- [ ] Add deprecation warnings to old scripts -- [ ] Update documentation -- [ ] Consider removing old scripts +**Phase 3: ✅ Complete** +- ✅ Removed the legacy top-level scripts (consolidated into `lib/`) +- ✅ `run_locally.sh` / `ci_run.sh` use the `./svcomp` CLI +- ✅ `runs/run_/{logs,results}` output layout; analysis reads per-testcase `stats.json` ## Examples @@ -190,11 +205,8 @@ However, **it's recommended to use the new CLI** for better user experience. # Run tests for specific category ./svcomp test run --categories valid-assert.prp --workers 30 -# Analyze results +# Analyze the latest run ./svcomp analyze results - -# Compare with previous run -./svcomp analyze compare results/old.json results/new.json ``` ### Development Workflow diff --git a/targets/sv-comp/scripts/analyse_ctx_loss.py b/targets/sv-comp/scripts/analyse_ctx_loss.py deleted file mode 100644 index f8019d6..0000000 --- a/targets/sv-comp/scripts/analyse_ctx_loss.py +++ /dev/null @@ -1,399 +0,0 @@ -#!/usr/bin/env python3 -""" -Analyze SV-Comp results to identify context loss methods that need implementation. -Run this script in the directory containing the results JSON file. - -Usage: python3 analyse_ctx_loss.py results_valid-assert.prp_XXXXXX.json -""" - -import json -import sys -import re -from collections import defaultdict -from pathlib import Path - - -def extract_context_loss_methods(log_content: str) -> list[str]: - """Extract all method names causing context loss from log content.""" - methods = set() # Use set to dedupe - if not log_content: - return list(methods) - - # Look for "Context loss:" pattern - for match in re.finditer(r'Context loss:\s*(.+?)(?:\n|$)', log_content): - methods.add(match.group(1).strip()) - - # Also look for "Uninstrumented invocation" pattern - for match in re.finditer(r'Uninstrumented invocation.*?:\s*(.+?)(?:\n|$)', log_content): - methods.add(match.group(1).strip()) - - # Look for "Context loss recorded" with method info on previous lines - for match in re.finditer(r'(\S+\.\S+)\s*\n.*Context loss recorded', log_content): - methods.add(match.group(1).strip()) - - return list(methods) - - -def extract_missing_invocations(log_content: str) -> list[str]: - """Extract missing/unimplemented method invocations from log content.""" - methods = set() # Use set to dedupe - if not log_content: - return list(methods) - - # Pattern: "Error visiting Instruction INVOKE* owner/class/method:desc" - # Example: "Error visiting Instruction INVOKEVIRTUAL java/lang/Double/byteValue:()B" - for match in re.finditer( - r'Error visiting Instruction (INVOKE\w+)\s+(\S+?)(?:\s*\(|$)', - log_content - ): - invoke_type = match.group(1) - method_sig = match.group(2) - # Clean up the method signature (remove id info if present) - method_sig = re.sub(r'\s*\(id:.*', '', method_sig) - methods.add(f"{invoke_type} {method_sig}") - - # Pattern: "Not implemented: in " - for match in re.finditer(r'Not implemented:\s*(.+?)\s+in\s+(\S+)', log_content): - method = match.group(1).strip() - cls = match.group(2).strip() - methods.add(f"NOT_IMPLEMENTED {cls}/{method}") - - return list(methods) - - -def extract_symbolic_invocations_from_stats(stats_path: Path) -> list[str]: - """ - Extract symbolic method invocations from stats JSON files. - - Stats files contain entries like: - {"owner":"java/lang/Character","isSymbolic":true,"name":"isUnicodeIdentifierStart","desc":"(I)Z"} - - Returns list of method signatures that have isSymbolic=true (missing implementations). - """ - methods = set() - - # Check both stats_1.json and stats_-1.json - for stats_file in ['stats_1.json', 'stats_-1.json']: - file_path = stats_path / stats_file - if not file_path.exists(): - continue - - try: - with open(file_path) as f: - data = json.load(f) - - if isinstance(data, list): - for entry in data: - if isinstance(entry, dict) and entry.get('isSymbolic', False): - owner = entry.get('owner', '') - name = entry.get('name', '') - desc = entry.get('desc', '') - is_instance = entry.get('isInstance', False) - invoke_type = 'INVOKEVIRTUAL' if is_instance else 'INVOKESTATIC' - if owner and name: - methods.add(f"{invoke_type} {owner}/{name}:{desc}") - except (json.JSONDecodeError, IOError): - pass - - return list(methods) - - -def extract_errors(log_content: str) -> list[str]: - """Extract error messages from log content.""" - errors = [] - if not log_content: - return errors - - # Look for SWAT Exception patterns - for match in re.finditer(r'\[SWAT Exception\]:\s*(.+?)(?:\n|$)', log_content): - errors.append(match.group(1).strip()) - - # Look for general exceptions - for match in re.finditer(r'Exception.*?:\s*(.+?)(?:\n|$)', log_content): - msg = match.group(1).strip() - if msg and len(msg) < 200: - errors.append(msg) - - return errors - - -def get_log_dir(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the log directory for a given task. - - Task name format: folder/testname (e.g., "objects/objects03") - Log dir format: logs//_/ - """ - parts = task_name.split('/') - if len(parts) >= 2: - folder = parts[0] - testname = parts[1] - else: - folder = "" - testname = parts[0] - - # Property name like "valid-assert.prp" -> "valid-assert" - prop_short = property_name.replace('.prp', '') - - return logs_dir / folder / f"{testname}_{prop_short}" - - -def get_log_path(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the explorer.log for a given task. - """ - return get_log_dir(logs_dir, task_name, property_name) / "explorer.log" - - -def get_stats_dir(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the stats directory (logs/ subdirectory) for a given task. - """ - return get_log_dir(logs_dir, task_name, property_name) / "logs" - - -def read_log_file(log_path: Path) -> str: - """Read log file content, return empty string if not found.""" - try: - if log_path.exists(): - return log_path.read_text(errors='replace') - except Exception: - pass - return "" - - -def main(): - if len(sys.argv) < 2: - # Find the latest results file - results_dir = Path('.') - json_files = list(results_dir.glob('results_*.json')) - if not json_files: - json_files = list(Path('results').glob('results_*.json')) - if not json_files: - print("Usage: python3 analyse_ctx_loss.py ") - print("No results files found in current directory") - sys.exit(1) - results_file = max(json_files, key=lambda p: p.stat().st_mtime) - print(f"Using latest results file: {results_file}") - else: - results_file = Path(sys.argv[1]) - - # Determine logs directory (sibling to results file or parent's logs/) - if results_file.parent.name == 'results': - logs_dir = results_file.parent.parent / 'logs' - else: - logs_dir = results_file.parent / 'logs' - - print(f"Looking for logs in: {logs_dir}") - - with open(results_file) as f: - data = json.load(f) - - results = data['results'] - category = data.get('category', 'valid-assert.prp') - - # Analyze all 0-point tasks - zero_points_by_folder = defaultdict(list) - context_loss_methods = defaultdict(list) - missing_invocations = defaultdict(list) - all_errors = defaultdict(list) - - for name, task in results.items(): - # task format: [status_change, points, execution_status, error_bool, validated, time] - points = task[1] - if points == 0: - folder = name.split('/')[0] - status = task[0] - exec_status = task[2] - - # Read the actual log file from disk - log_path = get_log_path(logs_dir, name, category) - log_content = read_log_file(log_path) - - # Get stats directory for symbolic invocations - stats_dir = get_stats_dir(logs_dir, name, category) - - zero_points_by_folder[folder].append({ - 'name': name, - 'status': status, - 'exec_status': exec_status, - 'log_path': str(log_path), - 'log_content': log_content, - 'log_exists': log_path.exists(), - 'stats_dir': str(stats_dir) - }) - - # Extract context loss methods - methods = extract_context_loss_methods(log_content) - for method in methods: - context_loss_methods[method].append(name) - - # Extract missing invocations from error logs - invocations = extract_missing_invocations(log_content) - for inv in invocations: - missing_invocations[inv].append(name) - - # Extract symbolic invocations from stats JSON files - symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir) - for inv in symbolic_invocations: - missing_invocations[inv].append(name) - - # Extract errors - errors = extract_errors(log_content) - for error in errors: - all_errors[error].append(name) - - # Print summary by folder - print("\n" + "=" * 80) - print("TASKS WITH 0 POINTS BY FOLDER") - print("=" * 80) - total_zero = 0 - logs_found = 0 - for folder, tasks in sorted(zero_points_by_folder.items(), key=lambda x: -len(x[1])): - folder_logs_found = sum(1 for t in tasks if t['log_exists']) - print(f"{folder}: {len(tasks)} tasks ({folder_logs_found} logs found)") - total_zero += len(tasks) - logs_found += folder_logs_found - print(f"\nTotal: {total_zero} tasks with 0 points ({logs_found} logs found)") - - # Print context loss methods sorted by frequency - print("\n" + "=" * 80) - print("CONTEXT LOSS METHODS (sorted by frequency)") - print("=" * 80) - - if not context_loss_methods: - print("No context loss methods found in logs.") - else: - for method, tasks in sorted(context_loss_methods.items(), key=lambda x: -len(x[1])): - print(f"\n{len(tasks):3d} tasks - {method}") - print(f" Examples: {', '.join(tasks[:3])}") - - # Print missing invocations sorted by frequency - print("\n" + "=" * 80) - print("MISSING/UNIMPLEMENTED INVOCATIONS (sorted by frequency)") - print("=" * 80) - - if not missing_invocations: - print("No missing invocations found in logs.") - else: - for inv, tasks in sorted(missing_invocations.items(), key=lambda x: -len(x[1])): - # Dedupe task list (same task may appear multiple times) - unique_tasks = list(dict.fromkeys(tasks)) - print(f"\n{len(unique_tasks):3d} tasks - {inv}") - print(f" Examples: {', '.join(unique_tasks[:3])}") - - # Print errors sorted by frequency - print("\n" + "=" * 80) - print("ERRORS (sorted by frequency)") - print("=" * 80) - - if not all_errors: - print("No specific errors found in logs.") - else: - for error, tasks in sorted(all_errors.items(), key=lambda x: -len(x[1]))[:20]: - print(f"\n{len(tasks):3d} tasks - {error[:100]}") - print(f" Examples: {', '.join(tasks[:3])}") - - # Detailed breakdown for each folder - print("\n" + "=" * 80) - print("DETAILED BREAKDOWN BY FOLDER") - print("=" * 80) - - for folder in ['autostub', 'jbmc-regression', 'java-ranger-regression', 'algorithms', 'argv-tasks', 'float-nonlinear-calculation', 'securibench', 'objects']: - if folder not in zero_points_by_folder: - continue - - print(f"\n--- {folder} ({len(zero_points_by_folder[folder])} tasks) ---") - - folder_context_loss = defaultdict(list) - folder_missing_invocations = defaultdict(list) - folder_errors = defaultdict(list) - other_issues = defaultdict(list) - tasks_with_missing_invocations = set() - - for task in zero_points_by_folder[folder]: - log_content = task['log_content'] - stats_dir = Path(task['stats_dir']) - methods = extract_context_loss_methods(log_content) - invocations = extract_missing_invocations(log_content) - symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir) - errors = extract_errors(log_content) - - if methods: - for method in methods: - folder_context_loss[method].append(task['name']) - - all_invocations = invocations + symbolic_invocations - if all_invocations: - tasks_with_missing_invocations.add(task['name']) - for inv in all_invocations: - folder_missing_invocations[inv].append(task['name']) - - # Always categorize by verdict/status (not just when no missing invocations) - if errors: - for error in errors: - folder_errors[error[:80]].append(task['name']) - - if 'timeout' in task['exec_status'].lower(): - other_issues['timeout'].append(task['name']) - elif not task['log_exists']: - other_issues['log file not found'].append(task['name']) - elif not log_content.strip(): - other_issues['log file empty'].append(task['name']) - elif 'DONT-KNOW' in log_content: - other_issues['verdict: DONT-KNOW'].append(task['name']) - elif 'NoThreadContextException' in log_content: - other_issues['NoThreadContextException'].append(task['name']) - elif not methods and not all_invocations: - other_issues['unknown (check log)'].append(task['name']) - - if folder_context_loss: - print(" Context loss methods:") - for method, tasks in sorted(folder_context_loss.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {method[:80]}") - - if folder_missing_invocations: - print(f" Missing invocations ({len(tasks_with_missing_invocations)} unique tasks):") - for inv, tasks in sorted(folder_missing_invocations.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {inv[:80]}") - - if folder_errors: - print(" Errors:") - for error, tasks in sorted(folder_errors.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {error[:80]}") - - if other_issues: - print(" Other issues:") - for issue, tasks in sorted(other_issues.items(), key=lambda x: -len(x[1])): - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {issue[:80]}") - - # Print sample logs for debugging - print("\n" + "=" * 80) - print("SAMPLE LOGS (first 5 tasks with 0 points)") - print("=" * 80) - - count = 0 - for name, task in results.items(): - if task[1] == 0 and count < 5: - log_path = get_log_path(logs_dir, name, category) - log_content = read_log_file(log_path) - - print(f"\n{name}:") - print(f" Status: {task[0]}") - print(f" Exec status: {task[2]}") - print(f" Log path: {log_path}") - print(f" Log exists: {log_path.exists()}") - if log_content: - # Show last 500 chars which usually has the verdict - print(f" Log tail: ...{log_content[-500:]}") - else: - print(f" Log: (empty or not found)") - count += 1 - - -if __name__ == '__main__': - main() diff --git a/targets/sv-comp/scripts/analyze_by_correctness.py b/targets/sv-comp/scripts/analyze_by_correctness.py deleted file mode 100644 index feaa4df..0000000 --- a/targets/sv-comp/scripts/analyze_by_correctness.py +++ /dev/null @@ -1,211 +0,0 @@ -#!/usr/bin/env python3 -""" -Analyze timing data grouped by verdict correctness. -""" -import json -from pathlib import Path -import statistics - -# Find most recent results file -results_dir = Path(__file__).resolve().parent.parent / 'results' -results_files = sorted(results_dir.glob('*.json'), key=lambda p: p.stat().st_mtime, reverse=True) - -if not results_files: - print("No results files found!") - exit(1) - -results_file = results_files[0] -print(f"Loading: {results_file.name}") -print(f"Note: Filtering out testcases with solver_count == 0") - -# Extract property from results filename (e.g., "valid-assert" from "results_valid-assert.prp_...") -results_filename = results_file.name -property_suffix = None -if results_filename.startswith("results_") and ".prp_" in results_filename: - property_part = results_filename[len("results_"):results_filename.index(".prp_")] - property_suffix = "_" + property_part - print(f"Detected property suffix: {property_suffix}") - -# Debug: count how many we skip -skipped_count = 0 -processed_count = 0 - -# Load results -with open(results_file) as f: - results = json.load(f) - -# Load timing data -log_dir = Path(__file__).resolve().parent.parent / 'logs' -timing_files = {tf.parent.name: tf for tf in log_dir.rglob('timing_data.json')} - -# Group testcases by different categories -correct = [] # All correct: expected == actual (TP + TN) -true_correct = [] # True Positives: violation -> violation -true_negative = [] # True Negatives: safe -> safe -false_results = [] # False Positives + False Negatives: expected != actual (excluding unknown/crash) -incorrect = [] # All incorrect: expected != actual (including unknown/crash) - -# Parse results structure: results[testcase_name] = [case_occurrence, points, status, dse_error, witness, elapsed, timing] -for testcase_name, result_data in results.get('results', {}).items(): - if not isinstance(result_data, list) or len(result_data) < 7: - continue - - case_occurrence = result_data[0] # e.g., "safe -> unknown" or "violation -> violation" - timing_breakdown = result_data[6] # Dict with timing data - - # Parse expected -> actual from case_occurrence - parts = case_occurrence.split(' -> ') - if len(parts) != 2: - continue - expected, actual = parts - - # Get timing data - try: - # Convert testcase name to directory name - # e.g., 'objects/objects08' -> 'objects08_valid-assert' - if '/' in testcase_name: - # Remove category prefix (everything before and including '/') - testcase_short = testcase_name.split('/')[-1] - else: - testcase_short = testcase_name - - # Add property suffix if detected - if property_suffix: - testcase_dir = testcase_short + property_suffix - else: - testcase_dir = testcase_short - - # Check if timing file exists to get solver_count - timing_file = timing_files.get(testcase_dir) - if timing_file: - with open(timing_file) as f: - timing_data_full = json.load(f) - solver_count = timing_data_full.get('statistics', {}).get('solver_count', 0) - # Skip testcases with zero solver calls - if solver_count == 0: - skipped_count += 1 - continue - else: - processed_count += 1 - else: - # No timing file found, skip this testcase - skipped_count += 1 - continue - - total_time = timing_breakdown.get('total_time', 0) - executor = timing_breakdown.get('symbolic_executor', 0) - solver = timing_breakdown.get('smt_solver', 0) - witness_gen = timing_breakdown.get('witness_generation', 0) - witness_val = timing_breakdown.get('witness_validation', 0) - - # Compute corrected explorer time as residual - corrected_explorer = max(0.0, total_time - executor - solver - witness_gen - witness_val) - - timing_entry = { - 'name': testcase_name, - 'total': total_time, - 'executor': executor, - 'solver': solver, - 'explorer': corrected_explorer, - 'witness_gen': witness_gen, - 'witness_val': witness_val, - 'expected': expected, - 'actual': actual, - 'case': case_occurrence - } - - # Categorize into groups - is_correct = (expected == actual) - - if is_correct: - correct.append(timing_entry) - if actual == 'violation': # True Positive - true_correct.append(timing_entry) - elif actual == 'safe': # True Negative - true_negative.append(timing_entry) - - if not is_correct: - incorrect.append(timing_entry) - # False results = incorrect but not unknown/crash - if actual not in ['unknown', 'crash']: - false_results.append(timing_entry) - - except Exception as e: - print(f"Error processing {testcase_name}: {e}") - -print(f"\n{'='*70}") -print(f"FILTERING RESULTS") -print(f"{'='*70}") -print(f"Skipped (no timing file or solver_count=0): {skipped_count}") -print(f"Processed (solver_count > 0): {processed_count}") - -print(f"\n{'='*70}") -print(f"RESULTS SUMMARY") -print(f"{'='*70}") -print(f"Correct (expected == actual): {len(correct):>4} testcases") -print(f" - True Correct (violation->violation): {len(true_correct):>4} testcases") -print(f" - True Negative (safe->safe): {len(correct)-len(true_correct):>4} testcases") -print(f"Incorrect (expected != actual): {len(incorrect):>4} testcases") -print(f" - False Results (not unknown/crash): {len(false_results):>4} testcases") -print(f" - Unknown/Crash: {len(incorrect)-len(false_results):>4} testcases") -print(f"Total: {len(correct) + len(incorrect):>4} testcases") - -def compute_stats(group, group_name): - if not group: - print(f"\n{group_name}: No data") - return - - print(f"\n{'='*70}") - print(f"{group_name} ({len(group)} testcases)") - print(f"{'='*70}") - - # Compute mean - mean_stats = { - 'executor': statistics.mean(t['executor'] for t in group), - 'solver': statistics.mean(t['solver'] for t in group), - 'explorer': statistics.mean(t['explorer'] for t in group), - 'witness_gen': statistics.mean(t['witness_gen'] for t in group), - 'witness_val': statistics.mean(t['witness_val'] for t in group), - } - mean_total = sum(mean_stats.values()) - - print("\nMEAN:") - for key, val in mean_stats.items(): - pct = (val / mean_total * 100) if mean_total > 0 else 0 - print(f" {key:<20} {val:>8.2f}s ({pct:>5.1f}%)") - print(f" {'Total':<20} {mean_total:>8.2f}s") - - # Compute median - median_stats = { - 'executor': statistics.median(t['executor'] for t in group), - 'solver': statistics.median(t['solver'] for t in group), - 'explorer': statistics.median(t['explorer'] for t in group), - 'witness_gen': statistics.median(t['witness_gen'] for t in group), - 'witness_val': statistics.median(t['witness_val'] for t in group), - } - median_total = sum(median_stats.values()) - - print("\nMEDIAN:") - for key, val in median_stats.items(): - pct = (val / median_total * 100) if median_total > 0 else 0 - print(f" {key:<20} {val:>8.2f}s ({pct:>5.1f}%)") - print(f" {'Total':<20} {median_total:>8.2f}s") - - # Show distribution for solver (all should have solver_count > 0 due to filtering) - solver_times = [t['solver'] for t in group] - zero_time = sum(1 for s in solver_times if s == 0.0) - print(f"\nSolver time distribution (all have solver_count > 0):") - print(f" Zero solver TIME: {zero_time:>4} ({zero_time/len(group)*100:>5.1f}%)") - print(f" Non-zero solver TIME: {len(group)-zero_time:>4} ({(len(group)-zero_time)/len(group)*100:>5.1f}%)") - - # Show some examples - print(f"\nFirst 5 examples:") - for i, t in enumerate(group[:5], 1): - print(f" {i}. {t['name']}: {t['expected']} -> {t['actual']}") - print(f" Executor: {t['executor']:.2f}s, Solver: {t['solver']:.2f}s, Explorer: {t['explorer']:.2f}s") - -compute_stats(correct, "CORRECT (All expected == actual)") -compute_stats(true_correct, "TRUE POSITIVE (violation -> violation)") -compute_stats(true_negative, "TRUE NEGATIVE (safe -> safe)") -compute_stats(false_results, "FALSE RESULTS (FP + FN, excluding unknown/crash)") -compute_stats(incorrect, "INCORRECT (All expected != actual)") diff --git a/targets/sv-comp/scripts/ci_run.sh b/targets/sv-comp/scripts/ci_run.sh index 3cc3fd2..8b07f37 100755 --- a/targets/sv-comp/scripts/ci_run.sh +++ b/targets/sv-comp/scripts/ci_run.sh @@ -1,7 +1,8 @@ #!/bin/bash -# Name of the virtual environment directory -VENV_DIR="venv" +# Name of the virtual environment directory (the svcomp CLI spawns the explorer +# via .venv/bin/python3, so this must be .venv). +VENV_DIR=".venv" echo "::group::Prepare dependencies..." # Check if the virtual environment directory exists if [ ! -d "$VENV_DIR" ]; then @@ -23,7 +24,7 @@ rm -rf ../sv-benchmarks/.github echo "::endgroup::" echo "Running Tests..." -python3 target_execution.py +python3 svcomp.py test run --mode parallel --categories valid-assert.prp # Deactivate the virtual environment (optional) deactivate diff --git a/targets/sv-comp/scripts/command_generation.py b/targets/sv-comp/scripts/command_generation.py deleted file mode 100644 index 37c2b5e..0000000 --- a/targets/sv-comp/scripts/command_generation.py +++ /dev/null @@ -1,115 +0,0 @@ -from target_selection import extract_testcases -import logging -import socket -from pathlib import Path -from pprint import pformat -from dtypes import Command, VerificationTask - -logging.basicConfig(level=logging.INFO) -logger = logging.getLogger(__name__) - -SCRIPT_DIR = Path(__file__).resolve().parent -BASE_PATH = SCRIPT_DIR.parents[2] -PYENV_PATH = SCRIPT_DIR / '.venv' / 'bin' / 'python3' - - -def is_port_available(port: int) -> bool: - """ - Check if a port is available for binding. - - Args: - port: The port number to check - - Returns: - True if the port is available, False if occupied - """ - sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) - try: - sock.bind(('127.0.0.1', port)) - sock.close() - return True - except OSError: - return False - - -def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg') -> list[str]: - - - test_case_dir = ver_task['file_path'].parent - agent_path = BASE_PATH / 'symbolic-executor' / 'lib' / 'symbolic-executor.jar' - config_path = SCRIPT_DIR / '..' / config_file - library_path = BASE_PATH / 'libs' / 'java-library-path' - - base_command: list[str] = [str(PYENV_PATH), "-u", str(BASE_PATH / 'symbolic-explorer' / 'SymbolicExplorer.py'), - "-prp", ver_task['category'].value, - "--agent", str(agent_path), - "--config", str(config_path), - "-z3", str(library_path), - "--logdir", str(logging_dir), - "--mode", "sv-comp", - '--port', str(port), - "--classpath"] - - cp: list[str] = [] - for input_file in ver_task['input_files']: - cp.append(str((test_case_dir / input_file).resolve())) - cp.append(str(BASE_PATH / 'libs' / 'java-library-path' / 'com.microsoft.z3.jar')) - return base_command + cp - - - - -def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg') -> list[VerificationTask]: - - port = 9000 - skipped_ports = [] - - for ver_task in ver_tasks: - # Find next available port - while not is_port_available(port): - skipped_ports.append(port) - port += 1 - - # Safety check: don't go beyond reasonable port range - if port > 65535: - raise RuntimeError("Ran out of available ports! Too many ports occupied.") - - # Extract unique identifier for the target (based on its relative path and the name of the .yml file) - target_dir = ver_task['file_path'].parent - - # Get relative path from sv-benchmarks/java/ - sv_benchmarks_java = Path('sv-benchmarks') / 'java' - rel_target_path = target_dir.relative_to(target_dir.parents[len(target_dir.parts) - list(target_dir.parts).index('sv-benchmarks') - 1] / sv_benchmarks_java) - - target_name = ver_task['file_path'].stem - target = rel_target_path / target_name - - # Include category in log dir to avoid collisions when same file has multiple properties - category_suffix = ver_task['category'].value.replace('.prp', '') - logging_dir = SCRIPT_DIR / '..' / 'logs' / rel_target_path / f"{target_name}_{category_suffix}" - command: Command = { - 'target_dir': target_dir, - 'target': target, - 'log_dir': logging_dir, - 'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file) - } - ver_task['command'] = command - port += 1 - - if skipped_ports: - logger.warning(f"Skipped {len(skipped_ports)} occupied ports during command generation: {skipped_ports[:10]}{'...' if len(skipped_ports) > 10 else ''}") - - return ver_tasks - - -if __name__ == "__main__": - logger.info("Generating commands...") - task_dir = SCRIPT_DIR.parent / 'sv-benchmarks' - logger.info(f"Base directory: {task_dir}") - ver_tasks: list[VerificationTask] = extract_testcases(task_dir) - logger.info(f"Extracted {len(ver_tasks)} test cases.") - commands = generate_commands(ver_tasks) - logger.info(f"Generated {len(commands)} commands.") - logger.info("\nFirst 3 commands:") - for i, command in enumerate(commands[:3], 1): - logger.info(f"\nCommand {i}:\n{pformat(dict(command), width=100)}") \ No newline at end of file diff --git a/targets/sv-comp/scripts/commands/analyze.py b/targets/sv-comp/scripts/commands/analyze.py index d214a38..ce71578 100644 --- a/targets/sv-comp/scripts/commands/analyze.py +++ b/targets/sv-comp/scripts/commands/analyze.py @@ -3,7 +3,6 @@ import click import logging from pathlib import Path -import sys logger = logging.getLogger(__name__) @@ -15,57 +14,29 @@ def analyze(): @analyze.command(name='results') -@click.argument('results_file', type=click.Path(exists=True), required=False) -@click.option('--logs-dir', type=click.Path(exists=True), help='Path to logs directory') +@click.argument('run_dir', type=click.Path(exists=True), required=False) @click.pass_context -def analyze_results(ctx, results_file, logs_dir): - """Analyze results to identify context losses and failures. +def analyze_results(ctx, run_dir): + """Analyze a run from its consolidated stats.json files. - If RESULTS_FILE is not provided, will use the most recent results file. + Prints a scoring summary plus the missing-invocation superset and its + context-loss subset. If RUN_DIR is not provided, uses the most recent + runs/run_* directory. """ - from lib.analysis.context_loss import main as run_analysis + from lib.analysis.context_loss import analyze_run, find_latest_run script_dir = ctx.obj['script_dir'] - # Determine results file - if results_file: - results_path = Path(results_file) + if run_dir: + run_path = Path(run_dir) else: - # Look for latest results file - results_dir = script_dir.parent / 'results' - if results_dir.exists(): - json_files = list(results_dir.glob('results_*.json')) - if json_files: - results_path = max(json_files, key=lambda p: p.stat().st_mtime) - click.echo(f"Using latest results file: {results_path}") - else: - click.echo("Error: No results files found in results/", err=True) - ctx.exit(1) - else: - click.echo("Error: results/ directory not found and no file specified", err=True) + run_path = find_latest_run(script_dir.parent / 'runs') + if run_path is None: + click.echo("Error: No runs found under runs/. Run 'svcomp test run' first.", err=True) ctx.exit(1) + click.echo(f"Using latest run: {run_path}") - # Determine logs directory - if logs_dir: - logs_path = Path(logs_dir) - else: - logs_path = script_dir.parent / 'logs' - - if not logs_path.exists(): - click.secho(f"Warning: Logs directory not found at {logs_path}", fg='yellow') - - click.echo(f"Analyzing results from: {results_path}") - click.echo(f"Looking for logs in: {logs_path}\n") - - # Run the analysis by temporarily modifying sys.argv - old_argv = sys.argv - try: - sys.argv = ['analyse_ctx_loss.py', str(results_path)] - run_analysis() - except SystemExit: - pass # analysis script calls sys.exit - finally: - sys.argv = old_argv + analyze_run(run_path) @analyze.command(name='compare') diff --git a/targets/sv-comp/scripts/commands/test.py b/targets/sv-comp/scripts/commands/test.py index a40e526..1aa207e 100644 --- a/targets/sv-comp/scripts/commands/test.py +++ b/targets/sv-comp/scripts/commands/test.py @@ -72,6 +72,7 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target check_port_availability, VerificationCategory, ) + from lib.command_gen import new_run_timestamp, run_dir as make_run_dir script_dir = ctx.obj['script_dir'] # Determine benchmark directory @@ -113,7 +114,9 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target else: config = config_file - ver_tasks_with_commands = generate_commands(ver_tasks, config) + # One timestamp ties this run's per-testcase logs to its results dir. + run_timestamp = new_run_timestamp() + ver_tasks_with_commands = generate_commands(ver_tasks, config, run_timestamp=run_timestamp) click.echo(f"Generated {len(ver_tasks_with_commands)} commands") # Check port availability @@ -143,7 +146,9 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target # Run default single target run_single_target(ver_tasks_with_commands, create_witness=not no_witness) else: - run_parallel(ver_tasks_with_commands, max_workers=workers, create_witness=not no_witness) + run = make_run_dir(run_timestamp) + click.echo(f"Run directory: {run}") + run_parallel(ver_tasks_with_commands, max_workers=workers, create_witness=not no_witness, run_dir=run) click.secho("✓ Test execution complete", fg='green') diff --git a/targets/sv-comp/scripts/commands/util.py b/targets/sv-comp/scripts/commands/util.py index f4ffbf6..c8da339 100644 --- a/targets/sv-comp/scripts/commands/util.py +++ b/targets/sv-comp/scripts/commands/util.py @@ -109,18 +109,16 @@ def show_config(ctx): click.echo(f"\nBenchmark directory: {benchmark_dir}") click.echo(f" Exists: {benchmark_dir.exists()}") - # Show results directory - results_dir = script_dir.parent / 'results' - click.echo(f"\nResults directory: {results_dir}") - click.echo(f" Exists: {results_dir.exists()}") - if results_dir.exists(): - result_files = list(results_dir.glob('results_*.json')) - click.echo(f" Result files: {len(result_files)}") - - # Show logs directory - logs_dir = script_dir.parent / 'logs' - click.echo(f"\nLogs directory: {logs_dir}") - click.echo(f" Exists: {logs_dir.exists()}") + # Show runs directory (each run has its own runs/run_/{logs,results}) + runs_dir = script_dir.parent / 'runs' + click.echo(f"\nRuns directory: {runs_dir}") + click.echo(f" Exists: {runs_dir.exists()}") + if runs_dir.exists(): + run_dirs = sorted((p for p in runs_dir.glob('run_*') if p.is_dir()), + key=lambda p: p.stat().st_mtime) + click.echo(f" Runs: {len(run_dirs)}") + if run_dirs: + click.echo(f" Latest run: {run_dirs[-1].name}") @util.command(name='check-deps') diff --git a/targets/sv-comp/scripts/compare_results.py b/targets/sv-comp/scripts/compare_results.py deleted file mode 100644 index d25a49d..0000000 --- a/targets/sv-comp/scripts/compare_results.py +++ /dev/null @@ -1,56 +0,0 @@ -import json -import os - -def compare_results(current_file, reference_file): - # Load current and reference data - with open(current_file, 'r') as f: - current_data = json.load(f) - - with open(reference_file, 'r') as f: - reference_data = json.load(f) - - # Extract results from both files - current_results = current_data.get("results", {}) - reference_results = reference_data.get("results", {}) - - # Compare cases - changes = [] - for case, current_value in current_results.items(): - current_status = current_value[0] # Extract the status from the current results - - # Check if the case exists in reference - if case in reference_results: - reference_status = reference_results[case][0] # Extract the status from the reference results - if current_status != reference_status: - changes.append({ - "case": case, - "from": reference_status, - "to": current_status - }) - else: - # New case added in current results - changes.append({ - "case": case, - "from": "Not present", - "to": current_status - }) - - # Identify cases removed in the current results - for case in reference_results: - if case not in current_results: - changes.append({ - "case": case, - "from": reference_results[case][0], - "to": "Removed" - }) - - # Print the changes - for change in changes: - print(f"Case: {change['case']} changed from {change['from']} to {change['to']}") - -# Replace these with paths to your JSON files -SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) -current_file = os.path.join(SCRIPT_DIR, '..', 'results', "results_20241122_103412.json") -reference_file = os.path.join(SCRIPT_DIR, '..', 'results', "results_20241122_100419.json") - -compare_results(current_file, reference_file) diff --git a/targets/sv-comp/scripts/dtypes.py b/targets/sv-comp/scripts/dtypes.py deleted file mode 100644 index 9d2f1c6..0000000 --- a/targets/sv-comp/scripts/dtypes.py +++ /dev/null @@ -1,38 +0,0 @@ -from pathlib import Path -from typing import Optional, TypedDict -import enum - -class ExpectedVerdict(enum.Enum): - VIOLATION = False - SAFE = True - -class Verdict(enum.Enum): - VIOLATION = "== ERROR" - SAFE = "== OK" - UNKNOWN = "== DONT-KNOW" - NO_SYMBOLIC_VARS = "== NON-SYMBOLIC" - -class VerificationCategory(enum.Enum): - VALID_ASSERT_PRP = "valid-assert.prp" - NO_RUNTIME_EXCEPTION_PRP = "no-runtime-exception.prp" - NO_DEADLOCK_PRP = "no-deadlock.prp" - -class Command(TypedDict): - target_dir: Path - target: Path - log_dir: Path - command: list[str] - -class VerificationResult(TypedDict): - points: int - case: str - -class VerificationTask(TypedDict): - category: VerificationCategory - verdict: ExpectedVerdict - file_path: Path - input_files: list[Path] - command: Optional[Command] - result: Optional[VerificationResult] - - \ No newline at end of file diff --git a/targets/sv-comp/scripts/lib/analysis/context_loss.py b/targets/sv-comp/scripts/lib/analysis/context_loss.py index f8019d6..26ce238 100644 --- a/targets/sv-comp/scripts/lib/analysis/context_loss.py +++ b/targets/sv-comp/scripts/lib/analysis/context_loss.py @@ -1,398 +1,226 @@ #!/usr/bin/env python3 """ -Analyze SV-Comp results to identify context loss methods that need implementation. -Run this script in the directory containing the results JSON file. +Analyze a SV-COMP run from its consolidated per-testcase ``stats.json`` files. -Usage: python3 analyse_ctx_loss.py results_valid-assert.prp_XXXXXX.json +A run lives under ``runs/run_/`` with: + - ``results/results__.json`` : per-target verdict / points / timing + - ``logs//_/stats.json`` : per-testcase missing invocations, + context-loss subset, execution errors + +This reads that structured data directly — no log scraping — and prints a scoring +summary (Correct / Failed / Unk / Error / Timeout) plus the missing-invocation +superset and its authoritative context-loss subset (issue #25). """ import json import sys -import re from collections import defaultdict from pathlib import Path +from typing import Optional +# lib/analysis/context_loss.py -> scripts/ +SCRIPT_DIR = Path(__file__).resolve().parents[2] -def extract_context_loss_methods(log_content: str) -> list[str]: - """Extract all method names causing context loss from log content.""" - methods = set() # Use set to dedupe - if not log_content: - return list(methods) - - # Look for "Context loss:" pattern - for match in re.finditer(r'Context loss:\s*(.+?)(?:\n|$)', log_content): - methods.add(match.group(1).strip()) - - # Also look for "Uninstrumented invocation" pattern - for match in re.finditer(r'Uninstrumented invocation.*?:\s*(.+?)(?:\n|$)', log_content): - methods.add(match.group(1).strip()) - - # Look for "Context loss recorded" with method info on previous lines - for match in re.finditer(r'(\S+\.\S+)\s*\n.*Context loss recorded', log_content): - methods.add(match.group(1).strip()) - - return list(methods) - +SCORE_BUCKETS = ['Correct', 'Failed', 'Unk', 'Error', 'Timeout'] -def extract_missing_invocations(log_content: str) -> list[str]: - """Extract missing/unimplemented method invocations from log content.""" - methods = set() # Use set to dedupe - if not log_content: - return list(methods) - # Pattern: "Error visiting Instruction INVOKE* owner/class/method:desc" - # Example: "Error visiting Instruction INVOKEVIRTUAL java/lang/Double/byteValue:()B" - for match in re.finditer( - r'Error visiting Instruction (INVOKE\w+)\s+(\S+?)(?:\s*\(|$)', - log_content - ): - invoke_type = match.group(1) - method_sig = match.group(2) - # Clean up the method signature (remove id info if present) - method_sig = re.sub(r'\s*\(id:.*', '', method_sig) - methods.add(f"{invoke_type} {method_sig}") +def find_latest_run(runs_root: Path) -> Optional[Path]: + """Return the most recently modified runs/run_* directory, or None.""" + if not runs_root.exists(): + return None + run_dirs = [p for p in runs_root.glob('run_*') if p.is_dir()] + if not run_dirs: + return None + return max(run_dirs, key=lambda p: p.stat().st_mtime) - # Pattern: "Not implemented: in " - for match in re.finditer(r'Not implemented:\s*(.+?)\s+in\s+(\S+)', log_content): - method = match.group(1).strip() - cls = match.group(2).strip() - methods.add(f"NOT_IMPLEMENTED {cls}/{method}") - return list(methods) +def classify(case: str, points, exec_status, error) -> str: + """Bucket a single result into Correct / Failed / Unk / Error / Timeout. - -def extract_symbolic_invocations_from_stats(stats_path: Path) -> list[str]: + Precedence: a timeout or a crash/error is reported as such regardless of points; + otherwise positive points are Correct, negative points are Failed (wrong verdict), + and zero points are Unknown (unknown / non-symbolic). """ - Extract symbolic method invocations from stats JSON files. - - Stats files contain entries like: - {"owner":"java/lang/Character","isSymbolic":true,"name":"isUnicodeIdentifierStart","desc":"(I)Z"} - - Returns list of method signatures that have isSymbolic=true (missing implementations). - """ - methods = set() - - # Check both stats_1.json and stats_-1.json - for stats_file in ['stats_1.json', 'stats_-1.json']: - file_path = stats_path / stats_file - if not file_path.exists(): - continue - - try: - with open(file_path) as f: - data = json.load(f) - - if isinstance(data, list): - for entry in data: - if isinstance(entry, dict) and entry.get('isSymbolic', False): - owner = entry.get('owner', '') - name = entry.get('name', '') - desc = entry.get('desc', '') - is_instance = entry.get('isInstance', False) - invoke_type = 'INVOKEVIRTUAL' if is_instance else 'INVOKESTATIC' - if owner and name: - methods.add(f"{invoke_type} {owner}/{name}:{desc}") - except (json.JSONDecodeError, IOError): - pass - - return list(methods) - - -def extract_errors(log_content: str) -> list[str]: - """Extract error messages from log content.""" - errors = [] - if not log_content: - return errors - - # Look for SWAT Exception patterns - for match in re.finditer(r'\[SWAT Exception\]:\s*(.+?)(?:\n|$)', log_content): - errors.append(match.group(1).strip()) - - # Look for general exceptions - for match in re.finditer(r'Exception.*?:\s*(.+?)(?:\n|$)', log_content): - msg = match.group(1).strip() - if msg and len(msg) < 200: - errors.append(msg) + s = str(exec_status).lower() + if 'timeout' in s: + return 'Timeout' + if 'error' in s or error or 'crash' in str(case).lower(): + return 'Error' + if points and points > 0: + return 'Correct' + if points and points < 0: + return 'Failed' + return 'Unk' + + +def load_json(path: Path): + """Load a JSON file, returning None if it is missing or unreadable.""" + try: + with open(path) as f: + return json.load(f) + except (OSError, json.JSONDecodeError): + return None - return errors +def stats_path_for(logs_dir: Path, target: str, category: str) -> Path: + """Path to a testcase's stats.json, derived from its target and property.""" + cat_short = category.replace('.prp', '') + return logs_dir / f"{target}_{cat_short}" / 'stats.json' -def get_log_dir(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the log directory for a given task. - Task name format: folder/testname (e.g., "objects/objects03") - Log dir format: logs//_/ - """ - parts = task_name.split('/') - if len(parts) >= 2: - folder = parts[0] - testname = parts[1] - else: - folder = "" - testname = parts[0] +def signature(inv: dict) -> str: + """Render a missing invocation as a stable owner/name:desc signature.""" + return f"{inv['owner']}/{inv['name']}:{inv['desc']}" - # Property name like "valid-assert.prp" -> "valid-assert" - prop_short = property_name.replace('.prp', '') - return logs_dir / folder / f"{testname}_{prop_short}" +def analyze_run(run_dir: Path): + """Aggregate and print the analysis for a single run directory.""" + run_dir = Path(run_dir) + results_dir = run_dir / 'results' + logs_dir = run_dir / 'logs' + results_files = sorted(results_dir.glob('results_*.json')) + if not results_files: + print(f"No results files found in {results_dir}") + return -def get_log_path(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the explorer.log for a given task. - """ - return get_log_dir(logs_dir, task_name, property_name) / "explorer.log" + print(f"Analyzing run: {run_dir.name}") + print(f" results: {results_dir}") + print(f" logs: {logs_dir}\n") + # Scoring buckets per category, and total points per category. + score: dict = {} + points_by_cat: dict = {} -def get_stats_dir(logs_dir: Path, task_name: str, property_name: str) -> Path: - """ - Construct the path to the stats directory (logs/ subdirectory) for a given task. - """ - return get_log_dir(logs_dir, task_name, property_name) / "logs" + # Missing-invocation aggregation across all testcases of the run. + # signature -> {tasks: set, count: int, context_loss: bool, isSymbolic: bool} + missing: dict = {} + exec_errors: dict = defaultdict(list) # message -> [tasks] + total_tasks = 0 + stats_missing = 0 # testcases with no stats.json on disk -def read_log_file(log_path: Path) -> str: - """Read log file content, return empty string if not found.""" - try: - if log_path.exists(): - return log_path.read_text(errors='replace') - except Exception: - pass - return "" + for rf in results_files: + data = load_json(rf) + if not data: + continue + category = data.get('category', rf.stem) + cat_buckets: dict = defaultdict(int) + + for target, tup in data.get('results', {}).items(): + total_tasks += 1 + case = tup[0] if len(tup) > 0 else '' + points = tup[1] if len(tup) > 1 else 0 + exec_status = tup[2] if len(tup) > 2 else '' + error = tup[3] if len(tup) > 3 else False + cat_buckets[classify(case, points, exec_status, error)] += 1 + + stats = load_json(stats_path_for(logs_dir, target, category)) + if stats is None: + stats_missing += 1 + continue + for inv in stats.get('missing_invocations', []): + sig = signature(inv) + m = missing.setdefault( + sig, {'tasks': set(), 'count': 0, 'context_loss': False, 'isSymbolic': False}) + m['tasks'].add(target) + m['count'] += inv.get('count', 1) + m['context_loss'] = m['context_loss'] or inv.get('context_loss', False) + m['isSymbolic'] = m['isSymbolic'] or inv.get('isSymbolic', False) + for e in stats.get('execution_errors', []): + exec_errors[e.get('message', '')].append(target) + + score[category] = dict(cat_buckets) + points_by_cat[category] = data.get('points') + + _print_scoring_summary(score, points_by_cat, total_tasks) + _print_missing_invocations(missing) + _print_execution_errors(exec_errors) + + if stats_missing: + print(f"\nNote: {stats_missing} testcase(s) had no stats.json " + f"(crash before the explorer wrote one, or an older run).") + + +def _print_scoring_summary(score: dict, points_by_cat: dict, total_tasks: int): + print("=" * 78) + print("SCORING SUMMARY") + print("=" * 78) + header = f"{'Category':<26}" + "".join(f"{b:>9}" for b in SCORE_BUCKETS) + f"{'Total':>8}{'Points':>9}" + print(header) + print("-" * len(header)) + + totals = {b: 0 for b in SCORE_BUCKETS} + total_points = 0 + for category in sorted(score): + buckets = score[category] + row_total = sum(buckets.get(b, 0) for b in SCORE_BUCKETS) + pts = points_by_cat.get(category) or 0 + total_points += pts + for b in SCORE_BUCKETS: + totals[b] += buckets.get(b, 0) + if row_total == 0: + continue # don't clutter the table with categories that had no testcases + cells = "".join(f"{buckets.get(b, 0):>9}" for b in SCORE_BUCKETS) + print(f"{category:<26}{cells}{row_total:>8}{pts:>9}") + + print("-" * len(header)) + grand_total = sum(totals.values()) + cells = "".join(f"{totals[b]:>9}" for b in SCORE_BUCKETS) + print(f"{'TOTAL':<26}{cells}{grand_total:>8}{total_points:>9}") + print() + + +def _print_missing_invocations(missing: dict): + print("=" * 78) + cl = {sig: m for sig, m in missing.items() if m['context_loss']} + print(f"MISSING INVOCATIONS (superset: {len(missing)} signatures; " + f"context-loss subset: {len(cl)})") + print("=" * 78) + if not missing: + print("None.") + print() + return + + # Most-impactful first: by number of testcases, then total count. + for sig, m in sorted(missing.items(), key=lambda kv: (-len(kv[1]['tasks']), -kv[1]['count'])): + marker = "CL " if m['context_loss'] else " " + print(f" {marker}{len(m['tasks']):>4} tasks (count={m['count']:<5}) {sig}") + print() + + if cl: + print("-" * 78) + print(f"CONTEXT-LOSS METHODS (subset that caused symbolic context loss):") + for sig in sorted(cl): + print(f" {sig}") + print() + + +def _print_execution_errors(exec_errors: dict): + if not exec_errors: + return + print("=" * 78) + print(f"EXECUTION ERRORS ({len(exec_errors)} distinct)") + print("=" * 78) + for msg, tasks in sorted(exec_errors.items(), key=lambda kv: -len(kv[1])): + unique = list(dict.fromkeys(tasks)) + print(f" {len(unique):>4} tasks {msg[:90]}") + print(f" e.g. {', '.join(unique[:3])}") + print() def main(): - if len(sys.argv) < 2: - # Find the latest results file - results_dir = Path('.') - json_files = list(results_dir.glob('results_*.json')) - if not json_files: - json_files = list(Path('results').glob('results_*.json')) - if not json_files: - print("Usage: python3 analyse_ctx_loss.py ") - print("No results files found in current directory") - sys.exit(1) - results_file = max(json_files, key=lambda p: p.stat().st_mtime) - print(f"Using latest results file: {results_file}") - else: - results_file = Path(sys.argv[1]) - - # Determine logs directory (sibling to results file or parent's logs/) - if results_file.parent.name == 'results': - logs_dir = results_file.parent.parent / 'logs' + """Standalone entry point: analyze a run dir argument or the latest run.""" + if len(sys.argv) >= 2: + run_dir = Path(sys.argv[1]) else: - logs_dir = results_file.parent / 'logs' - - print(f"Looking for logs in: {logs_dir}") - - with open(results_file) as f: - data = json.load(f) - - results = data['results'] - category = data.get('category', 'valid-assert.prp') - - # Analyze all 0-point tasks - zero_points_by_folder = defaultdict(list) - context_loss_methods = defaultdict(list) - missing_invocations = defaultdict(list) - all_errors = defaultdict(list) - - for name, task in results.items(): - # task format: [status_change, points, execution_status, error_bool, validated, time] - points = task[1] - if points == 0: - folder = name.split('/')[0] - status = task[0] - exec_status = task[2] - - # Read the actual log file from disk - log_path = get_log_path(logs_dir, name, category) - log_content = read_log_file(log_path) - - # Get stats directory for symbolic invocations - stats_dir = get_stats_dir(logs_dir, name, category) - - zero_points_by_folder[folder].append({ - 'name': name, - 'status': status, - 'exec_status': exec_status, - 'log_path': str(log_path), - 'log_content': log_content, - 'log_exists': log_path.exists(), - 'stats_dir': str(stats_dir) - }) - - # Extract context loss methods - methods = extract_context_loss_methods(log_content) - for method in methods: - context_loss_methods[method].append(name) - - # Extract missing invocations from error logs - invocations = extract_missing_invocations(log_content) - for inv in invocations: - missing_invocations[inv].append(name) - - # Extract symbolic invocations from stats JSON files - symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir) - for inv in symbolic_invocations: - missing_invocations[inv].append(name) - - # Extract errors - errors = extract_errors(log_content) - for error in errors: - all_errors[error].append(name) - - # Print summary by folder - print("\n" + "=" * 80) - print("TASKS WITH 0 POINTS BY FOLDER") - print("=" * 80) - total_zero = 0 - logs_found = 0 - for folder, tasks in sorted(zero_points_by_folder.items(), key=lambda x: -len(x[1])): - folder_logs_found = sum(1 for t in tasks if t['log_exists']) - print(f"{folder}: {len(tasks)} tasks ({folder_logs_found} logs found)") - total_zero += len(tasks) - logs_found += folder_logs_found - print(f"\nTotal: {total_zero} tasks with 0 points ({logs_found} logs found)") - - # Print context loss methods sorted by frequency - print("\n" + "=" * 80) - print("CONTEXT LOSS METHODS (sorted by frequency)") - print("=" * 80) - - if not context_loss_methods: - print("No context loss methods found in logs.") - else: - for method, tasks in sorted(context_loss_methods.items(), key=lambda x: -len(x[1])): - print(f"\n{len(tasks):3d} tasks - {method}") - print(f" Examples: {', '.join(tasks[:3])}") - - # Print missing invocations sorted by frequency - print("\n" + "=" * 80) - print("MISSING/UNIMPLEMENTED INVOCATIONS (sorted by frequency)") - print("=" * 80) - - if not missing_invocations: - print("No missing invocations found in logs.") - else: - for inv, tasks in sorted(missing_invocations.items(), key=lambda x: -len(x[1])): - # Dedupe task list (same task may appear multiple times) - unique_tasks = list(dict.fromkeys(tasks)) - print(f"\n{len(unique_tasks):3d} tasks - {inv}") - print(f" Examples: {', '.join(unique_tasks[:3])}") - - # Print errors sorted by frequency - print("\n" + "=" * 80) - print("ERRORS (sorted by frequency)") - print("=" * 80) - - if not all_errors: - print("No specific errors found in logs.") - else: - for error, tasks in sorted(all_errors.items(), key=lambda x: -len(x[1]))[:20]: - print(f"\n{len(tasks):3d} tasks - {error[:100]}") - print(f" Examples: {', '.join(tasks[:3])}") - - # Detailed breakdown for each folder - print("\n" + "=" * 80) - print("DETAILED BREAKDOWN BY FOLDER") - print("=" * 80) - - for folder in ['autostub', 'jbmc-regression', 'java-ranger-regression', 'algorithms', 'argv-tasks', 'float-nonlinear-calculation', 'securibench', 'objects']: - if folder not in zero_points_by_folder: - continue - - print(f"\n--- {folder} ({len(zero_points_by_folder[folder])} tasks) ---") - - folder_context_loss = defaultdict(list) - folder_missing_invocations = defaultdict(list) - folder_errors = defaultdict(list) - other_issues = defaultdict(list) - tasks_with_missing_invocations = set() - - for task in zero_points_by_folder[folder]: - log_content = task['log_content'] - stats_dir = Path(task['stats_dir']) - methods = extract_context_loss_methods(log_content) - invocations = extract_missing_invocations(log_content) - symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir) - errors = extract_errors(log_content) - - if methods: - for method in methods: - folder_context_loss[method].append(task['name']) - - all_invocations = invocations + symbolic_invocations - if all_invocations: - tasks_with_missing_invocations.add(task['name']) - for inv in all_invocations: - folder_missing_invocations[inv].append(task['name']) - - # Always categorize by verdict/status (not just when no missing invocations) - if errors: - for error in errors: - folder_errors[error[:80]].append(task['name']) - - if 'timeout' in task['exec_status'].lower(): - other_issues['timeout'].append(task['name']) - elif not task['log_exists']: - other_issues['log file not found'].append(task['name']) - elif not log_content.strip(): - other_issues['log file empty'].append(task['name']) - elif 'DONT-KNOW' in log_content: - other_issues['verdict: DONT-KNOW'].append(task['name']) - elif 'NoThreadContextException' in log_content: - other_issues['NoThreadContextException'].append(task['name']) - elif not methods and not all_invocations: - other_issues['unknown (check log)'].append(task['name']) - - if folder_context_loss: - print(" Context loss methods:") - for method, tasks in sorted(folder_context_loss.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {method[:80]}") - - if folder_missing_invocations: - print(f" Missing invocations ({len(tasks_with_missing_invocations)} unique tasks):") - for inv, tasks in sorted(folder_missing_invocations.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {inv[:80]}") - - if folder_errors: - print(" Errors:") - for error, tasks in sorted(folder_errors.items(), key=lambda x: -len(x[1]))[:10]: - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {error[:80]}") - - if other_issues: - print(" Other issues:") - for issue, tasks in sorted(other_issues.items(), key=lambda x: -len(x[1])): - unique_tasks = list(dict.fromkeys(tasks)) - print(f" {len(unique_tasks):3d} - {issue[:80]}") - - # Print sample logs for debugging - print("\n" + "=" * 80) - print("SAMPLE LOGS (first 5 tasks with 0 points)") - print("=" * 80) - - count = 0 - for name, task in results.items(): - if task[1] == 0 and count < 5: - log_path = get_log_path(logs_dir, name, category) - log_content = read_log_file(log_path) - - print(f"\n{name}:") - print(f" Status: {task[0]}") - print(f" Exec status: {task[2]}") - print(f" Log path: {log_path}") - print(f" Log exists: {log_path.exists()}") - if log_content: - # Show last 500 chars which usually has the verdict - print(f" Log tail: ...{log_content[-500:]}") - else: - print(f" Log: (empty or not found)") - count += 1 + run_dir = find_latest_run(SCRIPT_DIR / '..' / 'runs') + if run_dir is None: + print("Usage: python3 -m lib.analysis.context_loss ") + print("No runs found under runs/") + sys.exit(1) + print(f"Using latest run: {run_dir}") + analyze_run(run_dir) if __name__ == '__main__': diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py index ccfa7f6..9bf39f7 100644 --- a/targets/sv-comp/scripts/lib/command_gen.py +++ b/targets/sv-comp/scripts/lib/command_gen.py @@ -1,8 +1,10 @@ from .selection import extract_testcases +import datetime import logging import socket from pathlib import Path from pprint import pformat +from typing import Optional from .dtypes import Command, VerificationTask logging.basicConfig(level=logging.INFO) @@ -59,13 +61,27 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80 -def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg') -> list[VerificationTask]: +def new_run_timestamp() -> str: + """Returns a timestamp identifying a single run, shared across all its outputs.""" + return datetime.datetime.now().strftime("%Y%m%d_%H%M%S") + + +def run_dir(run_timestamp: str) -> Path: + """The directory holding a non-debug run's logs/ and results/.""" + return SCRIPT_DIR / '..' / 'runs' / f"run_{run_timestamp}" + + +def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg', run_timestamp: Optional[str] = None) -> list[VerificationTask]: port = 9000 skipped_ports = [] - # Determine log directory base based on config file - log_dir_base = 'logs-debug' if 'debug' in config_file.lower() else 'logs' + # A single timestamp ties a run's per-testcase logs to its results. + if run_timestamp is None: + run_timestamp = new_run_timestamp() + + # Debug runs keep a timestamped history per target; normal runs share one run dir. + is_debug = 'debug' in config_file.lower() for ver_task in ver_tasks: # Find next available port @@ -89,7 +105,14 @@ def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swa # Include category in log dir to avoid collisions when same file has multiple properties category_suffix = ver_task['category'].value.replace('.prp', '') - logging_dir = SCRIPT_DIR / '..' / log_dir_base / rel_target_path / f"{target_name}_{category_suffix}" + testcase = f"{target_name}_{category_suffix}" + if is_debug: + # runs-debug///run_/logs — grouped per target so a debug + # session keeps the history of its runs together. + logging_dir = SCRIPT_DIR / '..' / 'runs-debug' / rel_target_path / testcase / f"run_{run_timestamp}" / 'logs' + else: + # runs/run_/logs// — all testcases of a run share one run dir. + logging_dir = run_dir(run_timestamp) / 'logs' / rel_target_path / testcase command: Command = { 'target_dir': target_dir, 'target': target, diff --git a/targets/sv-comp/scripts/lib/execution.py b/targets/sv-comp/scripts/lib/execution.py index fbf1f1d..db5c354 100644 --- a/targets/sv-comp/scripts/lib/execution.py +++ b/targets/sv-comp/scripts/lib/execution.py @@ -8,7 +8,7 @@ from pprint import pformat from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command from .utils import ci_print -from .command_gen import extract_testcases, generate_commands +from .command_gen import extract_testcases, generate_commands, new_run_timestamp, run_dir as make_run_dir from .witness import generate_and_validate_witness from collections import Counter from pathlib import Path @@ -283,7 +283,15 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 900) -> tuple[Execut -def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_witness: bool = True): +def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_witness: bool = True, run_dir: Optional[Path] = None, run_timestamp: Optional[str] = None): + # Resolve the run context so all outputs (per-testcase logs + aggregated results) share one dir. + if run_timestamp is None: + run_timestamp = run_dir.name.replace('run_', '') if run_dir is not None else new_run_timestamp() + if run_dir is None: + run_dir = make_run_dir(run_timestamp) + run_dir = Path(run_dir) + results_dir = run_dir / 'results' + max_workers = min(max_workers, len(ver_tasks)) logger.info(f"Running parallel target execution with {max_workers} workers...") @@ -315,13 +323,13 @@ def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_ total_elapsed_time = time.perf_counter() - total_start_time logger.info(f"Total parallel execution time: {total_elapsed_time:.2f}s") - evaluate_results(results) + evaluate_results(results, results_dir, run_timestamp) # Run aggregate analysis from timing files from .analysis.timing import TimingAnalysis - TimingAnalysis.print_timing_statistics() + TimingAnalysis.print_timing_statistics(run_dir / 'logs') -def evaluate_results(results): +def evaluate_results(results, results_dir: Path, run_timestamp: str): """Evaluate results with per-category statistics including timing.""" total_points = 0 category_stats = {} @@ -473,13 +481,13 @@ def evaluate_results(results): all_elapsed = [t[2] for t in all_times] logger.info(f"Overall timing: min={min(all_elapsed):.2f}s, max={max(all_elapsed):.2f}s, mean={sum(all_elapsed)/len(all_elapsed):.2f}s") - save_results(category_stats, results) + save_results(category_stats, results, results_dir, run_timestamp) # Save aggregate stage timing to CSV - save_aggregate_stage_timing(category_stats) + save_aggregate_stage_timing(category_stats, results_dir, run_timestamp) # Generate timing histogram - generate_timing_histogram(category_stats, results) + generate_timing_histogram(category_stats, results, results_dir, run_timestamp) summary_path = os.getenv("GITHUB_STEP_SUMMARY") if summary_path is not None: @@ -488,17 +496,17 @@ def evaluate_results(results): return total_points -def generate_timing_histogram(category_stats, results, folder='results'): +def generate_timing_histogram(category_stats, results, results_dir: Path, run_timestamp: str): """Generate histogram(s) of execution times using matplotlib.""" if not MATPLOTLIB_AVAILABLE: logger.warning("matplotlib not available, skipping histogram generation. Install with: pip install matplotlib numpy") return - folder = os.path.join(SCRIPT_DIR, '..', folder) + folder = str(results_dir) if not os.path.exists(folder): os.makedirs(folder) - timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S") + timestamp = run_timestamp # Collect all times across categories all_times = [] @@ -610,14 +618,14 @@ def generate_timing_histogram(category_stats, results, folder='results'): logger.info(f"Timing boxplot saved to: {boxplot_path}") -def save_results(category_stats, results, folder='results'): +def save_results(category_stats, results, results_dir: Path, run_timestamp: str): """Save results with one JSON file per category, including timing data.""" - folder = os.path.join(SCRIPT_DIR, '..', folder) + folder = str(results_dir) if not os.path.exists(folder): os.makedirs(folder) - timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S") + timestamp = run_timestamp # Save one file per category for category_name, stats in category_stats.items(): @@ -656,14 +664,14 @@ def save_results(category_stats, results, folder='results'): logger.info(f"[{category_name}] Results saved to {filepath}") -def save_aggregate_stage_timing(category_stats, folder='results'): +def save_aggregate_stage_timing(category_stats, results_dir: Path, run_timestamp: str): """Save aggregate stage timing data to CSV file for easy analysis.""" - folder = os.path.join(SCRIPT_DIR, '..', folder) + folder = str(results_dir) if not os.path.exists(folder): os.makedirs(folder) - timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S") + timestamp = run_timestamp filename = f"stage_timing_{timestamp}.csv" filepath = os.path.join(folder, filename) @@ -834,7 +842,8 @@ def run_single_target(ver_tasks: list[VerificationTask], create_witness: bool = config_file = "sv-comp.cfg" else: raise ValueError(f"Invalid mode: {mode}") - ver_tasks_with_commands = generate_commands(ver_tasks, config_file)#[:10] + run_timestamp = new_run_timestamp() + ver_tasks_with_commands = generate_commands(ver_tasks, config_file, run_timestamp=run_timestamp)#[:10] logger.info(f"Generated {len(ver_tasks_with_commands)} commands.") # Check port availability before starting tests (sanity check) @@ -848,7 +857,7 @@ def run_single_target(ver_tasks: list[VerificationTask], create_witness: bool = if mode == Mode.SINGLE_TARGET: # type: ignore run_single_target(ver_tasks_with_commands) elif mode == Mode.PARALLEL: - run_parallel(ver_tasks_with_commands) + run_parallel(ver_tasks_with_commands, run_timestamp=run_timestamp) else: raise ValueError(f"Invalid mode: {mode}") diff --git a/targets/sv-comp/scripts/run_locally.sh b/targets/sv-comp/scripts/run_locally.sh index 209bdc2..0915c5e 100755 --- a/targets/sv-comp/scripts/run_locally.sh +++ b/targets/sv-comp/scripts/run_locally.sh @@ -24,7 +24,7 @@ echo "Clone target Repository" "$SCRIPT_DIR/checkout.sh" echo "Running Tests..." -python3 "$SCRIPT_DIR/target_execution.py" +python3 "$SCRIPT_DIR/svcomp.py" test run --mode parallel --categories valid-assert.prp # Deactivate the virtual environment (optional) deactivate diff --git a/targets/sv-comp/scripts/target_execution.py b/targets/sv-comp/scripts/target_execution.py deleted file mode 100644 index 0184aba..0000000 --- a/targets/sv-comp/scripts/target_execution.py +++ /dev/null @@ -1,703 +0,0 @@ -from contextlib import contextmanager -import logging, os, enum, subprocess -import socket -import time - -import concurrent.futures, json, datetime -from typing import List, Optional -from pprint import pformat -from dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command -from util import ci_print -from command_generation import extract_testcases, generate_commands -from witness_validation import generate_and_validate_witness -from collections import Counter -from pathlib import Path - -try: - import matplotlib.pyplot as plt - import numpy as np - MATPLOTLIB_AVAILABLE = True -except ImportError: - MATPLOTLIB_AVAILABLE = False - - -logging.basicConfig(level=logging.INFO) -logger = logging.getLogger(__name__) -SCRIPT_DIR = Path(__file__).resolve().parent - -class ExecutionStatus(enum.Enum): - SUCCESS = "success" - ERROR = "error" - TIMEOUT = "timeout" - - - -class Mode(enum.Enum): - SINGLE_TARGET = "single" - PARALLEL = "parallel" - - -def check_port_availability(ver_tasks: list[VerificationTask]) -> tuple[bool, list[int]]: - """ - Check if all ports required by verification tasks are available. - - Args: - ver_tasks: List of verification tasks with command configuration - - Returns: - Tuple of (all_available: bool, occupied_ports: list[int]) - """ - occupied_ports = [] - required_ports = set() - - # Extract all required ports from commands - for ver_task in ver_tasks: - command = ver_task.get('command') - if command: - cmd_list = command.get('command', []) - # Find --port argument - try: - port_idx = cmd_list.index('--port') - if port_idx + 1 < len(cmd_list): - port = int(cmd_list[port_idx + 1]) - required_ports.add(port) - except (ValueError, IndexError): - continue - - if not required_ports: - logger.info("No ports found in commands") - return True, [] - - logger.info(f"Checking availability of {len(required_ports)} ports (range: {min(required_ports)}-{max(required_ports)})") - - # Check each port - for port in sorted(required_ports): - sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) - try: - # Try to bind to the port - sock.bind(('127.0.0.1', port)) - sock.close() - except OSError: - # Port is already in use - occupied_ports.append(port) - - if occupied_ports: - logger.error(f"The following {len(occupied_ports)} ports are already in use: {occupied_ports}") - logger.error("Please kill the processes using these ports before running tests.") - logger.error(f"You can find processes with: lsof -i :{occupied_ports[0]} (for example)") - return False, occupied_ports - else: - logger.info(f"All {len(required_ports)} ports are available") - return True, [] - - -@contextmanager -def pushd(dirname): - """Context manager to temporarily change the working directory.""" - original_dir = os.getcwd() - logger.info(f"Changing directory to: {dirname}") - os.chdir(dirname) - try: - yield - finally: - os.chdir(original_dir) - -def reset_log_dir(log_dir) -> None: - logger.info("Resetting log directory...") - if os.path.exists(log_dir): - os.system(f"rm -rf {log_dir}") - os.makedirs(log_dir) - - -def parse_verdict_from_output(output: List[str], category: VerificationCategory) -> Optional[Verdict]: - """Parse the verdict for a specific category from the output.""" - - for line in output: - if f"[VERDICT {category.value}]" in line: - if "== OK" in line: - return Verdict.SAFE - elif "== ERROR" in line: - return Verdict.VIOLATION - elif "== DONT-KNOW" in line: - return Verdict.UNKNOWN - elif "== NON-SYMBOLIC" in line: - return Verdict.NO_SYMBOLIC_VARS - - return None # No verdict found for this category - - -def determine_result(output: List[str], category: VerificationCategory, expected_verdict: ExpectedVerdict) -> tuple[int, str]: - """Determine points and case based on the actual vs expected verdict for a single category.""" - actual_verdict = parse_verdict_from_output(output, category) - - # If no verdict found in output, treat as crash - if actual_verdict is None: - if expected_verdict == ExpectedVerdict.SAFE: - return 0, 'safe -> crash' - else: - return 0, 'violation -> crash' - - # Compare actual vs expected - if expected_verdict == ExpectedVerdict.SAFE: - if actual_verdict == Verdict.SAFE: - return 2, 'safe -> safe' - elif actual_verdict == Verdict.VIOLATION: - return -16, 'safe -> violation' - elif actual_verdict == Verdict.UNKNOWN: - return 0, 'safe -> unknown' - elif actual_verdict == Verdict.NO_SYMBOLIC_VARS: - return 0, 'safe -> non-symbolic' - else: # expected_verdict == ExpectedVerdict.VIOLATION - if actual_verdict == Verdict.SAFE: - return -32, 'violation -> safe' - elif actual_verdict == Verdict.VIOLATION: - return 1, 'violation -> violation' - elif actual_verdict == Verdict.UNKNOWN: - return 0, 'violation -> unknown' - elif actual_verdict == Verdict.NO_SYMBOLIC_VARS: - return 0, 'violation -> non-symbolic' - - # Shouldn't reach here, but handle gracefully - return 0, 'unknown' - -def target_execution(ver_task: VerificationTask) -> tuple[Path, str, int, ExecutionStatus, bool, Optional[bool], float]: - """ - Execute a verification task and return results including execution time. - - Returns: - Tuple of (target, case, points, execution_status, error, validated, elapsed_time_seconds) - """ - command = ver_task['command'] - if command is None: - raise ValueError(f"No command found for verification task: {ver_task['file_path']}") - - target = command["target"] - ci_print(f'::group:: Executing target: {target} ({ver_task["category"].value}) ------') - log_dir = command["log_dir"] - reset_log_dir(log_dir) - cmd = command["command"] - validated = None - - start_time = time.perf_counter() - - with pushd(log_dir): - execution_status, output = run_command_with_timeout(cmd) - log_output(output) - error: bool = check_for_dse_error(output) - points, case = determine_result(output, ver_task['category'], ver_task['verdict']) - - # Store result in the verification task - ver_task['result'] = { - 'points': points, - 'case': case - } - - # ToDo: add witness validation - if 'violation' in case: - validated = generate_and_validate_witness(ver_task, output) - - elapsed_time = time.perf_counter() - start_time - - logger.info(f"{ver_task['category'].value} | Points: {points}, Case: {case}, Execution Status: {execution_status}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s") - - ci_print(f"::endgroup::") - return target, case, points, execution_status, error, validated, elapsed_time - -def check_for_dse_error(output: List[str]) -> bool: - for line in output: - if "SWAT Assertion failed" in line: - return True - return False - - - -def log_output(output: List[str]): - for line in output: - logger.info(line.strip()) - -def run_command_with_timeout(cmd: list[str], timeout: int = 90) -> tuple[ExecutionStatus, list[str]]: - """Executes the given command and returns output from both STDOUT and STDERR.""" - - logger.info(f'[TARGET EXECUTION]: Running symbolic-explorer: {cmd}') - output = [] - with subprocess.Popen( - cmd, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - universal_newlines=True, - bufsize=1 - ) as proc: - try: - # Read output and wait for process to finish, with a timeout - stdout, _ = proc.communicate(timeout=timeout) - output = stdout.splitlines() - - return ExecutionStatus.SUCCESS, output - - - except subprocess.TimeoutExpired: - proc.kill() - stdout, _ = proc.communicate() - output = stdout.splitlines() - return ExecutionStatus.TIMEOUT, output - - except Exception as e: - logger.critical(f'[SVCOMP] Exception: {e}') - proc.kill() - output = [str(e)] - return ExecutionStatus.ERROR, output + [str(e)] - - - -def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50): - max_workers = min(max_workers, len(ver_tasks)) - - logger.info(f"Running parallel target execution with {max_workers} workers...") - - results = {} - for category in VerificationCategory: - results[category.value] = {} - - total_start_time = time.perf_counter() - - with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor: - # Create a mapping from futures to their corresponding tasks - future_to_task = {} - for ver_task in ver_tasks: - future = executor.submit(target_execution, ver_task) - future_to_task[future] = ver_task - - for future in concurrent.futures.as_completed(future_to_task): # type: ignore - try: - # Get the task associated with this future - ver_task = future_to_task[future] - target, case, points, execution_status, error, validated, elapsed_time = future.result() - logger.info(f"{ver_task['category'].value} | Points: {points}, Case: {case}, Execution Status: {execution_status}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s") - - results[ver_task['category'].value][target] = (case, points, execution_status.value, error, validated, elapsed_time) - except Exception as e: - logger.error(f'Exception occurred: {e}') - - total_elapsed_time = time.perf_counter() - total_start_time - logger.info(f"Total parallel execution time: {total_elapsed_time:.2f}s") - - evaluate_results(results) - -def evaluate_results(results): - """Evaluate results with per-category statistics including timing.""" - total_points = 0 - category_stats = {} - all_times = [] # Collect all execution times for histogram - - # Initialize per-category stats - for category_name in results.keys(): - category_stats[category_name] = { - 'points': 0, - 'case_occurrences': {}, - 'execution_statuses': {}, - 'dse_errors': 0, - 'witness_stats': {}, - 'timing': { - 'times': [], - 'min': None, - 'max': None, - 'mean': None, - 'median': None, - 'total': 0 - } - } - - # Process each category's results - for category_name, category_results in results.items(): - category_points = 0 - category_times = [] - - for target, result_tuple in category_results.items(): - # Handle both old format (5 elements) and new format (6 elements with timing) - if len(result_tuple) == 6: - case, points, execution_status, error, validated, elapsed_time = result_tuple - else: - case, points, execution_status, error, validated = result_tuple - elapsed_time = 0.0 - - # Update category stats - category_points += points - category_times.append(elapsed_time) - all_times.append((category_name, target, elapsed_time)) - - stats = category_stats[category_name] - - if case in stats['case_occurrences']: - stats['case_occurrences'][case] += 1 - else: - stats['case_occurrences'][case] = 1 - - if execution_status in stats['execution_statuses']: - stats['execution_statuses'][execution_status] += 1 - else: - stats['execution_statuses'][execution_status] = 1 - - if error: - stats['dse_errors'] += 1 - - if validated in stats['witness_stats']: - stats['witness_stats'][validated] += 1 - else: - stats['witness_stats'][validated] = 1 - - logger.info(f"[{category_name}] Target: {target}, Execution Status: {execution_status}, Case: {case}, Points: {points}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s") - - # Calculate timing statistics for this category - if category_times: - stats = category_stats[category_name] - stats['timing']['times'] = category_times - stats['timing']['min'] = min(category_times) - stats['timing']['max'] = max(category_times) - stats['timing']['mean'] = sum(category_times) / len(category_times) - stats['timing']['total'] = sum(category_times) - sorted_times = sorted(category_times) - mid = len(sorted_times) // 2 - stats['timing']['median'] = sorted_times[mid] if len(sorted_times) % 2 else (sorted_times[mid-1] + sorted_times[mid]) / 2 - - category_stats[category_name]['points'] = category_points - total_points += category_points - - logger.info(f"\n[{category_name}] Category Points: {category_points}") - logger.info(f"[{category_name}] Case occurrences: {category_stats[category_name]['case_occurrences']}") - logger.info(f"[{category_name}] Execution statuses: {category_stats[category_name]['execution_statuses']}") - logger.info(f"[{category_name}] DSE errors: {category_stats[category_name]['dse_errors']}") - logger.info(f"[{category_name}] Witness stats: {category_stats[category_name]['witness_stats']}") - - # Log timing stats - timing = category_stats[category_name]['timing'] - if timing['min'] is not None: - logger.info(f"[{category_name}] Timing: min={timing['min']:.2f}s, max={timing['max']:.2f}s, mean={timing['mean']:.2f}s, median={timing['median']:.2f}s, total={timing['total']:.2f}s") - - logger.info(f"\n{'='*50}") - logger.info(f"TOTAL POINTS (ALL CATEGORIES): {total_points}") - logger.info(f"{'='*50}") - - # Print overall timing summary - if all_times: - all_elapsed = [t[2] for t in all_times] - logger.info(f"Overall timing: min={min(all_elapsed):.2f}s, max={max(all_elapsed):.2f}s, mean={sum(all_elapsed)/len(all_elapsed):.2f}s") - - save_results(category_stats, results) - - # Generate timing histogram - generate_timing_histogram(category_stats, results) - - summary_path = os.getenv("GITHUB_STEP_SUMMARY") - if summary_path is not None: - print_github_ci(total_points, category_stats, results) - - return total_points - - -def generate_timing_histogram(category_stats, results, folder='results'): - """Generate histogram(s) of execution times using matplotlib.""" - if not MATPLOTLIB_AVAILABLE: - logger.warning("matplotlib not available, skipping histogram generation. Install with: pip install matplotlib numpy") - return - - folder = os.path.join(SCRIPT_DIR, '..', folder) - if not os.path.exists(folder): - os.makedirs(folder) - - timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S") - - # Collect all times across categories - all_times = [] - category_times_dict = {} - - for category_name, stats in category_stats.items(): - times = stats['timing'].get('times', []) - if times: - category_times_dict[category_name] = times - all_times.extend(times) - - if not all_times: - logger.info("No timing data available for histogram generation") - return - - # Create figure with subplots - num_categories = len(category_times_dict) - fig_height = 4 + (num_categories * 3) # Dynamic height based on categories - fig, axes = plt.subplots(num_categories + 1, 1, figsize=(12, fig_height)) - - if num_categories == 0: - axes = [axes] - elif num_categories == 1: - axes = [axes[0], axes[1]] - - # Overall histogram - ax_overall = axes[0] - all_times_array = np.array(all_times) - - # Use log scale bins if there's wide variation - if max(all_times) > 10 * min(all_times) and min(all_times) > 0: - bins = np.logspace(np.log10(max(0.1, min(all_times))), np.log10(max(all_times) + 0.1), 30) - ax_overall.set_xscale('log') - else: - bins = 30 - - ax_overall.hist(all_times_array, bins=bins, edgecolor='black', alpha=0.7, color='steelblue') - ax_overall.axvline(np.mean(all_times_array), color='red', linestyle='--', linewidth=2, label=f'Mean: {np.mean(all_times_array):.2f}s') - ax_overall.axvline(np.median(all_times_array), color='green', linestyle='--', linewidth=2, label=f'Median: {np.median(all_times_array):.2f}s') - ax_overall.set_xlabel('Execution Time (seconds)') - ax_overall.set_ylabel('Frequency') - ax_overall.set_title(f'Overall Execution Time Distribution (n={len(all_times)})') - ax_overall.legend() - ax_overall.grid(True, alpha=0.3) - - # Add text box with statistics - stats_text = f'Min: {min(all_times):.2f}s\nMax: {max(all_times):.2f}s\nMean: {np.mean(all_times_array):.2f}s\nMedian: {np.median(all_times_array):.2f}s\nTotal: {sum(all_times):.2f}s' - ax_overall.text(0.98, 0.95, stats_text, transform=ax_overall.transAxes, fontsize=9, - verticalalignment='top', horizontalalignment='right', - bbox=dict(boxstyle='round', facecolor='wheat', alpha=0.5)) - - # Per-category histograms - colors = plt.cm.Set2(np.linspace(0, 1, num_categories)) # type: ignore - for idx, (category_name, times) in enumerate(category_times_dict.items()): - ax = axes[idx + 1] - times_array = np.array(times) - - # Use same binning logic - if max(times) > 10 * min(times) and min(times) > 0: - cat_bins = np.logspace(np.log10(max(0.1, min(times))), np.log10(max(times) + 0.1), 25) - ax.set_xscale('log') - else: - cat_bins = 25 - - ax.hist(times_array, bins=cat_bins, edgecolor='black', alpha=0.7, color=colors[idx]) - ax.axvline(np.mean(times_array), color='red', linestyle='--', linewidth=2, label=f'Mean: {np.mean(times_array):.2f}s') - ax.axvline(np.median(times_array), color='green', linestyle='--', linewidth=2, label=f'Median: {np.median(times_array):.2f}s') - ax.set_xlabel('Execution Time (seconds)') - ax.set_ylabel('Frequency') - ax.set_title(f'{category_name} Execution Time Distribution (n={len(times)})') - ax.legend() - ax.grid(True, alpha=0.3) - - # Add stats box - cat_stats_text = f'Min: {min(times):.2f}s\nMax: {max(times):.2f}s\nMean: {np.mean(times_array):.2f}s\nMedian: {np.median(times_array):.2f}s' - ax.text(0.98, 0.95, cat_stats_text, transform=ax.transAxes, fontsize=9, - verticalalignment='top', horizontalalignment='right', - bbox=dict(boxstyle='round', facecolor='wheat', alpha=0.5)) - - plt.tight_layout() - - # Save histogram - histogram_path = os.path.join(folder, f'timing_histogram_{timestamp}.png') - plt.savefig(histogram_path, dpi=150, bbox_inches='tight') - plt.close() - logger.info(f"Timing histogram saved to: {histogram_path}") - - # Also generate a box plot for comparison - if num_categories > 1: - fig2, ax2 = plt.subplots(figsize=(10, 6)) - box_data = [times for times in category_times_dict.values()] - box_labels = list(category_times_dict.keys()) - - bp = ax2.boxplot(box_data, labels=box_labels, patch_artist=True) - for patch, color in zip(bp['boxes'], colors): - patch.set_facecolor(color) - - ax2.set_ylabel('Execution Time (seconds)') - ax2.set_title('Execution Time Comparison by Category') - ax2.grid(True, alpha=0.3, axis='y') - - # Rotate labels if they're long - plt.xticks(rotation=45, ha='right') - plt.tight_layout() - - boxplot_path = os.path.join(folder, f'timing_boxplot_{timestamp}.png') - plt.savefig(boxplot_path, dpi=150, bbox_inches='tight') - plt.close() - logger.info(f"Timing boxplot saved to: {boxplot_path}") - - -def save_results(category_stats, results, folder='results'): - """Save results with one JSON file per category, including timing data.""" - folder = os.path.join(SCRIPT_DIR, '..', folder) - - if not os.path.exists(folder): - os.makedirs(folder) - - timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S") - - # Save one file per category - for category_name, stats in category_stats.items(): - # Convert Path keys to strings for JSON serialization - category_results = results[category_name] - results_serializable = {str(k): v for k, v in category_results.items()} - - # Prepare timing stats (exclude raw times array for cleaner JSON) - timing_stats = { - 'min': stats['timing'].get('min'), - 'max': stats['timing'].get('max'), - 'mean': stats['timing'].get('mean'), - 'median': stats['timing'].get('median'), - 'total': stats['timing'].get('total'), - 'count': len(stats['timing'].get('times', [])) - } - - data = { - 'category': category_name, - 'points': stats['points'], - 'case_occurrences': stats['case_occurrences'], - 'execution_statuses': stats['execution_statuses'], - 'dse_errors': stats['dse_errors'], - 'witness_stats': stats['witness_stats'], - 'timing': timing_stats, - 'results': results_serializable - } - - filename = f"results_{category_name}_{timestamp}.json" - filepath = os.path.join(folder, filename) - - with open(filepath, 'w') as f: - json.dump(data, f, indent=4) - - logger.info(f"[{category_name}] Results saved to {filepath}") - - -def print_github_ci(total_points, category_stats, results): - """Print GitHub CI summary with per-category breakdown.""" - def bool_to_emoji(value): - if value is None: - return "❌" - return "✅" if value else "❌" - - summary_path = os.getenv("GITHUB_STEP_SUMMARY") - if summary_path is None: - raise EnvironmentError("GITHUB_STEP_SUMMARY is not set. Are you running inside GitHub Actions?") - - with open(summary_path, "a") as f: - # Header - f.write("## 🧾 Symbolic Execution Summary\n\n") - f.write(f"**Total Points (All Categories):** `{total_points}`\n\n") - - # Per-Category Summary - f.write("### 📊 Points by Category\n") - f.write("| Category | Points |\n") - f.write("|----------|--------|\n") - for category_name, stats in category_stats.items(): - f.write(f"| {category_name} | {stats['points']} |\n") - f.write("\n") - - # Detailed breakdown per category - for category_name, stats in category_stats.items(): - f.write(f"## {category_name}\n\n") - - # Case Occurrences - if stats['case_occurrences']: - f.write("### 📊 Case Occurrences\n") - f.write("| Case | Count |\n") - f.write("|------|-------|\n") - for k, v in stats['case_occurrences'].items(): - f.write(f"| {k} | {v} |\n") - f.write("\n") - - # Execution Statuses - if stats['execution_statuses']: - f.write("### ⚙️ Execution Statuses\n") - f.write("| Status | Count |\n") - f.write("|--------|-------|\n") - for k, v in stats['execution_statuses'].items(): - f.write(f"| {k} | {v} |\n") - f.write("\n") - - # DSE Errors - f.write(f"**DSE Errors:** `{stats['dse_errors']}`\n\n") - - # Timing Stats - timing = stats.get('timing', {}) - if timing.get('min') is not None: - f.write("### ⏱️ Timing Statistics\n") - f.write("| Metric | Value |\n") - f.write("|--------|-------|\n") - f.write(f"| Min | {timing['min']:.2f}s |\n") - f.write(f"| Max | {timing['max']:.2f}s |\n") - f.write(f"| Mean | {timing['mean']:.2f}s |\n") - f.write(f"| Median | {timing['median']:.2f}s |\n") - f.write(f"| Total | {timing['total']:.2f}s |\n") - f.write("\n") - - # Witness Stats - if stats['witness_stats'] and any(stats['witness_stats'].values()): - f.write("### 🧷 Witness Stats\n") - f.write("| Validated | Count |\n") - f.write("|-----------|-------|\n") - for validated, count in stats['witness_stats'].items(): - f.write(f"| {bool_to_emoji(validated)} | {count} |\n") - f.write("\n") - - -def select_target(ver_tasks: list[VerificationTask], target_name: str) -> Optional[VerificationTask]: - """Select a verification task by target name.""" - for ver_task in ver_tasks: - command = ver_task.get('command') - if command and str(command['target']) == target_name: - return ver_task - return None - - -def run_single_target(ver_tasks: list[VerificationTask]): - target = "autostub/Boolean_public_static_int_java_lang_Boolean_compare_boolean_boolean" - - ver_task = select_target(ver_tasks, target) - if ver_task is None: - logger.error(f"Target {target} not found.") - return - logger.info(f"Running single target: {target}") - ver_task["command"]["log_dir"] = Path(str(ver_task["command"]["log_dir"]).replace('/logs/', '/logs-debug/')) # type: ignore - target_execution(ver_task) - - - -if __name__ == "__main__": - mode = Mode.PARALLEL # Mode.SINGLE_TARGET - - # Configure which properties/categories to run (None = all) - selected_categories = [ - VerificationCategory.VALID_ASSERT_PRP, - #VerificationCategory.NO_RUNTIME_EXCEPTION_PRP - ] - - logger.info(f"Running target execution script in {mode.value} mode...") - test_dir = SCRIPT_DIR.parent / "sv-benchmarks" - logger.info(f"Base directory: {test_dir}") - ver_tasks: list[VerificationTask] = extract_testcases(test_dir) - logger.info(f"Extracted {len(ver_tasks)} test cases.") - - # Filter by selected categories if specified - if selected_categories is not None: # type: ignore - ver_tasks = [task for task in ver_tasks if task['category'] in selected_categories] - logger.info(f"Filtered to {len(ver_tasks)} test cases for categories: {[c.value for c in selected_categories]}") - - if mode == Mode.SINGLE_TARGET: # type: ignore - config_file = "swat-debug.cfg" - elif mode == Mode.PARALLEL: - config_file = "sv-comp.cfg" - else: - raise ValueError(f"Invalid mode: {mode}") - ver_tasks_with_commands = generate_commands(ver_tasks, config_file)#[:10] - logger.info(f"Generated {len(ver_tasks_with_commands)} commands.") - - # Check port availability before starting tests (sanity check) - # Note: Command generation already skips occupied ports, but this serves as a final validation - ports_available, occupied_ports = check_port_availability(ver_tasks_with_commands) - if not ports_available: - logger.warning(f"WARNING: {len(occupied_ports)} ports became occupied between command generation and execution.") - logger.warning(f"Occupied ports: {occupied_ports}") - logger.warning("This may cause some tests to fail. Consider restarting the script.") - - if mode == Mode.SINGLE_TARGET: # type: ignore - run_single_target(ver_tasks_with_commands) - elif mode == Mode.PARALLEL: - run_parallel(ver_tasks_with_commands) - else: - raise ValueError(f"Invalid mode: {mode}") - - logger.info("Done.") - diff --git a/targets/sv-comp/scripts/target_selection.py b/targets/sv-comp/scripts/target_selection.py deleted file mode 100644 index a72fa95..0000000 --- a/targets/sv-comp/scripts/target_selection.py +++ /dev/null @@ -1,90 +0,0 @@ -from typing import Any -from collections import defaultdict -import yaml -import logging -from pathlib import Path -from pprint import pformat -from dtypes import ExpectedVerdict, VerificationCategory, VerificationTask - -logging.basicConfig(level=logging.INFO) -logger = logging.getLogger(__name__) - -SCRIPT_DIR = Path(__file__).resolve().parent - -def validate_property_file_format(data: dict[str, Any]) -> bool: - # Validate the structure - return ( - "format_version" in data and data["format_version"] == "2.0" and - "input_files" in data and isinstance(data["input_files"], list) and - "properties" in data and isinstance(data["properties"], list) and - len(data["properties"]) >= 1 and # type: ignore - "property_file" in data["properties"][0] and "expected_verdict" in data["properties"][0] and - "options" in data and "language" in data["options"] and data["options"]["language"] == "Java" - ) - -def extract_testcases(path: Path) -> list[VerificationTask]: - ver_tasks: list[VerificationTask] = [] - - # Use Path.rglob to recursively find all YAML files - yaml_files = [*path.rglob("*.yml"), *path.rglob("*.yaml")] - for file_path in yaml_files: - logger.debug(f"Loading YAML file: {file_path}") - with open(file_path, 'r') as f: - try: - data: dict[str, Any] = yaml.safe_load(f) - except yaml.YAMLError as e: - raise ValueError(f"Error parsing YAML file {file_path}: {e}") - - if not validate_property_file_format(data): - raise ValueError(f"Invalid format in YAML file: {file_path}") - - for property in data["properties"]: - ver_task: VerificationTask = { - 'category': VerificationCategory(property['property_file'].split('/')[-1]), - 'verdict': ExpectedVerdict(property['expected_verdict']), - 'file_path': file_path, - 'input_files': data["input_files"], - 'command': None, - 'result': None - } - ver_tasks.append(ver_task) - - logger.debug(f"Loaded test case: {file_path}") - - return ver_tasks - - -def print_testcase_statistics(ver_tasks: list[VerificationTask]) -> None: - """Print concise statistics about test cases by category.""" - # Count verdicts for each category using nested defaultdict - stats: defaultdict[VerificationCategory, defaultdict[ExpectedVerdict, int]] = defaultdict(lambda: defaultdict(int)) - - for task in ver_tasks: - stats[task['category']][task['verdict']] += 1 - - logger.info(f"{'='*60}") - logger.info(f"Test Case Statistics (Total: {len(ver_tasks)})") - logger.info(f"{'='*60}") - logger.info(f"{'Property':<30} {'Safe':<10} {'Violation':<10}") - logger.info(f"{'-'*60}") - - for category in VerificationCategory: - safe_count = stats[category][ExpectedVerdict.SAFE] - violation_count = stats[category][ExpectedVerdict.VIOLATION] - logger.info(f"{category.value:<30} {safe_count:<10} {violation_count:<10}") - - logger.info(f"{'='*60}") - - -if __name__ == "__main__": - logger.info("Testing testcase extraction script...") - test_dir = (SCRIPT_DIR / ".." / "sv-benchmarks").resolve() - logger.info(f"Base directory: {test_dir}") - test_cases = extract_testcases(test_dir) - logger.info(f"Loaded {len(test_cases)} test cases from directory: {test_dir}") - - print_testcase_statistics(test_cases) - - logger.info("\nFirst 3 test cases:") - for i, case in enumerate(test_cases[:3], 1): - logger.info(f"\nTest Case {i}:\n{pformat(dict(case), width=100)}") \ No newline at end of file diff --git a/targets/sv-comp/scripts/util.py b/targets/sv-comp/scripts/util.py deleted file mode 100644 index f88041e..0000000 --- a/targets/sv-comp/scripts/util.py +++ /dev/null @@ -1,10 +0,0 @@ -import os -from typing import Any - - -IS_RUNNING_IN_CI: bool = os.getenv("CI", "false") == "true" - -def ci_print(message: Any) -> None: - """Print a message formatted for CI systems.""" - if IS_RUNNING_IN_CI: - print(f"{message}") \ No newline at end of file diff --git a/targets/sv-comp/scripts/witness_validation.py b/targets/sv-comp/scripts/witness_validation.py deleted file mode 100644 index 158821b..0000000 --- a/targets/sv-comp/scripts/witness_validation.py +++ /dev/null @@ -1,187 +0,0 @@ -import base64 -from contextlib import contextmanager -import os -import enum -import logging -import shutil -import subprocess -from typing import List, Optional -from pathlib import Path -from dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command - -logger = logging.getLogger(__name__) -SCRIPT_DIR = Path(__file__).resolve().parent -WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar') -WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java') - -class ExecutionStatus(enum.Enum): - SUCCESS = "success" - ERROR = "error" - TIMEOUT = "timeout" - - - -def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) -> Optional[bool]: - """Extract witnesses from `output`, create witness files and validate them. - - Returns True/False on validation result or None if no witness was found. - """ - # Build an `info` dict compatible with the legacy implementation - command_dict = ver_task.get('command', {}) - info = { - 'command': command_dict.get('command', []), - 'log_dir': str(command_dict.get('log_dir', SCRIPT_DIR)) - } - - out = extract_last_round(output) - witnesses = extract_markers(out, "[WITNESS]") - if not witnesses: - logger.debug("No witnesses found in output") - return None - - witness_dir = assemble_files(info) - logger.info("Generating witness files") - generate_witness(witness_dir, "\n".join(witnesses)) - logger.info("Validating witness") - return validate_witness(info) - - -def log_output(output: List[str]): - for line in output: - logger.info(line.strip()) - -def validate_witness(info: dict) -> bool: - """Run the external witness validator and return True if witness is correct.""" - cmd: List[str] = [str(WITNESS_VALIDATION_PATH), '--packages'] - main_folder = '' - - # find classpath entries (items after --classpath) - try: - classpath_index = info['command'].index('--classpath') - classpath_entries = info['command'][classpath_index + 1:] - except ValueError: - classpath_entries = [] - - for folder in classpath_entries: - try: - if 'Main.java' in os.listdir(folder): - main_folder = folder - else: - cmd.append(folder) - except Exception: - # ignore non-folders or missing paths - continue - - cmd.extend(['--witness', str(Path(info['log_dir']) / 'witness' / 'witness.graphml')]) - if main_folder: - cmd.append(main_folder) - - _, output = run_command_with_timeout(cmd) - logger.info("Witness Validation Output") - log_output(output) - for line in output: - if "wit4java: Witness Correct" in line: - return True - return False - - -@contextmanager -def pushd(dirname): - """Context manager to temporarily change the working directory.""" - original_dir = os.getcwd() - logger.info(f"Changing directory to: {dirname}") - os.chdir(dirname) - try: - yield - finally: - os.chdir(original_dir) - - - -def extract_last_round(out: List[str], marker: str = "============================== ROUND") -> str: - return "\n".join(out).split(marker)[-1] - - - -def extract_markers(out: str, marker: str) -> List[str]: - res: List[str] = [] - for line in out.split("\n"): - logger.debug(line) - if marker in line: - res.append(line) - return res - -def generate_witness(witness_dir: str, witness: str) -> None: - with pushd(str(SCRIPT_DIR.parent / 'WitnessCreator')): - # base64 encode the string - enc = base64.b64encode(witness.encode()).decode() - cmd = [ - 'java', - '-jar', - str(WITNESS_CREATION_PATH), - enc, - str(witness_dir) - ] - logger.info(f"Running witness creator: {cmd}") - _, output = run_command_with_timeout(cmd) - logger.info("Witness created") - log_output(output) - -def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[ExecutionStatus, list[str]]: - """Executes the given command and returns output from both STDOUT and STDERR.""" - - logger.info(f'[WITNESS] Running: {cmd}') - output = [] - with subprocess.Popen( - cmd, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - universal_newlines=True, - bufsize=1 - ) as proc: - try: - # Read output and wait for process to finish, with a timeout - stdout, _ = proc.communicate(timeout=timeout) - output = stdout.splitlines() - - return ExecutionStatus.SUCCESS, output - - - except subprocess.TimeoutExpired: - proc.kill() - stdout, _ = proc.communicate() - output = stdout.splitlines() - return ExecutionStatus.TIMEOUT, output - - except Exception as e: - logger.critical(f'[SVCOMP] Exception: {e}') - proc.kill() - output = [str(e)] - return ExecutionStatus.ERROR, output + [str(e)] - - -def assemble_files(info: dict) -> str: - witness_dir = Path(info['log_dir']) / 'witness' - witness_dir.mkdir(parents=True, exist_ok=True) - - try: - classpath_index = info['command'].index('--classpath') - classpath_entries = info['command'][classpath_index + 1:] - except ValueError: - classpath_entries = [] - - for folder in classpath_entries: - folder_path = Path(folder) - if not folder_path.exists(): - continue - for src in folder_path.rglob('*.java'): - # Preserve relative path structure (package directories) for WitnessCreator - rel_path = src.relative_to(folder_path) - dst = witness_dir / rel_path - dst.parent.mkdir(parents=True, exist_ok=True) - logger.info(f"Copying {src} to {dst}") - shutil.copy(str(src), str(dst)) - - return str(witness_dir) - - \ No newline at end of file