Improve calls in TS machine (#273)

Author: Lipen

buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts

@@ -48,7 +48,7 @@ tasks.named<Test>("test") {
     // Use JUnit Platform for unit tests.
     useJUnitPlatform()
 
-    maxHeapSize = "1G"
+    maxHeapSize = "4G"
 
     testLogging {
         events("passed")

usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt

@@ -8,8 +8,6 @@ import org.usvm.machine.expr.TsSimpleValueResolver
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsState
 import org.usvm.statistics.UMachineObserver
-import kotlin.collections.filter
-import kotlin.collections.isNotEmpty
 
 data class UncoveredIfSuccessors(val ifStmt: EtsIfStmt, val successors: Set<EtsStmt>)
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -3,6 +3,7 @@ package org.usvm.machine
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsAnyType
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
@@ -28,7 +29,7 @@ import org.usvm.machine.expr.TsUndefinedSort
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.types.FakeType
-import org.usvm.types.UTypeStream
+import org.usvm.memory.UReadOnlyMemory
 import org.usvm.types.single
 import org.usvm.util.mkFieldLValue
 import kotlin.contracts.ExperimentalContracts
@@ -48,42 +49,51 @@ class TsContext(
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
      */
-    private val undefinedValue: UExpr<UAddressSort> = mkNullRef()
-    fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
+    private val undefinedValue: UHeapRef = mkNullRef()
+    fun mkUndefinedValue(): UHeapRef = undefinedValue
 
     private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
     fun mkTsNullValue(): UConcreteHeapRef = nullValue
 
     fun typeToSort(type: EtsType): USort = when (type) {
         is EtsBooleanType -> boolSort
         is EtsNumberType -> fp64Sort
-        is EtsRefType -> addressSort
         is EtsNullType -> addressSort
         is EtsUndefinedType -> addressSort
-        is EtsUnknownType -> unresolvedSort
         is EtsUnionType -> unresolvedSort
+        is EtsRefType -> addressSort
         is EtsAnyType -> unresolvedSort
-        else -> TODO("Support all JacoDB types, encountered $type")
+        is EtsUnknownType -> unresolvedSort
+        else -> TODO("${type::class.simpleName} is not yet supported: $type")
     }
 
-    fun UHeapRef.getTypeStream(scope: TsStepScope): UTypeStream<EtsType> =
-        scope.calcOnState {
-            memory.typeStreamOf(this@getTypeStream)
-        }
+    // TODO: for now, ALL descriptors for array are UNKNOWN
+    //  in order to make ALL reading/writing, including '.length' access consistent
+    //  and possible in cases when the array type is not known.
+    //  For example, when we access '.length' of some array, we do not care about its type,
+    //  but we HAVE TO use some type consistent with the type used when this array was created.
+    //  Note: Using UnknownType everywhere does not lead to any errors yet,
+    //  since we do not rely on array types in any way.
+    fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType
+
+    fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): FakeType {
+        check(isFakeObject())
+        return memory.typeStreamOf(this).single() as FakeType
+    }
 
     fun UConcreteHeapRef.getFakeType(scope: TsStepScope): FakeType =
-        getTypeStream(scope).single() as FakeType
+        scope.calcOnState { getFakeType(memory) }
 
     @OptIn(ExperimentalContracts::class)
-    fun UExpr<out USort>.isFakeObject(): Boolean {
+    fun UExpr<*>.isFakeObject(): Boolean {
         contract {
             returns(true) implies (this@isFakeObject is UConcreteHeapRef)
         }
 
         return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET
     }
 
-    fun UExpr<out USort>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
+    fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
         if (isFakeObject()) {
             return this
         }
@@ -94,20 +104,20 @@ class TsContext(
             when (sort) {
                 boolSort -> {
                     val lvalue = getIntermediateBoolLValue(ref.address)
-                    memory.write(lvalue, this@toFakeObject.asExpr(boolSort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.fromBool(this@TsContext))
+                    memory.write(lvalue, asExpr(boolSort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.mkBool(this@TsContext))
                 }
 
                 fp64Sort -> {
                     val lValue = getIntermediateFpLValue(ref.address)
-                    memory.write(lValue, this@toFakeObject.asExpr(fp64Sort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.fromFp(this@TsContext))
+                    memory.write(lValue, asExpr(fp64Sort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.mkFp(this@TsContext))
                 }
 
                 addressSort -> {
                     val lValue = getIntermediateRefLValue(ref.address)
-                    memory.write(lValue, this@toFakeObject.asExpr(addressSort), guard = trueExpr)
-                    memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
+                    memory.write(lValue, asExpr(addressSort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.mkRef(this@TsContext))
                 }
 
                 else -> TODO("Not yet supported")
@@ -117,29 +127,15 @@ class TsContext(
         return ref
     }
 
-    fun UExpr<out USort>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
+    fun UExpr<*>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<*>? {
         if (!isFakeObject()) return null
 
         val type = getFakeType(scope)
-        return scope.calcOnState {
-            when {
-                type.boolTypeExpr.isTrue -> {
-                    val lValue = getIntermediateBoolLValue(address)
-                    memory.read(lValue).asExpr(boolSort)
-                }
-
-                type.fpTypeExpr.isTrue -> {
-                    val lValue = getIntermediateFpLValue(address)
-                    memory.read(lValue).asExpr(fp64Sort)
-                }
-
-                type.refTypeExpr.isTrue -> {
-                    val lValue = getIntermediateRefLValue(address)
-                    memory.read(lValue).asExpr(addressSort)
-                }
-
-                else -> null
-            }
+        return when {
+            type.boolTypeExpr.isTrue -> extractBool(scope)
+            type.fpTypeExpr.isTrue -> extractFp(scope)
+            type.refTypeExpr.isTrue -> extractRef(scope)
+            else -> null
         }
     }
 
@@ -163,19 +159,34 @@ class TsContext(
         return mkFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
     }
 
-    fun UConcreteHeapRef.extractBool(scope: TsStepScope): UBoolExpr {
+    fun UConcreteHeapRef.extractBool(memory: UReadOnlyMemory<*>): UBoolExpr {
+        check(isFakeObject())
         val lValue = getIntermediateBoolLValue(address)
-        return scope.calcOnState { memory.read(lValue) }
+        return memory.read(lValue)
     }
 
-    fun UConcreteHeapRef.extractFp(scope: TsStepScope): UExpr<KFp64Sort> {
+    fun UConcreteHeapRef.extractFp(memory: UReadOnlyMemory<*>): UExpr<KFp64Sort> {
+        check(isFakeObject())
         val lValue = getIntermediateFpLValue(address)
-        return scope.calcOnState { memory.read(lValue) }
+        return memory.read(lValue)
     }
 
-    fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
+    fun UConcreteHeapRef.extractRef(memory: UReadOnlyMemory<*>): UHeapRef {
+        check(isFakeObject())
         val lValue = getIntermediateRefLValue(address)
-        return scope.calcOnState { memory.read(lValue) }
+        return memory.read(lValue)
+    }
+
+    fun UConcreteHeapRef.extractBool(scope: TsStepScope): UBoolExpr {
+        return scope.calcOnState { extractBool(memory) }
+    }
+
+    fun UConcreteHeapRef.extractFp(scope: TsStepScope): UExpr<KFp64Sort> {
+        return scope.calcOnState { extractFp(memory) }
+    }
+
+    fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
+        return scope.calcOnState { extractRef(memory) }
     }
 }
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt renamed to usvm-ts/src/main/kotlin/org/usvm/machine/TsGraph.kt

@@ -7,29 +7,36 @@ import org.usvm.dataflow.ts.graph.EtsApplicationGraph
 import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl
 import org.usvm.statistics.ApplicationGraph
 
-class TsApplicationGraph(scene: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
-    private val applicationGraph: EtsApplicationGraph = EtsApplicationGraphImpl(scene)
+class TsGraph(scene: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
+    private val etsGraph: EtsApplicationGraph = EtsApplicationGraphImpl(scene)
+
+    val cp: EtsScene
+        get() = etsGraph.cp
 
     override fun predecessors(node: EtsStmt): Sequence<EtsStmt> =
-        applicationGraph.predecessors(node)
+        etsGraph.predecessors(node)
 
     override fun successors(node: EtsStmt): Sequence<EtsStmt> =
-        applicationGraph.successors(node)
+        if (node is TsMethodCall) {
+            etsGraph.successors(node.returnSite)
+        } else {
+            etsGraph.successors(node)
+        }
 
     override fun callees(node: EtsStmt): Sequence<EtsMethod> =
-        applicationGraph.callees(node)
+        etsGraph.callees(node)
 
     override fun callers(method: EtsMethod): Sequence<EtsStmt> =
-        applicationGraph.callers(method)
+        etsGraph.callers(method)
 
     override fun entryPoints(method: EtsMethod): Sequence<EtsStmt> =
-        applicationGraph.entryPoints(method)
+        etsGraph.entryPoints(method)
 
     override fun exitPoints(method: EtsMethod): Sequence<EtsStmt> =
-        applicationGraph.exitPoints(method)
+        etsGraph.exitPoints(method)
 
     override fun methodOf(node: EtsStmt): EtsMethod =
-        applicationGraph.methodOf(node)
+        etsGraph.methodOf(node)
 
     override fun statementsOf(method: EtsMethod): Sequence<EtsStmt> =
         method.cfg.stmts.asSequence()

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

@@ -35,9 +35,9 @@ class TsMachine(
     private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project)
     private val components = TsComponents(typeSystem, options)
     private val ctx = TsContext(project, components)
-    private val applicationGraph = TsApplicationGraph(project)
-    private val interpreter = TsInterpreter(ctx, applicationGraph, tsOptions, observer)
-    private val cfgStatistics = CfgStatisticsImpl(applicationGraph)
+    private val graph = TsGraph(project)
+    private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer)
+    private val cfgStatistics = CfgStatisticsImpl(graph)
 
     fun analyze(
         methods: List<EtsMethod>,
@@ -53,8 +53,8 @@ class TsMachine(
             }
 
         val coverageStatistics = CoverageStatistics<EtsMethod, EtsStmt, TsState>(
-            methodsToTrackCoverage,
-            applicationGraph
+            methods = methodsToTrackCoverage,
+            applicationGraph = graph,
         )
 
         val callGraphStatistics: PlainCallGraphStatistics<EtsMethod> =
@@ -66,13 +66,13 @@ class TsMachine(
         val timeStatistics = TimeStatistics<EtsMethod, TsState>()
 
         val pathSelector = createPathSelector(
-            initialStates,
-            options,
-            applicationGraph,
-            timeStatistics,
-            { coverageStatistics },
-            { cfgStatistics },
-            { callGraphStatistics },
+            initialStates = initialStates,
+            options = options,
+            applicationGraph = graph,
+            timeStatistics = timeStatistics,
+            coverageStatisticsFactory = { coverageStatistics },
+            cfgStatisticsFactory = { cfgStatistics },
+            callGraphStatisticsFactory = { callGraphStatistics },
         )
 
         val statesCollector =

usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt

@@ -0,0 +1,48 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStmtLocation
+import org.usvm.UExpr
+
+sealed interface TsMethodCall : EtsStmt {
+    val instance: UExpr<*>?
+    val args: List<UExpr<*>>
+    val returnSite: EtsStmt
+
+    override val location: EtsStmtLocation
+        get() = returnSite.location
+
+    override fun <R> accept(visitor: EtsStmt.Visitor<R>): R {
+        error("Auxiliary instruction")
+    }
+}
+
+class TsVirtualMethodCallStmt(
+    val callee: EtsMethodSignature,
+    override val instance: UExpr<*>?,
+    override val args: List<UExpr<*>>,
+    override val returnSite: EtsStmt,
+) : TsMethodCall {
+    override fun toString(): String {
+        return "virtual ${callee.enclosingClass.name}::${callee.name}"
+    }
+
+    fun toConcrete(callee: EtsMethod): TsConcreteMethodCallStmt {
+        return TsConcreteMethodCallStmt(callee, instance, args, returnSite)
+    }
+}
+
+// Note: `args` are resolved, but not yet truncated (if more than necessary),
+//  and not wrapped in array (if calling a vararg method)
+class TsConcreteMethodCallStmt(
+    val callee: EtsMethod,
+    override val instance: UExpr<*>?,
+    override val args: List<UExpr<*>>,
+    override val returnSite: EtsStmt,
+) : TsMethodCall {
+    override fun toString(): String {
+        return "concrete ${callee.signature.enclosingClass.name}::${callee.name}"
+    }
+}