diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 00217256c3..1fbddb7a90 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -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 @@ -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 @@ -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") } @@ -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 } @@ -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 } @@ -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() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 1a923d6550..75356c97ac 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -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 @@ -19,6 +20,12 @@ fun TsContext.mkTruthyExpr( expr: UExpr, 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) @@ -92,6 +99,12 @@ fun TsContext.mkNumericExpr( expr: UExpr, scope: TsStepScope, ): UExpr { + 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( @@ -154,6 +167,12 @@ fun TsContext.mkNullishExpr( expr: UExpr, 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) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index ff507fcf15..ef0c9a284e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -360,7 +360,6 @@ class TsExprResolver( override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { val arg = resolve(expr.arg) ?: return null - if (arg.sort == fp64Sort) { return mkStringConstant("number", scope) } @@ -368,43 +367,95 @@ class TsExprResolver( 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") } @@ -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 @@ -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) } @@ -1205,6 +1258,7 @@ class TsExprResolver( return expr } + // TODO condition for unwrapped value fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { val ref = instance.unwrapRef(scope) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index acb1953cbe..5491734833 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index 5188459900..bc0018f012 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -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 @@ -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 }) + // } + // } + } } }