Skip to content

More fixes for real applications #283

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 16 commits into
base: main
Choose a base branch
from
Draft

More fixes for real applications #283

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
89ed53e
Hacks
CaelmBleidd May 29, 2025
069cb78
More hacks
CaelmBleidd May 29, 2025
f85ef55
Some more fixes
CaelmBleidd May 30, 2025
51f5b9f
Tmp commit
CaelmBleidd May 30, 2025
545887c
Input arrays support
CaelmBleidd Jun 6, 2025
f6c17c4
Format
Lipen Jun 9, 2025
db952f6
Operators implementation
CaelmBleidd Jun 10, 2025
911e8ca
Some hacks
CaelmBleidd Jun 10, 2025
a07c653
Fix a class signature lookup
CaelmBleidd Jun 11, 2025
201e5f4
Support simple casts
CaelmBleidd Jun 11, 2025
f8fd3fa
Clear logs
CaelmBleidd Jun 11, 2025
59393c2
Add todo
CaelmBleidd Jun 11, 2025
0f18a8c
Rebase fix
CaelmBleidd Jun 18, 2025
bb4df1f
Tmp changes
CaelmBleidd Jun 19, 2025
7b1bcd8
Some fixes
CaelmBleidd Jun 20, 2025
c3e5fe0
Fix mocker return value
CaelmBleidd Jun 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Hacks
  • Loading branch information
@CaelmBleidd
CaelmBleidd committed Jun 18, 2025
commit 89ed53ec556d0c52f71c351f8855faa8b48f1b10
85 changes: 69 additions & 16 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,8 +105,8 @@ import org.usvm.machine.types.EtsAuxiliaryType
import org.usvm.machine.types.mkFakeValue
import org.usvm.memory.ULValue
import org.usvm.sizeSort
import org.usvm.util.EtsFieldResolutionResult
import org.usvm.util.EtsHierarchy
import org.usvm.util.EtsPropertyResolution
import org.usvm.util.createFakeField
import org.usvm.util.isResolved
import org.usvm.util.mkArrayIndexLValue
Expand All @@ -115,6 +115,7 @@ import org.usvm.util.mkFieldLValue
import org.usvm.util.mkRegisterStackLValue
import org.usvm.util.resolveEtsField
import org.usvm.util.throwExceptionWithoutStackFrameDrop
import org.usvm.util.type

private val logger = KotlinLogging.logger {}

Expand Down Expand Up @@ -520,6 +521,17 @@ class TsExprResolver(
}
}

if (expr.callee.name == "\$r") {
// TODO hack
return scope.calcOnState {
val mockSymbol = memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)

scope.assert(mkEq(mockSymbol, ctx.mkTsNullValue()).not())

mockSymbol
}
}

