Skip to content

Commit e85e253

Browse files
LipenLipen
committed
Extract statics initiliazation
1 parent 17c9166 commit e85e253

5 files changed

Lines changed: 81 additions & 60 deletions

File tree

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

Lines changed: 7 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -7,16 +7,11 @@ import org.jacodb.ets.model.EtsFieldSignature
77
import org.jacodb.ets.model.EtsInstanceFieldRef
88
import org.jacodb.ets.model.EtsLocal
99
import org.jacodb.ets.model.EtsStaticFieldRef
10-
import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
1110
import org.usvm.UExpr
1211
import org.usvm.UHeapRef
1312
import org.usvm.machine.TsContext
1413
import org.usvm.machine.interpreter.TsStepScope
15-
import org.usvm.machine.interpreter.isInitialized
16-
import org.usvm.machine.interpreter.markInitialized
17-
import org.usvm.machine.state.TsMethodResult
18-
import org.usvm.machine.state.localsCount
19-
import org.usvm.machine.state.newStmt
14+
import org.usvm.machine.interpreter.ensureStaticsInitialized
2015
import org.usvm.machine.types.EtsAuxiliaryType
2116
import org.usvm.machine.types.mkFakeValue
2217
import org.usvm.util.EtsHierarchy
@@ -135,37 +130,17 @@ internal fun TsContext.readStaticField(
135130
field: EtsFieldSignature,
136131
hierarchy: EtsHierarchy,
137132
): UExpr<*>? {
133+
// TODO: handle unresolved class, or multiple classes
138134
val clazz = scene.projectAndSdkClasses.singleOrNull {
139135
it.signature == field.enclosingClass
140136
} ?: return null
141137

142-
val instance = scope.calcOnState { getStaticInstance(clazz) }
138+
// Initialize statics in `clazz` if necessary.
139+
ensureStaticsInitialized(scope, clazz) ?: return null
143140

144-
val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
145-
if (initializer != null) {
146-
val isInitialized = scope.calcOnState { isInitialized(clazz) }
147-
if (isInitialized) {
148-
scope.doWithState {
149-
// TODO: Handle static initializer result
150-
val result = methodResult
151-
// TODO: Why this signature check is needed?
152-
// TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere.
153-
if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) {
154-
methodResult = TsMethodResult.NoCall
155-
}
156-
}
157-
} else {
158-
scope.doWithState {
159-
markInitialized(clazz)
160-
pushSortsForArguments(instance = null, args = emptyList()) { getLocalIdx(it, lastEnteredMethod) }
161-
registerCallee(currentStatement, initializer.cfg)
162-
callStack.push(initializer, currentStatement)
163-
memory.stack.push(arrayOf(instance), initializer.localsCount)
164-
newStmt(initializer.cfg.stmts.first())
165-
}
166-
return null
167-
}
168-
}
141+
// Get the static instance.
142+
val instance = scope.calcOnState { getStaticInstance(clazz) }
169143

