Skip to content

Commit 549720e

Browse files
CaelmBleiddCaelmBleidd
committed
Fixes
1 parent e28484f commit 549720e

5 files changed

Lines changed: 143 additions & 34 deletions

File tree

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

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,16 @@ import io.ksmt.utils.asExpr
55
import org.jacodb.ets.model.EtsAliasType
66
import org.jacodb.ets.model.EtsAnyType
77
import org.jacodb.ets.model.EtsArrayType
8+
import org.jacodb.ets.model.EtsBooleanLiteralType
89
import org.jacodb.ets.model.EtsBooleanType
910
import org.jacodb.ets.model.EtsEnumValueType
1011
import org.jacodb.ets.model.EtsGenericType
1112
import org.jacodb.ets.model.EtsNullType
13+
import org.jacodb.ets.model.EtsNumberLiteralType
1214
import org.jacodb.ets.model.EtsNumberType
1315
import org.jacodb.ets.model.EtsRefType
1416
import org.jacodb.ets.model.EtsScene
17+
import org.jacodb.ets.model.EtsStringLiteralType
1518
import org.jacodb.ets.model.EtsStringType
1619
import org.jacodb.ets.model.EtsType
1720
import org.jacodb.ets.model.EtsUndefinedType
@@ -25,6 +28,7 @@ import org.usvm.UConcreteHeapRef
2528
import org.usvm.UContext
2629
import org.usvm.UExpr
2730
import org.usvm.UHeapRef
31+
import org.usvm.UIteExpr
2832
import org.usvm.USort
2933
import org.usvm.api.allocateConcreteRef
3034
import org.usvm.api.allocateStaticRef
@@ -132,6 +136,10 @@ class TsContext(
132136
}
133137
}
134138

139+
is EtsNumberLiteralType -> fp64Sort
140+
is EtsStringLiteralType -> addressSort
141+
is EtsBooleanLiteralType -> boolSort
142+
135143
else -> TODO("${type::class.simpleName} is not yet supported: $type")
136144
}
137145

@@ -212,6 +220,13 @@ class TsContext(
212220
if (isFakeObject()) {
213221
return extractRef(scope)
214222
}
223+
224+
if (this is UIteExpr) {
225+
val positiveBranch = trueBranch.unwrapRef(scope)
226+
val negativeBranch = falseBranch.unwrapRef(scope)
227+
return mkIte(condition, positiveBranch, negativeBranch)
228+
}
229+
215230
return this
216231
}
217232

@@ -220,6 +235,13 @@ class TsContext(
220235
scope.assert(getFakeType(scope).refTypeExpr)
221236
return extractRef(scope)
222237
}
238+
239+
if (this is UIteExpr) {
240+
val positiveBranch = trueBranch.unwrapRefWithPathConstraint(scope)
241+
val negativeBranch = falseBranch.unwrapRefWithPathConstraint(scope)
242+
return mkIte(condition, positiveBranch, negativeBranch)
243+
}
244+
223245
return this
224246
}
225247

