Skip to content

Conversation

@Lipen
Copy link
Member

@Lipen Lipen commented Jun 20, 2025

This PR adds support for strings in TS machine.

@Lipen Lipen requested a review from Copilot June 20, 2025 09:20

if (expr.callee.name == "toString") {
return mkFp64(ADHOC_STRING)
return TODO()

Check warning

Code scanning / detekt

Unreachable code detected. This code should be removed. Warning

This expression is unreachable code which should either be used or removed.
)
)
}
val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type))

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.
state.pathConstraints += mkNot(mkHeapRefEq(thisRef, mkUndefinedValue()))

// TODO not equal but subtype for abstract/interfaces
state.pathConstraints += state.memory.types.evalTypeEquals(thisRef, method.enclosingClass!!.type)

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull Request Overview

Adds support for JavaScript string values in the TS machine, including type‐system, interpreter, context, and test updates.

  • Introduces heap‐allocated string constants and updates typeof handling to return proper string sorts.
  • Extends TsTypeSystem and TsInterpreter to recognize EtsStringType, and adds sample/tests for string behavior.
  • Refactors existing samples and code (strict equality, variable renames, commented‐out heuristics) for consistency.

Reviewed Changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 2 comments.

Show a summary per file
File Description
usvm-ts/src/test/resources/samples/types/StructuralEquality.ts Renamed locals and added lint suppression
usvm-ts/src/test/resources/samples/types/ObjectUsage.ts Changed parameter type to {} and used strict ===
usvm-ts/src/test/resources/samples/arrays/InputArrays.ts Switched == to === for undefined checks
usvm-ts/src/test/resources/samples/Strings.ts New sample class covering typeof on all JS basic values
usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt Added EtsStringType resolution, new helper import
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt Removed placeholder mapping for TsObject
usvm-ts/src/test/kotlin/org/usvm/util/Truthy.kt Deleted obsolete isTruthy for TsObject
usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt Updated property‐based testing for objectAsParameter
usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt Adjusted generics and exception handling in array tests
usvm-ts/src/test/kotlin/org/usvm/samples/Strings.kt Added full suite of Kotlin tests for Strings sample
usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt Refactored generics and removed null/undefined branch tests
usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt Included EtsStringType in object class type branches
usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt Refactored context usage, added string param constraints
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt Replaced magic‐number heuristics with mkStringConstant
usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt Implemented mkStringConstant to allocate string objects
usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt Removed TsObject from the sealed interface
Comments suppressed due to low confidence (6)

usvm-ts/src/test/resources/samples/types/StructuralEquality.ts:46

  • [nitpick] The variable name x is not descriptive. Consider renaming it to obj or instance to clarify its purpose.
        const x: A = new B(11);

usvm-ts/src/test/resources/samples/types/ObjectUsage.ts:5

  • [nitpick] The parameter name x is ambiguous. Consider renaming it to obj or inputObj for clarity.
    objectAsParameter(x: {}): number {

usvm-ts/src/test/kotlin/org/usvm/samples/types/ObjectUsage.kt:18

  • The test no longer asserts the undefined input path yields -1. Consider adding an explicit branch to cover x == undefined returning -1.0.
            { x, r -> r.number == 42.0 },

usvm-ts/src/test/kotlin/org/usvm/samples/InstanceFields.kt:17

  • The tests removed the branch covering undefined or null inputs producing exceptions. To maintain full coverage, reintroduce that case.
        discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt:38

  • The import isAllocated is never used in this file. You can remove it to keep imports tidy.
import org.usvm.isAllocated

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt:46

  • The import TsInterpreter is not referenced in this file. Consider removing it to avoid unused imports.
import org.usvm.machine.interpreter.TsInterpreter

@Lipen Lipen merged commit c9d843a into main Jun 20, 2025
6 checks passed
@Lipen Lipen deleted the lipen/strings branch June 20, 2025 10:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants