Skip to content

Commit 5f0b67f

Browse files
LipenLipen
authored
[TS] Some fixes to read/write, fake objects, calls (#329)
1 parent 6194bbd commit 5f0b67f

File tree

17 files changed

+405
-280
lines changed

17 files changed

+405
-280
lines changed

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

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
package org.usvm.machine.expr
2+
3+
import io.ksmt.utils.asExpr
4+
import mu.KotlinLogging
5+
import org.jacodb.ets.model.EtsInstanceCallExpr
6+
import org.jacodb.ets.model.EtsMethodSignature
7+
import org.usvm.UExpr
8+
import org.usvm.machine.TsContext
9+
import org.usvm.machine.TsVirtualMethodCallStmt
10+
import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation
11+
import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure
12+
import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation
13+
import org.usvm.machine.interpreter.TsStepScope
14+
import org.usvm.machine.state.TsMethodResult
15+
import org.usvm.machine.state.lastStmt
16+
import org.usvm.machine.state.newStmt
17+
18+
private val logger = KotlinLogging.logger {}
19+
20+
internal fun TsExprResolver.handleInstanceCall(
21+
expr: EtsInstanceCallExpr,
22+
): UExpr<*>? = with(ctx) {
23+
// Check if the method was already called and returned a value.
24+
when (val result = scope.calcOnState { methodResult }) {
25+
is TsMethodResult.Success -> {
26+
scope.doWithState { methodResult = TsMethodResult.NoCall }
27+
return result.value
28+
}
29+
30+
is TsMethodResult.TsException -> {
31+
error("Exception should be handled earlier")
32+
}
33+
34+
is TsMethodResult.NoCall -> {} // proceed to call
35+
}
36+
37+
// Try to approximate the call.
38+
when (val result = tryApproximateInstanceCall(expr)) {
39+
is SuccessfulApproximation -> return result.expr
40+
is ResolveFailure -> return null
41+
is NoApproximation -> {}
42+
}
43+
44+
// Resolve the instance.
45+
val instance = run {
46+
val resolved = resolve(expr.instance) ?: return null
47+
if (resolved.isFakeObject()) {
48+
val fakeType = resolved.getFakeType(scope)
49+
scope.assert(fakeType.refTypeExpr) ?: run {
50+
logger.warn { "Calls on non-ref (fake) instance is not supported: $expr" }
51+
return null
52+
}
53+
resolved.extractRef(scope)
54+
} else {
55+
if (resolved.sort != addressSort) {
56+
logger.warn { "Calling method on non-ref instance is not yet supported: $expr" }
57+
scope.assert(falseExpr)
58+
return null
59+
}
60+
resolved.asExpr(addressSort)
61+
}
62+
}
63+
64+
// Check for undefined or null property access.
65+
checkUndefinedOrNullPropertyRead(scope, instance, expr.callee.name) ?: return null
66+
67+
// Resolve arguments.
68+
val args = expr.args.map { resolve(it) ?: return null }
69+
70+
// Call.
71+
callInstanceMethod(scope, expr.callee, instance, args)
72+
}
73+
74+
fun TsContext.callInstanceMethod(
75+
scope: TsStepScope,
76+
callee: EtsMethodSignature,
77+
instance: UExpr<*>,
78+
args: List<UExpr<*>>,
79+
): UExpr<*>? {
80+
// Create the virtual call statement.
81+
val virtualCall = TsVirtualMethodCallStmt(
82+
callee = callee,
83+
instance = instance,
84+
args = args,
85+
returnSite = scope.calcOnState { lastStmt },
86+
)
87+
scope.doWithState { newStmt(virtualCall) }
88+
89+
// Return null to indicate that we are waiting for the call to be executed.
90+
return null
91+
}

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

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -31,20 +31,7 @@ import org.usvm.util.resolveEtsMethods
3131

3232
private val logger = KotlinLogging.logger {}
3333

34-
sealed interface TsExprApproximationResult {
35-
data class SuccessfulApproximation(val expr: UExpr<*>) : TsExprApproximationResult
36-
data object ResolveFailure : TsExprApproximationResult
37-
data object NoApproximation : TsExprApproximationResult
38-
39-
companion object {
40-
fun from(expr: UExpr<*>?): TsExprApproximationResult = when {
41-
expr != null -> SuccessfulApproximation(expr)
42-
else -> ResolveFailure
43-
}
44-
}
45-
}
46-
47-
fun TsExprResolver.tryApproximateInstanceCall(
34+
internal fun TsExprResolver.tryApproximateInstanceCall(
4835
expr: EtsInstanceCallExpr,
4936
): TsExprApproximationResult = with(ctx) {
5037
// Mock all calls to `Logger` methods

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

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
package org.usvm.machine.expr
2+
3+
import mu.KotlinLogging
4+
import org.jacodb.ets.model.EtsClassType
5+
import org.jacodb.ets.model.EtsMethod
6+
import org.jacodb.ets.model.EtsMethodSignature
7+
import org.jacodb.ets.model.EtsStaticCallExpr
8+
import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
9+
import org.usvm.UExpr
10+
import org.usvm.machine.Constants
11+
import org.usvm.machine.TsConcreteMethodCallStmt
12+
import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation
13+
import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure
14+
import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation
15+
import org.usvm.machine.state.TsMethodResult
16+
import org.usvm.machine.state.lastStmt
17+
import org.usvm.machine.state.newStmt
18+
import org.usvm.util.TsResolutionResult
19+
20+
private val logger = KotlinLogging.logger {}
21+
22+
internal fun TsExprResolver.handleStaticCall(
23+
expr: EtsStaticCallExpr,
24+
): UExpr<*>? = with(ctx) {
25+
// Check if the method was already called and returned a value.
26+
when (val result = scope.calcOnState { methodResult }) {
27+
is TsMethodResult.Success -> {
28+
scope.doWithState { methodResult = TsMethodResult.NoCall }
29+
return result.value
30+
}
31+
32+
is TsMethodResult.TsException -> {
33+
error("Exception should be handled earlier")
34+
}
35+
36+
is TsMethodResult.NoCall -> {} // proceed to call
37+
}
38+
39+
// Try to approximate the call.
40+
when (val result = tryApproximateStaticCall(expr)) {
41+
is SuccessfulApproximation -> return result.expr
42+
is ResolveFailure -> return null
43+
is NoApproximation -> {}
44+
}
45+
46+
// Resolve the static method.
47+
when (val resolved = resolveStaticMethod(expr.callee)) {
48+
is TsResolutionResult.Empty -> {
49+
logger.error { "Could not resolve static call: ${expr.callee}" }
50+
scope.assert(falseExpr) ?: return null
51+
}
52+
53+
is TsResolutionResult.Ambiguous -> {
54+
processAmbiguousStaticMethod(resolved, expr)
55+
}
56+
57+
is TsResolutionResult.Unique -> {
58+
processUniqueStaticMethod(resolved, expr)
59+
}
60+
}
61+
62+
// Return null to indicate that we are awaiting the call to be executed.
63+
null
64+
}
65+
66+
private fun TsExprResolver.resolveStaticMethod(
67+
method: EtsMethodSignature,
68+
): TsResolutionResult<EtsMethod> {
69+
// Perfect signature:
70+
if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
71+
val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass))
72+
if (classes.size > 1) {
73+
val methods = classes.map { it.methods.single { it.name == method.name } }
74+
return TsResolutionResult.create(methods)
75+
}
76+
77+
if (classes.isEmpty()) return TsResolutionResult.Empty
78+
79+
val clazz = classes.single()
80+
val methods = clazz.methods.filter { it.name == method.name }
81+
return TsResolutionResult.create(methods)
82+
}
83+
84+
// Unknown signature:
85+
val methods = ctx.scene.projectAndSdkClasses
86+
.flatMap { it.methods }
87+
.filter { it.name == method.name }
88+
89+
return TsResolutionResult.create(methods)
90+
}
91+
92+
private fun TsExprResolver.processAmbiguousStaticMethod(
93+
resolved: TsResolutionResult.Ambiguous<EtsMethod>,
94+
expr: EtsStaticCallExpr,
95+
) {
96+
val args = expr.args.map { resolve(it) ?: return }
97+
val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
98+
val staticInstances = scope.calcOnState {
99+
staticProperties.map { getStaticInstance(it.enclosingClass!!) }
100+
}
101+
val concreteCalls = staticProperties.mapIndexed { index, value ->
102+
TsConcreteMethodCallStmt(
103+
callee = value,
104+
instance = staticInstances[index],
105+
args = args,
106+
returnSite = scope.calcOnState { lastStmt }
107+
)
108+
}
109+
scope.forkMulti(
110+
concreteCalls.map { stmt ->
111+
ctx.mkTrue() to { newStmt(stmt) }
112+
}
113+
)
114+
}
115+
116+
private fun TsExprResolver.processUniqueStaticMethod(
117+
resolved: TsResolutionResult.Unique<EtsMethod>,
118+
expr: EtsStaticCallExpr,
119+
) {
120+
val instance = scope.calcOnState {
121+
getStaticInstance(resolved.property.enclosingClass!!)
122+
}
123+
val args = expr.args.map { resolve(it) ?: return }
124+
val concreteCall = TsConcreteMethodCallStmt(
125+
callee = resolved.property,
126+
instance = instance,
127+
args = args,
128+
returnSite = scope.calcOnState { lastStmt },
129+
)
130+
scope.doWithState { newStmt(concreteCall) }
131+
}

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

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
package org.usvm.machine.expr
2+
3+
import org.jacodb.ets.model.EtsStaticCallExpr
4+
import org.usvm.UExpr
5+
import org.usvm.machine.expr.TsExprApproximationResult.Companion.from
6+
7+
internal fun TsExprResolver.tryApproximateStaticCall(
8+
expr: EtsStaticCallExpr,
9+
): TsExprApproximationResult {
10+
// Mock `$r` calls
11+
if (expr.callee.name == "\$r") {
12+
return from(handleR())
13+
}
14+
15+
// Handle `Number(...)` calls
16+
if (expr.callee.name == "Number") {
17+
return from(handleNumberConverter(expr))
18+
}
19+
20+
// Handle `Boolean(...)` calls
21+
if (expr.callee.name == "Boolean") {
22+
return from(handleBooleanConverter(expr))
23+
}
24+
25+
return TsExprApproximationResult.NoApproximation
26+
}
27+
28+
private fun TsExprResolver.handleR(): UExpr<*> = with(ctx) {
29+
val mockSymbol = scope.calcOnState {
30+
memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)
31+
}
32+
scope.assert(mkNot(mkEq(mockSymbol, mkTsNullValue())))
33+
mockSymbol
34+
}
35+
36+
private fun TsExprResolver.handleNumberConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
37+
check(expr.args.size == 1) {
38+
"Number() should have exactly one argument, but got ${expr.args.size}"
39+
}
40+
val arg = resolve(expr.args.single()) ?: return null
41+
return mkNumericExpr(arg, scope)
42+
}
43+
44+
private fun TsExprResolver.handleBooleanConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
45+
check(expr.args.size == 1) {
46+
"Boolean() should have exactly one argument, but got ${expr.args.size}"
47+
}
48+
val arg = resolve(expr.args.single()) ?: return null
49+
return mkTruthyExpr(arg, scope)
50+
}

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

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -193,19 +193,30 @@ fun TsState.throwException(reason: String) {
193193
methodResult = TsMethodResult.TsException(ref, EtsStringType)
194194
}
195195

196+
fun TsContext.mkNotNullOrUndefined(ref: UHeapRef): UBoolExpr {
197+
require(!ref.isFakeObject()) {
198+
"Fake object handling should be done outside of this function"
199+
}
200+
return mkNot(
201+
mkOr(
202+
mkHeapRefEq(ref, mkTsNullValue()),
203+
mkHeapRefEq(ref, mkUndefinedValue())
204+
)
205+
)
206+
}
207+
196208
fun TsContext.checkUndefinedOrNullPropertyRead(
197209
scope: TsStepScope,
198210
instance: UHeapRef,
199211
propertyName: String,
200212
): Unit? {
201-
val ref = instance.unwrapRef(scope)
202-
val condition = mkAnd(
203-
mkNot(mkHeapRefEq(ref, mkUndefinedValue())),
204-
mkNot(mkHeapRefEq(ref, mkTsNullValue())),
205-
)
213+
require(!instance.isFakeObject()) {
214+
"Fake object handling should be done outside of this function"
215+
}
216+
val condition = mkNotNullOrUndefined(instance)
206217
return scope.fork(
207218
condition,
208-
blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $ref") }
219+
blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $instance") }
209220
)
210221
}
211222

0 commit comments

Comments
 (0)