Skip to content

Commit 1c0d4ff

Browse files
AnneKoziolekclaude
andcommitted
Move interception to second-pass transformer with relocated package
Architecture change: comparison interception is now a separate ClassFileTransformer registered in GaletteAgent.premain(), running as a second pass after the main Galette transformer. This avoids modifying the jlink image entirely. Key changes: - Move interception PathUtils from internal.runtime (module-owned by java.base in jlink) to edu.neu.ccs.prl.galette.interception package (loadable from bootclasspath at runtime) - Rename to InterceptionPathUtils to avoid confusion with knarr-runtime's PathUtils - Inline ComparisonInterceptorVisitor logic in GaletteAgent to avoid NoClassDefFoundError (internal.transform classes not in jlink image) - Remove interception from GaletteTransformer (handled by second pass) - Update PathConstraintAPI to reference new class location The jlink image is built from clean galette-instrument (pre-interception) and only the runtime agent JAR contains interception support. Note: execution currently hangs during first iteration - likely a classloading deadlock from intercepting too many framework classes. Needs exclusion list tuning. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 007f350 commit 1c0d4ff

5 files changed

Lines changed: 461 additions & 279 deletions

File tree

galette-agent/src/main/java/edu/neu/ccs/prl/galette/PathConstraintAPI.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ public class PathConstraintAPI {
1515
*/
1616
public static List<?> getCurrentConstraints() {
1717
try {
18-
Class<?> pathUtilsClass = Class.forName("edu.neu.ccs.prl.galette.internal.runtime.PathUtils");
18+
Class<?> pathUtilsClass = Class.forName("edu.neu.ccs.prl.galette.interception.InterceptionPathUtils");
1919
java.lang.reflect.Method getCurrentMethod = pathUtilsClass.getMethod("getCurrent");
2020
return (List<?>) getCurrentMethod.invoke(null);
2121
} catch (Exception e) {
@@ -30,7 +30,7 @@ public static List<?> getCurrentConstraints() {
3030
*/
3131
public static List<?> flushConstraints() {
3232
try {
33-
Class<?> pathUtilsClass = Class.forName("edu.neu.ccs.prl.galette.internal.runtime.PathUtils");
33+
Class<?> pathUtilsClass = Class.forName("edu.neu.ccs.prl.galette.interception.InterceptionPathUtils");
3434
java.lang.reflect.Method flushMethod = pathUtilsClass.getMethod("flush");
3535
return (List<?>) flushMethod.invoke(null);
3636
} catch (Exception e) {
@@ -45,7 +45,7 @@ public static List<?> flushConstraints() {
4545
*/
4646
public static boolean isAvailable() {
4747
try {
48-
Class.forName("edu.neu.ccs.prl.galette.internal.runtime.PathUtils");
48+
Class.forName("edu.neu.ccs.prl.galette.interception.InterceptionPathUtils");
4949
return true;
5050
} catch (ClassNotFoundException e) {
5151
return false;

galette-agent/src/main/java/edu/neu/ccs/prl/galette/internal/runtime/PathUtils.java renamed to galette-agent/src/main/java/edu/neu/ccs/prl/galette/interception/InterceptionPathUtils.java

Lines changed: 51 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package edu.neu.ccs.prl.galette.internal.runtime;
1+
package edu.neu.ccs.prl.galette.interception;
22

33
import java.util.ArrayList;
44
import java.util.List;
@@ -11,7 +11,7 @@
1111
*
1212
* Collected constraints are retrieved via flush() by GalettePathConstraintBridge in knarr-runtime.
1313
*/
14-
public final class PathUtils {
14+
public final class InterceptionPathUtils {
1515

1616
private static volatile boolean enabled =
1717
"true".equals(System.getProperty("galette.concolic.interception.enabled"));
@@ -45,7 +45,9 @@ public static int instrumentedLcmp(long v1, long v2) {
4545
PATH_CONDITIONS.get().add(new Constraint(v1, v2, "LCMP", result));
4646
}
4747
return result;
48-
} finally { exitMethod(); }
48+
} finally {
49+
exitMethod();
50+
}
4951
}
5052

5153
public static int instrumentedFcmpl(float v1, float v2) {
@@ -56,7 +58,9 @@ public static int instrumentedFcmpl(float v1, float v2) {
5658
PATH_CONDITIONS.get().add(new Constraint(v1, v2, "FCMPL", result));
5759
}
5860
return result;
59-
} finally { exitMethod(); }
61+
} finally {
62+
exitMethod();
63+
}
6064
}
6165

6266
public static int instrumentedFcmpg(float v1, float v2) {
@@ -67,7 +71,9 @@ public static int instrumentedFcmpg(float v1, float v2) {
6771
PATH_CONDITIONS.get().add(new Constraint(v1, v2, "FCMPG", result));
6872
}
6973
return result;
70-
} finally { exitMethod(); }
74+
} finally {
75+
exitMethod();
76+
}
7177
}
7278

7379
public static int instrumentedDcmpl(double v1, double v2) {
@@ -78,7 +84,9 @@ public static int instrumentedDcmpl(double v1, double v2) {
7884
PATH_CONDITIONS.get().add(new Constraint(v1, v2, "DCMPL", result));
7985
}
8086
return result;
81-
} finally { exitMethod(); }
87+
} finally {
88+
exitMethod();
89+
}
8290
}
8391

8492
public static int instrumentedDcmpg(double v1, double v2) {
@@ -89,43 +97,67 @@ public static int instrumentedDcmpg(double v1, double v2) {
8997
PATH_CONDITIONS.get().add(new Constraint(v1, v2, "DCMPG", result));
9098
}
9199
return result;
92-
} finally { exitMethod(); }
100+
} finally {
101+
exitMethod();
102+
}
93103
}
94104

