Skip to content

Commit c9d843a

Browse files
LipenLipen
authored
Add strings support (#295)
1 parent 54633bd commit c9d843a

File tree

16 files changed

+410
-130
lines changed

16 files changed

+410
-130
lines changed

‎usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,6 @@ sealed interface TsTestValue {
4848
}
4949
}
5050

51-
data class TsObject(val addr: Int) : TsTestValue
52-
5351
data class TsClass(
5452
val name: String,
5553
val properties: Map<String, TsTestValue>,

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

Lines changed: 36 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ import org.usvm.UContext
2424
import org.usvm.UExpr
2525
import org.usvm.UHeapRef
2626
import org.usvm.USort
27+
import org.usvm.api.allocateArrayInitialized
28+
import org.usvm.api.allocateConcreteRef
2729
import org.usvm.api.typeStreamOf
2830
import org.usvm.collection.field.UFieldLValue
2931
import org.usvm.isTrue
@@ -34,6 +36,7 @@ import org.usvm.machine.expr.TsVoidValue
3436
import org.usvm.machine.interpreter.TsStepScope
3537
import org.usvm.machine.types.EtsFakeType
3638
import org.usvm.memory.UReadOnlyMemory
39+
import org.usvm.sizeSort
3740
import org.usvm.types.single
3841
import org.usvm.util.mkFieldLValue
3942
import kotlin.contracts.ExperimentalContracts
@@ -65,7 +68,7 @@ class TsContext(
6568
fun typeToSort(type: EtsType): USort = when (type) {
6669
is EtsBooleanType -> boolSort
6770
is EtsNumberType -> fp64Sort
68-
is EtsStringType -> fp64Sort
71+
is EtsStringType -> addressSort
6972
is EtsNullType -> addressSort
7073
is EtsUndefinedType -> addressSort
7174
is EtsUnionType -> unresolvedSort
@@ -198,6 +201,38 @@ class TsContext(
198201
fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
199202
return scope.calcOnState { extractRef(memory) }
200203
}
204+
205+
private val stringConstantAllocatedRefs: MutableMap<String, UConcreteHeapRef> = hashMapOf()
206+
internal val heapRefToStringConstant: MutableMap<UConcreteHeapRef, String> = hashMapOf()
207+
208+
fun mkStringConstant(value: String, scope: TsStepScope): UConcreteHeapRef {
209+
return stringConstantAllocatedRefs.getOrPut(value) {
210+
val ref = allocateConcreteRef()
211+
heapRefToStringConstant[ref] = value
212+
213+
scope.doWithState {
214+
// Mark `ref` with String type
215+
memory.types.allocate(ref.address, EtsStringType)
216+
217+
// Initialize char array
218+
val valueType = EtsArrayType(EtsNumberType, dimensions = 1)
219+
val descriptor = arrayDescriptorOf(valueType)
220+
val charArray = memory.allocateArrayInitialized(
221+
type = descriptor,
222+
sort = bv16Sort,
223+
sizeSort = sizeSort,
224+
contents = value.asSequence().map { mkBv(it.code, bv16Sort) },
225+
)
226+
memory.types.allocate(charArray.address, valueType.elementType)
227+
228+
// Write char array to `ref.value`
229+
val valueLValue = mkFieldLValue(addressSort, ref, "value")
230+
memory.write(valueLValue, charArray, guard = trueExpr)
231+
}
232+
233+
ref
234+
}
235+
}
201236
}
202237

203238
const val MAGIC_OFFSET = 1000000

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt‎

Lines changed: 23 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ import org.usvm.UExpr
8585
import org.usvm.UHeapRef
8686
import org.usvm.USort
8787
import org.usvm.api.allocateArray
88+
import org.usvm.api.evalTypeEquals
8889
import org.usvm.dataflow.ts.infer.tryGetKnownType
8990
import org.usvm.dataflow.ts.util.type
9091
import org.usvm.machine.TsConcreteMethodCallStmt
@@ -118,15 +119,6 @@ import org.usvm.util.throwExceptionWithoutStackFrameDrop
118119

119120
private val logger = KotlinLogging.logger {}
120121

121-
@Suppress("MagicNumber")
122-
const val ADHOC_STRING = 777777.0 // arbitrary string
123-
124-
@Suppress("MagicNumber")
125-
const val ADHOC_STRING__NUMBER = 55555.0 // 'number'
126-
127-
@Suppress("MagicNumber")
128-
const val ADHOC_STRING__STRING = 2222.0 // 'string'
129-
130122
class TsExprResolver(
131123
private val ctx: TsContext,
132124
private val scope: TsStepScope,
@@ -277,10 +269,26 @@ class TsExprResolver(
277269
val arg = resolve(expr.arg) ?: return null
278270

279271
if (arg.sort == fp64Sort) {
280-
if (arg == mkFp64(ADHOC_STRING)) {
281-
return mkFp64(ADHOC_STRING__STRING)
282-
}
283-
return mkFp64(ADHOC_STRING__NUMBER) // 'number'
272+
return mkStringConstant("number", scope)
273+
}
274+
if (arg.sort == boolSort) {
275+
return mkStringConstant("boolean", scope)
276+
}
277+
if (arg.sort == addressSort) {
278+
val ref = arg.asExpr(addressSort)
279+
return mkIte(
280+
condition = mkHeapRefEq(ref, mkTsNullValue()),
281+
trueBranch = mkStringConstant("object", scope),
282+
falseBranch = mkIte(
283+
condition = mkHeapRefEq(ref, mkUndefinedValue()),
284+
trueBranch = mkStringConstant("undefined", scope),
285+
falseBranch = mkIte(
286+
condition = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) },
287+
trueBranch = mkStringConstant("string", scope),
288+
falseBranch = mkStringConstant("object", scope),
289+
)
290+
)
291+
)
284292
}
285293

286294
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
@@ -471,7 +479,7 @@ class TsExprResolver(
471479
}
472480

473481
if (expr.callee.name == "toString") {
474-
return mkFp64(ADHOC_STRING)
482+
return TODO()
475483
}
476484

477485
return when (val result = scope.calcOnState { methodResult }) {
@@ -1032,11 +1040,7 @@ class TsSimpleValueResolver(
10321040
}
10331041

10341042
override fun visit(value: EtsStringConstant): UExpr<out USort> = with(ctx) {
1035-
return when (value.value) {
1036-
"number" -> mkFp64(ADHOC_STRING__NUMBER)
1037-
"string" -> mkFp64(ADHOC_STRING__STRING)
1038-
else -> mkFp64(ADHOC_STRING)
1039-
}
1043+
mkStringConstant(value.value, scope)
10401044
}
10411045

10421046
override fun visit(value: EtsBooleanConstant): UExpr<out USort> = with(ctx) {

‎usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt‎

Lines changed: 66 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,11 @@ import org.jacodb.ets.model.EtsRefType
1919
import org.jacodb.ets.model.EtsReturnStmt
2020
import org.jacodb.ets.model.EtsStaticFieldRef
2121
import org.jacodb.ets.model.EtsStmt
22+
import org.jacodb.ets.model.EtsStringType
2223
import org.jacodb.ets.model.EtsThis
2324
import org.jacodb.ets.model.EtsThrowStmt
2425
import org.jacodb.ets.model.EtsType
26+
import org.jacodb.ets.model.EtsUndefinedType
2527
import org.jacodb.ets.model.EtsUnknownType
2628
import org.jacodb.ets.model.EtsValue
2729
import org.jacodb.ets.model.EtsVoidType
@@ -169,15 +171,15 @@ class TsInterpreter(
169171
if (isAllocatedConcreteHeapRef(resolvedInstance)) {
170172
val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single()
171173
if (type is EtsClassType) {
172-
val classes = ctx.scene.projectAndSdkClasses.filter { it.name == type.typeName }
174+
val classes = scene.projectAndSdkClasses.filter { it.name == type.typeName }
173175
if (classes.isEmpty()) {
174176
logger.warn { "Could not resolve class: ${type.typeName}" }
175-
scope.assert(ctx.falseExpr)
177+
scope.assert(falseExpr)
176178
return
177179
}
178180
if (classes.size > 1) {
179181
logger.warn { "Multiple classes with name: ${type.typeName}" }
180-
scope.assert(ctx.falseExpr)
182+
scope.assert(falseExpr)
181183
return
182184
}
183185
val cls = classes.single()
@@ -189,14 +191,14 @@ class TsInterpreter(
189191
logger.warn {
190192
"Could not resolve method: ${stmt.callee} on type: $type"
191193
}
192-
scope.assert(ctx.falseExpr)
194+
scope.assert(falseExpr)
193195
return
194196
}
195197
} else {
196-
val methods = ctx.resolveEtsMethods(stmt.callee)
198+
val methods = resolveEtsMethods(stmt.callee)
197199
if (methods.isEmpty()) {
198200
logger.warn { "Could not resolve method: ${stmt.callee}" }
199-
scope.assert(ctx.falseExpr)
201+
scope.assert(falseExpr)
200202
return
201203
}
202204
concreteMethods += methods
@@ -213,7 +215,7 @@ class TsInterpreter(
213215
val type = requireNotNull(method.enclosingClass).type
214216

215217
val constraint = scope.calcOnState {
216-
val ref = stmt.instance.asExpr(ctx.addressSort)
218+
val ref = stmt.instance.asExpr(addressSort)
217219
.takeIf { !it.isFakeObject() }
218220
?: uncoveredInstance.asExpr(addressSort)
219221
// TODO mistake, should be separated into several hierarchies
@@ -303,7 +305,7 @@ class TsInterpreter(
303305
}
304306

305307
check(args.size == numFormal) {
306-
"Expected ${numFormal} arguments, got ${args.size}"
308+
"Expected $numFormal arguments, got ${args.size}"
307309
}
308310

309311
args += stmt.instance!!
@@ -577,7 +579,12 @@ class TsInterpreter(
577579
}
578580

579581
private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver =
580-
TsExprResolver(ctx, scope, ::mapLocalToIdx, graph.hierarchy)
582+
TsExprResolver(
583+
ctx = ctx,
584+
scope = scope,
585+
localToIdx = ::mapLocalToIdx,
586+
hierarchy = graph.hierarchy,
587+
)
581588

582589
// (method, localName) -> idx
583590
private val localVarToIdx: MutableMap<EtsMethod, Map<String, Int>> = hashMapOf()
@@ -608,40 +615,38 @@ class TsInterpreter(
608615
else -> error("Unexpected local: $local")
609616
}
610617

611-
fun getInitialState(method: EtsMethod, targets: List<TsTarget>): TsState {
618+
fun getInitialState(method: EtsMethod, targets: List<TsTarget>): TsState = with(ctx) {
612619
val state = TsState(
613620
ctx = ctx,
614621
ownership = MutabilityOwnership(),
615622
entrypoint = method,
616623
targets = UTargetsSet.from(targets),
617624
)
618625

626+
state.memory.types.allocate(mkTsNullValue().address, EtsNullType)
627+
619628
val solver = ctx.solver<EtsType>()
620629

621630
// TODO check for statics
622-
val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count())
623-
val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)
624-
625-
state.pathConstraints += with(ctx) {
626-
mkNot(
627-
mkOr(
628-
ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()),
629-
ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue())
630-
)
631-
)
632-
}
631+
val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type))
632+
?: error("Cannot find index for 'this' in method: $method")
633+
val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx)
634+
val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort)
633635

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

640642
method.parameters.forEachIndexed { i, param ->
643+
val ref by lazy {
644+
val lValue = mkRegisterStackLValue(addressSort, i)
645+
state.memory.read(lValue).asExpr(addressSort)
646+
}
647+
641648
val parameterType = param.type
642649
if (parameterType is EtsRefType) {
643-
val argLValue = mkRegisterStackLValue(ctx.addressSort, i)
644-
val ref = state.memory.read(argLValue).asExpr(ctx.addressSort)
645650
val resolvedParameterType = graph.cp
646651
.projectAndSdkClasses
647652
.singleOrNull { it.name == parameterType.typeName }
@@ -653,6 +658,21 @@ class TsInterpreter(
653658
val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy)
654659
?: resolvedParameterType
655660
state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
661+
662+
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
663+
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
664+
}
665+
if (parameterType == EtsNullType) {
666+
state.pathConstraints += mkHeapRefEq(ref, mkTsNullValue())
667+
}
668+
if (parameterType == EtsUndefinedType) {
669+
state.pathConstraints += mkHeapRefEq(ref, mkUndefinedValue())
670+
}
671+
if (parameterType == EtsStringType) {
672+
state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType)
673+
674+
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
675+
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
656676
}
657677
}
658678

@@ -663,35 +683,32 @@ class TsInterpreter(
663683
state.memory.stack.push(method.parametersWithThisCount, method.localsCount)
664684
state.newStmt(method.cfg.instructions.first())
665685

666-
state.memory.types.allocate(ctx.mkTsNullValue().address, EtsNullType)
686+
state.memory.types.allocate(mkTsNullValue().address, EtsNullType)
667687

668-
return state
688+
state
669689
}
670690

671691
private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
672692
scope.doWithState {
673-
with(ctx) {
674-
if (method.returnType is EtsVoidType) {
675-
methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue)
676-
return@doWithState
677-
}
693+
if (method.returnType is EtsVoidType) {
694+
methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue)
695+
return@doWithState
696+
}
678697

679-
val resultSort = typeToSort(method.returnType)
680-
val resultValue = when (resultSort) {
681-
is UAddressSort -> makeSymbolicRefUntyped()
682-
is TsUnresolvedSort -> {
683-
mkFakeValue(
684-
scope,
685-
makeSymbolicPrimitive(ctx.boolSort),
686-
makeSymbolicPrimitive(ctx.fp64Sort),
687-
makeSymbolicRefUntyped()
688-
)
689-
}
698+
val resultSort = ctx.typeToSort(method.returnType)
699+
val resultValue = when (resultSort) {
700+
is UAddressSort -> makeSymbolicRefUntyped()
690701

691-
else -> makeSymbolicPrimitive(resultSort)
692-
}
693-
methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
702+
is TsUnresolvedSort -> ctx.mkFakeValue(
703+
scope,
704+
makeSymbolicPrimitive(ctx.boolSort),
705+
makeSymbolicPrimitive(ctx.fp64Sort),
706+
makeSymbolicRefUntyped()
707+
)
708+
709+
else -> makeSymbolicPrimitive(resultSort)
694710
}
711+
methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
695712
}
696713
}
697714

‎usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@ class TsTypeSystem(
288288
is EtsUnclearRefType,
289289
is EtsClassType ->
290290
if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
291-
scene.projectAndSdkClasses.asSequence().map { it.type }
291+
scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType
292292
} else {
293293
hierarchy.classesForType(t)
294294
.asSequence()

0 commit comments

Comments
 (0)