Skip to content

Add support for Strings #295

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

Merged
Lipen merged 1 commit into from
Jun 20, 2025
Merged

Add support for Strings #295

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 0 additions & 2 deletions usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,6 @@ sealed interface TsTestValue {
}
}

data class TsObject(val addr: Int) : TsTestValue

data class TsClass(
val name: String,
val properties: Map<String, TsTestValue>,
Expand Down
37 changes: 36 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.USort
import org.usvm.api.allocateArrayInitialized
import org.usvm.api.allocateConcreteRef
import org.usvm.api.typeStreamOf
import org.usvm.collection.field.UFieldLValue
import org.usvm.isTrue
Expand All @@ -34,6 +36,7 @@ import org.usvm.machine.expr.TsVoidValue
import org.usvm.machine.interpreter.TsStepScope
import org.usvm.machine.types.EtsFakeType
import org.usvm.memory.UReadOnlyMemory
import org.usvm.sizeSort
import org.usvm.types.single
import org.usvm.util.mkFieldLValue
import kotlin.contracts.ExperimentalContracts
Expand Down Expand Up @@ -65,7 +68,7 @@ class TsContext(
fun typeToSort(type: EtsType): USort = when (type) {
is EtsBooleanType -> boolSort
is EtsNumberType -> fp64Sort
is EtsStringType -> fp64Sort
is EtsStringType -> addressSort
is EtsNullType -> addressSort
is EtsUndefinedType -> addressSort
is EtsUnionType -> unresolvedSort
Expand Down Expand Up @@ -198,6 +201,38 @@ class TsContext(
fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
return scope.calcOnState { extractRef(memory) }
}

private val stringConstantAllocatedRefs: MutableMap<String, UConcreteHeapRef> = hashMapOf()
internal val heapRefToStringConstant: MutableMap<UConcreteHeapRef, String> = hashMapOf()

fun mkStringConstant(value: String, scope: TsStepScope): UConcreteHeapRef {
return stringConstantAllocatedRefs.getOrPut(value) {
val ref = allocateConcreteRef()
heapRefToStringConstant[ref] = value

scope.doWithState {
// Mark `ref` with String type
memory.types.allocate(ref.address, EtsStringType)

// Initialize char array
val valueType = EtsArrayType(EtsNumberType, dimensions = 1)
val descriptor = arrayDescriptorOf(valueType)
val charArray = memory.allocateArrayInitialized(
type = descriptor,
sort = bv16Sort,
sizeSort = sizeSort,
contents = value.asSequence().map { mkBv(it.code, bv16Sort) },
)
memory.types.allocate(charArray.address, valueType.elementType)

// Write char array to `ref.value`
val valueLValue = mkFieldLValue(addressSort, ref, "value")
memory.write(valueLValue, charArray, guard = trueExpr)
}

ref
}
}
}

const val MAGIC_OFFSET = 1000000
Expand Down
42 changes: 23 additions & 19 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 @@ -85,6 +85,7 @@
import org.usvm.UHeapRef
import org.usvm.USort
import org.usvm.api.allocateArray
import org.usvm.api.evalTypeEquals
import org.usvm.dataflow.ts.infer.tryGetKnownType
import org.usvm.dataflow.ts.util.type
import org.usvm.machine.TsConcreteMethodCallStmt
Expand Down Expand Up @@ -118,15 +119,6 @@

private val logger = KotlinLogging.logger {}

@Suppress("MagicNumber")
const val ADHOC_STRING = 777777.0 // arbitrary string

@Suppress("MagicNumber")
const val ADHOC_STRING__NUMBER = 55555.0 // 'number'

@Suppress("MagicNumber")
const val ADHOC_STRING__STRING = 2222.0 // 'string'

class TsExprResolver(
private val ctx: TsContext,
private val scope: TsStepScope,
Expand Down Expand Up @@ -277,10 +269,26 @@
val arg = resolve(expr.arg) ?: return null

if (arg.sort == fp64Sort) {
if (arg == mkFp64(ADHOC_STRING)) {
return mkFp64(ADHOC_STRING__STRING)
}
return mkFp64(ADHOC_STRING__NUMBER) // 'number'
return mkStringConstant("number", scope)
}
if (arg.sort == boolSort) {
return mkStringConstant("boolean", scope)
}
if (arg.sort == addressSort) {
val ref = arg.asExpr(addressSort)
return mkIte(
condition = mkHeapRefEq(ref, mkTsNullValue()),
trueBranch = mkStringConstant("object", scope),
falseBranch = mkIte(
condition = mkHeapRefEq(ref, mkUndefinedValue()),
trueBranch = mkStringConstant("undefined", scope),
falseBranch = mkIte(
condition = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) },
trueBranch = mkStringConstant("string", scope),
falseBranch = mkStringConstant("object", scope),
)
)
)
}

logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
Expand Down Expand Up @@ -471,7 +479,7 @@
}

