Skip to content

Commit c72b120

Browse files
authored
Refine TS internals (#275)
1 parent 9f65a6e commit c72b120

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+1097
-717
lines changed

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/graph/ApplicationGraph.kt

+1-7
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,9 @@
11
package org.usvm.dataflow.graph
22

3-
import org.jacodb.api.common.CommonMethod
4-
import org.jacodb.api.common.cfg.CommonInst
5-
63
/**
74
* Provides both CFG and call graph (i.e., the supergraph in terms of RHS95 paper).
85
*/
9-
interface ApplicationGraph<Method, Statement>
10-
where Method : CommonMethod,
11-
Statement : CommonInst {
12-
6+
interface ApplicationGraph<Method, Statement> {
137
fun predecessors(node: Statement): Sequence<Statement>
148
fun successors(node: Statement): Sequence<Statement>
159

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/graph/BackwardGraphs.kt

+1-9
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,9 @@
1818

1919
package org.usvm.dataflow.graph
2020

21-
import org.jacodb.api.common.CommonMethod
22-
import org.jacodb.api.common.cfg.CommonInst
23-
2421
private class BackwardApplicationGraphImpl<Method, Statement>(
2522
val forward: ApplicationGraph<Method, Statement>,
26-
) : ApplicationGraph<Method, Statement>
27-
where Method : CommonMethod,
28-
Statement : CommonInst {
29-
23+
) : ApplicationGraph<Method, Statement> {
3024
override fun predecessors(node: Statement) = forward.successors(node)
3125
override fun successors(node: Statement) = forward.predecessors(node)
3226

@@ -40,8 +34,6 @@ private class BackwardApplicationGraphImpl<Method, Statement>(
4034
}
4135

4236
val <Method, Statement> ApplicationGraph<Method, Statement>.reversed: ApplicationGraph<Method, Statement>
43-
where Method : CommonMethod,
44-
Statement : CommonInst
4537
get() = when (this) {
4638
is BackwardApplicationGraphImpl -> this.forward
4739
else -> BackwardApplicationGraphImpl(this)

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt

+10-26
Original file line numberDiff line numberDiff line change
@@ -17,17 +17,12 @@
1717
package org.usvm.dataflow.ts.infer.dto
1818

1919
import org.jacodb.ets.dto.ArrayRefDto
20-
import org.jacodb.ets.dto.BooleanTypeDto
2120
import org.jacodb.ets.dto.ConstantDto
2221
import org.jacodb.ets.dto.InstanceFieldRefDto
2322
import org.jacodb.ets.dto.LocalDto
24-
import org.jacodb.ets.dto.NullTypeDto
25-
import org.jacodb.ets.dto.NumberTypeDto
2623
import org.jacodb.ets.dto.ParameterRefDto
2724
import org.jacodb.ets.dto.StaticFieldRefDto
28-
import org.jacodb.ets.dto.StringTypeDto
2925
import org.jacodb.ets.dto.ThisRefDto
30-
import org.jacodb.ets.dto.UndefinedTypeDto
3126
import org.jacodb.ets.dto.ValueDto
3227
import org.jacodb.ets.model.EtsArrayAccess
3328
import org.jacodb.ets.model.EtsBooleanConstant
@@ -53,46 +48,35 @@ private object EtsValueToDto : EtsValue.Visitor<ValueDto> {
5348
)
5449
}
5550

56-
override fun visit(value: EtsConstant): ValueDto {
51+
private fun visitConstant(value: EtsConstant): ValueDto {
5752
return ConstantDto(
5853
value = value.toString(),
5954
type = value.type.toDto(),
6055
)
6156
}
6257

58+
override fun visit(value: EtsConstant): ValueDto {
59+
return visitConstant(value)
60+
}
61+
6362
override fun visit(value: EtsStringConstant): ValueDto {
64-
return ConstantDto(
65-
value = value.value,
66-
type = StringTypeDto,
67-
)
63+
return visitConstant(value)
6864
}
6965

7066
override fun visit(value: EtsBooleanConstant): ValueDto {
71-
return ConstantDto(
72-
value = value.value.toString(),
73-
type = BooleanTypeDto,
74-
)
67+
return visitConstant(value)
7568
}
7669

7770
override fun visit(value: EtsNumberConstant): ValueDto {
78-
return ConstantDto(
79-
value = value.value.toString(),
80-
type = NumberTypeDto,
81-
)
71+
return visitConstant(value)
8272
}
8373

8474
override fun visit(value: EtsNullConstant): ValueDto {
85-
return ConstantDto(
86-
value = "null",
87-
type = NullTypeDto,
88-
)
75+
return visitConstant(value)
8976
}
9077

9178
override fun visit(value: EtsUndefinedConstant): ValueDto {
92-
return ConstantDto(
93-
value = "undefined",
94-
type = UndefinedTypeDto,
95-
)
79+
return visitConstant(value)
9680
}
9781

9882
override fun visit(value: EtsThis): ValueDto {

usvm-ts/.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
src/test/resources/sdk

usvm-ts/build.gradle.kts

+141
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,11 @@
1+
import kotlinx.coroutines.CoroutineScope
2+
import kotlinx.coroutines.Dispatchers
3+
import kotlinx.coroutines.launch
4+
import kotlinx.coroutines.runBlocking
5+
import java.io.FileNotFoundException
6+
import java.io.Reader
7+
import kotlin.time.Duration
8+
19
plugins {
210
id("usvm.kotlin-conventions")
311
}
@@ -22,3 +30,136 @@ dependencies {
2230
// Use it to export all modules to all
2331
testImplementation("org.burningwave:core:12.62.7")
2432
}
33+
34+
val generateSdkIR by tasks.registering {
35+
group = "build"
36+
description = "Generates SDK IR using ArkAnalyzer."
37+
doLast {
38+
val envVarName = "ARKANALYZER_DIR"
39+
40+
val arkAnalyzerPath = System.getenv(envVarName) ?: run {
41+
error("Please, set $envVarName environment variable.")
42+
}
43+
val arkAnalyzerDir = rootDir.resolve(arkAnalyzerPath)
44+
45+
val scriptSubPath = "src/save/serializeArkIR"
46+
val script = arkAnalyzerDir.resolve("out").resolve("$scriptSubPath.js")
47+
if (!script.exists()) {
48+
throw FileNotFoundException("Script file not found: '$script'. Did you forget to execute 'npm run build' in the ArkAnalyzer folder?")
49+
}
50+
51+
val resources = projectDir.resolve("src/test/resources")
52+
val prefix = "sdk/ohos/"
53+
val inputDir = resources.resolve("${prefix}ets")
54+
val outputDir = resources.resolve("${prefix}etsir")
55+
println("Generating SDK IR into '${outputDir.relativeTo(projectDir)}'...")
56+
57+
// cd src/test/resources
58+
// cd sdk/ohos/5.0.1.111
59+
// npx ts-node .../serializeArkIR.ts -v -p ets etsir
60+
61+
val cmd: List<String> = listOf(
62+
"node",
63+
script.absolutePath,
64+
"-v",
65+
"-p",
66+
inputDir.relativeTo(resources).path,
67+
outputDir.relativeTo(resources).path,
68+
)
69+
println("Running: '${cmd.joinToString(" ")}'")
70+
val result = ProcessUtil.run(cmd) {
71+
directory(resources)
72+
}
73+
if (result.stdout.isNotBlank()) {
74+
println("[STDOUT]:\n--------\n${result.stdout}\n--------")
75+
}
76+
if (result.stderr.isNotBlank()) {
77+
println("[STDERR]:\n--------\n${result.stderr}\n--------")
78+
}
79+
if (result.isTimeout) {
80+
println("Timeout!")
81+
}
82+
if (result.exitCode != 0) {
83+
println("Exit code: ${result.exitCode}")
84+
}
85+
}
86+
}
87+
88+
object ProcessUtil {
89+
data class Result(
90+
val exitCode: Int,
91+
val stdout: String,
92+
val stderr: String,
93+
val isTimeout: Boolean, // true if the process was terminated due to timeout
94+
)
95+
96+
fun run(
97+
command: List<String>,
98+
input: String? = null,
99+
timeout: Duration? = null,
100+
builder: ProcessBuilder.() -> Unit = {},
101+
): Result {
102+
val reader = input?.reader() ?: "".reader()
103+
return run(command, reader, timeout, builder)
104+
}
105+
106+
fun run(
107+
command: List<String>,
108+
input: Reader,
109+
timeout: Duration? = null,
110+
builder: ProcessBuilder.() -> Unit = {},
111+
): Result {
112+
val process = ProcessBuilder(command).apply(builder).start()
113+
return communicate(process, input, timeout)
114+
}
115+
116+
private fun communicate(
117+
process: Process,
118+
input: Reader,
119+
timeout: Duration? = null,
120+
): Result {
121+
val stdout = StringBuilder()
122+
val stderr = StringBuilder()
123+
124+
val scope = CoroutineScope(Dispatchers.IO)
125+
126+
// Handle process input
127+
val stdinJob = scope.launch {
128+
process.outputStream.bufferedWriter().use { writer ->
129+
input.copyTo(writer)
130+
}
131+
}
132+
133+
// Launch output capture coroutines
134+
val stdoutJob = scope.launch {
135+
process.inputStream.bufferedReader().useLines { lines ->
136+
lines.forEach { stdout.appendLine(it) }
137+
}
138+
}
139+
val stderrJob = scope.launch {
140+
process.errorStream.bufferedReader().useLines { lines ->
141+
lines.forEach { stderr.appendLine(it) }
142+
}
143+
}
144+
145+
// Wait for completion
146+
val isTimeout = if (timeout != null) {
147+
!process.waitFor(timeout.inWholeNanoseconds, TimeUnit.NANOSECONDS)
148+
} else {
149+
process.waitFor()
150+
false
151+
}
152+
runBlocking {
153+
stdinJob.join()
154+
stdoutJob.join()
155+
stderrJob.join()
156+
}
157+
158+
return Result(
159+
exitCode = process.exitValue(),
160+
stdout = stdout.toString(),
161+
stderr = stderr.toString(),
162+
isTimeout = isTimeout,
163+
)
164+
}
165+
}

usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

+19-19
Original file line numberDiff line numberDiff line change
@@ -9,34 +9,34 @@ data class TsTest(
99
val method: EtsMethod,
1010
val before: TsParametersState,
1111
val after: TsParametersState,
12-
val returnValue: TsValue,
12+
val returnValue: TsTestValue,
1313
val trace: List<EtsStmt>? = null,
1414
)
1515

1616
data class TsParametersState(
17-
val thisInstance: TsValue?,
18-
val parameters: List<TsValue>,
17+
val thisInstance: TsTestValue?,
18+
val parameters: List<TsTestValue>,
1919
val globals: Map<EtsClass, List<GlobalFieldValue>>,
2020
)
2121

22-
data class GlobalFieldValue(val field: EtsField, val value: TsValue) // TODO is it right?????
22+
data class GlobalFieldValue(val field: EtsField, val value: TsTestValue) // TODO is it right?????
2323

2424
open class TsMethodCoverage
2525

2626
object NoCoverage : TsMethodCoverage()
2727

28-
sealed interface TsValue {
29-
data object TsAny : TsValue
30-
data object TsUnknown : TsValue
31-
data object TsNull : TsValue
32-
data object TsUndefined : TsValue
33-
data object TsException : TsValue
28+
sealed interface TsTestValue {
29+
data object TsAny : TsTestValue
30+
data object TsUnknown : TsTestValue
31+
data object TsNull : TsTestValue
32+
data object TsUndefined : TsTestValue
33+
data object TsException : TsTestValue
3434

35-
data class TsBoolean(val value: Boolean) : TsValue
36-
data class TsString(val value: String) : TsValue
37-
data class TsBigInt(val value: String) : TsValue
35+
data class TsBoolean(val value: Boolean) : TsTestValue
36+
data class TsString(val value: String) : TsTestValue
37+
data class TsBigInt(val value: String) : TsTestValue
3838

39-
sealed interface TsNumber : TsValue {
39+
sealed interface TsNumber : TsTestValue {
4040
data class TsInteger(val value: Int) : TsNumber
4141

4242
data class TsDouble(val value: Double) : TsNumber
@@ -48,14 +48,14 @@ sealed interface TsValue {
4848
}
4949
}
5050

51-
data class TsObject(val addr: Int) : TsValue
51+
data class TsObject(val addr: Int) : TsTestValue
5252

5353
data class TsClass(
5454
val name: String,
55-
val properties: Map<String, TsValue>,
56-
) : TsValue
55+
val properties: Map<String, TsTestValue>,
56+
) : TsTestValue
5757

58-
data class TsArray<T : TsValue>(
58+
data class TsArray<T : TsTestValue>(
5959
val values: List<T>,
60-
) : TsValue
60+
) : TsTestValue
6161
}

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

+2
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import org.jacodb.ets.model.EtsNullType
99
import org.jacodb.ets.model.EtsNumberType
1010
import org.jacodb.ets.model.EtsRefType
1111
import org.jacodb.ets.model.EtsScene
12+
import org.jacodb.ets.model.EtsStringType
1213
import org.jacodb.ets.model.EtsType
1314
import org.jacodb.ets.model.EtsUndefinedType
1415
import org.jacodb.ets.model.EtsUnionType
@@ -58,6 +59,7 @@ class TsContext(
5859
fun typeToSort(type: EtsType): USort = when (type) {
5960
is EtsBooleanType -> boolSort
6061
is EtsNumberType -> fp64Sort
62+
is EtsStringType -> fp64Sort
6163
is EtsNullType -> addressSort
6264
is EtsUndefinedType -> addressSort
6365
is EtsUnionType -> unresolvedSort

0 commit comments

Comments
 (0)