[TS] Materialize symbolic string input witnesses

[CaelmBleidd]

Summary

• Materialize symbolic string references from their modeled UTF-16 backing array instead of emitting placeholder text.

• Store string code units in a private array-memory region so mutation of a user array cannot change a string's length, even if internal references alias.

• Carry the configured TsOptions.maxArraySize through the symbolic state into test extraction, so exploration and extraction use the same string length bound.

• Cover empty and nonempty symbolic inputs, array isolation, the configured 10,001-character boundary, and a literal containing NUL, non-ASCII text, and a surrogate pair. Replay every generated witness in Node.js.

• Reject symbolic string witnesses whose backing array is missing with a typed test-resolution error; a source-level any input previously produced a false empty-string witness for the length-one branch.

Verification

./gradlew :usvm-ts:test --tests org.usvm.machine.TsSymbolicStringInputTest --tests org.usvm.samples.operators.TypeOf --tests org.usvm.samples.lang.Arg --tests org.usvm.machine.call.TsArrayShiftReplayTest --tests org.usvm.machine.call.TsInstanceCallReceiverTest :usvm-ts:detektMain :usvm-ts:detektTest --offline --console=plain

158 selected tests: 156 passed, 2 skipped, 0 failed. Both Detekt tasks passed with 0 code smells, and git diff --check passed. The new source-level regression failed against the previous head because it emitted "" for the length-one branch; it now observes a typed unsupported witness error and replays both real string outcomes in Node.js. The original alias and 10,001-character probes also passed.

• Independent core correctness and AI code hygiene reviews of head 5b866c7f found no actionable defects.
• CI run 37096099269 passed all seven reported jobs on this head.

Closes #421

[github-advanced-security]

detekt found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.