@@ -46,6 +46,12 @@ public class GaletteSymbolicator {
4646 */
4747 public static final boolean DEBUG = true ; // Boolean.valueOf(System.getProperty("DEBUG", "false"));
4848
49+ /**
50+ * Manual mode flag - when true, Tag verification is skipped.
51+ * This is used when running with PathUtils API instead of javaagent instrumentation.
52+ */
53+ public static final boolean MANUAL_MODE = Boolean .valueOf (System .getProperty ("skip.instrumentation.check" , "false" ));
54+
4955 /**
5056 * Internal class name for bytecode instrumentation.
5157 */
@@ -78,6 +84,13 @@ public class GaletteSymbolicator {
7884 */
7985 private static final ConcurrentHashMap <String , Tag > labelToTag = new ConcurrentHashMap <>();
8086
87+ /**
88+ * ThreadLocal mapping from concrete values to their qualified names.
89+ * Used for hybrid constraint collection when Tag propagation fails.
90+ * This enables symbolicVitruviusChoice to infer variable names.
91+ */
92+ private static final ThreadLocal <Map <Integer , String >> valueToQualifiedName = ThreadLocal .withInitial (HashMap ::new );
93+
8194 static {
8295 initializeSymbolicator ();
8396 }
@@ -168,11 +181,15 @@ public static Integer getOrMakeSymbolicInt(String qualifiedName, int concreteVal
168181 + " = " + concreteValue );
169182 }
170183
171- // CRITICAL FIX: Re-record constraints even when reusing tag!
172- // PathUtils.resetPC() clears constraints between iterations, so we must re-add them
173- // Both domain and switch constraints are needed for PathExplorer
184+ // HYBRID: Record domain constraint here
185+ // Switch constraint will be added by symbolicVitruviusChoice
174186 PathUtils .addIntDomainConstraint (qualifiedName , min , max + 1 );
175- PathUtils .addSwitchConstraint (qualifiedName , concreteValue );
187+
188+ // Register value-to-name mapping for hybrid inference
189+ valueToQualifiedName .get ().put (concreteValue , qualifiedName );
190+
191+ // Remove manual switch constraint (let symbolicVitruviusChoice handle it)
192+ // PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
176193
177194 if (DEBUG ) {
178195 System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Re-recorded constraints:" );
@@ -183,17 +200,21 @@ public static Integer getOrMakeSymbolicInt(String qualifiedName, int concreteVal
183200 // Apply the tag to the value and return
184201 Integer taggedValue = Tainter .setTag (concreteValue , existingTag );
185202
186- // Debug: Verify the tag was actually applied
187- Tag verifyTag = Tainter .getTag (taggedValue );
188- if (verifyTag == null ) {
189- System .err .println (
190- "[GaletteSymbolicator:getOrMakeSymbolicInt] WARNING: Reused tag was not applied!" );
191- System .err .println (" Instrumentation may not be working. Check that Galette agent is loaded." );
192- } else {
193- if (DEBUG ) {
194- System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Verified reused tag applied: "
195- + verifyTag .getLabels ()[0 ]);
203+ // Debug: Verify the tag was actually applied (skip in manual mode)
204+ if (!MANUAL_MODE ) {
205+ Tag verifyTag = Tainter .getTag (taggedValue );
206+ if (verifyTag == null ) {
207+ System .err .println (
208+ "[GaletteSymbolicator:getOrMakeSymbolicInt] WARNING: Reused tag was not applied!" );
209+ System .err .println (" Instrumentation may not be working. Check that Galette agent is loaded." );
210+ } else {
211+ if (DEBUG ) {
212+ System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Verified reused tag applied: "
213+ + verifyTag .getLabels ()[0 ]);
214+ }
196215 }
216+ } else if (DEBUG ) {
217+ System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Manual mode: Skipping tag verification for reused tag" );
197218 }
198219
199220 return taggedValue ;
@@ -208,13 +229,16 @@ public static Integer getOrMakeSymbolicInt(String qualifiedName, int concreteVal
208229 // Store for reuse in future iterations
209230 labelToTag .put (qualifiedName , newTag );
210231
211- // Record domain constraint [min, max] (only on first iteration)
232+ // HYBRID: Record domain constraint here
233+ // Switch constraint will be added by symbolicVitruviusChoice
212234 // Note: PathUtils.addIntDomainConstraint uses exclusive upper bound
213235 PathUtils .addIntDomainConstraint (qualifiedName , min , max + 1 );
214236
215- // CRITICAL: Also record the switch constraint for this specific value
216- // This is needed for path exploration to generate alternative inputs
217- PathUtils .addSwitchConstraint (qualifiedName , concreteValue );
237+ // Register value-to-name mapping for hybrid inference
238+ valueToQualifiedName .get ().put (concreteValue , qualifiedName );
239+
240+ // Remove manual switch constraint (let symbolicVitruviusChoice handle it)
241+ // PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
218242
219243 if (DEBUG ) {
220244 System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Created new tag for: " + qualifiedName
@@ -226,11 +250,15 @@ public static Integer getOrMakeSymbolicInt(String qualifiedName, int concreteVal
226250 // Apply the tag to the value and return
227251 Integer taggedValue = Tainter .setTag (concreteValue , newTag );
228252
229- // Debug: Verify the tag was actually applied
230- Tag verifyTag = Tainter .getTag (taggedValue );
231- if (verifyTag == null ) {
232- System .err .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] WARNING: New tag was not applied!" );
233- System .err .println (" Instrumentation may not be working. Check that Galette agent is loaded." );
253+ // Debug: Verify the tag was actually applied (skip in manual mode)
254+ if (!MANUAL_MODE ) {
255+ Tag verifyTag = Tainter .getTag (taggedValue );
256+ if (verifyTag == null ) {
257+ System .err .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] WARNING: New tag was not applied!" );
258+ System .err .println (" Instrumentation may not be working. Check that Galette agent is loaded." );
259+ }
260+ } else if (DEBUG ) {
261+ System .out .println ("[GaletteSymbolicator:getOrMakeSymbolicInt] Manual mode: Skipping tag verification" );
234262 }
235263
236264 return taggedValue ;
@@ -672,13 +700,43 @@ public static InputSolution sendConstraintToServer(Expression constraint) {
672700 }
673701 }
674702
703+ /**
704+ * Get qualified name for a concrete value (for hybrid constraint collection).
705+ * This is used by symbolicVitruviusChoice to auto-infer variable names
706+ * when Tag propagation fails.
707+ *
708+ * @param value The concrete value
709+ * @return Qualified name, or null if not found
710+ */
711+ public static String getQualifiedNameForValue (int value ) {
712+ String name = valueToQualifiedName .get ().get (value );
713+ if (DEBUG && name != null ) {
714+ System .out .println (
715+ "[GaletteSymbolicator:getQualifiedNameForValue] Resolved value " + value + " -> " + name );
716+ }
717+ return name ;
718+ }
719+
720+ /**
721+ * Clear value-to-name mapping at the end of each iteration.
722+ * This is called by PathExplorer after each iteration.
723+ */
724+ public static void clearValueMapping () {
725+ Map <Integer , String > map = valueToQualifiedName .get ();
726+ if (DEBUG && !map .isEmpty ()) {
727+ System .out .println ("[GaletteSymbolicator:clearValueMapping] Clearing " + map .size () + " value mappings" );
728+ }
729+ map .clear ();
730+ }
731+
675732 /**
676733 * Reset the symbolicator state.
677734 */
678735 public static void reset () {
679736 valueToTag .clear ();
680737 tagToExpression .clear ();
681738 labelToTag .clear (); // Clear label-to-tag mappings for tag reuse
739+ clearValueMapping (); // Also clear value-to-name mapping
682740 mySoln = null ;
683741 GaletteGreenBridge .clearVariableCache ();
684742 PathUtils .reset ();
0 commit comments