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 ""; + } +} 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()