Fix small executor bugs: entry start in <clinit>, nested mains, constructor exceptions, reflection, multiarray rows, fp toString

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

symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java

@@ -66,48 +66,95 @@ public static void unsupported() {
      */
     public static void init(String endpoint) {
         try {
-            int endpointID;
-            if (config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) {
-                endpointID = 0;
-            } else {
-                endpointID = endpoint.hashCode();
+            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(threadId);
+                logger.info("Entering nested endpoint {} (Thread: {})", endpoint, threadId);
+                return;
             }
-            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
      * added during instrumentation.
      */
     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(

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

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("<clinit>") && declaresEntryMethod) {
+                        SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
+                        return new StaticInitializerEntryMethodAdapter(
+                                mv, cname + "/" + ENTRY_METHOD_NAME + ENTRY_METHOD_DESC);
+                    }
                     if (!name.equals("main")) {
                         return mv;
                     }

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)) {

symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java

@@ -82,12 +82,16 @@ public synchronized void registerTypeInfoForClass(String className, List<String>
         classToInterfaces.put(normalized, interfaces);
     }
 
+    /** Returns the registered parents of a class; the list is shared and must not be modified. */
     public synchronized List<String> 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<String> getInterfacesForClass(String className) {
-        return classToInterfaces.getOrDefault(Util.formatClassName(className), Collections.emptyList());
+        return Collections.unmodifiableList(
+                classToInterfaces.getOrDefault(Util.formatClassName(className), Collections.emptyList()));
     }
 
     /**

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
      *
@@ -3281,9 +3316,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 {
@@ -3801,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));