Skip to content

[TS] Fixes with fake objects inside UIteExpr #327

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
CaelmBleidd wants to merge 1 commit into from
Closed

[TS] Fixes with fake objects inside UIteExpr #327

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 23 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,13 +5,16 @@ import io.ksmt.utils.asExpr
import org.jacodb.ets.model.EtsAliasType
import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsBooleanLiteralType
import org.jacodb.ets.model.EtsBooleanType
import org.jacodb.ets.model.EtsEnumValueType
import org.jacodb.ets.model.EtsGenericType
import org.jacodb.ets.model.EtsNullType
import org.jacodb.ets.model.EtsNumberLiteralType
import org.jacodb.ets.model.EtsNumberType
import org.jacodb.ets.model.EtsRefType
import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.model.EtsStringLiteralType
import org.jacodb.ets.model.EtsStringType
import org.jacodb.ets.model.EtsType
import org.jacodb.ets.model.EtsUndefinedType
Expand All @@ -25,6 +28,7 @@ import org.usvm.UConcreteHeapRef
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.UIteExpr
import org.usvm.USort
import org.usvm.api.allocateConcreteRef
import org.usvm.api.allocateStaticRef
Expand Down Expand Up @@ -132,6 +136,10 @@ class TsContext(
}
}

is EtsNumberLiteralType -> fp64Sort
is EtsStringLiteralType -> addressSort
is EtsBooleanLiteralType -> boolSort

else -> TODO("${type::class.simpleName} is not yet supported: $type")
}

Expand Down Expand Up @@ -212,6 +220,13 @@ class TsContext(
if (isFakeObject()) {
return extractRef(scope)
}

if (this is UIteExpr) {
val positiveBranch = trueBranch.unwrapRef(scope)
val negativeBranch = falseBranch.unwrapRef(scope)
return mkIte(condition, positiveBranch, negativeBranch)
}

return this
}

Expand All @@ -220,6 +235,13 @@ class TsContext(
scope.assert(getFakeType(scope).refTypeExpr)
return extractRef(scope)
}

if (this is UIteExpr) {
val positiveBranch = trueBranch.unwrapRefWithPathConstraint(scope)
val negativeBranch = falseBranch.unwrapRefWithPathConstraint(scope)
return mkIte(condition, positiveBranch, negativeBranch)
}

return this
}

Expand Down Expand Up @@ -272,7 +294,7 @@ class TsContext(
fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
return scope.calcOnState { extractRef(memory) }
}

