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 6 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
6 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
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