Skip to content

Commit 192ba27

Browse files
LipenLipen
authored
Switch to a new ETS model (#269)
1 parent e32d14f commit 192ba27

File tree

77 files changed

+981
-1320
lines changed

Some content is hidden

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

77 files changed

+981
-1320
lines changed

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

+1-1
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 = "6ec737ce76"
9+
const val jacodb = "3b6a17f000"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

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

+20-12
Original file line numberDiff line numberDiff line change
@@ -17,19 +17,19 @@
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
3128
import org.jacodb.ets.model.EtsScene
29+
import org.jacodb.ets.model.EtsStmt
30+
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
3231
import org.jacodb.ets.utils.Maybe
32+
import org.jacodb.ets.utils.UNKNOWN_FILE_NAME
3333
import org.jacodb.ets.utils.callExpr
3434
import org.jacodb.ets.utils.onSome
3535
import org.usvm.dataflow.graph.ApplicationGraph
@@ -136,10 +136,10 @@ class EtsApplicationGraphImpl(
136136
override fun callees(node: EtsStmt): Sequence<EtsMethod> {
137137
val expr = node.callExpr ?: return emptySequence()
138138

139-
val callee = expr.method
139+
val callee = expr.callee
140140

141141
// Note: the resolving code below expects that at least the current method signature is known.
142-
check(node.method.enclosingClass.isIdeal()) {
142+
check(node.method.signature.enclosingClass.isIdeal()) {
143143
"Incomplete signature in method: ${node.method}"
144144
}
145145

@@ -154,7 +154,7 @@ class EtsApplicationGraphImpl(
154154
}
155155

156156
if (prevStmt is EtsAssignStmt && prevStmt.rhv is EtsNewExpr) {
157-
val cls = prevStmt.rhv.type
157+
val cls = (prevStmt.rhv as EtsNewExpr).type
158158
if (cls !is EtsClassType) {
159159
return emptySequence()
160160
}
@@ -223,7 +223,7 @@ class EtsApplicationGraphImpl(
223223
// If the callee signature is not ideal, resolve it via a partial match...
224224
check(!callee.enclosingClass.isIdeal())
225225

226-
val cls = lookupClassWithIdealSignature(node.method.enclosingClass).let {
226+
val cls = lookupClassWithIdealSignature(node.method.signature.enclosingClass).let {
227227
if (it.isNone) {
228228
error("Could not find the enclosing class: ${node.method.enclosingClass}")
229229
}
@@ -250,10 +250,18 @@ class EtsApplicationGraphImpl(
250250
// try to *uniquely* resolve the callee via a partial signature match:
251251
val resolved = projectMethodsByName[callee.name].orEmpty()
252252
.asSequence()
253-
.filter { compareClassSignatures(it.enclosingClass, callee.enclosingClass) != ComparisonResult.NotEqual }
253+
.filter {
254+
compareClassSignatures(
255+
it.signature.enclosingClass,
256+
callee.enclosingClass
257+
) != ComparisonResult.NotEqual
258+
}
254259
// Note: exclude current class:
255260
.filterNot {
256-
compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual
261+
compareClassSignatures(
262+
it.signature.enclosingClass,
263+
node.method.signature.enclosingClass
264+
) != ComparisonResult.NotEqual
257265
}
258266
.toList()
259267
if (resolved.isEmpty()) {

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

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

+12-19
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@
1616

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

19-
import org.jacodb.ets.base.EtsInstLocation
20-
import org.jacodb.ets.base.EtsNopStmt
21-
import org.jacodb.ets.base.EtsStmt
2219
import org.jacodb.ets.model.EtsMethod
20+
import org.jacodb.ets.model.EtsNopStmt
2321
import org.jacodb.ets.model.EtsScene
22+
import org.jacodb.ets.model.EtsStmt
23+
import org.jacodb.ets.model.EtsStmtLocation
2424
import org.usvm.dataflow.ts.graph.EtsApplicationGraph
2525
import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl
2626

@@ -41,8 +41,8 @@ class EtsApplicationGraphWithExplicitEntryPoint(
4141

4242
override fun exitPoints(method: EtsMethod): Sequence<EtsStmt> = graph.exitPoints(method)
4343

44-
private fun methodEntryPoint(method: EtsMethod) =
45-
EtsNopStmt(EtsInstLocation(method, index = -1))
44+
private fun methodEntryPoint(method: EtsMethod): EtsStmt =
45+
EtsNopStmt(EtsStmtLocation(method, index = -1))
4646

4747
override fun entryPoints(method: EtsMethod): Sequence<EtsStmt> = sequenceOf(methodEntryPoint(method))
4848

@@ -51,28 +51,21 @@ class EtsApplicationGraphWithExplicitEntryPoint(
5151
override fun callees(node: EtsStmt): Sequence<EtsMethod> = graph.callees(node)
5252

5353
override fun successors(node: EtsStmt): Sequence<EtsStmt> {
54-
val method = methodOf(node)
55-
val methodEntry = methodEntryPoint(method)
56-
57-
if (node == methodEntry) {
58-
return graph.entryPoints(method)
54+
if (node.location.index == -1) {
55+
require(node is EtsNopStmt)
56+
return graph.entryPoints(node.method)
5957
}
60-
6158
return graph.successors(node)
6259
}
6360

6461
override fun predecessors(node: EtsStmt): Sequence<EtsStmt> {
65-
val method = methodOf(node)
66-
val methodEntry = methodEntryPoint(method)
67-
68-
if (node == methodEntry) {
62+
if (node.location.index == -1) {
63+
require(node is EtsNopStmt)
6964
return emptySequence()
7065
}
71-
72-
if (node in graph.entryPoints(method)) {
73-
return sequenceOf(methodEntry)
66+
if (node.location.index == 0) {
67+
return entryPoints(node.method)
7468
}
75-
7669
return graph.predecessors(node)
7770
}
7871
}

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

+2-3
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
package org.usvm.dataflow.ts.infer
22

3-
import org.jacodb.ets.base.EtsStmt
4-
import org.jacodb.ets.base.EtsType
53
import org.jacodb.ets.model.EtsMethod
4+
import org.jacodb.ets.model.EtsStmt
5+
import org.jacodb.ets.model.EtsType
66
import org.jacodb.impl.cfg.graphs.GraphDominators
7-
import org.usvm.dataflow.graph.ApplicationGraph
87
import org.usvm.dataflow.ifds.Analyzer
98
import org.usvm.dataflow.ifds.Edge
109
import org.usvm.dataflow.ifds.Vertex

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

+27-39
Original file line numberDiff line numberDiff line change
@@ -1,28 +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.EtsCastExpr
7-
import org.jacodb.ets.base.EtsEntity
8-
import org.jacodb.ets.base.EtsEqExpr
9-
import org.jacodb.ets.base.EtsFieldRef
10-
import org.jacodb.ets.base.EtsIfStmt
11-
import org.jacodb.ets.base.EtsInExpr
12-
import org.jacodb.ets.base.EtsInstanceCallExpr
13-
import org.jacodb.ets.base.EtsLValue
14-
import org.jacodb.ets.base.EtsLocal
15-
import org.jacodb.ets.base.EtsNewExpr
16-
import org.jacodb.ets.base.EtsNumberConstant
17-
import org.jacodb.ets.base.EtsParameterRef
18-
import org.jacodb.ets.base.EtsReturnStmt
19-
import org.jacodb.ets.base.EtsStmt
20-
import org.jacodb.ets.base.EtsStringConstant
21-
import org.jacodb.ets.base.EtsThis
22-
import org.jacodb.ets.base.EtsThrowStmt
23-
import org.jacodb.ets.base.EtsType
24-
import org.jacodb.ets.base.EtsValue
4+
import org.jacodb.ets.model.EtsArrayAccess
5+
import org.jacodb.ets.model.EtsAssignStmt
6+
import org.jacodb.ets.model.EtsCastExpr
7+
import org.jacodb.ets.model.EtsEntity
8+
import org.jacodb.ets.model.EtsEqExpr
9+
import org.jacodb.ets.model.EtsFieldRef
10+
import org.jacodb.ets.model.EtsIfStmt
11+
import org.jacodb.ets.model.EtsInExpr
12+
import org.jacodb.ets.model.EtsInstanceCallExpr
13+
import org.jacodb.ets.model.EtsLocal
2514
import org.jacodb.ets.model.EtsMethod
15+
import org.jacodb.ets.model.EtsNewExpr
16+
import org.jacodb.ets.model.EtsNumberConstant
17+
import org.jacodb.ets.model.EtsParameterRef
18+
import org.jacodb.ets.model.EtsReturnStmt
19+
import org.jacodb.ets.model.EtsStmt
20+
import org.jacodb.ets.model.EtsStringConstant
21+
import org.jacodb.ets.model.EtsThis
22+
import org.jacodb.ets.model.EtsThrowStmt
23+
import org.jacodb.ets.model.EtsType
24+
import org.jacodb.ets.model.EtsValue
2625
import org.jacodb.ets.utils.callExpr
2726
import org.jacodb.impl.cfg.graphs.GraphDominators
2827
import org.usvm.dataflow.ifds.FlowFunction
@@ -212,7 +211,8 @@ class BackwardFlowFunctions(
212211
if (returnValue != null) {
213212
val variable = returnValue.toBase()
214213
val type = if (doAddKnownTypes) {
215-
EtsTypeFact.from(returnValue.type).fixAnyToUnknown()
214+
val knownType = returnValue.tryGetKnownType(current.method)
215+
EtsTypeFact.from(knownType).fixAnyToUnknown()
216216
} else {
217217
EtsTypeFact.UnknownEtsTypeFact
218218
}
@@ -241,14 +241,8 @@ class BackwardFlowFunctions(
241241
// Case `x... := y`
242242
// ∅ |= y:unknown
243243
val type = if (doAddKnownTypes) {
244-
EtsTypeFact.from(current.rhv.type).let {
245-
// Note: convert Any to Unknown, because intersection with Any is Any
246-
if (it is EtsTypeFact.AnyEtsTypeFact) {
247-
EtsTypeFact.UnknownEtsTypeFact
248-
} else {
249-
it
250-
}
251-
}
244+
val knownType = current.rhv.tryGetKnownType(current.method)
245+
EtsTypeFact.from(knownType).fixAnyToUnknown()
252246
} else {
253247
EtsTypeFact.UnknownEtsTypeFact
254248
}
@@ -283,13 +277,7 @@ class BackwardFlowFunctions(
283277
}
284278
}
285279

286-
val lhv = when (val l = current.lhv) {
287-
is EtsLValue -> l.toPath()
288-
else -> {
289-
logger.info { "TODO backward assign zero: $current" }
290-
error("Unexpected LHV in assignment: $current")
291-
}
292-
}
280+
val lhv = current.lhv.toPath()
293281

294282
// Handle new possible facts for LHS:
295283
if (lhv.accesses.isNotEmpty()) {
@@ -543,7 +531,7 @@ class BackwardFlowFunctions(
543531
val objectWithMethod = EtsTypeFact.ObjectEtsTypeFact(
544532
cls = null,
545533
properties = mapOf(
546-
callExpr.method.name to EtsTypeFact.FunctionEtsTypeFact
534+
callExpr.callee.name to EtsTypeFact.FunctionEtsTypeFact
547535
)
548536
)
549537
result += TypedVariable(path, objectWithMethod)
@@ -552,7 +540,7 @@ class BackwardFlowFunctions(
552540
if (doAddKnownTypes) {
553541
// f(x:T) |= x:T, where T is the type of the argument in f's signature
554542
for ((index, arg) in callExpr.args.withIndex()) {
555-
val param = callExpr.method.parameters.getOrNull(index) ?: continue
543+
val param = callExpr.callee.parameters.getOrNull(index) ?: continue
556544
val base = arg.toBase()
557545
val type = EtsTypeFact.from(param.type)
558546
result += TypedVariable(base, type)

0 commit comments

Comments
 (0)