95105
public static boolean instrumentedIcmpJump(int v1, int v2, String op) {
96106
enterMethod();
97107
try {
98108
boolean result;
99109
switch (op) {
100-
case "EQ": result = v1 == v2; break;
101-
case "NE": result = v1 != v2; break;
102-
case "LT": result = v1 < v2; break;
103-
case "GE": result = v1 >= v2; break;
104-
case "GT": result = v1 > v2; break;
105-
case "LE": result = v1 <= v2; break;
106-
default: result = false;
110+
case "EQ":
111+
result = v1 == v2;
112+
break;
113+
case "NE":
114+
result = v1 != v2;
115+
break;
116+
case "LT":
117+
result = v1 < v2;
118+
break;
119+
case "GE":
120+
result = v1 >= v2;
121+
break;
122+
case "GT":
123+
result = v1 > v2;
124+
break;
125+
case "LE":
126+
result = v1 <= v2;
127+
break;
128+
default:
129+
result = false;
107130
}
108131
if (isEnabled()) {
109132
PATH_CONDITIONS.get().add(new Constraint(v1, v2, op, result ? 1 : 0));
110133
}
111134
return result;
112-
} finally { exitMethod(); }
135+
} finally {
136+
exitMethod();
137+
}
113138
}
114139

115140
public static boolean instrumentedAcmpJump(Object v1, Object v2, String op) {
116141
enterMethod();
117142
try {
118143
boolean result;
119144
switch (op) {
120-
case "ACMP_EQ": result = v1 == v2; break;
121-
case "ACMP_NE": result = v1 != v2; break;
122-
default: result = false;
145+
case "ACMP_EQ":
146+
result = v1 == v2;
147+
break;
148+
case "ACMP_NE":
149+
result = v1 != v2;
150+
break;
151+
default:
152+
result = false;
123153
}
124154
if (isEnabled()) {
125155
PATH_CONDITIONS.get().add(new Constraint(v1, v2, op, result ? 1 : 0));
126156
}
127157
return result;
128-
} finally { exitMethod(); }
158+
} finally {
159+
exitMethod();
160+
}
129161
}
130162

131163
// ===== Access methods (called by GalettePathConstraintBridge via PathConstraintAPI) =====

galette-agent/src/main/java/edu/neu/ccs/prl/galette/internal/agent/GaletteAgent.java

Lines changed: 164 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@
1010
import java.lang.instrument.ClassFileTransformer;
1111
import java.lang.instrument.Instrumentation;
1212
import java.security.ProtectionDomain;
13+
import org.objectweb.asm.*;
1314

1415
public final class GaletteAgent {
1516
static {
16-
// Thread should be safe to initialize at this point; initialize the spare frame store
1717
SpareFrameStore.initialize();
1818
}
1919

@@ -32,6 +32,10 @@ public static void premain(String agentArgs, Instrumentation inst) throws IOExce
3232
TransformationCache cache = cachePath == null ? null : new TransformationCache(new File(cachePath));
3333
GaletteTransformer.setCache(cache);
3434
inst.addTransformer(new TransformerWrapper());
35+
// Register comparison interception as a second-pass transformer.
36+
if (Boolean.getBoolean("galette.concolic.interception.enabled")) {
37+
inst.addTransformer(new ComparisonInterceptionTransformer());
38+
}
3539
}
3640

