Skip to content

Commit 4ae26f4

Browse files
AnneKoziolekclaude
AnneKoziolek
and
claude
committed
Native bytecode interception working end-to-end with Vitruvius
Use DUP+void-record approach instead of replacing comparison instructions: - DUP2 before IF_ICMP* to duplicate operands - DUP + ICONST_0 before IFEQ/IFLT/etc. for single-operand comparisons - Call recordIcmp(int,int,String)V to observe without changing behavior - Original comparison instruction executes unchanged This preserves the exact stack layout, so stack map frames remain valid and no frame recomputation (COMPUTE_FRAMES/getCommonSuperClass) is needed. Results: 5 paths explored with native interception enabled. 256-273 raw constraints collected per iteration. Constraint filtering needs tuning (too many framework comparisons captured alongside the target threshold comparisons). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent c1ad7ba commit 4ae26f4

2 files changed

Lines changed: 76 additions & 50 deletions

File tree

‎galette-agent/src/main/java/edu/neu/ccs/prl/galette/interception/InterceptionPathUtils.java‎

Lines changed: 42 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,7 @@ public final class InterceptionPathUtils {
1616
private static volatile boolean enabled =
1717
"true".equals(System.getProperty("galette.concolic.interception.enabled"));
1818

19-
static {
20-
System.out.println("[InterceptionPathUtils] loaded, enabled=" + enabled);
21-
}
19+
// No static initializer side effects — must be jlink-safe
2220

2321
private static final ThreadLocal<List<Constraint>> PATH_CONDITIONS = ThreadLocal.withInitial(ArrayList::new);
2422

@@ -106,9 +104,48 @@ public static int instrumentedDcmpg(double v1, double v2) {
106104
}
107105
}
108106

