Handle StackOverflowError in the target as the plain JVM would

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());

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.
+ *
+ * <ul>
+ *   <li>{@link #trackingLost}: a StackOverflowError was raised inside SWAT. The shadow state may be
+ *       half updated, so symbolic tracking stops for the rest of the execution; the error is
+ *       swallowed, so the target continues as it would without SWAT.
+ *   <li>{@link #targetOverflowed}: a StackOverflowError reached the target's code. It is set by the
+ *       instrumented exception handler of every call site (a PUTSTATIC, no call) before the
+ *       exception is reported to SWAT. The path then depends on the stack size of the JVM, which
+ *       the task semantics do not fix, so neither a SAFE nor a VIOLATION found on it can be trusted.
+ * </ul>
+ *
+ * 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;
+    }
+}

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
 

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.
+     *
+     * <pre>targetOverflowed |= (throwable instanceof StackOverflowError)</pre>
+     */
+    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(

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;
     }
 
     /**

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 {

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<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, ArrayList<NondetReturnDTO> nondetReturns, ViolationDTO violation, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange, boolean approximateModel) {
+    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, ArrayList<NondetReturnDTO> 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<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayLis
         this.symbolicPrecisionLoss = symbolicPrecisionLoss;
         this.referenceSemanticChange = referenceSemanticChange;
         this.approximateModel = approximateModel;
+        this.stackOverflow = stackOverflow;
 
     }
 

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)
+    }
+}

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;
+    }
+}