();
+
@Getter private static PrintBox printBox;
- private static final org.slf4j.Logger logger = LoggerFactory.getLogger(Transformer.class);
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+ public static void addRequestBodyClass(String parameter) {
+ requestBodyClass.add(Util.formatClassName(parameter));
+ }
- public static void retransform(String cname) {
- cname = cname.substring(1);
+ public static boolean containsRequestBodyClass(String parameter) {
+ return requestBodyClass.contains(Util.formatClassName(parameter));
+ }
+
+ public static void retransform(String cname, boolean isRequestBodyClass) {
+ cname = Util.formatClassName(cname);
boolean loaded = isLoaded(cname);
+ if (isRequestBodyClass) {
+ addRequestBodyClass(cname);
+ }
if (loaded) {
try {
- Class> clazz = Class.forName(cname);
+ Class> clazz = Class.forName(cname.replace("/", "."));
instrumentation.retransformClasses(clazz);
+ } catch (UnmodifiableClassException e) {
+ logger.warn("Class " + cname + " is not retransformable.");
} catch (Throwable e) {
+ logger.warn("Error while retransforming class " + cname + ". Reason: " + e.getMessage());
e.printStackTrace();
}
}
@@ -49,7 +89,7 @@ public static void retransform(String cname) {
* @return true if the class has been instrumented
*/
public static boolean isInstrumented(String cname) {
- return instrumentedClasses.containsKey(cname);
+ return instrumentedClasses.containsKey(Util.formatClassName(cname));
}
/**
* Adds a class to the list of instrumented classes
@@ -58,6 +98,7 @@ public static boolean isInstrumented(String cname) {
* @param transformer the transformer that instrumented the class
*/
public static void addInstrumentedClass(String cname, InternalTransformerType transformer) {
+ cname = Util.formatClassName(cname);
if (instrumentedClasses.containsKey(cname)) {
instrumentedClasses.get(cname).add(transformer);
} else {
@@ -67,22 +108,42 @@ public static void addInstrumentedClass(String cname, InternalTransformerType tr
}
}
- /*
- * ToDo: Class.getName() expects package notation with dots '.'
- * rather than '/', imo this should be ensured by the caller
- */
public static boolean isLoaded(String cname) {
+ cname = Util.formatClassName(cname);
for (Class> clazz : instrumentation.getAllLoadedClasses()) {
- if (cname.equals(clazz.getName())) return true;
+ if (cname.replace("/", ".").equals(clazz.getName())) {
+ return true;
+ }
}
return false;
}
+ public static void logMissedClasses(){
+ // Retransform already loaded classes
+ for (Class> loadedClass : instrumentation.getAllLoadedClasses()) {
+ String cname = Util.formatClassName(loadedClass.getName());
+ if (instrumentation.isModifiableClass(loadedClass) && Util.shouldInstrument(cname) && !isInstrumented(cname)) {
+ logger.warn("YYY: Class {} is already loaded and not instrumented!", loadedClass.getName());
+ }
+
+ }
+ }
+
@SuppressWarnings("unused")
public static void premain(String agentArgs, Instrumentation inst) {
- ThreadHandler.init();
try {
+ ThreadHandler.init();
+ ThreadHandler.addThreadContext(-1, "SymbolicThread", -1); // Main thread used during initialization and instrumentation
+
+ if (config.getInstrumentationTransformer().equals(TransformerType.SV_COMP)) {
+ Verifier.retrieveInputs(); // ToDo only conditionally and at a petter place
+ } else if (config.getInstrumentationTransformer().equals(TransformerType.ANNOTATION)) {
+ Intrinsics.retrieveAssignments();
+ }
+
+
instrumentation = inst;
+ logMissedClasses();
if (config.getInstrumentationTransformer().equals(TransformerType.NONE)) {
logger.info(
new PrintBox(
@@ -101,20 +162,42 @@ public static void premain(String agentArgs, Instrumentation inst) {
printBox = new PrintBox(60, "Instrumentation Agent started!");
printBox.addMsg(
"Selected Instrumentation Type: " + config.getInstrumentationTransformer());
+ printBox.addMsg("Can Retransform Classes: " + instrumentation.isRetransformClassesSupported());
+ printBox.addMsg("Redefine Classes Supported: " + instrumentation.isRedefineClassesSupported());
printBox.addMsg("Working Directory: " + System.getProperty("user.dir"));
printBox.addMsg("");
+ inst.addTransformer(new ClassInfoTransformer());
+ inst.addTransformer(new NoCacheTransformer());
+ inst.addTransformer(new RefEqualityTransformer());
+
switch (config.getInstrumentationTransformer()) {
- case SPRING_ENDPOINT, WEB_SERVLET -> {
- new ErrorHandler()
- .handleException(
- new RuntimeException(
- "Spring and WebServlet Instrumentation is not supported"
- + " yet!"));
+ case WEB_SERVLET -> {
+ throw new NotImplementedException("WEB_SERVLET");
+ }
+ case SPRING_ENDPOINT -> {
+ inst.addTransformer(new SpringEndpointTransformer());
+ // inst.addTransformer(new SpringExceptionTransformer());
+ if (Config.instance().isUseDataEndpointAdapter()) {
+ inst.addTransformer(new SpringRepositoryTransformer());
+ }
+ inst.addTransformer(
+ new ClassVariablesTransformer(), false); // TODO retransform has to be enabled
+ }
+ case PARAMETER -> {
+ inst.addTransformer(new ParameterTransformer());
+ if (Config.instance().isUseDataEndpointAdapter()) {
+ inst.addTransformer(new SpringRepositoryTransformer());
+ }
+ inst.addTransformer(
+ new ClassVariablesTransformer(), false); // TODO retransform has to be enabled
+ }
+ case SV_COMP -> {
+ inst.addTransformer(new SVCompTransformer());
+ }
+ case ANNOTATION -> {
+ inst.addTransformer(new AnnotationTransformer());
}
- case PARAMETER -> inst.addTransformer(new ParameterTransformer());
-
- case SV_COMP -> inst.addTransformer(new SVCompTransformer());
}
// Add transformer that tracks all instructions
@@ -127,37 +210,9 @@ public static void premain(String agentArgs, Instrumentation inst) {
inst.addTransformer(new ClassSavingTransformer());
}
logger.info(printBox.toString());
- } catch (Exception e) {
- ErrorHandler errorHandler = new ErrorHandler();
- errorHandler.handleException("Error during Transformer initialization!", e);
- }
- }
-
- /**
- * Checks if a class should be instrumented. If the instrumentPackages are set, only classes in
- * these packages will be instrumented. If the excludePackages are set, classes in these
- * packages will not be instrumented.
- *
- * @param cname the name of the class
- * @return true if the class should be instrumented, false otherwise
- */
- public static boolean shouldInstrument(String cname) {
- // Special case for SV-Comp
- if (cname.equals("de/uzl/its/swat/instrument/svcomp/Verifier")
- && config.getInstrumentationTransformer().equals(TransformerType.SV_COMP))
- return true;
-
- boolean shouldInst = true;
- if (config.getInstrumentationIncludePackages() != null) {
- shouldInst = false;
- for (String p : config.getInstrumentationIncludePackages()) {
- shouldInst = shouldInst || cname.startsWith(p);
- }
- } else if (config.getInstrumentationExcludePackages() != null) {
- for (String p : config.getInstrumentationExcludePackages()) {
- shouldInst = shouldInst && !cname.startsWith(p);
- }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to ASM
+ new ErrorHandler().handleException(new InstrumentationException(t));
}
- return shouldInst;
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TransformerType.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TransformerType.java
index 436f9ca..82d2ea4 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TransformerType.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TransformerType.java
@@ -1,6 +1,7 @@
package de.uzl.its.swat.instrument;
public enum TransformerType {
+ ANNOTATION,
SPRING_ENDPOINT,
PARAMETER,
WEB_SERVLET,
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TryCatchBlock.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TryCatchBlock.java
index 6e45138..21a4daf 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TryCatchBlock.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/TryCatchBlock.java
@@ -3,21 +3,9 @@
import org.objectweb.asm.Label;
import org.objectweb.asm.MethodVisitor;
-/** Author: Koushik Sen (ksen@cs.berkeley.edu) Date: 7/1/12 Time: 10:50 PM */
-public class TryCatchBlock {
- Label label;
- Label label1;
- Label label2;
- String type;
-
- public TryCatchBlock(Label label, Label label1, Label label2, String type) {
- this.label = label;
- this.label1 = label1;
- this.label2 = label2;
- this.type = type;
- }
+public record TryCatchBlock(Label start, Label end, Label handler, Label jumpTarget, String type) {
public void visit(MethodVisitor mv) {
- mv.visitTryCatchBlock(label, label1, label2, type);
+ mv.visitTryCatchBlock(start, end, handler, type);
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Utils.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Utils.java
index 17394f3..df63c6b 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Utils.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Utils.java
@@ -1,12 +1,258 @@
package de.uzl.its.swat.instrument;
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
import de.uzl.its.swat.config.Config;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
import org.objectweb.asm.Type;
+import org.objectweb.asm.tree.*;
public class Utils implements Opcodes {
private static final Config config = Config.instance();
+ private static final GlobalStateForInstrumentation instrumentationState = GlobalStateForInstrumentation.instance;
+
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+ public static void print(String specifier, String val) {
+ System.out.println(specifier + ": " + val);
+ }
+
+
+ public static boolean isBoxedPrimitive(Type type) {
+ if(type.equals(Type.getType(Integer.class))) return true;
+ if(type.equals(Type.getType(Long.class))) return true;
+ if(type.equals(Type.getType(Short.class))) return true;
+ if(type.equals(Type.getType(Byte.class))) return true;
+ if(type.equals(Type.getType(Float.class))) return true;
+ if(type.equals(Type.getType(Double.class))) return true;
+ if(type.equals(Type.getType(Character.class))) return true;
+ if(type.equals(Type.getType(Boolean.class))) return true;
+ return false;
+ }
+
+ public static boolean isBoxedPrimitive(String desc){
+ SWATAssert.check(desc.startsWith("L") && desc.endsWith(";"), "Descriptor is not a valid object type: {}", desc);
+ return switch (desc) {
+ case "Ljava/lang/Integer;", "Ljava/lang/Boolean;", "Ljava/lang/Byte;", "Ljava/lang/Character;", "Ljava/lang/Short;", "Ljava/lang/Long;", "Ljava/lang/Float;", "Ljava/lang/Double;" -> true;
+ default -> false;
+ };
+ }
+
+ public static InsnList addUnsupportedCall(){
+ InsnList instrumentation = new InsnList();
+
+ instrumentation.add(new MethodInsnNode(Opcodes.INVOKESTATIC,
+ Type.getInternalName(Intrinsics.class),
+ "unsupported",
+ "()V",
+ false));
+
+ return instrumentation;
+ }
+
+ /**
+ * Injects code to lift a class parameter to symbolic, reintrumenting the class to turn its class variables to
+ * symbolic fields. The class instance is assumed to be on the top of the stack.
+ * @param cname the internal name of the class to lift
+ */
+ public static InsnList liftClass(String cname) {
+ // The class instance is assumed to be on the top of the stack.
+ // Stack: [ref]
+ if(cname.startsWith("L")) cname = cname.substring(1, cname.length() - 1); // Remove leading L and trailing ;
+ InsnList instrumentation = new InsnList();
+ if (Util.shouldInstrument(cname)) {
+ Transformer.retransform(cname, true);
+
+ instrumentation.add(new InsnNode(Opcodes.DUP));
+ // Stack: [ref, ref]
+
+ // Call the instrumented lifting method that calls the helper method that was added to the (data) cls
+ instrumentation.add(new LdcInsnNode(cname.replace("/", "."))); // This notation is needed here
+ instrumentation.add(new LdcInsnNode(config.getInstrumentationPrefix())); // This notation is needed here
+ instrumentation.add(new InsnNode(Opcodes.ACONST_NULL));
+ instrumentation.add(new MethodInsnNode(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/UtilInstrumented",
+ "liftClass", "(Ljava/lang/Object;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)V",
+ false));
+ // Stack: [ref]
+
+ } else {
+ //instrumentation.add(new InsnNode(Opcodes.POP));
+ logger.warn("Symbolic parameter with out of scope class: {}", cname);
+ }
+ // Stack: [ref]
+ return instrumentation;
+ }
+
+
+ /**
+ * Create a sequence of instructions to inject instrumentation code for lifting a concrete value to symbolic.
+ * Note: The value to be lifted is assumed to be on the top of the stack!
+ * The sequence of instructions is as follows:
+ *
+ * LDC uid
+ * INVOKESTATIC Intrinsics.injectAssignment(uid, value)
+ * LDC uid
+ * INVOKESTATIC Intrinsics.liftValue(uid, value)
+ *
+ * @param type The type of the value to be lifted.
+ * @return The sequence of instructions.
+ */
+ public static InsnList createLiftInstrumentation(Type type, boolean addAssignment, boolean prefixOnStack, String prefix) {
+ // Note: The value to be lifted (and the prefix) is assumed to be on the top of the stack!
+ // [val, (prefix)]
+ InsnList list = new InsnList();
+ long uid = Intrinsics.getNextUid();
+ String desc = String.format("(%sJ)%s", type.getDescriptor(), type.getDescriptor());
+
+ if(prefixOnStack) {
+ SWATAssert.check(prefix == null, "Prefix must be null if prefixOnStack is true");
+ SWATAssert.check(!addAssignment, "Cannot add assignment if prefix is on stack (not implemented)");
+ desc = String.format("(%sLjava/lang/String;J)%s", type.getDescriptor(), type.getDescriptor());
+ // [val, prefix]
+ } else{
+ if(addAssignment) {
+ SWATAssert.check(prefix == null, "Prefix must be null if addAssignment is true (not implemented)");
+ // [val]
+ // Add the unique identifier for the value to be lifted.
+ list.add(new LdcInsnNode(uid));
+ list.add(new MethodInsnNode(Opcodes.INVOKESTATIC,
+ Type.getInternalName(Intrinsics.class),
+ "injectAssignment",
+ desc,
+ false));
+ // [val]
+ }
+ if(prefix != null) {
+ // Add the prefix for the value to be lifted.
+ list.add(new LdcInsnNode(prefix));
+ desc = String.format("(%sLjava/lang/String;J)%s", type.getDescriptor(), type.getDescriptor());
+ // [val, prefix]
+ }
+ }
+ // Add the unique identifier for the value to be lifted.
+ list.add(new LdcInsnNode(uid));
+ // [val, (prefix), uid]
+
+ list.add(new MethodInsnNode(Opcodes.INVOKESTATIC,
+ Type.getInternalName(Intrinsics.class),
+ "liftValue",
+ desc,
+ false));
+ // [val]
+ return list;
+ }
+
+
+ /**
+ * Creates an instruction list that loads a local variable, and lifts it to the symbolic domain,
+ * while also checking if an assignment is available for the variable.
+ *
+ * @param localIndex the index of the local variable to instrument
+ * @param loadOpcode the opcode used to load the variable
+ * @param storeOpcode the opcode used to store the result
+ * @param type the type descriptor of the variable
+ * @return an {@code InsnList} containing the instrumentation instructions
+ */
+ public static InsnList liftLocalVariable(int localIndex, int loadOpcode, int storeOpcode, Type type, boolean addAssignment) {
+ InsnList list = new InsnList();
+ list.add(new VarInsnNode(loadOpcode, localIndex));
+ list.add(Utils.createLiftInstrumentation(type, addAssignment, false, null));
+ list.add(new VarInsnNode(storeOpcode, localIndex));
+ return list;
+ }
+
+ /**
+ * Creates an instruction list that iterates through a list
+ * and lifts each element individually to the symbolic domain.
+ * If localIndex is -1 the list is assumed to be on the stack.
+ *
+ * @param localIndex the index of the local variable to instrument
+ * @param addAssignment whether to add assignment tracking
+ * @param leaveOnStack whether to leave the list reference on the stack after instrumentation (true for field lifting, false for parameter initialization)
+ * @return an {@code InsnList} containing the instrumentation instructions
+ */
+ public static InsnList liftListVariable(int localIndex, boolean addAssignment, boolean leaveOnStack) {
+ // If the list is on top of the stack, set localIndex to -1
+ InsnList list = new InsnList();
+ String symPrefix = "List";
+
+ if(localIndex != -1) { // Load the list from local variable
+ list.add(new VarInsnNode(Opcodes.ALOAD, localIndex));
+ }
+ // Stack: [list]
+
+ // Check if list is null
+ LabelNode nullLabel = new LabelNode();
+ LabelNode endLabel = new LabelNode();
+ list.add(new InsnNode(Opcodes.DUP));
+ list.add(new JumpInsnNode(Opcodes.IFNULL, nullLabel));
+ // Stack: [list]
+
+ list.add(new InsnNode(Opcodes.DUP));
+ // Stack: [list, list]
+
+ // Get ListIterator: list.listIterator()
+ list.add(new MethodInsnNode(Opcodes.INVOKEINTERFACE, "java/util/List", "listIterator", "()Ljava/util/ListIterator;", true));
+ // Stack: [list, listIterator]
+
+ // Loop through ListIterator
+ LabelNode loopStart = new LabelNode();
+ LabelNode loopEnd = new LabelNode();
+
+ list.add(loopStart);
+
+ // Check if iterator has next: listIterator.hasNext()
+ list.add(new InsnNode(Opcodes.DUP));
+ list.add(new MethodInsnNode(Opcodes.INVOKEINTERFACE, "java/util/ListIterator", "hasNext", "()Z", true));
+ list.add(new JumpInsnNode(Opcodes.IFEQ, loopEnd));
+ // Stack: [list, listIterator]
+
+ // Get next element: listIterator.next()
+ list.add(new InsnNode(Opcodes.DUP));
+ list.add(new MethodInsnNode(Opcodes.INVOKEINTERFACE, "java/util/ListIterator", "next", "()Ljava/lang/Object;", true));
+ // Stack: [list, listIterator, element]
+
+ // Apply lift instrumentation to the element
+ Type elementType = Type.getType(Object.class);
+ list.add(Utils.createLiftInstrumentation(elementType, addAssignment, false, symPrefix));
+ // Stack: [list, listIterator, liftedElement]
+
+ // Since we track by address, no need to put the element back - just pop the lifted element
+ list.add(new InsnNode(Opcodes.POP));
+ // Stack: [list, listIterator]
+
+ // Jump back to loop start
+ list.add(new JumpInsnNode(Opcodes.GOTO, loopStart));
+
+ // Loop end - pop the listIterator and jump to end
+ list.add(loopEnd);
+ // Stack: [list, listIterator]
+ list.add(new InsnNode(Opcodes.POP));
+ // Stack: [list]
+ list.add(new JumpInsnNode(Opcodes.GOTO, endLabel));
+
+ list.add(nullLabel);
+ // Stack: [list]
+
+ // End label
+ list.add(endLabel);
+ // Stack: [list]
+
+ if (!leaveOnStack) {
+ // For parameter initialization: pop the list to leave empty stack
+ list.add(new InsnNode(Opcodes.POP));
+ // Stack: []
+ }
+ // Stack: [list] if leaveOnStack, [] otherwise
+
+ return list;
+ }
+
+ public static boolean isStatic(int access) {
+ return (access & Opcodes.ACC_STATIC) != 0;
+ }
public static void addBipushInsn(MethodVisitor mv, int val) {
switch (val) {
@@ -20,10 +266,16 @@ public static void addBipushInsn(MethodVisitor mv, int val) {
}
}
+ public static void addJpushInsn(MethodVisitor mv, long val) {
+ mv.visitLdcInsn(val);
+ }
+
public static void addSpecialInsn(MethodVisitor mv, int val) {
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, val);
+
mv.visitMethodInsn(
- INVOKESTATIC, config.getInstrumentationDispatcher(), "SPECIAL", "(I)V", false);
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "SPECIAL", "(JI)V", false);
}
/**
@@ -36,9 +288,7 @@ public static void addValueReadInsn(MethodVisitor mv, String desc, String method
if (desc.contains(":")) {
String[] s = desc.split(":");
- if (s.length != 3)
- throw new RuntimeException(
- "Unexpected description (Expected \"owner:name:desc\"): " + desc);
+ SWATAssert.check(s.length == 3, "Unexpected description (Expected \"owner:name:desc\"): {}", desc);
desc = s[2];
}
@@ -50,104 +300,160 @@ public static void addValueReadInsn(MethodVisitor mv, String desc, String method
switch (t.getSort()) {
case Type.DOUBLE -> {
mv.visitInsn(DUP2);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "double",
- "(DI)V",
+ "(DJI)V",
false);
}
case Type.LONG -> {
mv.visitInsn(DUP2);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "long",
- "(JI)V",
+ "(JJI)V",
false);
}
case Type.ARRAY, Type.OBJECT -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "Object",
- "(Ljava/lang/Object;I)V",
+ "(Ljava/lang/Object;JI)V",
false);
}
case Type.BOOLEAN -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "boolean",
- "(ZI)V",
+ "(ZJI)V",
false);
}
case Type.BYTE -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "byte",
- "(BI)V",
+ "(BJI)V",
false);
}
case Type.CHAR -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "char",
- "(CI)V",
+ "(CJI)V",
false);
}
case Type.FLOAT -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "float",
- "(FI)V",
+ "(FJI)V",
false);
}
case Type.INT -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "int",
- "(II)V",
+ "(IJI)V",
false);
}
case Type.SHORT -> {
mv.visitInsn(DUP);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, identifier);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
methodNamePrefix + "short",
- "(SI)V",
+ "(SJI)V",
+ false);
+ }
+ case Type.VOID -> {
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ methodNamePrefix + "void",
+ "(J)V",
false);
}
- case Type.VOID -> mv.visitMethodInsn(
- INVOKESTATIC,
- config.getInstrumentationDispatcher(),
- methodNamePrefix + "void",
- "()V",
- false);
default -> {
System.err.println("Unknown field or method descriptor " + desc);
System.exit(1);
}
}
}
+
+ /**
+ * Adds either the beginning of the try block or the end of the try block including the catch block.
+ * @param mv The method visitor
+ * @param begin True if the beginning of the try block should be added, false if the end of the try block should be added
+ */
+ public static void addTryCatchBlock(MethodVisitor mv, boolean begin, TryCatchBlock tryCatchBlock){
+ if (begin) {
+ // Add the beginning of the try block
+ tryCatchBlock.visit(mv);
+ mv.visitLabel(tryCatchBlock.start());
+ } else {
+ // Add the end of the try block and the catch block
+ mv.visitLabel(tryCatchBlock.end());
+ mv.visitJumpInsn(Opcodes.GOTO, tryCatchBlock.jumpTarget());
+ mv.visitLabel(tryCatchBlock.handler());
+
+ mv.visitInsn(Opcodes.DUP); // The exception object is on the stack
+
+ mv.visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL, "java/lang/Throwable", "printStackTrace", "()V", false);
+ // Print string unsing system.out
+ mv.visitFieldInsn(
+ Opcodes.GETSTATIC,
+ "java/lang/System",
+ "out",
+ "Ljava/io/PrintStream;");
+ mv.visitLdcInsn("[SWAT] Unrecoverable exception in symbolic execution");
+ mv.visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL,
+ "java/io/PrintStream",
+ "println",
+ "(Ljava/lang/String;)V",
+ false);
+
+ mv.visitMethodInsn(Opcodes.INVOKESTATIC, "java/lang/Runtime", "getRuntime", "()Ljava/lang/Runtime;", false);
+ mv.visitLdcInsn(1);
+ mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Runtime", "exit", "(I)V", false);
+ mv.visitInsn(Opcodes.ATHROW); // Rethrow the exception. This will never happen due to the exit call above but the verifier does not know that.
+ mv.visitLabel(tryCatchBlock.jumpTarget());
+
+
+ }
+ }
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationClassAdapter.java
new file mode 100644
index 0000000..e64789c
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationClassAdapter.java
@@ -0,0 +1,97 @@
+package de.uzl.its.swat.instrument.annotation;
+
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.FieldVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * A {@code ClassVisitor} that instruments classes to support symbolic execution by handling
+ * the {@code @Symbolic} annotation. This adapter instruments:
+ *
+ * - Fields annotated with {@code @Symbolic} via {@link AnnotationFieldAdapter}.
+ * - Constructors to process symbolic fields using {@link ConstructorAdapter}.
+ * - Non-constructor methods to handle local variable annotations via {@link AnnotationMethodNode}.
+ *
+ */
+public class AnnotationClassAdapter extends ClassVisitor {
+ private String className;
+ private final List symbolicFields = new ArrayList<>();
+
+ /**
+ * Constructs a new {@code AnnotationClassAdapter} that delegates to the given {@code ClassVisitor}.
+ *
+ * @param cv the next {@code ClassVisitor} in the chain
+ */
+ public AnnotationClassAdapter(ClassVisitor cv) {
+ super(Opcodes.ASM9, cv);
+ }
+
+ /**
+ * Visits the class header and records the internal class name.
+ *
+ * @param version the class version
+ * @param access the class's access flags
+ * @param name the internal name of the class
+ * @param signature the signature of the class, or {@code null} if not generic
+ * @param superName the internal name of the super class
+ * @param interfaces the internal names of the class's interfaces
+ */
+ @Override
+ public void visit(int version, int access, String name, String signature, String superName, String[] interfaces) {
+ this.className = name;
+ super.visit(version, access, name, signature, superName, interfaces);
+ }
+
+ /**
+ * Visits a field of the class and wraps the returned {@code FieldVisitor}
+ * with an {@link AnnotationFieldAdapter} to handle {@code @Symbolic} annotations.
+ *
+ * @param access the field's access flags
+ * @param name the field's name
+ * @param desc the field's descriptor
+ * @param signature the field's signature, or {@code null} if not generic
+ * @param value the field's initial value, or {@code null} if none
+ * @return a visitor to visit field annotations and attributes
+ */
+ @Override
+ public FieldVisitor visitField(int access, String name, String desc, String signature, Object value) {
+ FieldVisitor fv = super.visitField(access, name, desc, signature, value);
+ return new AnnotationFieldAdapter(fv, access, this.className, name, desc, symbolicFields);
+ }
+
+ /**
+ * Visits a method of the class. For constructors, wraps the method visitor with a
+ * {@link ConstructorAdapter} to instrument symbolic fields. For other methods, wraps with
+ * an {@link AnnotationMethodNode} to handle local variable and parameter annotations.
+ *
+ * @param access the method's access flags
+ * @param name the method's name
+ * @param desc the method's descriptor
+ * @param signature the method's signature, or {@code null} if not generic
+ * @param exceptions the internal names of the method's exception classes, or {@code null}
+ * @return a visitor to visit the method's code
+ */
+ @Override
+ public MethodVisitor visitMethod(int access, String name, String desc, String signature, String[] exceptions) {
+ MethodVisitor mv = super.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ if (name.equals("")) {
+ // Instrument constructors to handle symbolic fields.
+ return new ConstructorAdapter(new AnnotationMethodNode(Opcodes.ASM9, access, name, desc, signature, exceptions, mv),
+ className, symbolicFields);
+ } else {
+ // Instrument non-constructors for local variable and parameter annotations.
+ return new AnnotationMethodNode(Opcodes.ASM9, access, name, desc, signature, exceptions, mv);
+ }
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationFieldAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationFieldAdapter.java
new file mode 100644
index 0000000..2b0fdbb
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationFieldAdapter.java
@@ -0,0 +1,63 @@
+package de.uzl.its.swat.instrument.annotation;
+
+import de.uzl.its.swat.annotations.Symbolic;
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import org.objectweb.asm.AnnotationVisitor;
+import org.objectweb.asm.FieldVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
+
+import java.util.List;
+
+/**
+ * A {@code FieldVisitor} that detects fields annotated with {@code @Symbolic} and records them
+ * for later instrumentation.
+ *
+ * When a field is visited, if an annotation matching {@code @Symbolic} is found, the field's
+ * name, descriptor, and whether it is static are recorded into a shared list.
+ *
+ */
+public class AnnotationFieldAdapter extends FieldVisitor {
+ private final String className;
+ private final String fieldName;
+ private final String fieldDesc;
+ private final int access;
+ private final List symbolicFields;
+
+ /**
+ * Constructs a new {@code AnnotationFieldAdapter}.
+ *
+ * @param fv the delegate {@code FieldVisitor}
+ * @param access the field's access flags
+ * @param fieldName the name of the field
+ * @param fieldDesc the descriptor of the field
+ * @param symbolicFields the list to which detected symbolic field information will be added
+ */
+ public AnnotationFieldAdapter(FieldVisitor fv, int access, String className, String fieldName, String fieldDesc, List symbolicFields) {
+ super(Opcodes.ASM9, fv);
+ this.className = className;
+ this.fieldName = fieldName;
+ this.fieldDesc = fieldDesc;
+ this.access = access;
+ this.symbolicFields = symbolicFields;
+ }
+
+ /**
+ * Visits an annotation of the field. If the annotation descriptor matches {@code @Symbolic},
+ * the field is recorded for later instrumentation.
+ *
+ * @param descriptor the descriptor of the annotation
+ * @param visible whether the annotation is visible at runtime
+ * @return an {@code AnnotationVisitor} to visit the annotation values, or the result of the
+ * superclass method if not overridden
+ */
+ @Override
+ public AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
+ AnnotationVisitor av = super.visitAnnotation(descriptor, visible);
+ if (Type.getDescriptor(Symbolic.class).equals(descriptor)) {
+ AnnotationTransformer.getPrintBox().addMsg("Symbolic field identified: " + fieldName);
+ symbolicFields.add(new FieldInfo(this.className, fieldName, fieldDesc, access));
+ }
+ return av;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationMethodNode.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationMethodNode.java
new file mode 100644
index 0000000..41df9fa
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationMethodNode.java
@@ -0,0 +1,257 @@
+package de.uzl.its.swat.instrument.annotation;
+
+import de.uzl.its.swat.annotations.Symbolic;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.instrument.Intrinsics;
+import de.uzl.its.swat.instrument.Utils;
+import org.objectweb.asm.*;
+import org.objectweb.asm.tree.*;
+import org.objectweb.asm.Type;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/**
+ * A {@code MethodNode} implementation that instruments both annotated local variables
+ * and annotated method parameters. For parameters annotated with {@code @Symbolic}, it inserts
+ * instrumentation at method entry (in {@code visitCode}). For local variables annotated with
+ * {@code @Symbolic}, it scans the instruction list at {@code visitEnd} and inserts instrumentation
+ * after each corresponding store instruction.
+ *
+ *
+ */
+public class AnnotationMethodNode extends MethodNode {
+ private final String methodName;
+ private final String methodDesc;
+ // Maps local variable indices to their type descriptors (e.g., "I", "Ljava/lang/String;", etc.)
+ private final Map localVarTypes = new HashMap<>();
+ // Holds indices of local variables annotated with @Symbolic.
+ private final Set symbolicLocalIndices = new HashSet<>();
+ // Holds indices of method parameters annotated with @Symbolic.
+ private final Set symbolicParamIndices = new HashSet<>();
+ // The delegate MethodVisitor.
+ private final MethodVisitor mv;
+
+ /**
+ * Constructs a new {@code AnnotationMethodNode}.
+ *
+ * @param api the ASM API version
+ * @param access the method's access flags
+ * @param name the method name
+ * @param desc the method descriptor
+ * @param signature the method signature (may be null)
+ * @param exceptions the method exceptions (may be null)
+ * @param mv the delegate {@code MethodVisitor}
+ */
+ public AnnotationMethodNode(int api, int access, String name, String desc,
+ String signature, String[] exceptions, MethodVisitor mv) {
+ super(api, access, name, desc, signature, exceptions);
+ this.methodName = name;
+ this.methodDesc = desc;
+ this.mv = mv;
+ }
+
+ /**
+ * Records method parameter annotations. If a parameter is annotated with {@code @Symbolic},
+ * its index is added to the symbolicParamIndices set.
+ *
+ * @param parameter the parameter index
+ * @param descriptor the annotation descriptor
+ * @param visible whether the annotation is visible at runtime
+ * @return an AnnotationVisitor for further annotation processing
+ */
+ @Override
+ public AnnotationVisitor visitParameterAnnotation(int parameter, String descriptor, boolean visible) {
+ if (Type.getDescriptor(Symbolic.class).equals(descriptor)) {
+ symbolicParamIndices.add(parameter);
+ }
+ return super.visitParameterAnnotation(parameter, descriptor, visible);
+ }
+
+ /**
+ * Records local variable type information.
+ *
+ * @param name the local variable name
+ * @param desc the type descriptor
+ * @param signature the variable signature (may be null)
+ * @param start the start label of the variable's scope
+ * @param end the end label of the variable's scope
+ * @param index the variable index
+ */
+ @Override
+ public void visitLocalVariable(String name, String desc, String signature,
+ Label start, Label end, int index) {
+ localVarTypes.put(index, desc);
+ super.visitLocalVariable(name, desc, signature, start, end, index);
+ }
+
+ /**
+ * Records annotations on local variables. If the annotation descriptor matches {@code @Symbolic},
+ * all affected variable indices are recorded.
+ *
+ * @param typeRef a reference to the annotated type
+ * @param typePath the path to the annotated type argument
+ * @param start the start labels for the variable's scope
+ * @param end the end labels for the variable's scope
+ * @param indices the variable indices
+ * @param descriptor the annotation descriptor
+ * @param visible whether the annotation is visible at runtime
+ * @return an AnnotationVisitor for further annotation processing
+ */
+ @Override
+ public AnnotationVisitor visitLocalVariableAnnotation(int typeRef, TypePath typePath,
+ Label[] start, Label[] end,
+ int[] indices, String descriptor,
+ boolean visible) {
+ if (Type.getDescriptor(Symbolic.class).equals(descriptor)) {
+ for (int index : indices) {
+ symbolicLocalIndices.add(index);
+ }
+ }
+ return super.visitLocalVariableAnnotation(typeRef, typePath, start, end, indices, descriptor, visible);
+ }
+
+ /**
+ * Inserts instrumentation code at the beginning of the method for each parameter annotated
+ * with {@code @Symbolic}. For non-static methods, the 'this' parameter is skipped.
+ */
+ @Override
+ public void visitCode() {
+ boolean isStatic = (access & Opcodes.ACC_STATIC) != 0;
+ Type[] argTypes = Type.getArgumentTypes(methodDesc);
+ InsnList paramInstrumentation = new InsnList();
+ for (int i = 0; i < argTypes.length; i++) {
+ if (symbolicParamIndices.contains(i)) {
+ int localIndex = isStatic ? i : i + 1;
+ Type t = argTypes[i];
+ switch (t.getSort()) {
+ case Type.INT:
+ case Type.BOOLEAN:
+ case Type.BYTE:
+ case Type.CHAR:
+ case Type.SHORT:
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.ILOAD, Opcodes.ISTORE, Type.INT_TYPE, true));
+ break;
+ case Type.LONG:
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.LLOAD, Opcodes.LSTORE, Type.LONG_TYPE, true));
+ break;
+ case Type.FLOAT:
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.FLOAD, Opcodes.FSTORE, Type.FLOAT_TYPE, true));
+ break;
+ case Type.DOUBLE:
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.DLOAD, Opcodes.DSTORE, Type.DOUBLE_TYPE, true));
+ break;
+ case Type.ARRAY:
+ // Handle array types (int[], boolean[], etc.)
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.ALOAD, Opcodes.ASTORE, t, true));
+ break;
+ case Type.OBJECT:
+ Type type = Type.getType(Object.class);
+ switch (t.getInternalName()) {
+ case "java/lang/String" -> type = Type.getType(String.class);
+ case "java/lang/Integer" -> type = Type.getType(Integer.class);
+ case "java/lang/Boolean" -> type = Type.getType(Boolean.class);
+ case "java/lang/Byte" -> type = Type.getType(Byte.class);
+ case "java/lang/Character" -> type = Type.getType(Character.class);
+ case "java/lang/Short" -> type = Type.getType(Short.class);
+ case "java/lang/Long" -> type = Type.getType(Long.class);
+ case "java/lang/Float" -> type = Type.getType(Float.class);
+ case "java/lang/Double" -> type = Type.getType(Double.class);
+ case "java/util/List" -> type = Type.getType(java.util.List.class);
+ case "java/util/ArrayList" -> type = Type.getType(java.util.ArrayList.class);
+ case "java/util/LinkedList" -> type = Type.getType(java.util.LinkedList.class);
+ }
+ if(type.equals(Type.getType(java.util.List.class)) ||
+ type.equals(Type.getType(java.util.ArrayList.class)) ||
+ type.equals(Type.getType(java.util.LinkedList.class))) {
+ paramInstrumentation.add(Utils.liftListVariable(localIndex, true, false));
+ break;
+ }
+ paramInstrumentation.add(Utils.liftLocalVariable(localIndex, Opcodes.ALOAD, Opcodes.ASTORE, type, true));
+ break;
+ default:
+ // Ignore unsupported types.
+ break;
+ }
+ }
+ }
+ if (paramInstrumentation.size() > 0) {
+ instructions.insert(paramInstrumentation);
+ }
+ super.visitCode();
+ }
+
+ /**
+ * At method end, iterates through the instruction list and inserts instrumentation code immediately
+ * after any local variable store instruction where the variable was annotated with {@code @Symbolic}.
+ */
+ @Override
+ public void visitEnd() {
+ for (AbstractInsnNode insn : instructions.toArray()) {
+ if (insn instanceof VarInsnNode) {
+ VarInsnNode varInsn = (VarInsnNode) insn;
+ int opcode = varInsn.getOpcode();
+ int var = varInsn.var;
+ if (symbolicLocalIndices.contains(var)) {
+ InsnList instrumentation = new InsnList();
+ switch (opcode) {
+ case Opcodes.ISTORE:
+ instrumentation.add(Utils.liftLocalVariable(var, Opcodes.ILOAD, Opcodes.ISTORE, Type.INT_TYPE, true));
+ break;
+ case Opcodes.LSTORE:
+ instrumentation.add(Utils.liftLocalVariable(var, Opcodes.LLOAD, Opcodes.LSTORE, Type.LONG_TYPE, true));
+ break;
+ case Opcodes.FSTORE:
+ instrumentation.add(Utils.liftLocalVariable(var, Opcodes.FLOAD, Opcodes.FSTORE, Type.FLOAT_TYPE, true));
+ break;
+ case Opcodes.DSTORE:
+ instrumentation.add(Utils.liftLocalVariable(var, Opcodes.DLOAD, Opcodes.DSTORE, Type.DOUBLE_TYPE, true));
+ break;
+ case Opcodes.ASTORE:
+ String descriptor = localVarTypes.get(var);
+ Type t = Type.getType(Object.class);
+
+ // Check if it's an array type
+ if (descriptor.startsWith("[")) {
+ t = Type.getType(descriptor);
+ } else {
+ switch(descriptor) {
+ case "Ljava/lang/String;" -> t = Type.getType(String.class);
+ case "Ljava/lang/Integer;" -> t = Type.getType(Integer.class);
+ case "Ljava/lang/Boolean;" -> t = Type.getType(Boolean.class);
+ case "Ljava/lang/Byte;" -> t = Type.getType(Byte.class);
+ case "Ljava/lang/Character;" -> t = Type.getType(Character.class);
+ case "Ljava/lang/Short;" -> t = Type.getType(Short.class);
+ case "Ljava/lang/Long;" -> t = Type.getType(Long.class);
+ case "Ljava/lang/Float;" -> t = Type.getType(Float.class);
+ case "Ljava/lang/Double;" -> t = Type.getType(Double.class);
+ case "Ljava/util/List;" -> t = Type.getType(java.util.List.class);
+ case "Ljava/util/ArrayList;" -> t = Type.getType(java.util.ArrayList.class);
+ case "Ljava/util/LinkedList;" -> t = Type.getType(java.util.LinkedList.class);
+ default -> SWATAssert.enforce(false, "Unsupported type: {}", descriptor);
+ }
+ }
+
+ if(t.equals(Type.getType(java.util.List.class)) ||
+ t.equals(Type.getType(java.util.ArrayList.class)) ||
+ t.equals(Type.getType(java.util.LinkedList.class))) {
+ instrumentation.add(Utils.liftListVariable(var, true, false));
+ break;
+ }
+ instrumentation.add(Utils.liftLocalVariable(var, Opcodes.ALOAD, Opcodes.ASTORE, t, true));
+ break;
+ default:
+ continue;
+ }
+ instructions.insert(insn, instrumentation);
+ symbolicLocalIndices.remove(var);
+ }
+ }
+ }
+ accept(mv);
+ }
+
+
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationTransformer.java
new file mode 100644
index 0000000..4b07930
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/AnnotationTransformer.java
@@ -0,0 +1,98 @@
+package de.uzl.its.swat.instrument.annotation;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
+import de.uzl.its.swat.instrument.Transformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import lombok.Getter;
+import org.objectweb.asm.ClassReader;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.ClassWriter;
+import org.objectweb.asm.util.CheckClassAdapter;
+
+/**
+ * A {@code ClassFileTransformer} that instruments classes to support symbolic execution
+ * based on the {@code @Symbolic} annotation.
+ *
+ * This transformer uses the {@link AnnotationClassAdapter} to modify classes whose internal
+ * name matches the instrumentation criteria (as determined by {@link Util#shouldInstrument(String)}).
+ * Instrumented classes are logged and added to the list of instrumented classes.
+ *
+ */
+public class AnnotationTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+ private final Config config = Config.instance();
+
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + AnnotationTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ /**
+ * Constructs a new {@code AnnotationTransformer} and initializes logging.
+ */
+ public AnnotationTransformer() {
+ Transformer.getPrintBox().addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ /**
+ * Transforms the supplied class file if it matches the target for annotation instrumentation.
+ *
+ * The transformer uses {@link AnnotationClassAdapter} to modify the class bytecode. It also
+ * verifies the correctness of the modified class if configured to do so.
+ *
+ *
+ * @param loader the defining loader of the class to be transformed, may be null
+ * @param cname the internal name of the class
+ * @param classBeingRedefined if this is triggered by a redefine or retransform, the class being redefined; null otherwise
+ * @param domain the protection domain of the class
+ * @param cbuf the input byte buffer in class file format
+ * @return a well-formed class file buffer (the result of the transform), or the original buffer if no transformation is performed
+ */
+ @Override
+ public byte[] transform(ClassLoader loader, String cname, Class> classBeingRedefined,
+ ProtectionDomain domain, byte[] cbuf) {
+
+ try {
+ // Skip redefinitions and classes that should not be instrumented.
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
+ return cbuf;
+ }
+ getPrintBox().addMsg("Class: " + cname);
+ ClassReader cr = new ClassReader(cbuf);
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new AnnotationClassAdapter(cw);
+ cr.accept(cv, 0);
+
+ if (config.isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(),
+ "Instrumentation error: {}", stringWriter);
+ }
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.ANNOTATION);
+ if (getPrintBox().isContentPresent()) {
+ logger.debug(getPrintBox().toString());
+ }
+ return cw.toByteArray();
+ } catch (Exception e) {
+ // The ErrorHandler has to be here as this method transfers control to ASM
+ new ErrorHandler().handleException("Error while instrumenting class: " + cname, e);
+ }
+ // Return the original bytecode (this transformer does not modify the class).
+ return cbuf;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/ConstructorAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/ConstructorAdapter.java
new file mode 100644
index 0000000..3439133
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/annotation/ConstructorAdapter.java
@@ -0,0 +1,72 @@
+package de.uzl.its.swat.instrument.annotation;
+
+import de.uzl.its.swat.instrument.Utils;
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.tree.InsnList;
+
+import java.util.List;
+
+/**
+ * A {@code MethodVisitor} adapter that instruments constructor methods to process
+ * instance fields annotated with {@code @Symbolic}. Before any return instruction
+ * in a constructor, this adapter injects code to replace the current field value with
+ * its symbolic equivalent.
+ *
+ * Static fields are not instrumented.
+ *
+ */
+public class ConstructorAdapter extends MethodVisitor {
+ private final String className;
+ private final List symbolicFields;
+ private boolean instrumented = false;
+
+ /**
+ * Constructs a new {@code ConstructorAdapter}.
+ *
+ * @param mv the delegate {@code MethodVisitor}
+ * @param className the internal name of the class being instrumented
+ * @param symbolicFields the list of symbolic field metadata to instrument
+ */
+ public ConstructorAdapter(MethodVisitor mv, String className, List symbolicFields) {
+ super(Opcodes.ASM9, mv);
+ this.className = className;
+ this.symbolicFields = symbolicFields;
+ }
+
+ /**
+ * Intercepts instructions in the constructor. Before a return instruction is encountered,
+ * injects instrumentation code for each non-static field annotated with {@code @Symbolic}.
+ *
+ * @param opcode the opcode of the instruction to be visited
+ */
+ @Override
+ public void visitInsn(int opcode) {
+ // If a return instruction is reached and instrumentation has not yet been done, instrument fields.
+ if (!instrumented && (opcode >= Opcodes.IRETURN && opcode <= Opcodes.RETURN)) {
+ for (FieldInfo field : symbolicFields) {
+
+ if (!Utils.isStatic(field.access())) { // Skip static fields
+ instrumentField(field);
+ }
+ }
+ instrumented = true;
+ }
+ super.visitInsn(opcode);
+ }
+
+ /**
+ * Instruments an instance field to lift it to the symbolic domain and fetches an assignment if available.
+ *
+ * @param field the field metadata to instrument
+ */
+ private void instrumentField(FieldInfo field) {
+ mv.visitVarInsn(Opcodes.ALOAD, 0);
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitFieldInsn(Opcodes.GETFIELD, className, field.name(), field.desc());
+ InsnList list = Utils.createLiftInstrumentation(field.getType(), true, false, null);
+ list.accept(mv);
+ mv.visitFieldInsn(Opcodes.PUTFIELD, className, field.name(), field.desc());
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/ClassInfoTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/ClassInfoTransformer.java
new file mode 100644
index 0000000..7799073
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/ClassInfoTransformer.java
@@ -0,0 +1,140 @@
+package de.uzl.its.swat.instrument.classinfo;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.InstrumentationException;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.Transformer;
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import de.uzl.its.swat.metadata.ClassDepot;
+import java.io.IOException;
+import java.io.InputStream;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+import org.objectweb.asm.ClassReader;
+
+public class ClassInfoTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + ClassInfoTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+ @Override
+ public byte[] transform(ClassLoader loader,
+ String cname,
+ Class> classBeingRedefined,
+ ProtectionDomain d,
+ byte[] cbuf) {
+ try {
+ // Only process new classes that should be instrumented.
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
+ return cbuf;
+ }
+
+ getPrintBox().addMsg("Processing class: " + cname);
+ ClassReader cr = new ClassReader(cbuf);
+
+ // --- Collect Parent Class Information ---
+ List parents = getParents(cname, cr, loader);
+ // For each parent, also collect its fields and add to registrations.
+ for (String parentName : parents) {
+ ClassReader parentCr = typeInfo(parentName, loader);
+ FieldCollectorVisitor parentFcv = new FieldCollectorVisitor();
+ parentCr.accept(parentFcv, ClassReader.SKIP_CODE | ClassReader.SKIP_DEBUG | ClassReader.SKIP_FRAMES);
+ }
+
+ // --- Collect Interface Information ---
+ List interfaces = getImplementedInterfaces(cname, cr, loader);
+ for (String iface : interfaces) {
+ ClassReader ifaceCr = typeInfo(iface, loader);
+ FieldCollectorVisitor ifaceFcv = new FieldCollectorVisitor();
+ ifaceCr.accept(ifaceFcv, ClassReader.SKIP_CODE | ClassReader.SKIP_DEBUG | ClassReader.SKIP_FRAMES);
+ }
+
+ // --- Register Collected Information in ClassDepot ---
+ // Register type metadata (parents and interfaces).
+ ClassDepot.getInstrumentationInstance().registerTypeInfoForClass(cname, parents, interfaces);
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.TYPE_MAP);
+ if (getPrintBox().isContentPresent()) {
+ logger.debug(getPrintBox().toString());
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to ASM
+ new ErrorHandler().handleException(new InstrumentationException(cname, t));
+ }
+ // Return the original bytecode (this transformer does not modify the class).
+ return cbuf;
+ }
+
+ /**
+ * Utility method to create a ClassReader for the given type.
+ */
+ private ClassReader typeInfo(final String type, ClassLoader loader) throws IOException {
+ String resource = type + ".class";
+ if (loader == null) {
+ new ErrorHandler().handleException(new InstrumentationException("Cannot create ClassReader for type " + type + " because the class loader is null"));
+ }
+ InputStream is = loader.getResourceAsStream(resource);
+ try (is) {
+ if (is == null) {
+ throw new IOException("Cannot create ClassReader for type " + type);
+ }
+ return new ClassReader(is);
+ }
+ }
+
+ /**
+ * Walks the superclass chain and returns the list of parent class names.
+ */
+ private List getParents(String type, ClassReader cr, ClassLoader loader) throws IOException {
+ List parents = new ArrayList<>();
+ String currentType = type;
+ ClassReader currentCr = cr;
+ while (!"java/lang/Object".equals(currentType)) {
+ currentType = currentCr.getSuperName();
+ parents.add(currentType);
+ currentCr = typeInfo(currentType, loader);
+ }
+ return parents;
+ }
+
+ /**
+ * Retrieves all interfaces implemented by the class (including inherited ones).
+ */
+ private List getImplementedInterfaces(String type, ClassReader cr, ClassLoader loader) throws IOException {
+ List interfaces = new ArrayList<>();
+ String currentType = type;
+ ClassReader currentCr = cr;
+ while (!"java/lang/Object".equals(currentType)) {
+ String[] itfs = currentCr.getInterfaces();
+ interfaces.addAll(Arrays.asList(itfs));
+ currentType = currentCr.getSuperName();
+ currentCr = typeInfo(currentType, loader);
+ }
+ // Also collect interfaces recursively.
+ List allInterfaces = new ArrayList<>(interfaces);
+ for (String itf : interfaces) {
+ allInterfaces.addAll(getInterfacesRecursively(itf, loader));
+ }
+ return allInterfaces;
+ }
+
+ private List getInterfacesRecursively(String name, ClassLoader loader) throws IOException {
+ List result = new ArrayList<>();
+ ClassReader cr = typeInfo(name, loader);
+ String[] itfs = cr.getInterfaces();
+ result.addAll(Arrays.asList(itfs));
+ for (String itf : itfs) {
+ result.addAll(getInterfacesRecursively(itf, loader));
+ }
+ return result;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/FieldCollectorVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/FieldCollectorVisitor.java
new file mode 100644
index 0000000..75f26bd
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classinfo/FieldCollectorVisitor.java
@@ -0,0 +1,35 @@
+package de.uzl.its.swat.instrument.classinfo;
+
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import lombok.Getter;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.FieldVisitor;
+import org.objectweb.asm.Opcodes;
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * A ClassVisitor that collects all declared fields.
+ */
+@Getter
+public class FieldCollectorVisitor extends ClassVisitor {
+ private String className;
+ private final List fields = new ArrayList<>();
+
+ public FieldCollectorVisitor() {
+ super(Opcodes.ASM9);
+ }
+
+ @Override
+ public void visit(int version, int access, String name, String signature, String superName, String[] interfaces) {
+ this.className = name;
+ super.visit(version, access, name, signature, superName, interfaces);
+ }
+
+ @Override
+ public FieldVisitor visitField(int access, String name, String descriptor, String signature, Object value) {
+ fields.add(new FieldInfo(this.className, name, descriptor, access));
+ return super.visitField(access, name, descriptor, signature, value);
+ }
+
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesClassAdapter.java
new file mode 100644
index 0000000..305dd2f
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesClassAdapter.java
@@ -0,0 +1,195 @@
+package de.uzl.its.swat.instrument.classvariables;
+
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.DataType;
+import de.uzl.its.swat.instrument.Utils;
+import java.util.ArrayList;
+
+import de.uzl.its.swat.instrument.common.FieldInfo;
+import org.objectweb.asm.*;
+import org.objectweb.asm.tree.*;
+
+/**
+ * A visitor to visit a Java class. The methods of this class must be called in the following order:
+ * visit [ visitSource ] [ visitModule ][ visitNestHost ][ visitOuterClass ] ( visitAnnotation |
+ * visitTypeAnnotation | visitAttribute )* ( visitNestMember | [ * visitPermittedSubclass ] |
+ * visitInnerClass | visitRecordComponent | visitField | visitMethod )* visitEnd. This class makes
+ * all Variables declared in the class scope symbolic
+ */
+public class ClassVariablesClassAdapter extends ClassVisitor {
+
+
+ private final ArrayList fields = new ArrayList<>(0);
+ private final String cname;
+ private boolean isCreated = false;
+ private final Config config = Config.instance();
+
+ /**
+ * Constructor that calls the super from the default ClassVisitor
+ *
+ * @param cv Parent ClassVisitor
+ */
+ public ClassVariablesClassAdapter(ClassVisitor cv, String cname) {
+ super(Opcodes.ASM9, cv);
+ this.cname = cname;
+ }
+
+ @Override
+ public FieldVisitor visitField(
+ int access, String name, String descriptor, String signature, Object value) {
+
+ FieldVisitor fv = cv.visitField(access, name, descriptor, signature, value);
+ fields.add(new FieldInfo(this.cname, name, descriptor, access));
+ return fv;
+ }
+
+ /**
+ * Visits a method of the class. This method must return a new MethodVisitor instance (or null)
+ * each time it is called, i.e., it should not return a previously returned visitor. Addition:
+ * Add a custom method visitor that instruments the parameters of the method to make them
+ * symbolic
+ *
+ * @param access the method's access flags (see Opcodes). This parameter also indicates if the
+ * method is synthetic and/or deprecated.
+ * @param name the method's name.
+ * @param desc the method's descriptor (see Type).
+ * @param signature the method's signature. May be null if the method parameters, return type
+ * and exceptions do not use generic types.
+ * @param exceptions the internal names of the method's exception classes (see
+ * Type.getInternalName()). May be null.
+ * @return an object to visit the byte code of the method, or null if this class visitor is not
+ * interested in visiting the code of this method.
+ */
+ @Override
+ public MethodVisitor visitMethod(
+ int access, String name, String desc, String signature, String[] exceptions) {
+
+ MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ if (!isCreated) createMethod();
+
+ return mv;
+ }
+
+ private void handleClassVariables(MethodVisitor mv) {
+ for (FieldInfo field : fields) {
+ boolean isStatic = Utils.isStatic(field.access());
+ if (isStatic) continue; // Skip static fields
+
+ ClassVariablesTransformer.getPrintBox().addMsg("Field: " + field.name() + " " + field.desc());
+ ClassVariablesTransformer.getPrintBox().setContentPresent(true);
+ DataType fieldType = DataType.getDataType(field.desc());
+
+ // Declare jump targets
+ Label liftWithoutPrefixString = new Label();
+ Label liftingDone = new Label();
+
+ // Load "this" for the PUTFIELD at the end
+ mv.visitVarInsn(Opcodes.ALOAD, 0);
+ // [this]
+
+ // Get the field value
+ mv.visitVarInsn(Opcodes.ALOAD, 0); // Load "this" again for GETFIELD
+ mv.visitFieldInsn(Opcodes.GETFIELD, cname, field.name(), field.desc());
+ // [this, field]
+
+ // Check if symbolic prefix is provided
+ mv.visitVarInsn(Opcodes.ALOAD, 1); // Load prefix string
+ mv.visitJumpInsn(Opcodes.IFNULL, liftWithoutPrefixString);
+
+ // Add lifting with prefix
+ mv.visitVarInsn(Opcodes.ALOAD, 1); // Load prefix
+ // [this, field, prefix]
+
+ switch (fieldType) {
+ case INTEGER_TYPE, BYTE_TYPE, SHORT_TYPE, CHAR_TYPE, BOOLEAN_TYPE,
+ LONG_TYPE, FLOAT_TYPE, DOUBLE_TYPE, STRING_TYPE -> {
+ // This method has to consume [val, prefix] and leave [val]
+ InsnList lift = Utils.createLiftInstrumentation(
+ field.getType(), false, true, null);
+ lift.accept(mv);
+ // [this, field]
+ }
+ default -> {
+ InsnList unsupported = Utils.addUnsupportedCall();
+ unsupported.accept(mv);
+ mv.visitInsn(Opcodes.POP);
+ // [this, field]
+ }
+ }
+
+ mv.visitJumpInsn(Opcodes.GOTO, liftingDone);
+
+ // Lift without prefix string
+ mv.visitLabel(liftWithoutPrefixString);
+ // [this, field]
+
+ switch (fieldType) {
+ case INTEGER_TYPE, BYTE_TYPE, SHORT_TYPE, CHAR_TYPE, BOOLEAN_TYPE,
+ LONG_TYPE, FLOAT_TYPE, DOUBLE_TYPE, STRING_TYPE -> {
+ InsnList lift = Utils.createLiftInstrumentation(
+ field.getType(), false, false, null);
+ lift.accept(mv);
+ // [this, field]
+ }
+ case LINKEDLIST_TYPE, LIST_TYPE, ARRAYLIST_TYPE -> {
+ InsnList lift = Utils.liftListVariable(-1, false, true);
+ lift.accept(mv);
+ // [this, field]
+ }
+ case OBJECT_TYPE -> {
+ if (Utils.isBoxedPrimitive(field.getType())) {
+ InsnList lift = Utils.createLiftInstrumentation(
+ field.getType(), false, false, null);
+ lift.accept(mv);
+ // [this, field]
+ break;
+ }
+ InsnList lift = Utils.liftClass(field.desc());
+ lift.accept(mv);
+ // [this, field]
+
+ }
+ case ARRAY_TYPE -> {
+ SWATAssert.enforce(false, "Arrays not supported (yet)");
+
+ }
+ default -> SWATAssert.enforce(false, "Unknown data type: " + fieldType);
+ }
+
+ // Store the lifted value back to the field
+ mv.visitLabel(liftingDone);
+ // Stack: [this, field]
+ mv.visitFieldInsn(Opcodes.PUTFIELD, cname, field.name(), field.desc());
+ // Stack: []
+ }
+ }
+
+
+ /** Adds a method to the current class that makes all class variables symbolic. */
+ private void createMethod() {
+ isCreated = true;
+
+ MethodVisitor mv = cv.visitMethod(
+ Opcodes.ACC_PUBLIC,
+ config.getInstrumentationPrefix(),
+ "(Ljava/lang/String;)V",
+ null,
+ null);
+
+ mv.visitCode();
+
+ handleClassVariables(mv);
+
+ mv.visitInsn(Opcodes.RETURN);
+ mv.visitMaxs(0, 0); // Let COMPUTE_FRAMES handle it
+ mv.visitEnd();
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesTransformer.java
new file mode 100644
index 0000000..cc10665
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/classvariables/ClassVariablesTransformer.java
@@ -0,0 +1,111 @@
+package de.uzl.its.swat.instrument.classvariables;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.Transformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+
+import de.uzl.its.swat.instrument.parameter.ParameterTransformer;
+import org.objectweb.asm.ClassReader;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.ClassWriter;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.tree.ClassNode;
+import org.objectweb.asm.util.CheckClassAdapter;
+// import java.util.logging.Logger;
+
+/**
+ * An agent provides an implementation of this interface in order to transform class files. The
+ * transformation occurs before the class is defined by the JVM.
+ */
+public class ClassVariablesTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+ Config config = Config.instance();
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(()
+ -> new PrintBox(60, "Transformer: " + ClassVariablesTransformer.class.getSimpleName()));
+
+ public ClassVariablesTransformer() {
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+
+ /**
+ * The implementation of this method may transform the supplied class file and return a new
+ * replacement class file. Addition: Adds the SpringEndpointClassAdapter for modifying the
+ * classFile
+ *
+ * @param loader the defining loader of the class to be transformed, may be null if the
+ * bootstrap loader
+ * @param cname the name of the class in the internal form of fully qualified class and
+ * interface names as defined in The Java Virtual Machine Specification. For example,
+ * "java/util/List".
+ * @param classBeingRedefined if this is triggered by a redefine or retransform, the class being
+ * redefined or retransformed; if this is a class load, null
+ * @param d the protection domain of the class being defined or redefined
+ * @param cbuf the input byte buffer in class file format - must not be modified
+ * @return a well-formed class file buffer (the result of the transform), or null if no
+ * transform is performed.
+ */
+ @Override
+ public byte[] transform(
+ ClassLoader loader,
+ String cname,
+ Class> classBeingRedefined,
+ ProtectionDomain d,
+ byte[] cbuf) {
+
+ try {
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
+ return cbuf;
+ }
+
+ if (!Transformer.containsRequestBodyClass(cname)) {
+ return cbuf;
+ }
+ getPrintBox().addMsg("Class: " + cname);
+
+ ClassReader cr = new ClassReader(cbuf);
+ ClassNode cn = new ClassNode(Opcodes.ASM9);
+ cr.accept(cn, 0);
+
+ // if (Transformer.getRequestBodyClassTransformed().contains(cname)) {
+ // return cbuf;
+ // }
+
+ ClassWriter cw = new ClassWriter(cr, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new ClassVariablesClassAdapter(cw, cname);
+ cr.accept(cv, 0);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.CLASS_VARIABLES);
+ return cw.toByteArray();
+
+ } catch (Exception e) {
+ // The ErrorHandler has to be here as this method transfers control to ASM
+ ErrorHandler errorHandler = new ErrorHandler();
+ errorHandler.handleException("Error while instrumenting class: " + cname, e);
+ }
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.CLASS_VARIABLES);
+ return cbuf;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/common/FieldInfo.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/common/FieldInfo.java
new file mode 100644
index 0000000..2e43480
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/common/FieldInfo.java
@@ -0,0 +1,23 @@
+package de.uzl.its.swat.instrument.common;
+
+import de.uzl.its.swat.instrument.Utils;
+import org.objectweb.asm.Type;
+
+/**
+ * A record representing metadata for a field annotated with {@code @Symbolic}.
+ *
+ * @param declaringClass the class name in which the field is declared
+ * @param name the field name
+ * @param desc the field descriptor (type information)
+ * @param type the field type
+ * @param access the field access flags
+ */
+public record FieldInfo(String declaringClass, String name, String desc, int access) {
+
+ public boolean isStatic() {
+ return Utils.isStatic(access);
+ }
+ public Type getType() {
+ return Type.getType(desc);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryClassAdapter.java
new file mode 100644
index 0000000..5c238e6
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryClassAdapter.java
@@ -0,0 +1,52 @@
+package de.uzl.its.swat.instrument.dataendpoint;
+
+import de.uzl.its.swat.common.Util;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.commons.LocalVariablesSorter;
+/**
+ * A visitor to visit a Java class. The methods of this class must be called in the following order:
+ * visit [ visitSource ] [ visitModule ][ visitNestHost ][ visitOuterClass ] ( visitAnnotation |
+ * visitTypeAnnotation | visitAttribute )* ( visitNestMember | [ * visitPermittedSubclass ] |
+ * visitInnerClass | visitRecordComponent | visitField | visitMethod )* visitEnd.
+ */
+public class SpringRepositoryClassAdapter extends ClassVisitor {
+ /**
+ * Constructor that calls the super from the default ClassVisitor
+ *
+ * @param cv Parent ClassVisitor
+ */
+ public SpringRepositoryClassAdapter(ClassVisitor cv) {
+ super(Opcodes.ASM9, cv);
+ }
+ /**
+ * Visits a method of the class. This method must return a new MethodVisitor instance (or null)
+ * each time it is called, i.e., it should not return a previously returned visitor. Addition:
+ * Add a custom method visitor that instruments the parameters of all endpoint methods to make
+ * them symbolic.
+ *
+ * @param access the method's access flags (see Opcodes). This parameter also indicates if the
+ * method is synthetic and/or deprecated.
+ * @param name the method's name.
+ * @param desc the method's descriptor (see Type).
+ * @param signature the method's signature. May be null if the method parameters, return type
+ * and exceptions do not use generic types.
+ * @param exceptions the internal names of the method's exception classes (see
+ * Type.getInternalName()). May be null.
+ * @return an object to visit the byte code of the method, or null if this class visitor is not
+ * interested in visiting the code of this method.
+ */
+ @Override
+ public MethodVisitor visitMethod(
+ int access, String name, String desc, String signature, String[] exceptions) {
+ MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ return new SpringRepositoryMethodAdapter(new LocalVariablesSorter(access, desc, mv), name, desc);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryMethodAdapter.java
new file mode 100644
index 0000000..387e5d2
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryMethodAdapter.java
@@ -0,0 +1,235 @@
+package de.uzl.its.swat.instrument.dataendpoint;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.DataType;
+import java.util.*;
+
+import de.uzl.its.swat.instrument.Transformer;
+import de.uzl.its.swat.instrument.Utils;
+import org.objectweb.asm.*;
+import org.objectweb.asm.commons.LocalVariablesSorter;
+import org.objectweb.asm.tree.InsnList;
+
+import static org.objectweb.asm.Opcodes.ASM9;
+
+/**
+ * A visitor to visit a Java method This class visits Spring RestEndpoints and makes all primitive
+ * Datatype parameters symbolic and marks Class objects for later instrumenting.
+ */
+public class SpringRepositoryMethodAdapter extends MethodVisitor {
+
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+ private static final String OWNER_INTERFACE =
+ "org.springframework.data.repository.CrudRepository";
+ // private static final String OWNER_INTERFACE =
+ // "org.springframework.data.jpa.repository.JpaRepository";
+ private static final Map dataTypeString;
+ static {
+ dataTypeString =
+ Map.ofEntries(
+ Map.entry(DataType.BOOLEAN_TYPE, "Z"),
+ Map.entry(DataType.BYTE_TYPE, "B"),
+ Map.entry(DataType.CHAR_TYPE, "C"),
+ Map.entry(DataType.DOUBLE_TYPE, "D"),
+ Map.entry(DataType.FLOAT_TYPE, "F"),
+ Map.entry(DataType.INTEGER_TYPE, "I"),
+ Map.entry(DataType.LONG_TYPE, "J"),
+ Map.entry(DataType.SHORT_TYPE, "S"),
+ Map.entry(DataType.VOID_TYPE, "V"),
+ Map.entry(DataType.STRING_TYPE, "Ljava/lang/String;"),
+ Map.entry(DataType.OBJECT_TYPE, "Ljava/lang/Object;"));
+ }
+
+ // protected int isACustomQuery;
+ private LocalVariablesSorter lvs;
+ /**
+ * Constructor that calls the super from the default MethodVisitor
+ *
+ * @param mv Parent MethodVisitor
+ * @param name The method name
+ * @param desc A string description of the parameters of the method
+ */
+ public SpringRepositoryMethodAdapter(MethodVisitor mv, String name, String desc) {
+ super(ASM9, mv);
+ lvs = (mv instanceof LocalVariablesSorter) ? (LocalVariablesSorter) mv : null;
+ }
+
+ /**
+ * We add logic after every method call (except those filtered in the first if condition) to check whether the
+ * call queries data from a database by checking the interface inheritance tree of the methods owner.
+ * If the owner inherits from the interface specified as string in OWNER_INTERFACE, liftValue or
+ * liftClass will be called on the return of the INVOKE... instruction.
+ *
+ * @param opcode
+ * @param owner
+ * @param name
+ * @param descriptor
+ * @param isInterface
+ */
+ @Override
+ public void visitMethodInsn(
+ final int opcode,
+ final String owner,
+ final String name,
+ final String descriptor,
+ final boolean isInterface) {
+
+ Type returnType;
+ returnType = Type.getReturnType(descriptor);
+
+ // For certain owners or return type we do not want or we do not need to add the lift logic
+ if (!owner.endsWith("SpringDataMethodAdapter")
+ && !owner.startsWith("java/lang")
+ && !owner.startsWith("de/uzl/its/swat")
+ && !(returnType.equals(Type.VOID_TYPE)
+ || (returnType.getSort() == Type.ARRAY)
+ || (returnType.getSort() == Type.METHOD))) {
+
+ String returnTypeString;
+
+ try {
+ returnTypeString = returnType.getDescriptor();
+ } catch (IndexOutOfBoundsException e) {
+ // TODO
+ returnTypeString = "V";
+ }
+
+ int arrayLengthIdx = lvs.newLocal(Type.INT_TYPE);
+ int loopCounterIdx = lvs.newLocal(Type.INT_TYPE);
+ int interfacesIdx = lvs.newLocal(Type.getReturnType("()[Ljava/lang/Class;"));
+ int classNameIdx = lvs.newLocal(Type.getType(String.class));
+ int classNameIdx2 = lvs.newLocal(Type.getType(String.class));
+ int retVarIdx = lvs.newLocal(returnType);
+
+ DataType returnDataType = DataType.getDataType(returnTypeString);
+
+ super.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
+
+ visitVarInsn(returnType.getOpcode(Opcodes.ISTORE), retVarIdx);
+ visitVarInsn(returnType.getOpcode(Opcodes.ILOAD), retVarIdx);
+
+ String crudInterface = OWNER_INTERFACE;
+ Label loop = new Label();
+ Label callMakeSymbolic = new Label();
+ Label done = new Label();
+
+ visitLdcInsn(owner.replace("/", "."));
+
+ // First we retrieve the java.lang.Class of the method's owner object
+ super.visitMethodInsn(
+ Opcodes.INVOKESTATIC,
+ "java/lang/Class",
+ "forName",
+ "(Ljava/lang/String;)Ljava/lang/Class;",
+ false);
+
+ visitVarInsn(Opcodes.ASTORE, classNameIdx);
+ visitVarInsn(Opcodes.ALOAD, classNameIdx);
+
+ // With the class object, we can get the interface inheritance tree ...
+ // ToDo (Issue 92): Performance optimization: Cache result of for loop
+ super.visitMethodInsn(Opcodes.INVOKESTATIC,
+ "de/uzl/its/swat/common/Util",
+ "getAllInterfaces",
+ "(Ljava/lang/Class;)[Ljava/lang/Class;",
+ false);
+ visitVarInsn(Opcodes.ASTORE, interfacesIdx);
+ visitVarInsn(Opcodes.ALOAD, interfacesIdx);
+ // ... and iterate over all interface to compare them against OWNER_INTERFACE
+ visitInsn(Opcodes.ARRAYLENGTH);
+ visitVarInsn(Opcodes.ISTORE, arrayLengthIdx);
+ visitVarInsn(Opcodes.ILOAD, arrayLengthIdx);
+ visitJumpInsn(Opcodes.IFEQ, done);
+ visitLdcInsn(0);
+ visitVarInsn(Opcodes.ISTORE, loopCounterIdx);
+ visitLabel(loop);
+ visitVarInsn(Opcodes.ALOAD, interfacesIdx);
+ visitVarInsn(Opcodes.ILOAD, loopCounterIdx);
+ visitInsn(Opcodes.AALOAD);
+ super.visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL,
+ "java/lang/Class",
+ "getName",
+ "()Ljava/lang/String;",
+ false);
+ visitVarInsn(Opcodes.ASTORE, classNameIdx2);
+ visitVarInsn(Opcodes.ALOAD, classNameIdx2);
+ visitLdcInsn(crudInterface);
+ super.visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL,
+ "java/lang/String",
+ "equals",
+ "(Ljava/lang/Object;)Z",
+ false);
+ // If one interface has the correct name (meaning equals does not return 0), we branch to the makeSymbolic
+ // call.
+ visitJumpInsn(Opcodes.IFNE, callMakeSymbolic);
+ // Otherwise we continue with the loop
+ visitIincInsn(loopCounterIdx, 1);
+ visitVarInsn(Opcodes.ILOAD, loopCounterIdx);
+ visitVarInsn(Opcodes.ILOAD, arrayLengthIdx);
+ // if we iterated over all interfaces and none matched, we go to done and do not make anything symbolic
+ visitJumpInsn(Opcodes.IF_ICMPGE, done);
+ visitJumpInsn(Opcodes.GOTO, loop);
+ visitLabel(callMakeSymbolic);
+ makeSymbolic(returnDataType, Type.getReturnType(descriptor), returnTypeString);
+ visitLabel(done);
+ } else {
+ super.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
+ }
+ }
+
+ private void makeSymbolic(DataType returnDataType, Type returnType, String returnTypeDescriptor) {
+ // ToDo: Either invoke DJVM calls directly or separate handling of MakeSymbolic and
+ // the like in the
+ // backend to be added by another transformer
+ if (dataTypeString.containsKey(returnDataType)) {
+ handleReturnType(returnDataType, returnType, returnTypeDescriptor, "db");
+ } else {
+ SpringRepositoryTransformer.getPrintBox().addMsg("No string mapping for key (while making database return symbolic): "
+ + returnDataType);
+ }
+ }
+
+
+ protected void handleReturnType(DataType returnParameterType, Type returnType, String returnTypeDescriptor, String symbolicVarPrefix) {
+
+ if (returnParameterType == DataType.BYTE_TYPE
+ || returnParameterType == DataType.CHAR_TYPE
+ || returnParameterType == DataType.DOUBLE_TYPE
+ || returnParameterType == DataType.FLOAT_TYPE
+ || returnParameterType == DataType.INTEGER_TYPE
+ || returnParameterType == DataType.LONG_TYPE
+ || returnParameterType == DataType.SHORT_TYPE
+ || returnParameterType == DataType.STRING_TYPE
+ || returnParameterType == DataType.BOOLEAN_TYPE) {
+
+ InsnList list = Utils.createLiftInstrumentation(returnType, false, false, symbolicVarPrefix);
+ list.accept(mv);
+
+ } else if (returnParameterType == DataType.OBJECT_TYPE) {
+ String returnTypeDescriptorCleaned = returnTypeDescriptor.substring(1, returnTypeDescriptor.length() - 1);
+ System.out.println("Return type: " + returnTypeDescriptorCleaned);
+ if (Util.shouldInstrument(returnTypeDescriptorCleaned)) {
+
+ Transformer.retransform(returnTypeDescriptorCleaned, true);
+ mv.visitInsn(Opcodes.DUP);
+
+ String returnTypeDescriptorDot = returnTypeDescriptor.substring(1, returnTypeDescriptor.length() - 1).replace("/", ".");
+ visitLdcInsn(returnTypeDescriptorDot);
+ visitLdcInsn(Config.instance().getInstrumentationPrefix());
+ visitLdcInsn(symbolicVarPrefix);
+ super.visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/common/UtilInstrumented",
+ "liftClass", "(Ljava/lang/Object;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)V",
+ false);
+ } else {
+ logger.warn("Unknown return Type {}", returnTypeDescriptor);
+ }
+ } else {
+ logger.warn("Unknown DataType in return value with type {}", dataTypeString.get(returnParameterType));
+ }
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryTransformer.java
new file mode 100644
index 0000000..8f41f71
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/dataendpoint/SpringRepositoryTransformer.java
@@ -0,0 +1,110 @@
+package de.uzl.its.swat.instrument.dataendpoint;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
+import de.uzl.its.swat.instrument.Transformer;
+
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+
+import lombok.Getter;
+import org.objectweb.asm.ClassReader;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.ClassWriter;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.tree.ClassNode;
+import org.objectweb.asm.util.CheckClassAdapter;
+
+/**
+ * An agent provides an implementation of this interface in order to transform class files. The
+ * transformation occurs before the class is defined by the JVM.
+ */
+public class SpringRepositoryTransformer implements ClassFileTransformer {
+
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+ @Getter private static PrintBox printBox;
+
+ public SpringRepositoryTransformer() {
+ printBox = new PrintBox(60, "Transformer: " + "DataEndpoint");
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ /**
+ * The implementation of this method may transform the supplied class file and return a new
+ * replacement class file. Addition: Adds the SpringEndpointClassAdapter for modifying the
+ * classFile
+ *
+ * @param loader the defining loader of the class to be transformed, may be null if the
+ * bootstrap loader
+ * @param cname the name of the class in the internal form of fully qualified class and
+ * interface names as defined in The Java Virtual Machine Specification. For example,
+ * "java/util/List".
+ * @param classBeingRedefined if this is triggered by a redefine or retransform, the class being
+ * redefined or retransformed; if this is a class load, null
+ * @param d the protection domain of the class being defined or redefined
+ * @param cbuf the input byte buffer in class file format - must not be modified
+ * @return a well-formed class file buffer (the result of the transform), or null if no
+ * transform is performed.
+ */
+ @Override
+ public byte[] transform(
+ ClassLoader loader,
+ String cname,
+ Class> classBeingRedefined,
+ ProtectionDomain d,
+ byte[] cbuf) {
+
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
+ return cbuf;
+ }
+
+ printBox.addMsg("Class: " + cname);
+ printBox.setContentPresent(true);
+
+ try {
+ ClassReader cr = new ClassReader(cbuf);
+ ClassNode cn = new ClassNode(Opcodes.ASM9);
+ cr.accept(cn, ClassReader.EXPAND_FRAMES);
+
+ ClassWriter cw = new SafeClassWriter(cr, loader,
+ ClassWriter.COMPUTE_FRAMES); // ClassWriter.COMPUTE_MAXS);
+ ClassVisitor cv = new SpringRepositoryClassAdapter(cw);
+
+ cr.accept(cv, ClassReader.EXPAND_FRAMES);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: " + stringWriter);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_DATA);
+ if (printBox.isContentPresent()) {
+ logger.debug(printBox.toString());
+ }
+ return cw.toByteArray();
+ } catch (Throwable t) {
+
+ ErrorHandler errorHandler = new ErrorHandler();
+ errorHandler.handleException("Error while instrumenting class: " + cname, t);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_DATA);
+ if (printBox.isContentPresent()) {
+ logger.debug(printBox.toString());
+ }
+
+ return cbuf;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java
index cf31c3f..60bba95 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java
@@ -1,10 +1,13 @@
package de.uzl.its.swat.instrument.instruction;
+import de.uzl.its.swat.common.Util;
import de.uzl.its.swat.instrument.GlobalStateForInstrumentation;
-import de.uzl.its.swat.symbolic.ClassNames;
+import de.uzl.its.swat.metadata.ClassDepot;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.commons.JSRInlinerAdapter;
+import org.objectweb.asm.commons.TryCatchBlockSorter;
/**
* A visitor to visit a Java class. The methods of this class must be called in the following order:
@@ -24,6 +27,20 @@ public InstructionClassAdapter(ClassVisitor cv, String cname) {
this.cname = cname;
}
+ @Override
+ public void visit(
+ int version,
+ int access,
+ String name,
+ String signature,
+ String superName,
+ String[] interfaces) {
+ long cIdx = ClassDepot.getInstrumentationInstance().getClassIndex(name);
+ GlobalStateForInstrumentation.instance.setCid(cIdx);
+
+ super.visit(version, access, name, signature, superName, interfaces);
+ }
+
/**
* Visits a method of the class. This method must return a new MethodVisitor instance (or null)
* each time it is called, i.e., it should not return a previously returned visitor. Addition:
@@ -47,13 +64,25 @@ public MethodVisitor visitMethod(
if (cname.equals("de/uzl/its/swat/instrument/svcomp/Verifier") && !name.equals("assume")) {
return mv;
}
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
if (mv != null) {
- return new InstructionMethodAdapter(
- mv,
- name.equals(""),
- GlobalStateForInstrumentation.instance,
- ClassNames.getInstance(),
- name);
+ InstructionMethodAdapter ima =
+ new InstructionMethodAdapter(
+ new TryCatchBlockSorter(
+ new JSRInlinerAdapter(mv, access, name, desc, signature, exceptions)
+ , access, name, desc, signature, exceptions),
+ name.equals(""),
+ (access & Opcodes.ACC_STATIC) != 0,
+ GlobalStateForInstrumentation.instance,
+ name,
+ desc,
+ cname);
+ return ima;
}
return null;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java
index 266d090..fa43293 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java
@@ -1,28 +1,45 @@
package de.uzl.its.swat.instrument.instruction;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.exceptions.InstrumentationException;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.coverage.BranchCoverage;
import de.uzl.its.swat.instrument.GlobalStateForInstrumentation;
import de.uzl.its.swat.instrument.TryCatchBlock;
import de.uzl.its.swat.instrument.Utils;
-import de.uzl.its.swat.symbolic.ClassNames;
-import de.uzl.its.swat.symbolic.ObjectInfo;
+import de.uzl.its.swat.metadata.ClassDepot;
+
+import java.lang.reflect.Field;
+import java.lang.reflect.Method;
+import java.lang.reflect.Modifier;
import java.util.Arrays;
-import java.util.LinkedList;
-import org.objectweb.asm.Handle;
-import org.objectweb.asm.Label;
-import org.objectweb.asm.MethodVisitor;
-import org.objectweb.asm.Opcodes;
+import java.util.List;
+
+import de.uzl.its.swat.metadata.ClassDepotInstrumentation;
+import org.objectweb.asm.*;
/** A visitor to visit a Java method */
public class InstructionMethodAdapter extends MethodVisitor implements Opcodes {
boolean isInit;
+ boolean isStatic;
boolean isSuperInitCalled;
- LinkedList tryCatchBlocks;
boolean calledNew = false;
+ private boolean seenCode = false;
private final GlobalStateForInstrumentation instrumentationState;
- private final ClassNames classNames;
+ private final ClassDepotInstrumentation classDepot = ClassDepot.getInstrumentationInstance();
private final String methodName;
+ private final String desc;
+ private final String owner;
+ // private final String parentCname;
+ private long clinitInvokeId = -1;
+
+ List setFieldMethods = Arrays.asList("set", "setBoolean", "setByte", "setChar", "setDouble",
+ "setFloat", "setInt", "setLong", "setShort");
+ List getFieldMethods = Arrays.asList("get", "getBoolean", "getByte", "getChar", "getDouble",
+ "getFloat", "getInt", "getLong", "getShort");
+
private final Config config = Config.instance();
/**
@@ -31,35 +48,61 @@ public class InstructionMethodAdapter extends MethodVisitor implements Opcodes {
* @param mv The MethodVisitor that should be used
* @param isInit Determines if the method is an initializer method
* @param instrumentationState The current state of instrumentation
- * @param classNames The class names
* @param methodName The Method name
*/
public InstructionMethodAdapter(
MethodVisitor mv,
boolean isInit,
+ boolean isStatic,
GlobalStateForInstrumentation instrumentationState,
- ClassNames classNames,
- String methodName) {
+ String methodName,
+ String desc,
+ String owner) {
super(ASM9, mv);
this.isInit = isInit;
+ this.isStatic = isStatic;
this.isSuperInitCalled = false;
- tryCatchBlocks = new LinkedList();
this.instrumentationState = instrumentationState;
- this.classNames = classNames;
this.methodName = methodName;
+ this.owner = owner;
+ this.desc = desc;
}
/** Starts the visit of the method's code, if any (i.e. non abstract method). */
@Override
public void visitCode() {
+ GlobalStateForInstrumentation.instance.setActiveInstrumentation(true);
+ seenCode = true;
+ // ToDo: Understand why or whether visitCode at the beginning is correct (rather than at the
+ // end)
+ mv.visitCode();
+
+ long mIdx = ClassDepot.getInstrumentationInstance().getMethodIdxForInstrumentation(owner, methodName, desc);
+ instrumentationState.setMid(mIdx);
+
if (methodName.equals("")) {
- addSpecialInsn(mv, 2);
+ int cIdx = classDepot.getClassIndex(this.owner);
+ String clinit_desc = "(JIJ)V"; // (long iid, int cIdx, long invokeId)
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addBipushInsn(mv, cIdx);
+ clinitInvokeId = instrumentationState.incAndGetInvokeId();
+ addJpushInsn(mv, clinitInvokeId);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "CLINIT",
+ clinit_desc,
+ false);
+
+ } else {
+ addSpecialInsn(mv, 0);
}
- instrumentationState.incMid();
- mv.visitCode();
}
+ private static void addJpushInsn(MethodVisitor mv, long val) {
+ Utils.addJpushInsn(mv, val);
+ }
/** Push a value onto the stack. */
private static void addBipushInsn(MethodVisitor mv, int val) {
Utils.addBipushInsn(mv, val);
@@ -76,27 +119,17 @@ private void addSpecialInsn(MethodVisitor mv, int val) {
}
private void addInsn(MethodVisitor mv, String insn, boolean exception, int opcode) {
- String desc = "()V";
- if (config.isInstrumentationInstructionIds()) {
- desc = "(II)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- addBipushInsn(mv, instrumentationState.getMid());
- } else if (exception) {
- desc = "(I)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- }
+ String desc = "(J)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
mv.visitMethodInsn(INVOKESTATIC, config.getInstrumentationDispatcher(), insn, desc, false);
mv.visitInsn(opcode);
}
/** Add var insn and its instrumentation code. */
private void addVarInsn(MethodVisitor mv, int var, String insn, int opcode) {
- String desc = "(I)V";
- if (config.isInstrumentationInstructionIds()) {
- desc = "(III)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(JI)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, var);
mv.visitMethodInsn(INVOKESTATIC, config.getInstrumentationDispatcher(), insn, desc, false);
@@ -104,12 +137,9 @@ private void addVarInsn(MethodVisitor mv, int var, String insn, int opcode) {
}
private void addTypeInsn(MethodVisitor mv, String type, int opcode, String name) {
- String desc = "(ILjava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(IILjava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(JLjava/lang/String;)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
mv.visitLdcInsn(type);
mv.visitMethodInsn(INVOKESTATIC, config.getInstrumentationDispatcher(), name, desc, false);
mv.visitTypeInsn(opcode, type);
@@ -565,32 +595,48 @@ public void visitInsn(int opcode) {
case IRETURN:
ex = true;
addInsn(mv, "IRETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case LRETURN:
ex = true;
addInsn(mv, "LRETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case FRETURN:
ex = true;
addInsn(mv, "FRETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case DRETURN:
ex = true;
addInsn(mv, "DRETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case ARETURN:
ex = true;
addInsn(mv, "ARETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case RETURN:
ex = true;
- addInsn(mv, "RETURN", ex, opcode);
- addSpecialInsn(mv, 0); // for non-exceptional path
+ // addInsn(mv, "RETURN", ex, opcode);
+ String desc = "(J)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "RETURN", desc, false);
+ if (methodName.equals("")) {
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, clinitInvokeId);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "INVOKECLINIT_END",
+ "(JJ)V",
+ false);
+ }
+ mv.visitInsn(opcode);
+
+ // addSpecialInsn(mv, 0); // for non-exceptional path
break;
case ARRAYLENGTH:
ex = true;
@@ -613,8 +659,7 @@ public void visitInsn(int opcode) {
addInsn(mv, "MONITOREXIT", ex, opcode);
addSpecialInsn(mv, 0); // for non-exceptional path
break;
- default:
- throw new RuntimeException("Unknown instruction opcode " + opcode);
+ default: throw new InstrumentationException("Unknown instruction opcode " + opcode);
}
}
@@ -671,7 +716,7 @@ public void visitVarInsn(int opcode, int var) {
addVarInsn(mv, var, "RET", opcode);
break;
default:
- throw new RuntimeException("Unknown var insn");
+ throw new InstrumentationException("Unknown var insn");
}
}
@@ -688,16 +733,9 @@ public void visitVarInsn(int opcode, int var) {
*/
@Override
public void visitIntInsn(int opcode, int operand) {
+ String desc = "(JI)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
- String desc = "(I)V";
- if (config.isInstrumentationInstructionIds()) {
- desc = "(III)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- addBipushInsn(mv, instrumentationState.getMid());
- } else if (opcode == NEWARRAY) {
- desc = "(II)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- }
switch (opcode) {
case BIPUSH:
addBipushInsn(mv, operand);
@@ -721,7 +759,7 @@ public void visitIntInsn(int opcode, int operand) {
addSpecialInsn(mv, 0); // for non-exceptional path
return;
default:
- throw new RuntimeException("Unknown int instruction opcode " + opcode);
+ throw new InstrumentationException("Unknown int instruction opcode " + opcode);
}
mv.visitIntInsn(opcode, operand);
}
@@ -739,17 +777,14 @@ public void visitIntInsn(int opcode, int operand) {
public void visitTypeInsn(int opcode, String type) {
switch (opcode) {
case NEW:
- String desc = "(ILjava/lang/String;I)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(IILjava/lang/String;I)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(JLjava/lang/String;I)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
mv.visitLdcInsn(type);
- int cIdx = classNames.get(type);
+ int cIdx = classDepot.getClassIndex(type);
addBipushInsn(mv, cIdx);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "NEW", desc, false);
+
mv.visitTypeInsn(opcode, type);
addSpecialInsn(mv, 0); // for non-exceptional path
@@ -769,7 +804,7 @@ public void visitTypeInsn(int opcode, String type) {
addValueReadInsn(mv, "I", "GETVALUE_");
break;
default:
- throw new RuntimeException("Unknown type instruction opcode " + opcode);
+ throw new InstrumentationException("Unknown type instruction opcode " + opcode);
}
}
@@ -785,19 +820,14 @@ public void visitTypeInsn(int opcode, String type) {
*/
@Override
public void visitFieldInsn(int opcode, String owner, String name, String desc) {
- String d = "(IIILjava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- d = "(IIIILjava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
- int cIdx = classNames.get(owner);
+ String d = "(JILjava/lang/String;Ljava/lang/String;)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
+ int cIdx = classDepot.getClassIndex(owner);
addBipushInsn(mv, cIdx);
- ObjectInfo tmp = classNames.get(cIdx);
switch (opcode) {
case GETSTATIC:
- int fIdx = tmp.getIdx(name, true);
- addBipushInsn(mv, fIdx);
+ mv.visitLdcInsn(name);
mv.visitLdcInsn(desc);
mv.visitMethodInsn(
@@ -805,21 +835,22 @@ public void visitFieldInsn(int opcode, String owner, String name, String desc) {
mv.visitFieldInsn(opcode, owner, name, desc);
addSpecialInsn(mv, 0); // for non-exceptional path
+
addValueReadInsn(mv, owner + ":" + name + ":" + desc, "GETVALUE_");
break;
case PUTSTATIC:
- fIdx = tmp.getIdx(name, true);
- addBipushInsn(mv, fIdx);
+ mv.visitLdcInsn(name);
mv.visitLdcInsn(desc);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "PUTSTATIC", d, false);
+
mv.visitFieldInsn(opcode, owner, name, desc);
addSpecialInsn(mv, 0); // for non-exceptional path
+
break;
case GETFIELD:
- fIdx = tmp.getIdx(name, false);
- addBipushInsn(mv, fIdx);
+ mv.visitLdcInsn(name);
mv.visitLdcInsn(desc);
mv.visitMethodInsn(
@@ -829,8 +860,7 @@ public void visitFieldInsn(int opcode, String owner, String name, String desc) {
addValueReadInsn(mv, owner + ":" + name + ":" + desc, "GETVALUE_");
break;
case PUTFIELD:
- fIdx = tmp.getIdx(name, false);
- addBipushInsn(mv, fIdx);
+ mv.visitLdcInsn(name);
mv.visitLdcInsn(desc);
mv.visitMethodInsn(
@@ -839,70 +869,700 @@ public void visitFieldInsn(int opcode, String owner, String name, String desc) {
addSpecialInsn(mv, 0); // for non-exceptional path
break;
default:
- throw new RuntimeException("Unknown field access opcode " + opcode);
+ throw new InstrumentationException("Unknown field access opcode " + opcode);
}
}
private String getMethodNameByOpcode(int opcode) {
- switch (opcode) {
- case INVOKESPECIAL:
- return "INVOKESPECIAL";
- case INVOKESTATIC:
- return "INVOKESTATIC";
- case INVOKEINTERFACE:
- return "INVOKEINTERFACE";
- case INVOKEVIRTUAL:
- return "INVOKEVIRTUAL";
- case INVOKEDYNAMIC:
- return "INVOKEDYNAMIC";
- default:
- throw new RuntimeException("Unknown opcode for method");
+ return switch (opcode) {
+ case INVOKESPECIAL -> "INVOKESPECIAL";
+ case INVOKESTATIC -> "INVOKESTATIC";
+ case INVOKEINTERFACE -> "INVOKEINTERFACE";
+ case INVOKEVIRTUAL -> "INVOKEVIRTUAL";
+ case INVOKEDYNAMIC -> "INVOKEDYNAMIC";
+ default -> throw new InstrumentationException("Unknown method access opcode " + opcode);
+ };
+ }
+
+ @SuppressWarnings("unused")
+ public static String getInitDescriptorFromParameterList(Class>[] constructorParameters) {
+
+ StringBuilder initDescriptor = new StringBuilder("(");
+ if (constructorParameters != null) {
+ for (Class> p : constructorParameters) {
+ String internalName = Type.getType(p).getDescriptor();
+ initDescriptor.append(internalName);
+ }
}
+ return initDescriptor.append(")V").toString();
}
- private void addMethodWithTryCatch(
- int opcode, String owner, String name, String desc, boolean itf) {
- String d = "(ILjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- d = "(IILjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
- addBipushInsn(mv, instrumentationState.getMid());
+ // First implementation only works for constructors without parameters
+ private void handleClassCreationByReflection(long invokeSpecialInvokeId) {
+
+ // get class name
+ mv.visitInsn(SWAP);
+ // DUP for getDeclaringClass
+ mv.visitInsn(DUP);
+ // DUP for Constructor Parameters
+ mv.visitInsn(DUP);
+
+ mv.visitMethodInsn(
+ INVOKEVIRTUAL,
+ "java/lang/reflect/Constructor",
+ "getParameterTypes",
+ "()[Ljava/lang/Class;",
+ false);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "getInitDescriptorFromParameterList",
+ "([Ljava/lang/Class;)Ljava/lang/String;",
+ false);
+
+ // Getting java/lang/Class object to retrieve constructor
+ mv.visitInsn(SWAP);
+
+ mv.visitMethodInsn(
+ INVOKEVIRTUAL,
+ "java/lang/reflect/Constructor",
+ "getDeclaringClass",
+ "()Ljava/lang/Class;",
+ false);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "org/objectweb/asm/Type",
+ "getInternalName",
+ "(Ljava/lang/Class;)Ljava/lang/String;",
+ false);
+
+ // Type name for NEW is on the stack; we duplicate because we need it to get the cidx
+ mv.visitInsn(DUP);
+ // Duplicating once more for the invoke special call at the end
+ mv.visitInsn(DUP);
+
+ long reflectNewId = instrumentationState.incAndGetId();
+ addJpushInsn(mv, reflectNewId);
+ // Duplicating the ID before the type name on the stack
+ mv.visitInsn(DUP2_X2);
+ // Afterward the ID on top of the stack can be discarded
+ mv.visitInsn(POP2);
+
+ // Finally, get the ClassDepot instance and put the cIdx on the stack
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "de/uzl/its/swat/metadata/ClassDepot",
+ "getRuntimeInstance",
+ "()Lde/uzl/its/swat/metadata/ClassDepotRuntime;",
+ false);
+ mv.visitInsn(SWAP);
+ mv.visitMethodInsn(
+ INVOKEINTERFACE,
+ "de/uzl/its/swat/metadata/ClassDepotRuntime",
+ "getClassIndex",
+ "(Ljava/lang/String;)I",
+ true);
+
+ String descriptorNew = "(JLjava/lang/String;I)V";
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "SWAP", "(J)V", false);
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "POP", "(J)V", false);
+
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "NEW", descriptorNew, false);
+ addSpecialInsn(mv, 0);
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "DUP_X1", "(J)V", false);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC, config.getInstrumentationDispatcher(), "SWAP", "(J)V", false);
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "UNPACK_INVOKE_PARAMETER",
+ "(J)V",
+ false);
+
+ // Filling the stack for INVOKESPECIAL, we should already have owner string on the stack,
+ // however, we have
+ // to move the instruction id and invoke id in front of that
+ // And before doing that, we swap the descriptor and classname
+ mv.visitInsn(SWAP);
+
+ long reflectInvokeSpecialId = instrumentationState.incAndGetId();
+ addJpushInsn(mv, reflectInvokeSpecialId);
+ mv.visitInsn(DUP2_X2);
+ mv.visitInsn(POP2);
+
+ addJpushInsn(mv, invokeSpecialInvokeId);
+ mv.visitInsn(DUP2_X2);
+ mv.visitInsn(POP2);
+
+ String invokeSpecialMethodName = "";
+
+ mv.visitLdcInsn(invokeSpecialMethodName);
+ // mv.visitLdcInsn(invokeSpecialMethodDesc);
+ // Function name must and descriptor must be swapped.
+ mv.visitInsn(SWAP);
+ // There is another signature which additionally includes the method id, not implemented yet
+
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "INVOKESPECIAL",
+ "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V",
+ false);
+
+ mv.visitInsn(SWAP);
+ }
+
+ @SuppressWarnings("unused")
+ public static MethodInvokeInformationHolder methodInvokeReceiver(
+ Method m, Object obj, Object[] args) {
+ String methodDescriptor = Type.getMethodDescriptor(m);
+ String methodName = m.getName();
+ // Class[] argTypes = m.getParameterTypes();
+ // Class returnType = m.getReturnType();
+ // ToDo: Do we have to add an L prefix?
+
+ boolean isStatic = Modifier.isStatic(m.getModifiers());
+
+ String owner;
+ if (isStatic) {
+ owner = Type.getInternalName(m.getDeclaringClass());
+ } else {
+ SWATAssert.enforce(obj != null, "Object cannot be null");
+ owner = Type.getInternalName(obj.getClass());
+ }
+
+ return new MethodInvokeInformationHolder(
+ methodName, methodDescriptor, owner, m, obj, args);
+ }
+
+ @SuppressWarnings("unused")
+ public static Method createSymbolicInvokeVirtualViaMethodInvoke(
+ MethodInvokeInformationHolder info) {
+ String dispatcherName = Config.instance().getInstrumentationDispatcher();
+ Method invokeVirtualMethod = null;
+ try {
+ Class> dispatcherClass = Class.forName(dispatcherName.replace("/", "."));
+ invokeVirtualMethod =
+ dispatcherClass.getMethod(
+ "INVOKEVIRTUAL",
+ long.class,
+ long.class,
+ String.class,
+ String.class,
+ String.class);
+ } catch (Exception e) {
+ throw new InstrumentationException(e);
+ }
+
+ return invokeVirtualMethod;
+ }
+
+ private void handleMethodInvokeCall(long invokeId, long iid) {
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "methodInvokeReceiver",
+ "(Ljava/lang/reflect/Method;Ljava/lang/Object;[Ljava/lang/Object;)Lde/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder;",
+ false);
+ mv.visitInsn(DUP);
+ mv.visitInsn(DUP);
+ // Prepare stack for invoke call
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "createSymbolicInvokeVirtualViaMethodInvoke",
+ "(Lde/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder;)Ljava/lang/reflect/Method;",
+ false);
+ // place owner (java.lang.reflect.Method object) for invokevirtual via method.invoke
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ // place first parameter for invoke virtual
+ mv.visitInsn(ACONST_NULL);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ // place second parameter for invoke virtual on the stack, this in a varargs array of
+ // java/lang/Objects
+ mv.visitInsn(ICONST_5);
+ mv.visitTypeInsn(ANEWARRAY, "java/lang/Object");
+ mv.visitInsn(DUP);
+ // Add first parameter of the dispatchers invokevirtual to the array
+ mv.visitInsn(ICONST_0);
+ mv.visitLdcInsn(iid);
+ mv.visitMethodInsn(INVOKESTATIC, "java/lang/Long", "valueOf", "(J)Ljava/lang/Long;", false);
+ mv.visitInsn(AASTORE);
+ mv.visitInsn(DUP);
+ // Add the second parameter of the dispatchers invokevirtual
+ mv.visitInsn(ICONST_1);
+ mv.visitLdcInsn(invokeId);
+ mv.visitMethodInsn(INVOKESTATIC, "java/lang/Long", "valueOf", "(J)Ljava/lang/Long;", false);
+ mv.visitInsn(AASTORE);
+
+ // Add the third parameter of the dispatchers invokevirtual to the array
+ // (owner)
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitInsn(DUP_X1);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "owner",
+ "Ljava/lang/String;");
+ mv.visitInsn(SWAP);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(ICONST_2);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(AASTORE);
+ // place fourth parameter of the dispatchers invokevirtual in the array
+ // (name)
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitInsn(DUP_X1);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "methodName",
+ "Ljava/lang/String;");
+ mv.visitInsn(SWAP);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(ICONST_3);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(AASTORE);
+ // place the fifth parameter of the dispatchers invokevirtual in the array
+ // (desc)
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitInsn(DUP_X1);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "methodDescriptor",
+ "Ljava/lang/String;");
+ mv.visitInsn(SWAP);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(ICONST_4);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(AASTORE);
+
+ mv.visitInsn(SWAP);
+ mv.visitInsn(POP);
+
+ mv.visitMethodInsn(
+ INVOKEVIRTUAL,
+ "java/lang/reflect/Method",
+ "invoke",
+ "(Ljava/lang/Object;[Ljava/lang/Object;)Ljava/lang/Object;",
+ false);
+ // Drop null return value as the called method returns null
+ mv.visitInsn(POP);
+
+ // restore stack for 'normal' execution
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "methodObject",
+ "Ljava/lang/reflect/Method;");
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "ownerObject",
+ "Ljava/lang/Object;");
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitFieldInsn(
+ GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder",
+ "argObjects",
+ "[Ljava/lang/Object;");
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.ObjectSetFieldInformationHolder setObjectFieldReceiver(
+ Field f, Object target, Object member) {
+ return new SetFieldInformationHolder.ObjectSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.BooleanSetFieldInformationHolder setBooleanFieldReceiver(
+ Field f, Object target, boolean member) {
+ return new SetFieldInformationHolder.BooleanSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.ByteSetFieldInformationHolder setByteFieldReceiver(
+ Field f, Object target, byte member) {
+ return new SetFieldInformationHolder.ByteSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.CharSetFieldInformationHolder setCharFieldReceiver(
+ Field f, Object target, char member) {
+ return new SetFieldInformationHolder.CharSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.DoubleSetFieldInformationHolder setDoubleFieldReceiver(
+ Field f, Object target, double member) {
+ return new SetFieldInformationHolder.DoubleSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.FloatSetFieldInformationHolder setFloatFieldReceiver(
+ Field f, Object target, float member) {
+ return new SetFieldInformationHolder.FloatSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.IntSetFieldInformationHolder setIntFieldReceiver(
+ Field f, Object target, int member) {
+ return new SetFieldInformationHolder.IntSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.LongSetFieldInformationHolder setLongFieldReceiver(
+ Field f, Object target, long member) {
+ return new SetFieldInformationHolder.LongSetFieldInformationHolder(f, target, member);
+ }
+
+ @SuppressWarnings("unused")
+ public static SetFieldInformationHolder.ShortSetFieldInformationHolder setShortFieldReceiver(
+ Field f, Object target, short member) {
+ return new SetFieldInformationHolder.ShortSetFieldInformationHolder(f, target, member);
+ }
+
+ private void handleFieldSetFieldCall(String owner, String name, String desc, long invokeId) {
+ boolean isWideOperand = false;
+
+ if (name.equals("set")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setObjectFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;Ljava/lang/Object;)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ObjectSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setBoolean")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setBooleanFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;Z)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BooleanSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setByte")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setByteFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;B)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ByteSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setChar")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setCharFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;C)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$CharSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setDouble")) {
+ isWideOperand = true;
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setDoubleFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;D)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$DoubleSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setFloat")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setFloatFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;F)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$FloatSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setInt")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setIntFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;I)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$IntSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setLong")) {
+ isWideOperand = true;
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setLongFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;J)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$LongSetFieldInformationHolder;",
+ false);
+ } else if (name.equals("setShort")) {
+ mv.visitMethodInsn(INVOKESTATIC,
+ "de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter",
+ "setShortFieldReceiver",
+ "(Ljava/lang/reflect/Field;Ljava/lang/Object;S)Lde/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ShortSetFieldInformationHolder;",
+ false);
}
+
+ mv.visitInsn(DUP);
+
mv.visitLdcInsn(owner);
+ mv.visitInsn(SWAP);
mv.visitLdcInsn(name);
+ mv.visitInsn(SWAP);
mv.visitLdcInsn(desc);
+ mv.visitInsn(SWAP);
+
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BaseSetFieldInformationHolder",
+ "f",
+ "Ljava/lang/reflect/Field;");
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getName", "()Ljava/lang/String;", false);
+ mv.visitInsn(SWAP);
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BaseSetFieldInformationHolder",
+ "f",
+ "Ljava/lang/reflect/Field;");
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getDeclaringClass", "()Ljava/lang/Class;", false);
mv.visitMethodInsn(
INVOKESTATIC,
+ "org/objectweb/asm/Type",
+ "getInternalName",
+ "(Ljava/lang/Class;)Ljava/lang/String;",
+ false);
+ mv.visitInsn(SWAP);
+ if (isWideOperand) {
+ mv.visitInsn(ICONST_1);
+ } else {
+ mv.visitInsn(ICONST_0);
+ }
+ mv.visitInsn(SWAP);
+ mv.visitFieldInsn(GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BaseSetFieldInformationHolder",
+ "f",
+ "Ljava/lang/reflect/Field;");
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getModifiers", "()I", false);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
+ mv.visitMethodInsn(INVOKESTATIC,
config.getInstrumentationDispatcher(),
- getMethodNameByOpcode(opcode),
- d,
+ "SET_FIELD_REFLECTION",
+ "(Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;ZIJJ)V",
false);
+
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BaseSetFieldInformationHolder",
+ "f",
+ "Ljava/lang/reflect/Field;");
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitInsn(DUP);
+ mv.visitFieldInsn(GETFIELD,
+ "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BaseSetFieldInformationHolder",
+ "target",
+ "Ljava/lang/Object;");
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ if (name.equals("set")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ObjectSetFieldInformationHolder",
+ "member", "Ljava/lang/Object;");
+ } else if (name.equals("setBoolean")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$BooleanSetFieldInformationHolder",
+ "member", "Z");
+ } else if (name.equals("setByte")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ByteSetFieldInformationHolder",
+ "member", "B");
+ } else if (name.equals("setChar")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$CharSetFieldInformationHolder",
+ "member", "C");
+ } else if (name.equals("setDouble")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$DoubleSetFieldInformationHolder",
+ "member", "D");
+ } else if (name.equals("setFloat")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$FloatSetFieldInformationHolder",
+ "member", "F");
+ } else if (name.equals("setInt")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$IntSetFieldInformationHolder",
+ "member", "I");
+ } else if (name.equals("setLong")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$LongSetFieldInformationHolder",
+ "member", "J");
+ } else if (name.equals("setShort")) {
+ mv.visitFieldInsn(GETFIELD, "de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder$ShortSetFieldInformationHolder",
+ "member", "S");
+ }
+
+ // No invokevirtual with set and get reflection calls
+ // ToDo: Is there a nicer way which includes INVOKEVIRTUAL?
+ // addJpushInsn(mv, instrumentationState.incAndGetId());
+ // addJpushInsn(mv, invokeId);
+ // mv.visitLdcInsn(owner);
+ // mv.visitLdcInsn(name);
+ // mv.visitLdcInsn(desc);
+ // mv.visitMethodInsn(
+ // INVOKESTATIC,
+ // config.getInstrumentationDispatcher(),
+ // "INVOKEVIRTUAL",
+ // "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V",
+ // false);
+ }
+
+ private void handleFieldGetFieldCall(String owner, String name, String desc, long invokeId) {
+ // Initial stack layout:
+ //
+ // Field
+ // Object (field holder)
+
+ mv.visitInsn(SWAP);
+ mv.visitInsn(DUP);
+
+ mv.visitLdcInsn(owner);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitLdcInsn(name);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+ mv.visitLdcInsn(desc);
+ mv.visitInsn(DUP_X1);
+ mv.visitInsn(POP);
+
+ mv.visitInsn(DUP);
+ mv.visitInsn(DUP);
+
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getName", "()Ljava/lang/String;", false);
+ mv.visitInsn(DUP_X2);
+ mv.visitInsn(POP);
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getDeclaringClass", "()Ljava/lang/Class;", false);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ "org/objectweb/asm/Type",
+ "getInternalName",
+ "(Ljava/lang/Class;)Ljava/lang/String;",
+ false);
+ mv.visitInsn(SWAP);
+ mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/reflect/Field", "getModifiers", "()I", false);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
+
+ mv.visitMethodInsn(INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "GET_FIELD_REFLECTION",
+ "(Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;IJJ)V",
+ false);
+
+ mv.visitInsn(SWAP);
+
+ // No invokevirtual with set and get reflection calls
+ // ToDo: Is there a nicer way which includes INVOKEVIRTUAL?
+ // addJpushInsn(mv, instrumentationState.incAndGetId());
+ // addJpushInsn(mv, invokeId);
+ // mv.visitLdcInsn(owner);
+ // mv.visitLdcInsn(name);
+ // mv.visitLdcInsn(desc);
+ // mv.visitMethodInsn(
+ // INVOKESTATIC,
+ // config.getInstrumentationDispatcher(),
+ // "INVOKEVIRTUAL",
+ // "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V",
+ // false);
+ }
+
+ private boolean isFieldSetFieldMethod(String method) {
+ return setFieldMethods.contains(method);
+ }
+
+ private boolean isFieldGetFieldMethod(String method) {
+ return getFieldMethods.contains(method);
+ }
+
+ private void addMethodWithTryCatch(
+ int opcode, String owner, String name, String desc, boolean itf) {
+
+ long invokeId = instrumentationState.incAndGetInvokeId();
+
+ TryCatchBlock tcb = new TryCatchBlock(new Label(),new Label(), new Label(), new Label(), null);
+ if (owner.equals("java/lang/reflect/Constructor") && name.equals("newInstance")) {
+ Utils.addTryCatchBlock(mv, true, tcb);
+ handleClassCreationByReflection(invokeId);
+ Utils.addTryCatchBlock(mv, false, tcb);
+ } else if (owner.equals("java/lang/reflect/Method") && name.equals("invoke")) {
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ Utils.addTryCatchBlock(mv, true, tcb);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ "UNPACK_INVOKE_PARAMETER",
+ "(J)V",
+ false);
+ handleMethodInvokeCall(invokeId, instrumentationState.incAndGetId());
+ Utils.addTryCatchBlock(mv, false, tcb);
+ } else if (owner.equals("java/lang/reflect/Field") && isFieldSetFieldMethod(name)) {
+ Utils.addTryCatchBlock(mv, true, tcb);
+ handleFieldSetFieldCall(owner, name, desc, invokeId);
+ Utils.addTryCatchBlock(mv, false, tcb);
+ } else if (owner.equals("java/lang/reflect/Field") && isFieldGetFieldMethod(name)) {
+ Utils.addTryCatchBlock(mv, true, tcb);
+ handleFieldGetFieldCall(owner, name, desc, invokeId);
+ Utils.addTryCatchBlock(mv, false, tcb);
+ } else {
+ String d = "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
+ addJpushInsn(mv, invokeId);
+ mv.visitLdcInsn(owner);
+ mv.visitLdcInsn(name);
+ mv.visitLdcInsn(desc);
+ mv.visitMethodInsn(
+ INVOKESTATIC,
+ config.getInstrumentationDispatcher(),
+ getMethodNameByOpcode(opcode),
+ d,
+ false);
+ }
// Wrap the method call in a try-catch block
- Label begin = new Label();
+ Label start = new Label();
Label handler = new Label();
Label end = new Label();
+ Label jumpTarget = new Label();
- tryCatchBlocks.addFirst(new TryCatchBlock(begin, handler, handler, null));
+ new TryCatchBlock(start, end, handler, jumpTarget, null).visit(mv);
+
+ mv.visitLabel(start);
- mv.visitLabel(begin);
mv.visitMethodInsn(opcode, owner, name, desc, itf);
- mv.visitJumpInsn(GOTO, end);
+ mv.visitLabel(end);
+ mv.visitJumpInsn(GOTO, jumpTarget);
mv.visitLabel(handler);
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
"INVOKEMETHOD_EXCEPTION",
- "()V",
+ "(JJ)V",
false);
mv.visitInsn(ATHROW);
- mv.visitLabel(end);
+ mv.visitLabel(jumpTarget);
+
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
"INVOKEMETHOD_END",
- "()V",
+ "(JJ)V",
false);
addValueReadInsn(mv, owner + ":" + name + ":" + desc, "GETVALUE_");
@@ -921,14 +1581,13 @@ private void addMethodWithTryCatch(
*/
@Override
public void visitInvokeDynamicInsn(String name, String desc, Handle bsm, Object... bsmArgs) {
- String d = "(ILjava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
+ String d = "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
// increment and pushes the instruction id to the stack using the mv
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- d = "(IILjava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
- // push the current method id to the stack using mv
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
+ long invokeId = instrumentationState.incAndGetInvokeId();
+ addJpushInsn(mv, invokeId);
+
// load the owner to the stack (param 1)
mv.visitLdcInsn(bsm.getOwner());
// load the name to the stack (param 2)
@@ -949,28 +1608,35 @@ public void visitInvokeDynamicInsn(String name, String desc, Handle bsm, Object.
Label begin = new Label();
Label handler = new Label();
Label end = new Label();
+ Label jumpTarget = new Label();
- tryCatchBlocks.addFirst(new TryCatchBlock(begin, handler, handler, null));
+ new TryCatchBlock(begin, end, handler, jumpTarget, null).visit(mv);
mv.visitLabel(begin); // for adding try catch?
mv.visitInvokeDynamicInsn(name, desc, bsm, bsmArgs); // calling the actual method
- mv.visitJumpInsn(GOTO, end); // still try catch
+ mv.visitLabel(end);
+ mv.visitJumpInsn(GOTO, jumpTarget); // still try catch
mv.visitLabel(handler);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
"INVOKEMETHOD_EXCEPTION",
- "()V",
+ "(JJ)V",
false);
mv.visitInsn(ATHROW);
- mv.visitLabel(end);
+ mv.visitLabel(jumpTarget);
+ // mv.visitLabel(end);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
"INVOKEMETHOD_END",
- "()V",
+ "(JJ)V",
false);
addValueReadInsn(mv, bsm.getOwner() + ":" + name + ":" + desc, "GETVALUE_");
@@ -1000,14 +1666,12 @@ public void visitMethodInsn(int opcode, String owner, String name, String desc,
// if (!desc.equals("()V") || true) {
addSpecialInsn(mv, 420);
- String d = "(ILjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
+ String d = "(JJLjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
// increment and pushes the instruction id to the stack using the mv
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- d = "(IILjava/lang/String;Ljava/lang/String;Ljava/lang/String;)V";
- // push the current method id to the stack using mv
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
+ long invokeId = instrumentationState.incAndGetInvokeId();
+ addJpushInsn(mv, invokeId);
mv.visitLdcInsn(owner);
mv.visitLdcInsn(name);
@@ -1021,11 +1685,13 @@ public void visitMethodInsn(int opcode, String owner, String name, String desc,
mv.visitMethodInsn(opcode, owner, name, desc, itf);
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+ addJpushInsn(mv, invokeId);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
"INVOKEMETHOD_END",
- "()V",
+ "(JJ)V",
false);
addValueReadInsn(mv, owner + ":" + name + ":" + desc, "GETVALUE_");
@@ -1043,8 +1709,6 @@ public void visitMethodInsn(int opcode, String owner, String name, String desc,
calledNew = false;
addValueReadInsn(mv, "Ljava/lang/Object;", "GETVALUE_");
}
- // throw new RuntimeException("I will never be called, because name== and thus
- // isInit is true " + name + ", " + isInit);
}
} else {
addMethodWithTryCatch(opcode, owner, name, desc, itf);
@@ -1053,52 +1717,56 @@ public void visitMethodInsn(int opcode, String owner, String name, String desc,
@Override
public void visitJumpInsn(int opcode, Label label) {
- int iid3;
- String desc = "(II)V";
- addBipushInsn(mv, iid3 = instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(III)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ long iid3;
+ String desc = "(JI)V";
+ addJpushInsn(mv, iid3 = instrumentationState.incAndGetId());
+
addBipushInsn(mv, System.identityHashCode(label)); // label.getOffset()
switch (opcode) {
case IFEQ:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFEQ", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFNE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFNE", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFLT:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFLT", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFGE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFGE", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFGT:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFGT", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFLE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFLE", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPEQ:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1109,6 +1777,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPNE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1119,6 +1788,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPLT:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1129,6 +1799,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPGE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1139,6 +1810,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPGT:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1149,6 +1821,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ICMPLE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1159,6 +1832,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ACMPEQ:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1169,6 +1843,7 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
case IF_ACMPNE:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1189,12 +1864,14 @@ public void visitJumpInsn(int opcode, Label label) {
mv.visitJumpInsn(opcode, label);
break;
case IFNULL:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC, config.getInstrumentationDispatcher(), "IFNULL", desc, false);
mv.visitJumpInsn(opcode, label);
addSpecialInsn(mv, 1); // for true path
break;
case IFNONNULL:
+ BranchCoverage.addBranch(iid3);
mv.visitMethodInsn(
INVOKESTATIC,
config.getInstrumentationDispatcher(),
@@ -1205,19 +1882,16 @@ public void visitJumpInsn(int opcode, Label label) {
addSpecialInsn(mv, 1); // for true path
break;
default:
- throw new RuntimeException("Unknown jump opcode " + opcode);
+ throw new InstrumentationException("Unknown jump opcode " + opcode);
}
}
@Override
public void visitLdcInsn(Object cst) {
- String desc = "(I";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(II";
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(J";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
mv.visitLdcInsn(cst);
if (cst instanceof Integer) {
mv.visitMethodInsn(
@@ -1269,12 +1943,8 @@ public void visitLdcInsn(Object cst) {
@Override
public void visitIincInsn(int var, int increment) {
- String desc = "(II)V";
- if (config.isInstrumentationInstructionIds()) {
- desc = "(IIII)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(JII)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
addBipushInsn(mv, var);
addBipushInsn(mv, increment);
mv.visitMethodInsn(
@@ -1284,14 +1954,12 @@ public void visitIincInsn(int var, int increment) {
@Override
public void visitTableSwitchInsn(int min, int max, Label dflt, Label... labels) {
- int iid3;
+ long iid3;
- String desc = "(IIII[I[I)V"; // Add an extra array for case values
- addBipushInsn(mv, iid3 = instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(IIIII[I[I)V"; // Adjust descriptor for the added array
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String desc = "(JIII[I[I)V"; // Add an extra array for case values
+ addJpushInsn(mv, iid3 = instrumentationState.incAndGetId());
+
+ BranchCoverage.addBranch(iid3);
addBipushInsn(mv, min);
addBipushInsn(mv, max);
addBipushInsn(mv, System.identityHashCode(dflt)); // label.getOffset()
@@ -1322,14 +1990,11 @@ public void visitTableSwitchInsn(int min, int max, Label dflt, Label... labels)
@Override
public void visitLookupSwitchInsn(Label dflt, int[] keys, Label[] labels) {
- int iid3;
+ long iid3;
+
+ String desc = "(JI[I[I)V";
+ addJpushInsn(mv, iid3 = instrumentationState.incAndGetId());
- String desc = "(II[I[I)V";
- addBipushInsn(mv, iid3 = instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- desc = "(III[I[I)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
addBipushInsn(mv, System.identityHashCode(dflt)); // label.getOffset()
addBipushInsn(mv, keys.length);
@@ -1361,12 +2026,9 @@ public void visitLookupSwitchInsn(Label dflt, int[] keys, Label[] labels) {
@Override
public void visitMultiANewArrayInsn(String desc, int dims) {
- String d = "(ILjava/lang/String;I)V";
- addBipushInsn(mv, instrumentationState.incAndGetId());
- if (config.isInstrumentationInstructionIds()) {
- d = "(IILjava/lang/String;I)V";
- addBipushInsn(mv, instrumentationState.getMid());
- }
+ String d = "(JLjava/lang/String;I)V";
+ addJpushInsn(mv, instrumentationState.incAndGetId());
+
mv.visitLdcInsn(desc);
addBipushInsn(mv, dims);
mv.visitMethodInsn(
@@ -1374,17 +2036,11 @@ public void visitMultiANewArrayInsn(String desc, int dims) {
mv.visitMultiANewArrayInsn(desc, dims);
addSpecialInsn(mv, 0); // for non-exceptional path
}
-
@Override
- public void visitMaxs(int maxStack, int maxLocals) {
- for (TryCatchBlock b : tryCatchBlocks) {
- b.visit(mv);
+ public void visitEnd() {
+ mv.visitEnd();
+ if(seenCode) {
+ GlobalStateForInstrumentation.instance.setActiveInstrumentation(false);
}
- super.visitMaxs(maxStack, maxLocals);
- }
-
- @Override
- public void visitTryCatchBlock(Label label, Label label1, Label label2, String s) {
- tryCatchBlocks.addLast(new TryCatchBlock(label, label1, label2, s));
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionTransformer.java
index 04f9f33..31ac218 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionTransformer.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionTransformer.java
@@ -1,30 +1,40 @@
package de.uzl.its.swat.instrument.instruction;
+import ch.qos.logback.classic.Logger;
import de.uzl.its.swat.common.ErrorHandler;
import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
import de.uzl.its.swat.instrument.InternalTransformerType;
import de.uzl.its.swat.instrument.SafeClassWriter;
import de.uzl.its.swat.instrument.Transformer;
+import java.io.*;
import java.lang.instrument.ClassFileTransformer;
import java.security.ProtectionDomain;
+import java.util.Arrays;
import lombok.Getter;
import org.objectweb.asm.ClassReader;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.ClassWriter;
-import org.slf4j.LoggerFactory;
+import org.objectweb.asm.util.CheckClassAdapter;
/**
* An agent provides an implementation of this interface in order to transform class files. The
* transformation occurs before the class is defined by the JVM.
*/
public class InstructionTransformer implements ClassFileTransformer {
- private static final org.slf4j.Logger logger =
- LoggerFactory.getLogger(InstructionTransformer.class);
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
- @Getter private static PrintBox printBox;
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + InstructionTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
public InstructionTransformer() {
- printBox = new PrintBox(60, "Transformer: " + "Instruction");
Transformer.getPrintBox()
.addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
}
@@ -53,34 +63,77 @@ public byte[] transform(
Class> classBeingRedefined,
ProtectionDomain d,
byte[] cbuf) {
-
- if (classBeingRedefined != null || !Transformer.shouldInstrument(cname)) return cbuf;
- printBox.addMsg("Class: " + cname);
- printBox.setContentPresent(true);
try {
+
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) return cbuf;
+ getPrintBox().addMsg("Class: " + cname);
+ getPrintBox().setContentPresent(true);
+
ClassReader cr = new ClassReader(cbuf);
ClassWriter cw =
new SafeClassWriter(
- cr, loader, ClassWriter.COMPUTE_FRAMES | ClassWriter.COMPUTE_MAXS);
- ClassVisitor cv = new InstructionClassAdapter(cw, cname);
+ cr, loader, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new InstructionClassAdapter(new CheckClassAdapter(cw, true), cname);
try {
cr.accept(cv, ClassReader.SKIP_FRAMES);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
} catch (Exception e) {
- logger.info("Error: " + e);
+ byte[] partlyTransformedClass = cw.toByteArray();
+ saveClass(partlyTransformedClass, cname);
+ logger.info("Error: " + e.getMessage());
+ for (StackTraceElement ste : Arrays.stream(e.getStackTrace()).toList()) {
+
+ logger.info("Error: " + ste.toString());
+ }
new ErrorHandler()
.handleException("[INSTRUCTION TRANSFORMER] Error while instrumenting", e);
}
Transformer.addInstrumentedClass(cname, InternalTransformerType.INSTRUCTION);
- // if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
return cw.toByteArray();
} catch (Exception e) {
new ErrorHandler()
.handleException("[INSTRUCTION TRANSFORMER] Error while instrumenting", e);
+ System.err.println("HALT!");
+ Runtime.getRuntime().halt(3742);
+ // new ErrorHandler()
+ // .handleException("[INSTRUCTION TRANSFORMER] Error while instrumenting", e);
}
+
Transformer.addInstrumentedClass(cname, InternalTransformerType.INSTRUCTION);
- // if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
return cbuf;
}
+
+ public void saveClass(byte[] transformedClass, String cname) throws Exception {
+ String fullPath =
+ Config.instance().getLoggingDirectory()
+ + "/"
+ + "instrumented"
+ + "/"
+ + cname.replace('.', '/')
+ + ".class";
+
+ try {
+ File file = new File(fullPath);
+ File parent = new File(file.getParent());
+ if (!parent.exists()) {
+ parent.mkdirs();
+ }
+
+ try (FileOutputStream out = new FileOutputStream(file)) {
+ out.write(transformedClass);
+ }
+ } catch (Exception e) {
+ new ErrorHandler().handleException(e);
+ }
+ }
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder.java
new file mode 100644
index 0000000..d1a0a62
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/MethodInvokeInformationHolder.java
@@ -0,0 +1,28 @@
+package de.uzl.its.swat.instrument.instruction;
+
+import java.lang.reflect.Method;
+
+public class MethodInvokeInformationHolder {
+ public String methodName;
+ public String methodDescriptor;
+ public String owner;
+
+ public Method methodObject;
+ public Object ownerObject;
+ public Object[] argObjects;
+
+ public MethodInvokeInformationHolder(
+ String methodName,
+ String methodDescriptor,
+ String owner,
+ Method methodObject,
+ Object ownerObject,
+ Object[] argObjects) {
+ this.methodName = methodName;
+ this.methodDescriptor = methodDescriptor;
+ this.owner = owner;
+ this.methodObject = methodObject;
+ this.ownerObject = ownerObject;
+ this.argObjects = argObjects;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder.java
new file mode 100644
index 0000000..b0ed4ce
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/SetFieldInformationHolder.java
@@ -0,0 +1,96 @@
+package de.uzl.its.swat.instrument.instruction;
+
+import java.lang.reflect.Field;
+
+public class SetFieldInformationHolder {
+ public static class BaseSetFieldInformationHolder {
+ public BaseSetFieldInformationHolder(Field f, Object target) {
+ this.f = f;
+ this.target = target;
+ }
+
+ public Field f;
+ public Object target;
+ }
+
+ public static class ObjectSetFieldInformationHolder extends BaseSetFieldInformationHolder{
+ public ObjectSetFieldInformationHolder(Field f, Object target, Object member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public Object member;
+ }
+
+ public static class BooleanSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public BooleanSetFieldInformationHolder(Field f, Object target, boolean member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public boolean member;
+ }
+
+ public static class ByteSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public ByteSetFieldInformationHolder(Field f, Object target, byte member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public byte member;
+ }
+
+ public static class CharSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public CharSetFieldInformationHolder(Field f, Object target, char member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public char member;
+ }
+
+ public static class DoubleSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public DoubleSetFieldInformationHolder(Field f, Object target, double member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public double member;
+ }
+
+ public static class FloatSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public FloatSetFieldInformationHolder(Field f, Object target, float member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public float member;
+ }
+
+ public static class IntSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public IntSetFieldInformationHolder(Field f, Object target, int member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public int member;
+ }
+
+ public static class LongSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public LongSetFieldInformationHolder(Field f, Object target, long member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public long member;
+ }
+
+ public static class ShortSetFieldInformationHolder extends BaseSetFieldInformationHolder {
+ public ShortSetFieldInformationHolder(Field f, Object target, long member) {
+ super(f, target);
+ this.member = member;
+ }
+
+ public long member;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheClassAdapter.java
new file mode 100644
index 0000000..0705c17
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheClassAdapter.java
@@ -0,0 +1,29 @@
+package de.uzl.its.swat.instrument.nocache;
+
+import de.uzl.its.swat.common.Util;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+
+class NoCacheClassAdapter extends ClassVisitor {
+ private final String cname;
+
+ public NoCacheClassAdapter(ClassVisitor classVisitor, String cname) {
+ super(Opcodes.ASM9, classVisitor);
+ this.cname = cname;
+ }
+
+ @Override
+ public MethodVisitor visitMethod(int access, String name, String descriptor,
+ String signature, String[] exceptions) {
+ MethodVisitor mv = super.visitMethod(access, name, descriptor, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ // Use our custom method visitor that extends LocalVariablesSorter.
+ return new NoCacheMethodAdapter(api, access, descriptor, mv);
+ }
+}
\ No newline at end of file
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java
new file mode 100644
index 0000000..aba06b8
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheMethodAdapter.java
@@ -0,0 +1,166 @@
+package de.uzl.its.swat.instrument.nocache;
+
+import de.uzl.its.swat.config.Config;
+import org.objectweb.asm.Label;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
+import org.objectweb.asm.commons.LocalVariablesSorter;
+
+
+class NoCacheMethodAdapter extends LocalVariablesSorter {
+ public NoCacheMethodAdapter(int api, int access, String descriptor, MethodVisitor mv) {
+ super(api, access, descriptor, mv);
+ }
+
+ // Replace LDC instructions that load a String constant with code that creates a new String.
+ @Override
+ public void visitLdcInsn(Object value) {
+ if (value instanceof String && Config.instance().isUseStringInterning()) {
+ // Generate: new java/lang/String; DUP; LDC "literal"; INVOKESPECIAL (Ljava/lang/String;)V
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/String");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitLdcInsn(value);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/String", "",
+ "(Ljava/lang/String;)V", false);
+ //NoCacheTransformer.getPrintBox()
+ // .addMsg("Replacing LDC with new String");
+ } else {
+ mv.visitLdcInsn(value);
+ }
+ }
+
+ // Intercept method calls to disable interning and caching.
+ @Override
+ public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) {
+ // Skip String.intern() calls.
+ if (opcode == Opcodes.INVOKEVIRTUAL &&
+ owner.equals("java/lang/String") &&
+ name.equals("intern") &&
+ descriptor.equals("()Ljava/lang/String;") &&
+ Config.instance().isUseStringInterning()) {
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Removing String.intern() call");
+ return;
+ }
+ // Replace Integer.valueOf(int) with new Integer(int)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Integer") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(I)Ljava/lang/Integer;")) {
+ int localVarIndex = newLocal(Type.INT_TYPE);
+ mv.visitVarInsn(Opcodes.ISTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Integer");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "", "(I)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Integer.valueOf with new Integer");
+ return;
+ }
+ // Replace Long.valueOf(long) with new Long(long)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Long") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(J)Ljava/lang/Long;")) {
+ int localVarIndex = newLocal(Type.LONG_TYPE);
+ mv.visitVarInsn(Opcodes.LSTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Long");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.LLOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Long", "", "(J)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Long.valueOf with new Long");
+ return;
+ }
+ // Replace Short.valueOf(short) with new Short(short)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Short") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(S)Ljava/lang/Short;")) {
+ int localVarIndex = newLocal(Type.INT_TYPE);
+ mv.visitVarInsn(Opcodes.ISTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Short");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Short", "", "(S)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Short.valueOf with new Short");
+ return;
+ }
+ // Replace Byte.valueOf(byte) with new Byte(byte)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Byte") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(B)Ljava/lang/Byte;")) {
+ int localVarIndex = newLocal(Type.INT_TYPE);
+ mv.visitVarInsn(Opcodes.ISTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Byte");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Byte", "", "(B)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Byte.valueOf with new Byte");
+ return;
+ }
+ // Replace Character.valueOf(char) with new Character(char)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Character") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(C)Ljava/lang/Character;")) {
+ int localVarIndex = newLocal(Type.INT_TYPE);
+ mv.visitVarInsn(Opcodes.ISTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Character");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "", "(C)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Character.valueOf with new Character");
+ return;
+ }
+ // Replace Boolean.valueOf(boolean) with new Boolean(boolean)
+ if (opcode == Opcodes.INVOKESTATIC &&
+ owner.equals("java/lang/Boolean") &&
+ name.equals("valueOf") &&
+ descriptor.equals("(Z)Ljava/lang/Boolean;")) {
+ int localVarIndex = newLocal(Type.INT_TYPE);
+ mv.visitVarInsn(Opcodes.ISTORE, localVarIndex);
+ mv.visitTypeInsn(Opcodes.NEW, "java/lang/Boolean");
+ mv.visitInsn(Opcodes.DUP);
+ mv.visitVarInsn(Opcodes.ILOAD, localVarIndex);
+ mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "", "(Z)V", false);
+ NoCacheTransformer.getPrintBox()
+ .addMsg("Replacing Boolean.valueOf with new Boolean");
+ return;
+ }
+ // For all other method calls, proceed normally.
+ mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
+ }
+
+ /*
+ // Instrument object reference comparisons (IF_ACMPEQ and IF_ACMPNE) to print a warning.
+ @Override
+ public void visitJumpInsn(int opcode, Label label) {
+ if (opcode == Opcodes.IF_ACMPEQ || opcode == Opcodes.IF_ACMPNE) {
+ // Dynamically allocate two local variables for the two object references.
+ int refLocal1 = newLocal(Type.getType("Ljava/lang/Object;"));
+ int refLocal2 = newLocal(Type.getType("Ljava/lang/Object;"));
+ // Store the two references.
+ mv.visitVarInsn(Opcodes.ASTORE, refLocal2);
+ mv.visitVarInsn(Opcodes.ASTORE, refLocal1);
+ // Load them back to pass to our helper.
+ mv.visitVarInsn(Opcodes.ALOAD, refLocal1);
+ mv.visitVarInsn(Opcodes.ALOAD, refLocal2);
+ mv.visitMethodInsn(Opcodes.INVOKESTATIC, "org/example/InstrumentationHelper", "checkEquality",
+ "(Ljava/lang/Object;Ljava/lang/Object;)Z", false);
+ if (opcode == Opcodes.IF_ACMPEQ) {
+ mv.visitJumpInsn(Opcodes.IFNE, label);
+ } else {
+ mv.visitJumpInsn(Opcodes.IFEQ, label);
+ }
+ } else {
+ mv.visitJumpInsn(opcode, label);
+ }
+ }
+ */
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheTransformer.java
new file mode 100644
index 0000000..7726440
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/nocache/NoCacheTransformer.java
@@ -0,0 +1,88 @@
+package de.uzl.its.swat.instrument.nocache;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
+import de.uzl.its.swat.instrument.Transformer;
+import lombok.Getter;
+import org.objectweb.asm.*;
+
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import java.util.Arrays;
+
+import org.objectweb.asm.util.CheckClassAdapter;
+
+public class NoCacheTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + NoCacheTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ public NoCacheTransformer() {
+
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ @Override
+ public byte[] transform(ClassLoader loader, String cname, Class> classBeingRedefined,
+ ProtectionDomain d, byte[] cbuf) {
+
+ try {
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) return cbuf;
+ getPrintBox().addMsg("Class: " + cname);
+ getPrintBox().setContentPresent(true);
+
+ ClassReader cr = new ClassReader(cbuf);
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new NoCacheClassAdapter(new CheckClassAdapter(cw, true), cname);
+ try {
+ cr.accept(cv, ClassReader.SKIP_FRAMES);
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+ } catch (Exception e) {
+ logger.info("Error: " + e.getMessage());
+ for (StackTraceElement ste : Arrays.stream(e.getStackTrace()).toList()) {
+
+ logger.info("Error: " + ste.toString());
+ }
+ new ErrorHandler()
+ .handleException("[NOCACHE TRANSFORMER] Error while instrumenting class: " + cname, e);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.REF_EQUALITY);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cw.toByteArray();
+
+ } catch (Exception e) {
+ new ErrorHandler()
+ .handleException("[NOCACHE TRANSFORMER] Error while instrumenting class: " + cname, e);
+ System.err.println("HALT!");
+ Runtime.getRuntime().halt(3742);
+ // new ErrorHandler()
+ // .handleException("[INSTRUCTION TRANSFORMER] Error while instrumenting", e);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.REF_EQUALITY);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cbuf;
+ }
+}
+
+
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterClassAdapter.java
index 42e5653..54ec478 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterClassAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterClassAdapter.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.instrument.parameter;
+import de.uzl.its.swat.common.Util;
import de.uzl.its.swat.config.Config;
import java.util.regex.Pattern;
import org.objectweb.asm.ClassVisitor;
@@ -13,19 +14,17 @@
* visitInnerClass | visitRecordComponent | visitField | visitMethod )* visitEnd.
*/
public class ParameterClassAdapter extends ClassVisitor {
-
- private final String cname;
private final Config config = Config.instance();
+ private final String cname;
/**
* Constructor that calls the super from the default ClassVisitor
*
* @param cv Parent ClassVisitor
- * @param className Name of the Class
*/
- public ParameterClassAdapter(ClassVisitor cv, String className) {
+ public ParameterClassAdapter(ClassVisitor cv, String cname) {
super(Opcodes.ASM9, cv);
- this.cname = className;
+ this.cname = cname;
}
/**
@@ -51,8 +50,14 @@ public MethodVisitor visitMethod(
MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
// Check if the name matches the pattern
- if (!Pattern.matches(config.getInstrumentationParameterSymbolicMethodName(), name))
+ if (!Util.isSymbolicMethod(cname, name))
return mv;
ParameterTransformer.getPrintBox().addMsg("Method: " + name);
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterMethodAdapter.java
index dcd5270..ba2cd09 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterMethodAdapter.java
@@ -34,6 +34,6 @@ public ParameterMethodAdapter(
*/
@Override
public void visitCode() {
- handleMethodParameters(access, ParameterTransformer.getPrintBox());
+ handleMethodParameters(access, ParameterTransformer.getPrintBox(), false);
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterTransformer.java
index bcab2db..f49aa24 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterTransformer.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/parameter/ParameterTransformer.java
@@ -1,11 +1,17 @@
package de.uzl.its.swat.instrument.parameter;
+import ch.qos.logback.classic.Logger;
import de.uzl.its.swat.common.ErrorHandler;
import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
import de.uzl.its.swat.config.Config;
import de.uzl.its.swat.instrument.InternalTransformerType;
import de.uzl.its.swat.instrument.SafeClassWriter;
import de.uzl.its.swat.instrument.Transformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
import java.lang.instrument.ClassFileTransformer;
import java.security.ProtectionDomain;
import java.util.regex.Pattern;
@@ -13,31 +19,35 @@
import org.objectweb.asm.ClassReader;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.ClassWriter;
-import org.slf4j.LoggerFactory;
+import org.objectweb.asm.util.CheckClassAdapter;
/**
* An agent provides an implementation of this interface in order to transform class files. The
* transformation occurs before the class is defined by the JVM.
*/
public class ParameterTransformer implements ClassFileTransformer {
- private static final org.slf4j.Logger logger =
- LoggerFactory.getLogger(ParameterTransformer.class);
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
Config config = Config.instance();
- @Getter private static PrintBox printBox;
+
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer: " + ParameterTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
public ParameterTransformer() {
- printBox = new PrintBox(60, "Transformer: " + "Parameter");
Transformer.getPrintBox()
.addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
Transformer.getPrintBox()
.addMsg(
" => Matching cname: "
- + config.getInstrumentationParameterSymbolicClassName());
+ + config.getInstrumentationParameterSymbolicClassNames().toString());
Transformer.getPrintBox()
.addMsg(
" => Matching method: "
+ Pattern.compile(
- config.getInstrumentationParameterSymbolicMethodName()));
+ config.getInstrumentationParameterSymbolicMethodNames().toString()));
}
/**
* The implementation of this method may transform the supplied class file and return a new
@@ -63,22 +73,29 @@ public byte[] transform(
ProtectionDomain d,
byte[] cbuf) {
- if (classBeingRedefined != null
- || !cname.equals(config.getInstrumentationParameterSymbolicClassName())) {
+ if (classBeingRedefined != null || cname == null
+ || !Util.isSymbolicClass(cname)) {
return cbuf;
}
- printBox.addMsg("Class: " + cname);
+ getPrintBox().addMsg("Class: " + cname);
try {
ClassReader cr = new ClassReader(cbuf);
- ClassWriter cw =
- new SafeClassWriter(
- cr, loader, ClassWriter.COMPUTE_FRAMES | ClassWriter.COMPUTE_MAXS);
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
+ // | ClassWriter.COMPUTE_MAXS
ClassVisitor cv = new ParameterClassAdapter(cw, cname);
cr.accept(cv, 0);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+
Transformer.addInstrumentedClass(cname, InternalTransformerType.PARAMETER);
- if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
return cw.toByteArray();
} catch (Exception e) {
@@ -86,7 +103,7 @@ public byte[] transform(
errorHandler.handleException("Error while instrumenting class: " + cname, e);
}
Transformer.addInstrumentedClass(cname, InternalTransformerType.PARAMETER);
- if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
return cbuf;
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityClassAdapter.java
new file mode 100644
index 0000000..039b260
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityClassAdapter.java
@@ -0,0 +1,29 @@
+package de.uzl.its.swat.instrument.refequality;
+
+import de.uzl.its.swat.common.Util;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+
+class RefEqualityClassAdapter extends ClassVisitor {
+ private final String cname;
+
+ public RefEqualityClassAdapter(ClassVisitor classVisitor, String cname) {
+ super(Opcodes.ASM9, classVisitor);
+ this.cname = cname;
+ }
+
+ @Override
+ public MethodVisitor visitMethod(int access, String name, String descriptor,
+ String signature, String[] exceptions) {
+ MethodVisitor mv = super.visitMethod(access, name, descriptor, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ // Use our custom method visitor that replaces reference equality checks.
+ return new RefEqualityMethodAdapter(api, access, descriptor, mv);
+ }
+}
\ No newline at end of file
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityMethodAdapter.java
new file mode 100644
index 0000000..46d99fb
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityMethodAdapter.java
@@ -0,0 +1,51 @@
+package de.uzl.its.swat.instrument.refequality;
+
+import org.objectweb.asm.Label;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
+import org.objectweb.asm.commons.LocalVariablesSorter;
+
+class RefEqualityMethodAdapter extends LocalVariablesSorter {
+
+ public RefEqualityMethodAdapter(int api, int access, String descriptor, MethodVisitor mv) {
+ super(api, access, descriptor, mv);
+ }
+
+ @Override
+ public void visitJumpInsn(int opcode, Label label) {
+ // Intercept IF_ACMPEQ and IF_ACMPNE (reference equality comparisons)
+ if (opcode == Opcodes.IF_ACMPEQ || opcode == Opcodes.IF_ACMPNE) {
+ // Stack at this point: [..., ref1, ref2]
+ // We can call Objects.equals directly without storing
+
+ // Call Objects.equals(Object, Object) which consumes both refs from stack
+ mv.visitMethodInsn(
+ Opcodes.INVOKESTATIC,
+ "de/uzl/its/swat/common/UtilInstrumented",
+ "refEquals",
+ "(Ljava/lang/Object;Ljava/lang/Object;)Z",
+ false
+ );
+
+ // Now stack has: [..., boolean result (0 or 1)]
+ // Convert the comparison based on original opcode
+ if (opcode == Opcodes.IF_ACMPEQ) {
+ // Original: if (ref1 == ref2) goto label
+ // New: if (Objects.equals(ref1, ref2) == true) goto label
+ mv.visitJumpInsn(Opcodes.IFNE, label); // If not equal to 0 (i.e., true), jump
+ } else { // IF_ACMPNE
+ // Original: if (ref1 != ref2) goto label
+ // New: if (Objects.equals(ref1, ref2) == false) goto label
+ mv.visitJumpInsn(Opcodes.IFEQ, label); // If equal to 0 (i.e., false), jump
+ }
+
+ RefEqualityTransformer.getPrintBox()
+ .addMsg("Replacing " + (opcode == Opcodes.IF_ACMPEQ ? "IF_ACMPEQ" : "IF_ACMPNE") +
+ " with UtilInstrumented.refEquals");
+ } else {
+ // For all other jump instructions, proceed normally
+ mv.visitJumpInsn(opcode, label);
+ }
+ }
+}
\ No newline at end of file
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityTransformer.java
new file mode 100644
index 0000000..c749857
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/refequality/RefEqualityTransformer.java
@@ -0,0 +1,86 @@
+package de.uzl.its.swat.instrument.refequality;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
+import de.uzl.its.swat.instrument.Transformer;
+import org.objectweb.asm.*;
+import org.objectweb.asm.util.CheckClassAdapter;
+
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import java.util.Arrays;
+
+public class RefEqualityTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(
+ () -> new PrintBox(60, "Transformer" + RefEqualityTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ public RefEqualityTransformer() {
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ @Override
+ public byte[] transform(ClassLoader loader, String cname, Class> classBeingRedefined,
+ ProtectionDomain d, byte[] cbuf) {
+
+ try {
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) return cbuf;
+
+ // Don't touch UtilInstrumented because it needs to contain reference equality checks
+ if(Util.isInstrumentedUtilClass(cname)) {
+ return cbuf;
+ }
+ getPrintBox().addMsg("Class: " + cname);
+ getPrintBox().setContentPresent(true);
+
+ ClassReader cr = new ClassReader(cbuf);
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new RefEqualityClassAdapter(new CheckClassAdapter(cw, true), cname);
+ try {
+ cr.accept(cv, ClassReader.SKIP_FRAMES);
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+ } catch (Exception e) {
+ logger.info("Error: " + e.getMessage());
+ for (StackTraceElement ste : Arrays.stream(e.getStackTrace()).toList()) {
+ logger.info("Error: " + ste.toString());
+ }
+ new ErrorHandler()
+ .handleException("[REFEQUALITY TRANSFORMER] Error while instrumenting class: " + cname, e);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.INSTRUCTION);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cw.toByteArray();
+
+ } catch (Exception e) {
+ new ErrorHandler()
+ .handleException("[REFEQUALITY TRANSFORMER] Error while instrumenting class: " + cname, e);
+ System.err.println("HALT!");
+ Runtime.getRuntime().halt(3742);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.INSTRUCTION);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cbuf;
+ }
+}
\ No newline at end of file
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/EndpointMappingMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/EndpointMappingMethodAdapter.java
new file mode 100644
index 0000000..466db78
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/EndpointMappingMethodAdapter.java
@@ -0,0 +1,60 @@
+package de.uzl.its.swat.instrument.springendpoint;
+
+import de.uzl.its.swat.instrument.AbstractMethodAdapter;
+import org.objectweb.asm.AnnotationVisitor;
+import org.objectweb.asm.MethodVisitor;
+
+/**
+ * A visitor to visit a Java method This class visits Spring RestEndpoints and makes all primitive
+ * Datatype parameters symbolic and marks Class objects for later instrumenting.
+ */
+public class EndpointMappingMethodAdapter extends AbstractMethodAdapter {
+
+ private boolean isRequestMapping;
+ private final boolean isInterfaceMapping;
+ private int access;
+ private final String cname;
+
+ /**
+ * Constructor that calls the super from the default MethodVisitor
+ *
+ * @param mv Parent MethodVisitor
+ * @param cname The class name
+ * @param name The method name
+ * @param desc A string description of the parameters of the method
+ */
+ public EndpointMappingMethodAdapter(
+ MethodVisitor mv,
+ int access,
+ String cname,
+ String name,
+ String desc,
+ boolean isInterfaceMapping) {
+ super(mv, name, desc);
+ this.isRequestMapping = false;
+ this.isInterfaceMapping = isInterfaceMapping;
+ this.access = access;
+ this.cname = cname;
+ }
+
+ @Override
+ public void visitCode() {
+ // instrument if either the method itself had @GetMapping/etc. or the interface did
+ if (isRequestMapping || isInterfaceMapping) {
+ handleMethodParameters(access, SpringEndpointTransformer.getPrintBox(), false);
+ SpringEndpointTransformer.addInstrumentedClass(cname);
+ SpringEndpointTransformer.addInstrumentedEndpoint(cname + ":" + this.getName());
+ }
+ super.visitCode();
+ }
+
+ @Override
+ public AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
+ // catch method-level annotations too
+ if (SpringEndpointTransformer.isRestEndpointAnnotation(descriptor)) {
+ isRequestMapping = true;
+ }
+ return super.visitAnnotation(descriptor, visible);
+ }
+
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointClassAdapter.java
new file mode 100644
index 0000000..29f89f3
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointClassAdapter.java
@@ -0,0 +1,66 @@
+package de.uzl.its.swat.instrument.springendpoint;
+
+import de.uzl.its.swat.common.Util;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+
+import java.util.Set;
+
+/**
+ * A visitor to visit a Java class. The methods of this class must be called in the following order:
+ * visit [ visitSource ] [ visitModule ][ visitNestHost ][ visitOuterClass ] ( visitAnnotation |
+ * visitTypeAnnotation | visitAttribute )* ( visitNestMember | [ * visitPermittedSubclass ] |
+ * visitInnerClass | visitRecordComponent | visitField | visitMethod )* visitEnd.
+ */
+public class SpringEndpointClassAdapter extends ClassVisitor {
+
+ private final String cname;
+ private final Set interfaceEndpoints;
+
+ /**
+ * Constructor that calls the super from the default ClassVisitor
+ *
+ * @param cv Parent ClassVisitor
+ */
+ public SpringEndpointClassAdapter(
+ ClassVisitor cv,
+ String cname,
+ Set interfaceEndpoints) {
+ super(Opcodes.ASM9, cv);
+ this.cname = cname;
+ this.interfaceEndpoints = interfaceEndpoints;
+ }
+
+ /**
+ * Visits a method of the class. This method must return a new MethodVisitor instance (or null)
+ * each time it is called, i.e., it should not return a previously returned visitor. Addition:
+ * Add a custom method visitor that instruments the parameters of all endpoint methods to make
+ * them symbolic.
+ *
+ * @param access the method's access flags (see Opcodes). This parameter also indicates if the
+ * method is synthetic and/or deprecated.
+ * @param name the method's name.
+ * @param desc the method's descriptor (see Type).
+ * @param signature the method's signature. May be null if the method parameters, return type
+ * and exceptions do not use generic types.
+ * @param exceptions the internal names of the method's exception classes (see
+ * Type.getInternalName()). May be null.
+ * @return an object to visit the byte code of the method, or null if this class visitor is not
+ * interested in visiting the code of this method.
+ */
+ @Override
+ public MethodVisitor visitMethod(
+ int access, String name, String desc, String signature, String[] exceptions) {
+ MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+ SpringEndpointTransformer.getPrintBox().addMsg("Method: " + name);
+
+ boolean fromInterface = interfaceEndpoints.contains(name + desc);
+ return new EndpointMappingMethodAdapter(mv, access, cname, name, desc, fromInterface);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointTransformer.java
new file mode 100644
index 0000000..8113e53
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springendpoint/SpringEndpointTransformer.java
@@ -0,0 +1,176 @@
+package de.uzl.its.swat.instrument.springendpoint;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
+import de.uzl.its.swat.instrument.Transformer;
+
+import java.io.InputStream;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import lombok.Getter;
+import org.objectweb.asm.ClassReader;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.ClassWriter;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.tree.AnnotationNode;
+import org.objectweb.asm.tree.ClassNode;
+import org.objectweb.asm.tree.MethodNode;
+import org.objectweb.asm.util.CheckClassAdapter;
+
+/**
+ * An agent provides an implementation of this interface in order to transform class files. The
+ * transformation occurs before the class is defined by the JVM.
+ */
+public class SpringEndpointTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + SpringEndpointTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ @Getter private static HashSet instrumentedClasses = new HashSet<>();
+ @Getter private static HashSet instrumentedEndpoints = new HashSet<>();
+
+ public SpringEndpointTransformer() {
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ }
+
+ static boolean isRestEndpointAnnotation(String desc) {
+ return desc.equals("Lorg/springframework/web/bind/annotation/RequestMapping;")
+ || desc.equals("Lorg/springframework/web/bind/annotation/PostMapping;")
+ || desc.equals("Lorg/springframework/web/bind/annotation/DeleteMapping;")
+ || desc.equals("Lorg/springframework/web/bind/annotation/GetMapping;")
+ || desc.equals("Lorg/springframework/web/bind/annotation/PutMapping;");
+ }
+
+
+ /**
+ * The implementation of this method may transform the supplied class file and return a new
+ * replacement class file. Addition: Adds the SpringEndpointClassAdapter for modifying the
+ * classFile
+ *
+ * @param loader the defining loader of the class to be transformed, may be null if the
+ * bootstrap loader
+ * @param cname the name of the class in the internal form of fully qualified class and
+ * interface names as defined in The Java Virtual Machine Specification. For example,
+ * "java/util/List".
+ * @param classBeingRedefined if this is triggered by a redefine or retransform, the class being
+ * redefined or retransformed; if this is a class load, null
+ * @param d the protection domain of the class being defined or redefined
+ * @param cbuf the input byte buffer in class file format - must not be modified
+ * @return a well-formed class file buffer (the result of the transform), or null if no
+ * transform is performed.
+ */
+ @Override
+ public byte[] transform(
+ ClassLoader loader,
+ String cname,
+ Class> classBeingRedefined,
+ ProtectionDomain d,
+ byte[] cbuf) {
+
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
+ return cbuf;
+ }
+ getPrintBox().addMsg("Class: " + cname);
+
+ try {
+ // parse the class
+ ClassReader cr = new ClassReader(cbuf);
+ ClassNode cn = new ClassNode(Opcodes.ASM9);
+ cr.accept(cn, 0);
+
+ // only controllers
+ boolean restController = false;
+ if (cn.visibleAnnotations != null) {
+ for (AnnotationNode an : cn.visibleAnnotations) {
+ if (an.desc.contains("Controller")) {
+ restController = true;
+ break;
+ }
+ }
+ }
+ if (!restController) {
+ return cbuf;
+ }
+
+
+ // 1) scan interfaces for mapping annotations
+ Set interfaceEndpoints = new HashSet<>();
+ for (String iface : cn.interfaces) {
+ // iface is in internal form, e.g. "org/springframework/samples/…/OwnersApi"
+ try (InputStream in = loader.getResourceAsStream(iface + ".class")) {
+ if (in == null) continue;
+ ClassReader icr = new ClassReader(in);
+ ClassNode icn = new ClassNode(Opcodes.ASM9);
+ // skip code, we only need annotations
+ icr.accept(icn, ClassReader.SKIP_CODE | ClassReader.SKIP_FRAMES);
+ for (MethodNode mn : icn.methods) {
+ if (mn.visibleAnnotations != null) {
+ for (AnnotationNode an : mn.visibleAnnotations) {
+ if (isRestEndpointAnnotation(an.desc)) {
+ interfaceEndpoints.add(mn.name + mn.desc);
+ break;
+ }
+ }
+ }
+ }
+ } catch (Exception ignored) {
+ // If the interface class cannot be found, we ignore it/ throw an assertion error.
+ // This can happen if the interface is not in the classpath or is not a valid class file.
+ SWATAssert.check(false, "Could not read interface {}: {}", iface, ignored.getMessage());
+ }
+ }
+
+
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
+
+ ClassVisitor cv = new SpringEndpointClassAdapter(cw, cname, interfaceEndpoints);
+ cr.accept(cv, 0);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_ENDPOINT);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cw.toByteArray();
+
+ } catch (Exception e) {
+ ErrorHandler errorHandler = new ErrorHandler();
+ errorHandler.handleException("Error while instrumenting class: " + cname, e);
+ }
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_ENDPOINT);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+
+ return cbuf;
+ }
+
+ public static void addInstrumentedEndpoint(String name) {
+ instrumentedEndpoints.add(name);
+ }
+
+ public static void addInstrumentedClass(String cname) {
+ instrumentedClasses.add(cname);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionClassAdapter.java
new file mode 100644
index 0000000..f93e47d
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionClassAdapter.java
@@ -0,0 +1,89 @@
+package de.uzl.its.swat.instrument.springexception;
+
+import java.util.HashMap;
+import java.util.HashSet;
+
+import de.uzl.its.swat.common.Util;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+
+/**
+ * A visitor to visit a Java class. The methods of this class must be called in the following order:
+ * visit [ visitSource ] [ visitModule ][ visitNestHost ][ visitOuterClass ] ( visitAnnotation |
+ * visitTypeAnnotation | visitAttribute )* ( visitNestMember | [ * visitPermittedSubclass ] |
+ * visitInnerClass | visitRecordComponent | visitField | visitMethod )* visitEnd.
+ */
+public class SpringExceptionClassAdapter extends ClassVisitor {
+
+ private String cname;
+ // HashMap> interfaceMap;
+
+ /**
+ * Constructor that calls the super from the default ClassVisitor
+ *
+ * @param cv Parent ClassVisitor
+ * @param interfaceMap
+ */
+ public SpringExceptionClassAdapter(
+ ClassVisitor cv, String cname, HashMap> interfaceMap) {
+ super(Opcodes.ASM9, cv);
+ this.cname = cname;
+ // this.interfaceMap = interfaceMap;
+ }
+
+ /* @Override
+ public void visit(int version, int access, String name, String signature, String superName, String[] interfaces) {
+
+ if (!interfaceMap.containsKey(this.cname)){
+ interfaceMap.put(this.cname, new HashSet<>(List.of(interfaces)));
+ } else {
+ interfaceMap.get(this.cname).addAll(List.of(interfaces));
+ }
+
+ if (interfaceMap.containsKey(superName)) {
+ interfaceMap.get(this.cname).addAll(interfaceMap.get(superName));
+ }
+
+ if (cname.equals("org/springframework/boot/autoconfigure/web/servlet/error/BasicErrorController")
+ || cname.equals("org/springframework/boot/autoconfigure/web/servlet/error/AbstractErrorController")) {
+ System.out.println("!!!!!!!! " + name);
+ System.out.println("!!!!!!!! " + superName);
+ for (String s : interfaceMap.get(this.cname)) {
+ System.out.println("!!!!!!!! " + s);
+ }
+ }
+ super.visit(version, access, name, signature, superName, interfaces);
+ } */
+
+ /**
+ * Visits a method of the class. This method must return a new MethodVisitor instance (or null)
+ * each time it is called, i.e., it should not return a previously returned visitor. Addition:
+ * Add a custom method visitor that instruments the parameters of all endpoint methods to make
+ * them symbolic.
+ *
+ * @param access the method's access flags (see Opcodes). This parameter also indicates if the
+ * method is synthetic and/or deprecated.
+ * @param name the method's name.
+ * @param desc the method's descriptor (see Type).
+ * @param signature the method's signature. May be null if the method parameters, return type
+ * and exceptions do not use generic types.
+ * @param exceptions the internal names of the method's exception classes (see
+ * Type.getInternalName()). May be null.
+ * @return an object to visit the byte code of the method, or null if this class visitor is not
+ * interested in visiting the code of this method.
+ */
+ @Override
+ public MethodVisitor visitMethod(
+ int access, String name, String desc, String signature, String[] exceptions) {
+
+ MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
+ return new SpringExceptionMethodAdapter(mv, access, name, desc, this.cname);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionMethodAdapter.java
new file mode 100644
index 0000000..d9d02b1
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionMethodAdapter.java
@@ -0,0 +1,143 @@
+package de.uzl.its.swat.instrument.springexception;
+
+import de.uzl.its.swat.instrument.AbstractMethodAdapter;
+import de.uzl.its.swat.instrument.Intrinsics;
+import org.objectweb.asm.AnnotationVisitor;
+import org.objectweb.asm.MethodVisitor;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
+
+/**
+ * A visitor to visit a Java method This class visits Spring RestEndpoints and makes all primitive
+ * Datatype parameters symbolic and marks Class objects for later instrumenting.
+ */
+public class SpringExceptionMethodAdapter extends AbstractMethodAdapter implements Opcodes {
+
+ private boolean isExceptionHandler;
+ private boolean isRequestMapping;
+ private final String methodName;
+ private final String cname;
+
+ /**
+ * Constructor that calls the super from the default MethodVisitor
+ *
+ * @param mv Parent MethodVisitor
+ * @param name The method name
+ * @param desc A string description of the parameters of the method
+ */
+ public SpringExceptionMethodAdapter(
+ MethodVisitor mv, int access, String name, String desc, String cname) {
+ super(mv, name, desc);
+ this.isExceptionHandler = false;
+ this.cname = cname;
+ this.methodName = name;
+ }
+
+ @Override
+ public void visitInsn(int opcode) {
+ // if (cname.equals("org/springframework/boot/web/servlet/support/ErrorPageFilter")) {
+ // System.out.println("@@@@@@@@@@@@@ " + cname + ":" + methodName);
+ // }
+ if (isExceptionHandler
+ || isErrorPageFilterForwardToErrorPage()
+ || isRequestMappingInErrorController()
+ || isAuthenticationFailureHandlerOnAuthenticationFailure()) {
+ if (opcode == IRETURN
+ || opcode == LRETURN
+ || opcode == FRETURN
+ || opcode == DRETURN
+ || opcode == ARETURN
+ || opcode == RETURN) {
+ SpringExceptionTransformer.getPrintBox()
+ .addMsg(
+ "("
+ + this.cname
+ + "."
+ + this.methodName
+ + ")"
+ + " => Adding termination: Intrinsics.terminate()");
+ visitMethodInsn(
+ Opcodes.INVOKESTATIC, Type.getInternalName(Intrinsics.class), "terminate", "()V", false);
+ mv.visitInsn(opcode);
+ } else {
+ mv.visitInsn(opcode);
+ }
+ } else {
+ mv.visitInsn(opcode);
+ }
+ }
+
+ // ToDo: This is an oversimplification. An application might create it's own
+ // AuthenticationFailureHandler and implement
+ // error handling methods. This however requires tracing interface back up the inheritance
+ // structure ...
+ private boolean isAuthenticationFailureHandlerOnAuthenticationFailure() {
+ return this.cname.startsWith("org/springframework/security/web/authentication")
+ && this.methodName.equals("onAuthenticationFailure");
+ }
+
+ // ToDo: This is an oversimplification. An application might create it's own ErrorController and
+ // implement
+ // error handling methods. This however requires tracing interface back up the inheritance
+ // structure ...
+ // ToDo: There seems to be a standard defining at least a bit about default error pages for
+ // servlets
+ // look into it and see whether this can be handled framework agnositc
+ private boolean isRequestMappingInErrorController() {
+ return isRequestMapping
+ && cname.equals(
+ "org/springframework/boot/autoconfigure/web/servlet/error/BasicErrorController");
+ }
+
+ private boolean isErrorPageFilterForwardToErrorPage() {
+ return this.cname.equals("org/springframework/boot/web/servlet/support/ErrorPageFilter")
+ && this.methodName.equals("forwardToErrorPage");
+ }
+
+ /**
+ * Visits annotation of this method. Checks if it is a REST endpoint
+ *
+ * @param descriptor the class descriptor of the annotation class.
+ * @param visible true if the annotation is visible at runtime.
+ * @return a visitor to visit the annotation values, or null if this visitor is not interested
+ * in visiting this annotation.
+ */
+ @Override
+ public AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
+ // if (descriptor.contains("Exception")) {
+ // System.out.println("YYYYUUUU" + descriptor);
+ // }
+ if (isExceptionHandler(descriptor)) {
+ isExceptionHandler = true;
+ }
+ if (isRequestMapping(descriptor)) {
+ isRequestMapping = true;
+ }
+
+ return super.visitAnnotation(descriptor, visible);
+ }
+
+ private boolean isRequestMapping(String annotation) {
+ String[] requestMappingAnnotations = {
+ "Lorg/springframework/web/bind/annotation/RequestMapping;"
+ };
+ for (String requestMappingAnnotation : requestMappingAnnotations) {
+ if (annotation.equals(requestMappingAnnotation)) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public boolean isExceptionHandler(String annotation) {
+ String[] exceptionAnnotations = {
+ "Lorg/springframework/web/bind/annotation/ExceptionHandler;"
+ };
+ for (String endpointAnnotation : exceptionAnnotations) {
+ if (annotation.equals(endpointAnnotation)) {
+ return true;
+ }
+ }
+ return false;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionTransformer.java
new file mode 100644
index 0000000..32e0cd9
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/springexception/SpringExceptionTransformer.java
@@ -0,0 +1,131 @@
+package de.uzl.its.swat.instrument.springexception;
+
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.Transformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.lang.instrument.ClassFileTransformer;
+import java.security.ProtectionDomain;
+import java.util.HashMap;
+import java.util.HashSet;
+import lombok.Getter;
+import org.objectweb.asm.ClassReader;
+import org.objectweb.asm.ClassVisitor;
+import org.objectweb.asm.ClassWriter;
+import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.tree.ClassNode;
+import org.objectweb.asm.util.CheckClassAdapter;
+
+/**
+ * An agent provides an implementation of this interface in order to transform class files. The
+ * transformation occurs before the class is defined by the JVM.
+ */
+public class SpringExceptionTransformer implements ClassFileTransformer {
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
+
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + SpringExceptionTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ private HashMap> interfaces;
+
+ public SpringExceptionTransformer() {
+ Transformer.getPrintBox()
+ .addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
+ interfaces = new HashMap<>();
+ }
+
+ private boolean shouldInstrument(String cname) {
+ return (Util.shouldInstrument(cname)
+ || cname.equals(
+ "org/springframework/web/servlet/mvc/method/annotation/ResponseEntityExceptionHandler")
+ || cname.equals(
+ "org/springframework/boot/autoconfigure/web/servlet/error/BasicErrorController")
+ || cname.equals(
+ "org/springframework/boot/autoconfigure/web/servlet/error/AbstractErrorController")
+ || cname.equals("org/springframework/boot/web/servlet/support/ErrorPageFilter"));
+ // || cname.startsWith("org/springframework/security/web/authentication"));
+ }
+
+ /**
+ * The implementation of this method may transform the supplied class file and return a new
+ * replacement class file. Addition: Adds the SpringEndpointClassAdapter for modifying the
+ * classFile
+ *
+ * @param loader the defining loader of the class to be transformed, may be null if the
+ * bootstrap loader
+ * @param cname the name of the class in the internal form of fully qualified class and
+ * interface names as defined in The Java Virtual Machine Specification. For example,
+ * "java/util/List".
+ * @param classBeingRedefined if this is triggered by a redefine or retransform, the class being
+ * redefined or retransformed; if this is a class load, null
+ * @param d the protection domain of the class being defined or redefined
+ * @param cbuf the input byte buffer in class file format - must not be modified
+ * @return a well-formed class file buffer (the result of the transform), or null if no
+ * transform is performed.
+ */
+ @Override
+ public byte[] transform(
+ ClassLoader loader,
+ String cname,
+ Class> classBeingRedefined,
+ ProtectionDomain d,
+ byte[] cbuf) {
+
+ // System.out.println("!!!!!!!!!!!!! " + cname);
+
+ if (classBeingRedefined != null || cname == null || !shouldInstrument(cname)) { // TODO only temporary
+ return cbuf;
+ }
+ getPrintBox().addMsg("Class: " + cname);
+
+ try {
+ ClassReader cr = new ClassReader(cbuf);
+ ClassNode cn = new ClassNode(Opcodes.ASM9);
+ cr.accept(cn, 0);
+ // List visibleAnnotations = cn.visibleAnnotations;
+ // boolean restController = false;
+ // if (visibleAnnotations != null) {
+ // for (AnnotationNode an : visibleAnnotations) {
+ // restController = restController || an.desc.contains("Controller");
+ // }
+ // }
+ // if (!restController) {
+ // return cbuf;
+ // }
+ ClassWriter cw = new ClassWriter(cr, 0); // For some reason changing this to 0 from
+ // ClassWriter.COMPUTE_FRAMES helps??
+ ClassVisitor cv = new SpringExceptionClassAdapter(cw, cname, interfaces);
+ cr.accept(cv, 0);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_EXCEPTION);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+ return cw.toByteArray();
+
+ } catch (Exception e) {
+ ErrorHandler errorHandler = new ErrorHandler();
+ errorHandler.handleException("Error while instrumenting class: " + cname, e);
+ }
+ Transformer.addInstrumentedClass(cname, InternalTransformerType.SPRING_EXCEPTION);
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
+
+ return cbuf;
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
index 8f6beaa..8ed6911 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.instrument.svcomp;
+import de.uzl.its.swat.common.Util;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
@@ -19,7 +20,7 @@ public class SVCompClassAdapter extends ClassVisitor {
*
* @param cv Parent ClassVisitor
*/
- public SVCompClassAdapter(String cname, ClassVisitor cv) {
+ public SVCompClassAdapter(ClassVisitor cv, String cname) {
super(Opcodes.ASM9, cv);
this.cname = cname;
}
@@ -46,6 +47,12 @@ public MethodVisitor visitMethod(
int access, String name, String desc, String signature, String[] exceptions) {
MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
if (!cname.equals("org/sosy_lab/sv_benchmarks/Verifier")) {
SVCompTransformer.getPrintBox().addMsg("Method: " + name);
return new SVCompMethodAdapter(access, mv, cname, name, desc);
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
index 8b8d1e0..df2a387 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
@@ -1,10 +1,12 @@
package de.uzl.its.swat.instrument.svcomp;
import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.Intrinsics;
import de.uzl.its.swat.instrument.Transformer;
import org.objectweb.asm.Label;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
import org.objectweb.asm.commons.LocalVariablesSorter;
/** A visitor to visit a Java method */
@@ -45,7 +47,9 @@ public void visitMethodInsn(
final String name,
final String descriptor,
final boolean isInterface) {
- if (name.startsWith("nondet") && owner.equals("org/sosy_lab/sv_benchmarks/Verifier")) {
+ // The weird concatenation is needed to avoid the relocation from the ShadowJar plugin to move this owner
+ String targetOwner = "org/".concat("sosy_lab/sv_benchmarks/Verifier");
+ if (name.startsWith("nondet") && owner.equals(targetOwner)) {
Transformer.addInstrumentedClass(cname, InternalTransformerType.SV_COMP);
String newOwner = "de/uzl/its/swat/instrument/svcomp/Verifier";
// Add one long argument into the desc (will be the only argument) old : ()X where x is
@@ -86,16 +90,41 @@ public void visitMethodInsn(
*/
visitMethodInsn(
Opcodes.INVOKESTATIC,
- "de/uzl/its/swat/Main",
- "MakeSymbolic",
+ Type.getInternalName(Intrinsics.class),
+ "liftValue",
"(" + retType + "J" + ")" + retType,
false);
SVCompTransformer.getPrintBox().addMsg(" => Adding symbolic tracking");
} else if (name.equals("assume")) {
String newOwner = "de/uzl/its/swat/instrument/svcomp/Verifier";
mv.visitMethodInsn(opcode, newOwner, name, descriptor, isInterface);
+ } else if (owner.equals("java/net/Socket")) {
+ String newOwner = "de/uzl/its/swat/instrument/svcomp/Socket";
+ mv.visitMethodInsn(opcode, newOwner, name, descriptor, isInterface);
} else {
mv.visitMethodInsn(opcode, owner, name, descriptor, isInterface);
}
}
+
+ @Override
+ public void visitTypeInsn(int opcode, String type) {
+ // Replace the type for `new java.net.Socket` with the mock type
+ if (opcode == Opcodes.NEW && type.equals("java/net/Socket")) {
+ String newType = "de/uzl/its/swat/instrument/svcomp/Socket";
+ super.visitTypeInsn(opcode, newType);
+ } else {
+ super.visitTypeInsn(opcode, type);
+ }
+ }
+
+ @Override
+ public void visitFieldInsn(int opcode, String owner, String name, String descriptor) {
+ // Redirect static field references or any field accesses from `java.net.Socket` to the mock
+ if (owner.equals("java/net/Socket")) {
+ String newOwner = "de/uzl/its/swat/instrument/svcomp/Socket";
+ super.visitFieldInsn(opcode, newOwner, name, descriptor);
+ } else {
+ super.visitFieldInsn(opcode, owner, name, descriptor);
+ }
+ }
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompTransformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompTransformer.java
index 80f47f0..c739242 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompTransformer.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompTransformer.java
@@ -1,18 +1,25 @@
package de.uzl.its.swat.instrument.svcomp;
+import ch.qos.logback.classic.Logger;
import de.uzl.its.swat.common.ErrorHandler;
import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.config.Config;
import de.uzl.its.swat.instrument.InternalTransformerType;
+import de.uzl.its.swat.instrument.SafeClassWriter;
import de.uzl.its.swat.instrument.Transformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
import java.lang.instrument.ClassFileTransformer;
import java.security.ProtectionDomain;
+
import lombok.Getter;
import org.objectweb.asm.ClassReader;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.ClassWriter;
-import org.objectweb.asm.Opcodes;
-import org.objectweb.asm.tree.ClassNode;
-import org.slf4j.LoggerFactory;
+import org.objectweb.asm.util.CheckClassAdapter;
/**
* An agent provides an implementation of this interface in order to transform class files. The
@@ -20,13 +27,16 @@
*/
public class SVCompTransformer implements ClassFileTransformer {
- @Getter private static PrintBox printBox;
- @Getter
- private static final org.slf4j.Logger logger = LoggerFactory.getLogger(SVCompTransformer.class);
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + SVCompTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ @Getter private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
public SVCompTransformer() {
- printBox = new PrintBox(60, "Transformer: " + "SV-Comp");
Transformer.getPrintBox()
.addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
}
@@ -56,18 +66,25 @@ public byte[] transform(
ProtectionDomain d,
byte[] cbuf) {
- if (classBeingRedefined != null || !Transformer.shouldInstrument(cname)) return cbuf;
- printBox.addMsg("Class: " + cname);
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) return cbuf;
+ getPrintBox().addMsg("Class: " + cname);
+ getPrintBox().setContentPresent(true);
try {
ClassReader cr = new ClassReader(cbuf);
- ClassNode cn = new ClassNode(Opcodes.ASM9);
- cr.accept(cn, ClassReader.EXPAND_FRAMES);
+ ClassWriter cw =
+ new SafeClassWriter(
+ cr, loader, ClassWriter.COMPUTE_FRAMES);
+ ClassVisitor cv = new SVCompClassAdapter(new CheckClassAdapter(cw, true), cname);
+ cr.accept(cv, ClassReader.SKIP_FRAMES);
- ClassWriter cw = new ClassWriter(cr, ClassReader.EXPAND_FRAMES);
- ClassVisitor cv = new SVCompClassAdapter(cname, cw);
- cr.accept(cv, ClassReader.EXPAND_FRAMES);
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
- if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.info(getPrintBox().toString());
return cw.toByteArray();
} catch (Exception e) {
@@ -75,7 +92,7 @@ public byte[] transform(
errorHandler.handleException("Error while instrumenting class: " + cname, e);
}
Transformer.addInstrumentedClass(cname, InternalTransformerType.SV_COMP);
- if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.info(getPrintBox().toString());
return cbuf;
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Socket.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Socket.java
new file mode 100644
index 0000000..92ef18e
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Socket.java
@@ -0,0 +1,31 @@
+package de.uzl.its.swat.instrument.svcomp;
+
+import java.io.InputStream;
+
+public class Socket {
+ public Socket() {
+ // create a new socket
+ System.out.println("Creating mock socket...");
+ }
+ public Socket(String host, int port) {
+ // create a new socket
+ System.out.println("Creating mock socket to " + host + ":" + port + "...");
+ }
+ public InputStream getInputStream() {
+ // return the input stream
+ System.out.println("Getting input stream from mock socket...");
+ return new InputStream() {
+ @Override
+ public int read() {
+ // read from the input stream
+ System.out.println("Reading from mock input stream...");
+ return 0;
+ }
+ };
+ }
+ public void close() {
+ // close the socket
+ System.out.println("Closing mock socket...");
+ }
+
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Verifier.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Verifier.java
index b5a8090..56c7ac4 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Verifier.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/Verifier.java
@@ -1,27 +1,29 @@
package de.uzl.its.swat.instrument.svcomp;
-import de.uzl.its.swat.Main;
+import ch.qos.logback.classic.Logger;
+import de.uzl.its.swat.common.ErrorHandler;
import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.logging.GlobalLogger;
import de.uzl.its.swat.config.Config;
import java.util.*;
+
+import de.uzl.its.swat.instrument.Intrinsics;
+import de.uzl.its.swat.symbolic.invoke.InternalInvocation;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.*;
+import de.uzl.its.swat.symbolic.value.reference.lang.StringValue;
+import de.uzl.its.swat.thread.ThreadContext;
+import de.uzl.its.swat.thread.ThreadHandler;
import lombok.Getter;
import lombok.Setter;
-import org.slf4j.LoggerFactory;
+import static java.lang.Thread.currentThread;
+@SuppressWarnings("removal")
public class Verifier {
private static long nextId = 0;
- private static final String prefixBoolean = "Z_";
- private static final String prefixChar = "C_";
- private static final String prefixByte = "B_";
- private static final String prefixShort = "S_";
- private static final String prefixInt = "I_";
- private static final String prefixFloat = "F_";
- private static final String prefixLong = "L_";
- private static final String prefixDouble = "D_";
- private static final String prefixString = "Ljava/lang/String_";
- private static final org.slf4j.Logger logger = LoggerFactory.getLogger(Verifier.class);
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
private static final Config config;
-
static {
config = Config.instance();
}
@@ -50,7 +52,7 @@ public static void retrieveInputs() {
printBox.addMsg(
"Input with name: "
+ key.toString().replace("swat.input.", "")
- + " and value: "
+ + " and (encoded) value: "
+ value
+ " registered");
}
@@ -59,7 +61,6 @@ public static void retrieveInputs() {
}
public static void assume(boolean condition) {
- PrintBox printBox = new PrintBox(60);
logger.info(
new PrintBox(
60,
@@ -67,228 +68,378 @@ public static void assume(boolean condition) {
new ArrayList<>(List.of("Assuming condition: " + condition)))
.toString());
if (!condition) {
- Main.terminate();
+ Intrinsics.terminate();
Runtime.getRuntime().halt(0);
}
}
+ @SuppressWarnings("removal")
public static boolean nondetBoolean(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetDouble");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixBoolean + id) && !inputs.get(prefixBoolean + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- boolean b = Boolean.parseBoolean(inputs.get(prefixBoolean + id).remove());
- printBox.addMsg("Returning: " + b);
- logger.info(printBox.toString());
- return b;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetBoolean");
+ String prefix = BooleanValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetBoolean with the same name: {}. Assigning new idx: {}", requestedName, newId);
- } else {
- boolean rnd =
- config.isSvcompRandomInputs()
- ? (new Random()).nextBoolean()
- : Boolean.valueOf(false);
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ boolean b = Boolean.parseBoolean(inputs.get(prefix + newId).remove());
+ printBox.addMsg("Returning: " + b);
+ logger.info(printBox.toString());
+ return b;
+
+ } else {
+ boolean rnd =
+ config.isSvcompRandomInputs()
+ ? (new Random()).nextBoolean()
+ : Boolean.valueOf(false);
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Boolean(rnd); // Needed to prevent intering
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return false;
}
}
+
public static byte nondetByte(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetByte");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixByte + id) && !inputs.get(prefixByte + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- byte b = Byte.parseByte(inputs.get(prefixByte + id).remove());
- printBox.addMsg("Returning: " + b);
- logger.info(printBox.toString());
- return b;
- } else {
- byte rnd =
- config.isSvcompRandomInputs()
- ? (byte) (new Random()).nextInt()
- : Byte.valueOf((byte) 0);
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetByte");
+ String prefix = ByteValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetByte with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ // Parse as int first to handle unsigned byte values (0-255) from SMT solver
+ int intVal = Integer.parseInt(inputs.get(prefix + newId).remove());
+ byte b = (byte) intVal; // Cast handles conversion from unsigned to signed
+ printBox.addMsg("Returning: " + b);
+ logger.info(printBox.toString());
+ return b;
+ } else {
+ byte rnd =
+ config.isSvcompRandomInputs()
+ ? (byte) (new Random()).nextInt()
+ : Byte.valueOf((byte) 0);
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Byte(rnd); // Needed to prevent intering
+ }
+
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0;
}
}
+ @SuppressWarnings("removal")
public static char nondetChar(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetChar");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixChar + id) && !inputs.get(prefixChar + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- char c = inputs.get(prefixChar + id).remove().charAt(0);
- printBox.addMsg("Returning: " + c);
- logger.info(printBox.toString());
- return c;
- } else {
- char rnd =
- config.isSvcompRandomInputs()
- ? (char) (new Random()).nextInt()
- : Character.valueOf((char) 0);
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetChar");
+ String prefix = CharValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetChar with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ String encodedValue = inputs.get(prefix + newId).remove();
+ char c = (char) Integer.parseInt(encodedValue);
+ printBox.addMsg("Returning: " + c);
+ logger.info(printBox.toString());
+ return new Character(c); // Needed to prevent intering
+ } else {
+ char rnd =
+ config.isSvcompRandomInputs()
+ ? (char) (new Random()).nextInt()
+ : Character.valueOf((char) 0);
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Character(rnd); // Needed to prevent intering
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return '\u0000';
}
}
+ @SuppressWarnings("removal")
public static short nondetShort(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetShort");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixShort + id) && !inputs.get(prefixShort + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- short s = Short.parseShort(inputs.get(prefixShort + id).remove());
- printBox.addMsg("Returning: " + s);
- logger.info(printBox.toString());
- return s;
- } else {
- short rnd =
- config.isSvcompRandomInputs()
- ? (short) (new Random()).nextInt()
- : Short.valueOf((short) 0);
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetShort");
+ String prefix = ShortValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetShort with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ // Parse as int first to handle unsigned short values (0-65535) from SMT solver
+ int intVal = Integer.parseInt(inputs.get(prefix + newId).remove());
+ short s = (short) intVal; // Cast handles conversion from unsigned to signed
+ printBox.addMsg("Returning: " + s);
+ logger.info(printBox.toString());
+ return s;
+ } else {
+ short rnd =
+ config.isSvcompRandomInputs()
+ ? (short) (new Random()).nextInt()
+ : Short.valueOf((short) 0);
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Short(rnd); // Needed to prevent intering
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0;
}
}
+ @SuppressWarnings("removal")
public static int nondetInt(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetInt");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixInt + id) && !inputs.get(prefixInt + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- int i = Integer.parseInt(inputs.get(prefixInt + id).remove());
- printBox.addMsg("Returning: " + i);
- logger.info(printBox.toString());
- return i;
- } else {
- int rnd = config.isSvcompRandomInputs() ? (new Random()).nextInt() : 0;
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetInt");
+ String prefix = IntValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetInt with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ // Parse as unsigned to handle values from SMT solver bitvector representation
+ long longVal = Long.parseLong(inputs.get(prefix + newId).remove());
+ int i = (int) longVal; // Cast handles conversion from unsigned to signed
+ printBox.addMsg("Returning: " + i);
+ logger.info(printBox.toString());
+ return i;
+ } else {
+ int rnd = config.isSvcompRandomInputs() ? (new Random()).nextInt() : 0;
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Integer(rnd); // Needed to prevent intering
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0;
}
}
+ @SuppressWarnings("removal")
public static long nondetLong(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetLong");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixLong + id) && !inputs.get(prefixLong + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- long l = Long.parseLong(inputs.get(prefixLong + id).remove());
- printBox.addMsg("Returning: " + l);
- logger.info(printBox.toString());
- return l;
- } else {
- long rnd = config.isSvcompRandomInputs() ? (new Random()).nextLong() : 0L;
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetLong");
+ String prefix = LongValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetLong with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ // Parse as unsigned to handle values from SMT solver bitvector representation
+ long l = Long.parseUnsignedLong(inputs.get(prefix + newId).remove());
+ printBox.addMsg("Returning: " + l);
+ logger.info(printBox.toString());
+ return l;
+ } else {
+ long rnd = config.isSvcompRandomInputs() ? (new Random()).nextLong() : 0L;
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return new Long(rnd); // Needed to prevent intering
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0L;
}
}
public static float nondetFloat(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetFloat");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixFloat + id) && !inputs.get(prefixFloat + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- int enc = Integer.parseUnsignedInt(inputs.get(prefixFloat + id).remove());
- float f = Float.intBitsToFloat(enc);
- printBox.addMsg("Returning: " + f);
- logger.info(printBox.toString());
- return f;
- } else {
- float rnd = config.isSvcompRandomInputs() ? (new Random()).nextFloat() : 0f;
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetFloat");
+ String prefix = FloatValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetFloat with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ int enc = Integer.parseUnsignedInt(inputs.get(prefix + newId).remove());
+ float f = Float.intBitsToFloat(enc);
+ printBox.addMsg("Returning: " + f);
+ logger.info(printBox.toString());
+ return f;
+ } else {
+ float rnd = config.isSvcompRandomInputs() ? (new Random()).nextFloat() : 0f;
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return rnd;
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0.0f;
}
}
public static double nondetDouble(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetDouble");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixDouble + id) && !inputs.get(prefixDouble + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- long enc = Long.parseUnsignedLong(inputs.get(prefixDouble + id).remove());
- double d = Double.longBitsToDouble(enc);
- printBox.addMsg("Returning: " + d);
- logger.info(printBox.toString());
- return d;
- } else {
- double rnd = config.isSvcompRandomInputs() ? (new Random()).nextDouble() : 0d;
- String msg =
- config.isSvcompRandomInputs()
- ? "Randomness enabled, using random value"
- : "Randomness disabled, using fixed value";
- printBox.addMsg(msg);
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetDouble");
+ String prefix = DoubleValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetDouble with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ long enc = Long.parseUnsignedLong(inputs.get(prefix + newId).remove());
+ double d = Double.longBitsToDouble(enc);
+ printBox.addMsg("Returning: " + d);
+ logger.info(printBox.toString());
+ return d;
+ } else {
+ double rnd = config.isSvcompRandomInputs() ? (new Random()).nextDouble() : 0d;
+ String msg =
+ config.isSvcompRandomInputs()
+ ? "Randomness enabled, using random value"
+ : "Randomness disabled, using fixed value";
+ printBox.addMsg(msg);
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return rnd;
+ }
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return 0.0d;
}
}
public static String nondetString(long id) {
- PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetString");
- printBox.addMsg("Requested ID: " + id);
- if (inputs.containsKey(prefixString + id) && !inputs.get(prefixString + id).isEmpty()) {
- printBox.addMsg("Predetermined value available!");
- var val = inputs.get(prefixString + id).peek();
- printBox.addMsg("Returning: " + val);
- logger.info(printBox.toString());
- return val;
- } else {
- printBox.addMsg("No predetermined value available");
- String rnd = "";
- if (config.isSvcompRandomInputs()) {
- printBox.addMsg("Randomness enabled, using random value");
- Random random = new Random();
- int size = random.nextInt(100);
- byte[] bytes = new byte[size];
- random.nextBytes(bytes);
- rnd = new String(bytes);
+ try{
+ PrintBox printBox = new PrintBox(60, "SV-Comp Verifier: nondetString");
+ String prefix = StringValue.getSymbolicPrefix() + "_";
+ String requestedName = prefix + id;
+ String newId = String.valueOf(id);
+ int occurrence = ThreadHandler.getSymbolicIdxOccurrence(currentThread().getId()).getOrDefault(requestedName, 0);
+ if (occurrence > 0) {
+ newId = id + String.format("%02d", occurrence);
+ logger.warn("Multiple calls to nondetString with the same name: {}. Assigning new idx: {}", requestedName, newId);
+
+ }
+ printBox.addMsg("Requested ID: " + newId);
+ if (inputs.containsKey(prefix + newId) && !inputs.get(prefix + newId).isEmpty()) {
+ printBox.addMsg("Predetermined value available!");
+ var val = inputs.get(prefix + newId).peek();
+ printBox.addMsg("Returning: " + val);
+ logger.info(printBox.toString());
+ return val;
} else {
- printBox.addMsg("Randomness disabled, using fixed value");
- rnd = "fixed";
+ printBox.addMsg("No predetermined value available");
+ String rnd = "";
+ if (config.isSvcompRandomInputs()) {
+ printBox.addMsg("Randomness enabled, using random value");
+ Random random = new Random();
+ int size = random.nextInt(100);
+ byte[] bytes = new byte[size];
+ random.nextBytes(bytes);
+ rnd = new String(bytes);
+ } else {
+ printBox.addMsg("Randomness disabled, using fixed value");
+ rnd = new String("fixed"); // constructor required for preventing interning
+ }
+ printBox.addMsg("Returning " + rnd);
+ logger.info(printBox.toString());
+ return rnd;
}
- printBox.addMsg("Returning " + rnd);
- logger.info(printBox.toString());
- return rnd;
+ } catch (Throwable t) {
+ // The ErrorHandler has to be here as this method transfers control to the target domain
+ new ErrorHandler().handleException("Error retrieving value for SV-Comp", t);
+ return null;
}
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
index 55f0f67..bc59a3f 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
@@ -1,20 +1,23 @@
package de.uzl.its.swat.instrument.symbolicwrapper;
-import de.uzl.its.swat.config.Config;
import de.uzl.its.swat.instrument.AbstractMethodAdapter;
+import de.uzl.its.swat.instrument.Intrinsics;
+import de.uzl.its.swat.instrument.TryCatchBlock;
import org.objectweb.asm.Label;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
/**
- * A visitor to visit a Java method This class surrounds the whole function with a try catch blog to
- * ad a solve in case of an error.
+ * A visitor to visit a Java method. This class surrounds the whole function with a try catch blog
+ * to add a solve in case of an error.
*/
public class SurroundingTryCatchMethodAdapter extends AbstractMethodAdapter {
- private final Label[] surroundingTryCatch;
+ private final TryCatchBlock surroundingTryCatch;
private boolean addEndOfTryCatch = false;
- Config config = Config.instance();
+
+ private final boolean shouldInstrument;
/**
* Constructor that calls the super from the default MethodVisitor
@@ -22,65 +25,97 @@ public class SurroundingTryCatchMethodAdapter extends AbstractMethodAdapter {
* @param mv Parent MethodVisitor
* @param name The method name
*/
- public SurroundingTryCatchMethodAdapter(MethodVisitor mv, String name, String desc) {
+ public SurroundingTryCatchMethodAdapter(
+ MethodVisitor mv, String cname, String name, String desc) {
super(mv, name, desc);
// Label used for try catch
- this.surroundingTryCatch = new Label[] {new Label(), new Label(), new Label()};
+ this.surroundingTryCatch =
+ new TryCatchBlock(new Label(), new Label(), new Label(), new Label(), null);
+ this.shouldInstrument = shouldInstrument(cname, name);
}
- /**
- * Add a solve in case an exception happened inside the method
- *
- * @param maxStack
- * @param maxLocals
- */
@Override
- public void visitMaxs(int maxStack, int maxLocals) {
-
- if (!addEndOfTryCatch) {
- super.visitMaxs(maxStack, maxLocals);
- return;
+ public void visitCode() {
+ if (shouldInstrument) {
+ addBeginOfSurrounding();
}
-
- // Add end of try catch
- addEndOfSurrounding();
-
- visitTryCatchBlock(
- surroundingTryCatch[0],
- surroundingTryCatch[1],
- surroundingTryCatch[2],
- "java/lang/Throwable");
- super.visitMaxs(
- maxStack + 10, maxLocals + 10); // 10 might not be an adequate number but it works
}
@Override
- public void visitCode() {
- addBeginOfSurrounding();
+ public void visitMaxs(int maxStack, int maxLocals) {
+
+ if (shouldInstrument && addEndOfTryCatch) {
+ addEndOfSurrounding();
+ }
+
+ // visit the corresponding instructions
+ super.visitMaxs(maxStack, maxLocals);
}
private void addBeginOfSurrounding() {
- visitTryCatchBlock(
- surroundingTryCatch[0],
- surroundingTryCatch[1],
- surroundingTryCatch[2],
- "java/lang/Throwable");
- visitLabel(surroundingTryCatch[0]);
+ surroundingTryCatch.visit(mv);
+ mv.visitLabel(surroundingTryCatch.start());
addEndOfTryCatch = true;
}
private void addEndOfSurrounding() {
- visitLabel(surroundingTryCatch[1]);
- visitLabel(surroundingTryCatch[2]);
-
- visitFrame(Opcodes.F_SAME1, 0, null, 1, new Object[] {"java/lang/Throwable"});
- visitVarInsn(Opcodes.ASTORE, 2);
-
- visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "solve", "()V", false);
-
- visitVarInsn(Opcodes.ALOAD, 2);
+ mv.visitLabel(surroundingTryCatch.end());
+ mv.visitJumpInsn(Opcodes.GOTO, surroundingTryCatch.jumpTarget());
+ mv.visitLabel(surroundingTryCatch.handler());
+
+ visitInsn(Opcodes.DUP);
+
+ visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL, "java/lang/Throwable", "printStackTrace", "()V", false);
+
+ // Duplicate exception for instanceof check
+ visitInsn(Opcodes.DUP);
+
+ // Check if exception instanceof RuntimeException
+ visitTypeInsn(Opcodes.INSTANCEOF, "java/lang/RuntimeException");
+
+ // Create labels for conditional branching
+ Label isRuntimeException = new Label();
+ Label continueExecution = new Label();
+
+ // If instanceof returns true (non-zero), jump to isRuntimeException label
+ visitJumpInsn(Opcodes.IFNE, isRuntimeException);
+
+ // Not a RuntimeException - print checked exception message
+ visitFieldInsn(
+ Opcodes.GETSTATIC,
+ "java/lang/System",
+ "out",
+ "Ljava/io/PrintStream;");
+ visitLdcInsn("[SWAT] Uncaught top-level checked exception in symbolic execution");
+ visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL,
+ "java/io/PrintStream",
+ "println",
+ "(Ljava/lang/String;)V",
+ false);
+ visitJumpInsn(Opcodes.GOTO, continueExecution);
+
+ // Is a RuntimeException - print runtime exception message
+ visitLabel(isRuntimeException);
+ visitFieldInsn(
+ Opcodes.GETSTATIC,
+ "java/lang/System",
+ "out",
+ "Ljava/io/PrintStream;");
+ visitLdcInsn("[SWAT] Uncaught top-level RuntimeException in symbolic execution");
+ visitMethodInsn(
+ Opcodes.INVOKEVIRTUAL,
+ "java/io/PrintStream",
+ "println",
+ "(Ljava/lang/String;)V",
+ false);
+
+ visitLabel(continueExecution);
+ visitMethodInsn(Opcodes.INVOKESTATIC, Type.getInternalName(Intrinsics.class), "terminate", "()V", false);
visitInsn(Opcodes.ATHROW);
+ mv.visitLabel(surroundingTryCatch.jumpTarget());
}
}
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 bbb760a..2540fbd 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
@@ -1,11 +1,14 @@
package de.uzl.its.swat.instrument.symbolicwrapper;
import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.Util;
import de.uzl.its.swat.config.Config;
+import de.uzl.its.swat.instrument.springendpoint.SpringEndpointTransformer;
import java.util.regex.Pattern;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.commons.TryCatchBlockSorter;
/**
* A visitor to visit a Java class. The methods of this class must be called in the following order:
@@ -50,72 +53,72 @@ public MethodVisitor visitMethod(
// Generate default MethodVisitor
MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions);
+
+ if(Util.ignoreMethod(name)) {
+ // Avoid Jacoco
+ return mv;
+ }
+
if (mv != null) {
switch (config.getInstrumentationTransformer()) {
- case SV_COMP:
- if (name.equals("main")) {
- SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
- mv =
- new SymbolicWrapperMethodAdapter(
- new SurroundingTryCatchMethodAdapter(mv, name, desc),
- cname,
- name,
- desc);
+ case SV_COMP -> {
+ if (!name.equals("main")) {
+ return mv;
+ }
+ }
+ case SPRING_ENDPOINT -> {
+ if (!SpringEndpointTransformer.getInstrumentedEndpoints()
+ .contains(cname + ":" + name)) {
+ return mv;
}
- break;
+ }
- case SPRING_ENDPOINT:
- /*
- SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
- mv =
- new SymbolicWrapperMethodAdapter(
- new SurroundingTryCatchMethodAdapter(mv, name, desc),
- cname,
- name,
- desc);
- */
- new ErrorHandler()
- .handleException(
- new RuntimeException(
- "Spring Endpoints are not supported currently."));
- break;
- case WEB_SERVLET:
+ case WEB_SERVLET -> {
/*
- if (name.equals("doPost")) {
- SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
- mv =
- new SymbolicWrapperMethodAdapter(
- new SurroundingTryCatchMethodAdapter(mv, name, desc),
- cname,
- name,
- desc);
+ if (!name.equals("doPost")) {
+ return mv;
}
*/
new ErrorHandler()
.handleException(
new RuntimeException(
"Servlet Endpoints are not supported currently."));
- break;
- case PARAMETER:
- if (Pattern.matches(
- config.getInstrumentationParameterSymbolicMethodName(), name)) {
- SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
- mv =
- new SymbolicWrapperMethodAdapter(
- new SurroundingTryCatchMethodAdapter(mv, name, desc),
- cname,
- name,
- desc);
+ }
+
+ case ANNOTATION -> {
+ String pattern =
+ config.getInstrumentationAnnotationSymbolicMethodName() == null ?
+ "main" :
+ config.getInstrumentationAnnotationSymbolicMethodName();
+ if (!Pattern.matches(pattern, name)) {
+ return mv;
+ }
+ }
+ case PARAMETER -> {
+ if (!Util.isSymbolicMethod(cname, name)) {
+ return mv;
}
- case NONE:
- break;
- default:
- break;
+ }
+ case NONE -> {
+ return mv;
+ }
}
+ SymbolicWrapperTransformer.getPrintBox().addMsg("Method: " + name);
+
+ mv =
+ new SymbolicWrapperMethodAdapter(
+ new SurroundingTryCatchMethodAdapter(
+ new TryCatchBlockSorter(
+ mv, access, name, desc, signature, exceptions),
+ cname,
+ name,
+ desc),
+ cname,
+ name,
+ desc);
return mv;
}
-
return null;
}
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperMethodAdapter.java
index 71f5b62..4c2bfe2 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SymbolicWrapperMethodAdapter.java
@@ -1,14 +1,18 @@
package de.uzl.its.swat.instrument.symbolicwrapper;
import de.uzl.its.swat.instrument.AbstractMethodAdapter;
+import de.uzl.its.swat.instrument.Intrinsics;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
+import org.objectweb.asm.Type;
public class SymbolicWrapperMethodAdapter extends AbstractMethodAdapter {
- private boolean headerPossiblyInserted = false;
+ private boolean headerInserted = false;
private String cname;
+ private final boolean shouldInstrument;
+
/**
* Constructor that calls the super from the default MethodVisitor
*
@@ -19,14 +23,17 @@ public class SymbolicWrapperMethodAdapter extends AbstractMethodAdapter {
public SymbolicWrapperMethodAdapter(MethodVisitor mv, String cname, String name, String desc) {
super(mv, name, desc);
this.cname = cname;
+ shouldInstrument = this.shouldInstrument(cname, name);
}
@Override
public void visitCode() {
- if (!headerPossiblyInserted) {
- insertHeaderIfNeeded();
- headerPossiblyInserted = true;
+ if (!headerInserted && shouldInstrument) {
+ addInitializer();
+ headerInserted = true;
}
+
+ super.visitCode();
}
/**
@@ -46,37 +53,31 @@ public void visitCode() {
*/
@Override
public void visitInsn(int opcode) {
- switch (opcode) {
- case Opcodes.IRETURN,
- Opcodes.FRETURN,
- Opcodes.ARETURN,
- Opcodes.LRETURN,
- Opcodes.DRETURN,
- Opcodes.RETURN -> addSolver();
- default -> {}
+ if (shouldInstrument) {
+ switch (opcode) {
+ case Opcodes.IRETURN,
+ Opcodes.FRETURN,
+ Opcodes.ARETURN,
+ Opcodes.LRETURN,
+ Opcodes.DRETURN,
+ Opcodes.RETURN -> addSolver();
+ default -> {}
+ }
}
super.visitInsn(opcode);
}
- /**
- * Starts the visit of the method's code, if any (i.e. non abstract method). Adds the beginning
- * call for the concolic engine to the method
- */
- public void insertHeaderIfNeeded() {
- addInitializer();
- }
-
/** Adds the initializer call */
private void addInitializer() {
String endpointID = cname + "/" + this.getName() + this.getDesc();
SymbolicWrapperTransformer.getPrintBox()
- .addMsg(" => Adding initializer: Main.init(endpointID)");
+ .addMsg(" => Adding initializer: Intrinsics.init(endpointID)");
SymbolicWrapperTransformer.getPrintBox().setContentPresent(true);
visitLdcInsn(endpointID);
visitMethodInsn(
Opcodes.INVOKESTATIC,
- "de/uzl/its/swat/Main",
+ Type.getInternalName(Intrinsics.class),
"init",
"(Ljava/lang/String;)V",
false);
@@ -87,9 +88,9 @@ private void addSolver() {
// Add a call to solve and reset the symbolic engine
SymbolicWrapperTransformer.getPrintBox()
- .addMsg(" => Adding termination: Main.terminate()");
+ .addMsg(" => Adding termination: Intrinsics.terminate()");
SymbolicWrapperTransformer.getPrintBox().setContentPresent(true);
- visitMethodInsn(Opcodes.INVOKESTATIC, "de/uzl/its/swat/Main", "terminate", "()V", false);
+ visitMethodInsn(Opcodes.INVOKESTATIC, Type.getInternalName(Intrinsics.class), "terminate", "()V", false);
}
}
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 a343a27..05eeed5 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
@@ -1,11 +1,18 @@
package de.uzl.its.swat.instrument.symbolicwrapper;
+import ch.qos.logback.classic.Logger;
import de.uzl.its.swat.common.ErrorHandler;
import de.uzl.its.swat.common.PrintBox;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.logging.GlobalLogger;
import de.uzl.its.swat.config.Config;
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.springendpoint.SpringEndpointTransformer;
+import java.io.PrintWriter;
+import java.io.StringWriter;
import java.lang.instrument.ClassFileTransformer;
import java.lang.instrument.IllegalClassFormatException;
import java.security.ProtectionDomain;
@@ -13,7 +20,7 @@
import org.objectweb.asm.ClassReader;
import org.objectweb.asm.ClassVisitor;
import org.objectweb.asm.ClassWriter;
-import org.slf4j.LoggerFactory;
+import org.objectweb.asm.util.CheckClassAdapter;
/**
* An agent provides an implementation of this interface in order to transform class files. The
@@ -23,12 +30,16 @@ public class SymbolicWrapperTransformer implements ClassFileTransformer {
Config config = Config.instance();
- @Getter private static PrintBox printBox;
- private static final org.slf4j.Logger logger =
- LoggerFactory.getLogger(SymbolicWrapperTransformer.class);
+
+ private static final ThreadLocal printBox = ThreadLocal.withInitial(() -> new PrintBox(60, "Transformer" + SymbolicWrapperTransformer.class.getSimpleName()));
+
+ public static PrintBox getPrintBox() {
+ return printBox.get();
+ }
+
+ private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger();
public SymbolicWrapperTransformer() {
- printBox = new PrintBox(60, "Transformer: " + this.getClass().getSimpleName());
Transformer.getPrintBox()
.addMsg("Initializing Transformer: " + this.getClass().getSimpleName());
}
@@ -57,45 +68,54 @@ public byte[] transform(
ProtectionDomain d,
byte[] cbuf)
throws IllegalClassFormatException {
- if (classBeingRedefined != null || !Transformer.shouldInstrument(cname)) {
+ try {
+ if (classBeingRedefined != null || cname == null || !Util.shouldInstrument(cname)) {
return cbuf;
}
switch (config.getInstrumentationTransformer()) {
- case SPRING_ENDPOINT -> new ErrorHandler()
- .handleException(
- new RuntimeException(
- "Spring Endpoint Instrumentation is not supported for symbolic"
- + " execution"));
+ case SPRING_ENDPOINT -> {
+ if (!SpringEndpointTransformer.getInstrumentedClasses().contains(cname)) {
+ return cbuf;
+ }
+ }
case WEB_SERVLET -> new ErrorHandler()
.handleException(
new RuntimeException(
"Servlet Endpoint Instrumentation is not supported for symbolic"
+ " execution"));
case SV_COMP, NONE -> {}
+ case ANNOTATION -> {
+ if (!cname.equals(config.getInstrumentationAnnotationSymbolicClassName()) &&
+ config.getInstrumentationAnnotationSymbolicClassName() != null)
+ return cbuf;
+ }
case PARAMETER -> {
- if (!cname.equals(config.getInstrumentationParameterSymbolicClassName()))
+ if (!Util.isSymbolicClass(cname))
return cbuf;
}
}
- printBox.addMsg("Class: " + cname);
- try {
+ getPrintBox().addMsg("Class: " + cname);
ClassReader cr = new ClassReader(cbuf);
- ClassWriter cw =
- new SafeClassWriter(
- cr, loader, ClassWriter.COMPUTE_FRAMES | ClassWriter.COMPUTE_MAXS);
+ ClassWriter cw = new SafeClassWriter(cr, loader, ClassWriter.COMPUTE_FRAMES);
ClassVisitor cv = new SymbolicWrapperClassAdapter(cw, cname);
cr.accept(cv, 0);
+
+ if (Config.instance().isUseCheckClassAdapter() && Util.useCheckClassAdapterForClass(cname)) {
+ StringWriter stringWriter = new StringWriter();
+ PrintWriter printWriter = new PrintWriter(stringWriter);
+ CheckClassAdapter.verify(new ClassReader(cw.toByteArray()), false, printWriter);
+ SWATAssert.enforce(stringWriter.toString().isEmpty(), "Instrumentation error: {}", stringWriter);
+ }
+
Transformer.addInstrumentedClass(cname, InternalTransformerType.SYMBOLIC_WRAPPER);
- if (printBox.isContentPresent()) logger.info(printBox.toString());
+ if (getPrintBox().isContentPresent()) logger.debug(getPrintBox().toString());
return cw.toByteArray();
- } catch (Exception e) {
- new ErrorHandler().handleException("Error while instrumenting class: " + cname, e);
+ } catch (Throwable t) {
+ new ErrorHandler().handleException("Error while instrumenting class: " + cname, t);
}
- Transformer.addInstrumentedClass(cname, InternalTransformerType.SYMBOLIC_WRAPPER);
- if (printBox.isContentPresent()) logger.info(printBox.toString());
return cbuf;
}
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
new file mode 100644
index 0000000..b1f69d3
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepot.java
@@ -0,0 +1,246 @@
+package de.uzl.its.swat.metadata;
+
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.NoThreadContextException;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.common.ErrorHandler;
+import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException;
+import de.uzl.its.swat.common.exceptions.ThreadAlreadyEnabledException;
+import lombok.Getter;
+
+import javax.annotation.Nullable;
+import java.io.Serializable;
+import java.util.*;
+
+/**
+ * A singleton repository that tracks classes and their corresponding fields.
+ * Each unique (formatted) class name is assigned a stable index.
+ * Field indices within a class are assigned based on a per–class-hierarchy layout.
+ *
+ * Inherited instance fields are merged into a subclass’s layout (preserving their original index).
+ * For static fields, the template of the referenced class (typically the one from the constant pool) is used.
+ */
+public class ClassDepot implements Serializable, ClassDepotInstrumentation, ClassDepotRuntime {
+
+ // Global counter to assign a unique index to each class.
+ @Getter
+ private int classCounter = 0;
+
+ // Maps a formatted class name to its unique integer index.
+ private final Map classToIndex = new HashMap<>();
+
+ // Maps the class index back to its formatted name.
+ private final Map indexToClass = new HashMap<>();
+
+ /**
+ * Holds ClassTemplate instances keyed by class index.
+ * Each template contains the field layout (instance and static) for that class,
+ * including fields inherited from its superclasses and interfaces.
+ */
+ private final Map classTemplates = new HashMap<>();
+
+ private final Map> classToParents = new HashMap<>();
+ private final Map> classToInterfaces = new HashMap<>();
+
+ private final Map> ancestorBaseCache = new HashMap<>();
+
+
+ // Singleton instance.
+ private static final ClassDepot instance = new ClassDepot();
+
+ private ClassDepot() {
+ // Prevent outside instantiation.
+ }
+
+ public static ClassDepotRuntime getRuntimeInstance() {
+ return instance;
+ }
+
+ public synchronized Map> getAncestorBaseCache() {
+ return ancestorBaseCache;
+ }
+
+ public static ClassDepotInstrumentation getInstrumentationInstance() {
+ return instance;
+ }
+
+ /**
+ * Registers type metadata (parent and interface names) for a class.
+ */
+ public synchronized void registerTypeInfoForClass(String className, List parents, List interfaces) {
+ String normalized = Util.formatClassName(className);
+ classToParents.put(normalized, parents);
+ classToInterfaces.put(normalized, interfaces);
+ SWATAssert.enforce(!ancestorBaseCache.containsKey(normalized), "Class " + normalized + " already registered in ancestorBaseCache");
+ }
+
+ public synchronized List getParentsForClass(String className) {
+ return classToParents.getOrDefault(Util.formatClassName(className), Collections.emptyList());
+ }
+
+ public synchronized List getInterfacesForClass(String className) {
+ return classToInterfaces.getOrDefault(Util.formatClassName(className), Collections.emptyList());
+ }
+
+ /**
+ * Retrieves (or creates) a ClassTemplate for the given class using reflection.
+ * This method loads the class if necessary, merges in parent and interface fields,
+ * and then caches the complete template.
+ */
+ private ClassTemplate getFillOrCreateTemplateWithReflection(String className, @Nullable Class> clazz)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException {
+ className = Util.formatClassName(className);
+ int cIdx = getClassIndex(className);
+ ClassTemplate template = classTemplates.get(cIdx);
+ if (template != null && template.isComplete()) {
+ return template;
+ }
+
+ // Load class via reflection if not provided.
+ if (clazz == null) {
+ clazz = Util.loadClassForName(className);
+ }
+ if(template == null) {
+ template = new ClassTemplate(className);
+ }
+
+ // Process parent class: merge its fields so inherited fields retain their indices.
+ Class> parentClazz = Util.getSuperclass(clazz);
+ if (parentClazz != null && parentClazz != Object.class) {
+ String parentName = Util.formatClassName(parentClazz.getName());
+ ClassTemplate parentTemplate = getFillOrCreateTemplateWithReflection(parentName, parentClazz);
+ template.mergeFields(parentTemplate);
+ }
+
+ // Process implemented interfaces.
+ Class>[] interfaces = Util.getInterfaces(clazz);
+ for (Class> interfaceClazz : interfaces) {
+ String interfaceName = Util.formatClassName(interfaceClazz.getName());
+ ClassTemplate interfaceTemplate = getFillOrCreateTemplateWithReflection(interfaceName, interfaceClazz);
+ template.mergeFields(interfaceTemplate);
+ }
+
+ // Add fields declared in the current class using reflection.
+ template.addFields(Util.getDeclaredFields(clazz));
+
+ // Mark the template as complete and cache it.
+ template.setComplete(true);
+ classTemplates.put(cIdx, template);
+
+ return template;
+ }
+
+ @Override
+ public String getMethodIdentifier(int cIdx, int mIdx) {
+ ClassTemplate ct = classTemplates.get(cIdx);
+ if (ct != null) {
+ return ct.getMethodIdentifier(mIdx);
+ } else {
+ new ErrorHandler().handleException(new RuntimeException("Class " + cIdx + " not found. Method " + mIdx));
+ return null;
+ }
+ }
+
+ @Override
+ public synchronized int getMethodIdxForInstrumentation(String className, String methodName, String desc) {
+ int cIdx = getClassIndex(className);
+ String methodNameFormatted = Util.formatMethodName(className, methodName, desc);
+ ClassTemplate template = classTemplates.get(cIdx);
+
+ if (template == null) {
+ template = new ClassTemplate(Util.formatClassName(className));
+ classTemplates.put(cIdx, template);
+ }
+
+ return template.getMethodIndex(methodNameFormatted);
+ }
+
+ @Override
+ public int getMethodIdxAtRuntime(String className, @Nullable Class> cls, String methodName, String desc)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException {
+ String methodNameFormatted = Util.formatMethodName(className, methodName, desc);
+ ClassTemplate template = getFillOrCreateTemplateWithReflection(className, cls);
+
+ return template.getMethodIndex(methodNameFormatted);
+ }
+
+ /**
+ * For instrumented field access, this helper returns the field index.
+ * If the field name is not fully qualified (does not contain the divider),
+ * it is formatted using the concrete class name.
+ *
+ * In the static case (or when no instance is available), the concreteClassName
+ * is taken from the instruction’s reference.
+ *
+ * @param cIdx the class index (as stored in the depot)
+ * @param fieldName the field name from the instruction
+ * @param isStatic whether the field is static
+ * @return the field index from the corresponding ClassTemplate
+ */
+ public int getFieldIndex(int cIdx, String fieldName, boolean isStatic) throws ThreadAlreadyDisabledException, NoThreadContextException, ThreadAlreadyEnabledException, ClassNotFoundException {
+ String className = getClassName(cIdx);
+ ClassTemplate template = classTemplates.get(cIdx);
+ if (template == null || !template.isComplete()) {
+ template = getFillOrCreateTemplateWithReflection(className, null);
+ }
+
+ String fieldIdentifier = fieldName.contains(Util.FIELD_DIVIDER)
+ ? fieldName
+ : Util.formatFieldName(className, fieldName);
+ return template.getFieldIndex(fieldIdentifier, isStatic);
+ }
+
+ @Override
+ public int getTotalFieldCountWithReflection(String className, @Nullable Class> cls)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException {
+ ClassTemplate ct = getFillOrCreateTemplateWithReflection(className, cls);
+ int totalFieldCount = ct.getTotalFieldCount();
+ SWATAssert.check(totalFieldCount ==
+ Util.getFieldCount(className, cls, false) +
+ Util.getFieldCount(className, cls, true), "Total field count mismatch");
+ return totalFieldCount;
+ }
+
+ @Override
+ public int getFieldCountWithReflection(String className, @Nullable Class> cls, boolean isStatic)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException {
+ ClassTemplate ct = getFillOrCreateTemplateWithReflection(className, cls);
+ int fieldCount = ct.getFieldCount(isStatic);
+ SWATAssert.check(fieldCount == Util.getFieldCount(className, cls, isStatic), "Field count mismatch");
+ return fieldCount;
+ }
+
+ /**
+ * Returns a stable integer "class index" for the specified class name.
+ * The class name is normalized before being stored.
+ */
+ @Override
+ public synchronized int getClassIndex(String className) {
+ String normalized = Util.formatClassName(className);
+
+ Integer classIndex = classToIndex.get(normalized);
+ if (classIndex == null) {
+ classIndex = classCounter++;
+ classToIndex.put(normalized, classIndex);
+ indexToClass.put(classIndex, normalized);
+ }
+ return classIndex;
+ }
+
+ /**
+ *
+ * Retrieves the formatted class name (e.g., "java/lang/String") corresponding to a given integer
+ * index. This is the inverse operation of {@link #getClassIndex(String)}.
+ *
+ *
+ * @param cIdx The class index.
+ * @return The formatted class name associated with the provided index, or {@code null} if none exists.
+ */
+ @Override
+ public String getClassName(int cIdx) {
+ if (cIdx >= classCounter) {
+ System.out.println("Class index " + cIdx + " is out of bounds. Maximum index is " + (classCounter - 1));
+ }
+ return indexToClass.get(cIdx);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotInstrumentation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotInstrumentation.java
new file mode 100644
index 0000000..e6680dd
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotInstrumentation.java
@@ -0,0 +1,14 @@
+package de.uzl.its.swat.metadata;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+public interface ClassDepotInstrumentation {
+ String getClassName(int cIdx);
+ int getClassIndex(String className);
+ int getMethodIdxForInstrumentation(String className, String methodName, String desc);
+ String getMethodIdentifier(int cIdx, int mIdx);
+ void registerTypeInfoForClass(String className, List parents, List interfaces);
+ Map> getAncestorBaseCache();
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotRuntime.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotRuntime.java
new file mode 100644
index 0000000..507cb46
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassDepotRuntime.java
@@ -0,0 +1,21 @@
+package de.uzl.its.swat.metadata;
+
+import de.uzl.its.swat.common.exceptions.NoThreadContextException;
+import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException;
+import de.uzl.its.swat.common.exceptions.ThreadAlreadyEnabledException;
+
+import javax.annotation.Nullable;
+import java.util.List;
+
+public interface ClassDepotRuntime extends ClassDepotInstrumentation {
+ int getFieldIndex(int cIdx, String fieldName, boolean isStatic) throws ThreadAlreadyDisabledException, NoThreadContextException, ThreadAlreadyEnabledException, ClassNotFoundException;
+ int getTotalFieldCountWithReflection(String className, @Nullable Class> cls)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException;
+ int getFieldCountWithReflection(String className, @Nullable Class> cls, boolean isStatic)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException;
+ int getMethodIdxAtRuntime(String className, @Nullable Class> cls, String methodName, String desc)
+ throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException;
+ List getParentsForClass(String className);
+ List getInterfacesForClass(String className);
+ int getClassCounter();
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassTemplate.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassTemplate.java
new file mode 100644
index 0000000..6a3275f
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/ClassTemplate.java
@@ -0,0 +1,233 @@
+package de.uzl.its.swat.metadata;
+
+import de.uzl.its.swat.common.Util;
+import de.uzl.its.swat.common.exceptions.SWATAssert;
+import lombok.Getter;
+import lombok.Setter;
+
+import java.lang.reflect.Field;
+import java.lang.reflect.Modifier;
+import java.util.*;
+
+/**
+ * A class template that holds the field and method information for a class.
+ * It maintains separate mappings for instance and static fields.
+ * When building a template for a class, inherited fields are merged in so that
+ * the parent's fields retain their indices.
+ *
+ * Additionally, we track short field names -> the "winning" fully qualified name.
+ * This lets us unify references like "ChildClass#field" to the parent's actual
+ * "ParentClass#field" if the child does not truly hide that field.
+ */
+public class ClassTemplate {
+
+ // Indicates whether the template has been fully populated.
+ @Getter @Setter
+ private boolean complete = false;
+
+ // The normalized/unique name of the class (e.g., "java/lang/String").
+ @Getter
+ private final String className;
+
+ /**
+ * Method information.
+ */
+ private final Map methodToIndex = new HashMap<>();
+ private final List methodNames = new ArrayList<>();
+
+ /**
+ * Instance field mappings:
+ * key = fully qualified field identifier (e.g. "package/Class#field")
+ * value = index (slot) within the instance layout.
+ */
+ private final Map instanceFieldToIndex = new HashMap<>();
+ private final List instanceFields = new ArrayList<>();
+
+ /**
+ * Static field mappings:
+ * key = fully qualified field identifier
+ * value = index in the static field list.
+ */
+ private final Map staticFieldToIndex = new HashMap<>();
+ private final List staticFields = new ArrayList<>();
+
+ /**
+ * Short-name resolution for instance fields:
+ * key = short field name (e.g. "foo"),
+ * value = the fully qualified field identifier that "wins" in this class
+ * (e.g. "parentPkg/ParentClass#foo" or "childPkg/ChildClass#foo").
+ */
+ private final Map shortNameToFqInstance = new HashMap<>();
+
+ /**
+ * Short-name resolution for static fields.
+ */
+ private final Map shortNameToFqStatic = new HashMap<>();
+
+ public ClassTemplate(String className) {
+ this.className = className;
+ }
+
+ /* ------------------------------------------------
+ * Field lookup / indexing
+ * ------------------------------------------------ */
+
+ /**
+ * Primary lookup method. The fieldIdentifier can be either:
+ * 1) Fully qualified, e.g. "pkg/ChildClass#foo"
+ * 2) Already partially "resolved" but still referencing the child's name for an inherited field
+ *
+ * If we don't find a direct match in fieldToIndex, we parse the short name
+ * and see if there's an inherited or parent-defined field that wins.
+ */
+ public int getFieldIndex(String fieldIdentifier, boolean isStatic) {
+ Map fieldToIndex = isStatic ? staticFieldToIndex : instanceFieldToIndex;
+
+ // 1) If we have a direct match (fully qualified exactly),
+ // return its index right away.
+ Integer directIndex = fieldToIndex.get(fieldIdentifier);
+ if (directIndex != null) {
+ return directIndex;
+ }
+
+ // 2) Otherwise, parse out the short name from "className#fieldName".
+ int fieldBegin = fieldIdentifier.indexOf(Util.FIELD_DIVIDER);
+ SWATAssert.enforce(fieldBegin > 0, "Invalid field identifier: {}", fieldIdentifier);
+ String shortName = fieldIdentifier.substring(fieldBegin + 1);
+
+ // 3) Check the shortName -> FQ map. If we have an entry, use that.
+ Map shortMap = isStatic ? shortNameToFqStatic : shortNameToFqInstance;
+ String winningFqName = shortMap.get(shortName);
+ if (winningFqName != null) {
+ // If we have a "winning" FQ name, that's the real field.
+ Integer idx = fieldToIndex.get(winningFqName);
+ if (idx != null) {
+ return idx;
+ }
+ }
+
+ // 4) If not found, that means we have a truly new field that wasn't discovered
+ // by merging. We'll add it. (Rare if we enumerated all fields, but possible.)
+ return addField(fieldIdentifier, isStatic);
+ }
+
+ /**
+ * Returns the field identifier at the specified index.
+ */
+ public String getFieldIdentifier(int fieldIndex, boolean isStatic) {
+ List fields = isStatic ? staticFields : instanceFields;
+ return fields.get(fieldIndex);
+ }
+
+ /**
+ * Adds a new field (if not already present) and returns its assigned index.
+ * This also updates the shortName -> FQ map, overriding a parent's entry if needed.
+ */
+ public int addField(String fieldIdentifier, boolean isStatic) {
+ Map fieldToIndex = isStatic ? staticFieldToIndex : instanceFieldToIndex;
+ List fields = isStatic ? staticFields : instanceFields;
+ Map shortMap = isStatic ? shortNameToFqStatic : shortNameToFqInstance;
+
+ if (fieldToIndex.containsKey(fieldIdentifier)) {
+ return fieldToIndex.get(fieldIdentifier);
+ }
+
+ // Extract short name: "pkg/Class#field" -> "field"
+ int hashPos = fieldIdentifier.indexOf('#');
+ String shortName = fieldIdentifier.substring(hashPos + 1);
+
+ // Overwrite the shortName -> FQ entry. (Hiding or brand new field.)
+ shortMap.put(shortName, fieldIdentifier);
+
+ int newIndex = fields.size();
+ fieldToIndex.put(fieldIdentifier, newIndex);
+ fields.add(fieldIdentifier);
+ return newIndex;
+ }
+
+ /**
+ * Merges fields from a parent or interface template into this template.
+ * Inherited fields are added only if they do not already exist or are not hidden.
+ */
+ public void mergeFields(ClassTemplate otherTemplate) {
+ // Merge instance fields.
+ for (String parentFq : otherTemplate.instanceFields) {
+ // If we already have that exact FQ name, skip.
+ if (!instanceFieldToIndex.containsKey(parentFq)) {
+ addField(parentFq, false);
+ }
+ }
+ // Merge static fields.
+ for (String parentFq : otherTemplate.staticFields) {
+ if (!staticFieldToIndex.containsKey(parentFq)) {
+ addField(parentFq, true);
+ }
+ }
+ }
+
+ /* ------------------------------------------------
+ * Method indexing
+ * ------------------------------------------------ */
+
+ int getMethodIndex(String methodIdentifier) {
+ Integer existing = methodToIndex.get(methodIdentifier);
+ if (existing != null) {
+ return existing;
+ }
+ return addMethod(methodIdentifier);
+ }
+
+ String getMethodIdentifier(int mIdx) {
+ return methodNames.get(mIdx);
+ }
+
+ private int addMethod(String methodIdentifier) {
+ if (methodToIndex.containsKey(methodIdentifier)) {
+ return methodToIndex.get(methodIdentifier);
+ }
+ int newIndex = methodNames.size();
+ methodToIndex.put(methodIdentifier, newIndex);
+ methodNames.add(methodIdentifier);
+ return newIndex;
+ }
+
+ /* ------------------------------------------------
+ * Reflection-based addition
+ * ------------------------------------------------ */
+
+ /**
+ * Adds fields from an array of reflected Field objects.
+ * (Assuming we gather private/protected as well via getDeclaredFields.)
+ */
+ public void addFields(Field[] fields) {
+ for (Field field : fields) {
+ // "declaringClass#fieldName"
+ String declClass = Util.formatClassName(field.getDeclaringClass().getName());
+ String fieldIdentifier = Util.formatFieldName(declClass, field.getName());
+ addField(fieldIdentifier, Modifier.isStatic(field.getModifiers()));
+ }
+ }
+
+ /* ------------------------------------------------
+ * Utilities
+ * ------------------------------------------------ */
+
+ /**
+ * Returns the count of fields in this template for the specified static-ness.
+ */
+ int getFieldCount(boolean isStatic) {
+ return isStatic ? staticFields.size() : instanceFields.size();
+ }
+
+ /**
+ * Returns the total number of fields (static + instance) in this template.
+ */
+ int getTotalFieldCount() {
+ return staticFields.size() + instanceFields.size();
+ }
+
+ public boolean hasField(String fieldIdentifier, boolean isStatic) {
+ Map fieldToIndex = isStatic ? staticFieldToIndex : instanceFieldToIndex;
+ return fieldToIndex.containsKey(fieldIdentifier);
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/package-info.java b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/package-info.java
new file mode 100644
index 0000000..dd2db51
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/metadata/package-info.java
@@ -0,0 +1,19 @@
+/**
+ *
+ * This package provides classes and templates for managing metadata about classes and their fields,
+ * both at instrumentation time and at runtime.
+ *
+ *
+ *
+ * The central component is {@link de.uzl.its.swat.metadata.ClassDepot}, which acts as a registry to track each class and
+ * its fields. It uses two different template types:
+ *
+ * - {@link de.uzl.its.swat.metadata.InstrumentationClassTemplate} - for assigning/creating field indices during
+ * the instrumentation process.
+ * - {@link de.uzl.its.swat.metadata.RuntimeClassTemplate} - for looking up field indices at runtime.
+ *
+ * {@link de.uzl.its.swat.metadata.ClassTemplate} is an abstract base for these template
+ * implementations.
+ *