Skip to content

Commit c6e023f

Browse files
LipenLipen
committed
Switch to a new ETS model
1 parent 4a9d7a5 commit c6e023f

File tree

78 files changed

+965
-1292
lines changed

Some content is hidden

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

78 files changed

+965
-1292
lines changed

Diff for: ‎.github/workflows/ci.yml

+35
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,13 @@ jobs:
1818
- name: Checkout repository
1919
uses: actions/checkout@v4
2020

21+
- name: Checkout local jacodb
22+
uses: actions/checkout@v4
23+
with:
24+
repository: UnitTestBot/jacodb
25+
ref: lipen/ts-model
26+
path: jacodb
27+
2128
- name: Setup Java JDK
2229
uses: actions/setup-java@v4
2330
with:
@@ -45,6 +52,13 @@ jobs:
4552
- name: Checkout repository
4653
uses: actions/checkout@v4
4754

55+
- name: Checkout local jacodb
56+
uses: actions/checkout@v4
57+
with:
58+
repository: UnitTestBot/jacodb
59+
ref: lipen/ts-model
60+
path: jacodb
61+
4862
- name: Setup Java JDK
4963
uses: actions/setup-java@v4
5064
with:
@@ -74,6 +88,13 @@ jobs:
7488
# 'usvm-python/cpythonadapter/cpython' is a submodule
7589
submodules: true
7690

91+
- name: Checkout local jacodb
92+
uses: actions/checkout@v4
93+
with:
94+
repository: UnitTestBot/jacodb
95+
ref: lipen/ts-model
96+
path: jacodb
97+
7798
- name: Setup Java JDK
7899
uses: actions/setup-java@v4
79100
with:
@@ -107,6 +128,13 @@ jobs:
107128
- name: Checkout repository
108129
uses: actions/checkout@v4
109130

131+
- name: Checkout local jacodb
132+
uses: actions/checkout@v4
133+
with:
134+
repository: UnitTestBot/jacodb
135+
ref: lipen/ts-model
136+
path: jacodb
137+
110138
- name: Setup Java JDK
111139
uses: actions/setup-java@v4
112140
with:
@@ -165,6 +193,13 @@ jobs:
165193
- name: Checkout repository
166194
uses: actions/checkout@v4
167195

196+
- name: Checkout local jacodb
197+
uses: actions/checkout@v4
198+
with:
199+
repository: UnitTestBot/jacodb
200+
ref: lipen/ts-model
201+
path: jacodb
202+
168203
- name: Setup Java JDK
169204
uses: actions/setup-java@v4
170205
with:

Diff for: ‎buildSrc/src/main/kotlin/Dependencies.kt