3741
private static final class TransformerWrapper implements ClassFileTransformer {
@@ -42,23 +46,175 @@ public byte[] transform(
4246
ClassLoader loader,
4347
String className,
4448
Class<?> classBeingRedefined,
45-
ProtectionDomain protectionDomain,
46-
byte[] classFileBuffer,
49+
ProtectionDomain pd,
50+
byte[] buf,
4751
TagFrame frame) {
48-
return transform(loader, className, classBeingRedefined, protectionDomain, classFileBuffer);
52+
return transform(loader, className, classBeingRedefined, pd, buf);
4953
}
5054

5155
@Override
56+
public byte[] transform(
57+
ClassLoader loader, String className, Class<?> classBeingRedefined, ProtectionDomain pd, byte[] buf) {
58+
if (classBeingRedefined != null) return null;
59+
return transformer.transform(buf, false);
60+
}
61+
}
62+
63+
/**
64+
* Second-pass transformer that intercepts comparison bytecodes in application classes.
65+
* All interception logic is inlined here to avoid loading classes from internal.transform
66+
* (which may not exist in the jlink image).
67+
*/
68+
private static final class ComparisonInterceptionTransformer implements ClassFileTransformer {
69+
private static final String PATH_UTILS = "edu/neu/ccs/prl/galette/interception/InterceptionPathUtils";
70+
71+
@SuppressWarnings("unused")
5272
public byte[] transform(
5373
ClassLoader loader,
5474
String className,
5575
Class<?> classBeingRedefined,
56-
ProtectionDomain protectionDomain,
57-
byte[] classFileBuffer) {
58-
if (classBeingRedefined != null) {
76+
ProtectionDomain pd,
77+
byte[] buf,
78+
TagFrame frame) {
79+
return transform(loader, className, classBeingRedefined, pd, buf);
80+
}
81+
82+
@Override
83+
public byte[] transform(
84+
ClassLoader loader, String className, Class<?> classBeingRedefined, ProtectionDomain pd, byte[] buf) {
85+
if (classBeingRedefined != null || className == null || isExcluded(className)) return null;
86+
try {
87+
ClassReader cr = new ClassReader(buf);
88+
ClassWriter cw = new ClassWriter(cr, ClassWriter.COMPUTE_MAXS);
89+
cr.accept(new InterceptionClassVisitor(cw), ClassReader.EXPAND_FRAMES);
90+
return cw.toByteArray();
91+
} catch (Throwable t) {
5992
return null;
6093
}
61-
return transformer.transform(classFileBuffer, false);
94+
}
95+
96+
private static boolean isExcluded(String cn) {
97+
return cn.startsWith("java/")
98+
|| cn.startsWith("javax/")
99+
|| cn.startsWith("sun/")
100+
|| cn.startsWith("jdk/")
101+
|| cn.startsWith("com/sun/")
102+
|| cn.startsWith("edu/neu/ccs/prl/galette/internal/")
103+
|| cn.startsWith("edu/neu/ccs/prl/galette/concolic/")
104+
|| cn.startsWith("za/ac/sun/cs/green/")
105+
|| cn.startsWith("edu/gmu/swe/")
106+
|| cn.startsWith("org/objectweb/asm/")
107+
|| cn.startsWith("org/eclipse/")
108+
|| cn.startsWith("tools/vitruv/")
109+
|| cn.startsWith("com/google/");
110+
}
111+
112+
/** Inlined ClassVisitor that intercepts comparison bytecodes. */
113+
private static final class InterceptionClassVisitor extends ClassVisitor {
114+
InterceptionClassVisitor(ClassVisitor cv) {
115+
super(Opcodes.ASM9, cv);
116+
}
117+
118+
@Override
119+
public MethodVisitor visitMethod(int access, String name, String desc, String sig, String[] ex) {
120+
MethodVisitor mv = super.visitMethod(access, name, desc, sig, ex);
121+
return new InterceptionMethodVisitor(mv);
122+
}
123+
}
124+
125+
/** Inlined MethodVisitor that replaces comparison instructions with PathUtils calls. */
126+
private static final class InterceptionMethodVisitor extends MethodVisitor {
127+
InterceptionMethodVisitor(MethodVisitor mv) {
128+
super(Opcodes.ASM9, mv);
129+
}
130+
131+
@Override
132+
public void visitInsn(int opcode) {
133+
switch (opcode) {
134+
case Opcodes.LCMP:
135+
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedLcmp", "(JJ)I", false);
136+
break;
137+
case Opcodes.FCMPL:
138+
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedFcmpl", "(FF)I", false);
139+
break;
140+
case Opcodes.FCMPG:
141+
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedFcmpg", "(FF)I", false);
142+
break;
143+
case Opcodes.DCMPL:
144+
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedDcmpl", "(DD)I", false);
145+
break;
146+
case Opcodes.DCMPG:
147+
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedDcmpg", "(DD)I", false);
148+
break;
149+
default:
150+
super.visitInsn(opcode);
151+
}
152+
}
153+
154+
@Override
155+
public void visitJumpInsn(int opcode, Label label) {
156+
switch (opcode) {
157+
case Opcodes.IF_ICMPEQ:
158+
case Opcodes.IF_ICMPNE:
159+
case Opcodes.IF_ICMPLT:
160+
case Opcodes.IF_ICMPGE:
161+
case Opcodes.IF_ICMPGT:
162+
case Opcodes.IF_ICMPLE:
163+
mv.visitLdcInsn(opToString(opcode));
164+
mv.visitMethodInsn(
165+
Opcodes.INVOKESTATIC,
166+
PATH_UTILS,
167+
"instrumentedIcmpJump",
168+
"(IILjava/lang/String;)Z",
169+
false);
170+
mv.visitJumpInsn(Opcodes.IFNE, label);
171+
break;
172+
case Opcodes.IFEQ:
173+
case Opcodes.IFNE:
174+
case Opcodes.IFLT:
175+
case Opcodes.IFGE:
176+
case Opcodes.IFGT:
177+
case Opcodes.IFLE:
178+
// Single-operand: push 0 and use two-operand version
179+
mv.visitInsn(Opcodes.ICONST_0);
180+
mv.visitLdcInsn(opToString(opcode));
181+
mv.visitMethodInsn(
182+
Opcodes.INVOKESTATIC,
183+
PATH_UTILS,
184+
"instrumentedIcmpJump",
185+
"(IILjava/lang/String;)Z",
186+
false);
187+
mv.visitJumpInsn(Opcodes.IFNE, label);
188+
break;
189+
default:
190+
super.visitJumpInsn(opcode, label);
191+
}
192+
}
193+
194+
private static String opToString(int opcode) {
195+
switch (opcode) {
196+
case Opcodes.IF_ICMPEQ:
197+
case Opcodes.IFEQ:
198+
return "EQ";
199+
case Opcodes.IF_ICMPNE:
200+
case Opcodes.IFNE:
201+
return "NE";
202+
case Opcodes.IF_ICMPLT:
203+
case Opcodes.IFLT:
204+
return "LT";
205+
case Opcodes.IF_ICMPGE:
206+
case Opcodes.IFGE:
207+
return "GE";
208+
case Opcodes.IF_ICMPGT:
209+
case Opcodes.IFGT:
210+
return "GT";
211+
case Opcodes.IF_ICMPLE:
212+
case Opcodes.IFLE:
213+
return "LE";
214+
default:
215+
return "UNKNOWN";
216+
}
217+
}
62218
}
63219
}
64220
}

