Modify bytecode injection logic for the new model checking algorithm

bootstrap/src/sun/nio/ch/lincheck/EventTracker.java

@@ -39,19 +39,24 @@ public interface EventTracker {
 
     void updateSnapshotBeforeConstructorCall(Object[] objs);
 
-    boolean beforeReadField(Object obj, String className, String fieldName, int codeLocation,
+    boolean beforeReadField(Object obj, String className, String fieldName, Type fieldType,
+                            int codeLocation,
                             boolean isStatic, boolean isFinal);
-    boolean beforeReadArrayElement(Object array, int index, int codeLocation);
+    boolean beforeReadArrayElement(Object array, int index, Type arrayElementType, int codeLocation);
     void afterRead(Object value);
+    Object interceptReadResult();
 
-    boolean beforeWriteField(Object obj, String className, String fieldName, Object value, int codeLocation,
+    boolean beforeWriteField(Object obj, String className, String fieldName, Type fieldType, Object value,
+                             int codeLocation,
                              boolean isStatic, boolean isFinal);
-    boolean beforeWriteArrayElement(Object array, int index, Object value, int codeLocation);
+    boolean beforeWriteArrayElement(Object array, int index, Type arrayElementType, Object value,
+                                    int codeLocation);
     void afterWrite();
 
-    void beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params);
+    boolean beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params);
     void onMethodCallReturn(Object result);
     void onMethodCallException(Throwable t);
+    Object interceptMethodCallResult();
 
     Random getThreadLocalRandom();
     int randomNextInt();

bootstrap/src/sun/nio/ch/lincheck/Injections.java

@@ -317,20 +317,26 @@ public static boolean isRandom(Object any) {
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeReadField(Object obj, String className, String fieldName, int codeLocation,
+    public static boolean beforeReadField(Object obj, String className, String fieldName, int fieldType,
+                                          int codeLocation,
                                           boolean isStatic, boolean isFinal) {
         if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadField(obj, className, fieldName, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeReadField(obj, className, fieldName, Type.getType(fieldType),
+                codeLocation, isStatic, isFinal
+        );
     }
 
     /**
      * Called from the instrumented code before any array cell read.
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeReadArray(Object array, int index, int codeLocation) {
+    public static boolean beforeReadArray(Object array, int index, int arrayElementType,
+                                          int codeLocation) {
         if (array == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadArrayElement(array, index, codeLocation);
+        return getEventTracker().beforeReadArrayElement(array, index, Type.getType(arrayElementType),
+                codeLocation
+        );
     }
 
     /**
@@ -340,25 +346,41 @@ public static void afterRead(Object value) {
         getEventTracker().afterRead(value);
     }
 
+    /**
+     * Called from the instrumented code to intercept and substitute the result of a read operation
+     * (if reads interception is enabled).
+     *
+     * @return the substituted read result.
+     */
+    public static Object interceptReadResult() {
+        return getEventTracker().interceptReadResult();
+    }
+
     /**
      * Called from the instrumented code before each field write.
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeWriteField(Object obj, String className, String fieldName, Object value, int codeLocation,
+    public static boolean beforeWriteField(Object obj, String className, String fieldName, int fieldType, Object value,
+                                           int codeLocation,
                                            boolean isStatic, boolean isFinal) {
         if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeWriteField(obj, className, fieldName, value, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeWriteField(obj, className, fieldName, Type.getType(fieldType), value,
+                codeLocation, isStatic, isFinal
+        );
     }
 
     /**
      * Called from the instrumented code before any array cell write.
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeWriteArray(Object array, int index, Object value, int codeLocation) {
+    public static boolean beforeWriteArray(Object array, int index, int arrayElementType, Object value,
+                                           int codeLocation) {
         if (array == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeWriteArrayElement(array, index, value, codeLocation);
+        return getEventTracker().beforeWriteArrayElement(array, index, Type.getType(arrayElementType), value,
+                codeLocation
+        );
     }
 
     /**
@@ -372,9 +394,10 @@ public static void afterWrite() {
      * Called from the instrumented code before any method call.
      *
      * @param owner is `null` for public static methods.
+     * @return true if the method result should be intercepted.
      */
-    public static void beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params) {
-        getEventTracker().beforeMethodCall(owner, className, methodName, codeLocation, methodId, params);
+    public static boolean beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params) {
+        return getEventTracker().beforeMethodCall(owner, className, methodName, codeLocation, methodId, params);
     }
 
     /**
@@ -398,6 +421,16 @@ public static void onMethodCallException(Throwable t) {
         getEventTracker().onMethodCallException(t);
     }
 
+    /**
+     * Called from the instrumented code to intercept and substitute the result of a method call
+     * (if method results interception is enabled).
+     *
+     * @return The substituted result of the method call.
+     */
+    public static Object interceptMethodCallResult() {
+        return getEventTracker().interceptMethodCallResult();
+    }
+
     /**
      * Called from the instrumented code before NEW instruction
      */

bootstrap/src/sun/nio/ch/lincheck/Type.java

@@ -0,0 +1,72 @@
+/*
+ * Lincheck
+ *
+ * Copyright (C) 2019 - 2025 JetBrains s.r.o.
+ *
+ * This Source Code Form is subject to the terms of the
+ * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed
+ * with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+package sun.nio.ch.lincheck;
+
+/**
+ * Enumeration representing various value types that can be tracked and analyzed in Lincheck.
+ *
+ * <p>
+ * Note: this enumeration basically represents JVM types. 
+ * It is similar to {@code asm.Type} class from the ASM library.
+ * We do not use ASM class here, to avoid adding a dependency on ASM library to the bootstrap module.
+ * However, we rely on the fact that {@code asm.Type.sort == Type.ordinal()}.
+ */
+public enum Type {
+    VOID,
+    BOOLEAN,
+    CHAR,
+    BYTE,
+    SHORT,
+    INT,
+    FLOAT,
+    LONG,
+    DOUBLE,
+    ARRAY,
+    OBJECT;
+
+    /**
+     * Returns the {@code Type} corresponding to the specified integer value.
+     *
+     * @param sort the integer value representing the desired {@code Type}
+     * @return the {@code Type} corresponding to the given integer value.
+     * @throws IllegalArgumentException if the integer value is out of range.
+     */
+    static Type getType(int sort) {
+        switch (sort) {
+            case 0:  return VOID;
+            case 1:  return BOOLEAN;
+            case 2:  return CHAR;
+            case 3:  return BYTE;
+            case 4:  return SHORT;
+            case 5:  return INT;
+            case 6:  return FLOAT;
+            case 7:  return LONG;
+            case 8:  return DOUBLE;
+            case 9:  return ARRAY;
+            case 10: return OBJECT;
+            default: throw new IllegalArgumentException("Invalid sort value: " + sort);
+        }
+    }
+
+    /**
+     * Determines whether the given {@code Type} represents a primitive type.
+     */
+    static boolean isPrimitiveType(Type type) {
+        return type.ordinal() > VOID.ordinal() && type.ordinal() <= DOUBLE.ordinal();
+    }
+
+    /**
+     * Determines whether the specified {@code Type} is a reference type.
+     */
+    static boolean isReferenceType(Type type) {
+        return type == ARRAY || type == OBJECT;
+    }
+}

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt

@@ -102,8 +102,8 @@ abstract class Runner protected constructor(
      * Is invoked after each actor execution from the specified thread, even if a legal exception was thrown.
      * The invocations are inserted into the generated code.
      */
-    fun onActorFinish() {
-        strategy.onActorFinish()
+    fun onActorFinish(iThread: Int) {
+        strategy.onActorFinish(iThread)
     }
 
     fun beforePart(part: ExecutionPart) {

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java

@@ -38,7 +38,7 @@ public class TestThreadExecutionGenerator {
     private static final Method RUNNER_ON_THREAD_START_METHOD = new Method("onThreadStart", VOID_TYPE, new Type[]{INT_TYPE});
     private static final Method RUNNER_ON_THREAD_FINISH_METHOD = new Method("onThreadFinish", VOID_TYPE, new Type[]{INT_TYPE});
     private static final Method RUNNER_ON_ACTOR_START = new Method("onActorStart", Type.VOID_TYPE, new Type[]{ Type.INT_TYPE });
-    private static final Method RUNNER_ON_ACTOR_FINISH = new Method("onActorFinish", Type.VOID_TYPE, NO_ARGS);
+    private static final Method RUNNER_ON_ACTOR_FINISH = new Method("onActorFinish", Type.VOID_TYPE, new Type[]{ Type.INT_TYPE });
 
     private static final Type TEST_THREAD_EXECUTION_TYPE = getType(TestThreadExecution.class);
     private static final Method TEST_THREAD_EXECUTION_CONSTRUCTOR;
@@ -251,6 +251,7 @@ private static void generateRun(ClassVisitor cv, Type testType, int iThread, Lis
             // Invoke runner onActorFinish method
             mv.loadThis();
             mv.getField(TEST_THREAD_EXECUTION_TYPE, "runner", RUNNER_TYPE);
+            mv.push(iThread);
             mv.invokeVirtual(RUNNER_TYPE, RUNNER_ON_ACTOR_FINISH);
             // Increment the clock
             mv.loadThis();

src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt

@@ -97,7 +97,7 @@ abstract class Strategy protected constructor(
     /**
      * Is invoked after each actor execution, even if a legal exception was thrown
      */
-    open fun onActorFinish() {}
+    open fun onActorFinish(iThread: Int) {}
 
     /**
      * Closes the strategy and releases any resources associated with it.

src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt

@@ -20,6 +20,7 @@ import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
 import org.jetbrains.kotlinx.lincheck.transformation.*
 import org.jetbrains.kotlinx.lincheck.util.*
 import sun.nio.ch.lincheck.*
+import sun.nio.ch.lincheck.Type
 import kotlinx.coroutines.*
 import org.jetbrains.kotlinx.lincheck.strategy.managed.AtomicFieldUpdaterNames.getAtomicFieldUpdaterName
 import org.jetbrains.kotlinx.lincheck.strategy.managed.AtomicReferenceMethodType.*
@@ -75,6 +76,9 @@ abstract class ManagedStrategy(
     // Tracker of the thread parking.
     protected abstract val parkingTracker: ParkingTracker
 
+    // A flag indicating whether final fields should be tracked.
+    protected open val trackFinalFields: Boolean = false
+
     // Snapshot of the memory, reachable from static fields
     protected val staticMemorySnapshot = SnapshotTracker()
 
@@ -618,7 +622,7 @@ abstract class ManagedStrategy(
         enterTestingCode()
     }
 
-    override fun onActorFinish() {
+    override fun onActorFinish(iThread: Int) {
         // This is a hack to guarantee correct stepping in the plugin.
         // When stepping out to the TestThreadExecution class, stepping continues unproductively.
         // With this method, we force the debugger to stop at the beginning of the next actor.
@@ -910,7 +914,8 @@ abstract class ManagedStrategy(
     /**
      * Returns `true` if a switch point is created.
      */
-    override fun beforeReadField(obj: Any?, className: String, fieldName: String, codeLocation: Int,
+    override fun beforeReadField(obj: Any?, className: String, fieldName: String, fieldType: Type,
+                                 codeLocation: Int,
                                  isStatic: Boolean, isFinal: Boolean) = runInIgnoredSection {
          updateSnapshotOnFieldAccess(obj, className.canonicalClassName, fieldName)
         // We need to ensure all the classes related to the reading object are instrumented.
@@ -919,7 +924,7 @@ abstract class ManagedStrategy(
             LincheckJavaAgent.ensureClassHierarchyIsTransformed(className.canonicalClassName)
         }
         // Optimization: do not track final field reads
-        if (isFinal) {
+        if (isFinal && !trackFinalFields) {
             return@runInIgnoredSection false
         }
         // Do not track accesses to untracked objects
@@ -948,7 +953,8 @@ abstract class ManagedStrategy(
     }
 
     /** Returns <code>true</code> if a switch point is created. */
-    override fun beforeReadArrayElement(array: Any, index: Int, codeLocation: Int): Boolean = runInIgnoredSection {
+    override fun beforeReadArrayElement(array: Any, index: Int, arrayElementType: Type,
+                                        codeLocation: Int): Boolean = runInIgnoredSection {
         updateSnapshotOnArrayElementAccess(array, index)
         if (!objectTracker.shouldTrackObjectAccess(array)) {
             return@runInIgnoredSection false
@@ -983,15 +989,22 @@ abstract class ManagedStrategy(
         loopDetector.afterRead(value)
     }
 
-    override fun beforeWriteField(obj: Any?, className: String, fieldName: String, value: Any?, codeLocation: Int,
+    override fun interceptReadResult(): Any? = runInIgnoredSection {
+        // will be implemented in the new model checking strategy:
+        // https://github.com/JetBrains/lincheck/issues/257
+        throw UnsupportedOperationException()
+    }
+
+    override fun beforeWriteField(obj: Any?, className: String, fieldName: String, fieldType: Type, value: Any?,
+                                  codeLocation: Int,
                                   isStatic: Boolean, isFinal: Boolean): Boolean = runInIgnoredSection {
         updateSnapshotOnFieldAccess(obj, className.canonicalClassName, fieldName)
         objectTracker.registerObjectLink(fromObject = obj ?: StaticObject, toObject = value)
         if (!objectTracker.shouldTrackObjectAccess(obj ?: StaticObject)) {
             return@runInIgnoredSection false
         }
         // Optimization: do not track final field writes
-        if (isFinal) {
+        if (isFinal && !trackFinalFields) {
             return@runInIgnoredSection false
         }
         val iThread = threadScheduler.getCurrentThreadId()
@@ -1014,7 +1027,8 @@ abstract class ManagedStrategy(
         return@runInIgnoredSection true
     }
 
-    override fun beforeWriteArrayElement(array: Any, index: Int, value: Any?, codeLocation: Int): Boolean = runInIgnoredSection {
+    override fun beforeWriteArrayElement(array: Any, index: Int, fieldType: Type, value: Any?,
+                                         codeLocation: Int): Boolean = runInIgnoredSection {
         updateSnapshotOnArrayElementAccess(array, index)
         objectTracker.registerObjectLink(fromObject = array, toObject = value)
         if (!objectTracker.shouldTrackObjectAccess(array)) {
@@ -1133,7 +1147,7 @@ abstract class ManagedStrategy(
         codeLocation: Int,
         methodId: Int,
         params: Array<Any?>
-    ) {
+    ): Boolean {
         val guarantee = runInIgnoredSection {
             val iThread = threadScheduler.getCurrentThreadId()
             // re-throw abort error if the thread was aborted
@@ -1184,6 +1198,7 @@ abstract class ManagedStrategy(
             // so `enterIgnoredSection` would have no effect
             enterIgnoredSection()
         }
+        return false // shouldInterceptMethodResult
     }
 
     override fun onMethodCallReturn(result: Any?) {
@@ -1233,6 +1248,12 @@ abstract class ManagedStrategy(
         leaveIgnoredSection()
     }
 
+    override fun interceptMethodCallResult(): Any? = runInIgnoredSection {
+        // will be implemented in the new model checking strategy:
+        // https://github.com/JetBrains/lincheck/issues/257
+        throw UnsupportedOperationException()
+    }
+
     private fun isSuspendFunction(className: String, methodName: String, params: Array<Any?>): Boolean =
         try {
             getMethod(className.canonicalClassName, methodName, params)?.isSuspendable() ?: false