107+
/**
108+
* Record an integer comparison without affecting the result.
109+
* Called via DUP2 before the original IF_ICMP* instruction,
110+
* so the stack layout is preserved exactly.
111+
*/
112+
public static void recordIcmp(int v1, int v2, String op) {
113+
if (!enabled) return;
114+
enterMethod();
115+
try {
116+
if (isEnabled()) {
117+
// Compute the result based on the operation
118+
int result;
119+
switch (op) {
120+
case "EQ":
121+
result = (v1 == v2) ? 1 : 0;
122+
break;
123+
case "NE":
124+
result = (v1 != v2) ? 1 : 0;
125+
break;
126+
case "LT":
127+
result = (v1 < v2) ? 1 : 0;
128+
break;
129+
case "GE":
130+
result = (v1 >= v2) ? 1 : 0;
131+
break;
132+
case "GT":
133+
result = (v1 > v2) ? 1 : 0;
134+
break;
135+
case "LE":
136+
result = (v1 <= v2) ? 1 : 0;
137+
break;
138+
default:
139+
result = 0;
140+
}
141+
PATH_CONDITIONS.get().add(new Constraint(v1, v2, op, result));
142+
}
143+
} finally {
144+
exitMethod();
145+
}
146+
}
147+
109148
public static boolean instrumentedIcmpJump(int v1, int v2, String op) {
110-
System.out.println("[InterceptionPathUtils] instrumentedIcmpJump called: " + v1 + " " + op + " " + v2
111-
+ " enabled=" + enabled);
112149
enterMethod();
113150
try {
114151
boolean result;

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

Lines changed: 34 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -93,24 +93,13 @@ public byte[] transform(
9393
ClassLoader loader, String className, Class<?> classBeingRedefined, ProtectionDomain pd, byte[] buf) {
9494
if (classBeingRedefined != null || className == null || isExcluded(className)) return null;
9595
try {
96+
// DUP+void-record preserves stack layout, so frames stay valid.
97+
// COMPUTE_MAXS recalculates max stack for the extra DUP2+LDC slots.
9698
ClassReader cr = new ClassReader(buf);
97-
// Use COMPUTE_MAXS to fix max stack/locals. Pass 0 to accept()
98-
// to preserve existing stack map frames from the first pass.
99-
ClassWriter cw = new ClassWriter(cr, ClassWriter.COMPUTE_MAXS) {
100-
@Override
101-
protected String getCommonSuperClass(String type1, String type2) {
102-
return "java/lang/Object";
103-
}
104-
};
99+
ClassWriter cw = new ClassWriter(cr, ClassWriter.COMPUTE_MAXS);
105100
cr.accept(new InterceptionClassVisitor(cw), 0);
106-
byte[] result = cw.toByteArray();
107-
if (result.length != buf.length) {
108-
System.out.println("[Interception2ndPass] Modified: " + className + " (" + buf.length + " -> "
109-
+ result.length + ")");
110-
}
111-
return result;
101+
return cw.toByteArray();
112102
} catch (Throwable t) {
113-
System.err.println("[Interception2ndPass] ERROR: " + className + ": " + t);
114103
return null;
115104
}
116105
}
@@ -138,33 +127,20 @@ public MethodVisitor visitMethod(int access, String name, String desc, String si
138127
}
139128
}
140129

141-
/** Inlined MethodVisitor that replaces comparison instructions with PathUtils calls. */
130+
/**
131+
* Observes comparison instructions by duplicating operands and recording them
132+
* via a void method BEFORE the original instruction executes unchanged.
133+
* This preserves the exact stack layout — no frame invalidation.
134+
*/
142135
private static final class InterceptionMethodVisitor extends MethodVisitor {
143136
InterceptionMethodVisitor(MethodVisitor mv) {
144137
super(Opcodes.ASM9, mv);
145138
}
146139

147140
@Override
148-
public void visitInsn(int opcode) {
149-
switch (opcode) {
150-
case Opcodes.LCMP:
151-
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedLcmp", "(JJ)I", false);
152-
break;
153-
case Opcodes.FCMPL:
154-
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedFcmpl", "(FF)I", false);
155-
break;
156-
case Opcodes.FCMPG:
157-
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedFcmpg", "(FF)I", false);
158-
break;
159-
case Opcodes.DCMPL:
160-
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedDcmpl", "(DD)I", false);
161-
break;
162-
case Opcodes.DCMPG:
163-
mv.visitMethodInsn(Opcodes.INVOKESTATIC, PATH_UTILS, "instrumentedDcmpg", "(DD)I", false);
164-
break;
165-
default:
166-
super.visitInsn(opcode);
167-
}
141+
public void visitMaxs(int maxStack, int maxLocals) {
142+
// DUP2 + LDC adds 3 extra stack slots temporarily
143+
super.visitMaxs(maxStack + 3, maxLocals);
168144
}
169145

170146
@Override
@@ -176,23 +152,36 @@ public void visitJumpInsn(int opcode, Label label) {
176152
case Opcodes.IF_ICMPGE:
177153
case Opcodes.IF_ICMPGT:
178154
case Opcodes.IF_ICMPLE:
155+
// Two-operand: Stack [v1, v2] → DUP2 → record → original
156+
mv.visitInsn(Opcodes.DUP2);
179157
mv.visitLdcInsn(opToString(opcode));
180158
mv.visitMethodInsn(
181-
Opcodes.INVOKESTATIC,
182-
PATH_UTILS,
183-
"instrumentedIcmpJump",
184-
"(IILjava/lang/String;)Z",
185-
false);
186-
mv.visitJumpInsn(Opcodes.IFNE, label);
159+
Opcodes.INVOKESTATIC, PATH_UTILS, "recordIcmp", "(IILjava/lang/String;)V", false);
160+
super.visitJumpInsn(opcode, label);
161+
break;
162+
case Opcodes.IFEQ:
163+
case Opcodes.IFNE:
164+
case Opcodes.IFLT:
165+
case Opcodes.IFGE:
166+
case Opcodes.IFGT:
167+
case Opcodes.IFLE:
168+
// Single-operand: Stack [v] → DUP, ICONST_0, LDC → record(v,0,op) → original
169+
mv.visitInsn(Opcodes.DUP);
170+
mv.visitInsn(Opcodes.ICONST_0);
171+
mv.visitLdcInsn(opToString(opcode));
172+
mv.visitMethodInsn(
173+
Opcodes.INVOKESTATIC, PATH_UTILS, "recordIcmp", "(IILjava/lang/String;)V", false);
174+
super.visitJumpInsn(opcode, label);
187175
break;
188-
// Single-operand jumps (IFEQ/IFNE/IFLT/IFGE/IFGT/IFLE) are NOT
189-
// intercepted: they are ubiquitous in bytecode (boolean checks,
190-
// null checks, loop counters) and produce massive constraint noise.
191176
default:
192177
super.visitJumpInsn(opcode, label);
193178
}
194179
}
195180

181+
// LCMP/DCMPL etc. could be observed similarly with DUP2/DUP2_X2,
182+
// but for now we focus on IF_ICMP* which covers the integer comparisons
183+
// in the brake reactions.
184+
196185
private static String opToString(int opcode) {
197186
switch (opcode) {
198187
case Opcodes.IF_ICMPEQ:

0 commit comments

Comments
 (0)