Skip to content

Concolic for TypeScript #341

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Draft
CaelmBleidd wants to merge 21 commits into
base: main
Choose a base branch
from
Draft

Concolic for TypeScript #341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
d732601
[TS] Support input type hints and promote TsTestResolver to main sources
CaelmBleidd Jul 5, 2026
8d49b19
[TS] Add usvm-ts-pbt: hybrid PBT + targeted symbolic execution prototype
CaelmBleidd Jul 5, 2026
2741f34
[TS] Add research notes for the hybrid PBT + symbolic execution effort
CaelmBleidd Jul 5, 2026
f43c77a
[TS] Whitelist Less.lessUnknown in the differential suite
CaelmBleidd Jul 5, 2026
1db59c3
[TS] Fix CI for the usvm-ts-pbt module
CaelmBleidd Jul 5, 2026
fa39061
[TS] Support the jacodb native TS parser (jacodb#361) in usvm-ts-pbt
CaelmBleidd Jul 6, 2026
e19de97
[TS] Benchmark harness over open-source TypeScript corpora
CaelmBleidd Jul 6, 2026
41f0565
[TS] Extend the concrete interpreter: functions, HOFs, Map/Set, ptr_call
CaelmBleidd Jul 6, 2026
b1b910e
[TS] One-command measurement pipeline for open-source TS projects
CaelmBleidd Jul 6, 2026
14319b1
[TS] Add the module README and the project-state handoff document
CaelmBleidd Jul 8, 2026
03b571c
[TS] Project state: engine-fixes progress, resolution-frequency data …
CaelmBleidd Jul 10, 2026
d1bd513
[TS] Load the corpus into one project scene by default
CaelmBleidd Jul 10, 2026
69a0aec
[TS] Project state: project-scene loading done, refreshed residual-un…
CaelmBleidd Jul 10, 2026
20e4386
[TS] Make symbolic-input replay robust to partially resolvable objects
CaelmBleidd Jul 10, 2026
668cfaf
[TS] Project state: replay-robustness progress and residual divergenc…
CaelmBleidd Jul 10, 2026
97ae9c5
[TS] Resolver: guard cyclic object graphs; look fake objects up by bo…
CaelmBleidd Jul 10, 2026
7733c2e
[TS] Align the truthiness-idiom contract: ToBoolean for all operand k…
CaelmBleidd Jul 10, 2026
dc95536
[TS] Project state: truthiness idiom and Array constructor done
CaelmBleidd Jul 10, 2026
42cfeb5
[TS] Generators produce real functions and containers; new intrinsics…
CaelmBleidd Jul 10, 2026
26b2507
[TS] Prefer class definitions over phantom import declarations; riche…
CaelmBleidd Jul 10, 2026
7bccca7
[TS] Project state: frontend feedback items from the generator/resolv…
CaelmBleidd Jul 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,10 +149,16 @@ jobs:
cd $DEST_DIR

npm install
# Transitively hoisted @types/node >= 24 uses TypeScript syntax that the
# ArkAnalyzer toolchain cannot parse; pin a compatible version. Both
# --no-save packages must be installed in one command: each `npm install`
# re-resolves the tree and drops previous --no-save additions
# (ohos-typescript is installed --no-save by the postinstall script).
npm install --no-save @types/node@22 arktools/lib/ohos-typescript-4.9.5-r4-OpenHarmony-v5.0.0-Release.tgz
npm run build

- name: Run TS tests
run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check
run: ./gradlew :usvm-ts:check :usvm-ts-dataflow:check :usvm-ts-pbt:check

- name: Upload Gradle reports
if: (!cancelled())
Expand Down
1 change: 1 addition & 0 deletions build.gradle.kts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ tasks.register("validateProjectList") {
project(":usvm-python"),
project(":usvm-ts"),
project(":usvm-ts-dataflow"),
project(":usvm-ts-pbt"),
)

// Gather the actual subprojects from the current root project.
Expand Down
87 changes: 87 additions & 0 deletions detekt/baselines/usvm-ts-pbt-Main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
<?xml version="1.0" ?>
<SmellBaseline>
<ManuallySuppressedIssues></ManuallySuppressedIssues>
<CurrentIssues>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}")</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame)))</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(left, frame))</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(eval(right, frame))</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(left, frame)</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(op(JsSemantics.toInt32(eval(left, frame)), JsSemantics.toInt32(eval(right, frame))).toDouble())</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(right, frame)</ID>
<ID>ArgumentListWrapping:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$(target)</ID>
<ID>BracesOnWhenStatements:ConstantMiner.kt$MinedConstants.Companion$when</ID>
<ID>BracesOnWhenStatements:Conversions.kt$when</ID>
<ID>BracesOnWhenStatements:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$when</ID>
<ID>BracesOnWhenStatements:Generators.kt$InputGenerator$when</ID>
<ID>BracesOnWhenStatements:Intrinsics.kt$Intrinsics$when</ID>
<ID>BracesOnWhenStatements:JsSemantics.kt$JsSemantics$when</ID>
<ID>BracesOnWhenStatements:Main.kt$when</ID>
<ID>BracesOnWhenStatements:PbtPhase.kt$PbtPhase$when</ID>
<ID>EmptyFunctionBlock:CoverageTracker.kt$CoverageTracker${}</ID>
<ID>Filename:ConstantMiner.kt$org.usvm.ts.pbt.gen.ConstantMiner.kt</ID>
<ID>Filename:Generators.kt$org.usvm.ts.pbt.gen.Generators.kt</ID>
<ID>ForbiddenMethodCall:Main.kt$println( " ${m.method}: stmt=%.1f%%, branch=%.1f%% (pbt: %s, symbolic: %s), %d ms".format( m.stmtCoverage * 100, m.branchCoverage * 100, m.pbt?.let { "${it.executions} runs, ${it.failures.size} failures" } ?: "-", m.symbolic?.let { "${it.reached}/${it.targets.size} targets" } ?: "-", m.totalWallMs, ) )</ID>
<ID>ForbiddenMethodCall:Main.kt$println("Analyzing ${methods.size} method(s) in mode $mode...")</ID>
<ID>ForbiddenMethodCall:Main.kt$println("Loading ${files.size} file(s) via ArkAnalyzer...")</ID>
<ID>ForbiddenMethodCall:Main.kt$println("Report written to $out")</ID>
<ID>ForbiddenMethodCall:Main.kt$println("Unknown option: ${args[i]}\n$USAGE")</ID>
<ID>ForbiddenMethodCall:Main.kt$println(USAGE)</ID>
<ID>LoopWithTooManyJumpStatements:PbtPhase.kt$PbtPhase$while</ID>
<ID>MagicNumber:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$31</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$0.0</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$0.6</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$10</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$100</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$1000</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$1001</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$101</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$11</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$1e6</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$3</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$4</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$5</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$6</ID>
<ID>MagicNumber:Generators.kt$InputGenerator$8</ID>
<ID>MagicNumber:Intrinsics.kt$Intrinsics$9007199254740991.0</ID>
<ID>MagicNumber:JsSemantics.kt$JsSemantics$0xFFFFFFFFL</ID>
<ID>MagicNumber:JsSemantics.kt$JsSemantics$16</ID>
<ID>MagicNumber:JsSemantics.kt$JsSemantics$1e21</ID>
<ID>MagicNumber:JsSemantics.kt$JsSemantics$8</ID>
<ID>MagicNumber:JsSemantics.kt$JsSemantics$9.007199254740992E15</ID>
<ID>MagicNumber:Main.kt$100</ID>
<ID>MagicNumber:Main.kt$20</ID>
<ID>MagicNumber:Main.kt$2_000</ID>
<ID>MagicNumber:PbtPhase.kt$PbtPhase$100</ID>
<ID>MagicNumber:SymbolicPhase.kt$SymbolicPhase$1_000_000</ID>
<ID>MatchingDeclarationName:ConstantMiner.kt$MinedConstants</ID>
<ID>MatchingDeclarationName:Generators.kt$InputGenerator</ID>
<ID>MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$)</ID>
<ID>MaxLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw typeError("cannot set property '${lhv.field.name}' of ${JsSemantics.toStringJs(target)}")</ID>
<ID>MaximumLineLength:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$ </ID>
<ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VNamespace(e.name)</ID>
<ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VString(array.value[i.toInt()].toString())</ID>
<ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$VUndefined</ID>
<ID>MultiLineIfElse:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$throw UnsupportedFeatureSignal("global ref: ${e.name}")</ID>
<ID>MultiLineIfElse:Generators.kt$InputGenerator$genAny(depth)</ID>
<ID>MultiLineIfElse:Generators.kt$InputGenerator$generate(type.types[random.nextInt(type.types.size)], depth)</ID>
<ID>MultiLineIfElse:Generators.kt$InputGenerator$random.nextDouble(-1e6, 1e6)</ID>
<ID>MultiLineIfElse:Generators.kt$InputGenerator$random.nextInt(-100, 101) + random.nextDouble()</ID>
<ID>MultiLineIfElse:JsSemantics.kt$JsSemantics$d.toLong().toString()</ID>
<ID>MultiLineIfElse:JsSemantics.kt$JsSemantics$java.math.BigDecimal(d).toBigInteger().toString()</ID>
<ID>MultiLineIfElse:PbtPhase.kt$PbtPhase$args</ID>
<ID>NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List&lt;VValue&gt;): VValue</ID>
<ID>NestedBlockDepth:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame)</ID>
<ID>NestedBlockDepth:Shrinker.kt$Shrinker$fun shrink(args: List&lt;VValue&gt;, stillFails: (List&lt;VValue&gt;) -&gt; Boolean): List&lt;VValue&gt;</ID>
<ID>NoMultipleSpaces:Generators.kt$InputGenerator$ </ID>
<ID>SwallowedException:EtsConcreteInterpreter.kt$EtsConcreteInterpreter$e: StackOverflowError</ID>
<ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun evalCall(expr: EtsCallExpr, frame: Frame): VValue</ID>
<ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$fun runMethod(method: EtsMethod, thisValue: VValue, args: List&lt;VValue&gt;): VValue</ID>
<ID>ThrowsCount:EtsConcreteInterpreter.kt$EtsConcreteInterpreter.Execution$private fun assign(lhv: EtsLValue, value: VValue, frame: Frame)</ID>
<ID>TooGenericExceptionCaught:SymbolicPhase.kt$SymbolicPhase$e: Throwable</ID>
<ID>UnderscoresInNumericLiterals:Intrinsics.kt$Intrinsics$9007199254740991.0</ID>
<ID>Wrapping:Generators.kt$InputGenerator$;</ID>
<ID>Wrapping:Intrinsics.kt$Intrinsics$(</ID>
<ID>Wrapping:Intrinsics.kt$Intrinsics$;</ID>
</CurrentIssues>
</SmellBaseline>
27 changes: 27 additions & 0 deletions detekt/baselines/usvm-ts-pbt-Test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
<?xml version="1.0" ?>
<SmellBaseline>
<ManuallySuppressedIssues></ManuallySuppressedIssues>
<CurrentIssues>
<ID>ArgumentListWrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
<ID>ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = hints, hintFallback = false, )</ID>
<ID>ArgumentListWrapping:HybridE2eTest.kt$HybridE2eTest$( scene, m, coverage, hints = pbt.typeProfiler.toHints(), )</ID>
<ID>BracesOnWhenStatements:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$when</ID>
<ID>CommentSpacing:LoadEts.kt$//-----------------------------------------------------------------------------</ID>
<ID>ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println(" MISMATCH: $it")</ID>
<ID>ForbiddenMethodCall:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
<ID>ForbiddenMethodCall:HybridE2eTest.kt$HybridE2eTest$println( "[ablation] with hints: steps=${withHints.steps}, reached=${withHints.reached}, " + "wallMs=${withHints.wallMs}; without: steps=${withoutHints.steps}, " + "reached=${withoutHints.reached}, wallMs=${withoutHints.wallMs}" )</ID>
<ID>ImportOrdering:ConcreteInterpreterDslTest.kt$import org.jacodb.ets.dsl.add import org.jacodb.ets.dsl.and import org.jacodb.ets.dsl.const import org.jacodb.ets.dsl.eqq import org.jacodb.ets.dsl.gt import org.jacodb.ets.dsl.local import org.jacodb.ets.dsl.lt import org.jacodb.ets.dsl.mul import org.jacodb.ets.dsl.neg import org.jacodb.ets.dsl.param import org.jacodb.ets.dsl.program import org.jacodb.ets.dsl.sub import org.jacodb.ets.dsl.toBlockCfg import org.jacodb.ets.dsl.ProgramBuilder import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.toEtsBlockCfg import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test</ID>
<ID>MaxLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$println("[$className] compared=${verdict.compared}, skipped=${verdict.skipped}, mismatches=${verdict.mismatches.size}")</ID>
<ID>MaximumLineLength:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$ </ID>
<ID>MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$compared++</ID>
<ID>MultiLineIfElse:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$mismatches += "$ctx: concrete threw ${result.value}, symbolic returned ${test.returnValue}"</ID>
<ID>NestedBlockDepth:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$private fun runDifferential(resourcePath: String, className: String): Verdict</ID>
<ID>NoMultipleSpaces:JsSemanticsTest.kt$JsSemanticsTest$ </ID>
<ID>SwallowedException:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$e: Throwable</ID>
<ID>UnderscoresInNumericLiterals:HybridE2eTest.kt$HybridE2eTest$49382.0</ID>
<ID>UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295.0</ID>
<ID>UnderscoresInNumericLiterals:JsSemanticsTest.kt$JsSemanticsTest$4294967295L</ID>
<ID>Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$(</ID>
<ID>Wrapping:ConcreteVsSymbolicDifferentialTest.kt$ConcreteVsSymbolicDifferentialTest$;</ID>
</CurrentIssues>
</SmellBaseline>
Loading
Loading