144+
// Read the field.
170145
return readField(scope, null, instance, field, hierarchy)
171146
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ internal fun TsState.initializeGlobals(file: EtsFile) {
6464
markGlobalsInitialized(file)
6565
val dfltObject = getDfltObject(file)
6666
val dfltMethod = file.getDfltMethod()
67-
pushSortsForArguments(instance = null, args = emptyList()) { null }
67+
pushSortsForArguments(0) { null }
6868
registerCallee(currentStatement, dfltMethod.cfg)
6969
callStack.push(dfltMethod, currentStatement)
7070
memory.stack.push(arrayOf(dfltObject), dfltMethod.localsCount)

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

Lines changed: 53 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,74 @@
11
package org.usvm.machine.interpreter
22

3+
import mu.KotlinLogging
34
import org.jacodb.ets.model.EtsClass
45
import org.jacodb.ets.model.EtsClassSignature
6+
import org.jacodb.ets.model.EtsMethod
7+
import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
58
import org.usvm.UBoolSort
9+
import org.usvm.UExpr
610
import org.usvm.UHeapRef
711
import org.usvm.collection.field.UFieldLValue
812
import org.usvm.isTrue
13+
import org.usvm.machine.TsContext
14+
import org.usvm.machine.state.TsMethodResult
915
import org.usvm.machine.state.TsState
16+
import org.usvm.machine.state.localsCount
17+
import org.usvm.machine.state.newStmt
1018
import org.usvm.util.mkFieldLValue
1119

20+
private val logger = KotlinLogging.logger {}
21+
22+
private fun mkStaticFieldsInitializedFlag(
23+
instance: UHeapRef,
24+
clazz: EtsClassSignature,
25+
): UFieldLValue<String, UBoolSort> {
26+
return mkFieldLValue(instance.ctx.boolSort, instance, "__initialized__")
27+
}
28+
1229
internal fun TsState.isInitialized(clazz: EtsClass): Boolean {
13-
val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
30+
val instance = getStaticInstance(clazz)
1431
val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
1532
return memory.read(initializedFlag).isTrue
1633
}
1734

18-
internal fun TsState.markInitialized(clazz: EtsClass) {
19-
val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
35+
internal fun TsState.markStaticsInitialized(clazz: EtsClass) {
36+
val instance = getStaticInstance(clazz)
2037
val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
2138
memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr)
2239
}
2340

24-
private fun mkStaticFieldsInitializedFlag(
25-
instance: UHeapRef,
26-
clazz: EtsClassSignature,
27-
): UFieldLValue<String, UBoolSort> {
28-
return mkFieldLValue(instance.ctx.boolSort, instance, "__initialized__")
41+
private fun TsState.initializeStatics(clazz: EtsClass, initializer: EtsMethod) {
42+
markStaticsInitialized(clazz)
43+
val instance = getStaticInstance(clazz)
44+
pushSortsForArguments(0) { null }
45+
registerCallee(currentStatement, initializer.cfg)
46+
callStack.push(initializer, currentStatement)
47+
memory.stack.push(arrayOf(instance), initializer.localsCount)
48+
newStmt(initializer.cfg.stmts.first())
49+
}
50+
51+
internal fun TsContext.ensureStaticsInitialized(
52+
scope: TsStepScope,
53+
clazz: EtsClass,
54+
): Unit? = scope.calcOnState {
55+
val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
56+
if (initializer == null) {
57+
return@calcOnState Unit
58+
}
59+
60+
// Initialize statics in `clazz` if necessary
61+
if (!isInitialized(clazz)) {
62+
logger.info { "Statics are not initialized for class: $clazz" }
63+
initializeStatics(clazz, initializer)
64+
return@calcOnState null
65+
}
66+
67+
// TODO: Handle static initializer result
68+
val result = methodResult
69+
// TODO: Why this signature check is needed?
70+
// TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere.
71+
if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) {
72+
methodResult = TsMethodResult.NoCall
73+
}
2974
}

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

Lines changed: 7 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,11 @@ import org.jacodb.ets.model.EtsBlockCfg
55
import org.jacodb.ets.model.EtsClass
66
import org.jacodb.ets.model.EtsFile
77
import org.jacodb.ets.model.EtsFileSignature
8-
import org.jacodb.ets.model.EtsLocal
98
import org.jacodb.ets.model.EtsMethod
109
import org.jacodb.ets.model.EtsNumberType
1110
import org.jacodb.ets.model.EtsStmt
1211
import org.jacodb.ets.model.EtsStringType
1312
import org.jacodb.ets.model.EtsType
14-
import org.jacodb.ets.model.EtsValue
1513
import org.usvm.PathNode
1614
import org.usvm.UCallStack
1715
import org.usvm.UConcreteHeapRef
@@ -132,25 +130,15 @@ class TsState(
132130
}
133131

134132
fun pushSortsForArguments(
135-
instance: EtsLocal?,
136-
args: List<EtsLocal>,
137-
localToIdx: (EtsValue) -> Int?,
133+
n: Int,
134+
idxToSort: (Int) -> USort?,
138135
) {
139-
val argSorts = args.map { arg ->
140-
val argIdx = localToIdx(arg)
141-
?: error("Arguments must present in the locals, but $arg is absent")
142-
getOrPutSortForLocal(argIdx) { ctx.typeToSort(arg.type) }
143-
}
144-
145-
val instanceIdx = instance?.let { localToIdx(it) }
146-
val instanceSort = instanceIdx?.let { getOrPutSortForLocal(it) { ctx.typeToSort(instance.type) } }
147-
148-
// Note: first, push an empty map, then fill the arguments, and then the instance (this)
149136
pushLocalToSortStack()
150-
instanceSort?.let { saveSortForLocal(0, it) }
151-
argSorts.forEachIndexed { i, sort ->
152-
val idx = i + 1 // + 1 because 0 is reserved for `this`
153-
saveSortForLocal(idx, sort)
137+
for (i in 0..n) {
138+
val sort = idxToSort(i)
139+
if (sort != null) {
140+
saveSortForLocal(i, sort)
141+
}
154142
}
155143
}
156144

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,3 +32,16 @@ inline val EtsMethod.parametersWithThisCount: Int
3232

3333
inline val EtsMethod.localsCount: Int
3434
get() = locals.size
35+
36+
// TODO: fix handling of arguments and use this function in machine
37+
fun TsState.makeCall(
38+
method: EtsMethod,
39+
instance: UExpr<*>,
40+
args: List<UExpr<*>>,
41+
) {
42+
pushSortsForArguments(0) { null }
43+
registerCallee(currentStatement, method.cfg)
44+
callStack.push(method, currentStatement)
45+
memory.stack.push(arrayOf(instance) + args.toTypedArray(), method.localsCount)
46+
newStmt(method.cfg.stmts.first())
47+
}

0 commit comments

Comments
 (0)