From 58d97b070670aa1f7a0a1e443db9995cbebe517d Mon Sep 17 00:00:00 2001 From: Evgeniy Moiseenko Date: Thu, 16 Jan 2025 20:18:19 +0100 Subject: [PATCH 1/4] add type argument to memory access injections Signed-off-by: Evgeniy Moiseenko --- .../src/sun/nio/ch/lincheck/EventTracker.java | 11 +-- .../src/sun/nio/ch/lincheck/Injections.java | 28 +++++--- bootstrap/src/sun/nio/ch/lincheck/Type.java | 72 +++++++++++++++++++ .../strategy/managed/ManagedStrategy.kt | 13 ++-- .../SharedMemoryAccessTransformer.kt | 34 +++++---- 5 files changed, 129 insertions(+), 29 deletions(-) create mode 100644 bootstrap/src/sun/nio/ch/lincheck/Type.java diff --git a/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java b/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java index 6d7b4b5d55..959f452782 100644 --- a/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java +++ b/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java @@ -39,14 +39,17 @@ 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); - 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); diff --git a/bootstrap/src/sun/nio/ch/lincheck/Injections.java b/bootstrap/src/sun/nio/ch/lincheck/Injections.java index 9e3bd4d0e6..45f61c1a57 100644 --- a/bootstrap/src/sun/nio/ch/lincheck/Injections.java +++ b/bootstrap/src/sun/nio/ch/lincheck/Injections.java @@ -317,10 +317,13 @@ 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 + ); } /** @@ -328,9 +331,12 @@ public static boolean beforeReadField(Object obj, String className, String field * * @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 + ); } /** @@ -345,10 +351,13 @@ public static void afterRead(Object value) { * * @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 + ); } /** @@ -356,9 +365,12 @@ public static boolean beforeWriteField(Object obj, String className, String fiel * * @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 + ); } /** diff --git a/bootstrap/src/sun/nio/ch/lincheck/Type.java b/bootstrap/src/sun/nio/ch/lincheck/Type.java new file mode 100644 index 0000000000..92ff672ac8 --- /dev/null +++ b/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. + * + *

+ * 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; + } +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index 1f0c5b1ddf..9b54e03070 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/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.* @@ -910,7 +911,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. @@ -948,7 +950,8 @@ abstract class ManagedStrategy( } /** Returns true 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,7 +986,8 @@ abstract class ManagedStrategy( loopDetector.afterRead(value) } - override fun beforeWriteField(obj: Any?, className: String, fieldName: String, value: Any?, codeLocation: Int, + 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) @@ -1014,7 +1018,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)) { diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt index 67080c113f..fe93ed780d 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt @@ -51,14 +51,16 @@ internal class SharedMemoryAccessTransformer( visitFieldInsn(opcode, owner, fieldName, desc) }, code = { + val valueType = getType(desc) // STACK: pushNull() push(owner) push(fieldName) + push(valueType.sort) loadNewCodeLocationId() push(true) // isStatic push(FinalFields.isFinalField(owner, fieldName)) // isFinal - // STACK: null, className, fieldName, codeLocation, isStatic, isFinal + // STACK: null, className, fieldName, fieldType, codeLocation, isStatic, isFinal invokeStatic(Injections::beforeReadField) // STACK: isTracePointCreated ifStatement( @@ -83,15 +85,17 @@ internal class SharedMemoryAccessTransformer( visitFieldInsn(opcode, owner, fieldName, desc) }, code = { + val valueType = getType(desc) // STACK: obj dup() // STACK: obj, obj push(owner) push(fieldName) + push(valueType.sort) loadNewCodeLocationId() push(false) // isStatic push(FinalFields.isFinalField(owner, fieldName)) // isFinal - // STACK: obj, obj, className, fieldName, codeLocation, isStatic, isFinal + // STACK: obj, obj, className, fieldName, fieldType, codeLocation, isStatic, isFinal invokeStatic(Injections::beforeReadField) // STACK: obj, isTracePointCreated ifStatement( @@ -124,12 +128,13 @@ internal class SharedMemoryAccessTransformer( pushNull() push(owner) push(fieldName) + push(valueType.sort) loadLocal(valueLocal) box(valueType) loadNewCodeLocationId() push(true) // isStatic push(FinalFields.isFinalField(owner, fieldName)) // isFinal - // STACK: value, null, className, fieldName, value, codeLocation, isStatic, isFinal + // STACK: value, null, className, fieldName, fieldType, value, codeLocation, isStatic, isFinal invokeStatic(Injections::beforeWriteField) // STACK: isTracePointCreated ifStatement( @@ -162,12 +167,13 @@ internal class SharedMemoryAccessTransformer( // STACK: obj, obj push(owner) push(fieldName) + push(valueType.sort) loadLocal(valueLocal) box(valueType) loadNewCodeLocationId() push(false) // isStatic push(FinalFields.isFinalField(owner, fieldName)) // isFinal - // STACK: obj, obj, className, fieldName, value, codeLocation, isStatic, isFinal + // STACK: obj, obj, className, fieldName, fieldType, value, codeLocation, isStatic, isFinal invokeStatic(Injections::beforeWriteField) // STACK: isTracePointCreated ifStatement( @@ -202,12 +208,13 @@ internal class SharedMemoryAccessTransformer( visitInsn(opcode) }, code = { - // STACK: array: Array, index: Int + // STACK: array, index val arrayElementType = getArrayElementType(opcode) dup2() - // STACK: array: Array, index: Int, array: Array, index: Int + // STACK: array, index, array, index + push(arrayElementType.sort) loadNewCodeLocationId() - // STACK: array: Array, index: Int, array: Array, index: Int, codeLocation: Int + // STACK: array, index, array, index, arrayElementType, codeLocation invokeStatic(Injections::beforeReadArray) ifStatement( condition = { /* already on stack */ }, @@ -231,17 +238,18 @@ internal class SharedMemoryAccessTransformer( visitInsn(opcode) }, code = { - // STACK: array: Array, index: Int, value: Object + // STACK: array, index, value val arrayElementType = getArrayElementType(opcode) val valueLocal = newLocal(arrayElementType) // we cannot use DUP as long/double require DUP2 storeLocal(valueLocal) - // STACK: array: Array, index: Int + // STACK: array, index dup2() - // STACK: array: Array, index: Int, array: Array, index: Int + // STACK: array, index, array, index + push(arrayElementType.sort) loadLocal(valueLocal) box(arrayElementType) loadNewCodeLocationId() - // STACK: array: Array, index: Int, array: Array, index: Int, value: Object, codeLocation: Int + // STACK: array, index, array, index, arrayElementType, value, codeLocation invokeStatic(Injections::beforeWriteArray) ifStatement( condition = { /* already on stack */ }, @@ -250,9 +258,9 @@ internal class SharedMemoryAccessTransformer( }, elseClause = {} ) - // STACK: array: Array, index: Int + // STACK: array, index loadLocal(valueLocal) - // STACK: array: Array, index: Int, value: Object + // STACK: array, index, value visitInsn(opcode) // STACK: invokeStatic(Injections::afterWrite) From 9fbcda7862eb91616f200cf33a70bfd569ff7a91 Mon Sep 17 00:00:00 2001 From: Evgeniy Moiseenko Date: Thu, 16 Jan 2025 21:02:28 +0100 Subject: [PATCH 2/4] add optional reads and method calls results interception Signed-off-by: Evgeniy Moiseenko --- .../src/sun/nio/ch/lincheck/EventTracker.java | 4 ++- .../src/sun/nio/ch/lincheck/Injections.java | 25 ++++++++++++-- .../strategy/managed/ManagedStrategy.kt | 15 +++++++- .../transformers/MethodCallTransformer.kt | 31 +++++++++++++++-- .../SharedMemoryAccessTransformer.kt | 34 +++++++++++++++---- 5 files changed, 96 insertions(+), 13 deletions(-) diff --git a/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java b/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java index 959f452782..30a3d12eaf 100644 --- a/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java +++ b/bootstrap/src/sun/nio/ch/lincheck/EventTracker.java @@ -44,6 +44,7 @@ boolean beforeReadField(Object obj, String className, String fieldName, Type fie boolean isStatic, boolean isFinal); boolean beforeReadArrayElement(Object array, int index, Type arrayElementType, int codeLocation); void afterRead(Object value); + Object interceptReadResult(); boolean beforeWriteField(Object obj, String className, String fieldName, Type fieldType, Object value, int codeLocation, @@ -52,9 +53,10 @@ boolean beforeWriteArrayElement(Object array, int index, Type arrayElementType, 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(); diff --git a/bootstrap/src/sun/nio/ch/lincheck/Injections.java b/bootstrap/src/sun/nio/ch/lincheck/Injections.java index 45f61c1a57..88c4e1e730 100644 --- a/bootstrap/src/sun/nio/ch/lincheck/Injections.java +++ b/bootstrap/src/sun/nio/ch/lincheck/Injections.java @@ -346,6 +346,16 @@ 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. * @@ -384,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); } /** @@ -410,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 */ diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index 9b54e03070..f2407d5673 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -986,6 +986,12 @@ abstract class ManagedStrategy( loopDetector.afterRead(value) } + 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 { @@ -1138,7 +1144,7 @@ abstract class ManagedStrategy( codeLocation: Int, methodId: Int, params: Array - ) { + ): Boolean { val guarantee = runInIgnoredSection { val iThread = threadScheduler.getCurrentThreadId() // re-throw abort error if the thread was aborted @@ -1189,6 +1195,7 @@ abstract class ManagedStrategy( // so `enterIgnoredSection` would have no effect enterIgnoredSection() } + return false // shouldInterceptMethodResult } override fun onMethodCallReturn(result: Any?) { @@ -1238,6 +1245,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): Boolean = try { getMethod(className.canonicalClassName, methodName, params)?.isSuspendable() ?: false diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/MethodCallTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/MethodCallTransformer.kt index dd98091ad2..ca99300b2c 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/MethodCallTransformer.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/MethodCallTransformer.kt @@ -28,6 +28,7 @@ internal class MethodCallTransformer( className: String, methodName: String, adapter: GeneratorAdapter, + private val interceptAtomicMethodCallResult: Boolean = false, ) : ManagedStrategyMethodVisitor(fileName, className, methodName, adapter) { override fun visitMethodInsn(opcode: Int, owner: String, name: String, desc: String, itf: Boolean) = adapter.run { @@ -86,8 +87,34 @@ internal class MethodCallTransformer( val handlerExceptionStartLabel = newLabel() visitTryCatchBlock(methodCallStartLabel, methodCallEndLabel, handlerExceptionStartLabel, null) visitLabel(methodCallStartLabel) - loadLocals(argumentLocals) - visitMethodInsn(opcode, owner, name, desc, itf) + if (interceptAtomicMethodCallResult) { + // STACK: shouldInterceptMethodResult + ifStatement( + condition = { /* already on stack */ }, + ifClause = { + val resultType = Type.getReturnType(desc) + if (opcode != INVOKESTATIC) { + pop() + } + // STACK : + invokeStatic(Injections::interceptMethodCallResult) + if (resultType == Type.VOID_TYPE) { + pop() + } else { + unbox(resultType) + } + }, + elseClause = { + loadLocals(argumentLocals) + visitMethodInsn(opcode, owner, name, desc, itf) + } + ) + } else { + // STACK: shouldInterceptMethodResult + pop() + loadLocals(argumentLocals) + visitMethodInsn(opcode, owner, name, desc, itf) + } visitLabel(methodCallEndLabel) // STACK [INVOKEVIRTUAL]: owner, arguments // STACK [INVOKESTATIC] : arguments diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt index fe93ed780d..d9e808b5c8 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/transformation/transformers/SharedMemoryAccessTransformer.kt @@ -28,6 +28,7 @@ internal class SharedMemoryAccessTransformer( className: String, methodName: String, adapter: GeneratorAdapter, + private val interceptReadAccesses: Boolean = false, ) : ManagedStrategyMethodVisitor(fileName, className, methodName, adapter) { lateinit var analyzer: AnalyzerAdapter @@ -68,11 +69,17 @@ internal class SharedMemoryAccessTransformer( ifClause = { invokeBeforeEventIfPluginEnabled("read static field") }, - elseClause = {}) + elseClause = {} + ) // STACK: - visitFieldInsn(opcode, owner, fieldName, desc) + if (interceptReadAccesses) { + invokeStatic(Injections::interceptReadResult) + unbox(valueType) + } else { + visitFieldInsn(opcode, owner, fieldName, desc) + } // STACK: value - invokeAfterRead(getType(desc)) + invokeAfterRead(valueType) // STACK: value } ) @@ -106,9 +113,15 @@ internal class SharedMemoryAccessTransformer( elseClause = {} ) // STACK: obj - visitFieldInsn(opcode, owner, fieldName, desc) + if (interceptReadAccesses) { + pop() + invokeStatic(Injections::interceptReadResult) + unbox(valueType) + } else { + visitFieldInsn(opcode, owner, fieldName, desc) + } // STACK: value - invokeAfterRead(getType(desc)) + invokeAfterRead(valueType) // STACK: value } ) @@ -223,8 +236,15 @@ internal class SharedMemoryAccessTransformer( }, elseClause = {} ) - // STACK: array: Array, index: Int - visitInsn(opcode) + // STACK: array, index + if (interceptReadAccesses) { + pop() + pop() + invokeStatic(Injections::interceptReadResult) + unbox(arrayElementType) + } else { + visitInsn(opcode) + } // STACK: value invokeAfterRead(arrayElementType) // STACK: value From cc454325e629e3bd5cc0283a7cd2209a6aa20408 Mon Sep 17 00:00:00 2001 From: Evgeniy Moiseenko Date: Thu, 16 Jan 2025 21:06:12 +0100 Subject: [PATCH 3/4] make final fields tracking optional, enabled/disabled by the flag Signed-off-by: Evgeniy Moiseenko --- .../kotlinx/lincheck/strategy/managed/ManagedStrategy.kt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index f2407d5673..bad109e212 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -76,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() @@ -921,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 @@ -1001,7 +1004,7 @@ abstract class ManagedStrategy( return@runInIgnoredSection false } // Optimization: do not track final field writes - if (isFinal) { + if (isFinal && !trackFinalFields) { return@runInIgnoredSection false } val iThread = threadScheduler.getCurrentThreadId() From 475d92bbb140863834a4f43f79f7a58971e998cd Mon Sep 17 00:00:00 2001 From: Evgeniy Moiseenko Date: Thu, 16 Jan 2025 21:32:18 +0100 Subject: [PATCH 4/4] add `iThread` argument to `onActorFinish` Signed-off-by: Evgeniy Moiseenko --- src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt | 4 ++-- .../kotlinx/lincheck/runner/TestThreadExecutionGenerator.java | 3 ++- .../main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt | 2 +- .../kotlinx/lincheck/strategy/managed/ManagedStrategy.kt | 2 +- 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt index da78123082..cff8b2a8c4 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt +++ b/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) { diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java index 6646989367..24fce94f12 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/TestThreadExecutionGenerator.java +++ b/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(); diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt index 3c2f49b06f..2f6edbdd92 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt +++ b/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. diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index bad109e212..d854dec598 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -622,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.