Skip to content

Commit a2242a9

Browse files
LipenLipen
authored
Support static fields (#261)
1 parent faf3bc9 commit a2242a9

File tree

21 files changed

+646
-184
lines changed

21 files changed

+646
-184
lines changed

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

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -120,10 +120,7 @@ class TsContext(
120120
fun UExpr<out USort>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
121121
if (!isFakeObject()) return null
122122

123-
val type = scope.calcOnState {
124-
memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType
125-
}
126-
123+
val type = getFakeType(scope)
127124
return scope.calcOnState {
128125
when {
129126
type.boolTypeExpr.isTrue -> {

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,5 +16,6 @@ class TsComposer(
1616
ownership: MutabilityOwnership,
1717
) : UComposer<EtsType, TsSizeSort>(ctx, memory, ownership), TsTransformer
1818

19-
class TsExprTranslator(ctx: UContext<TsSizeSort>) : UExprTranslator<EtsType, TsSizeSort>(ctx), TsTransformer
20-
19+
class TsExprTranslator(
20+
ctx: UContext<TsSizeSort>,
21+
) : UExprTranslator<EtsType, TsSizeSort>(ctx), TsTransformer

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

Lines changed: 70 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -64,15 +64,14 @@ import org.jacodb.ets.base.EtsType
6464
import org.jacodb.ets.base.EtsTypeOfExpr
6565
import org.jacodb.ets.base.EtsUnaryExpr
6666
import org.jacodb.ets.base.EtsUnaryPlusExpr
67-
import org.jacodb.ets.base.EtsUnclearRefType
6867
import org.jacodb.ets.base.EtsUndefinedConstant
6968
import org.jacodb.ets.base.EtsUnknownType
7069
import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
7170
import org.jacodb.ets.base.EtsValue
7271
import org.jacodb.ets.base.EtsVoidExpr
7372
import org.jacodb.ets.base.EtsYieldExpr
73+
import org.jacodb.ets.base.STATIC_INIT_METHOD_NAME
7474
import org.jacodb.ets.base.UNKNOWN_CLASS_NAME
75-
import org.jacodb.ets.model.EtsField
7675
import org.jacodb.ets.model.EtsFieldSignature
7776
import org.jacodb.ets.model.EtsMethod
7877
import org.jacodb.ets.model.EtsMethodSignature
@@ -86,12 +85,15 @@ import org.usvm.api.allocateArray
8685
import org.usvm.isTrue
8786
import org.usvm.machine.TsContext
8887
import org.usvm.machine.interpreter.TsStepScope
88+
import org.usvm.machine.interpreter.isInitialized
89+
import org.usvm.machine.interpreter.markInitialized
8990
import org.usvm.machine.operator.TsBinaryOperator
9091
import org.usvm.machine.operator.TsUnaryOperator
9192
import org.usvm.machine.state.TsMethodResult
9293
import org.usvm.machine.state.TsState
9394
import org.usvm.machine.state.localsCount
9495
import org.usvm.machine.state.newStmt
96+
import org.usvm.machine.state.parametersWithThisCount
9597
import org.usvm.machine.types.FakeType
9698
import org.usvm.machine.types.mkFakeValue
9799
import org.usvm.memory.ULValue
@@ -101,6 +103,7 @@ import org.usvm.util.mkArrayIndexLValue
101103
import org.usvm.util.mkArrayLengthLValue
102104
import org.usvm.util.mkFieldLValue
103105
import org.usvm.util.mkRegisterStackLValue
106+
import org.usvm.util.resolveEtsField
104107
import org.usvm.util.throwExceptionWithoutStackFrameDrop
105108

106109
private val logger = KotlinLogging.logger {}
@@ -111,7 +114,7 @@ class TsExprResolver(
111114
private val localToIdx: (EtsMethod, EtsValue) -> Int,
112115
) : EtsEntity.Visitor<UExpr<out USort>?> {
113116

114-
private val simpleValueResolver: TsSimpleValueResolver =
117+
val simpleValueResolver: TsSimpleValueResolver =
115118
TsSimpleValueResolver(ctx, scope, localToIdx)
116119

117120
fun resolve(expr: EtsEntity): UExpr<out USort>? {
@@ -446,11 +449,10 @@ class TsExprResolver(
446449
doWithState {
447450
val method = resolveInstanceCall(expr.instance, expr.method)
448451

452+
check(args.size == method.parametersWithThisCount)
449453
pushSortsForArguments(expr.instance, expr.args, localToIdx)
450-
451454
callStack.push(method, currentStatement)
452455
memory.stack.push(args.toTypedArray(), method.localsCount)
453-
454456
newStmt(method.cfg.stmts.first())
455457
}
456458
}
@@ -610,46 +612,47 @@ class TsExprResolver(
610612
state.throwExceptionWithoutStackFrameDrop(address, type)
611613
}
612614

613-
private fun resolveInstanceField(
614-
instance: EtsLocal,
615+
private fun handleFieldRef(
616+
instance: EtsLocal?,
617+
instanceRef: UHeapRef,
615618
field: EtsFieldSignature,
616-
): EtsField {
617-
// Perfect signature:
618-
if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
619-
val clazz = ctx.scene.projectAndSdkClasses.single { it.name == field.enclosingClass.name }
620-
val fields = clazz.fields.filter { it.name == field.name }
621-
if (fields.size == 1) return fields.single()
622-
}
619+
): UExpr<out USort>? = with(ctx) {
620+
val etsField = resolveEtsField(instance, field)
621+
val sort = typeToSort(etsField.type)
623622

624-
// Unknown signature:
625-
val instanceType = instance.type
626-
if (instanceType is EtsClassType) {
627-
val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.signature.name }
628-
if (classes.size == 1) {
629-
val clazz = classes.single()
630-
return clazz.fields.single { it.name == field.name }
631-
}
632-
val fields = classes.flatMap { it.fields.filter { it.name == field.name } }
633-
if (fields.size == 1) {
634-
return fields.single()
635-
}
636-
} else if (instanceType is EtsUnclearRefType) {
637-
val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.name }
638-
if (classes.size == 1) {
639-
val clazz = classes.single()
640-
return clazz.fields.single { it.name == field.name }
641-
}
642-
val fields = classes.flatMap { it.fields.filter { it.name == field.name } }
643-
if (fields.size == 1) {
644-
return fields.single()
623+
val expr = if (sort == unresolvedSort) {
624+
val boolLValue = mkFieldLValue(boolSort, instanceRef, field)
625+
val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field)
626+
val refLValue = mkFieldLValue(addressSort, instanceRef, field)
627+
628+
scope.calcOnState {
629+
val bool = memory.read(boolLValue)
630+
val fp = memory.read(fpLValue)
631+
val ref = memory.read(refLValue)
632+
633+
// If a fake object is already created and assigned to the field,
634+
// there is no need to recreate another one
635+
val fakeRef = if (ref.isFakeObject()) {
636+
ref
637+
} else {
638+
mkFakeValue(scope, bool, fp, ref)
639+
}
640+
641+
memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
642+
643+
fakeRef
645644
}
646645
} else {
647-
val fields = ctx.scene.projectAndSdkClasses.flatMap { it.fields.filter { it.name == field.name } }
648-
if (fields.size == 1) {
649-
return fields.single()
650-
}
646+
val lValue = mkFieldLValue(sort, instanceRef, field)
647+
scope.calcOnState { memory.read(lValue) }
648+
}
649+
650+
// TODO: check 'field.type' vs 'etsField.type'
651+
if (assertIsSubtype(expr, field.type)) {
652+
expr
653+
} else {
654+
null
651655
}
652-
error("Cannot resolve field $field")
653656
}
654657

655658
override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
@@ -683,46 +686,40 @@ class TsExprResolver(
683686
}
684687
}
685688

686-
val field = resolveInstanceField(value.instance, value.field)
687-
val sort = typeToSort(field.type)
689+
return handleFieldRef(value.instance, instanceRef, value.field)
690+
}
688691

689-
val expr = if (sort == unresolvedSort) {
690-
val boolLValue = mkFieldLValue(boolSort, instanceRef, value.field)
691-
val fpLValue = mkFieldLValue(fp64Sort, instanceRef, value.field)
692-
val refLValue = mkFieldLValue(addressSort, instanceRef, value.field)
692+
override fun visit(value: EtsStaticFieldRef): UExpr<out USort>? = with(ctx) {
693+
val clazz = scene.projectAndSdkClasses.singleOrNull {
694+
it.signature == value.field.enclosingClass
695+
} ?: return null
693696

694-
scope.calcOnState {
695-
val bool = memory.read(boolLValue)
696-
val fp = memory.read(fpLValue)
697-
val ref = memory.read(refLValue)
697+
val instanceRef = scope.calcOnState { getStaticInstance(clazz) }
698698

699-
// If a fake object is already created and assigned to the field,
700-
// there is no need to recreate another one
701-
val fakeRef = if (ref.isFakeObject()) {
702-
ref
703-
} else {
704-
mkFakeValue(scope, bool, fp, ref)
699+
val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
700+
if (initializer != null) {
701+
val isInitialized = scope.calcOnState { isInitialized(clazz) }
702+
if (isInitialized) {
703+
scope.doWithState {
704+
// TODO: Handle static initializer result
705+
val result = methodResult
706+
if (result is TsMethodResult.Success && result.method == initializer) {
707+
methodResult = TsMethodResult.NoCall
708+
}
705709
}
706-
707-
memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
708-
709-
fakeRef
710+
} else {
711+
scope.doWithState {
712+
markInitialized(clazz)
713+
pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
714+
callStack.push(initializer, currentStatement)
715+
memory.stack.push(arrayOf(instanceRef), initializer.localsCount)
716+
newStmt(initializer.cfg.stmts.first())
717+
}
718+
return null
710719
}
711-
} else {
712-
val lValue = mkFieldLValue(sort, instanceRef, value.field)
713-
scope.calcOnState { memory.read(lValue) }
714720
}
715721

716-
if (assertIsSubtype(expr, value.type)) {
717-
expr
718-
} else {
719-
null
720-
}
721-
}
722-
723-
override fun visit(value: EtsStaticFieldRef): UExpr<out USort>? {
724-
logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
725-
error("Not supported $value")
722+
return handleFieldRef(instance = null, instanceRef, value.field)
726723
}
727724

728725
// endregion

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

Lines changed: 38 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,15 @@ import org.jacodb.ets.base.EtsNopStmt
1313
import org.jacodb.ets.base.EtsNullType
1414
import org.jacodb.ets.base.EtsParameterRef
1515
import org.jacodb.ets.base.EtsReturnStmt
16+
import org.jacodb.ets.base.EtsStaticFieldRef
1617
import org.jacodb.ets.base.EtsStmt
1718
import org.jacodb.ets.base.EtsSwitchStmt
1819
import org.jacodb.ets.base.EtsThis
1920
import org.jacodb.ets.base.EtsThrowStmt
2021
import org.jacodb.ets.base.EtsType
2122
import org.jacodb.ets.base.EtsValue
2223
import org.jacodb.ets.model.EtsMethod
24+
import org.jacodb.ets.utils.getDeclaredLocals
2325
import org.usvm.StepResult
2426
import org.usvm.StepScope
2527
import org.usvm.UInterpreter
@@ -43,6 +45,7 @@ import org.usvm.util.mkArrayIndexLValue
4345
import org.usvm.util.mkArrayLengthLValue
4446
import org.usvm.util.mkFieldLValue
4547
import org.usvm.util.mkRegisterStackLValue
48+
import org.usvm.util.resolveEtsField
4649
import org.usvm.utils.ensureSat
4750

4851
typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
@@ -178,15 +181,38 @@ class TsInterpreter(
178181

179182
is EtsInstanceFieldRef -> {
180183
val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState
181-
182-
val sort = typeToSort(lhv.type)
184+
val etsField = resolveEtsField(lhv.instance, lhv.field)
185+
val sort = typeToSort(etsField.type)
183186
if (sort == unresolvedSort) {
184187
val fakeObject = expr.toFakeObject(scope)
185188
val lValue = mkFieldLValue(addressSort, instance, lhv.field)
186189
memory.write(lValue, fakeObject, guard = trueExpr)
187190
} else {
188191
val lValue = mkFieldLValue(sort, instance, lhv.field)
189-
memory.write(lValue, expr.asExpr(sort), guard = trueExpr)
192+
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
193+
}
194+
}
195+
196+
is EtsStaticFieldRef -> {
197+
val clazz = scene.projectAndSdkClasses.singleOrNull {
198+
it.signature == lhv.field.enclosingClass
199+
} ?: return@doWithState
200+
201+
val instance = scope.calcOnState { getStaticInstance(clazz) }
202+
203+
// TODO: initialize the static field first
204+
// Note: Since we are assigning to a static field, we can omit its initialization,
205+
// if it does not have any side effects.
206+
207+
val field = clazz.fields.single { it.name == lhv.field.name }
208+
val sort = typeToSort(field.type)
209+
if (sort == unresolvedSort) {
210+
val lValue = mkFieldLValue(addressSort, instance, field.signature)
211+
val fakeObject = expr.toFakeObject(scope)
212+
memory.write(lValue, fakeObject, guard = trueExpr)
213+
} else {
214+
val lValue = mkFieldLValue(sort, instance, field.signature)
215+
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
190216
}
191217
}
192218

@@ -229,17 +255,21 @@ class TsInterpreter(
229255
TsExprResolver(ctx, scope, ::mapLocalToIdx)
230256

231257
// (method, localName) -> idx
232-
private val localVarToIdx: MutableMap<EtsMethod, MutableMap<String, Int>> = hashMapOf()
258+
private val localVarToIdx: MutableMap<EtsMethod, Map<String, Int>> = hashMapOf()
233259

234260
private fun mapLocalToIdx(method: EtsMethod, local: EtsValue): Int =
235261
// Note: below, 'n' means the number of arguments
236262
when (local) {
237263
// Note: locals have indices starting from (n+1)
238-
is EtsLocal -> localVarToIdx
239-
.getOrPut(method) { hashMapOf() }
240-
.let {
241-
it.getOrPut(local.name) { method.parametersWithThisCount + it.size }
264+
is EtsLocal -> {
265+
val map = localVarToIdx.getOrPut(method) {
266+
method.getDeclaredLocals().mapIndexed { idx, local ->
267+
val localIdx = idx + method.parametersWithThisCount
268+
local.name to localIdx
269+
}.toMap()
242270
}
271+
map[local.name] ?: error("Local not declared: $local")
272+
}
243273

244274
// Note: 'this' has index 'n'
245275
is EtsThis -> method.parameters.size

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

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
package org.usvm.machine.interpreter
2+
3+
import org.jacodb.ets.base.EtsBooleanType
4+
import org.jacodb.ets.model.EtsClass
5+
import org.jacodb.ets.model.EtsClassSignature
6+
import org.jacodb.ets.model.EtsFieldSignature
7+
import org.jacodb.ets.model.EtsFieldSubSignature
8+
import org.usvm.UBoolSort
9+
import org.usvm.UHeapRef
10+
import org.usvm.collection.field.UFieldLValue
11+
import org.usvm.isTrue
12+
import org.usvm.machine.state.TsState
13+
import org.usvm.util.mkFieldLValue
14+
15+
internal fun TsState.isInitialized(clazz: EtsClass): Boolean {
16+
val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
17+
val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
18+
return memory.read(initializedFlag).isTrue
19+
}
20+
21+
internal fun TsState.markInitialized(clazz: EtsClass) {
22+
val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
23+
val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
24+
memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr)
25+
}
26+
27+
private fun mkStaticFieldsInitializedFlag(
28+
instance: UHeapRef,
29+
clazz: EtsClassSignature,
30+
): UFieldLValue<String, UBoolSort> {
31+
val field = EtsFieldSignature(
32+
enclosingClass = clazz,
33+
sub = EtsFieldSubSignature(
34+
name = "__initialized__",
35+
type = EtsBooleanType,
36+
),
37+
)
38+
return mkFieldLValue(instance.ctx.boolSort, instance, field)
39+
}

0 commit comments

Comments
 (0)