// This is an identifier for a special function representing the 'resolve' function used in promises.
// It is not a real function in the code, but we need it to handle promise resolution.
val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()
Expand Down
19 changes: 19 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
import org.usvm.UBoolExpr
import org.usvm.UBoolSort
import org.usvm.UExpr
import org.usvm.UIteExpr
import org.usvm.USort
import org.usvm.api.makeSymbolicPrimitive
import org.usvm.isFalse
Expand All @@ -19,6 +20,12 @@ fun TsContext.mkTruthyExpr(
expr: UExpr<out USort>,
scope: TsStepScope,
): UBoolExpr = scope.calcOnState {
if (expr is UIteExpr) {
val trueBranch = mkTruthyExpr(expr.trueBranch, scope)
val falseBranch = mkTruthyExpr(expr.falseBranch, scope)
return@calcOnState mkIte(expr.condition, trueBranch, falseBranch)
}

if (expr.isFakeObject()) {
val falseBranchGround = makeSymbolicPrimitive(boolSort)

Expand Down Expand Up @@ -92,6 +99,12 @@ fun TsContext.mkNumericExpr(
expr: UExpr<out USort>,
scope: TsStepScope,
): UExpr<KFp64Sort> {
if (expr is UIteExpr) {
val trueBranch = mkNumericExpr(expr.trueBranch, scope)
val falseBranch = mkNumericExpr(expr.falseBranch, scope)
return mkIte(expr.condition, trueBranch, falseBranch)
}

if (expr.isFakeObject()) {
val type = expr.getFakeType(scope)
return mkIte(
Expand Down Expand Up @@ -154,6 +167,12 @@ fun TsContext.mkNullishExpr(
expr: UExpr<out USort>,
scope: TsStepScope,
): UBoolExpr {
if (expr is UIteExpr) {
val trueBranch = mkNullishExpr(expr.trueBranch, scope)
val falseBranch = mkNullishExpr(expr.falseBranch, scope)
return mkIte(expr.condition, trueBranch, falseBranch)
}

// Handle fake objects specially
if (expr.isFakeObject()) {
val fakeType = expr.getFakeType(scope)
Expand Down
120 changes: 87 additions & 33 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -360,51 +360,102 @@ class TsExprResolver(

override fun visit(expr: EtsTypeOfExpr): UExpr<out USort>? = with(ctx) {
val arg = resolve(expr.arg) ?: return null

if (arg.sort == fp64Sort) {
return mkStringConstant("number", scope)
}
if (arg.sort == boolSort) {
return mkStringConstant("boolean", scope)
}
if (arg.sort == addressSort) {
val ref = arg.asExpr(addressSort)
return mkIte(
condition = mkHeapRefEq(ref, mkTsNullValue()),
trueBranch = mkStringConstant("object", scope),
falseBranch = mkIte(
condition = mkHeapRefEq(ref, mkUndefinedValue()),
trueBranch = mkStringConstant("undefined", scope),
val resolvedArg = arg.asExpr(addressSort)

val processFakeFunction = { ref: UHeapRef ->
check(ref.isFakeObject())

val fakeType = scope.calcOnState { ref.getFakeType(memory) }
mkIte(
fakeType.fpTypeExpr,
mkStringConstant("number", scope),
mkIte(
fakeType.boolTypeExpr,
mkStringConstant("boolean", scope),
mkIte(
fakeType.refTypeExpr and mkHeapRefEq(ref.extractRef(scope), mkTsNullValue()),
mkStringConstant("object", scope),
mkIte(
fakeType.refTypeExpr and mkHeapRefEq(ref.extractRef(scope), mkUndefinedValue()),
mkStringConstant("undefined", scope),
mkStringConstant("object", scope) // TODO add string, function
)
)
)
)
}

val regularResolve = { ref: UHeapRef ->
mkIte(
condition = mkHeapRefEq(ref, mkTsNullValue()),
trueBranch = mkStringConstant("object", scope),
falseBranch = mkIte(
condition = scope.calcOnState {
val unwrappedRef = ref.unwrapRefWithPathConstraint(scope)

// TODO: adhoc: "expand" ITE
if (unwrappedRef is UIteExpr<*>) {
val trueBranch = unwrappedRef.trueBranch
val falseBranch = unwrappedRef.falseBranch
if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
val unwrappedTrueExpr =
trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
val unwrappedFalseExpr =
falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
return@calcOnState mkIte(
condition = unwrappedRef.condition,
trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType),
)
condition = mkHeapRefEq(ref, mkUndefinedValue()),
trueBranch = mkStringConstant("undefined", scope),
falseBranch = mkIte(
condition = scope.calcOnState {
val unwrappedRef = ref.unwrapRef(scope)

// TODO: adhoc: "expand" ITE
// TODO correst support for fake objects, including primitive branches
if (unwrappedRef is UIteExpr<*>) {
val trueBranch = unwrappedRef.trueBranch
val falseBranch = unwrappedRef.falseBranch
if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
val unwrappedTrueExpr =
trueBranch.asExpr(addressSort).unwrapRef(scope)
val unwrappedFalseExpr =
falseBranch.asExpr(addressSort).unwrapRef(scope)
return@calcOnState mkIte(
condition = unwrappedRef.condition,
trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
falseBranch = memory.types.evalTypeEquals(
unwrappedFalseExpr,
EtsStringType
),
)
}
}
}

memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
},
trueBranch = mkStringConstant("string", scope),
falseBranch = mkStringConstant("object", scope),
memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
},
trueBranch = mkStringConstant("string", scope),
falseBranch = mkStringConstant("object", scope),
)
)
)
)
}

}

if (resolvedArg.isFakeObject()) {
return processFakeFunction(resolvedArg)
}

if (resolvedArg is UIteExpr) {
val trueBranch = if (resolvedArg.trueBranch.isFakeObject()) {
processFakeFunction(resolvedArg.trueBranch)
} else {
regularResolve(resolvedArg.trueBranch)
}

val falseBranch = if (resolvedArg.falseBranch.isFakeObject()) {
processFakeFunction(resolvedArg.falseBranch)
} else {
regularResolve(resolvedArg.falseBranch)
}

return mkIte(resolvedArg.condition, trueBranch, falseBranch)
}

return regularResolve(resolvedArg)
}
logger.error { "visit(${expr::class.simpleName}) is not implemented yet" }
error("Not supported $expr")
}
Expand All @@ -419,6 +470,7 @@ class TsExprResolver(
when (val operand = expr.arg) {
is EtsInstanceFieldRef -> {
val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null
val unwrappedRef = instance.unwrapRefWithPathConstraint(scope)

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

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

Expand Down
2 changes: 2 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -845,6 +845,8 @@ class TsInterpreter(
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
}

// TODO union type
}

val model = solver.check(state.pathConstraints).ensureSat().model
Expand Down
12 changes: 12 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsLocal
import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.model.EtsScene
import org.jacodb.ets.model.EtsUnclearRefType
import org.jacodb.ets.model.EtsUnionType
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
import org.usvm.machine.TsContext
Expand Down Expand Up @@ -46,6 +47,17 @@ fun TsContext.resolveEtsField(
val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
if (field != null) return TsResolutionResult.create(field)
}

is EtsUnionType -> {
// TODO something similar to
// if (instanceType.types.all { it is EtsRefType }) {
// val fields = instanceType.types
// .map { tryGetSingleField(scene, it.typeName, field.name, hierarchy) }
// if (fields.all { it != null }) {
// return TsResolutionResult.create(fields.mapNotNull { it })
// }
// }
}
}
}

Expand Down