@@ -272,7 +294,7 @@ class TsContext(
272294
fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
273295
return scope.calcOnState { extractRef(memory) }
274296
}
275-
297+
276298
// This is an identifier for a special function representing the 'resolve' function used in promises.
277299
// It is not a real function in the code, but we need it to handle promise resolution.
278300
val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
55
import org.usvm.UBoolExpr
66
import org.usvm.UBoolSort
77
import org.usvm.UExpr
8+
import org.usvm.UIteExpr
89
import org.usvm.USort
910
import org.usvm.api.makeSymbolicPrimitive
1011
import org.usvm.isFalse
@@ -19,6 +20,12 @@ fun TsContext.mkTruthyExpr(
1920
expr: UExpr<out USort>,
2021
scope: TsStepScope,
2122
): UBoolExpr = scope.calcOnState {
23+
if (expr is UIteExpr) {
24+
val trueBranch = mkTruthyExpr(expr.trueBranch, scope)
25+
val falseBranch = mkTruthyExpr(expr.falseBranch, scope)
26+
return@calcOnState mkIte(expr.condition, trueBranch, falseBranch)
27+
}
28+
2229
if (expr.isFakeObject()) {
2330
val falseBranchGround = makeSymbolicPrimitive(boolSort)
2431

@@ -92,6 +99,12 @@ fun TsContext.mkNumericExpr(
9299
expr: UExpr<out USort>,
93100
scope: TsStepScope,
94101
): UExpr<KFp64Sort> {
102+
if (expr is UIteExpr) {
103+
val trueBranch = mkNumericExpr(expr.trueBranch, scope)
104+
val falseBranch = mkNumericExpr(expr.falseBranch, scope)
105+
return mkIte(expr.condition, trueBranch, falseBranch)
106+
}
107+
95108
if (expr.isFakeObject()) {
96109
val type = expr.getFakeType(scope)
97110
return mkIte(
@@ -154,6 +167,12 @@ fun TsContext.mkNullishExpr(
154167
expr: UExpr<out USort>,
155168
scope: TsStepScope,
156169
): UBoolExpr {
170+
if (expr is UIteExpr) {
171+
val trueBranch = mkNullishExpr(expr.trueBranch, scope)
172+
val falseBranch = mkNullishExpr(expr.falseBranch, scope)
173+
return mkIte(expr.condition, trueBranch, falseBranch)
174+
}
175+
157176
// Handle fake objects specially
158177
if (expr.isFakeObject()) {
159178
val fakeType = expr.getFakeType(scope)

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

Lines changed: 87 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -360,51 +360,102 @@ class TsExprResolver(
360360

361361
override fun visit(expr: EtsTypeOfExpr): UExpr<out USort>? = with(ctx) {
362362
val arg = resolve(expr.arg) ?: return null
363-
364363
if (arg.sort == fp64Sort) {
365364
return mkStringConstant("number", scope)
366365
}
367366
if (arg.sort == boolSort) {
368367
return mkStringConstant("boolean", scope)
369368
}
370369
if (arg.sort == addressSort) {
371-
val ref = arg.asExpr(addressSort)
372-
return mkIte(
373-
condition = mkHeapRefEq(ref, mkTsNullValue()),
374-
trueBranch = mkStringConstant("object", scope),
375-
falseBranch = mkIte(
376-
condition = mkHeapRefEq(ref, mkUndefinedValue()),
377-
trueBranch = mkStringConstant("undefined", scope),
370+
val resolvedArg = arg.asExpr(addressSort)
371+
372+
val processFakeFunction = { ref: UHeapRef ->
373+
check(ref.isFakeObject())
374+
375+
val fakeType = scope.calcOnState { ref.getFakeType(memory) }
376+
mkIte(
377+
fakeType.fpTypeExpr,
378+
mkStringConstant("number", scope),
379+
mkIte(
380+
fakeType.boolTypeExpr,
381+
mkStringConstant("boolean", scope),
382+
mkIte(
383+
fakeType.refTypeExpr and mkHeapRefEq(ref.extractRef(scope), mkTsNullValue()),
384+
mkStringConstant("object", scope),
385+
mkIte(
386+
fakeType.refTypeExpr and mkHeapRefEq(ref.extractRef(scope), mkUndefinedValue()),
387+
mkStringConstant("undefined", scope),
388+
mkStringConstant("object", scope) // TODO add string, function
389+
)
390+
)
391+
)
392+
)
393+
}
394+
395+
val regularResolve = { ref: UHeapRef ->
396+
mkIte(
397+
condition = mkHeapRefEq(ref, mkTsNullValue()),
398+
trueBranch = mkStringConstant("object", scope),
378399
falseBranch = mkIte(
379-
condition = scope.calcOnState {
380-
val unwrappedRef = ref.unwrapRefWithPathConstraint(scope)
381-
382-
// TODO: adhoc: "expand" ITE
383-
if (unwrappedRef is UIteExpr<*>) {
384-
val trueBranch = unwrappedRef.trueBranch
385-
val falseBranch = unwrappedRef.falseBranch
386-
if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
387-
val unwrappedTrueExpr =
388-
trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
389-
val unwrappedFalseExpr =
390-
falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
391-
return@calcOnState mkIte(
392-
condition = unwrappedRef.condition,
393-
trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
394-
falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType),
395-
)
400+
condition = mkHeapRefEq(ref, mkUndefinedValue()),
401+
trueBranch = mkStringConstant("undefined", scope),
402+
falseBranch = mkIte(
403+
condition = scope.calcOnState {
404+
val unwrappedRef = ref.unwrapRef(scope)
405+
406+
// TODO: adhoc: "expand" ITE
407+
// TODO correst support for fake objects, including primitive branches
408+
if (unwrappedRef is UIteExpr<*>) {
409+
val trueBranch = unwrappedRef.trueBranch
410+
val falseBranch = unwrappedRef.falseBranch
411+
if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
412+
val unwrappedTrueExpr =
413+
trueBranch.asExpr(addressSort).unwrapRef(scope)
414+
val unwrappedFalseExpr =
415+
falseBranch.asExpr(addressSort).unwrapRef(scope)
416+
return@calcOnState mkIte(
417+
condition = unwrappedRef.condition,
418+
trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
419+
falseBranch = memory.types.evalTypeEquals(
420+
unwrappedFalseExpr,
421+
EtsStringType
422+
),
423+
)
424+
}
396425
}
397-
}
398426

399-
memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
400-
},
401-
trueBranch = mkStringConstant("string", scope),
402-
falseBranch = mkStringConstant("object", scope),
427+
memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
428+
},
429+
trueBranch = mkStringConstant("string", scope),
430+
falseBranch = mkStringConstant("object", scope),
431+
)
403432
)
404433
)
405-
)
406-
}
407434

435+
}
436+
437+
if (resolvedArg.isFakeObject()) {
438+
return processFakeFunction(resolvedArg)
439+
}
440+
441+
if (resolvedArg is UIteExpr) {
442+
val trueBranch = if (resolvedArg.trueBranch.isFakeObject()) {
443+
processFakeFunction(resolvedArg.trueBranch)
444+
} else {
445+
regularResolve(resolvedArg.trueBranch)
446+
}
447+
448+
val falseBranch = if (resolvedArg.falseBranch.isFakeObject()) {
449+
processFakeFunction(resolvedArg.falseBranch)
450+
} else {
451+
regularResolve(resolvedArg.falseBranch)
452+
}
453+
454+
return mkIte(resolvedArg.condition, trueBranch, falseBranch)
455+
}
456+
457+
return regularResolve(resolvedArg)
458+
}
408459
logger.error { "visit(${expr::class.simpleName}) is not implemented yet" }
409460
error("Not supported $expr")
410461
}
@@ -419,6 +470,7 @@ class TsExprResolver(
419470
when (val operand = expr.arg) {
420471
is EtsInstanceFieldRef -> {
421472
val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null
473+
val unwrappedRef = instance.unwrapRefWithPathConstraint(scope)
422474

423475
// Check for null/undefined access
424476
checkUndefinedOrNullPropertyRead(instance) ?: return null
@@ -429,7 +481,8 @@ class TsExprResolver(
429481
// In such case, the "overwriting" the field value with undefined does nothing
430482
// to the actual number/boolean/string value inside the field,
431483
// [if only we read the field using that "other" sort].
432-
val fieldLValue = mkFieldLValue(addressSort, instance, operand.field)
484+
// TODO use val resolvedField = resolveEtsField(operand.instance, operand.field, hierarchy) instead
485+
val fieldLValue = mkFieldLValue(addressSort, unwrappedRef, operand.field)
433486
scope.doWithState {
434487
memory.write(fieldLValue, mkUndefinedValue(), guard = trueExpr)
435488
}
@@ -1205,6 +1258,7 @@ class TsExprResolver(
12051258
return expr
12061259
}
12071260

1261+
// TODO condition for unwrapped value
12081262
fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
12091263
val ref = instance.unwrapRef(scope)
12101264

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -845,6 +845,8 @@ class TsInterpreter(
845845
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
846846
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
847847
}
848+
849+
// TODO union type
848850
}
849851

850852
val model = solver.check(state.pathConstraints).ensureSat().model

‎usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsLocal
88
import org.jacodb.ets.model.EtsMethod
99
import org.jacodb.ets.model.EtsScene
1010
import org.jacodb.ets.model.EtsUnclearRefType
11+
import org.jacodb.ets.model.EtsUnionType
1112
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
1213
import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
1314
import org.usvm.machine.TsContext
@@ -46,6 +47,17 @@ fun TsContext.resolveEtsField(
4647
val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
4748
if (field != null) return TsResolutionResult.create(field)
4849
}
50+
51+
is EtsUnionType -> {
52+
// TODO something similar to
53+
// if (instanceType.types.all { it is EtsRefType }) {
54+
// val fields = instanceType.types
55+
// .map { tryGetSingleField(scene, it.typeName, field.name, hierarchy) }
56+
// if (fields.all { it != null }) {
57+
// return TsResolutionResult.create(fields.mapNotNull { it })
58+
// }
59+
// }
60+
}
4961
}
5062
}
5163

0 commit comments

Comments
 (0)