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); } /** 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..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,41 +66,84 @@ 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 @@ -108,6 +151,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/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/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/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 771f7759..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 @@ -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)); 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."); 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/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/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/main/java/de/uzl/its/swat/thread/ThreadContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java index 38c571d8..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 @@ -65,6 +65,14 @@ 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; + + // 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 b83a3e8d..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,64 @@ 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. + * + * @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) { 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/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() + } +} 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 // ======================================================================== 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++; + } + } +}