if (expr.callee.name == "toString") {
return mkFp64(ADHOC_STRING)
return TODO()

Check warning

Code scanning / detekt

Unreachable code detected. This code should be removed. Warning

This expression is unreachable code which should either be used or removed.
}

return when (val result = scope.calcOnState { methodResult }) {
Expand Down Expand Up @@ -1032,11 +1040,7 @@
}

override fun visit(value: EtsStringConstant): UExpr<out USort> = with(ctx) {
return when (value.value) {
"number" -> mkFp64(ADHOC_STRING__NUMBER)
"string" -> mkFp64(ADHOC_STRING__STRING)
else -> mkFp64(ADHOC_STRING)
}
mkStringConstant(value.value, scope)
}

override fun visit(value: EtsBooleanConstant): UExpr<out USort> = with(ctx) {
Expand Down
115 changes: 66 additions & 49 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 @@ -19,9 +19,11 @@
import org.jacodb.ets.model.EtsReturnStmt
import org.jacodb.ets.model.EtsStaticFieldRef
import org.jacodb.ets.model.EtsStmt
import org.jacodb.ets.model.EtsStringType
import org.jacodb.ets.model.EtsThis
import org.jacodb.ets.model.EtsThrowStmt
import org.jacodb.ets.model.EtsType
import org.jacodb.ets.model.EtsUndefinedType
import org.jacodb.ets.model.EtsUnknownType
import org.jacodb.ets.model.EtsValue
import org.jacodb.ets.model.EtsVoidType
Expand Down Expand Up @@ -169,15 +171,15 @@
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 = scene.projectAndSdkClasses.filter { it.name == type.typeName }
if (classes.isEmpty()) {
logger.warn { "Could not resolve class: ${type.typeName}" }
scope.assert(ctx.falseExpr)
scope.assert(falseExpr)
return
}
if (classes.size > 1) {
logger.warn { "Multiple classes with name: ${type.typeName}" }
scope.assert(ctx.falseExpr)
scope.assert(falseExpr)
return
}
val cls = classes.single()
Expand All @@ -189,14 +191,14 @@
logger.warn {
"Could not resolve method: ${stmt.callee} on type: $type"
}
scope.assert(ctx.falseExpr)
scope.assert(falseExpr)
return
}
} else {
val methods = ctx.resolveEtsMethods(stmt.callee)
val methods = resolveEtsMethods(stmt.callee)
if (methods.isEmpty()) {
logger.warn { "Could not resolve method: ${stmt.callee}" }
scope.assert(ctx.falseExpr)
scope.assert(falseExpr)
return
}
concreteMethods += methods
Expand All @@ -213,7 +215,7 @@
val type = requireNotNull(method.enclosingClass).type

val constraint = scope.calcOnState {
val ref = stmt.instance.asExpr(ctx.addressSort)
val ref = stmt.instance.asExpr(addressSort)
.takeIf { !it.isFakeObject() }
?: uncoveredInstance.asExpr(addressSort)
// TODO mistake, should be separated into several hierarchies
Expand Down Expand Up @@ -303,7 +305,7 @@
}

check(args.size == numFormal) {
"Expected ${numFormal} arguments, got ${args.size}"
"Expected $numFormal arguments, got ${args.size}"
}

args += stmt.instance!!
Expand Down Expand Up @@ -577,7 +579,12 @@
}

private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver =
TsExprResolver(ctx, scope, ::mapLocalToIdx, graph.hierarchy)
TsExprResolver(
ctx = ctx,
scope = scope,
localToIdx = ::mapLocalToIdx,
hierarchy = graph.hierarchy,
)

