Java 9+ instrumentation without VM options

[ndkoval]

The current model checking implementation requires the following VM options to be added:

--add-opens java.base/jdk.internal.misc=ALL-UNNAMED
--add-exports java.base/jdk.internal.util=ALL-UNNAMED

We can overcome this restriction by transforming classes via a dynamically attached Java agent. See #249.

Subtasks to do:

• [x] Check on the Kotlin Coroutines build - 3d
• [x] Investigate whether we need beforeMethodCall[1,2,3,..] optimizations - 0.5d
• [x] Cleanup - 1.5d
• [x] Code review - 3d

[ndkoval]

The best option (if it works) would be transforming classes via a special java agent.

[jifang]

Hello, I am still getting the error when running with model check, even with the JVM options set. I was using the sample code from the official doc.

class Counter<T> {
    // The following line will generate the error
    private val size = AtomicInteger(0)
    @Volatile
    private var value = 0

    fun inc(): Int = ++value
    fun get() = value
}

class BasicCounterTest {
    private val c = Counter<Int>() // Initial state

    // Operations on the Counter
    @Operation
    fun inc() = c.inc()

    @Operation
    fun get() = c.get()

    @Test // JUnit
    fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
}

error.log

[ndkoval]

Fixed under #285 and #296