Implementation of the JacoDB interpreter (#18)

Co-authored-by: Alexey Menshutin <[email protected]>

buildSrc/build.gradle.kts

@@ -6,7 +6,7 @@ repositories {
     gradlePluginPortal()
 }
 
-val kotlinVersion = "1.7.10"
+val kotlinVersion = "1.8.22"
 
 dependencies {
     implementation("org.jetbrains.kotlin:kotlin-gradle-plugin:$kotlinVersion")

buildSrc/src/main/kotlin/Versions.kt

@@ -2,6 +2,6 @@ object Versions {
     const val ksmt = "0.5.3"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.0_main-SNAPSHOT"
+    const val jcdb = "1.0.0"
     const val mockk = "1.13.4"
 }

usvm-core/src/main/kotlin/org/usvm/ApplicationGraph.kt

@@ -11,4 +11,6 @@ interface ApplicationGraph<Method, Statement> {
     fun exitPoints(method: Method): Sequence<Statement>
 
     fun methodOf(node: Statement): Method
+
+    fun statementsOf(method: Method): Sequence<Statement>
 }

usvm-core/src/main/kotlin/org/usvm/CallStack.kt

@@ -1,11 +1,13 @@
 package org.usvm
 
-data class UCallStackFrame<Method, Statement>(val method: Method, val returnSite: Statement?)
+data class UCallStackFrame<Method, Statement>(
+    val method: Method,
+    val returnSite: Statement?,
+)
 
 class UCallStack<Method, Statement> private constructor(
     private val stack: ArrayDeque<UCallStackFrame<Method, Statement>>,
-) :
-    Collection<UCallStackFrame<Method, Statement>> by stack {
+) : Collection<UCallStackFrame<Method, Statement>> by stack {
     constructor() : this(ArrayDeque())
     constructor(method: Method) : this(
         ArrayDeque<UCallStackFrame<Method, Statement>>().apply {

usvm-core/src/main/kotlin/org/usvm/Composition.kt

@@ -20,7 +20,7 @@ open class UComposer<Field, Type>(
 
     override fun <Sort : USort> transform(
         expr: URegisterReading<Sort>,
-    ): UExpr<Sort> = with(expr) { stackEvaluator.eval(idx, sort) }
+    ): UExpr<Sort> = with(expr) { stackEvaluator.readRegister(idx, sort) }
 
     override fun <Sort : USort> transform(expr: UHeapReading<*, *, *>): UExpr<Sort> =
         error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")

usvm-core/src/main/kotlin/org/usvm/Context.kt

@@ -27,7 +27,7 @@ open class UContext(
 ) : KContext(operationMode, astManagementMode, simplificationMode) {
 
     private val solver by lazy { components.mkSolver(this) }
-    private val typeSystem = components.mkTypeSystem(this)
+    private val typeSystem by lazy { components.mkTypeSystem(this) }
 
     @Suppress("UNCHECKED_CAST")
     fun <Field, Type, Method> solver(): USolverBase<Field, Type, Method> =

usvm-core/src/main/kotlin/org/usvm/Expressions.kt

@@ -25,6 +25,7 @@ typealias UBoolSort = KBoolSort
 typealias UBvSort = KBvSort
 typealias UBv32Sort = KBv32Sort
 typealias USizeSort = KBv32Sort
+typealias UFpSort = KFpSort
 
 typealias UExpr<Sort> = KExpr<Sort>
 typealias UBoolExpr = UExpr<UBoolSort>
@@ -110,25 +111,30 @@ class UNullRef internal constructor(
 //region LValues
 open class ULValue(val sort: USort)
 
-class URegisterRef(sort: USort, val idx: Int) : ULValue(sort)
+class URegisterLValue(sort: USort, val idx: Int) : ULValue(sort)
 
-class UFieldRef<Field>(fieldSort: USort, val ref: UHeapRef, val field: Field) : ULValue(fieldSort)
+class UFieldLValue<Field>(fieldSort: USort, val ref: UHeapRef, val field: Field) : ULValue(fieldSort)
 
-class UArrayIndexRef<ArrayType>(
+class UArrayIndexLValue<ArrayType>(
     cellSort: USort,
     val ref: UHeapRef,
     val index: USizeExpr,
-    val arrayType: ArrayType
+    val arrayType: ArrayType,
 ) : ULValue(cellSort)
 
+class UArrayLengthLValue<ArrayType>(
+    val ref: UHeapRef,
+    val arrayType: ArrayType,
+) : ULValue(ref.uctx.sizeSort)
+
 //endregion
 
 //region Read Expressions
 
 class URegisterReading<Sort : USort> internal constructor(
     ctx: UContext,
     val idx: Int,
-    override val sort: Sort
+    override val sort: Sort,
 ) : USymbol<Sort>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<Sort> {
         require(transformer is UExprTransformer<*, *>)
@@ -146,7 +152,7 @@ class URegisterReading<Sort : USort> internal constructor(
 
 abstract class UHeapReading<RegionId : URegionId<Key, Sort, RegionId>, Key, Sort : USort>(
     ctx: UContext,
-    val region: USymbolicMemoryRegion<RegionId, Key, Sort>
+    val region: USymbolicMemoryRegion<RegionId, Key, Sort>,
 ) : USymbol<Sort>(ctx) {
     override val sort: Sort get() = region.sort
 }
@@ -212,7 +218,7 @@ class UInputArrayReading<ArrayType, Sort : USort> internal constructor(
     ctx: UContext,
     region: UInputArrayRegion<ArrayType, Sort>,
     val address: UHeapRef,
-    val index: USizeExpr
+    val index: USizeExpr,
 ) : UHeapReading<UInputArrayId<ArrayType, Sort>, USymbolicArrayIndex, Sort>(ctx, region) {
     init {
         require(address !is UNullRef)
@@ -277,15 +283,14 @@ class UInputArrayLengthReading<ArrayType> internal constructor(
 
 //region Mocked Expressions
 
-abstract class UMockSymbol<Sort : USort>(ctx: UContext, override val sort: Sort) : USymbol<Sort>(ctx) {
-}
+abstract class UMockSymbol<Sort : USort>(ctx: UContext, override val sort: Sort) : USymbol<Sort>(ctx)
 
 // TODO: make indices compositional!
 class UIndexedMethodReturnValue<Method, Sort : USort> internal constructor(
     ctx: UContext,
     val method: Method,
     val callIndex: Int,
-    override val sort: Sort
+    override val sort: Sort,
 ) : UMockSymbol<Sort>(ctx, sort) {
     override fun accept(transformer: KTransformerBase): KExpr<Sort> {
         require(transformer is UExprTransformer<*, *>)
@@ -308,7 +313,7 @@ class UIndexedMethodReturnValue<Method, Sort : USort> internal constructor(
 class UIsExpr<Type> internal constructor(
     ctx: UContext,
     val ref: UHeapRef,
-    val type: Type
+    val type: Type,
 ) : USymbol<UBoolSort>(ctx) {
     override val sort = ctx.boolSort
 
@@ -332,7 +337,7 @@ class UIsExpr<Type> internal constructor(
 
 //region Utils
 
-val UBoolExpr.isFalse get() = this === ctx.falseExpr
-val UBoolExpr.isTrue get() = this === ctx.trueExpr
+val UBoolExpr.isFalse get() = this == ctx.falseExpr
+val UBoolExpr.isTrue get() = this == ctx.trueExpr
 
 //endregion

usvm-core/src/main/kotlin/org/usvm/Machine.kt

@@ -1,32 +1,32 @@
 package org.usvm
 
+import org.usvm.ps.stopstrategies.StoppingStrategy
+
 
 /**
  * An abstract symbolic machine.
  *
  * @see [run]
  */
-abstract class UMachine<State : UState<*, *, *, *>, Target> : AutoCloseable {
+abstract class UMachine<State> : AutoCloseable {
     /**
      * The main entry point. Template method for running the machine on a specified [target].
      *
      * @param target a generic target to run on.
      * @param onState called on every forked state. Can be used for collecting results.
      * @param continueAnalyzing filtering function for states. If it returns `false`, a state
      * won't be analyzed further. It is called on an original state and every forked state as well.
-     * @param shouldStop is called on every step, before peeking a next state from path selector.
+     * @param stoppingStrategy is called on every step, before peeking a next state from the path selector.
      * Returning `true` aborts analysis.
      */
     fun run(
-        target: Target,
+        interpreter: UInterpreter<State>,
+        pathSelector: UPathSelector<State>,
         onState: (State) -> Unit,
         continueAnalyzing: (State) -> Boolean,
-        shouldStop: () -> Boolean = { false },
+        stoppingStrategy: StoppingStrategy = StoppingStrategy { false },
     ) {
-        val interpreter = getInterpreter(target)
-        val pathSelector = getPathSelector(target)
-
-        while (!pathSelector.isEmpty() && !shouldStop()) {
+        while (!pathSelector.isEmpty() && !stoppingStrategy.shouldStop()) {
             pathSelector.peekAndUpdate { state ->
                 val (forkedStates, stateAlive) = interpreter.step(state)
 
@@ -54,16 +54,6 @@ abstract class UMachine<State : UState<*, *, *, *>, Target> : AutoCloseable {
         } else {
             remove(state)
         }
-        add(forkedStates)
+        add(forkedStates.toList())
     }
-
-    /**
-     * @return a configured interpreter suitable for a [target].
-     */
-    protected abstract fun getInterpreter(target: Target): UInterpreter<State>
-
-    /**
-     * @return a configured path selector with initial states obtained from a [target].
-     */
-    protected abstract fun getPathSelector(target: Target): UPathSelector<State>
 }

usvm-core/src/main/kotlin/org/usvm/PathSelector.kt

@@ -16,7 +16,7 @@ interface UPathSelector<State> {
     /**
      * Adds [states] to the path selector.
      */
-    fun add(states: Sequence<State>)
+    fun add(states: Collection<State>)
 
     /**
      * Updates the internal priority of the [state].

usvm-core/src/main/kotlin/org/usvm/State.kt

@@ -4,19 +4,19 @@ import io.ksmt.expr.KInterpretedValue
 import kotlinx.collections.immutable.PersistentList
 import org.usvm.constraints.UPathConstraints
 import org.usvm.memory.UMemoryBase
-import org.usvm.model.UModel
+import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
 import org.usvm.solver.UUnknownResult
 import org.usvm.solver.UUnsatResult
 
 abstract class UState<Type, Field, Method, Statement>(
     // TODO: add interpreter-specific information
-    val ctx: UContext,
-    val callStack: UCallStack<Method, Statement>,
-    val pathConstraints: UPathConstraints<Type>,
-    val memory: UMemoryBase<Field, Type, Method>,
-    var models: List<UModel>,
-    var path: PersistentList<Statement>,
+    open val ctx: UContext,
+    open val callStack: UCallStack<Method, Statement>,
+    open val pathConstraints: UPathConstraints<Type>,
+    open val memory: UMemoryBase<Field, Type, Method>,
+    open var models: List<UModelBase<Field, Type>>,
+    open var path: PersistentList<Statement>,
 ) {
     /**
      * Creates new state structurally identical to this.
@@ -51,7 +51,7 @@ class ForkResult<T>(
  * - if [forkToSatisfied], then c = [conditionToCheck]
  * - if ![forkToSatisfied], then c = [satisfiedCondition]
  */
-private fun <T : UState<Type, *, *, *>, Type> forkIfSat(
+private fun <T : UState<Type, Field, *, *>, Type, Field> forkIfSat(
     state: T,
     satisfiedCondition: UBoolExpr,
     conditionToCheck: UBoolExpr,
@@ -64,7 +64,7 @@ private fun <T : UState<Type, *, *, *>, Type> forkIfSat(
         return null
     }
 
-    val solver = state.ctx.solver<Any?, Type, Any?>()
+    val solver = state.ctx.solver<Field, Type, Any?>()
     val satResult = solver.check(pathConstraints, useSoftConstraints = true)
 
     return when (satResult) {
@@ -111,7 +111,7 @@ private fun <T : UState<Type, *, *, *>, Type> forkIfSat(
  * 2. makes not more than one query to USolver;
  * 3. if both [condition] and ![condition] are satisfiable, then [ForkResult.positiveState] === [state].
  */
-fun <T : UState<Type, *, *, *>, Type> fork(
+fun <T : UState<Type, Field, *, *>, Type, Field> fork(
     state: T,
     condition: UBoolExpr,
 ): ForkResult<T> {

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -12,13 +12,13 @@ package org.usvm
  *
  * @param originalState an initial state.
  */
-class StepScope<T : UState<Type, *, *, *>, Type>(
-    val uctx: UContext,
+class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
     originalState: T,
 ) {
     private val forkedStates = mutableListOf<T>()
     private var curState: T? = originalState
-    private var alive: Boolean = true
+    var alive: Boolean = true
+        private set
 
     /**
      * @return forked states and the status of initial state.

usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt

@@ -27,7 +27,10 @@ open class UPathConstraints<Type> private constructor(
     /**
      * Constraints solved by type solver.
      */
-    val typeConstraints: UTypeConstraints<Type> = UTypeConstraints(ctx.typeSystem(), equalityConstraints)
+    val typeConstraints: UTypeConstraints<Type> = UTypeConstraints(
+        ctx.typeSystem(),
+        equalityConstraints
+    ),
 ) {
     /**
      * Constraints solved by SMT solver.
@@ -39,8 +42,8 @@ open class UPathConstraints<Type> private constructor(
 
     open val isFalse: Boolean
         get() = equalityConstraints.isContradiction ||
-                typeConstraints.isContradiction ||
-                logicalConstraints.singleOrNull() is UFalse
+            typeConstraints.isContradiction ||
+            logicalConstraints.singleOrNull() is UFalse
 
     @Suppress("UNCHECKED_CAST")
     open operator fun plusAssign(constraint: UBoolExpr): Unit =
@@ -50,9 +53,8 @@ open class UPathConstraints<Type> private constructor(
 
                 constraint == trueExpr || constraint in logicalConstraints -> {}
 
-                constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) -> {
+                constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) ->
                     equalityConstraints.addReferenceEquality(constraint.lhs as UHeapRef, constraint.rhs as UHeapRef)
-                }
 
                 constraint is UIsExpr<*> -> typeConstraints.cast(constraint.ref, constraint.type as Type)
 
@@ -61,7 +63,9 @@ open class UPathConstraints<Type> private constructor(
                 constraint is UNotExpr -> {
                     val notConstraint = constraint.arg
                     when {
-                        notConstraint is UEqExpr<*> && isSymbolicHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) -> {
+                        notConstraint is UEqExpr<*> &&
+                            isSymbolicHeapRef(notConstraint.lhs) &&
+                            isSymbolicHeapRef(notConstraint.rhs) -> {
                             require(notConstraint.rhs.sort == addressSort)
                             equalityConstraints.addReferenceDisequality(
                                 notConstraint.lhs as UHeapRef,

usvm-core/src/main/kotlin/org/usvm/memory/Heap.kt

@@ -86,7 +86,7 @@ class UAddressCounter {
     }
 }
 
-data class URegionHeap<Field, ArrayType>(
+class URegionHeap<Field, ArrayType>(
     private val ctx: UContext,
     private var lastAddress: UAddressCounter = UAddressCounter(),
     private var allocatedFields: PersistentMap<Pair<UConcreteHeapAddress, Field>, UExpr<out USort>> = persistentMapOf(),