galette-agent/src/main/java/edu/neu/ccs/prl/galette/internal/transform/GaletteTransformer.java

Lines changed: 3 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -136,21 +136,9 @@ private byte[] transform(ClassReader cr, boolean propagate, boolean isHostedAnon
136136
// Remove computed frames
137137
ClassVisitor cv = hasFrames ? cw : new FrameRemover(cw);
138138

139-
// Add comparison interception for bytecode-level constraint collection.
140-
// Only enabled when explicitly requested via system property.
141-
// At jlink time the property is not set, so JDK classes are not intercepted.
142-
// At runtime the agent reads the property and intercepts application classes.
143-
if (Boolean.getBoolean("galette.concolic.interception.enabled")
144-
&& !cn.name.startsWith("edu/neu/ccs/prl/galette/internal/")) {
145-
// For application classes (not JDK/internal), also intercept single-operand jumps
146-
// (IFEQ/IFLT/etc.) which capture comparisons like `if (x < 0)`.
147-
boolean isApplicationClass = !cn.name.startsWith("java/")
148-
&& !cn.name.startsWith("javax/")
149-
&& !cn.name.startsWith("sun/")
150-
&& !cn.name.startsWith("jdk/")
151-
&& !cn.name.startsWith("com/sun/");
152-
cv = new ComparisonInterceptorVisitor(cv, isApplicationClass);
153-
}
139+
// NOTE: Comparison interception is handled by ComparisonInterceptionTransformer
140+
// registered as a second-pass transformer in GaletteAgent.premain().
141+
// This keeps the jlink image clean (no interception baked in).
154142

155143
// Make the members of certain classes publicly accessible
156144
if (AccessModifier.isApplicable(cn.name)) {

0 commit comments

Comments
 (0)