From e9ae9b0ca76a480047cf3cbaa8c546dff9db7dc0 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 20:58:11 +0000 Subject: [PATCH 01/10] Make the class name check descriptor-aware Util.checkClassName rejected every name starting with 'L' as a type descriptor, with an allowlist for two benign names. Class names such as LinkedListEntry still failed. A reference descriptor always ends in ';', which the check already rejects, so the leading-'L' clause and the allowlist are dropped. Co-Authored-By: Claude Opus 5.5 --- .../main/java/de/uzl/its/swat/common/Util.java | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java index 2247fb86..a68e76bd 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/Util.java @@ -233,19 +233,18 @@ public static Class[] getInterfaces(Class clazz) return interfaces; } - private static final List allowlistedClassNames = List.of("LinkedList", "LogOutput"); // Benign names beginning with 'L' - + /** + * Asserts that a class name is not a type descriptor. A reference descriptor has the form + * {@code Lpkg/Name;}, so the trailing ';' identifies it; a leading 'L' alone does not, as + * class names such as {@code LinkedList} or {@code LinkedListEntry} start with it too. + */ private static void checkClassName(String className) { if (className.startsWith("[")) { return; // array class, skip check for now } - if (allowlistedClassNames.contains(className)) { - return; - } SWATAssert.check( - !className.contains(";") && !className.contains("(") && !className.contains(")") - && !className.startsWith("L"), - "Class name '{}' should not contain ';', '(', ')', or start with 'L'", className); + !className.contains(";") && !className.contains("(") && !className.contains(")"), + "Class name '{}' should not be a descriptor (contains ';', '(' or ')')", className); } /** From eaeb2d922a6bb3095871ec7672304bafd8a7b0f3 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:12:56 +0000 Subject: [PATCH 02/10] Continue the running symbolic execution in nested endpoints Every method named main is an endpoint in SV_COMP mode, so a harness whose Main.main calls another main (e.g. harness.Environment.main) ran Intrinsics.init twice on the same thread and halted with DuplicateThreadContextException. An endpoint entered while the thread's context exists now only increments a nesting count, and its terminate call decrements it; the outermost endpoint still ends the execution. Co-Authored-By: Claude Opus 5.5 --- .../uzl/its/swat/instrument/Intrinsics.java | 11 +++++++ .../de/uzl/its/swat/thread/ThreadContext.java | 4 +++ .../de/uzl/its/swat/thread/ThreadHandler.java | 29 +++++++++++++++++++ 3 files changed, 44 insertions(+) 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 f280c9ba..cecd99ec 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 @@ -66,6 +66,13 @@ public static void unsupported() { */ public static void init(String endpoint) { try { + if (ThreadHandler.hasThreadContext(currentThread().getId())) { + // An endpoint called from within a running one (e.g. a harness main calling + // another main) continues the running symbolic execution. + ThreadHandler.enterNestedEndpoint(currentThread().getId()); + logger.info("Entering nested endpoint {} (Thread: {})", endpoint, currentThread().getId()); + return; + } int endpointID; if (config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) { endpointID = 0; @@ -108,6 +115,10 @@ public static void init(String endpoint) { */ public static void terminate() { try { + if (ThreadHandler.leaveNestedEndpoint(currentThread().getId())) { + logger.info("Leaving nested endpoint (Thread: {})", currentThread().getId()); + return; + } Transformer.logMissedClasses(); ThreadHandler.disableThreadContext(currentThread().getId()); logger.info( 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 38c571d8..dbe63319 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 @@ -65,6 +65,10 @@ public class ThreadContext { @Setter @Getter private int endpointID; @Setter @Getter private String endpointName; + // Number of endpoints entered while this context was already running, e.g. a harness main + // that calls another main. Their init/terminate calls only adjust this count. + @Getter @Setter private int nestedEndpoints = 0; + // Tracks if liftValue is called multiple times with the same index. @Getter private final HashMap symbolicIdxOccurrence = new java.util.HashMap<>(); private HashMap SubUid = new HashMap<>(); 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 b83a3e8d..30f6f743 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 @@ -80,6 +80,35 @@ public static void addThreadContext(long id, String endpointName, int endpointId } } + /** + * Records that an endpoint was entered on a thread whose symbolic execution is already running. + * + * @param id the thread id + */ + public static void enterNestedEndpoint(long id) throws NoThreadContextException { + ThreadContext context = threadContextHashMap.get(id); + if (context != null) { + context.setNestedEndpoints(context.getNestedEndpoints() + 1); + } else { + throw new NoThreadContextException(id); + } + } + + /** + * Leaves a nested endpoint if one is open. + * + * @param id the thread id + * @return true if a nested endpoint was left, false if the outermost endpoint ends + */ + public static boolean leaveNestedEndpoint(long id) { + ThreadContext context = threadContextHashMap.get(id); + if (context != null && context.getNestedEndpoints() > 0) { + context.setNestedEndpoints(context.getNestedEndpoints() - 1); + return true; + } + return false; + } + public static void removeThreadContext(long id) throws NoThreadContextException { ThreadContext context = threadContextHashMap.get(id); if (context != null) { From b09b432a3f3518b75db0b9c9f7bd96c7b313dc29 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:15:08 +0000 Subject: [PATCH 03/10] Start the symbolic execution in the entry class's static initializer The JVM initialises the entry class before it calls main, so a Verifier.nondet* call in Main. (e.g. a static field initialiser) ran before Intrinsics.init had created the thread context and halted with NoThreadContextException. In SV_COMP mode the static initializer of a class declaring static main(String[]) now calls Intrinsics.initBeforeEntry, which starts the execution if none is running; main's init then continues it and clears the initializer's locals from the initial frame. Co-Authored-By: Claude Opus 5.5 --- .../uzl/its/swat/instrument/Intrinsics.java | 98 +++++++++++++------ .../StaticInitializerEntryMethodAdapter.java | 41 ++++++++ .../SymbolicWrapperClassAdapter.java | 40 +++++++- .../SymbolicWrapperTransformer.java | 6 +- .../uzl/its/swat/symbolic/shadow/Frame.java | 5 + .../de/uzl/its/swat/thread/ThreadContext.java | 4 + .../de/uzl/its/swat/thread/ThreadHandler.java | 29 ++++++ 7 files changed, 190 insertions(+), 33 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/StaticInitializerEntryMethodAdapter.java 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 cecd99ec..9310f272 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 @@ -66,48 +66,84 @@ public static void unsupported() { */ public static void init(String endpoint) { try { - if (ThreadHandler.hasThreadContext(currentThread().getId())) { + long threadId = currentThread().getId(); + if (ThreadHandler.hasThreadContext(threadId)) { + if (ThreadHandler.enterStartedEndpoint(threadId)) { + // The entry class's static initializer started the execution (initBeforeEntry). + // Its locals live in the initial frame that the endpoint now runs in. + ThreadHandler.getSymbolicVisitor(threadId).getStack().getActiveFrame().clearLocals(); + logger.info("Entering endpoint {} started by its static initializer (Thread: {})", + endpoint, threadId); + return; + } // An endpoint called from within a running one (e.g. a harness main calling // another main) continues the running symbolic execution. - ThreadHandler.enterNestedEndpoint(currentThread().getId()); - logger.info("Entering nested endpoint {} (Thread: {})", endpoint, currentThread().getId()); + ThreadHandler.enterNestedEndpoint(threadId); + logger.info("Entering nested endpoint {} (Thread: {})", endpoint, threadId); return; } - int endpointID; - if (config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) { - endpointID = 0; - } else { - endpointID = endpoint.hashCode(); - } - ThreadHandler.addThreadContext(currentThread().getId(), endpoint, endpointID); + startExecution(endpoint); + } catch (Throwable t) { + // The ErrorHandler has to be here as this method transfers control to the target domain + new ErrorHandler().handleException("Error during initialization of symbolic engine: ", t); + } + } - logger.info( - new PrintBox( - 60, - "Symbolic execution started (Thread: " - + Thread.currentThread().getId() - + ")", - new ArrayList<>( - List.of( - new String[]{ - "Execution started (Thread: " - + Thread.currentThread().getId() - + ")", - "Threads (tracked / active): (" - + ThreadHandler.getThreadCount() - + " / " - + Thread.activeCount() - + ")", - "Method: " + endpoint, - "ID: " + endpointID - }))) - .toString()); + /** + * Starts symbolic tracking in the static initializer of the entry class, which the JVM runs + * before the entry method, so that inputs read there (e.g. a static field initialised with a + * Verifier.nondet* call) are tracked. The entry method's init call then continues this + * execution. Does nothing if the thread's execution is already running. The method call is + * added during instrumentation. + * + * @param endpoint The name of the endpoint whose class is being initialised. + */ + public static void initBeforeEntry(String endpoint) { + try { + long threadId = currentThread().getId(); + if (ThreadHandler.hasThreadContext(threadId)) { + return; + } + startExecution(endpoint); + ThreadHandler.setStartedBeforeEndpoint(threadId); } catch (Throwable t) { // The ErrorHandler has to be here as this method transfers control to the target domain new ErrorHandler().handleException("Error during initialization of symbolic engine: ", t); } } + private static void startExecution(String endpoint) throws Exception { + int endpointID; + if (config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) { + endpointID = 0; + } else { + endpointID = endpoint.hashCode(); + } + ThreadHandler.addThreadContext(currentThread().getId(), endpoint, endpointID); + + logger.info( + new PrintBox( + 60, + "Symbolic execution started (Thread: " + + Thread.currentThread().getId() + + ")", + new ArrayList<>( + List.of( + new String[]{ + "Execution started (Thread: " + + Thread.currentThread().getId() + + ")", + "Threads (tracked / active): (" + + ThreadHandler.getThreadCount() + + " / " + + Thread.activeCount() + + ")", + "Method: " + endpoint, + "ID: " + endpointID + }))) + .toString()); + } + /** * Finishes symbolic tracking and initializes constrain transfer to coordinator. Method call diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/StaticInitializerEntryMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/StaticInitializerEntryMethodAdapter.java new file mode 100644 index 00000000..a9d237ee --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/StaticInitializerEntryMethodAdapter.java @@ -0,0 +1,41 @@ +package de.uzl.its.swat.instrument.symbolicwrapper; + +import de.uzl.its.swat.instrument.Intrinsics; +import org.objectweb.asm.MethodVisitor; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; + +/** + * Starts the symbolic execution at the beginning of the static initializer of a class that + * declares the entry method. The JVM initialises that class before it calls the entry method, so + * without this, inputs read by the initializer would run without a thread context. + */ +public class StaticInitializerEntryMethodAdapter extends MethodVisitor { + + private final String endpointID; + + /** + * @param mv Parent MethodVisitor + * @param endpointID The name of the endpoint whose class is initialised, as passed to + * Intrinsics.init by the endpoint itself + */ + public StaticInitializerEntryMethodAdapter(MethodVisitor mv, String endpointID) { + super(Opcodes.ASM9, mv); + this.endpointID = endpointID; + } + + @Override + public void visitCode() { + super.visitCode(); + SymbolicWrapperTransformer.getPrintBox() + .addMsg(" => Adding initializer: Intrinsics.initBeforeEntry(endpointID)"); + SymbolicWrapperTransformer.getPrintBox().setContentPresent(true); + visitLdcInsn(endpointID); + visitMethodInsn( + Opcodes.INVOKESTATIC, + Type.getInternalName(Intrinsics.class), + "initBeforeEntry", + "(Ljava/lang/String;)V", + false); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperClassAdapter.java index 2540fbd4..61bebd14 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperClassAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperClassAdapter.java @@ -5,6 +5,7 @@ import de.uzl.its.swat.config.Config; import de.uzl.its.swat.instrument.springendpoint.SpringEndpointTransformer; import java.util.regex.Pattern; +import org.objectweb.asm.ClassReader; import org.objectweb.asm.ClassVisitor; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -18,16 +19,48 @@ */ public class SymbolicWrapperClassAdapter extends ClassVisitor { + static final String ENTRY_METHOD_NAME = "main"; + static final String ENTRY_METHOD_DESC = "([Ljava/lang/String;)V"; + private String cname; private final Config config = Config.instance(); + private final boolean declaresEntryMethod; + /** * Constructor that calls the super from the default ClassVisitor * * @param cv Parent ClassVisitor + * @param declaresEntryMethod whether the class declares a static main(String[]) method */ - public SymbolicWrapperClassAdapter(ClassVisitor cv, String cname) { + public SymbolicWrapperClassAdapter(ClassVisitor cv, String cname, boolean declaresEntryMethod) { super(Opcodes.ASM9, cv); this.cname = cname; + this.declaresEntryMethod = declaresEntryMethod; + } + + /** + * Checks whether a class declares a static main(String[]) method. + * + * @param cr The reader of the class + * @return true if the class declares the method + */ + public static boolean declaresEntryMethod(ClassReader cr) { + boolean[] found = {false}; + cr.accept( + new ClassVisitor(Opcodes.ASM9) { + @Override + public MethodVisitor visitMethod( + int access, String name, String desc, String signature, String[] exceptions) { + if ((access & Opcodes.ACC_STATIC) != 0 + && name.equals(ENTRY_METHOD_NAME) + && desc.equals(ENTRY_METHOD_DESC)) { + found[0] = true; + } + return null; + } + }, + ClassReader.SKIP_CODE | ClassReader.SKIP_DEBUG | ClassReader.SKIP_FRAMES); + return found[0]; } /** @@ -62,6 +95,11 @@ public MethodVisitor visitMethod( if (mv != null) { switch (config.getInstrumentationTransformer()) { case SV_COMP -> { + if (name.equals("") && declaresEntryMethod) { + SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name); + return new StaticInitializerEntryMethodAdapter( + mv, cname + "/" + ENTRY_METHOD_NAME + ENTRY_METHOD_DESC); + } if (!name.equals("main")) { return mv; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperTransformer.java index 05eeed58..e40ae9b7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperTransformer.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperTransformer.java @@ -10,6 +10,7 @@ import de.uzl.its.swat.instrument.InternalTransformerType; import de.uzl.its.swat.instrument.SafeClassWriter; import de.uzl.its.swat.instrument.Transformer; +import de.uzl.its.swat.instrument.TransformerType; import de.uzl.its.swat.instrument.springendpoint.SpringEndpointTransformer; import java.io.PrintWriter; import java.io.StringWriter; @@ -99,7 +100,10 @@ public byte[] transform( getPrintBox().addMsg("Class: " + cname); ClassReader cr = new ClassReader(cbuf); ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES); - ClassVisitor cv = new SymbolicWrapperClassAdapter(cw, cname); + boolean declaresEntryMethod = + config.getInstrumentationTransformer() == TransformerType.SV_COMP + && SymbolicWrapperClassAdapter.declaresEntryMethod(cr); + ClassVisitor cv = new SymbolicWrapperClassAdapter(cw, cname, declaresEntryMethod); cr.accept(cv, 0); if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java index ed10cad6..07aeab6c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java @@ -123,6 +123,11 @@ public void setLocal(int index, Value o) { locals.set(index, o); } + /** Removes all symbolic locals */ + public void clearLocals() { + locals.clear(); + } + /** * Gets a Value from the symbolic locals * 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 dbe63319..39911e70 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 @@ -69,6 +69,10 @@ public class ThreadContext { // that calls another main. Their init/terminate calls only adjust this count. @Getter @Setter private int nestedEndpoints = 0; + // Set while the execution was started by the entry class's static initializer and the + // endpoint itself has not been entered yet. + @Getter @Setter private boolean startedBeforeEndpoint = false; + // Tracks if liftValue is called multiple times with the same index. @Getter private final HashMap symbolicIdxOccurrence = new java.util.HashMap<>(); private HashMap SubUid = new HashMap<>(); 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 30f6f743..cd3c38b4 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 @@ -80,6 +80,35 @@ public static void addThreadContext(long id, String endpointName, int endpointId } } + /** + * Marks the thread's execution as started before its endpoint was entered. + * + * @param id the thread id + */ + public static void setStartedBeforeEndpoint(long id) throws NoThreadContextException { + ThreadContext context = threadContextHashMap.get(id); + if (context != null) { + context.setStartedBeforeEndpoint(true); + } else { + throw new NoThreadContextException(id); + } + } + + /** + * Enters the endpoint of an execution that was started before it. + * + * @param id the thread id + * @return true if the execution was waiting for its endpoint, false otherwise + */ + public static boolean enterStartedEndpoint(long id) { + ThreadContext context = threadContextHashMap.get(id); + if (context != null && context.isStartedBeforeEndpoint()) { + context.setStartedBeforeEndpoint(false); + return true; + } + return false; + } + /** * Records that an endpoint was entered on a thread whose symbolic execution is already running. * From ccd0536ea12531efa83530bcb85fc3107ab80949 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:19:49 +0000 Subject: [PATCH 04/10] Stop growing ClassDepot's cached hierarchy lists on every allocation ValueFactory.createObjectValue appended the parents of a class to the interface list ClassDepot returned, which is the cached list itself, so every NEW grew it and the type checks after it scanned an ever longer list (quadratic on allocation-heavy loops), and an unregistered class would hit Collections.emptyList().addAll. ClassDepot now hands out unmodifiable views and ValueFactory merges into a copy. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/metadata/ClassDepot.java | 8 +++-- .../its/swat/symbolic/value/ValueFactory.java | 2 +- .../metadata/ClassDepotTypeInfoSpec.groovy | 29 +++++++++++++++++++ 3 files changed, 36 insertions(+), 3 deletions(-) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/metadata/ClassDepotTypeInfoSpec.groovy diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java index ee0bee37..07708f1d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java @@ -82,12 +82,16 @@ public synchronized void registerTypeInfoForClass(String className, List classToInterfaces.put(normalized, interfaces); } + /** Returns the registered parents of a class; the list is shared and must not be modified. */ public synchronized List getParentsForClass(String className) { - return classToParents.getOrDefault(Util.formatClassName(className), Collections.emptyList()); + return Collections.unmodifiableList( + classToParents.getOrDefault(Util.formatClassName(className), Collections.emptyList())); } + /** Returns the registered interfaces of a class; the list is shared and must not be modified. */ public synchronized List getInterfacesForClass(String className) { - return classToInterfaces.getOrDefault(Util.formatClassName(className), Collections.emptyList()); + return Collections.unmodifiableList( + classToInterfaces.getOrDefault(Util.formatClassName(className), Collections.emptyList())); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java index fe32e31c..dac05c37 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java @@ -163,7 +163,7 @@ public static StringValue createStringValue(String concrete, int address) throws public static ObjectValue createObjectValue(int nFields, String className) throws NoThreadContextException, NotImplementedException, TypeException, ValueConversionException { SolverContext context = ThreadHandler.getSolverContext(Thread.currentThread().getId()); List classInterfacesAndParents = - ClassDepot.getRuntimeInstance().getInterfacesForClass(className); + new ArrayList<>(ClassDepot.getRuntimeInstance().getInterfacesForClass(className)); classInterfacesAndParents.addAll( ClassDepot.getRuntimeInstance().getParentsForClass(className)); diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/metadata/ClassDepotTypeInfoSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/metadata/ClassDepotTypeInfoSpec.groovy new file mode 100644 index 00000000..ccca79f0 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/metadata/ClassDepotTypeInfoSpec.groovy @@ -0,0 +1,29 @@ +package de.uzl.its.swat.metadata + +import spock.lang.Specification + +/** + * L0: the registered type metadata of a class is shared, so the lists ClassDepot hands out must + * not grow when callers merge them (as ValueFactory.createObjectValue does on every NEW). + */ +class ClassDepotTypeInfoSpec extends Specification { + + def "the parent and interface lists of a class cannot be modified through the getters"() { + given: + def depot = ClassDepot.getInstrumentationInstance() + depot.registerTypeInfoForClass("spec/TypeInfoA", ["java/lang/Object"], ["java/lang/Runnable"]) + + when: + depot.getInterfacesForClass("spec/TypeInfoA").addAll(depot.getParentsForClass("spec/TypeInfoA")) + + then: + thrown(UnsupportedOperationException) + depot.getInterfacesForClass("spec/TypeInfoA") == ["java/lang/Runnable"] + } + + def "an unregistered class has empty lists"() { + expect: + ClassDepot.getRuntimeInstance().getParentsForClass("spec/TypeInfoUnknown").isEmpty() + ClassDepot.getRuntimeInstance().getInterfacesForClass("spec/TypeInfoUnknown").isEmpty() + } +} From 16245418781d83f684fe365449fe7fe2f44a0db7 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:20:38 +0000 Subject: [PATCH 05/10] Look up the reflected field by its name in Field.get visitGET_FIELD_REFLECTION resolved the instance field by the invoked method's name ("get") instead of the reflected field name, so the class template gained an unknown field and ObjectValue.getField read past the object's fields array. Use reflectFieldName as the setter path does, and box the value of a primitive field for Field.get. Co-Authored-By: Claude Opus 5.5 --- .../uzl/its/swat/symbolic/SymbolicInstructionVisitor.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 771f7759..2a2b9fb4 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -3281,9 +3281,15 @@ public void visitGET_FIELD_REFLECTION(GET_FIELD_REFLECTION inst) throws Symbolic } else { ObjectValue targetObject = (ObjectValue) stack.getLocal(1); - int fieldIndex = classDepot.getFieldIndex(cIdx, inst.name, false); + int fieldIndex = classDepot.getFieldIndex(cIdx, reflectFieldName, false); getObject = targetObject.getField(fieldIndex); } + if (inst.name.equals("get") + && !(getObject instanceof ObjectValue) + && !(getObject instanceof PlaceHolder)) { + // Field.get boxes the value of a primitive field + getObject = getObject.asObjectValue(); + } // if (getObject instanceof DoubleValue || getObject instanceof LongValue) { // stack.pushWideOperand(getObject); // } else { From 81f8042c1c298d05531b51dd4dec3e8cc9d32812 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:22:20 +0000 Subject: [PATCH 06/10] Store String[] rows created by ANEWARRAY into multi-dimensional arrays AASTORE into a MULTIANEWARRAY's ArrayArrayValue only accepted AbstractArrayValue rows, but ANEWARRAY creates ObjectArrayValues, so array[0] = new String[]{...} was dropped and later loads returned the stale row. For String[][] the row is now copied into a StringArrayValue and stored; since writes through other references to the row do not reach the copy, the store records a context loss. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 2a2b9fb4..e6917b1e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -275,6 +275,23 @@ public void visitAASTORE(AASTORE inst) throws SymbolicInstructionException { } else { enforceException(); } + } else if (ref instanceof ArrayArrayValue arr + && val instanceof ObjectArrayValue row + && "[[Ljava/lang/String;".equals(arr.desc)) { + // A String[] row created by ANEWARRAY stored into a MULTIANEWARRAY: the + // multi-dimensional array holds its rows as StringArrayValues, so it stores a copy. + // Writes through other references to the row do not reach the copy. + StringArrayValue copy = toStringArrayValue(row); + if (copy == null) { + recordUntrackedBoundsCheck(inst, idx, ref); + logger.warn("[AASTORE]: Unsupported row {} for multi-dimensional array", row); + } else if (checkArrayBounds(arr, idx, inst.iid)) { + arr.storeElement(idx, copy); + logger.warn("[AASTORE]: Storing a copy of row {} in a multi-dimensional array causes context loss", row); + symbolicTraceHandler.recordSymbolicContextLoss(); + } else { + enforceException(); + } } else if (ref instanceof StringArrayValue arr) { boolean result = checkArrayBounds(arr, idx, inst.iid); if (result) { @@ -291,6 +308,24 @@ public void visitAASTORE(AASTORE inst) throws SymbolicInstructionException { } } + /** + * Copies a String[] row into a StringArrayValue. + * + * @param row The row + * @return The copy, or null if an element is not a String value (e.g. null) + */ + private StringArrayValue toStringArrayValue(ObjectArrayValue row) throws NoThreadContextException { + SolverContext context = ThreadHandler.getSolverContext(currentThread().getId()); + StringArrayValue copy = new StringArrayValue(context, row.size, row.getAddress()); + for (int i = 0; i < row.size.concrete; i++) { + if (!(row.getField(i) instanceof StringValue element)) { + return null; + } + copy.storeElement(new IntValue(context, i), element); + } + return copy; + } + /** * Pushes NULL onto the symbolic stack * From 30be08faefed417586e6b3da060790bde6477050 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:25:05 +0000 Subject: [PATCH 07/10] Close constructor invokes left by an exception inside a constructor A constructor call inside a constructor (super(...), this(...) or a new in the body) is instrumented without a try/catch, because the handler could cover the uninitialized this, which the verifier rejects. An exception leaving such a call therefore emitted no INVOKEMETHOD_EXCEPTION, its invoke id stayed open, and the next exception event halted the executor with "Invocation stack is broken!". The processor now records these invokes from the probe the instrumentation places before them and, like abandoned static initializers, closes them and their frames when an invoke below them ends or throws. Co-Authored-By: Claude Opus 5.5 --- .../SymbolicInstructionProcessor.java | 50 ++++++++++++++----- 1 file changed, 37 insertions(+), 13 deletions(-) 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..735a6bff 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 @@ -41,6 +41,16 @@ public SymbolicInstructionProcessor() {} private final Stack openInvokeIds = new Stack<>(); /** The open invokes that are static initializers (CLINIT). */ private final Set clinitInvokeIds = new HashSet<>(); + /** + * The open invokes of a constructor called from within a constructor. The instrumentation + * cannot wrap them in a try/catch (the receiver may be the uninitialized this), so an exception + * leaving them emits no INVOKEMETHOD_EXCEPTION. + */ + private final Set unwrappedInitInvokeIds = new HashSet<>(); + /** Set by the probe the instrumentation places before such a constructor call. */ + private boolean nextInvokeIsUnwrappedInit = false; + /** The value of that probe (see InstructionMethodAdapter.visitMethodInsn). */ + private static final int UNWRAPPED_INIT_PROBE = 420; /** * Returns whether we're currently in a delegation context (non-instrumented → instrumented). @@ -439,7 +449,7 @@ private void recordUnknownSpaceContextLoss(long threadId, String expectedClassFu /** * Closes static initializers that an exception left, once an instruction of the frame below - * them runs. unwindAbandonedClinits only catches this when an invoke below ends; an + * them runs. unwindAbandonedInitializers only catches this when an invoke below ends; an * initializer triggered by a field access or {@code new} has none, and the next instruction * already belongs to the handler of the frame below. Without this, that handler would run as * untracked code inside the initializer's frame. @@ -474,25 +484,29 @@ private void closeClinitsLeftByException(ShadowContext stack, Instruction inst, } /** - * A static initializer left by an exception emits no INVOKECLINIT_END, so its invoke and its - * shadow frame stay open. When the end (or exception) of an invoke below it arrives, the - * initializer is certainly over: close it first, as the JVM did when it unwound it. + * A static initializer left by an exception emits no INVOKECLINIT_END, and a constructor + * called from within a constructor left by an exception emits no INVOKEMETHOD_EXCEPTION, so + * their invokes and shadow frames stay open. When the end (or exception) of an invoke below + * them arrives, they are certainly over: close them first, as the JVM did when it unwound them. */ - private void unwindAbandonedClinits(long invokeId, ShadowContext stack, Logger logger) { + private void unwindAbandonedInitializers(long invokeId, ShadowContext stack, Logger logger) { if (openInvokeIds.empty() || openInvokeIds.peek() == invokeId || !openInvokeIds.contains(invokeId)) { return; } List above = openInvokeIds.subList(openInvokeIds.lastIndexOf(invokeId) + 1, openInvokeIds.size()); - if (!clinitInvokeIds.containsAll(above)) { - return; // not only initializers: leave it to the consistency check below + for (long id : above) { + if (!clinitInvokeIds.contains(id) && !unwrappedInitInvokeIds.contains(id)) { + return; // not only initializers: leave it to the consistency check below + } } while (openInvokeIds.peek() != invokeId) { - long clinit = openInvokeIds.pop(); - clinitInvokeIds.remove(clinit); - if (stack.getActiveFrame().getMethodName().equals("")) { + long open = openInvokeIds.pop(); + String method = clinitInvokeIds.remove(open) ? "" : ""; + unwrappedInitInvokeIds.remove(open); + if (stack.getActiveFrame().getMethodName().equals(method)) { stack.popFrame(); } - logger.info("Closing static initializer (invoke {}) left by an exception", clinit); + logger.info("Closing initializer {} (invoke {}) left by an exception", method, open); } } @@ -514,20 +528,30 @@ private boolean handleInvokeStack(Instruction currentInstruction, ShadowContext || currentInstruction instanceof INVOKEMETHOD_EXCEPTION || currentInstruction instanceof INVOKECLINIT_END; + if (currentInstruction instanceof SPECIAL special && special.i == UNWRAPPED_INIT_PROBE) { + nextInvokeIsUnwrappedInit = !isInUnknownSpace; + } + if (!isInUnknownSpace && currentInstructionIsInvokeX) { openInvokeIds.push(((InvokeIdInstruction) currentInstruction).invokeId); if (currentInstruction instanceof CLINIT) { clinitInvokeIds.add(((InvokeIdInstruction) currentInstruction).invokeId); } + if (nextInvokeIsUnwrappedInit && currentInstruction instanceof INVOKESPECIAL) { + unwrappedInitInvokeIds.add(((InvokeIdInstruction) currentInstruction).invokeId); + } + } + if (currentInstructionIsInvokeX) { + nextInvokeIsUnwrappedInit = false; } if (currentInstructionIsMethodEndOrException) { - unwindAbandonedClinits(((InvokeIdInstruction) currentInstruction).invokeId, stack, logger); + unwindAbandonedInitializers(((InvokeIdInstruction) currentInstruction).invokeId, stack, logger); if (!openInvokeIds.empty() && openInvokeIds.peek() > 0 && openInvokeIds.peek() == ((InvokeIdInstruction) currentInstruction).invokeId) { - openInvokeIds.pop(); + unwrappedInitInvokeIds.remove(openInvokeIds.pop()); closeOpenInvoke = true; if (isInUnknownSpace) { logger.info("Leaving unknown space."); From 519c375de14d9a91eab6cdef413474bf3a293555 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:30:58 +0000 Subject: [PATCH 08/10] Resync a diverged primitive value with a context loss instead of halting visitGETVALUE_primitive asserted when the shadow value did not match the value the JVM produced, which halts the executor, so one model bug ended the whole run. It now continues with the concrete value and records a context loss, since what the trace derived from the diverged shadow value cannot be trusted: a SAFE becomes UNKNOWN, while violations found on later paths are still reported. Co-Authored-By: Claude Opus 5.5 --- .../uzl/its/swat/symbolic/SymbolicInstructionVisitor.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index e6917b1e..46df493e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -3842,9 +3842,12 @@ private void visitGETVALUE_primitive(GETVALUE_primitive inst, ValueType type) th } else if ((peek instanceof BoxedValue && !checkEquality(((BoxedValue) peek).getVal().concrete, inst.v)) || (!(peek instanceof BoxedValue) && !checkEquality(peek.concrete, inst.v))) { - SWATAssert.check(false, - "[GETVALUE_primitive]: Value on stack does not match expected value! Expected: {}, Actual: {}", + // The shadow value diverged from the JVM (a model bug). Continue with the concrete + // value: what the trace derived from the shadow value cannot be trusted, which is + // recorded as a context loss. + logger.warn("[GETVALUE_primitive]: Value on stack does not match expected value, causes context loss! Expected: {}, Actual: {}", inst.v, peek.concrete); + symbolicTraceHandler.recordSymbolicContextLoss(); if (cat2) { stack.popWideOperand(); stack.pushWideOperand(ValueFactory.createNumericalValue(type, inst.v)); From 3ee3cb4828427b039da3c1df59253bc927b04865 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:37:41 +0000 Subject: [PATCH 09/10] Convert floats and doubles to strings concretely Value.asStringValue threw NotImplementedException for DoubleValue and FloatValue, so StringBuilder.append(D/F) and String.valueOf(D/F) failed even for concrete values. They now return String.valueOf of the concrete value; there is no symbolic model of the conversion, so a symbolic value records a context loss. Co-Authored-By: Claude Opus 5.5 --- .../numeric/floatingpoint/DoubleValue.java | 27 ++++++++++++++++--- .../numeric/floatingpoint/FloatValue.java | 27 ++++++++++++++++--- .../floatingpoint/FloatValueTest.groovy | 16 +++++++++++ 3 files changed, 62 insertions(+), 8 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java index 0bacd823..12fd9fee 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java @@ -21,6 +21,11 @@ import de.uzl.its.swat.symbolic.value.reference.ObjectValue; import de.uzl.its.swat.symbolic.value.reference.lang.DoubleObjectValue; import lombok.Getter; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; + +import static java.lang.Thread.currentThread; /** * Wrapper for doubles to represent symbolic and concrete information on the symbolic stack @@ -441,10 +446,24 @@ public LongValue asLongValue() { return D2L(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * Converts this DoubleValue to its decimal string, as String.valueOf(double) does. There is no + * symbolic model of the conversion: the string is concrete, and a symbolic value records a + * context loss. + * + * @return The resulting StringValue + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("Cannot record the context loss of a double to string conversion", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public DoubleObjectValue asObjectValue(){ diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java index 2f14df0e..c4bc992e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java @@ -21,6 +21,11 @@ import de.uzl.its.swat.symbolic.value.reference.ObjectValue; import de.uzl.its.swat.symbolic.value.reference.lang.FloatObjectValue; import lombok.Getter; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; + +import static java.lang.Thread.currentThread; public class FloatValue extends NumericalValue { @Getter @@ -391,10 +396,24 @@ public DoubleValue asDoubleValue() { return F2D(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * Converts this FloatValue to its decimal string, as String.valueOf(float) does. There is no + * symbolic model of the conversion: the string is concrete, and a symbolic value records a + * context loss. + * + * @return The resulting StringValue + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("Cannot record the context loss of a float to string conversion", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public FloatObjectValue asObjectValue(){ diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy index 1081d342..4d5d5a1e 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/floatingpoint/FloatValueTest.groovy @@ -337,6 +337,22 @@ class FloatValueTest extends Specification { ].transpose().collect { (it[0] == Float.NaN || it[1] == Float.NaN) ? -1 : (it[0] == it[1] ? 0 : (it[0] > it[1] ? 1 : -1)) } } + def "asStringValue of a concrete float is String.valueOf"(float c1) { + expect: + new FloatValue(context, c1).asStringValue().concrete == String.valueOf(c1) + + where: + c1 << [0.0f, -0.0f, 1.5f, -7.01f, Float.NaN, Float.POSITIVE_INFINITY, Float.MIN_VALUE, 1.0e10f] + } + + def "asStringValue of a concrete double is String.valueOf"(double c1) { + expect: + new DoubleValue(context, c1).asStringValue().concrete == String.valueOf(c1) + + where: + c1 << [0.0d, -0.0d, 1.5d, -7.01d, Double.NaN, Double.NEGATIVE_INFINITY, Double.MIN_VALUE, 1.0e100d] + } + // ======================================================================== // Float Narrowing Conversions - Testing fpToIntFormula Fix // ======================================================================== From f6c0a513afee5ac98328ac77629eb992bbb49295 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:39:42 +0000 Subject: [PATCH 10/10] Add agent tests for entry-method start, nested mains and constructor exceptions Co-Authored-By: Claude Opus 5.5 --- .../its/swat/instrument/EntryAgentSpec.groovy | 104 ++++++++++++++++++ .../resources/targets/entry/clinit/Main.java | 12 ++ .../targets/entry/initexception/Main.java | 27 +++++ .../resources/targets/entry/nested/Main.java | 23 ++++ 4 files changed, 166 insertions(+) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/EntryAgentSpec.groovy create mode 100644 symbolic-executor/src/test/resources/targets/entry/clinit/Main.java create mode 100644 symbolic-executor/src/test/resources/targets/entry/initexception/Main.java create mode 100644 symbolic-executor/src/test/resources/targets/entry/nested/Main.java diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/EntryAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/EntryAgentSpec.groovy new file mode 100644 index 00000000..0d45e30e --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/instrument/EntryAgentSpec.groovy @@ -0,0 +1,104 @@ +package de.uzl.its.swat.instrument + +import com.fasterxml.jackson.databind.ObjectMapper +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): how the SV-COMP instrumentation starts and ends the symbolic execution of an + * entry method. Each target under {@code targets/entry/} is compiled with the SV-COMP + * Verifier stub and run with the agent in {@code solver.mode=PRINT}; the TraceDTO printed to + * stdout is checked. Runs via the {@code agentTest} Gradle task (needs the agent jar from + * {@code copyJar}). + */ +class EntryAgentSpec 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 TARGETS = Path.of("src", "test", "resources", "targets").toAbsolutePath() + + def "an input read by the entry class's static initializer is tracked"() { + when: + def output = run("clinit", ["-Dswat.input.I_0=7"]) + def trace = parseTrace(output) + + then: + !output.contains("NoThreadContextException") + trace.inputs*.name == ["I_0"] + !trace.trace.isEmpty() + trace.violation?.throwable == "java.lang.AssertionError" + } + + def "a main called from the entry method continues the running execution"() { + when: + def output = run("nested", ["-Dswat.input.I_0=2", "-Dswat.input.I_1=2"]) + def trace = parseTrace(output) + + then: + !output.contains("DuplicateThreadContextException") + traceCount(output) == 1 + trace.inputs*.name.toSet() == ["I_0", "I_1"].toSet() + trace.violation?.throwable == "java.lang.AssertionError" + } + + def "an exception leaving a super constructor does not break the invocation stack"() { + when: + def output = run("initexception", ["-Dswat.input.I_0=3"]) + def trace = parseTrace(output) + + then: + !output.contains("Invocation stack is broken") + trace.inputs*.name == ["I_0"] + trace.violation?.throwable == "java.lang.AssertionError" + } + + private static String run(String target, List inputs) { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + Path classes = Files.createTempDirectory("swat-entry-agent-spec") + try { + compile([TARGETS.resolve("entry").resolve(target), TARGETS.resolve("svcomp").resolve("org")], classes) + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false"] + inputs + + ["-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 + } finally { + classes.toFile().deleteDir() + } + } + + private static void compile(List sourceDirs, Path outDir) { + def sources = sourceDirs.collectMany { dir -> + Files.walk(dir).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 int traceCount(String out) { + return out.split("\n").count { it == "{" } + } + + /** 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/entry/clinit/Main.java b/symbolic-executor/src/test/resources/targets/entry/clinit/Main.java new file mode 100644 index 00000000..9b2d9868 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/entry/clinit/Main.java @@ -0,0 +1,12 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Agent test target: the input is read by the static initializer of the entry class. */ +public class Main { + static int x = Verifier.nondetInt(); + + public static void main(String[] args) { + if (x > 5) { + assert false : "clinit target"; + } + } +} diff --git a/symbolic-executor/src/test/resources/targets/entry/initexception/Main.java b/symbolic-executor/src/test/resources/targets/entry/initexception/Main.java new file mode 100644 index 00000000..c4966ca5 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/entry/initexception/Main.java @@ -0,0 +1,27 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Agent test target: an exception leaves a superclass constructor called by super(...). */ +public class Main { + public static void main(String[] args) { + int v = Verifier.nondetInt(); + try { + new Derived(v); + } catch (IllegalStateException e) { + assert false : "init target"; + } + } +} + +class Base { + Base(int v) { + if (v == 3) { + throw new IllegalStateException("bad"); + } + } +} + +class Derived extends Base { + Derived(int v) { + super(v); + } +} diff --git a/symbolic-executor/src/test/resources/targets/entry/nested/Main.java b/symbolic-executor/src/test/resources/targets/entry/nested/Main.java new file mode 100644 index 00000000..425e0bb5 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/entry/nested/Main.java @@ -0,0 +1,23 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Agent test target: the entry method calls another main method. */ +public class Main { + public static void main(String[] args) { + Harness.main(new String[] {"a"}); + int y = Verifier.nondetInt(); + if (y == 2) { + assert false : "nested target"; + } + } +} + +class Harness { + static int calls = 0; + + public static void main(String[] args) { + int z = Verifier.nondetInt(); + if (z > 1 && args.length == 1) { + calls++; + } + } +}