From ae1b9e5ae083be642a8e6d5ed7a6988dedef951e Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:55:09 +0000 Subject: [PATCH 1/2] Handle a StackOverflowError in the target as the plain JVM would Deep recursion plus the frames of the symbolic tracking can exhaust the stack anywhere, including inside SWAT. The second overflow then hit the lazy static initializer of ErrorHandler, which broke the class for the rest of the run, left isActive set and replaced the target's error by a NoClassDefFoundError: the target's own handlers did not run, and the truncated trace was sent without any marker. - ErrorHandler and the new StackOverflowGuard are initialised in premain. - processInstruction swallows a StackOverflowError raised inside SWAT (field writes only) and stops tracking for the rest of the execution; isActive is reset in finally. ErrorHandler passes a stack overflow on instead of halting. - The exception handler of every instrumented call site records a StackOverflowError that reaches the target's code (DUP, INSTANCEOF, IOR into a static field; no call, no branch) before INVOKEMETHOD_EXCEPTION. - The trace of such an execution is marked as context loss, and as stackOverflow when the error reached the target: that path depends on the JVM's stack size, which the task does not fix. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/common/ErrorHandler.java | 8 ++ .../its/swat/common/StackOverflowGuard.java | 60 +++++++++ .../uzl/its/swat/instrument/Transformer.java | 5 + .../instruction/InstructionMethodAdapter.java | 20 +++ .../SymbolicInstructionProcessor.java | 22 +++- .../its/swat/symbolic/trace/DTOBuilder.java | 11 +- .../its/swat/symbolic/trace/dto/TraceDTO.java | 7 +- .../symbolic/StackOverflowAgentSpec.groovy | 116 ++++++++++++++++++ .../resources/targets/stackoverflow/Main.java | 31 +++++ .../org/sosy_lab/sv_benchmarks/Verifier.java | 46 +++++++ 10 files changed, 319 insertions(+), 7 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/common/StackOverflowGuard.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StackOverflowAgentSpec.groovy create mode 100644 symbolic-executor/src/test/resources/targets/stackoverflow/Main.java create mode 100644 symbolic-executor/src/test/resources/targets/stackoverflow/org/sosy_lab/sv_benchmarks/Verifier.java 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 18a888a1..95bb5338 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 @@ -50,6 +50,14 @@ public void raiseException(String msg) { * @param t the throwable to handle */ public void handleException(String msg, Throwable t) { + // A stack overflow is not a SWAT failure: stop the symbolic tracking (the trace becomes + // context loss) and let the error take its course in the target, as without SWAT. Nothing + // is logged, the stack is exhausted. + Error stackOverflow = StackOverflowGuard.findStackOverflow(t); + if (stackOverflow != null) { + StackOverflowGuard.trackingLost = true; + throw stackOverflow; + } long instCnt = -1; try { instCnt = ThreadHandler.getInstructionCount(currentThread().getId()); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/StackOverflowGuard.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/StackOverflowGuard.java new file mode 100644 index 00000000..df54fa86 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/StackOverflowGuard.java @@ -0,0 +1,60 @@ +package de.uzl.its.swat.common; + +/** + * Records that the JVM stack overflowed during the execution. Deep recursion in the target plus the + * frames of the symbolic tracking can exhaust the stack, and a {@link StackOverflowError} can then + * strike anywhere: in the target's own frames or inside SWAT while an instruction is processed. + * + * + * + * Both end the symbolic tracking and mark the trace as context loss. The fields are written + * without any call, so that they can be set on an exhausted stack; the class is initialised + * eagerly by the agent for the same reason. They are global, like the instruction processor whose + * state they guard. + */ +public final class StackOverflowGuard { + + public static volatile boolean trackingLost = false; + public static volatile boolean targetOverflowed = false; + + private StackOverflowGuard() {} + + /** Forces the initialisation of the class (see the class comment). */ + public static void init() {} + + /** Whether symbolic tracking has stopped because of a stack overflow. */ + public static boolean isOverflowed() { + return trackingLost | targetOverflowed; + } + + /** + * Returns the StackOverflowError behind {@code t}, or the initialiser error of a class whose + * static initialiser it broke, or null if {@code t} is not caused by a stack overflow. + */ + public static Error findStackOverflow(Throwable t) { + for (int depth = 0; t != null && depth < 16; depth++, t = t.getCause()) { + if (t instanceof StackOverflowError e) { + return e; + } + if (t instanceof ExceptionInInitializerError e + && String.valueOf(e.getMessage()).contains("java.lang.StackOverflowError")) { + return e; + } + } + return null; + } + + /** Clears the state; only for tests that run several executions in one JVM. */ + public static void reset() { + trackingLost = false; + targetOverflowed = false; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java index bb29b91e..aa76fe5d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java @@ -3,6 +3,7 @@ import ch.qos.logback.classic.Logger; import ch.qos.logback.classic.LoggerContext; import de.uzl.its.swat.common.ErrorHandler; +import de.uzl.its.swat.common.StackOverflowGuard; import de.uzl.its.swat.common.PrintBox; import de.uzl.its.swat.common.Util; import de.uzl.its.swat.common.exceptions.InstrumentationException; @@ -134,6 +135,10 @@ public static void logMissedClasses(){ @SuppressWarnings("unused") public static void premain(String agentArgs, Instrumentation inst) { try { + // Initialised here, not on first use: that can be on an exhausted stack, where a + // failing static initialiser would break the class for the rest of the run + StackOverflowGuard.init(); + new ErrorHandler(); ThreadHandler.init(); ThreadHandler.addThreadContext(-1, "SymbolicThread", -1); // Main thread used during initialization and instrumentation diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java index b24ee90c..82975e31 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java @@ -1,6 +1,7 @@ package de.uzl.its.swat.instrument.instruction; import de.uzl.its.swat.common.ErrorHandler; +import de.uzl.its.swat.common.StackOverflowGuard; import de.uzl.its.swat.common.exceptions.InstrumentationException; import de.uzl.its.swat.common.exceptions.SWATAssert; import de.uzl.its.swat.config.Config; @@ -1521,6 +1522,23 @@ private boolean isFieldGetFieldMethod(String method) { return getFieldMethods.contains(method); } + /** + * Records a StackOverflowError that reaches the exception handler of a call site in + * StackOverflowGuard.targetOverflowed, before the exception is reported to SWAT. Expects the + * throwable on top of the operand stack and leaves it there. No call and no branch: on an + * exhausted stack a call could replace the exception in flight. + * + * 
targetOverflowed |= (throwable instanceof StackOverflowError)
+ */ + private void addStackOverflowCheck(MethodVisitor mv) { + String guard = Type.getInternalName(StackOverflowGuard.class); + mv.visitInsn(DUP); + mv.visitTypeInsn(INSTANCEOF, "java/lang/StackOverflowError"); + mv.visitFieldInsn(GETSTATIC, guard, "targetOverflowed", "Z"); + mv.visitInsn(IOR); + mv.visitFieldInsn(PUTSTATIC, guard, "targetOverflowed", "Z"); + } + private void addMethodWithTryCatch( int opcode, String owner, String name, String desc, boolean itf) { @@ -1580,6 +1598,7 @@ private void addMethodWithTryCatch( mv.visitJumpInsn(GOTO, jumpTarget); mv.visitLabel(handler); + addStackOverflowCheck(mv); addJpushInsn(mv, instrumentationState.incAndGetId()); addJpushInsn(mv, invokeId); @@ -1656,6 +1675,7 @@ public void visitInvokeDynamicInsn(String name, String desc, Handle bsm, Object. mv.visitJumpInsn(GOTO, jumpTarget); // still try catch mv.visitLabel(handler); + addStackOverflowCheck(mv); addJpushInsn(mv, instrumentationState.incAndGetId()); addJpushInsn(mv, invokeId); mv.visitMethodInsn( diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/SymbolicInstructionProcessor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/SymbolicInstructionProcessor.java index cd419184..5b0e9228 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/SymbolicInstructionProcessor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/SymbolicInstructionProcessor.java @@ -3,6 +3,7 @@ import ch.qos.logback.classic.Level; import ch.qos.logback.classic.Logger; import de.uzl.its.swat.common.ErrorHandler; +import de.uzl.its.swat.common.StackOverflowGuard; import de.uzl.its.swat.common.Util; import de.uzl.its.swat.common.exceptions.SWATAssert; import de.uzl.its.swat.common.logging.GlobalLogger; @@ -175,6 +176,10 @@ private boolean isActualMethodNameExpectedMethodName(String actualMethodName, St */ @Override public void processInstruction(Instruction nextInstruction) { + // After a stack overflow the shadow state is no longer reliable: stop tracking + if (StackOverflowGuard.trackingLost | StackOverflowGuard.targetOverflowed) { + return; + } try { SWATAssert.enforce(!isActive, "Symbolic execution is already active!"); isActive = true; @@ -350,13 +355,22 @@ && adoptLambdaFrame(visitor.getStack(), expectedCnameFull, ThreadHandler.setCurrentInstruction(id, ThreadHandler.getNextInstruction(id)); } + } catch (StackOverflowError e) { + // Only field writes here: the stack is still exhausted. The error is swallowed, so the + // target continues as it would without SWAT; the trace is marked as context loss. + StackOverflowGuard.trackingLost = true; } catch (Throwable t) { - new ErrorHandler().handleException("Error visiting Instruction!", t); + if (StackOverflowGuard.findStackOverflow(t) != null) { + StackOverflowGuard.trackingLost = true; + } else { + new ErrorHandler().handleException("Error visiting Instruction!", t); + } } finally { - long id = Thread.currentThread().getId(); - ThreadHandler.checkThreadContextAbortTimer(id); + isActive = false; + } + if (!(StackOverflowGuard.trackingLost | StackOverflowGuard.targetOverflowed)) { + ThreadHandler.checkThreadContextAbortTimer(Thread.currentThread().getId()); } - isActive = false; } /** 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 e272cf71..dacb6da9 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 @@ -8,6 +8,7 @@ import com.fasterxml.jackson.core.JsonProcessingException; import com.fasterxml.jackson.databind.ObjectMapper; import de.uzl.its.swat.common.ErrorHandler; +import de.uzl.its.swat.common.StackOverflowGuard; import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.logging.GlobalLogger; @@ -148,8 +149,14 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage trace.add(new BranchDTO(se.getIid(), se.getInst())); } } - return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), Witness.getNondetReturns(), Witness.getViolation(), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange(), - symbolicTrace.isSymbolicPrecisionLoss()); + // Symbolic tracking stopped at a stack overflow: the rest of the execution is not in the trace + boolean stackOverflow = StackOverflowGuard.isOverflowed(); + if (stackOverflow) { + logger.warn("Stack overflow during the execution (in SWAT: {}, reached the target: {}): recording symbolic context loss", + StackOverflowGuard.trackingLost, StackOverflowGuard.targetOverflowed); + } + return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), Witness.getNondetReturns(), Witness.getViolation(), symbolicTrace.isSymbolicContextLoss() || stackOverflow, symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange(), + symbolicTrace.isSymbolicPrecisionLoss(), StackOverflowGuard.targetOverflowed); } protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException { 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 bc99d00f..a9046e05 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 @@ -35,8 +35,12 @@ public class TraceDTO { // which also covers exact UF-based models, solutions from such a trace are only guesses. @SuppressWarnings("unused") private boolean approximateModel = false; + // A StackOverflowError reached the target's code: the path depends on the JVM's stack size, + // so a violation of this execution is not a verdict (see StackOverflowGuard) + @SuppressWarnings("unused") + private boolean stackOverflow = false; - public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, ArrayList missingInvocations, ArrayList nondetReturns, ViolationDTO violation, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange, boolean approximateModel) { + public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, ArrayList missingInvocations, ArrayList nondetReturns, ViolationDTO violation, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange, boolean approximateModel, boolean stackOverflow) { this.trace = trace; this.inputs = inputs; this.ufs = ufs; @@ -47,6 +51,7 @@ public TraceDTO(ArrayList inputs, ArrayList trace, ArrayLis this.symbolicPrecisionLoss = symbolicPrecisionLoss; this.referenceSemanticChange = referenceSemanticChange; this.approximateModel = approximateModel; + this.stackOverflow = stackOverflow; } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StackOverflowAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StackOverflowAgentSpec.groovy new file mode 100644 index 00000000..81ddf82a --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StackOverflowAgentSpec.groovy @@ -0,0 +1,116 @@ +package de.uzl.its.swat.symbolic + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): a StackOverflowError in the target behaves as without SWAT. The target + * recurses as deep as its first input, on a small stack so that the overflow comes quickly; the + * second input selects whether main catches the overflow. Run in {@code solver.mode=PRINT}, the + * target must produce its own output, and the trace must be sent and marked as context loss and as + * stack overflow. Runs via the {@code agentTest} Gradle task (needs the agent jar from + * {@code copyJar}). + */ +class StackOverflowAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGET_SOURCES = Path.of("src", "test", "resources", "targets", "stackoverflow").toAbsolutePath() + static final String DEEP = "1000000000" + + @Shared Path classes + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-stackoverflow-agent-spec") + compile(classes) + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + def "a shallow recursion is tracked as usual"() { + when: + def out = run(classes, "100", "0") + def trace = parseTrace(out) + + then: + out.contains("result 100") + !trace.stackOverflow + !trace.symbolicContextLoss + trace.violation == null + } + + def "an overflow caught by the target is handled by the target and recorded in the trace"() { + when: + def out = run(classes, DEEP, "0") + def trace = parseTrace(out) + + then: "the target's handler ran, and SWAT neither crashed nor halted" + out.contains("result -1") + !out.contains("[SWAT Exception]") + !out.contains("NoClassDefFoundError") + + and: "the trace up to the overflow is sent, and cannot lead to SAFE or to a violation" + trace.stackOverflow + trace.symbolicContextLoss + trace.trace.size() > 0 + } + + def "an uncaught overflow ends the target as without SWAT"() { + when: + def out = run(classes, DEEP, "1") + def trace = parseTrace(out) + + then: + !out.contains("result") + !out.contains("[SWAT Exception]") + !out.contains("[SWAT] Uncaught top-level RuntimeException") + trace.violation.throwable == "java.lang.StackOverflowError" + trace.stackOverflow + trace.symbolicContextLoss + } + + private static void compile(Path outDir) { + def sources = Files.walk(TARGET_SOURCES).filter { it.toString().endsWith(".java") }.collect { it.toString() } + def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[]) + assert rc == 0: "javac failed: ${err}" + } + + private static String run(Path classes, String n, String uncaught) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-Xss256k", + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=true", + "-DlogShadowStateToConsole=false", + "-Dswat.input.I_0=${n}".toString(), + "-Dswat.input.I_1=${uncaught}".toString(), + "-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/resources/targets/stackoverflow/Main.java b/symbolic-executor/src/test/resources/targets/stackoverflow/Main.java new file mode 100644 index 00000000..6f36def0 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/stackoverflow/Main.java @@ -0,0 +1,31 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Recursion as deep as the first input; the second input selects whether main catches an overflow. */ +public class Main { + static int depth(int n) { + if (n == 0) { + return 0; + } + return 1 + depth(n - 1); + } + + public static void main(String[] args) { + int n = Verifier.nondetInt(); + boolean catchOverflow = Verifier.nondetInt() == 0; + if (n < 0) { + return; + } + if (!catchOverflow) { + System.out.println("result " + depth(n)); + return; + } + int r; + try { + r = depth(n); + } catch (StackOverflowError e) { + r = -1; + } + System.out.println("result " + r); + assert r == n; + } +} diff --git a/symbolic-executor/src/test/resources/targets/stackoverflow/org/sosy_lab/sv_benchmarks/Verifier.java b/symbolic-executor/src/test/resources/targets/stackoverflow/org/sosy_lab/sv_benchmarks/Verifier.java new file mode 100644 index 00000000..2dcbc9ac --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/stackoverflow/org/sosy_lab/sv_benchmarks/Verifier.java @@ -0,0 +1,46 @@ +package org.sosy_lab.sv_benchmarks; + +/** Minimal stand-in for the sv-benchmarks Verifier; the SV-COMP transformer redirects the calls. */ +public final class Verifier { + public static void assume(boolean condition) { + if (!condition) { + Runtime.getRuntime().halt(1); + } + } + + public static boolean nondetBoolean() { + return false; + } + + public static byte nondetByte() { + return 0; + } + + public static char nondetChar() { + return 0; + } + + public static short nondetShort() { + return 0; + } + + public static int nondetInt() { + return 0; + } + + public static long nondetLong() { + return 0; + } + + public static float nondetFloat() { + return 0; + } + + public static double nondetDouble() { + return 0; + } + + public static String nondetString() { + return ""; + } +} From db097ce1ece30be5a2c325deb389a62b3de9e0c9 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:55:09 +0000 Subject: [PATCH 2/2] Do not report a violation of an execution that overflowed the stack The executor marks a trace with stackOverflow when a StackOverflowError reached the target's code. Whether such an execution fails an assertion or throws a RuntimeException depends on the JVM's stack size, not on the task, so the driver drops its violation lines (recorded as the execution error stack_overflow_violation) and continues the search; the trace's context loss keeps the run from ending SAFE. An execution without symbolic inputs that overflowed ends UNKNOWN instead of SAFE. Co-Authored-By: Claude Opus 5.5 --- .../constraint/ConstraintController.py | 4 +- .../constraint/ConstraintService.py | 7 +- .../data/BinaryExecutionTree/Tree.py | 3 + symbolic-explorer/data/Database.py | 12 ++- symbolic-explorer/driver/SVCompDriver.py | 34 ++++++- .../parse/DataTransferObjects.py | 3 + symbolic-explorer/svcomp/TestcaseStats.py | 1 + .../tests/test_stack_overflow.py | 93 +++++++++++++++++++ 8 files changed, 152 insertions(+), 5 deletions(-) create mode 100644 symbolic-explorer/tests/test_stack_overflow.py diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py index b00359d9..29e7b7aa 100755 --- a/symbolic-explorer/constraint/ConstraintController.py +++ b/symbolic-explorer/constraint/ConstraintController.py @@ -45,6 +45,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str nondetReturns = request.nondetReturns violation = request.violation approximateModel = request.approximateModel + stackOverflow = request.stackOverflow # Start a new thread to add constraints thread = threading.Thread(target=ConstraintService.add_constraints, kwargs={ @@ -59,7 +60,8 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str 'reference_semantic_change': referenceSemanticChange, 'nondet_returns': nondetReturns, 'violation': violation, - 'approximate_model': approximateModel}) + 'approximate_model': approximateModel, + 'stack_overflow': stackOverflow}) thread.start() thread.join() # To ensure trace is added in SV-Comp mode # Return a response indicating that the request has been accepted diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py index 7bba9d09..c9171edd 100755 --- a/symbolic-explorer/constraint/ConstraintService.py +++ b/symbolic-explorer/constraint/ConstraintService.py @@ -27,7 +27,8 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp missing_invocations: List[InvocationItem] = None, nondet_returns: List[NondetReturnItem] = None, violation: Optional[ViolationItem] = None, - approximate_model: bool = False): + approximate_model: bool = False, + stack_overflow: bool = False): """ Adds constraints to the database. @@ -49,6 +50,8 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp violation (ViolationItem): The throwable that escaped the entry method, if any. approximate_model (bool): Whether an approximate model (a sampled Math function) was used, so that solutions built from this trace are only guesses. + stack_overflow (bool): Whether a StackOverflowError reached the target's code, so that a + violation of this execution depends on the JVM's stack size. Returns: None: The result is the side effect of adding data to the database. @@ -71,5 +74,5 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp 'violation': violation.model_dump() if violation is not None else None, } # 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, missing_invocations_data, witness_data, approximate_model) + 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, witness_data, approximate_model, stack_overflow) 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 978dc99e..613a8f53 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -36,6 +36,9 @@ def __init__(self, endpoint_id: Union[str, int]): # Traces that used an approximate model (a sampled Math function). A solution built from one # is a guess, so the next run may take another path than predicted without anything being wrong. self.approximate_traces: Set[str] = set() + # Traces whose execution had a StackOverflowError reach the target's code: their outcome + # depends on the JVM's stack size, so a violation they show is not a verdict. + self.stack_overflow_traces: Set[str] = set() # How often the next run did take another path than such a guessed solution predicted. self.expected_divergences: int = 0 self.uncaught_exceptions: int = 0 diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index 53bf1882..79bb476e 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -119,7 +119,8 @@ def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Bra symbolic_context_loss: bool, symbolic_precision_loss: bool, reference_semantic_change: bool = False, missing_invocations: list = None, witness_data: dict = None, - approximate_model: bool = False): + approximate_model: bool = False, + stack_overflow: bool = False): endpoint_id = str(endpoint_id) lock.acquire() @@ -136,6 +137,7 @@ def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Bra 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 self.tree[endpoint_id].approximate_traces.add(trace_id) if approximate_model else None + self.tree[endpoint_id].stack_overflow_traces.add(trace_id) if stack_overflow else None lock.release() @@ -187,6 +189,14 @@ def is_approximate_trace(self, endpoint_id: Union[str, int], trace_id: str) -> b lock.release() return ret + def is_stack_overflow_trace(self, endpoint_id: Union[str, int], trace_id: str) -> bool: + """Whether a StackOverflowError reached the target's code in the execution of the trace.""" + endpoint_id = str(endpoint_id) + lock.acquire() + ret = trace_id in self.tree[endpoint_id].stack_overflow_traces + lock.release() + return ret + def record_expected_divergence(self, endpoint_id: Union[str, int]): endpoint_id = str(endpoint_id) lock.acquire() diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..c412e96e 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -165,7 +165,12 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac """Determines the next step based on the execution status.""" if status == ExecutionStatus.SUCCESS: - + # A StackOverflowError reached the target in this execution: its outcome depends on the + # JVM's stack size, which the task does not fix, so a violation it shows is not reported. + # The trace carries context loss, so the search goes on but cannot end in SAFE. + stack_overflow = self.round_has_stack_overflow() + if stack_overflow: + output = self.drop_violations(output) for l in output: if "java.lang.AssertionError: [SWAT]" in l: # Internal assertion error in the DSE @@ -192,6 +197,11 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac if len(Database.instance().get_tree(ENDPOINT_ID).symbolic_vars) == 0: + if stack_overflow: + # The only execution there is overflowed the stack: its outcome is not a verdict + logger.info(f'[SVCOMP] No symbolic vars found, but the execution overflowed the stack') + self.state.verdict = Verdict.UNKNOWN + return Action.REPORTVERDICT # No symbolic vars found, safe to assume no violation logger.info(f'[SVCOMP] No symbolic vars found') self.state.verdict = Verdict.NO_SYMBOLIC_VARS @@ -208,6 +218,28 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac return Action.REPORTVERDICT + def is_violation_line(self, line: str) -> bool: + """Whether the executor output line reports a violation of the checked property.""" + if self.verification_category == VerificationCategory.VALID_ASSERT_PRP: + return "java.lang.AssertionError" in line and "java.lang.AssertionError: [SWAT]" not in line + if self.verification_category == VerificationCategory.NO_RUNTIME_EXCEPTION_PRP: + return "[SWAT] Uncaught top-level RuntimeException in symbolic execution" in line + return False + + def drop_violations(self, output: List[str]) -> List[str]: + """Removes the violation lines of an execution whose outcome is not a verdict.""" + violations = [l for l in output if self.is_violation_line(l)] + if violations: + logger.warning(f'[SVCOMP] Violation after a stack overflow, not reported: {violations[0].strip()}') + Database.instance().record_execution_error(ENDPOINT_ID, 'stack_overflow_violation', violations[0].strip()) + return [l for l in output if not self.is_violation_line(l)] + + def round_has_stack_overflow(self) -> bool: + """Whether the trace of this round (if one arrived) reports a stack overflow in the target.""" + witness_data = Database.instance().get_witness_data(ENDPOINT_ID) + return witness_data is not None and Database.instance().is_stack_overflow_trace( + ENDPOINT_ID, witness_data['trace_id']) + def log_output(self, output: List[str]): logger.info(f'[SVCOMP] Java Output Begin') for line in output: diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 68be5da1..4c6c9b1b 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -93,6 +93,9 @@ class ConstraintRequest(BaseModel): referenceSemanticChange: bool = False # An approximate model (a sampled Math function) was used: solutions from this trace are guesses. approximateModel: bool = False + # A StackOverflowError reached the target's code: the path depends on the JVM's stack size, so a + # violation of this execution is not a verdict (the executor also reports context loss). + stackOverflow: bool = False class CoverageRequest(BaseModel): diff --git a/symbolic-explorer/svcomp/TestcaseStats.py b/symbolic-explorer/svcomp/TestcaseStats.py index 6f129eaa..f76e7543 100644 --- a/symbolic-explorer/svcomp/TestcaseStats.py +++ b/symbolic-explorer/svcomp/TestcaseStats.py @@ -54,6 +54,7 @@ def build_testcase_stats(verdict, category, tree, symbolic_exec_iterations: int, 'symbolic_precision_loss': tree.symbolic_precision_loss, 'reference_semantic_change': tree.reference_semantic_change, 'uncaught_exceptions': tree.uncaught_exceptions, + 'stack_overflow_traces': len(tree.stack_overflow_traces), }, 'symbolic_vars': sorted(tree.symbolic_vars), 'missing_invocations': missing, diff --git a/symbolic-explorer/tests/test_stack_overflow.py b/symbolic-explorer/tests/test_stack_overflow.py new file mode 100644 index 00000000..377d8652 --- /dev/null +++ b/symbolic-explorer/tests/test_stack_overflow.py @@ -0,0 +1,93 @@ +""" +Unit tests for SVCompDriver.determine_next_step on executions whose trace reports a stack overflow +in the target: their outcome depends on the JVM's stack size, so a violation they show is not a +verdict, and an execution without symbolic inputs is not SAFE. + +It imports the driver, which needs the explorer's dependencies (z3, fastapi, ...) that the system +Python lacks, so run it with the harness venv, from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_stack_overflow -v +""" + +import os +import sys +import unittest +from types import SimpleNamespace +from unittest import mock + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from driver import SVCompDriver as svcomp + +ASSERTION = 'Exception in thread "main" java.lang.AssertionError' +RUNTIME_EXCEPTION = '[SWAT] Uncaught top-level RuntimeException in symbolic execution' + + +class StackOverflowRoundTest(unittest.TestCase): + + def setUp(self): + self.tree = SimpleNamespace(execution_errors=[], symbolic_vars={'I_0'}, uncaught_exceptions=0) + self.overflowed_traces = set() + def record_execution_error(endpoint_id, kind, message): + self.tree.execution_errors.append({'kind': kind, 'message': message}) + def record_uncaught_exception(endpoint_id): + self.tree.uncaught_exceptions += 1 + db = SimpleNamespace( + record_execution_error=record_execution_error, + record_uncaught_exception=record_uncaught_exception, + get_tree=lambda endpoint_id: self.tree, + get_witness_data=lambda endpoint_id: {'trace_id': 't1'}, + is_stack_overflow_trace=lambda endpoint_id, trace_id: trace_id in self.overflowed_traces) + patcher = mock.patch.object(svcomp.Database, 'instance', return_value=db) + patcher.start() + self.addCleanup(patcher.stop) + self.driver = svcomp.SVCompDriver.__new__(svcomp.SVCompDriver) + self.driver.state = svcomp.State() + + def step(self, category, output): + self.driver.verification_category = category + return self.driver.determine_next_step(svcomp.ExecutionStatus.SUCCESS, output) + + def test_assertion_without_stack_overflow_is_a_violation(self): + action = self.step(svcomp.VerificationCategory.VALID_ASSERT_PRP, [ASSERTION]) + self.assertEqual(action, svcomp.Action.REPORTVERDICT) + self.assertEqual(self.driver.state.verdict, svcomp.Verdict.VIOLATION) + + def test_assertion_after_stack_overflow_is_not_reported(self): + self.overflowed_traces.add('t1') + action = self.step(svcomp.VerificationCategory.VALID_ASSERT_PRP, [ASSERTION]) + self.assertEqual(action, svcomp.Action.SYMBOLICNEXT) + self.assertNotEqual(self.driver.state.verdict, svcomp.Verdict.VIOLATION) + self.assertEqual([e['kind'] for e in self.tree.execution_errors], ['stack_overflow_violation']) + + def test_runtime_exception_after_stack_overflow_is_not_reported(self): + self.overflowed_traces.add('t1') + action = self.step(svcomp.VerificationCategory.NO_RUNTIME_EXCEPTION_PRP, [RUNTIME_EXCEPTION]) + self.assertEqual(action, svcomp.Action.SYMBOLICNEXT) + self.assertNotEqual(self.driver.state.verdict, svcomp.Verdict.VIOLATION) + + def test_swat_exception_still_ends_the_run(self): + self.overflowed_traces.add('t1') + action = self.step(svcomp.VerificationCategory.VALID_ASSERT_PRP, [ASSERTION, '[SWAT Exception]: boom']) + self.assertEqual(action, svcomp.Action.REPORTVERDICT) + self.assertEqual(self.driver.state.verdict, svcomp.Verdict.UNKNOWN) + + def test_overflow_of_another_round_does_not_count(self): + self.overflowed_traces.add('t0') + self.step(svcomp.VerificationCategory.VALID_ASSERT_PRP, [ASSERTION]) + self.assertEqual(self.driver.state.verdict, svcomp.Verdict.VIOLATION) + + def test_no_symbolic_vars_after_stack_overflow_is_unknown(self): + self.overflowed_traces.add('t1') + self.tree.symbolic_vars = set() + action = self.step(svcomp.VerificationCategory.NO_RUNTIME_EXCEPTION_PRP, []) + self.assertEqual(action, svcomp.Action.REPORTVERDICT) + self.assertEqual(self.driver.state.verdict, svcomp.Verdict.UNKNOWN) + + def test_no_symbolic_vars_without_stack_overflow_is_safe(self): + self.tree.symbolic_vars = set() + self.step(svcomp.VerificationCategory.NO_RUNTIME_EXCEPTION_PRP, []) + self.assertEqual(self.driver.state.verdict, svcomp.Verdict.NO_SYMBOLIC_VARS) + + +if __name__ == '__main__': + unittest.main()