// (method, localName) -> idx
private val localVarToIdx: MutableMap<EtsMethod, Map<String, Int>> = hashMapOf()
Expand Down Expand Up @@ -608,40 +615,38 @@
else -> error("Unexpected local: $local")
}

fun getInitialState(method: EtsMethod, targets: List<TsTarget>): TsState {
fun getInitialState(method: EtsMethod, targets: List<TsTarget>): TsState = with(ctx) {
val state = TsState(
ctx = ctx,
ownership = MutabilityOwnership(),
entrypoint = method,
targets = UTargetsSet.from(targets),
)

state.memory.types.allocate(mkTsNullValue().address, EtsNullType)

val solver = ctx.solver<EtsType>()

// TODO check for statics
val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count())
val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)

state.pathConstraints += with(ctx) {
mkNot(
mkOr(
ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()),
ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue())
)
)
}
val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type))

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.
?: error("Cannot find index for 'this' in method: $method")
val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx)
val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort)

method.enclosingClass?.let { thisClass ->
// TODO not equal but subtype for abstract/interfaces
val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, thisClass.type)
state.pathConstraints += thisTypeConstraint
}
state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkTsNullValue()))
state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkUndefinedValue()))

// TODO not equal but subtype for abstract/interfaces
state.pathConstraints += state.memory.types.evalTypeEquals(thisRef, method.enclosingClass!!.type)

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.

method.parameters.forEachIndexed { i, param ->
val ref by lazy {
val lValue = mkRegisterStackLValue(addressSort, i)
state.memory.read(lValue).asExpr(addressSort)
}

val parameterType = param.type
if (parameterType is EtsRefType) {
val argLValue = mkRegisterStackLValue(ctx.addressSort, i)
val ref = state.memory.read(argLValue).asExpr(ctx.addressSort)
val resolvedParameterType = graph.cp
.projectAndSdkClasses
.singleOrNull { it.name == parameterType.typeName }
Expand All @@ -653,6 +658,21 @@
val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy)
?: resolvedParameterType
state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)

state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
}
if (parameterType == EtsNullType) {
state.pathConstraints += mkHeapRefEq(ref, mkTsNullValue())
}
if (parameterType == EtsUndefinedType) {
state.pathConstraints += mkHeapRefEq(ref, mkUndefinedValue())
}
if (parameterType == EtsStringType) {
state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType)

state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
}
}

Expand All @@ -663,35 +683,32 @@
state.memory.stack.push(method.parametersWithThisCount, method.localsCount)
state.newStmt(method.cfg.instructions.first())

state.memory.types.allocate(ctx.mkTsNullValue().address, EtsNullType)
state.memory.types.allocate(mkTsNullValue().address, EtsNullType)

return state
state
}

private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
scope.doWithState {
with(ctx) {
if (method.returnType is EtsVoidType) {
methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue)
return@doWithState
}
if (method.returnType is EtsVoidType) {
methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue)
return@doWithState
}

val resultSort = typeToSort(method.returnType)
val resultValue = when (resultSort) {
is UAddressSort -> makeSymbolicRefUntyped()
is TsUnresolvedSort -> {
mkFakeValue(
scope,
makeSymbolicPrimitive(ctx.boolSort),
makeSymbolicPrimitive(ctx.fp64Sort),
makeSymbolicRefUntyped()
)
}
val resultSort = ctx.typeToSort(method.returnType)
val resultValue = when (resultSort) {
is UAddressSort -> makeSymbolicRefUntyped()

else -> makeSymbolicPrimitive(resultSort)
}
methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
is TsUnresolvedSort -> ctx.mkFakeValue(
scope,
makeSymbolicPrimitive(ctx.boolSort),
makeSymbolicPrimitive(ctx.fp64Sort),
makeSymbolicRefUntyped()
)

else -> makeSymbolicPrimitive(resultSort)
}
methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
}
}

Expand Down
2 changes: 1 addition & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,7 @@ class TsTypeSystem(
is EtsUnclearRefType,
is EtsClassType ->
if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
scene.projectAndSdkClasses.asSequence().map { it.type }
scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType
} else {
hierarchy.classesForType(t)
.asSequence()
Expand Down
Loading