diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index f331675b5b..ca55b77f83 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "d3e97200d6" + const val jacodb = "bb51484fb4" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index adcff2dd7d..749ca6a40d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -22,12 +22,14 @@ fun mockMethodCall( result = when (sort) { is UAddressSort -> makeSymbolicRefUntyped() - is TsUnresolvedSort -> ctx.mkFakeValue( - scope, - makeSymbolicPrimitive(ctx.boolSort), - makeSymbolicPrimitive(ctx.fp64Sort), - makeSymbolicRefUntyped() - ) + is TsUnresolvedSort -> scope.calcOnState { + mkFakeValue( + scope = scope, + boolValue = makeSymbolicPrimitive(ctx.boolSort), + fpValue = makeSymbolicPrimitive(ctx.fp64Sort), + refValue = makeSymbolicRefUntyped(), + ) + } else -> makeSymbolicPrimitive(sort) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index 3c31edebaf..98549222ce 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -30,7 +30,12 @@ sealed interface TsTestValue { data object TsUnknown : TsTestValue data object TsNull : TsTestValue data object TsUndefined : TsTestValue - data object TsException : TsTestValue + + sealed interface TsException : TsTestValue { + data object UnknownException : TsException + data class StringException(val message: String) : TsException + data class ObjectException(val value: TsTestValue) : TsException + } data class TsBoolean(val value: Boolean) : TsTestValue 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..39370250cb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -8,15 +8,20 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsValue import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -111,6 +116,23 @@ class TsContext( return heapRefToStringConstant[ref] } + fun getLocalIdx(local: EtsValue, method: EtsMethod): Int? = + // Note: below, 'n' means the number of arguments + when (local) { + // Note: 'this' has index 0 + is EtsThis -> 0 + + // Note: arguments have indices from 1 to n + is EtsParameterRef -> local.index + 1 + + // Note: locals have indices starting from (n+1) + is EtsLocal -> method.locals.indexOfFirst { it.name == local.name } + .takeIf { it >= 0 } + ?.let { it + method.parameters.size + 1 } + + else -> error("Unexpected local: $local") + } + fun typeToSort(type: EtsType): USort = when (type) { is EtsBooleanType -> boolSort is EtsNumberType -> fp64Sort @@ -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..d61e9a4ad8 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 @@ -2,14 +2,19 @@ package org.usvm.machine.expr import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsStringType import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.makeSymbolicPrimitive import org.usvm.isFalse import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.types.single @@ -182,3 +187,47 @@ fun TsContext.mkNullishExpr( // Non-reference types (numbers, booleans, strings) are never nullish return mkFalse() } + +fun TsState.throwException(reason: String) { + val ref = ctx.mkStringConstantRef(reason) + methodResult = TsMethodResult.TsException(ref, EtsStringType) +} + +fun TsContext.checkUndefinedOrNullPropertyRead( + scope: TsStepScope, + instance: UHeapRef, + propertyName: String, +): Unit? { + val ref = instance.unwrapRef(scope) + val condition = mkAnd( + mkNot(mkHeapRefEq(ref, mkUndefinedValue())), + mkNot(mkHeapRefEq(ref, mkTsNullValue())), + ) + return scope.fork( + condition, + blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $ref") } + ) +} + +fun TsContext.checkNegativeIndexRead( + scope: TsStepScope, + index: UExpr, +): Unit? { + val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) + return scope.fork( + condition, + blockOnFalseState = { throwException("Negative index access: $index") } + ) +} + +fun TsContext.checkReadingInRange( + scope: TsStepScope, + index: UExpr, + length: UExpr, +): Unit? { + val condition = mkBvSignedLessExpr(index, length) + return scope.fork( + condition, + blockOnFalseState = { throwException("Index out of bounds: $index, length: $length") } + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt new file mode 100644 index 0000000000..36d8814dbd --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -0,0 +1,135 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.mkFakeValue +import org.usvm.sizeSort +import org.usvm.types.first +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +internal fun TsExprResolver.handleArrayAccess( + value: EtsArrayAccess, +): UExpr<*>? = with(ctx) { + // Resolve the array. + val array = resolve(value.array) ?: return null + check(array.sort == addressSort) { + "Expected address sort for array, got: ${array.sort}" + } + val arrayRef = array.asExpr(addressSort) + + // Check for undefined or null array access. + checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null + + // Resolve the index. + val resolvedIndex = resolve(value.index) ?: return null + check(resolvedIndex.sort == fp64Sort) { + "Expected fp64 sort for index, got: ${resolvedIndex.sort}" + } + val index = resolvedIndex.asExpr(fp64Sort) + + // Convert the index to a bit-vector. + val bvIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = index, + bvSize = sizeSort.sizeBits.toInt(), + isSigned = true, + ).asExpr(sizeSort) + + // Determine the array type. + val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) { + scope.calcOnState { memory.typeStreamOf(arrayRef).first() } + } else { + value.array.type + } + check(arrayType is EtsArrayType) { + "Expected EtsArrayType, got: ${value.array.type}" + } + + // Read the array element. + readArray(scope, arrayRef, bvIndex, arrayType) +} + +fun TsContext.readArray( + scope: TsStepScope, + array: UHeapRef, + index: UExpr, + arrayType: EtsArrayType, +): UExpr<*>? { + // Read the array length. + val length = scope.calcOnState { + val lengthLValue = mkArrayLengthLValue(array, arrayType) + memory.read(lengthLValue) + } + + // Check for out-of-bounds access. + checkNegativeIndexRead(scope, index) ?: return null + checkReadingInRange(scope, index, length) ?: return null + + // Determine the element sort. + val sort = typeToSort(arrayType.elementType) + + // If the element type is known, we can read it directly. + if (sort !is TsUnresolvedSort) { + val lValue = mkArrayIndexLValue( + sort = sort, + ref = array, + index = index, + type = arrayType, + ) + return scope.calcOnState { memory.read(lValue) } + } + + // Concrete arrays with the unresolved sort should consist of fake objects only. + if (array is UConcreteHeapRef) { + // Read a fake object from the array. + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = index, + type = arrayType, + ) + return scope.calcOnState { memory.read(lValue) } + } + + // If the element type is unresolved, we need to create a fake object + // that can hold boolean, number, and reference values. + // We read all three types from the array and combine them into a fake object. + return scope.calcOnState { + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType) + val bool = memory.read(boolLValue) + + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType) + val fp = memory.read(fpLValue) + + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType) + val ref = memory.read(refLValue) + + // If the read reference is already a fake object, we can return it directly. + // Otherwise, we need to create a new fake object and write it back to the memory. + // TODO: Think about the type constraint to get a consistent array resolution later + if (ref.isFakeObject()) { + ref + } else { + val fakeObj = mkFakeValue(scope, bool, fp, ref) + lValuesToAllocatedFakeObjects += refLValue to fakeObj + memory.write(refLValue, fakeObj, guard = trueExpr) + fakeObj + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt new file mode 100644 index 0000000000..435c7cb402 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -0,0 +1,146 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import mu.KotlinLogging +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsStaticFieldRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.ensureStaticsInitialized +import org.usvm.machine.types.EtsAuxiliaryType +import org.usvm.machine.types.mkFakeValue +import org.usvm.util.EtsHierarchy +import org.usvm.util.TsResolutionResult +import org.usvm.util.createFakeField +import org.usvm.util.mkFieldLValue +import org.usvm.util.resolveEtsField + +private val logger = KotlinLogging.logger {} + +internal fun TsExprResolver.handleInstanceFieldRef( + value: EtsInstanceFieldRef, +): UExpr<*>? = with(ctx) { + val instanceLocal = value.instance + + // Resolve the instance. + val instance = resolve(instanceLocal) ?: return null + check(instance.sort == addressSort) { + "Expected address sort for instance, got: ${instance.sort}" + } + val instanceRef = instance.asExpr(addressSort) + + // TODO: consider moving this to 'readField' + // Check for undefined or null property access. + checkUndefinedOrNullPropertyRead(scope, instanceRef, value.field.name) ?: return null + + // Handle reading "length" property for arrays. + if (value.field.name == "length" && instanceLocal.type is EtsArrayType) { + return readLengthArray(scope, instanceLocal, instanceRef) + } + + // Handle reading "length" property for fake objects. + // TODO: handle "length" property for arrays inside fake objects + if (value.field.name == "length" && instanceRef.isFakeObject()) { + return readLengthFake(scope, instanceLocal, instanceRef) + } + + // Read the field. + return readField(scope, instanceLocal, instanceRef, value.field, hierarchy) +} + +internal fun TsContext.readField( + scope: TsStepScope, + instanceLocal: EtsLocal?, + instance: UHeapRef, + field: EtsFieldSignature, + hierarchy: EtsHierarchy, +): UExpr<*> { + // Unwrap to get non-fake reference. + val unwrappedInstance = instance.unwrapRef(scope) + + val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) { + is TsResolutionResult.Empty -> { + if (field.name !in listOf("i", "LogLevel")) { + logger.warn { "Field $field not found, creating fake field" } + } + // If we didn't find any real fields, let's create a fake one. + // It is possible due to mistakes in the IR or if the field was added explicitly + // in the code. + // Probably, the right behaviour here is to fork the state. + unwrappedInstance.createFakeField(scope, field.name) + addressSort + } + + is TsResolutionResult.Unique -> typeToSort(etsField.property.type) + + is TsResolutionResult.Ambiguous -> unresolvedSort + } + + scope.doWithState { + // If we accessed some field, we make an assumption that + // this field should present in the object. + // That's not true in the common case for TS, but that's the decision we made. + val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) + // assert is required to update models + scope.assert(memory.types.evalIsSubtype(unwrappedInstance, auxiliaryType)) + } + + // If the field type is known, we can read it directly. + if (sort !is TsUnresolvedSort) { + val lValue = mkFieldLValue(sort, unwrappedInstance, field) + return scope.calcOnState { memory.read(lValue) } + } + + // If the field type is unknown, we create a fake object. + return scope.calcOnState { + val boolLValue = mkFieldLValue(boolSort, instance, field) + val fpLValue = mkFieldLValue(fp64Sort, instance, field) + val refLValue = mkFieldLValue(addressSort, instance, field) + + val bool = memory.read(boolLValue) + val fp = memory.read(fpLValue) + val ref = memory.read(refLValue) + + // If a fake object is already created and assigned to the field, + // there is no need to recreate another one. + if (ref.isFakeObject()) { + ref + } else { + val fakeObj = mkFakeValue(scope, bool, fp, ref) + lValuesToAllocatedFakeObjects += refLValue to fakeObj + memory.write(refLValue, fakeObj, guard = trueExpr) + fakeObj + } + } +} + +internal fun TsExprResolver.handleStaticFieldRef( + value: EtsStaticFieldRef, +): UExpr<*>? = with(ctx) { + return readStaticField(scope, value.field, hierarchy) +} + +internal fun TsContext.readStaticField( + scope: TsStepScope, + field: EtsFieldSignature, + hierarchy: EtsHierarchy, +): UExpr<*>? { + // TODO: handle unresolved class, or multiple classes + val clazz = scene.projectAndSdkClasses.singleOrNull { + it.signature == field.enclosingClass + } ?: return null + + // Initialize statics in `clazz` if necessary. + ensureStaticsInitialized(scope, clazz) ?: return null + + // Get the static instance. + val instance = scope.calcOnState { getStaticInstance(clazz) } + + // Read the field. + return readField(scope, null, instance, field, hierarchy) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt new file mode 100644 index 0000000000..6db88b9726 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt @@ -0,0 +1,36 @@ +package org.usvm.machine.expr + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsFile +import org.usvm.UExpr +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.ensureGlobalsInitialized +import org.usvm.util.mkFieldLValue + +private val logger = KotlinLogging.logger {} + +internal fun TsContext.readGlobal( + scope: TsStepScope, + file: EtsFile, + name: String, +): UExpr<*>? = scope.calcOnState { + // Initialize globals in `file` if necessary + ensureGlobalsInitialized(scope, file) ?: return@calcOnState null + + // Get the globals container object + val dfltObject = getDfltObject(file) + + // Restore the sort of the requested global variable + val savedSort = getSortForDfltObjectField(file, name) + if (savedSort == null) { + // No saved sort means this variable was never assigned to, which is an error to read. + logger.error { "Trying to read unassigned global variable: $name in $file" } + scope.assert(falseExpr) + return@calcOnState null + } + + // Read the global variable as a field of the globals container object + val lValue = mkFieldLValue(savedSort, dfltObject, name) + memory.read(lValue) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt new file mode 100644 index 0000000000..d407cff825 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -0,0 +1,88 @@ +package org.usvm.machine.expr + +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.sizeSort +import org.usvm.util.mkArrayLengthLValue + +// Handles reading the `length` property of an array. +internal fun TsContext.readLengthArray( + scope: TsStepScope, + instanceLocal: EtsLocal, + instance: UHeapRef, // array +): UExpr<*> { + // Assume that instance is always an array. + val arrayType = instanceLocal.type as EtsArrayType + + // Read the length of the array. + return readArrayLength(scope, instance, arrayType) +} + +// Handles reading the `length` property of a fake object. +internal fun TsContext.readLengthFake( + scope: TsStepScope, + instanceLocal: EtsLocal, + instance: UHeapRef, // fake object +): UExpr<*> { + require(instance.isFakeObject()) + + // If we want to get length from a fake object, + // we assume that it is an array (has address sort). + scope.doWithState { + val fakeType = instance.getFakeType(scope) + pathConstraints += fakeType.refTypeExpr + } + + // Unwrap to get non-fake reference. + val unwrappedInstance = instance.unwrapRef(scope) + + // Determine the array type. + val arrayType = when (val type = instanceLocal.type) { + is EtsArrayType -> type + + is EtsAnyType, is EtsUnknownType -> { + // If the type is not an array, we assume it is a fake object with + // a length property that behaves like an array. + EtsArrayType(EtsUnknownType, dimensions = 1) + } + + else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") + } + + // Read the length of the array. + return readArrayLength(scope, unwrappedInstance, arrayType) +} + +// Reads the length of the array and returns it as a fp64 expression. +internal fun TsContext.readArrayLength( + scope: TsStepScope, + array: UHeapRef, + arrayType: EtsArrayType, +): UExpr { + // Read the length of the array. + val length = scope.calcOnState { + val lengthLValue = mkArrayLengthLValue(array, arrayType) + memory.read(lengthLValue) + } + + // Ensure that the length is non-negative. + scope.doWithState { + pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + } + + // Convert the length to fp64. + return mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.asExpr(sizeSort), + signed = true, + ) +} 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..bfea1c8634 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 @@ -1,12 +1,10 @@ package org.usvm.machine.expr -import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import io.ksmt.utils.cast import mu.KotlinLogging import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAndExpr -import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsAwaitExpr @@ -16,7 +14,6 @@ import org.jacodb.ets.model.EtsBitNotExpr import org.jacodb.ets.model.EtsBitOrExpr import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant -import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsCaughtExceptionRef import org.jacodb.ets.model.EtsClassSignature @@ -28,7 +25,6 @@ import org.jacodb.ets.model.EtsDivExpr import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsEqExpr import org.jacodb.ets.model.EtsExpExpr -import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGlobalRef import org.jacodb.ets.model.EtsGtEqExpr @@ -53,7 +49,6 @@ import org.jacodb.ets.model.EtsNotExpr import org.jacodb.ets.model.EtsNullConstant import org.jacodb.ets.model.EtsNullishCoalescingExpr import org.jacodb.ets.model.EtsNumberConstant -import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsOrExpr import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsPostDecExpr @@ -61,7 +56,6 @@ import org.jacodb.ets.model.EtsPostIncExpr import org.jacodb.ets.model.EtsPreDecExpr import org.jacodb.ets.model.EtsPreIncExpr import org.jacodb.ets.model.EtsPtrCallExpr -import org.jacodb.ets.model.EtsRawType import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsRemExpr import org.jacodb.ets.model.EtsRightShiftExpr @@ -73,7 +67,6 @@ import org.jacodb.ets.model.EtsStringConstant import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsSubExpr import org.jacodb.ets.model.EtsThis -import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsTypeOfExpr import org.jacodb.ets.model.EtsUnaryExpr import org.jacodb.ets.model.EtsUnaryPlusExpr @@ -84,15 +77,11 @@ import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidExpr import org.jacodb.ets.model.EtsYieldExpr import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX -import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.jacodb.ets.utils.getDeclaredLocals -import org.usvm.UAddressSort import org.usvm.UBoolExpr -import org.usvm.UBoolSort -import org.usvm.UConcreteHeapRef import org.usvm.UExpr -import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef @@ -100,21 +89,18 @@ import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.mockMethodCall -import org.usvm.api.typeStreamOf import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.Constants import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext -import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.getGlobals import org.usvm.machine.interpreter.getResolvedValue -import org.usvm.machine.interpreter.isInitialized import org.usvm.machine.interpreter.isResolved -import org.usvm.machine.interpreter.markInitialized import org.usvm.machine.interpreter.markResolved import org.usvm.machine.interpreter.setResolvedValue import org.usvm.machine.operator.TsBinaryOperator @@ -124,22 +110,16 @@ import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt -import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.machine.types.iteWriteIntoFakeObject -import org.usvm.machine.types.mkFakeValue import org.usvm.sizeSort -import org.usvm.types.first import org.usvm.util.EtsHierarchy +import org.usvm.util.SymbolResolutionResult import org.usvm.util.TsResolutionResult -import org.usvm.util.createFakeField import org.usvm.util.isResolved -import org.usvm.util.mkArrayIndexLValue -import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.resolveEtsField import org.usvm.util.resolveEtsMethods -import org.usvm.util.throwExceptionWithoutStackFrameDrop +import org.usvm.util.resolveImportInfo private val logger = KotlinLogging.logger {} @@ -161,12 +141,11 @@ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111 class TsExprResolver( internal val ctx: TsContext, internal val scope: TsStepScope, - private val localToIdx: (EtsMethod, EtsValue) -> Int?, - private val hierarchy: EtsHierarchy, + internal val hierarchy: EtsHierarchy, ) : EtsEntity.Visitor?> { val simpleValueResolver: TsSimpleValueResolver = - TsSimpleValueResolver(ctx, scope, localToIdx) + TsSimpleValueResolver(ctx, scope) fun resolve(expr: EtsEntity): UExpr? { return expr.accept(this) @@ -217,15 +196,15 @@ class TsExprResolver( // region SIMPLE VALUE - override fun visit(value: EtsLocal): UExpr { + override fun visit(value: EtsLocal): UExpr? { return simpleValueResolver.visit(value) } - override fun visit(value: EtsParameterRef): UExpr { + override fun visit(value: EtsParameterRef): UExpr? { return simpleValueResolver.visit(value) } - override fun visit(value: EtsThis): UExpr { + override fun visit(value: EtsThis): UExpr? { return simpleValueResolver.visit(value) } @@ -421,7 +400,7 @@ class TsExprResolver( val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null // Check for null/undefined access - checkUndefinedOrNullPropertyRead(instance) ?: return null + checkUndefinedOrNullPropertyRead(scope, instance, operand.field.name) ?: return null // For now, we simulate deletion by setting the property to undefined // This is a simplification of the real semantics but sufficient for basic cases @@ -847,7 +826,7 @@ class TsExprResolver( val obj = resolve(expr.right)?.asExpr(addressSort) ?: return null // Check for null/undefined access - checkUndefinedOrNullPropertyRead(obj) ?: return null + checkUndefinedOrNullPropertyRead(scope, obj, propertyName = "") ?: return null logger.warn { "The 'in' operator is supported yet, the result may not be accurate" @@ -902,7 +881,7 @@ class TsExprResolver( resolved.asExpr(addressSort) } - checkUndefinedOrNullPropertyRead(instance) ?: return null + checkUndefinedOrNullPropertyRead(scope, instance, expr.callee.name) ?: return null val resolvedArgs = expr.args.map { resolve(it) ?: return null } @@ -1123,333 +1102,11 @@ class TsExprResolver( // region ACCESS - override fun visit(value: EtsArrayAccess): UExpr? = with(ctx) { - val array = resolve(value.array)?.asExpr(addressSort) ?: return null - - checkUndefinedOrNullPropertyRead(array) ?: return null - - val index = resolve(value.index)?.asExpr(fp64Sort) ?: return null - val bvIndex = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = index, - bvSize = sizeSort.sizeBits.toInt(), - isSigned = true, - ).asExpr(sizeSort) - - val arrayType = if (isAllocatedConcreteHeapRef(array)) { - scope.calcOnState { memory.typeStreamOf(array).first() } - } else { - value.array.type - } as? EtsArrayType ?: error("Expected EtsArrayType, got: ${value.array.type}") - val sort = typeToSort(arrayType.elementType) - - val lengthLValue = mkArrayLengthLValue(array, arrayType) - val length = scope.calcOnState { memory.read(lengthLValue) } - - checkNegativeIndexRead(bvIndex) ?: return null - checkReadingInRange(bvIndex, length) ?: return null - - val expr = if (sort is TsUnresolvedSort) { - // Concrete arrays with the unresolved sort should consist of fake objects only. - if (array is UConcreteHeapRef) { - // Read a fake object from the array. - val lValue = mkArrayIndexLValue( - sort = addressSort, - ref = array, - index = bvIndex, - type = arrayType - ) - - scope.calcOnState { memory.read(lValue) } - } else { - // If the array is not concrete, we need to allocate a fake object - val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) - val boolLValue = mkArrayIndexLValue(boolSort, array, bvIndex, boolArrayType) - - val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) - val fpLValue = mkArrayIndexLValue(fp64Sort, array, bvIndex, numberArrayType) - - val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) - val refLValue = mkArrayIndexLValue(addressSort, array, bvIndex, unknownArrayType) - - scope.calcOnState { - val boolValue = memory.read(boolLValue) - val fpValue = memory.read(fpLValue) - val refValue = memory.read(refLValue) - - // Read an object from the memory at first, - // we don't need to recreate it if it is already a fake object. - val fakeObj = if (refValue.isFakeObject()) { - refValue - } else { - mkFakeValue(scope, boolValue, fpValue, refValue).also { - lValuesToAllocatedFakeObjects += refLValue to it - } - } - - memory.write(refLValue, fakeObj.asExpr(addressSort), guard = trueExpr) - - fakeObj - } - } - } else { - val lValue = mkArrayIndexLValue( - sort = sort, - ref = array, - index = bvIndex, - type = arrayType - ) - scope.calcOnState { memory.read(lValue) } - } - - return expr - } - - fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) { - val ref = instance.unwrapRef(scope) - - val neqNull = mkAnd( - mkHeapRefEq(ref, mkUndefinedValue()).not(), - mkHeapRefEq(ref, mkTsNullValue()).not(), - ) - - scope.fork( - neqNull, - blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type - ) - } - - fun checkNegativeIndexRead(index: UExpr) = with(ctx) { - val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) - - scope.fork( - condition, - blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type - ) - } - - fun checkReadingInRange(index: UExpr, length: UExpr) = with(ctx) { - val condition = mkBvSignedLessExpr(index, length) - - scope.fork( - condition, - blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type - ) - } - - private fun allocateException(type: EtsType): (TsState) -> Unit = { state -> - val address = state.memory.allocConcrete(type) - state.throwExceptionWithoutStackFrameDrop(address, type) - } - - private fun handleFieldRef( - instance: EtsLocal?, - instanceRef: UHeapRef, - field: EtsFieldSignature, - hierarchy: EtsHierarchy, - ): UExpr? = with(ctx) { - val resolvedAddr = instanceRef.unwrapRef(scope) - - val etsField = resolveEtsField(instance, field, hierarchy) - - val sort = when (etsField) { - is TsResolutionResult.Empty -> { - if (field.name !in listOf("i", "LogLevel")) { - logger.warn { "Field $field not found, creating fake field" } - } - // If we didn't find any real fields, let's create a fake one. - // It is possible due to mistakes in the IR or if the field was added explicitly - // in the code. - // Probably, the right behaviour here is to fork the state. - resolvedAddr.createFakeField(field.name, scope) - addressSort - } - - is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> unresolvedSort - } - - scope.doWithState { - // If we accessed some field, we make an assumption that - // this field should present in the object. - // That's not true in the common case for TS, but that's the decision we made. - val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) - // assert is required to update models - scope.assert(memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)) - } - - if (sort == unresolvedSort) { - val boolLValue = mkFieldLValue(boolSort, instanceRef, field) - val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field) - val refLValue = mkFieldLValue(addressSort, instanceRef, field) - - scope.calcOnState { - val bool = memory.read(boolLValue) - val fp = memory.read(fpLValue) - val ref = memory.read(refLValue) - - // If a fake object is already created and assigned to the field, - // there is no need to recreate another one - val fakeRef = if (ref.isFakeObject()) { - ref - } else { - mkFakeValue(scope, bool, fp, ref).also { - lValuesToAllocatedFakeObjects += refLValue to it - } - } - - // TODO ambiguous enum fields resolution - if (etsField is TsResolutionResult.Unique) { - val fieldType = etsField.property.type - if (fieldType is EtsRawType && fieldType.kind == "EnumValueType") { - val fakeType = fakeRef.getFakeType(scope) - pathConstraints += ctx.mkOr( - fakeType.fpTypeExpr, - fakeType.refTypeExpr - ) - - // val supertype = TODO() - // TODO add enum type as a constraint - // pathConstraints += memory.types.evalIsSubtype( - // ref, - // TODO() - // ) - } - } - - memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr) - - fakeRef - } - } else { - val lValue = mkFieldLValue(sort, resolvedAddr, field) - scope.calcOnState { memory.read(lValue) } - } - } - - private fun handleArrayLength( - value: EtsInstanceFieldRef, - instance: UHeapRef, - ): UExpr<*> = with(ctx) { - val arrayType = value.instance.type as EtsArrayType - val length = scope.calcOnState { - val lengthLValue = mkArrayLengthLValue(instance, arrayType) - memory.read(lengthLValue) - } - - scope.doWithState { - pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - } - - return mkBvToFpExpr( - fp64Sort, - fpRoundingModeSortDefaultValue(), - length.asExpr(sizeSort), - signed = true, - ) - } - - private fun handleFakeLength( - value: EtsInstanceFieldRef, - instance: UConcreteHeapRef, - ): UExpr<*> = with(ctx) { - val fakeType = instance.getFakeType(scope) - - // If we want to get length from a fake object, we assume that it is an array. - scope.doWithState { - pathConstraints += fakeType.refTypeExpr - } - - val ref = instance.unwrapRef(scope) - - val arrayType = when (val type = value.instance.type) { - is EtsArrayType -> type - - is EtsAnyType, is EtsUnknownType -> { - // If the type is not an array, we assume it is a fake object with - // a length property that behaves like an array. - EtsArrayType(EtsUnknownType, dimensions = 1) - } + override fun visit(value: EtsArrayAccess): UExpr<*>? = handleArrayAccess(value) - else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type") - } - val length = scope.calcOnState { - val lengthLValue = mkArrayLengthLValue(ref, arrayType) - memory.read(lengthLValue) - } + override fun visit(value: EtsInstanceFieldRef): UExpr<*>? = handleInstanceFieldRef(value) - scope.doWithState { - pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - } - - return mkBvToFpExpr( - fp64Sort, - fpRoundingModeSortDefaultValue(), - length.asExpr(sizeSort), - signed = true - ) - } - - override fun visit(value: EtsInstanceFieldRef): UExpr? = with(ctx) { - val instanceResolved = resolve(value.instance) ?: return null - if (instanceResolved.sort != addressSort) { - logger.error { "Instance of field ref should be a reference, but got $instanceResolved" } - scope.assert(falseExpr) - return null - } - val instanceRef = instanceResolved.asExpr(addressSort) - - checkUndefinedOrNullPropertyRead(instanceRef) ?: return null - - // Handle array length - if (value.field.name == "length" && value.instance.type is EtsArrayType) { - return handleArrayLength(value, instanceRef) - } - - // Handle length property for fake objects - // TODO: handle "length" property for arrays inside fake objects - if (value.field.name == "length" && instanceRef.isFakeObject()) { - return handleFakeLength(value, instanceRef) - } - - return handleFieldRef(value.instance, instanceRef, value.field, hierarchy) - } - - override fun visit(value: EtsStaticFieldRef): UExpr? = with(ctx) { - val clazz = scene.projectAndSdkClasses.singleOrNull { - it.signature == value.field.enclosingClass - } ?: return null - - val instanceRef = scope.calcOnState { getStaticInstance(clazz) } - - val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME } - if (initializer != null) { - val isInitialized = scope.calcOnState { isInitialized(clazz) } - if (isInitialized) { - scope.doWithState { - // TODO: Handle static initializer result - val result = methodResult - // TODO: Why this signature check is needed? - // TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere. - if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) { - methodResult = TsMethodResult.NoCall - } - } - } else { - scope.doWithState { - markInitialized(clazz) - pushSortsForArguments(instance = null, args = emptyList(), localToIdx) - registerCallee(currentStatement, initializer.cfg) - callStack.push(initializer, currentStatement) - memory.stack.push(arrayOf(instanceRef), initializer.localsCount) - newStmt(initializer.cfg.stmts.first()) - } - return null - } - } - - return handleFieldRef(instance = null, instanceRef, value.field, hierarchy) - } + override fun visit(value: EtsStaticFieldRef): UExpr<*>? = handleStaticFieldRef(value) override fun visit(value: EtsCaughtExceptionRef): UExpr? { logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } @@ -1530,18 +1187,23 @@ class TsExprResolver( val condition = mkAnd( mkEq( - mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), bvSize, signed = true), + mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = bvSize, + signed = true, + ), size.asExpr(fp64Sort) ), mkAnd( - mkBvSignedLessOrEqualExpr(0.toBv(), bvSize.asExpr(bv32Sort)), - mkBvSignedLessOrEqualExpr(bvSize, Int.MAX_VALUE.toBv().asExpr(bv32Sort)) + mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)), + mkBvSignedLessOrEqualExpr(bvSize.asExpr(bv32Sort), mkBv(Int.MAX_VALUE)) ) ) scope.fork( condition, - blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type + blockOnFalseState = { throwException("Invalid array size: ${size.asExpr(fp64Sort)}") } ) if (arrayType.elementType is EtsArrayType) { @@ -1561,124 +1223,119 @@ class TsExprResolver( class TsSimpleValueResolver( private val ctx: TsContext, private val scope: TsStepScope, - private val localToIdx: (EtsMethod, EtsValue) -> Int?, ) : EtsValue.Visitor?> { - private fun resolveLocal(local: EtsValue): UExpr<*> = with(ctx) { - val currentMethod = scope.calcOnState { lastEnteredMethod } - val entrypoint = scope.calcOnState { entrypoint } - - val localIdx = localToIdx(currentMethod, local) - - // If there is no local variable corresponding to the local, - // we treat it as a field of some global object with the corresponding name. - // It helps us to support global variables that are missed in the IR. - if (localIdx == null) { - require(local is EtsLocal) + private fun resolveLocal(local: EtsValue): UExpr<*>? = with(ctx) { + check(local is EtsLocal || local is EtsThis || local is EtsParameterRef) { + "Expected EtsLocal, EtsThis, or EtsParameterRef, but got ${local::class.java}: $local" + } - // Handle closures - if (local.name.startsWith("%closures")) { - val existingClosures = scope.calcOnState { closureObject[local.name] } - if (existingClosures != null) { - return existingClosures - } - val type = local.type - check(type is EtsLexicalEnvType) - val obj = allocateConcreteRef() - for (captured in type.closures) { - val resolvedCaptured = resolveLocal(captured) - val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name) - scope.doWithState { - memory.write(lValue, resolvedCaptured.cast(), guard = ctx.trueExpr) - } - } + // Handle closures + if (local is EtsLocal && local.name.startsWith("%closures")) { + // TODO: add comments + val existingClosures = scope.calcOnState { closureObject[local.name] } + if (existingClosures != null) { + return existingClosures + } + val type = local.type + check(type is EtsLexicalEnvType) + val obj = allocateConcreteRef() + // TODO: consider 'types.allocate' + for (captured in type.closures) { + val resolvedCaptured = resolveLocal(captured) ?: return null + val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name) scope.doWithState { - setClosureObject(local.name, obj) + memory.write(lValue, resolvedCaptured.cast(), guard = trueExpr) } - return obj } - - val globalObject = scope.calcOnState { globalObject } - - val localName = local.name - // Check whether this local was already created or not - if (localName in scope.calcOnState { addedArtificialLocals }) { - val sort = ctx.typeToSort(local.type) - val lValue = if (sort is TsUnresolvedSort) { - mkFieldLValue(ctx.addressSort, globalObject, local.name) - } else { - mkFieldLValue(sort, globalObject, local.name) - } - return scope.calcOnState { memory.read(lValue) } + scope.doWithState { + setClosureObject(local.name, obj) } + return obj + } - logger.warn { "Cannot resolve local $local, creating a field of the global object" } + val currentMethod = scope.calcOnState { lastEnteredMethod } - scope.doWithState { - addedArtificialLocals += localName + // Locals in %dflt method are a little bit *special*... + if (currentMethod.name == DEFAULT_ARK_METHOD_NAME) { + val file = currentMethod.enclosingClass!!.declaringFile!! + if (local is EtsLocal) { + val name = local.name + if (!name.startsWith("%") && !name.startsWith("_tmp") && name != "this") { + logger.info { + "Reading global variable in %dflt: $local in $file" + } + return readGlobal(scope, file, name) + } } + } - val sort = ctx.typeToSort(local.type) - val lValue = if (sort is TsUnresolvedSort) { - globalObject.createFakeField(localName, scope) - mkFieldLValue(ctx.addressSort, globalObject, local.name) - } else { - mkFieldLValue(sort, globalObject, local.name) + // Get local index + val idx = getLocalIdx(local, currentMethod) + + // If local is found in the current method: + if (idx != null) { + return scope.calcOnState { + val sort = getOrPutSortForLocal(idx) { + val type = local.tryGetKnownType(currentMethod) + typeToSort(type).let { + if (it is TsUnresolvedSort) { + addressSort + } else { + it + } + } + } + val lValue = mkRegisterStackLValue(sort, idx) + memory.read(lValue) } - return scope.calcOnState { memory.read(lValue) } } - val sort = scope.calcOnState { - val type = local.tryGetKnownType(currentMethod) - getOrPutSortForLocal(localIdx, type) - } + // Local not found, either global or imported + val file = currentMethod.enclosingClass!!.declaringFile!! + val globals = file.getGlobals() - // If we are not in the entrypoint, all correct values are already resolved and we can just return - // a registerStackLValue for the local - if (currentMethod != entrypoint) { - val lValue = mkRegisterStackLValue(sort, localIdx) - return scope.calcOnState { memory.read(lValue) } + require(local is EtsLocal) { + "Only locals are supported here, but got ${local::class.java}: $local" } - // arguments and this for the first stack frame - when (sort) { - is UBoolSort -> { - val lValue = mkRegisterStackLValue(sort, localIdx) - scope.calcOnState { memory.read(lValue) } - } - - is KFp64Sort -> { - val lValue = mkRegisterStackLValue(sort, localIdx) - scope.calcOnState { memory.read(lValue) } - } - - is UAddressSort -> { - val lValue = mkRegisterStackLValue(sort, localIdx) - scope.calcOnState { memory.read(lValue) } - } + // If local is a global variable: + if (globals.any { it.name == local.name }) { + logger.info { "Reading global variable: $local in $file" } + return readGlobal(scope, file, local.name) + } - is TsUnresolvedSort -> { - check(local is EtsThis || local is EtsParameterRef) { - "Only This and ParameterRef are expected here" + // If local is an imported variable: + val importInfo = file.importInfos.find { it.name == local.name } + if (importInfo != null) { + when (val resolutionResult = scene.resolveImportInfo(file, importInfo)) { + is SymbolResolutionResult.Success -> { + val importedFile = resolutionResult.file + val importedName = resolutionResult.exportInfo.originalName + logger.info { "Reading imported variable: $importedName from $importedFile" } + return readGlobal(scope, importedFile, importedName) } - val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort) - val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort) - val refRValue = ctx.mkRegisterReading(localIdx, ctx.addressSort) + is SymbolResolutionResult.FileNotFound -> { + logger.error { "Cannot resolve import for '$local': ${resolutionResult.reason}" } + scope.assert(falseExpr) + return null + } - val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue) - val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx) - scope.calcOnState { - memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr) + is SymbolResolutionResult.SymbolNotFound -> { + logger.error { "Cannot find symbol '$local' in '${resolutionResult.file.name}': ${resolutionResult.reason}" } + scope.assert(falseExpr) + return null } - fakeObject } - - else -> error("Unsupported sort $sort") } + + logger.error { "Cannot resolve local variable '$local' in method: $currentMethod" } + scope.assert(falseExpr) + return null } - override fun visit(local: EtsLocal): UExpr { + override fun visit(local: EtsLocal): UExpr? { if (local.name == "NaN") { return ctx.mkFp64NaN() } @@ -1710,11 +1367,11 @@ class TsSimpleValueResolver( return resolveLocal(local) } - override fun visit(value: EtsParameterRef): UExpr { + override fun visit(value: EtsParameterRef): UExpr? { return resolveLocal(value) } - override fun visit(value: EtsThis): UExpr { + override fun visit(value: EtsThis): UExpr? { return resolveLocal(value) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt new file mode 100644 index 0000000000..60790925f1 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -0,0 +1,110 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsArrayType +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.sizeSort +import org.usvm.types.first +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +internal fun TsExprResolver.handleAssignToArrayIndex( + lhv: EtsArrayAccess, + expr: UExpr<*>, +): Unit? = with(ctx) { + // Resolve the array. + val resolvedArray = resolve(lhv.array) ?: return null + check(resolvedArray.sort == addressSort) { + "Expected address sort for array, got: ${resolvedArray.sort}" + } + val array = resolvedArray.asExpr(addressSort) + + // Check for undefined or null array access. + checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null + + // Resolve the index. + val resolvedIndex = resolve(lhv.index) ?: return null + check(resolvedIndex.sort == fp64Sort) { + "Expected fp64 sort for index, got: ${resolvedIndex.sort}" + } + val index = resolvedIndex.asExpr(fp64Sort) + + // Convert the index to a bit-vector. + val bvIndex = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = index, + bvSize = 32, + isSigned = true, + ).asExpr(sizeSort) + + // Determine the array type. + // TODO: handle the case when `lhv.array.type` is NOT an array. + // In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`. + val arrayType = if (isAllocatedConcreteHeapRef(array)) { + scope.calcOnState { memory.typeStreamOf(array).first() } + } else { + lhv.array.type + } + check(arrayType is EtsArrayType) { + "Expected EtsArrayType, got: ${lhv.array.type}" + } + + return assignToArrayIndex(scope, array, bvIndex, expr, arrayType) +} + +internal fun TsContext.assignToArrayIndex( + scope: TsStepScope, + array: UHeapRef, + index: UExpr, + expr: UExpr<*>, + arrayType: EtsArrayType, +): Unit? { + // Read the array length. + val length = scope.calcOnState { + val lengthLValue = mkArrayLengthLValue(array, arrayType) + memory.read(lengthLValue) + } + + // Note: out-of-bound write is not an error in JS, since it can grow the array. + // However, we decided to forbid this behavior in our model for simplicity. + // Instead, we only allow writing to existing indices. + + // Check for out-of-bounds access. + checkNegativeIndexRead(scope, index) ?: return null + checkReadingInRange(scope, index, length) ?: return null + + val elementSort = typeToSort(arrayType.elementType) + + // If the element sort is known, write directly. + if (elementSort !is TsUnresolvedSort) { + val lValue = mkArrayIndexLValue( + sort = elementSort, + ref = array, + index = index.asExpr(sizeSort), + type = arrayType, + ) + return scope.doWithState { + memory.write(lValue, expr.asExpr(elementSort), guard = trueExpr) + } + } + + // If the element sort is unknown, we need to employ a fake object. + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = index.asExpr(sizeSort), + type = arrayType, + ) + val fakeExpr = expr.toFakeObject(scope) + return scope.doWithState { + lValuesToAllocatedFakeObjects += lValue to fakeExpr + memory.write(lValue, fakeExpr, guard = trueExpr) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt new file mode 100644 index 0000000000..dd15548291 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -0,0 +1,152 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStaticFieldRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.EtsAuxiliaryType +import org.usvm.util.EtsHierarchy +import org.usvm.util.TsResolutionResult +import org.usvm.util.mkFieldLValue +import org.usvm.util.resolveEtsField + +internal fun TsExprResolver.handleAssignToInstanceField( + lhv: EtsInstanceFieldRef, + expr: UExpr<*>, +): Unit? = with(ctx) { + val instanceLocal = lhv.instance + val field = lhv.field + + // Resolve the instance. + val instance = resolve(instanceLocal) ?: return null + check(instance.sort == addressSort) { + "Expected address sort for instance, got: ${instance.sort}" + } + val instanceRef = instance.asExpr(addressSort) + + // Check for undefined or null field access. + checkUndefinedOrNullPropertyRead(scope, instanceRef, field.name) ?: return null + + // Assign to the field. + assignToInstanceField(scope, instanceLocal, instanceRef, field, expr, hierarchy) +} + +internal fun TsContext.assignToInstanceField( + scope: TsStepScope, + instanceLocal: EtsLocal, + instance: UHeapRef, + field: EtsFieldSignature, + expr: UExpr<*>, + hierarchy: EtsHierarchy, +) { + // Unwrap to get non-fake reference. + val unwrappedInstance = instance.unwrapRef(scope) + + val etsField = resolveEtsField(instanceLocal, field, hierarchy) + // If we access some field, we expect that the object must have this field. + // It is not always true for TS, but we decided to process it so. + val supertype = EtsAuxiliaryType(properties = setOf(field.name)) + // assert is required to update models + scope.doWithState { + scope.assert(memory.types.evalIsSubtype(unwrappedInstance, supertype)) + } + + // Determine the field sort. + val sort = when (etsField) { + is TsResolutionResult.Empty -> unresolvedSort + is TsResolutionResult.Unique -> typeToSort(etsField.property.type) + is TsResolutionResult.Ambiguous -> unresolvedSort + } + + // If the field type is unknown, we create a fake object for the expr and assign it. + // Otherwise, assign expr directly. + scope.doWithState { + if (sort is TsUnresolvedSort) { + val fakeObject = expr.toFakeObject(scope) + val lValue = mkFieldLValue(addressSort, unwrappedInstance, field) + lValuesToAllocatedFakeObjects += lValue to fakeObject + memory.write(lValue, fakeObject, guard = trueExpr) + } else { + val lValue = mkFieldLValue(sort, unwrappedInstance, field) + if (lValue.sort != expr.sort) { + if (expr.isFakeObject()) { + val lhvType = instanceLocal.type + val value = when (lhvType) { + is EtsBooleanType -> { + pathConstraints += expr.getFakeType(scope).boolTypeExpr + expr.extractBool(scope) + } + + is EtsNumberType -> { + pathConstraints += expr.getFakeType(scope).fpTypeExpr + expr.extractFp(scope) + } + + else -> { + pathConstraints += expr.getFakeType(scope).refTypeExpr + expr.extractRef(scope) + } + } + memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) + } else { + TODO("Support enums fields") + } + } else { + memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) + } + } + } +} + +internal fun TsExprResolver.handleAssignToStaticField( + lhv: EtsStaticFieldRef, + expr: UExpr<*>, +): Unit? = with(ctx) { + assignToStaticField(scope, lhv.field, expr) +} + +internal fun TsContext.assignToStaticField( + scope: TsStepScope, + field: EtsFieldSignature, + expr: UExpr<*>, +): Unit? { + val clazz = scene.projectAndSdkClasses.singleOrNull { + it.signature == field.enclosingClass + } ?: return null + + val instance = scope.calcOnState { getStaticInstance(clazz) } + + // TODO: initialize the static field first + // Note: Since we are assigning to a static field, we can omit its initialization, + // if it does not have any side effects. + + val sort = run { + val fields = clazz.fields.filter { it.name == field.name } + if (fields.size == 1) { + val field = fields.single() + val sort = typeToSort(field.type) + return@run sort + } + unresolvedSort + } + return if (sort == unresolvedSort) { + val lValue = mkFieldLValue(addressSort, instance, field.name) + val fakeObject = expr.toFakeObject(scope) + scope.doWithState { + lValuesToAllocatedFakeObjects += lValue to fakeObject + memory.write(lValue, fakeObject, guard = trueExpr) + } + } else { + val lValue = mkFieldLValue(sort, instance, field.name) + scope.doWithState { + memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt new file mode 100644 index 0000000000..327c9eba73 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteGlobal.kt @@ -0,0 +1,29 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsFile +import org.usvm.UExpr +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.interpreter.ensureGlobalsInitialized +import org.usvm.util.mkFieldLValue + +internal fun TsContext.writeGlobal( + scope: TsStepScope, + file: EtsFile, + name: String, + expr: UExpr<*>, +): Unit? = scope.calcOnState { + // Initialize globals in `file` if necessary + ensureGlobalsInitialized(scope, file) ?: return@calcOnState null + + // Get the globals container object + val dfltObject = getDfltObject(file) + + // Write the global variable as a field of the globals container object + val lValue = mkFieldLValue(expr.sort, dfltObject, name) + memory.write(lValue, expr.cast(), guard = trueExpr) + + // Save the sort of the global variable for future reads + saveSortForDfltObjectField(file, name, expr.sort) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt new file mode 100644 index 0000000000..f5802e7735 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteLocal.kt @@ -0,0 +1,44 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.cast +import mu.KotlinLogging +import org.jacodb.ets.model.EtsLocal +import org.usvm.UExpr +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.util.mkRegisterStackLValue + +private val logger = KotlinLogging.logger {} + +internal fun TsExprResolver.handleAssignToLocal( + local: EtsLocal, + expr: UExpr<*>, +): Unit? = with(ctx) { + return assignToLocal(scope, local, expr) +} + +internal fun TsContext.assignToLocal( + scope: TsStepScope, + local: EtsLocal, + expr: UExpr<*>, +): Unit? { + val currentMethod = scope.calcOnState { lastEnteredMethod } + + val idx = getLocalIdx(local, currentMethod) + + // If local is found in the current method: + if (idx != null) { + return scope.doWithState { + saveSortForLocal(idx, expr.sort) + val lValue = mkRegisterStackLValue(expr.sort, idx) + memory.write(lValue, expr.cast(), guard = trueExpr) + } + } + + // Local not found, probably a global + val file = currentMethod.enclosingClass!!.declaringFile!! + logger.warn { + "Assigning to a global variable: ${local.name} in $file" + } + return writeGlobal(scope, file, local.name, expr) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsGlobals.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsGlobals.kt new file mode 100644 index 0000000000..5c2e3f6a4e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsGlobals.kt @@ -0,0 +1,89 @@ +package org.usvm.machine.interpreter + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME +import org.usvm.UBoolSort +import org.usvm.UHeapRef +import org.usvm.collection.field.UFieldLValue +import org.usvm.isTrue +import org.usvm.machine.TsContext +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.state.localsCount +import org.usvm.machine.state.newStmt +import org.usvm.util.mkFieldLValue + +private val logger = KotlinLogging.logger {} + +fun EtsFile.getDfltClass(): EtsClass { + return classes.first { it.name == DEFAULT_ARK_CLASS_NAME } +} + +fun EtsClass.getDfltMethod(): EtsMethod { + return methods.first { it.name == DEFAULT_ARK_METHOD_NAME } +} + +fun EtsFile.getDfltMethod(): EtsMethod { + val dfltClass = getDfltClass() + return dfltClass.getDfltMethod() +} + +fun EtsFile.getGlobals(): List { + val dfltMethod = getDfltMethod() + return dfltMethod.cfg.stmts + .filterIsInstance() + .mapNotNull { it.lhv as? EtsLocal } + .distinct() +} + +private fun TsContext.mkGlobalsInitializedFlag( + instance: UHeapRef, +): UFieldLValue { + return mkFieldLValue(boolSort, instance, "__initialized__") +} + +internal fun TsState.isGlobalsInitialized(file: EtsFile): Boolean { + val instance = getDfltObject(file) + val initializedFlag = ctx.mkGlobalsInitializedFlag(instance) + return memory.read(initializedFlag).isTrue +} + +internal fun TsState.markGlobalsInitialized(file: EtsFile) { + val instance = getDfltObject(file) + val initializedFlag = ctx.mkGlobalsInitializedFlag(instance) + memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr) +} + +internal fun TsState.initializeGlobals(file: EtsFile) { + markGlobalsInitialized(file) + val dfltObject = getDfltObject(file) + val dfltMethod = file.getDfltMethod() + pushSortsForArguments(0) { null } + registerCallee(currentStatement, dfltMethod.cfg) + callStack.push(dfltMethod, currentStatement) + memory.stack.push(arrayOf(dfltObject), dfltMethod.localsCount) + newStmt(dfltMethod.cfg.stmts.first()) +} + +internal fun TsContext.ensureGlobalsInitialized( + scope: TsStepScope, + file: EtsFile, +): Unit? = scope.calcOnState { + // Initialize globals in `file` if necessary + if (!isGlobalsInitialized(file)) { + logger.info { "Globals are not initialized for file: $file" } + initializeGlobals(file) + return@calcOnState null + } + + // TODO: handle methodResult + if (methodResult is TsMethodResult.Success) { + methodResult = TsMethodResult.NoCall + } +} 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..b509c82d3e 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 @@ -1,6 +1,7 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr +import io.ksmt.utils.cast import mu.KotlinLogging import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess @@ -11,27 +12,26 @@ import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLValue import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType -import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStringType -import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsThrowStmt import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType -import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.callExpr -import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr @@ -53,7 +53,13 @@ import org.usvm.machine.TsOptions import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.expr.TsExprResolver import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.handleAssignToArrayIndex +import org.usvm.machine.expr.handleAssignToInstanceField +import org.usvm.machine.expr.handleAssignToLocal +import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.mkTruthyExpr +import org.usvm.machine.expr.readGlobal +import org.usvm.machine.expr.writeGlobal import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt @@ -61,19 +67,16 @@ import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.returnValue -import org.usvm.machine.types.EtsAuxiliaryType +import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort import org.usvm.targets.UTargetsSet import org.usvm.types.TypesResult import org.usvm.types.first import org.usvm.types.single -import org.usvm.util.TsResolutionResult import org.usvm.util.mkArrayIndexLValue -import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.resolveEtsField import org.usvm.util.resolveEtsMethods import org.usvm.util.type import org.usvm.utils.ensureSat @@ -457,237 +460,180 @@ class TsInterpreter( } } - private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) { + private fun assignTo( + scope: TsStepScope, + lhv: EtsLValue, + expr: UExpr<*>, + ): Unit? { val exprResolver = exprResolverWithScope(scope) + return when (lhv) { + is EtsLocal -> { + exprResolver.handleAssignToLocal(lhv, expr) + } - val callExpr = stmt.callExpr - if (callExpr != null) { - val methodResult = scope.calcOnState { methodResult } - - when (methodResult) { - is TsMethodResult.NoCall -> observer?.onCallWithUnresolvedArguments( - exprResolver.simpleValueResolver, - callExpr, - scope - ) - - is TsMethodResult.Success -> observer?.onAssignStatement( - exprResolver.simpleValueResolver, - stmt, - scope - ) - - is TsMethodResult.TsException -> error("Exceptions must be processed earlier") + is EtsArrayAccess -> { + exprResolver.handleAssignToArrayIndex(lhv, expr) } - if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { - mockMethodCall(scope, callExpr.callee) - scope.doWithState { newStmt(stmt) } - return + is EtsInstanceFieldRef -> { + exprResolver.handleAssignToInstanceField(lhv, expr) } - } else { - observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) - } - val expr = exprResolver.resolve(stmt.rhv) ?: return + is EtsStaticFieldRef -> { + exprResolver.handleAssignToStaticField(lhv, expr) + } - check(expr.sort != unresolvedSort) { - "A value of the unresolved sort should never be returned from `resolve` function" + else -> TODO("Not yet implemented") } + } - scope.doWithState { - when (val lhv = stmt.lhv) { - is EtsLocal -> { - val idx = mapLocalToIdx(lastEnteredMethod, lhv) - - // If we found the corresponding index, process it as usual. - // Otherwise, process it as a field of the global object. - if (idx != null) { - saveSortForLocal(idx, expr.sort) - - val lValue = mkRegisterStackLValue(expr.sort, idx) - memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) - } else { - val lValue = mkFieldLValue(expr.sort, globalObject, lhv.name) - addedArtificialLocals += lhv.name - memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) + private fun assignToInDfltDflt( + scope: TsStepScope, + lhv: EtsLValue, + expr: UExpr<*>, + ): Unit? = with(ctx) { + val exprResolver = exprResolverWithScope(scope) + val file = scope.calcOnState { lastEnteredMethod.enclosingClass!!.declaringFile!! } + when (lhv) { + is EtsLocal -> { + val name = lhv.name + if (name.startsWith("%") || name.startsWith("_tmp") || name == "this") { + // Normal local variable + exprResolver.handleAssignToLocal(lhv, expr) + } else { + // Global variable + logger.info { + "Assigning to a global variable in %dflt: $name in $file" } + writeGlobal(scope, file, name, expr) } + } - is EtsArrayAccess -> { - val instance = exprResolver.resolve(lhv.array)?.asExpr(addressSort) ?: return@doWithState - exprResolver.checkUndefinedOrNullPropertyRead(instance) ?: return@doWithState - - val index = exprResolver.resolve(lhv.index)?.asExpr(fp64Sort) ?: return@doWithState - - // TODO fork on floating point field + is EtsArrayAccess -> { + val name = lhv.array.name + if (name.startsWith("%") || name.startsWith("_tmp") || name == "this") { + // Normal local array variable + exprResolver.handleAssignToArrayIndex(lhv, expr) + } else { + // Global array variable + logger.info { + "Assigning to an element of a global array variable in dflt: $name[${lhv.index}] in $file" + } + val array = readGlobal(scope, file, name) ?: return null + check(array.sort == addressSort) { + "Expected address sort for the array, got: ${array.sort}" + } + val arrayRef = array.asExpr(addressSort) + val resolvedIndex = exprResolver.resolve(lhv.index) ?: return null + val index = resolvedIndex.asExpr(fp64Sort) val bvIndex = mkFpToBvExpr( roundingMode = fpRoundingModeSortDefaultValue(), value = index, bvSize = 32, - isSigned = true + isSigned = true, ).asExpr(sizeSort) - - // We don't allow access by negative indices and treat is as an error. - exprResolver.checkNegativeIndexRead(bvIndex) ?: return@doWithState - - // TODO: handle the case when `lhv.array.type` is NOT an array. - // In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`. - val arrayType = if (isAllocatedConcreteHeapRef(instance)) { - scope.calcOnState { (memory.typeStreamOf(instance).first()) } + val arrayType = if (isAllocatedConcreteHeapRef(array)) { + scope.calcOnState { memory.typeStreamOf(array).first() } } else { lhv.array.type - } as? EtsArrayType ?: error("Expected EtsArrayType, got: ${lhv.array.type}") - val lengthLValue = mkArrayLengthLValue(instance, arrayType) - val currentLength = memory.read(lengthLValue) - - // We allow readings from the array only in the range [0, length - 1]. - exprResolver.checkReadingInRange(bvIndex, currentLength) ?: return@doWithState - + } + check(arrayType is EtsArrayType) { + "Expected EtsArrayType, got: ${lhv.array.type}" + } val elementSort = typeToSort(arrayType.elementType) - - if (elementSort is TsUnresolvedSort) { - val fakeExpr = expr.toFakeObject(scope) - - val lValue = mkArrayIndexLValue( - addressSort, - instance, - bvIndex.asExpr(sizeSort), - arrayType - ) - - lValuesToAllocatedFakeObjects += lValue to fakeExpr - - memory.write(lValue, fakeExpr, guard = trueExpr) - } else { - val lValue = mkArrayIndexLValue( - elementSort, - instance, - bvIndex.asExpr(sizeSort), - arrayType - ) - - memory.write(lValue, expr.asExpr(elementSort), guard = trueExpr) + val elementLValue = mkArrayIndexLValue( + sort = elementSort, + ref = arrayRef, + index = bvIndex.asExpr(sizeSort), + type = arrayType, + ) + scope.doWithState { + memory.write(elementLValue, expr.cast(), guard = trueExpr) } } + } - is EtsInstanceFieldRef -> { - val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState - exprResolver.checkUndefinedOrNullPropertyRead(instance) ?: return@doWithState - - val instanceRef = instance.unwrapRef(scope) - - val etsField = resolveEtsField(lhv.instance, lhv.field, graph.hierarchy) - scope.doWithState { - // If we access some field, we expect that the object must have this field. - // It is not always true for TS, but we decided to process it so. - val supertype = EtsAuxiliaryType(properties = setOf(lhv.field.name)) - // assert is required to update models - scope.assert(memory.types.evalIsSubtype(instanceRef, supertype)) + is EtsInstanceFieldRef -> { + val name = lhv.instance.name + if (name.startsWith("%") || name.startsWith("_tmp") || name == "this") { + // Normal local instance variable + exprResolver.handleAssignToInstanceField(lhv, expr) + } else { + // Global instance variable + logger.info { + "Assigning to a field of a global variable in dflt: $name.${lhv.field.name} in $file" } - - // If there is no such field, we create a fake field for the expr - val sort = when (etsField) { - is TsResolutionResult.Empty -> unresolvedSort - is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> unresolvedSort + val instance = readGlobal(scope, file, name) ?: return null + check(instance.sort == addressSort) { + "Expected address sort for the instance, got: ${instance.sort}" } - - if (sort == unresolvedSort) { - val fakeObject = expr.toFakeObject(scope) - val lValue = mkFieldLValue(addressSort, instanceRef, lhv.field) - - lValuesToAllocatedFakeObjects += lValue to fakeObject - - memory.write(lValue, fakeObject, guard = trueExpr) - } else { - val lValue = mkFieldLValue(sort, instanceRef, lhv.field) - if (lValue.sort != expr.sort) { - if (expr.isFakeObject()) { - val lhvType = lhv.type - val value = when (lhvType) { - is EtsBooleanType -> { - scope.calcOnState { - pathConstraints += expr.getFakeType(scope).boolTypeExpr - expr.extractBool(scope) - } - } - - is EtsNumberType -> { - scope.calcOnState { - pathConstraints += expr.getFakeType(scope).fpTypeExpr - expr.extractFp(scope) - } - } - - else -> { - scope.calcOnState { - pathConstraints += expr.getFakeType(scope).refTypeExpr - expr.extractRef(scope) - } - } - } - - memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) - } else { - TODO("Support enums fields") - } - } else { - memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) - } + val fieldLValue = mkFieldLValue(expr.sort, instance.asExpr(addressSort), lhv.field) + scope.doWithState { + memory.write(fieldLValue, expr.cast(), guard = trueExpr) } } + } - is EtsStaticFieldRef -> { - val clazz = scene.projectAndSdkClasses.singleOrNull { - it.signature == lhv.field.enclosingClass - } ?: return@doWithState + else -> { + error("LHV of type ${lhv::class.java} is not supported in %dflt::%dflt: $lhv") + } + } + } - val instance = scope.calcOnState { getStaticInstance(clazz) } + private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) { + val exprResolver = exprResolverWithScope(scope) - // TODO: initialize the static field first - // Note: Since we are assigning to a static field, we can omit its initialization, - // if it does not have any side effects. + val callExpr = stmt.callExpr + if (callExpr == null) { + observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) + } else { + val methodResult = scope.calcOnState { methodResult } - val sort = run { - val fields = clazz.fields.filter { it.name == lhv.field.name } - if (fields.size == 1) { - val field = fields.single() - val sort = typeToSort(field.type) - return@run sort - } - unresolvedSort - } - if (sort == unresolvedSort) { - val lValue = mkFieldLValue(addressSort, instance, lhv.field.name) - val fakeObject = expr.toFakeObject(scope) + when (methodResult) { + is TsMethodResult.NoCall -> { + observer?.onCallWithUnresolvedArguments(exprResolver.simpleValueResolver, callExpr, scope) + } - lValuesToAllocatedFakeObjects += lValue to fakeObject + is TsMethodResult.Success -> { + observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) + } - memory.write(lValue, fakeObject, guard = trueExpr) - } else { - val lValue = mkFieldLValue(sort, instance, lhv.field.name) - memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) - } + is TsMethodResult.TsException -> { + error("Exceptions must be processed earlier") } + } - else -> TODO("Not yet implemented") + if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { + mockMethodCall(scope, callExpr.callee) + scope.doWithState { newStmt(stmt) } + return } + } - val nextStmt = stmt.nextStmt ?: return@doWithState - newStmt(nextStmt) + val expr = exprResolver.resolve(stmt.rhv) ?: return + + check(expr.sort != unresolvedSort) { + "A value of the unresolved sort should never be returned from `resolve` function" } + + // Assignments in %dflt::%dflt are *special*... + val isDflt = stmt.location.method.name == DEFAULT_ARK_METHOD_NAME && + stmt.location.method.enclosingClass?.name == DEFAULT_ARK_CLASS_NAME + if (isDflt) { + assignToInDfltDflt(scope, stmt.lhv, expr) ?: return + } else { + assignTo(scope, stmt.lhv, expr) ?: return + } + + val nextStmt = stmt.nextStmt ?: return + scope.doWithState { newStmt(nextStmt) } } private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) { if (scope.calcOnState { methodResult } is TsMethodResult.Success) { - scope.doWithState { - methodResult = TsMethodResult.NoCall - } + scope.doWithState { methodResult = TsMethodResult.NoCall } val nextStmt = stmt.nextStmt ?: return - scope.doWithState { - newStmt(nextStmt) - } + scope.doWithState { newStmt(nextStmt) } return } @@ -705,31 +651,37 @@ class TsInterpreter( private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) { val exprResolver = exprResolverWithScope(scope) + observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) val exception = exprResolver.resolve(stmt.exception) + // Pop the call stack to return to the caller scope.doWithState { memory.stack.pop() + } - if (exception != null) { - val exceptionType: EtsType = when { - exception.sort == ctx.addressSort -> { - // If it's an object reference, try to determine its type - val ref = exception.asExpr(ctx.addressSort) - // For now, assume it's a generic error type - EtsStringType // TODO: improve type detection - } + if (exception != null) { + val exceptionType: EtsType = when (exception.sort) { + ctx.addressSort -> { + // If it's an object reference, try to determine its type + val ref = exception.asExpr(ctx.addressSort) + // For now, assume it's a generic error type + EtsStringType // TODO: improve type detection + } - exception.sort == ctx.fp64Sort -> EtsNumberType + ctx.fp64Sort -> EtsNumberType - exception.sort == ctx.boolSort -> EtsBooleanType + ctx.boolSort -> EtsBooleanType - else -> EtsStringType - } + else -> EtsStringType + } + scope.doWithState { methodResult = TsMethodResult.TsException(exception, exceptionType) - } else { + } + } else { + scope.doWithState { // If we couldn't resolve the exception value, throw a generic exception methodResult = TsMethodResult.TsException(ctx.mkUndefinedValue(), EtsStringType) } @@ -744,36 +696,9 @@ class TsInterpreter( TsExprResolver( ctx = ctx, scope = scope, - localToIdx = ::mapLocalToIdx, hierarchy = graph.hierarchy, ) - // (method, localName) -> idx - private val localVarToIdx: MutableMap> = hashMapOf() - - private fun mapLocalToIdx(method: EtsMethod, local: EtsValue): Int? = - // Note: below, 'n' means the number of arguments - when (local) { - // Note: locals have indices starting from (n+1) - is EtsLocal -> { - val map = localVarToIdx.getOrPut(method) { - method.getDeclaredLocals().mapIndexed { idx, local -> - val localIdx = idx + method.parametersWithThisCount - local.name to localIdx - }.toMap() - } - map[local.name] - } - - // Note: 'this' has index 0 - is EtsThis -> 0 - - // Note: arguments have indices from 1 to n - is EtsParameterRef -> local.index + 1 - - else -> error("Unexpected local: $local") - } - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { val state = TsState( ctx = ctx, @@ -782,14 +707,14 @@ class TsInterpreter( targets = UTargetsSet.from(targets), ) - state.memory.types.allocate(mkTsNullValue().address, EtsNullType) + state.callStack.push(method, returnSite = null) + state.memory.stack.push(method.parametersWithThisCount, method.localsCount) + state.newStmt(method.cfg.instructions.first()) - val solver = ctx.solver() + state.memory.types.allocate(mkTsNullValue().address, EtsNullType) // TODO check for statics - val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type)) - ?: error("Cannot find index for 'this' in method: $method") - check(thisIdx == 0) + val thisIdx = 0 val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx) val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort) @@ -808,23 +733,20 @@ class TsInterpreter( } val parameterType = param.type - if (parameterType is EtsRefType) { + if (parameterType is EtsRefType) run { state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) - val argLValue = mkRegisterStackLValue(addressSort, idx) - val ref = state.memory.read(argLValue).asExpr(addressSort) - if (parameterType is EtsArrayType) { state.pathConstraints += state.memory.types.evalTypeEquals(ref, parameterType) - return@forEachIndexed + return@run } val resolvedParameterType = graph.hierarchy.classesForType(parameterType) if (resolvedParameterType.isEmpty()) { logger.error("Cannot resolve class for parameter type: $parameterType") - return@forEachIndexed // TODO should be an error + return@run // TODO should be an error } // Because of structural equality in TS we cannot determine the exact type @@ -840,22 +762,31 @@ class TsInterpreter( state.pathConstraints += mkHeapRefEq(ref, mkUndefinedValue()) } if (parameterType == EtsStringType) { - state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + + state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) + } + + val parameterSort = typeToSort(parameterType) + if (parameterSort is TsUnresolvedSort) { + // If the parameter type is unresolved, we create a fake object for it + val bool = mkRegisterReading(idx, boolSort) + val fp = mkRegisterReading(idx, fp64Sort) + val ref = mkRegisterReading(idx, addressSort) + val fakeObject = state.mkFakeValue(null, bool, fp, ref) + val lValue = mkRegisterStackLValue(addressSort, idx) + state.memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr) + state.saveSortForLocal(idx, addressSort) + } else { + state.saveSortForLocal(idx, parameterSort) } } + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) - state.callStack.push(method, returnSite = null) - state.memory.stack.push(method.parametersWithThisCount, method.localsCount) - state.newStmt(method.cfg.instructions.first()) - - state.memory.types.allocate(mkTsNullValue().address, EtsNullType) - state } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt index f6a8fdd87c..cba36ca32a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt @@ -1,29 +1,74 @@ package org.usvm.machine.interpreter +import mu.KotlinLogging import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.usvm.UBoolSort +import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue +import org.usvm.machine.TsContext +import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.state.localsCount +import org.usvm.machine.state.newStmt import org.usvm.util.mkFieldLValue +private val logger = KotlinLogging.logger {} + +private fun mkStaticFieldsInitializedFlag( + instance: UHeapRef, + clazz: EtsClassSignature, +): UFieldLValue { + return mkFieldLValue(instance.ctx.boolSort, instance, "__initialized__") +} + internal fun TsState.isInitialized(clazz: EtsClass): Boolean { - val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated") + val instance = getStaticInstance(clazz) val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature) return memory.read(initializedFlag).isTrue } -internal fun TsState.markInitialized(clazz: EtsClass) { - val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated") +internal fun TsState.markStaticsInitialized(clazz: EtsClass) { + val instance = getStaticInstance(clazz) val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature) memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr) } -private fun mkStaticFieldsInitializedFlag( - instance: UHeapRef, - clazz: EtsClassSignature, -): UFieldLValue { - return mkFieldLValue(instance.ctx.boolSort, instance, "__initialized__") +private fun TsState.initializeStatics(clazz: EtsClass, initializer: EtsMethod) { + markStaticsInitialized(clazz) + val instance = getStaticInstance(clazz) + pushSortsForArguments(0) { null } + registerCallee(currentStatement, initializer.cfg) + callStack.push(initializer, currentStatement) + memory.stack.push(arrayOf(instance), initializer.localsCount) + newStmt(initializer.cfg.stmts.first()) +} + +internal fun TsContext.ensureStaticsInitialized( + scope: TsStepScope, + clazz: EtsClass, +): Unit? = scope.calcOnState { + val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME } + if (initializer == null) { + return@calcOnState Unit + } + + // Initialize statics in `clazz` if necessary + if (!isInitialized(clazz)) { + logger.info { "Statics are not initialized for class: $clazz" } + initializeStatics(clazz, initializer) + return@calcOnState null + } + + // TODO: Handle static initializer result + val result = methodResult + // TODO: Why this signature check is needed? + // TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere. + if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) { + methodResult = TsMethodResult.NoCall + } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt index 9a8ac828b9..1cb07d7614 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt @@ -4,7 +4,6 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsType import org.usvm.UExpr -import org.usvm.UHeapRef /** * Represents a result of a method invocation. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index c4531bcf19..37034ea083 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -3,15 +3,13 @@ package org.usvm.machine.state import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsValue import org.usvm.PathNode import org.usvm.UCallStack import org.usvm.UConcreteHeapRef @@ -60,7 +58,6 @@ class TsState( targets: UTargetsSet = UTargetsSet.empty(), val localToSortStack: MutableList> = mutableListOf(persistentHashMapOf()), var staticStorage: UPersistentHashMap = persistentHashMapOf(), - val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)), val addedArtificialLocals: MutableSet = hashSetOf(), val lValuesToAllocatedFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf(), var discoveredCallees: UPersistentHashMap, EtsBlockCfg> = persistentHashMapOf(), @@ -70,6 +67,13 @@ class TsState( var associatedFunction: UPersistentHashMap = persistentHashMapOf(), var closureObject: UPersistentHashMap = persistentHashMapOf(), var boundThis: UPersistentHashMap = persistentHashMapOf(), + var dfltObject: UPersistentHashMap = persistentHashMapOf(), + + /** + * Maps (file signature, field name) to the sort used for that field in the dflt object. + * This tracks sorts for global variables that are represented as fields of dflt objects. + */ + var dfltObjectFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), /** * Maps string values to their corresponding heap references that were allocated for string constants. @@ -94,9 +98,9 @@ class TsState( return localToSort[idx] } - fun getOrPutSortForLocal(idx: Int, localType: EtsType): USort { + fun getOrPutSortForLocal(idx: Int, sort: () -> USort): USort { val localToSort = localToSortStack.last() - val (updated, result) = localToSort.getOrPut(idx, ownership) { ctx.typeToSort(localType) } + val (updated, result) = localToSort.getOrPut(idx, ownership, sort) localToSortStack[localToSortStack.lastIndex] = updated return result } @@ -126,25 +130,15 @@ class TsState( } fun pushSortsForArguments( - instance: EtsLocal?, - args: List, - localToIdx: (EtsMethod, EtsValue) -> Int?, + n: Int, + idxToSort: (Int) -> USort?, ) { - val argSorts = args.map { arg -> - val argIdx = localToIdx(lastEnteredMethod, arg) - ?: error("Arguments must present in the locals, but $arg is absent") - getOrPutSortForLocal(argIdx, arg.type) - } - - val instanceIdx = instance?.let { localToIdx(lastEnteredMethod, it) } - val instanceSort = instanceIdx?.let { getOrPutSortForLocal(it, instance.type) } - - // Note: first, push an empty map, then fill the arguments, and then the instance (this) pushLocalToSortStack() - instanceSort?.let { saveSortForLocal(0, it) } - argSorts.forEachIndexed { i, sort -> - val idx = i + 1 // + 1 because 0 is reserved for `this` - saveSortForLocal(idx, sort) + for (i in 0..n) { + val sort = idxToSort(i) + if (sort != null) { + saveSortForLocal(i, sort) + } } } @@ -203,6 +197,31 @@ class TsState( boundThis = boundThis.put(instance, thisRef, ownership) } + fun getDfltObject(file: EtsFile): UConcreteHeapRef { + val (updated, result) = dfltObject.getOrPut(file.signature, ownership) { + // val dfltClass = file.getDfltClass() + // memory.allocConcrete(dfltClass.type) + ctx.allocateConcreteRef() + } + dfltObject = updated + return result + } + + fun getSortForDfltObjectField( + file: EtsFile, + fieldName: String, + ): USort? { + return dfltObjectFieldSorts[file.signature to fieldName] + } + + fun saveSortForDfltObjectField( + file: EtsFile, + fieldName: String, + sort: USort, + ) { + dfltObjectFieldSorts = dfltObjectFieldSorts.put(file.signature to fieldName, sort, ownership) + } + /** * Initializes and returns a fully constructed string constant in this state's memory. * This function handles both heap reference allocation (via context) and memory initialization. @@ -266,7 +285,6 @@ class TsState( targets = targets.clone(), localToSortStack = localToSortStack.toMutableList(), staticStorage = staticStorage, - globalObject = globalObject, addedArtificialLocals = addedArtificialLocals, lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(), discoveredCallees = discoveredCallees, @@ -276,6 +294,8 @@ class TsState( associatedFunction = associatedFunction, closureObject = closureObject, boundThis = boundThis, + dfltObject = dfltObject, + dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index 2a639ca915..09ac543689 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -2,7 +2,6 @@ package org.usvm.machine.state import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.UExpr import org.usvm.USort @@ -32,4 +31,4 @@ inline val EtsMethod.parametersWithThisCount: Int get() = parameters.size + 1 inline val EtsMethod.localsCount: Int - get() = getDeclaredLocals().size + get() = locals.size diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index 0a67fdcafe..2dcd2bfb8b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -15,55 +15,58 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.memory.ULValue -fun TsContext.mkFakeValue( - scope: TsStepScope, +fun TsState.mkFakeValue( + scope: TsStepScope?, // pass `null` only in the initial state, where `scope` is not available! boolValue: UBoolExpr? = null, fpValue: UExpr? = null, refValue: UHeapRef? = null, -): UConcreteHeapRef { +): UConcreteHeapRef = with(ctx) { require(boolValue != null || fpValue != null || refValue != null) { "Fake object should contain at least one value" } - return scope.calcOnState { - val fakeValueRef = createFakeObjectRef() - val address = fakeValueRef.address - - val boolTypeExpr = trueExpr - .takeIf { boolValue != null && fpValue == null && refValue == null } - ?: makeSymbolicPrimitive(boolSort) - val fpTypeExpr = trueExpr - .takeIf { boolValue == null && fpValue != null && refValue == null } - ?: makeSymbolicPrimitive(boolSort) - val refTypeExpr = trueExpr - .takeIf { boolValue == null && fpValue == null && refValue != null } - ?: makeSymbolicPrimitive(boolSort) - - val type = EtsFakeType( - boolTypeExpr = boolTypeExpr, - fpTypeExpr = fpTypeExpr, - refTypeExpr = refTypeExpr, - ) - memory.types.allocate(address, type) - scope.assert(type.mkExactlyOneTypeConstraint(ctx)) - - if (boolValue != null) { - val boolLValue = ctx.getIntermediateBoolLValue(address) - memory.write(boolLValue, boolValue, guard = ctx.trueExpr) - } + val fakeValueRef = createFakeObjectRef() + val address = fakeValueRef.address + + val boolTypeExpr = trueExpr + .takeIf { boolValue != null && fpValue == null && refValue == null } + ?: makeSymbolicPrimitive(boolSort) + val fpTypeExpr = trueExpr + .takeIf { boolValue == null && fpValue != null && refValue == null } + ?: makeSymbolicPrimitive(boolSort) + val refTypeExpr = trueExpr + .takeIf { boolValue == null && fpValue == null && refValue != null } + ?: makeSymbolicPrimitive(boolSort) + + val type = EtsFakeType( + boolTypeExpr = boolTypeExpr, + fpTypeExpr = fpTypeExpr, + refTypeExpr = refTypeExpr, + ) + memory.types.allocate(address, type) + val constraint = type.mkExactlyOneTypeConstraint(ctx) + if (scope != null) { + scope.assert(constraint) + } else { + pathConstraints += constraint + } - if (fpValue != null) { - val fpLValue = ctx.getIntermediateFpLValue(address) - memory.write(fpLValue, fpValue, guard = ctx.trueExpr) - } + if (boolValue != null) { + val boolLValue = ctx.getIntermediateBoolLValue(address) + memory.write(boolLValue, boolValue, guard = ctx.trueExpr) + } - if (refValue != null) { - val refLValue = ctx.getIntermediateRefLValue(address) - memory.write(refLValue, refValue, guard = ctx.trueExpr) - } + if (fpValue != null) { + val fpLValue = ctx.getIntermediateFpLValue(address) + memory.write(fpLValue, fpValue, guard = ctx.trueExpr) + } - fakeValueRef + if (refValue != null) { + val refLValue = ctx.getIntermediateRefLValue(address) + memory.write(refLValue, refValue, guard = ctx.trueExpr) } + + fakeValueRef } fun TsState.extractValue( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index f2cd906efb..c29c149dd9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -250,8 +250,7 @@ class TsTypeSystem( } override fun isInstantiable(type: EtsType): Boolean { - val t = unwrapAlias(type) - return when (t) { + return when (val t = unwrapAlias(type)) { is EtsNeverType -> false // no runtime value is EtsAnyType, is EtsUnknownType, @@ -272,8 +271,7 @@ class TsTypeSystem( } override fun findSubtypes(type: EtsType): Sequence { - val t = unwrapAlias(type) - return when (t) { + return when (val t = unwrapAlias(type)) { is EtsPrimitiveType -> emptySequence() is EtsAnyType, is EtsUnknownType, diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/BuildEtsMethod.kt b/usvm-ts/src/main/kotlin/org/usvm/util/BuildEtsMethod.kt index 876905ade5..de11cc07ad 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/BuildEtsMethod.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/BuildEtsMethod.kt @@ -3,8 +3,10 @@ package org.usvm.util import org.jacodb.ets.dsl.ProgramBuilder import org.jacodb.ets.dsl.program import org.jacodb.ets.dsl.toBlockCfg +import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter @@ -35,6 +37,11 @@ fun buildEtsMethod( val etsCfg = blockCfg.toEtsBlockCfg(method) method.body.cfg = etsCfg + method.body.locals = etsCfg.stmts + .filterIsInstance() + .mapNotNull { it.lhv as? EtsLocal } + .distinct() + ((enclosingClass as EtsClassImpl).methods as MutableList).add(method) method.enclosingClass = enclosingClass 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..17df6cff52 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -35,8 +35,7 @@ fun TsContext.resolveEtsField( // Unknown signature: if (instance != null) { - val instanceType = instance.type - when (instanceType) { + when (val instanceType = instance.type) { is EtsClassType -> { val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy) if (field != null) return TsResolutionResult.create(field) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsImports.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsImports.kt new file mode 100644 index 0000000000..51bc7f56ab --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsImports.kt @@ -0,0 +1,203 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsExportInfo +import org.jacodb.ets.model.EtsExportType +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsImportInfo +import org.jacodb.ets.model.EtsImportType +import org.jacodb.ets.model.EtsScene + +sealed class ImportResolutionResult { + data class Success(val file: EtsFile) : ImportResolutionResult() + data class NotFound(val reason: String) : ImportResolutionResult() +} + +sealed class SymbolResolutionResult { + data class Success(val file: EtsFile, val exportInfo: EtsExportInfo) : SymbolResolutionResult() + data class FileNotFound(val reason: String) : SymbolResolutionResult() + data class SymbolNotFound(val file: EtsFile, val symbolName: String, val reason: String) : SymbolResolutionResult() +} + +fun EtsScene.resolveImport( + currentFile: EtsFile, + importPath: String, +): ImportResolutionResult { + return try { + when { + importPath.startsWith("@") -> resolveSystemLibrary(importPath) + importPath.startsWith("/") -> resolveAbsolutePath(importPath) + else -> resolveRelativePath(currentFile, importPath) + } + } catch (e: Exception) { + ImportResolutionResult.NotFound(e.message ?: "Unknown error") + } +} + +fun EtsScene.resolveSymbol( + currentFile: EtsFile, + importPath: String, + symbolName: String, + importType: EtsImportType, +): SymbolResolutionResult { + return when (val fileResult = resolveImport(currentFile, importPath)) { + is ImportResolutionResult.NotFound -> SymbolResolutionResult.FileNotFound(fileResult.reason) + is ImportResolutionResult.Success -> resolveSymbolInFile(fileResult.file, symbolName, importType) + } +} + +fun EtsScene.resolveImportInfo( + currentFile: EtsFile, + importInfo: EtsImportInfo, +): SymbolResolutionResult { + return resolveSymbol(currentFile, importInfo.from, importInfo.originalName, importInfo.type) +} + +private fun EtsScene.resolveSystemLibrary(importPath: String): ImportResolutionResult { + val foundFile = sdkFiles.find { file -> + file.signature.fileName.equals(importPath, ignoreCase = true) || + file.signature.fileName.equals("$importPath.ts", ignoreCase = true) || + file.signature.fileName.equals("$importPath.ets", ignoreCase = true) || + file.signature.fileName.equals("$importPath.d.ts", ignoreCase = true) + } + + return if (foundFile != null) { + ImportResolutionResult.Success(foundFile) + } else { + ImportResolutionResult.NotFound("System library not found: '$importPath'") + } +} + +private fun EtsScene.resolveAbsolutePath(importPath: String): ImportResolutionResult { + val normalizedPath = importPath.removePrefix("/") + + val foundFile = (projectFiles + sdkFiles).find { file -> + val fileName = file.signature.fileName + fileName == normalizedPath || + fileName == "$normalizedPath.ts" || + fileName == "$normalizedPath.ets" || + fileName == "$normalizedPath.d.ts" || + fileName.endsWith("/$normalizedPath") || + fileName.endsWith("/$normalizedPath.ts") || + fileName.endsWith("/$normalizedPath.ets") || + fileName.endsWith("/$normalizedPath.d.ts") + } + + return if (foundFile != null) { + ImportResolutionResult.Success(foundFile) + } else { + ImportResolutionResult.NotFound("File not found for absolute path: '$importPath'") + } +} + +private fun EtsScene.resolveRelativePath(currentFile: EtsFile, importPath: String): ImportResolutionResult { + val currentFileName = currentFile.signature.fileName + val currentDir = if (currentFileName.contains("/")) { + currentFileName.substringBeforeLast("/") + } else { + "" + } + + val targetPath = if (currentDir.isEmpty()) { + normalizeRelativePath(importPath) + } else { + normalizeRelativePath("$currentDir/$importPath") + } + + val foundFile = (projectFiles + sdkFiles).find { file -> + val fileName = file.signature.fileName + fileName == targetPath || + fileName == "$targetPath.ts" || + fileName == "$targetPath.ets" || + fileName == "$targetPath.d.ts" || + fileName == "$targetPath/index.ts" || + fileName == "$targetPath/index.ets" || + fileName == "$targetPath/index.d.ts" + } + + return if (foundFile != null) { + ImportResolutionResult.Success(foundFile) + } else { + ImportResolutionResult.NotFound("File not found for relative path: '$importPath' from ${currentFile.signature.fileName}") + } +} + +private fun resolveSymbolInFile( + targetFile: EtsFile, + symbolName: String, + importType: EtsImportType, +): SymbolResolutionResult { + val exports = targetFile.exportInfos + + return when (importType) { + EtsImportType.DEFAULT -> { + val defaultExport = exports.find { it.isDefaultExport } + if (defaultExport != null) { + SymbolResolutionResult.Success(targetFile, defaultExport) + } else { + SymbolResolutionResult.SymbolNotFound( + targetFile, + symbolName, + "Default export not found in ${targetFile.signature.fileName}" + ) + } + } + + EtsImportType.NAMED -> { + val namedExport = exports.find { + it.name == symbolName + } + if (namedExport != null) { + SymbolResolutionResult.Success(targetFile, namedExport) + } else { + SymbolResolutionResult.SymbolNotFound( + targetFile, + symbolName, + "Named export '$symbolName' not found in ${targetFile.signature.fileName}" + ) + } + } + + EtsImportType.NAMESPACE -> { + // For namespace imports, we create a virtual export that represents all exports + if (exports.isNotEmpty()) { + // Create a synthetic namespace export + val namespaceExport = EtsExportInfo( + name = symbolName, + type = EtsExportType.NAMESPACE, + ) + SymbolResolutionResult.Success(targetFile, namespaceExport) + } else { + SymbolResolutionResult.SymbolNotFound( + targetFile, + symbolName, + "No exports found for namespace import in ${targetFile.signature.fileName}" + ) + } + } + + EtsImportType.SIDE_EFFECT -> { + // Side effect imports don't import specific symbols + // Create a synthetic export to represent the side effect + val sideEffectExport = EtsExportInfo( + name = "", + type = EtsExportType.UNKNOWN, + ) + SymbolResolutionResult.Success(targetFile, sideEffectExport) + } + } +} + +fun normalizeRelativePath(path: String): String { + val parts = path.split("/") + val result = mutableListOf() + + for (part in parts) { + when (part) { + "", "." -> continue + ".." -> if (result.isNotEmpty()) result.removeLastOrNull() + else -> result.add(part) + } + } + + return result.joinToString("/") +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 8315e690b7..5762923b69 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -24,8 +24,8 @@ import org.usvm.machine.types.mkFakeValue fun TsContext.boolToFp(expr: UExpr): UExpr = mkIte(expr, mkFp64(1.0), mkFp64(0.0)) -fun TsState.throwExceptionWithoutStackFrameDrop(address: UHeapRef, type: EtsType) { - methodResult = TsMethodResult.TsException(address, type) +fun TsState.throwExceptionWithoutStackFrameDrop(ref: UHeapRef, type: EtsType) { + methodResult = TsMethodResult.TsException(ref, type) } val EtsClass.type: EtsClassType @@ -55,29 +55,27 @@ fun EtsType.getClassesForType( // TODO save info about this field somewhere // https://github.com/UnitTestBot/usvm/issues/288 -fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHeapRef { - val ctx = this.tctx +fun UHeapRef.createFakeField( + scope: TsStepScope, + fieldName: String, +): UConcreteHeapRef = with(tctx) { + val lValue = mkFieldLValue(addressSort, this@createFakeField, fieldName) - val lValue = mkFieldLValue(ctx.addressSort, this, fieldName) + val boolLValue = mkFieldLValue(boolSort, this@createFakeField, fieldName) + val fpLValue = mkFieldLValue(fp64Sort, this@createFakeField, fieldName) + val refLValue = mkFieldLValue(addressSort, this@createFakeField, fieldName) - val boolLValue = mkFieldLValue(ctx.boolSort, this, fieldName) - val fpLValue = mkFieldLValue(ctx.fp64Sort, this, fieldName) - val refLValue = mkFieldLValue(ctx.addressSort, this, fieldName) + val bool = scope.calcOnState { memory.read(boolLValue) } + val fp = scope.calcOnState { memory.read(fpLValue) } + val ref = scope.calcOnState { memory.read(refLValue) } - val boolValue = scope.calcOnState { memory.read(boolLValue) } - val fpValue = scope.calcOnState { memory.read(fpLValue) } - val refValue = scope.calcOnState { memory.read(refLValue) } - - with(ctx) { - if (refValue.isFakeObject()) { - return refValue - } + if (ref.isFakeObject()) { + return ref } - val fakeObject = ctx.mkFakeValue(scope, boolValue, fpValue, refValue) - scope.doWithState { + scope.calcOnState { + val fakeObject = mkFakeValue(scope, bool, fp, ref) memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr) + fakeObject } - - return fakeObject } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt new file mode 100644 index 0000000000..660b670a17 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/ImportExportResolution.kt @@ -0,0 +1,492 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsExportInfo +import org.jacodb.ets.model.EtsExportType +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsImportInfo +import org.jacodb.ets.model.EtsImportType +import org.jacodb.ets.model.EtsModifier +import org.jacodb.ets.model.EtsModifiers +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.DisplayName +import org.junit.jupiter.api.Test +import org.usvm.util.ImportResolutionResult +import org.usvm.util.SymbolResolutionResult +import org.usvm.util.resolveImport +import org.usvm.util.resolveImportInfo +import org.usvm.util.resolveSymbol +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +@DisplayName("Import and Export Resolution Tests") +class ImportExportResolutionTest { + + private lateinit var scene: EtsScene + private lateinit var currentFile: EtsFile + private lateinit var targetFile1: EtsFile + private lateinit var targetFile2: EtsFile + private lateinit var systemLibraryFile: EtsFile + + @BeforeEach + fun setup() { + // Create target file with various export types + targetFile1 = createMockFile( + signature = EtsFileSignature("TestProject", "src/utils/helper.ets"), + exports = listOf( + // Default export: + // export default class Helper {} + EtsExportInfo( + "default", + EtsExportType.CLASS, + nameBeforeAs = "Helper", + modifiers = EtsModifiers.of(EtsModifier.DEFAULT) + ), + + // Named exports: + // export function utility() {} + EtsExportInfo("utility", EtsExportType.METHOD), + // export const CONSTANT = 42; + EtsExportInfo("CONSTANT", EtsExportType.LOCAL), + + // Aliased export: + // function internalName() {} + // export { internalName as PublicName }; + EtsExportInfo("PublicName", EtsExportType.METHOD, nameBeforeAs = "internalName"), + + // Re-export from another module: + // export class ExternalUtil {} (in 'src/utils/external.ts') + // export { ExternalUtil } from './external'; + EtsExportInfo("ExternalUtil", EtsExportType.CLASS, from = "./external"), + ) + ) + + // Create another target file with namespace and type exports + targetFile2 = createMockFile( + signature = EtsFileSignature("TestProject", "src/types/index.ets"), + exports = listOf( + // Namespace export: + // export namespace Types {} + EtsExportInfo("Types", EtsExportType.NAMESPACE), + + // Type export: + // export type UserType = { name: string; } + EtsExportInfo("UserType", EtsExportType.TYPE), + + // Star re-export: + // export * from './all-types'; + EtsExportInfo("*", EtsExportType.NAMESPACE, from = "./all-types"), + ) + ) + + // Create system library file + systemLibraryFile = createMockFile( + signature = EtsFileSignature("SystemLibrary", "@ohos.router.d.ts"), + exports = listOf( + EtsExportInfo("Router", EtsExportType.CLASS), + EtsExportInfo("navigate", EtsExportType.METHOD), + ) + ) + + // Create current file + currentFile = createMockFile( + signature = EtsFileSignature("TestProject", "src/components/Component.ets"), + exports = emptyList() + ) + + // Create scene with all files + scene = EtsScene( + projectFiles = listOf(currentFile, targetFile1, targetFile2), + sdkFiles = listOf(systemLibraryFile), + projectName = "TestProject", + ) + } + + // Test file resolution for different path types + @Test + @DisplayName("Test system library import resolution") + fun testSystemLibraryResolution() { + val result = scene.resolveImport(currentFile, "@ohos.router") + assertIs(result) + assertEquals("@ohos.router.d.ts", result.file.signature.fileName) + } + + @Test + @DisplayName("Test relative import resolution") + fun testRelativeImportResolution() { + val result = scene.resolveImport(currentFile, "../utils/helper") + assertIs(result) + assertEquals("src/utils/helper.ets", result.file.signature.fileName) + } + + @Test + @DisplayName("Test absolute import resolution") + fun testAbsoluteImportResolution() { + val result = scene.resolveImport(currentFile, "/src/types/index") + assertIs(result) + assertEquals("src/types/index.ets", result.file.signature.fileName) + } + + @Test + @DisplayName("Test import resolution failure") + fun testImportNotFound() { + val result = scene.resolveImport(currentFile, "./nonexistent") + assertIs(result) + assertTrue(result.reason.contains("File not found")) + } + + // Test symbol resolution for default imports + @Test + @DisplayName("Test default import symbol resolution") + fun testDefaultImportResolution() { + // Import a default symbol: + // import Helper from '../utils/helper'; + // export default Helper; (in helper.ets) + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "Helper", + importType = EtsImportType.DEFAULT, + ) + assertIs(result) + assertTrue(result.exportInfo.isDefaultExport) + assertEquals("default", result.exportInfo.name) + assertEquals("Helper", result.exportInfo.originalName) + assertEquals(EtsExportType.CLASS, result.exportInfo.type) + } + + @Test + @DisplayName("Test default import when no default export exists") + fun testDefaultImportNoDefaultExport() { + // Try to import a default export that doesn't exist: + // import Types from '/src/types/index'; + // Should fail since index.ets does not have a default export + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "/src/types/index", + symbolName = "Types", + importType = EtsImportType.DEFAULT, + ) + assertIs(result) + assertTrue(result.reason.contains("Default export not found")) + } + + // Test symbol resolution for named imports + @Test + @DisplayName("Test named import symbol resolution") + fun testNamedImportResolution() { + // Import a named symbol: + // import { utility } from '../utils/helper'; + // export function utility() {} (in helper.ets) + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "utility", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertEquals("utility", result.exportInfo.name) + assertEquals(EtsExportType.METHOD, result.exportInfo.type) + } + + @Test + @DisplayName("Test named import with aliased export") + fun testNamedImportWithAlias() { + // Import an aliased symbol: + // import { PublicName } from '../utils/helper'; + // export { internalName as PublicName }; (in helper.ets) + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "PublicName", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertEquals("PublicName", result.exportInfo.name) + assertEquals("internalName", result.exportInfo.originalName) + assertTrue(result.exportInfo.isAliased) + } + + @Test + @DisplayName("Test named import matching original name before alias") + fun testNamedImportMatchingOriginalName() { + // Try to import the aliased symbol by its original name: + // import { internalName } from '../utils/helper'; + // export { internalName as PublicName }; + // Should fail since 'internalName' is not exported directly, but aliased to 'PublicName'. + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "internalName", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertTrue(result.reason.contains("Named export 'internalName' not found")) + } + + @Test + @DisplayName("Test named import when symbol not found") + fun testNamedImportNotFound() { + // Try to import a non-existent symbol: + // import { nonexistent } from '../utils/helper'; + // no such export in helper.ets + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "nonexistent", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertTrue(result.reason.contains("Named export 'nonexistent' not found")) + } + + // Test symbol resolution for namespace imports + @Test + @DisplayName("Test namespace import symbol resolution") + fun testNamespaceImportResolution() { + // Import all symbols from a module: + // import * as HelperModule from '../utils/helper'; + // Should resolve to a virtual namespace export + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "HelperModule", + importType = EtsImportType.NAMESPACE, + ) + assertIs(result) + assertEquals("HelperModule", result.exportInfo.name) + assertEquals(EtsExportType.NAMESPACE, result.exportInfo.type) + } + + @Test + @DisplayName("Test namespace import when no exports exist") + fun testNamespaceImportNoExports() { + // Create file with no exports + val emptyFileSignature = EtsFileSignature("TestProject", "src/empty.ets") + val emptyFile = createMockFile(emptyFileSignature, exports = emptyList()) + val sceneWithEmpty = EtsScene( + projectFiles = listOf(currentFile, emptyFile), + sdkFiles = emptyList(), + projectName = "TestProject", + ) + + // Import all symbols from an empty module: + // import * as EmptyModule from '/src/empty'; + // Should fail since there are no exports in empty.ets + val result = sceneWithEmpty.resolveSymbol( + currentFile = currentFile, + importPath = "/src/empty", + symbolName = "EmptyModule", + importType = EtsImportType.NAMESPACE, + ) + assertIs(result) + assertTrue(result.reason.contains("No exports found for namespace import")) + } + + // Test symbol resolution for side effect imports + @Test + @DisplayName("Test side effect import symbol resolution") + fun testSideEffectImportResolution() { + // Import a module for its side effects: + // import '../utils/helper'; + // Should resolve to a virtual export with no specific symbol + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "", + importType = EtsImportType.SIDE_EFFECT, + ) + assertIs(result) + assertEquals("", result.exportInfo.name) + assertEquals(EtsExportType.UNKNOWN, result.exportInfo.type) + } + + // Test complete import info resolution + @Test + @DisplayName("Test complete import info resolution for default import") + fun testCompleteDefaultImportInfo() { + // Import a default symbol: + // import Helper from '../utils/helper'; + val importInfo = EtsImportInfo( + name = "Helper", + type = EtsImportType.DEFAULT, + from = "../utils/helper", + ) + + // export default class Helper {} (in helper.ets) + val result = scene.resolveImportInfo(currentFile, importInfo) + assertIs(result) + assertEquals("default", result.exportInfo.name) + assertEquals("Helper", result.exportInfo.originalName) + } + + @Test + @DisplayName("Test complete import info resolution for named import") + fun testCompleteNamedImportInfo() { + // Import a named symbol: + // import { utility } from '../utils/helper'; + val importInfo = EtsImportInfo( + name = "utility", + type = EtsImportType.NAMED, + from = "../utils/helper", + ) + + // export function utility() {} (in helper.ets) + val result = scene.resolveImportInfo(currentFile, importInfo) + assertIs(result) + assertEquals("utility", result.exportInfo.name) + assertEquals(EtsExportType.METHOD, result.exportInfo.type) + } + + @Test + @DisplayName("Test complete import info resolution with alias") + fun testCompleteImportAliasResolution() { + // Import an aliased named symbol: + // import { PublicName as importedName } from '../utils/helper'; + val importInfo = EtsImportInfo( + name = "importedName", + nameBeforeAs = "PublicName", + type = EtsImportType.NAMED, + from = "../utils/helper", + ) + // in helper.ets: + // export { internalName as PublicName }; + val result = scene.resolveImportInfo(currentFile, importInfo) + assertIs(result, "Expected successful resolution, but got: $result") + assertEquals("PublicName", result.exportInfo.name) + assertEquals("internalName", result.exportInfo.originalName) + } + + @Test + @DisplayName("Test complete import info resolution for namespace import") + fun testCompleteNamespaceImportInfo() { + // Import all symbols from a module: + // import * as HelperNamespace from '../utils/helper'; + val importInfo = EtsImportInfo( + name = "HelperNamespace", + type = EtsImportType.NAMESPACE, + from = "../utils/helper", + ) + + // Should resolve to a virtual namespace export + val result = scene.resolveImportInfo(currentFile, importInfo) + assertIs(result) + assertEquals("HelperNamespace", result.exportInfo.name) + assertEquals(EtsExportType.NAMESPACE, result.exportInfo.type) + } + + // Test various export scenarios + @Test + @DisplayName("Test resolution with re-exported symbols") + fun testReExportedSymbolResolution() { + // Import re-exported symbol: + // import { ExternalUtil } from '../utils/helper'; + // export { ExternalUtil } from './external'; (in helper.ets) + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "../utils/helper", + symbolName = "ExternalUtil", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertEquals("ExternalUtil", result.exportInfo.name) + assertEquals("./external", result.exportInfo.from) + } + + @Test + @DisplayName("Test path normalization in relative imports") + fun testPathNormalizationInImports() { + // Test complex relative path that should normalize to the target + val result = scene.resolveImport(currentFile, "./../../src/utils/helper") + assertIs(result) + assertEquals("src/utils/helper.ets", result.file.signature.fileName) + } + + @Test + @DisplayName("Test file resolution with different extensions") + fun testFileResolutionWithExtensions() { + // Should match files with .ets extension even when not specified + val result1 = scene.resolveImport(currentFile, "../utils/helper") + assertIs(result1) + + // Should also work with explicit .ets extension + val result2 = scene.resolveImport(currentFile, "../utils/helper.ets") + assertIs(result2) + } + + // Test edge cases + @Test + @DisplayName("Test symbol resolution when file not found") + fun testSymbolResolutionFileNotFound() { + // Attempt to resolve a symbol from a non-existent file: + // import { SomeSymbol } from './nonexistent'; + val result = scene.resolveSymbol( + currentFile = currentFile, + importPath = "./nonexistent", + symbolName = "SomeSymbol", + importType = EtsImportType.NAMED, + ) + assertIs(result) + assertTrue(result.reason.contains("File not found")) + } + + @Test + @DisplayName("Test various import types against same file") + fun testMultipleImportTypesAgainstSameFile() { + val filePath = "../utils/helper" + + // Test default import: + // import Helper from '../utils/helper'; + val defaultResult = scene.resolveSymbol( + currentFile = currentFile, + importPath = filePath, + symbolName = "Helper", + importType = EtsImportType.DEFAULT, + ) + assertIs(defaultResult) + + // Test named import: + // import { utility } from '../utils/helper'; + val namedResult = scene.resolveSymbol( + currentFile = currentFile, + importPath = filePath, + symbolName = "utility", + importType = EtsImportType.NAMED, + ) + assertIs(namedResult) + + // Test namespace import: + // import * as HelperNs from '../utils/helper'; + val namespaceResult = scene.resolveSymbol( + currentFile = currentFile, + importPath = filePath, + symbolName = "HelperNs", + importType = EtsImportType.NAMESPACE, + ) + assertIs(namespaceResult) + + // Test side effect import + // import '../utils/helper'; + val sideEffectResult = scene.resolveSymbol( + currentFile = currentFile, + importPath = filePath, + symbolName = "", + importType = EtsImportType.SIDE_EFFECT, + ) + assertIs(sideEffectResult) + } + + // Helper function to create mock EtsFile instances + private fun createMockFile(signature: EtsFileSignature, exports: List): EtsFile { + // Since EtsFile is a final class, we need to create it using its constructor + return EtsFile( + signature = signature, + classes = emptyList(), + namespaces = emptyList(), + importInfos = emptyList(), + exportInfos = exports, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/ImportResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/project/ImportResolver.kt new file mode 100644 index 0000000000..03efb4f2c8 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/project/ImportResolver.kt @@ -0,0 +1,355 @@ +package org.usvm.project + +import mu.KotlinLogging +import org.jacodb.ets.model.EtsExportInfo +import org.jacodb.ets.model.EtsExportType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Assumptions +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.DisplayName +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.TestInstance +import org.usvm.util.ImportResolutionResult +import org.usvm.util.SymbolResolutionResult +import org.usvm.util.abort +import org.usvm.util.getResourcePathOrNull +import org.usvm.util.normalizeRelativePath +import org.usvm.util.resolveImport +import org.usvm.util.resolveSymbol +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +private val logger = KotlinLogging.logger {} + +@TestInstance(TestInstance.Lifecycle.PER_CLASS) +@DisplayName("Import Resolution Tests") +class ImportResolverTest { + + companion object { + private const val TEST_PROJECT_PATH = "/projects/Demo_Photos/source" + } + + private lateinit var scene: EtsScene + + @BeforeAll + fun setupScene() { + println("\n--- Setting up scene for import resolution tests ---") + scene = run { + val path = TEST_PROJECT_PATH + println("Loading project from resources: $path") + val projectPath = getResourcePathOrNull(path) + if (projectPath == null) { + logger.warn { "Project '$path' not found in resources. Ensure the project is available." } + abort() + } + + println("Loading project from path: $projectPath") + val projectScene = loadEtsProjectAutoConvert(projectPath) + println("Project loaded: ${projectScene.projectName} with ${projectScene.projectFiles.size} files") + assertTrue( + projectScene.projectFiles.isNotEmpty(), + "No project files found in the project at '$path'. Ensure the project is correctly set up." + ) + + val sdks = listOf( + "/sdk/ohos/5.0.1.111/ets/api", + "/sdk/ohos/5.0.1.111/ets/arkts", + "/sdk/ohos/5.0.1.111/ets/component", + "/sdk/ohos/5.0.1.111/ets/kits", + "/sdk/typescript", + ).map { + println("Loading SDK from resource: $it") + val sdkPath = getResourcePathOrNull(it) + assertNotNull( + sdkPath, + "SDK path '$it' not found in resources. Ensure the SDK is available." + ) + + println("Loading SDK from path: $sdkPath") + val sdkScene = loadEtsProjectAutoConvert(sdkPath, useArkAnalyzerTypeInference = null) + println("SDK loaded: ${sdkScene.projectName} with ${sdkScene.projectFiles.size} files") + assertTrue( + sdkScene.projectFiles.isNotEmpty(), + "No SDK files found in the SDK at '$it'. Ensure the SDK is correctly set up." + ) + + sdkScene + } + + println("Merging project and SDK files...") + EtsScene( + projectFiles = projectScene.projectFiles, + sdkFiles = sdks.flatMap { it.projectFiles }, + projectName = projectScene.projectName, + ) + } + + println("Scene loaded with ${scene.projectFiles.size} project files and ${scene.sdkFiles.size} SDK files") + } + + @Test + @DisplayName("Test file-level import resolution with real imports from project files") + fun testFileImportResolver() { + println("\n--- Testing file-level import resolver ---") + + val allFiles = scene.projectFiles + var totalImports = 0 + var successfulImports = 0 + var failedImports = 0 + + allFiles.forEachIndexed { index, currentFile -> + val fileName = currentFile.signature.fileName + val imports = currentFile.importInfos + + if (imports.isEmpty()) { + println("\n[${index + 1}/${allFiles.size}] File: $fileName (no imports)") + } else { + println("\n[${index + 1}/${allFiles.size}] File: $fileName (${imports.size} imports)") + + imports.forEach { importInfo -> + totalImports++ + + when (val result = scene.resolveImport(currentFile, importInfo.from)) { + is ImportResolutionResult.Success -> { + successfulImports++ + println( + " ✅ '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + + " (type: ${importInfo.type})" + ) + } + + is ImportResolutionResult.NotFound -> { + failedImports++ + println( + " ❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + + " (type: ${importInfo.type})" + ) + } + } + } + } + } + + println("\n--- File Import Resolution Summary ---") + println("Total imports found: $totalImports") + println("Successfully resolved files: $successfulImports") + println("Failed to resolve files: $failedImports") + if (totalImports > 0) { + val successRate = (successfulImports.toDouble() / totalImports * 100).toInt() + println("File resolution success rate: $successRate%") + } + + // Assert that we found some imports and some were successful + assertTrue(totalImports > 0, "Should find at least some imports in the project files") + // Note: We don't assert on success rate as it depends on the availability of imported files + } + + @Test + @DisplayName("Test complete symbol resolution with real imports matching actual exports") + fun testSymbolResolver() { + println("\n--- Testing complete symbol resolver ---") + + val allFiles = scene.projectFiles + var totalSymbols = 0 + var successfulSymbols = 0 + var fileNotFoundSymbols = 0 + var symbolNotFoundSymbols = 0 + + allFiles.forEachIndexed { index, currentFile -> + val fileName = currentFile.signature.fileName + val imports = currentFile.importInfos + + if (imports.isEmpty()) { + println("\n[${index + 1}/${allFiles.size}] File: '$fileName' (no imports)") + } else { + println("\n[${index + 1}/${allFiles.size}] File: '$fileName' (${imports.size} imports)") + + imports.forEach { importInfo -> + totalSymbols++ + + when (val result = + scene.resolveSymbol( + currentFile = currentFile, + importPath = importInfo.from, + symbolName = importInfo.name, + importType = importInfo.type, + )) { + is SymbolResolutionResult.Success -> { + successfulSymbols++ + val exportInfo = result.exportInfo + println( + " 🎯 '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + + " exports: ${getExportDescription(exportInfo)} (import type: ${importInfo.type})" + ) + } + + is SymbolResolutionResult.FileNotFound -> { + fileNotFoundSymbols++ + println( + " 📁❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + + " (import type: ${importInfo.type})" + ) + } + + is SymbolResolutionResult.SymbolNotFound -> { + symbolNotFoundSymbols++ + println( + " 🔍❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + + " (import type: ${importInfo.type})" + ) + val availableExports = result.file.exportInfos + if (availableExports.isNotEmpty()) { + val exportNames = availableExports.map { it.name }.take(5) + println( + " Available exports: ${ + exportNames.joinToString(", ") + }${ + if (availableExports.size > 5) " ..." else "" + }" + ) + } + } + } + } + } + } + + println("\n--- Complete Symbol Resolution Summary ---") + println("Total symbols to resolve: $totalSymbols") + println("Successfully resolved symbols: $successfulSymbols") + println("File not found: $fileNotFoundSymbols") + println("Symbol not found in file: $symbolNotFoundSymbols") + if (totalSymbols > 0) { + val symbolSuccessRate = (successfulSymbols.toDouble() / totalSymbols * 100).toInt() + println("Complete symbol resolution success rate: $symbolSuccessRate%") + } + + // Assert that we found some symbols to resolve + assertTrue(totalSymbols > 0, "Should find at least some symbols to resolve in the project files") + // Note: We don't assert on success rate as it depends on the availability of matching exports + } + + @Test + @DisplayName("Test common import patterns and path normalization") + fun testCommonImportPatterns() { + println("\n--- Testing common import patterns ---") + + Assumptions.assumeTrue( + scene.projectFiles.isNotEmpty(), + "No project files found in the scene" + ) + + val testFile = scene.projectFiles.first() + println("Using test file: ${testFile.signature.fileName}") + + // Test cases for different import types + val testCases = mapOf( + "System Library Imports" to listOf( + "@ohos.router", + "@ohos.app.ability.UIAbility", + "@ohos.hilog", + "@system.app", + "@system.router", + ), + "Relative Imports" to listOf( + "./component", + "../utils/helper", + "../../shared/types", + "./index", + "../common", + ), + "Absolute Imports" to listOf( + "/src/main", + "/common/GlobalContext", + "/utils/Log", + "/models/Action", + "/components/ToolBar", + "/pages/Index", + ) + ) + + var totalTestedImports = 0 + var successfulImports = 0 + + testCases.forEach { (category, imports) -> + println("\n$category:") + imports.forEach { importPath -> + totalTestedImports++ + when (val result = scene.resolveImport(testFile, importPath)) { + is ImportResolutionResult.Success -> { + successfulImports++ + println(" ✓ '$importPath' resolved to '${result.file.signature.fileName}'") + } + + is ImportResolutionResult.NotFound -> { + println(" ✗ '$importPath' failed: ${result.reason}") + } + } + } + } + + // Test path normalization + println("\nPath Normalization Tests:") + val normalizationTests = listOf( + "./a/../b" to "b", + "a/./b" to "a/b", + "a/../b/./c" to "b/c", + "./a/b/../c" to "a/c", + "a/b/../../c" to "c" + ) + + var correctNormalizations = 0 + normalizationTests.forEach { (input, expected) -> + val result = normalizeRelativePath(input) + val status = if (result == expected) "✓" else "✗" + if (result == expected) correctNormalizations++ + println(" $status '$input' -> '$result' (expected: '$expected')") + } + + // Summary statistics + println("\n--- Summary ---") + println("Project files: ${scene.projectFiles.size}") + println("SDK files: ${scene.sdkFiles.size}") + println("Total files: ${scene.projectAndSdkClasses.size}") + println("Total imports in project files: ${scene.projectFiles.sumOf { it.importInfos.size }}") + + val projectFilesByExtension = scene.projectFiles.groupBy { + it.signature.fileName.substringAfterLast(".", "no-ext") + } + println("Project files by extension: ${projectFilesByExtension.mapValues { it.value.size }}") + + val sdkFilesByExtension = scene.sdkFiles.groupBy { + it.signature.fileName.substringAfterLast(".", "no-ext") + } + println("SDK files by extension: ${sdkFilesByExtension.mapValues { it.value.size }}") + + // Assertions + assertTrue(scene.projectFiles.isNotEmpty(), "Should have at least one project file") + assertTrue(scene.sdkFiles.isNotEmpty(), "Should have at least one SDK file") + assertTrue(totalTestedImports > 0, "Should have tested at least one import pattern") + assertEquals( + correctNormalizations, + normalizationTests.size, + "All path normalization tests should pass (expected: ${normalizationTests.size}, actual: $correctNormalizations)" + ) + assertEquals( + totalTestedImports, + testCases.values.sumOf { it.size }, + "Should have tested all import patterns" + ) + } + + // Helper function to describe export information + private fun getExportDescription(exportInfo: EtsExportInfo): String { + return when (exportInfo.type) { + EtsExportType.NAMESPACE -> "namespace ${exportInfo.name}" + EtsExportType.CLASS -> "class ${exportInfo.name}" + EtsExportType.METHOD -> "method ${exportInfo.name}" + EtsExportType.LOCAL -> "local ${exportInfo.name}" + EtsExportType.TYPE -> "type ${exportInfo.name}" + EtsExportType.UNKNOWN -> "unknown export ${exportInfo.name}" + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/imports/Imports.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/imports/Imports.kt new file mode 100644 index 0000000000..adab612c65 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/imports/Imports.kt @@ -0,0 +1,472 @@ +package org.usvm.samples.imports + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.util.getResourcePath + +class Imports : TsMethodTestRunner() { + private val tsPath = "/samples/imports" + + override val scene: EtsScene = run { + val path = getResourcePath(tsPath) + loadEtsProjectAutoConvert(path, useArkAnalyzerTypeInference = null) + } + + @Test + fun `test get exported number`() { + val method = getMethod("getExportedNumber") + discoverProperties( + method = method, + { r -> r eq 123 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported string`() { + val method = getMethod("getExportedString") + discoverProperties( + method = method, + { r -> r eq "hello" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported boolean`() { + val method = getMethod("getExportedBoolean") + discoverProperties( + method = method, + { r -> r.value }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported null`() { + val method = getMethod("getExportedNull") + discoverProperties( + method = method, + { r -> r == TsTestValue.TsNull }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported undefined`() { + val method = getMethod("getExportedUndefined") + discoverProperties( + method = method, + { r -> r == TsTestValue.TsUndefined }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported float`() { + val method = getMethod("getExportedFloat") + discoverProperties( + method = method, + { r -> r eq 3.14159 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported negative number`() { + val method = getMethod("getExportedNegativeNumber") + discoverProperties( + method = method, + { r -> r eq -456 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get exported empty string`() { + val method = getMethod("getExportedEmptyString") + discoverProperties( + method = method, + { r -> r eq "" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get default value`() { + val method = getMethod("getDefaultValue") + discoverProperties( + method = method, + { r -> r eq "default-string" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get renamed value`() { + val method = getMethod("getRenamedValue") + discoverProperties( + method = method, + { r -> r eq 100 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get renamed string`() { + val method = getMethod("getRenamedString") + discoverProperties( + method = method, + { r -> r eq "mixed" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get renamed boolean`() { + val method = getMethod("getRenamedBoolean") + discoverProperties( + method = method, + { r -> r.value }, // true + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Star imports are not yet supported") + @Test + fun `test use namespace variables`() { + val method = getMethod("useNamespaceVariables") + discoverProperties( + method = method, + { r -> r eq 126.14159 }, // 123 + 3.14159 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Re-exporting is not yet supported") + @Test + fun `test use re-exported values`() { + val method = getMethod("useReExportedValues") + discoverProperties( + method = method, + { r -> r eq 165 }, // reExportedNumber (123) + AllFromDefault.namedValue (42) + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test get computed number`() { + val method = getMethod("getComputedNumber") + discoverProperties( + method = method, + { r -> r eq 314.159 }, // PI * MAX_SIZE = 3.14159 * 100 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("String operations are not yet supported") + @Test + fun `test get config string`() { + val method = getMethod("getConfigString") + discoverProperties( + method = method, + { r -> r eq "timeout:5000ms" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test use const imports`() { + val method = getMethod("useConstImports") + discoverProperties( + method = method, + { r -> r eq 5103.14159 }, // PI(3.14159) + MAX_SIZE(100) + timeout(5000) + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Star imports are not yet supported") + @Test + fun `test use destructuring`() { + val method = getMethod("useDestructuring") + discoverProperties( + method = method, + { r -> r eq 246 }, // bool ? num * 2 : num -> true ? 123 * 2 : 123 = 246 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("String operations are not yet supported") + @Test + fun `test combine variables`() { + val method = getMethod("combineVariables") + discoverProperties( + method = method, + { r -> r eq "hello-named-export-mixed-timeout:5000ms" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test math operations on variables`() { + val method = getMethod("mathOperationsOnVariables") + discoverProperties( + method = method, + { r -> r eq 537.159 }, // 123 + 100 + 314.159 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Imported functions are not supported yet") + @Test + fun `test use imported function`() { + val method = getMethod("useImportedFunction") + discoverProperties( + method = method, + { input, r -> (input eq 5) && (r eq 10) }, + { input, r -> (input eq 0) && (r eq 0) }, + { input, r -> (input eq -3) && (r eq -6) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Imported classes are not supported yet") + @Test + fun `test use imported class`() { + val method = getMethod("useImportedClass") + discoverProperties( + method = method, + { value, r -> (value eq 10) && (r eq 30) }, + { value, r -> (value eq 5) && (r eq 15) }, + { value, r -> (value eq 0) && (r eq 0) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Imported functions and classes are not supported yet") + @Test + fun `test use renamed complex imports`() { + val method = getMethod("useRenamedComplexImports") + discoverProperties( + method = method, + { r -> r eq 160 }, // computeValue(10) = 110, + instance.value = 50 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Namespace imports with functions/classes are not supported yet") + @Test + fun `test use namespace complex import`() { + val method = getMethod("useNamespaceComplexImport") + discoverProperties( + method = method, + { value, r -> (value eq 10) && (r eq 20) }, + { value, r -> (value eq 5) && (r eq 10) }, + { value, r -> (value eq 0) && (r eq 0) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Async functions are not supported yet") + @Test + fun `test use async import`() { + val method = getMethod("useAsyncImport") + discoverProperties( + method = method, + { delay, r -> (delay eq 10) && (r eq 105) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Enums are not supported yet") + @Test + fun `test use enum imports`() { + val method = getMethod("useEnumImports") + discoverProperties( + method = method, + { r -> r eq "red-2" }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Function overloads are not supported yet") + @Test + fun `test use function overloads number`() { + val method = getMethod("useFunctionOverloadsNumber") + discoverProperties( + method = method, + { input, r -> (input eq 5) && (r eq 10) }, + { input, r -> (input eq 0) && (r eq 0) }, + { input, r -> (input eq 10) && (r eq 20) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Function overloads are not supported yet") + @Test + fun `test use function overloads string`() { + val method = getMethod("useFunctionOverloadsString") + discoverProperties( + method = method, + { input, r -> (input eq "hello") && (r eq "HELLO") }, + { input, r -> (input eq "test") && (r eq "TEST") }, + { input, r -> (input eq "") && (r eq "") }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Disabled("Generic functions are not supported yet") + @Test + fun `test use generic function`() { + val method = getMethod("useGenericFunction") + discoverProperties( + method = method, + { r -> r eq 126 }, // createArray(42, 3) -> length(3) * value(42) = 126 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Static class methods are not supported yet") + @Test + fun `test use static methods`() { + val method = getMethod("useStaticMethods") + discoverProperties( + method = method, + { r -> r eq 3 }, // reset(), increment() = 1, increment() = 2, return 1 + 2 = 3 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Class inheritance is not supported yet") + @Test + fun `test use inheritance`() { + val method = getMethod("useInheritance") + discoverProperties( + method = method, + { r -> r eq 50 }, // NumberProcessor.process(5) = 5 * 10 = 50 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test use module state`() { + val method = getMethod("useModuleState") + discoverProperties( + method = method, + { r -> r eq 100 }, // setModuleState(100), getModuleState() = 100 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Enum operations are not supported yet") + @Test + fun `test chained enum operations`() { + val method = getMethod("chainedEnumOperations") + discoverProperties( + method = method, + { r -> r eq 9 }, // colors.length(3) + numbers.reduce(1+2+3=6) = 3 + 6 = 9 + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Disabled("Interface patterns are not supported yet") + @Test + fun `test use interface pattern`() { + val method = getMethod("useInterfacePattern") + discoverProperties( + method = method, + { id, name, r -> (id eq 1) && (name eq "test") && (r eq "1-test") }, + { id, name, r -> (id eq 42) && (name eq "hello") && (r eq "42-hello") }, + { id, name, r -> (id eq 0) && (name eq "") && (r eq "0-") }, + invariants = arrayOf( + { _, _, _ -> true } + ) + ) + } + + @Disabled("Type aliases are not supported yet") + @Test + fun `test use type alias`() { + val method = getMethod("useTypeAlias") + discoverProperties( + method = method, + { count, active, r -> (count eq 10) && (active eq true) && (r eq 20) }, + { count, active, r -> (count eq 10) && (active eq false) && (r eq 10) }, + { count, active, r -> (count eq 5) && (active eq true) && (r eq 10) }, + invariants = arrayOf( + { _, _, _ -> true } + ) + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt index 5ed4d5d403..ce2d9a0ec4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/FieldAccess.kt @@ -130,14 +130,4 @@ class FieldAccess : TsMethodTestRunner() { { r -> r eq 1 }, ) } - - @Test - fun `test read from nested fake objects`() { - val method = getMethod("readFromNestedFakeObjects") - discoverProperties( - method = method, - { r -> r eq 1 }, - { r -> r eq 2 }, - ) - } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Globals.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Globals.kt new file mode 100644 index 0000000000..e67e13cf52 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Globals.kt @@ -0,0 +1,53 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.util.isNaN +import org.usvm.util.neq +import kotlin.test.Test + +class Globals : TsMethodTestRunner() { + private val tsPath = "/samples/lang/Globals.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `test getValue`() { + val method = getMethod("getValue") + discoverProperties( + method, + { r -> r eq 42 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } + + @Test + fun `test setValue`() { + val method = getMethod("setValue") + discoverProperties( + method, + { a, r -> a.isNaN() && r.isNaN() }, + { a, r -> (a eq 0) && (r eq 0) }, + { a, r -> !a.isNaN() && (a neq 0) && (a eq r) }, + invariants = arrayOf( + { _, _ -> true } + ) + ) + } + + @Test + fun `test useValue`() { + val method = getMethod("useValue") + discoverProperties( + method, + { r -> r eq 142 }, + invariants = arrayOf( + { _ -> true } + ) + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Assumptions.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Assumptions.kt new file mode 100644 index 0000000000..452fc09935 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Assumptions.kt @@ -0,0 +1,28 @@ +@file:OptIn(ExperimentalContracts::class) + +package org.usvm.util + +import org.junit.jupiter.api.Assumptions +import kotlin.contracts.ExperimentalContracts +import kotlin.contracts.contract + +fun abort(message: String = ""): Nothing { + Assumptions.abort(message) + error("Unreachable") +} + +fun assumeTrue(assumption: Boolean, message: String = "Assumption failed") { + contract { returns() implies assumption } + Assumptions.assumeTrue(assumption, message) +} + +fun assumeFalse(assumption: Boolean, message: String = "Assumption failed") { + contract { returns() implies !assumption } + Assumptions.assumeFalse(assumption, message) +} + +fun assumeNotNull(value: T?, message: String = "Value should not be null"): T { + contract { returns() implies (value != null) } + assumeTrue(value != null, message) + return value +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 08900f5358..78aaaa09cf 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -331,6 +331,24 @@ abstract class TsMethodTestRunner : TestRunner EtsUnknownType TsTestValue.TsNull::class -> EtsNullType + TsTestValue.TsException.StringException::class -> { + // TODO incorrect + val signature = EtsClassSignature("StringException", EtsFileSignature.UNKNOWN) + EtsClassType(signature) + } + + TsTestValue.TsException.ObjectException::class -> { + // TODO incorrect + val signature = EtsClassSignature("ObjectException", EtsFileSignature.UNKNOWN) + EtsClassType(signature) + } + + TsTestValue.TsException.UnknownException::class -> { + // TODO incorrect + val signature = EtsClassSignature("UnknownException", EtsFileSignature.UNKNOWN) + EtsClassType(signature) + } + TsTestValue.TsException::class -> { // TODO incorrect val signature = EtsClassSignature("Exception", EtsFileSignature.UNKNOWN) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 2caa3857bf..651b93eb34 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -47,7 +47,6 @@ import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory -import org.usvm.memory.URegisterStackLValue import org.usvm.mkSizeExpr import org.usvm.model.UModel import org.usvm.model.UModelBase @@ -117,13 +116,39 @@ class TsTestResolver { } } - @Suppress("unused") private fun resolveException( res: TsMethodResult.TsException, afterMemoryScope: MemoryScope, ): TsTestValue.TsException { - // TODO support exceptions - return TsTestValue.TsException + return afterMemoryScope.withMode(ResolveMode.CURRENT) { + try { + // Dispatch based on the exception type, similar to string const resolution + when (res.type) { + is EtsStringType -> { + val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef + if (concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) { + val stringValue = ctx.getStringConstantValue(concreteRef) + if (stringValue != null) { + TsTestValue.TsException.StringException(stringValue) + } else { + TsTestValue.TsException.UnknownException + } + } else { + TsTestValue.TsException.UnknownException + } + } + + else -> { + // Other types of exceptions - resolve and wrap the value + val resolvedValue = resolveExpr(res.value) + TsTestValue.TsException.ObjectException(resolvedValue) + } + } + } catch (_: Exception) { + // Fallback to unknown exception if resolution fails + TsTestValue.TsException.UnknownException + } + } } private class MemoryScope( @@ -307,9 +332,8 @@ open class TsTestStateResolver( return TsTestValue.TsString(value) } - fun resolveThisInstance(): TsTestValue? { - val parametersCount = method.parameters.size - val ref = mkRegisterStackLValue(ctx.addressSort, parametersCount) // TODO check for statics + fun resolveThisInstance(): TsTestValue { + val ref = mkRegisterStackLValue(ctx.addressSort, 0) // TODO check for statics return resolveLValue(ref) } @@ -320,12 +344,13 @@ open class TsTestStateResolver( if (sort is TsUnresolvedSort) { // this means that a fake object was created, and we need to read it from the current memory - val address = finalStateMemory.read(mkRegisterStackLValue(addressSort, idx)) + val ref = mkRegisterStackLValue(addressSort, idx) + val address = finalStateMemory.read(ref) check(address.isFakeObject()) return@mapIndexed resolveFakeObject(address) } - val ref = URegisterStackLValue(sort, idx) + val ref = mkRegisterStackLValue(sort, idx) resolveLValue(ref) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt index cde655cecc..a8b6b12321 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -1,6 +1,8 @@ package org.usvm.util import org.usvm.api.TsTestValue.TsNumber +import org.usvm.api.TsTestValue.TsString +import org.usvm.api.TsTestValue.TsBoolean import kotlin.math.absoluteValue fun Boolean.toDouble() = if (this) 1.0 else 0.0 @@ -40,3 +42,35 @@ infix fun TsNumber.neq(other: Int): Boolean { fun TsNumber.isNaN(): Boolean { return number.isNaN() } + +infix fun TsString.eq(other: String): Boolean { + return value == other +} + +infix fun TsString.neq(other: String): Boolean { + return value != other +} + +infix fun TsString.eq(other: TsString): Boolean { + return eq(other.value) +} + +infix fun TsString.neq(other: TsString): Boolean { + return neq(other.value) +} + +infix fun TsBoolean.eq(other: Boolean): Boolean { + return value == other +} + +infix fun TsBoolean.neq(other: Boolean): Boolean { + return value != other +} + +infix fun TsBoolean.eq(other: TsBoolean): Boolean { + return eq(other.value) +} + +infix fun TsBoolean.neq(other: TsBoolean): Boolean { + return neq(other.value) +} diff --git a/usvm-ts/src/test/resources/samples/imports/Imports.ts b/usvm-ts/src/test/resources/samples/imports/Imports.ts new file mode 100644 index 0000000000..11a0b3b281 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/imports/Imports.ts @@ -0,0 +1,226 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols,JSUnusedLocalSymbols + +import { + exportedNumber, + exportedString, + exportedBoolean, + exportedNull, + exportedUndefined, + exportedArray, + exportedObject, + exportedFloat, + exportedNegativeNumber, + exportedEmptyString, + exportedFunction, + ExportedClass, + exportedAsyncFunction, +} from './namedExports'; + +import defaultValue from './defaultExport'; + +import { + renamedValue as aliasedValue, + renamedString as aliasedString, + renamedBoolean as aliasedBoolean, + renamedArray as aliasedArray, + renamedObject as aliasedObject, + calculate as computeValue, + ExportedClass as RenamedClass, +} from './mixedExports'; + +import * as AllExports from './namedExports'; + +import { + reExportedNumber, +} from './mixedExports'; + +import { + CONSTANTS, + computedNumber, + configString, + Color, + NumberEnum, + processValue, + createArray, + Utility, + NumberProcessor, + getModuleState, + setModuleState, +} from './advancedExports'; + +class Imports { + getExportedNumber(): number { + return exportedNumber; + } + + getExportedString(): string { + return exportedString; + } + + getExportedBoolean(): boolean { + return exportedBoolean; + } + + getExportedNull(): null { + return exportedNull; + } + + getExportedUndefined(): undefined { + return exportedUndefined; + } + + getExportedArray(): number[] { + return exportedArray; + } + + getExportedObject(): object { + return exportedObject; + } + + getExportedFloat(): number { + return exportedFloat; + } + + getExportedNegativeNumber(): number { + return exportedNegativeNumber; + } + + getExportedEmptyString(): string { + return exportedEmptyString; + } + + getDefaultValue(): string { + return defaultValue; + } + + getRenamedValue(): number { + return aliasedValue; + } + + getRenamedString(): string { + return aliasedString; + } + + getRenamedBoolean(): boolean { + return aliasedBoolean; + } + + getRenamedArray(): number[] { + return aliasedArray; + } + + getRenamedObject(): object { + return aliasedObject; + } + + useNamespaceVariables(): number { + return AllExports.exportedNumber + AllExports.exportedFloat; + } + + useReExportedValues(): number { + return reExportedNumber; + } + + getComputedNumber(): number { + return computedNumber; + } + + getConfigString(): string { + return configString; + } + + useConstImports(): number { + return CONSTANTS.PI + CONSTANTS.MAX_SIZE + CONSTANTS.CONFIG.timeout; + } + + useDestructuring(): number { + const { exportedNumber: num, exportedBoolean: bool } = AllExports; + return bool ? num * 2 : num; + } + + combineVariables(): string { + return `${exportedString}-${aliasedString}-${configString}`; + } + + mathOperationsOnVariables(): number { + return exportedNumber + aliasedValue + computedNumber; + } + + useImportedFunction(input: number): number { + return exportedFunction(input); + } + + useImportedClass(value: number): number { + const instance = new ExportedClass(value); + return instance.multiply(3); + } + + useRenamedComplexImports(): number { + const result = computeValue(10); + const instance = new RenamedClass(); + return result + instance.value; + } + + useNamespaceComplexImport(value: number): number { + const instance = new AllExports.ExportedClass(value); + return AllExports.exportedFunction(instance.getValue()); + } + + async useAsyncImport(delay: number): Promise { + const result = await exportedAsyncFunction(delay); + return result + 5; + } + + useEnumImports(): string { + const color = Color.Red; + const num = NumberEnum.Second; + return `${color}-${num}`; + } + + useFunctionOverloadsNumber(input: number): number { + return processValue(input); + } + + useFunctionOverloadsString(input: string): string { + return processValue(input); + } + + useGenericFunction(): number { + const numbers = createArray(42, 3); + return numbers.length * numbers[0]; + } + + useStaticMethods(): number { + Utility.reset(); + const first = Utility.increment(); + const second = Utility.increment(); + return first + second; + } + + useInheritance(): number { + const processor = new NumberProcessor(); + return processor.process(5); + } + + useModuleState(): number { + setModuleState(100); + return getModuleState(); + } + + chainedEnumOperations(): number { + const colors = [Color.Red, Color.Green, Color.Blue]; + const numbers = [NumberEnum.First, NumberEnum.Second, NumberEnum.Third]; + return colors.length + numbers.reduce((sum, num) => sum + num, 0); + } + + useInterfacePattern(id: number, name: string): string { + const obj = { id: id, name: name }; + return `${obj.id}-${obj.name}`; + } + + useTypeAlias(count: number, active: boolean): number { + const obj = { count: count, active: active }; + return active ? obj.count * 2 : obj.count; + } +} diff --git a/usvm-ts/src/test/resources/samples/imports/advancedExports.ts b/usvm-ts/src/test/resources/samples/imports/advancedExports.ts new file mode 100644 index 0000000000..086f766f13 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/imports/advancedExports.ts @@ -0,0 +1,96 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Const object with nested values +export const CONSTANTS = { + PI: 3.14159, + MAX_SIZE: 100, + CONFIG: { + timeout: 5000, + retries: 3, + }, +} // as const; + +// Computed variable exports +export const computedNumber = CONSTANTS.PI * CONSTANTS.MAX_SIZE; +export const configString = `timeout:${CONSTANTS.CONFIG.timeout}ms`; + +// Enum definitions +export enum Color { + Red = "red", + Green = "green", + Blue = "blue" +} + +export enum NumberEnum { + First = 1, + Second = 2, + Third = 3 +} + +// Function overloads +export function processValue(value: number): number; +export function processValue(value: string): string; +export function processValue(value: number | string): number | string { + if (typeof value === "number") { + return value * 2; + } + return value.toUpperCase(); +} + +// Generic function +export function createArray(item: T, count: number): T[] { + return new Array(count).fill(item); +} + +// Class with static methods +export class Utility { + static readonly VERSION = "1.0.0"; + static counter = 0; + + static increment(): number { + return ++this.counter; + } + + static reset(): void { + this.counter = 0; + } + + static getInfo(): string { + return `Utility v${this.VERSION}, counter: ${this.counter}`; + } +} + +// Inheritance classes +export class BaseProcessor { + protected name: string; + + constructor(name: string) { + this.name = name; + } + + process(data: any): string { + return `${this.name}: ${data}`; + } +} + +export class NumberProcessor extends BaseProcessor { + constructor() { + super("NumberProcessor"); + } + + process(data: number): number { + return data * 10; + } +} + +// Module state functions +let moduleState = 0; + +export function getModuleState(): number { + return moduleState; +} + +export function setModuleState(value: number): void { + moduleState = value; +} diff --git a/usvm-ts/src/test/resources/samples/imports/defaultExport.ts b/usvm-ts/src/test/resources/samples/imports/defaultExport.ts new file mode 100644 index 0000000000..ff0965a7c7 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/imports/defaultExport.ts @@ -0,0 +1,6 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Default value export +const defaultValue = "default-string"; +export default defaultValue; diff --git a/usvm-ts/src/test/resources/samples/imports/mixedExports.ts b/usvm-ts/src/test/resources/samples/imports/mixedExports.ts new file mode 100644 index 0000000000..ac3749f20a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/imports/mixedExports.ts @@ -0,0 +1,40 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Internal variables for export +const internalValue = 100; +const internalString = "mixed"; +const internalBoolean = true; +const internalArray = [10, 20, 30]; +const internalObject = { count: 5, active: true }; + +// Internal complex symbols +function internalFunction(x: number): number { + return x + internalValue; +} + +class InternalClass { + value: number = 50; +} + +// Renamed exports of variables +export { + internalValue as renamedValue, + internalString as renamedString, + internalBoolean as renamedBoolean, + internalArray as renamedArray, + internalObject as renamedObject, +}; + +// Renamed exports of complex symbols +export { internalFunction as calculate }; +export { InternalClass as ExportedClass }; + +// Re-exports from other modules +export { + exportedNumber as reExportedNumber, + exportedString as reExportedString, +} from './namedExports'; + +// Namespace re-export +export * as AllFromDefault from './defaultExport'; diff --git a/usvm-ts/src/test/resources/samples/imports/namedExports.ts b/usvm-ts/src/test/resources/samples/imports/namedExports.ts new file mode 100644 index 0000000000..db90e61a3a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/imports/namedExports.ts @@ -0,0 +1,54 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Variable exports +export const exportedNumber: number = 123; +export const exportedString: string = "hello"; +export const exportedBoolean: boolean = true; +export const exportedFloat: number = 3.14159; +export const exportedNull = null; +export const exportedUndefined = undefined; +export const exportedArray = [1, 2, 3]; +export const exportedObject = { id: 100, name: "test" }; +export const exportedNegativeNumber: number = -456; +export const exportedEmptyString: string = ""; + +// Function export +export function exportedFunction(x: number): number { + return x * 2; +} + +// Class export +export class ExportedClass { + private readonly value: number; + + constructor(value: number) { + this.value = value; + } + + getValue(): number { + return this.value; + } + + multiply(factor: number): number { + return this.value * factor; + } +} + +// Type definitions +export interface ExportedInterface { + id: number; + name: string; +} + +export type ExportedType = { + count: number; + active: boolean; +}; + +// Async function export +export async function exportedAsyncFunction(delay: number): Promise { + return new Promise((resolve) => { + setTimeout(() => resolve(delay * 10), 1); + }); +} diff --git a/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts b/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts index fdb1b86dc0..1b4b9f008d 100644 --- a/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts +++ b/usvm-ts/src/test/resources/samples/lang/FieldAccess.ts @@ -77,16 +77,6 @@ class FieldAccess { return obj.x.length; } - readFromNestedFakeObjects(): number { - let x = Foo.Bar.x; - let y = Foo.Bar.y; - if (x === undefined && y === undefined) { - return 1; - } else { - return 2; - } - } - private createObject(): { x: number } { return { x: 42 }; } diff --git a/usvm-ts/src/test/resources/samples/lang/Globals.ts b/usvm-ts/src/test/resources/samples/lang/Globals.ts new file mode 100644 index 0000000000..2bd0e06c17 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/Globals.ts @@ -0,0 +1,21 @@ +let myValue = 42; + +class Globals { + getValue(): number { + return myValue; + } + + setValue(value: number): number { + myValue = value; + if (value != value) return myValue; + if (value == 0) return myValue; + return myValue; + } + + useValue(): number { + const x = this.getValue(); // 42 + this.setValue(100); + const y = this.getValue(); // 100 + return x + y; // 42 + 100 = 142 + } +}