+3-2
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ object Versions {
66
const val clikt = "5.0.0"
77
const val detekt = "1.23.7"
88
const val ini4j = "0.5.4"
9-
const val jacodb = "903fd1da7c"
9+
const val jacodb = "6ec737ce76"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"
@@ -116,7 +116,8 @@ object Libs {
116116
)
117117

118118
// https://github.com/UnitTestBot/jacodb
119-
private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild
119+
// private const val jacodbPackage = "com.github.UnitTestBot.jacodb" // use "org.jacodb" with includeBuild
120+
private const val jacodbPackage = "org.jacodb"
120121
val jacodb_core = dep(
121122
group = jacodbPackage,
122123
name = "jacodb-core",

Diff for: ‎settings.gradle.kts

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
2525
// Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink.
2626
// As a workaround, we convert it to a real absolute path.
2727
// See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
28-
// includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath())
28+
includeBuild(file("jacodb").toPath().toRealPath().toAbsolutePath())
2929

3030
pluginManagement {
3131
resolutionStrategy {

Diff for: ‎usvm-ts-dataflow/build.gradle.kts

+1
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ dependencies {
1616

1717
api(Libs.jacodb_api_common)
1818
api(Libs.jacodb_ets)
19+
implementation(Libs.jacodb_core)
1920
implementation(Libs.jacodb_taint_configuration)
2021
implementation(Libs.kotlinx_collections)
2122
implementation(Libs.kotlinx_serialization_json)

Diff for: ‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@
1616

1717
package org.usvm.dataflow.ts.graph
1818

19-
import org.jacodb.ets.base.EtsStmt
2019
import org.jacodb.ets.model.EtsMethod
2120
import org.jacodb.ets.model.EtsScene
21+
import org.jacodb.ets.model.EtsStmt
2222

2323
private class BackwardEtsApplicationGraphImpl(
2424
val forward: EtsApplicationGraph,

Diff for: ‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt

+30-12
Original file line numberDiff line numberDiff line change
@@ -17,19 +17,20 @@
1717
package org.usvm.dataflow.ts.graph
1818

1919
import mu.KotlinLogging
20-
import org.jacodb.ets.base.CONSTRUCTOR_NAME
21-
import org.jacodb.ets.base.EtsAssignStmt
22-
import org.jacodb.ets.base.EtsClassType
23-
import org.jacodb.ets.base.EtsNewExpr
24-
import org.jacodb.ets.base.EtsStmt
25-
import org.jacodb.ets.base.UNKNOWN_FILE_NAME
20+
import org.jacodb.ets.model.EtsAssignStmt
2621
import org.jacodb.ets.model.EtsClass
2722
import org.jacodb.ets.model.EtsClassSignature
23+
import org.jacodb.ets.model.EtsClassType
2824
import org.jacodb.ets.model.EtsFileSignature
2925
import org.jacodb.ets.model.EtsMethod
3026
import org.jacodb.ets.model.EtsMethodSignature
27+
import org.jacodb.ets.model.EtsNewExpr
28+
import org.jacodb.ets.model.EtsNopStmt
3129
import org.jacodb.ets.model.EtsScene
30+
import org.jacodb.ets.model.EtsStmt
31+
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
3232
import org.jacodb.ets.utils.Maybe
33+
import org.jacodb.ets.utils.UNKNOWN_FILE_NAME
3334
import org.jacodb.ets.utils.callExpr
3435
import org.jacodb.ets.utils.onSome
3536
import org.usvm.dataflow.graph.ApplicationGraph
@@ -80,12 +81,14 @@ class EtsApplicationGraphImpl(
8081
) : EtsApplicationGraph {
8182

8283
override fun predecessors(node: EtsStmt): Sequence<EtsStmt> {
84+
if (node is EtsNopStmt && node.location.index == -1) return emptySequence()
8385
val graph = node.method.flowGraph()
8486
val predecessors = graph.predecessors(node)
8587
return predecessors.asSequence()
8688
}
8789

8890
override fun successors(node: EtsStmt): Sequence<EtsStmt> {
91+
if (node is EtsNopStmt && node.location.index == -1) return entryPoints(node.method)
8992
val graph = node.method.flowGraph()
9093
val successors = graph.successors(node)
9194
return successors.asSequence()
@@ -136,10 +139,10 @@ class EtsApplicationGraphImpl(
136139
override fun callees(node: EtsStmt): Sequence<EtsMethod> {
137140
val expr = node.callExpr ?: return emptySequence()
138141

139-
val callee = expr.method
142+
val callee = expr.callee
140143

141144
// Note: the resolving code below expects that at least the current method signature is known.
142-
check(node.method.enclosingClass.isIdeal()) {
145+
check(node.method.signature.enclosingClass.isIdeal()) {
143146
"Incomplete signature in method: ${node.method}"
144147
}
145148

@@ -154,8 +157,9 @@ class EtsApplicationGraphImpl(
154157
}
155158

156159
if (prevStmt is EtsAssignStmt && prevStmt.rhv is EtsNewExpr) {
157-
val cls = prevStmt.rhv.type
160+
val cls = (prevStmt.rhv as EtsNewExpr).type
158161
if (cls !is EtsClassType) {
162+
// logger.warn { "Could not resolve callees for $node" }
159163
return emptySequence()
160164
}
161165

@@ -176,6 +180,7 @@ class EtsApplicationGraphImpl(
176180
}
177181

178182
// Constructor signature is garbage. Sorry, can't do anything in such case.
183+
// logger.warn { "Could not resolve callees for $node" }
179184
return emptySequence()
180185
}
181186

@@ -186,6 +191,7 @@ class EtsApplicationGraphImpl(
186191
if (cls.isSome) {
187192
return sequenceOf(cls.getOrThrow().ctor)
188193
} else {
194+
// logger.warn { "Could not resolve callees for $node" }
189195
return emptySequence()
190196
}
191197
}
@@ -197,6 +203,7 @@ class EtsApplicationGraphImpl(
197203
if (resolved.isSome) {
198204
return sequenceOf(resolved.getOrThrow())
199205
} else {
206+
// logger.warn { "Could not resolve callees for $node" }
200207
return emptySequence()
201208
}
202209
}
@@ -205,13 +212,15 @@ class EtsApplicationGraphImpl(
205212

206213
val resolved = run {
207214
if (cls.isNone) {
215+
// logger.warn { "Could not resolve callees for $node" }
208216
emptySequence()
209217
} else {
210218
cls.getOrThrow().methods.asSequence().filter { it.name == callee.name }
211219
}
212220
}
213221
if (resolved.none()) {
214222
cacheMethodWithIdealSignature[callee] = Maybe.none()
223+
// logger.warn { "Could not resolve callees for $node" }
215224
return emptySequence()
216225
}
217226
val r = resolved.singleOrNull()
@@ -223,7 +232,7 @@ class EtsApplicationGraphImpl(
223232
// If the callee signature is not ideal, resolve it via a partial match...
224233
check(!callee.enclosingClass.isIdeal())
225234

226-
val cls = lookupClassWithIdealSignature(node.method.enclosingClass).let {
235+
val cls = lookupClassWithIdealSignature(node.method.signature.enclosingClass).let {
227236
if (it.isNone) {
228237
error("Could not find the enclosing class: ${node.method.enclosingClass}")
229238
}
@@ -250,14 +259,23 @@ class EtsApplicationGraphImpl(
250259
// try to *uniquely* resolve the callee via a partial signature match:
251260
val resolved = projectMethodsByName[callee.name].orEmpty()
252261
.asSequence()
253-
.filter { compareClassSignatures(it.enclosingClass, callee.enclosingClass) != ComparisonResult.NotEqual }
262+
.filter {
263+
compareClassSignatures(
264+
it.signature.enclosingClass,
265+
callee.enclosingClass
266+
) != ComparisonResult.NotEqual
267+
}
254268
// Note: exclude current class:
255269
.filterNot {
256-
compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual
270+
compareClassSignatures(
271+
it.signature.enclosingClass,
272+
node.method.signature.enclosingClass
273+
) != ComparisonResult.NotEqual
257274
}
258275
.toList()
259276
if (resolved.isEmpty()) {
260277
cachePartiallyMatchedCallees[callee] = emptyList()
278+
// logger.warn { "Could not resolve callees for $node" }
261279
return emptySequence()
262280
}
263281
val r = resolved.singleOrNull() ?: run {

Diff for: ‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt

+11-11
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
package org.usvm.dataflow.ts.infer
22

3-
import org.jacodb.ets.base.EtsArrayAccess
4-
import org.jacodb.ets.base.EtsAwaitExpr
5-
import org.jacodb.ets.base.EtsCastExpr
6-
import org.jacodb.ets.base.EtsConstant
7-
import org.jacodb.ets.base.EtsEntity
8-
import org.jacodb.ets.base.EtsInstanceFieldRef
9-
import org.jacodb.ets.base.EtsLocal
10-
import org.jacodb.ets.base.EtsParameterRef
11-
import org.jacodb.ets.base.EtsStaticFieldRef
12-
import org.jacodb.ets.base.EtsThis
13-
import org.jacodb.ets.base.EtsValue
3+
import org.jacodb.ets.model.EtsArrayAccess
4+
import org.jacodb.ets.model.EtsAwaitExpr
5+
import org.jacodb.ets.model.EtsCastExpr
146
import org.jacodb.ets.model.EtsClassSignature
7+
import org.jacodb.ets.model.EtsConstant
8+
import org.jacodb.ets.model.EtsEntity
9+
import org.jacodb.ets.model.EtsInstanceFieldRef
10+
import org.jacodb.ets.model.EtsLocal
11+
import org.jacodb.ets.model.EtsParameterRef
12+
import org.jacodb.ets.model.EtsStaticFieldRef
13+
import org.jacodb.ets.model.EtsThis
14+
import org.jacodb.ets.model.EtsValue
1515

1616
data class AccessPath(val base: AccessPathBase, val accesses: List<Accessor>) {
1717
operator fun plus(accessor: Accessor) = AccessPath(base, accesses + accessor)

Diff for: ‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt

+21-21
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,27 @@
11
package org.usvm.dataflow.ts.infer
22

33
import mu.KotlinLogging
4-
import org.jacodb.ets.base.EtsArrayAccess
5-
import org.jacodb.ets.base.EtsAssignStmt
6-
import org.jacodb.ets.base.EtsBinaryExpr
7-
import org.jacodb.ets.base.EtsCallExpr
8-
import org.jacodb.ets.base.EtsCallStmt
9-
import org.jacodb.ets.base.EtsCastExpr
10-
import org.jacodb.ets.base.EtsConstant
11-
import org.jacodb.ets.base.EtsEntity
12-
import org.jacodb.ets.base.EtsInstanceCallExpr
13-
import org.jacodb.ets.base.EtsInstanceFieldRef
14-
import org.jacodb.ets.base.EtsInstanceOfExpr
15-
import org.jacodb.ets.base.EtsLocal
16-
import org.jacodb.ets.base.EtsNewArrayExpr
17-
import org.jacodb.ets.base.EtsNewExpr
18-
import org.jacodb.ets.base.EtsParameterRef
19-
import org.jacodb.ets.base.EtsStaticFieldRef
20-
import org.jacodb.ets.base.EtsStmt
21-
import org.jacodb.ets.base.EtsThis
22-
import org.jacodb.ets.base.EtsUnaryExpr
4+
import org.jacodb.ets.model.EtsArrayAccess
5+
import org.jacodb.ets.model.EtsAssignStmt
6+
import org.jacodb.ets.model.EtsBinaryExpr
7+
import org.jacodb.ets.model.EtsCallExpr
8+
import org.jacodb.ets.model.EtsCallStmt
9+
import org.jacodb.ets.model.EtsCastExpr
2310
import org.jacodb.ets.model.EtsClassSignature
11+
import org.jacodb.ets.model.EtsConstant
12+
import org.jacodb.ets.model.EtsEntity
13+
import org.jacodb.ets.model.EtsInstanceCallExpr
14+
import org.jacodb.ets.model.EtsInstanceFieldRef
15+
import org.jacodb.ets.model.EtsInstanceOfExpr
16+
import org.jacodb.ets.model.EtsLocal
2417
import org.jacodb.ets.model.EtsMethod
18+
import org.jacodb.ets.model.EtsNewArrayExpr
19+
import org.jacodb.ets.model.EtsNewExpr
20+
import org.jacodb.ets.model.EtsParameterRef
21+
import org.jacodb.ets.model.EtsStaticFieldRef
22+
import org.jacodb.ets.model.EtsStmt
23+
import org.jacodb.ets.model.EtsThis
24+
import org.jacodb.ets.model.EtsUnaryExpr
2525
import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation
2626

2727
private val logger = KotlinLogging.logger {}
@@ -425,7 +425,7 @@ class MethodAliasInfoImpl(
425425

426426
is EtsInstanceCallExpr -> {
427427
initEntity(entity.instance)
428-
newString(entity.method.name)
428+
newString(entity.callee.name)
429429
entity.args.forEach { initEntity(it) }
430430
}
431431
}
@@ -516,7 +516,7 @@ class MethodAliasInfoImpl(
516516
}
517517
}
518518

519-
val root = method.cfg.stmts[0]
519+
val root = method.cfg.stmts.first()
520520
postOrderDfs(root)
521521
order.reverse()
522522

Diff for: ‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
package org.usvm.dataflow.ts.infer
22

3-
import org.jacodb.ets.base.EtsStmt
43
import org.jacodb.ets.model.EtsMethod
4+
import org.jacodb.ets.model.EtsStmt
55
import org.usvm.dataflow.ifds.Vertex
66

77
sealed interface AnalyzerEvent

0 commit comments

Comments
 (0)