return when (val result = scope.calcOnState { methodResult }) {
is TsMethodResult.Success -> {
scope.doWithState { methodResult = TsMethodResult.NoCall }
Expand All @@ -531,21 +543,51 @@ class TsExprResolver(
}

is TsMethodResult.NoCall -> {
// TODO: spawn VirtualCall when method resolution fails
val method = resolveStaticMethod(expr.callee)
val resolutionResult = resolveStaticMethod(expr.callee)

if (method == null) {
if (resolutionResult is EtsPropertyResolution.Empty) {
logger.error { "Could not resolve static call: ${expr.callee}" }
scope.assert(falseExpr)
return null
}

val instance = scope.calcOnState { getStaticInstance(method.enclosingClass!!) }
// static virtual call
if (resolutionResult is EtsPropertyResolution.Ambiguous) {
val resolvedArgs = expr.args.map { resolve(it) ?: return null }

val staticInstances = scope.calcOnState {
resolutionResult.properties.take(1).map { getStaticInstance(it.enclosingClass!!) }

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.
}

// TODO take 1 is an error
val concreteCalls = resolutionResult.properties.take(1).mapIndexed { index, value ->
TsConcreteMethodCallStmt(
callee = value,
instance = staticInstances[index],
args = resolvedArgs,
returnSite = scope.calcOnState { lastStmt }
)
}

val blocks = concreteCalls.map {
ctx.mkTrue() to { state: TsState -> state.newStmt(it) }
} // TODO error with true Expr

logger.warn { "Forking on ${blocks.size} branches" }

scope.forkMulti(blocks)

return null
}

require(resolutionResult is EtsPropertyResolution.Unique)

val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) }

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.

val resolvedArgs = expr.args.map { resolve(it) ?: return null }

val concreteCall = TsConcreteMethodCallStmt(
callee = method,
callee = resolutionResult.property,
instance = instance,
args = resolvedArgs,
returnSite = scope.calcOnState { lastStmt },
Expand All @@ -559,25 +601,22 @@ class TsExprResolver(

private fun resolveStaticMethod(
method: EtsMethodSignature,
): EtsMethod? {
): EtsPropertyResolution<out EtsMethod> {
// Perfect signature:
if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
val classes = ctx.scene.projectAndSdkClasses.filter { it.name == method.enclosingClass.name }
if (classes.size != 1) return null
if (classes.size != 1) return EtsPropertyResolution.Empty
val clazz = classes.single()
val methods = clazz.methods.filter { it.name == method.name }
if (methods.size != 1) return null
return methods.single()
return EtsPropertyResolution.create(methods)
}

// Unknown signature:
val methods = ctx.scene.projectAndSdkClasses
.flatMap { it.methods }
.filter { it.name == method.name }
if (methods.size == 1) return methods.single()

// error("Cannot resolve method $method")
return null
return EtsPropertyResolution.create(methods)
}

override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
Expand Down Expand Up @@ -722,7 +761,7 @@ class TsExprResolver(
val etsField = resolveEtsField(instance, field, hierarchy)

val sort = when (etsField) {
is EtsFieldResolutionResult.Empty -> {
is EtsPropertyResolution.Empty -> {
logger.error("Field $etsField not found, creating fake field")
// If we didn't find any real fields, let's create a fake one.
// It is possible due to mistakes in the IR or if the field was added explicitly
Expand All @@ -732,10 +771,13 @@ class TsExprResolver(
addressSort
}

is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type)
is EtsFieldResolutionResult.Ambiguous -> unresolvedSort
is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
is EtsPropertyResolution.Ambiguous -> unresolvedSort
}

// Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,

Check warning

Code scanning / detekt

Line detected, which is longer than the defined maximum line length in the code style. Warning

Line detected, which is longer than the defined maximum line length in the code style.
// мы проигнорируем что уже туда писали и считаем не оттуда

if (sort == unresolvedSort) {
val boolLValue = mkFieldLValue(boolSort, instanceRef, field)
val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field)
Expand Down Expand Up @@ -866,6 +908,17 @@ class TsExprResolver(
} else {
expr.type
}

if (expr.type.typeName == "Boolean") {
val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxBy { it.methods.size }
return@with scope.calcOnState { memory.allocConcrete(clazz.type) }
}

if (expr.type.typeName == "Number") {
val clazz = scene.sdkClasses.filter { it.name == "Number" }.maxBy { it.methods.size }
return@with scope.calcOnState { memory.allocConcrete(clazz.type) }
}

scope.calcOnState { memory.allocConcrete(resolvedType) }
}

Expand Down
50 changes: 43 additions & 7 deletions usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import mu.KotlinLogging
import org.jacodb.ets.model.EtsArrayAccess
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsAssignStmt
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsCallStmt
import org.jacodb.ets.model.EtsClassType
import org.jacodb.ets.model.EtsIfStmt
Expand All @@ -14,6 +15,7 @@ import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.model.EtsMethodSignature
import org.jacodb.ets.model.EtsNopStmt
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsParameterRef
import org.jacodb.ets.model.EtsRefType
import org.jacodb.ets.model.EtsReturnStmt
Expand Down Expand Up @@ -63,7 +65,7 @@ import org.usvm.machine.types.toAuxiliaryType
import org.usvm.sizeSort
import org.usvm.targets.UTargetsSet
import org.usvm.types.single
import org.usvm.util.EtsFieldResolutionResult
import org.usvm.util.EtsPropertyResolution
import org.usvm.util.mkArrayIndexLValue
import org.usvm.util.mkArrayLengthLValue
import org.usvm.util.mkFieldLValue
Expand Down Expand Up @@ -169,7 +171,7 @@ class TsInterpreter(
if (isAllocatedConcreteHeapRef(resolvedInstance)) {
val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single()
if (type is EtsClassType) {
val classes = ctx.scene.projectAndSdkClasses.filter { it.name == type.typeName }
val classes = graph.hierarchy.classesForType(type)
if (classes.isEmpty()) {
logger.warn { "Could not resolve class: ${type.typeName}" }
scope.assert(ctx.falseExpr)
Expand All @@ -183,7 +185,9 @@ class TsInterpreter(
val cls = classes.single()
val method = cls.methods
.singleOrNull { it.name == stmt.callee.name }
?: TODO("Overloads are not supported yet")
?: run {
TODO("Overloads are not supported yet")
}
concreteMethods += method
} else {
logger.warn {
Expand Down Expand Up @@ -346,6 +350,8 @@ class TsInterpreter(

val (posStmt, negStmt) = graph.successors(stmt).take(2).toList()

logger.warn { "Forking on if stmt $stmt" }

scope.forkWithBlackList(
boolExpr,
posStmt,
Expand Down Expand Up @@ -485,9 +491,9 @@ class TsInterpreter(

// If there is no such field, we create a fake field for the expr
val sort = when (etsField) {
is EtsFieldResolutionResult.Empty -> unresolvedSort
is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type)
is EtsFieldResolutionResult.Ambiguous -> unresolvedSort
is EtsPropertyResolution.Empty -> unresolvedSort
is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
is EtsPropertyResolution.Ambiguous -> unresolvedSort
}

if (sort == unresolvedSort) {
Expand All @@ -499,7 +505,37 @@ class TsInterpreter(
memory.write(lValue, fakeObject, guard = trueExpr)
} else {
val lValue = mkFieldLValue(sort, instance, lhv.field)
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
if (lValue.sort != expr.sort) {
if (expr.isFakeObject()) {
val lhvType = lhv.type
val value = when (lhvType) {
is EtsBooleanType -> {
scope.calcOnState {
pathConstraints += expr.getFakeType(scope).boolTypeExpr
expr.extractBool(scope)
}
}
is EtsNumberType -> {
scope.calcOnState {
pathConstraints += expr.getFakeType(scope).fpTypeExpr
expr.extractFp(scope)
}
}
else -> {
scope.calcOnState {
pathConstraints += expr.getFakeType(scope).refTypeExpr
expr.extractRef(scope)
}
}
}

memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
} else {
error("TODO")
}
} else {
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
}
}
}

Expand Down
32 changes: 15 additions & 17 deletions usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,10 @@ fun TsContext.resolveEtsField(
instance: EtsLocal?,
field: EtsFieldSignature,
hierarchy: EtsHierarchy,
): EtsFieldResolutionResult {
): EtsPropertyResolution<out EtsField> {
// Perfect signature:
if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
val classes = scene.projectAndSdkClasses.filter { cls ->
cls.name == field.enclosingClass.name
}
val classes = scene.projectAndSdkClasses.filter { it.signature == field.enclosingClass }
if (classes.isEmpty()) {
error("Cannot resolve class ${field.enclosingClass.name}")
}
Expand All @@ -31,7 +29,7 @@ fun TsContext.resolveEtsField(
val clazz = classes.single()
val fields = clazz.getAllFields(hierarchy).filter { it.name == field.name }
if (fields.size == 1) {
return EtsFieldResolutionResult.create(fields.single())
return EtsPropertyResolution.create(fields.single())
}
}

Expand All @@ -41,12 +39,12 @@ fun TsContext.resolveEtsField(
when (instanceType) {
is EtsClassType -> {
val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy)
if (field != null) return EtsFieldResolutionResult.create(field)
if (field != null) return EtsPropertyResolution.create(field)
}

is EtsUnclearRefType -> {
val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
if (field != null) return EtsFieldResolutionResult.create(field)
if (field != null) return EtsPropertyResolution.create(field)
}
}
}
Expand All @@ -55,7 +53,7 @@ fun TsContext.resolveEtsField(
cls.getAllFields(hierarchy).filter { it.name == field.name }
}

return EtsFieldResolutionResult.create(fields)
return EtsPropertyResolution.create(fields)
}

private fun tryGetSingleField(
Expand Down Expand Up @@ -118,19 +116,19 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair<Set<EtsFieldName>,
return allFields to allMethods
}

sealed class EtsFieldResolutionResult {
data class Unique(val field: EtsField) : EtsFieldResolutionResult()
data class Ambiguous(val fields: List<EtsField>) : EtsFieldResolutionResult()
data object Empty : EtsFieldResolutionResult()
sealed class EtsPropertyResolution<T> {
data class Unique<T>(val property: T) : EtsPropertyResolution<T>()
data class Ambiguous<T>(val properties: List<T>) : EtsPropertyResolution<T>()
data object Empty : EtsPropertyResolution<Nothing>()

companion object {
fun create(field: EtsField) = Unique(field)
fun <T> create(property: T) = Unique(property)

fun create(fields: List<EtsField>): EtsFieldResolutionResult {
fun <T> create(properties: List<T>): EtsPropertyResolution<out T> {
return when {
fields.isEmpty() -> Empty
fields.size == 1 -> Unique(fields.single())
else -> Ambiguous(fields)
properties.isEmpty() -> Empty
properties.size == 1 -> Unique(properties.single())
else -> Ambiguous(properties)
}
}
}
Expand Down
19 changes: 19 additions & 0 deletions usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
package org.usvm.project

import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
import org.jacodb.ets.utils.getDeclaredLocals
import org.jacodb.ets.utils.getLocals
import org.jacodb.ets.utils.loadEtsProjectFromIR
Expand Down Expand Up @@ -72,11 +75,27 @@ class RunOnPhotosProject : TsMethodTestRunner() {
.filterNot { it.isStatic }
.filterNot { it.name.startsWith("%AM") }
.filterNot { it.name == "build" }
.filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
.filterNot { it.name == STATIC_INIT_METHOD_NAME }

Check warning

Code scanning / detekt

Disallow shadowing variable declarations. Warning test

Name shadowed: implicit lambda parameter 'it'
.filterNot { it.name == CONSTRUCTOR_NAME }

Check warning

Code scanning / detekt

Disallow shadowing variable declarations. Warning test

Name shadowed: implicit lambda parameter 'it'
}
val tsOptions = TsOptions()
TsMachine(scene, options, tsOptions).use { machine ->
val states = machine.analyze(methods)
states.let {}
}
}

@Test
fun `test on particular method`() {
val method = scene.projectClasses
.flatMap { it.methods }
.single { it.name == "createActionBar" && it.enclosingClass?.name == "NewAlbumBarModel" }

val tsOptions = TsOptions()
TsMachine(scene, options, tsOptions).use { machine ->
val states = machine.analyze(listOf(method))
states.let {}
}
}
}
2 changes: 1 addition & 1 deletion usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -343,7 +343,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
exceptionsPropagation = true,
timeout = Duration.INFINITE,
stepsFromLastCovered = 3500L,
stepsFromLastCovered = 50000L,
solverType = SolverType.YICES,
solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
Expand Down