Skip to content

Commit 814740d

Browse files
MForest7Lipen
andauthored
Replaced access path bases with access paths in backward dataflow (#282)
Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent 72914ba commit 814740d

13 files changed

Lines changed: 299 additions & 566 deletions

File tree

.github/workflows/ci.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ jobs:
127127
DEST_DIR="arkanalyzer"
128128
MAX_RETRIES=10
129129
RETRY_DELAY=3 # Delay between retries in seconds
130-
BRANCH="neo/2025-06-16"
130+
BRANCH="neo/2025-06-24"
131131
132132
for ((i=1; i<=MAX_RETRIES; i++)); do
133133
git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

usvm-ts-dataflow/build.gradle.kts

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ dependencies {
2121
implementation(Libs.kotlinx_collections)
2222
implementation(Libs.kotlinx_serialization_json)
2323
implementation(Libs.clikt)
24+
runtimeOnly(Libs.logback)
2425

2526
testImplementation(Libs.mockk)
2627
testImplementation(Libs.junit_jupiter_params)
@@ -129,5 +130,8 @@ tasks.shadowJar {
129130
// Provider com.github.ajalt.mordant.terminal.terminalinterface.jna.TerminalInterfaceProviderJna not found
130131
// ```
131132
exclude(dependency("com.github.ajalt.mordant:.*:.*"))
133+
134+
// Keep the logback in shadow jar:
135+
exclude(dependency("ch.qos.logback:logback-classic:.*"))
132136
}
133137
}

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

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,21 +2,17 @@ package org.usvm.dataflow.ts.infer
22

33
import org.jacodb.ets.model.EtsMethod
44
import org.jacodb.ets.model.EtsStmt
5-
import org.jacodb.ets.model.EtsType
6-
import org.jacodb.impl.cfg.graphs.GraphDominators
75
import org.usvm.dataflow.ifds.Analyzer
86
import org.usvm.dataflow.ifds.Edge
97
import org.usvm.dataflow.ifds.Vertex
108
import org.usvm.dataflow.ts.graph.EtsApplicationGraph
119

1210
class BackwardAnalyzer(
1311
val graph: EtsApplicationGraph,
14-
savedTypes: MutableMap<EtsType, MutableList<EtsTypeFact>>,
15-
dominators: (EtsMethod) -> GraphDominators<EtsStmt>,
1612
doAddKnownTypes: Boolean = true,
1713
) : Analyzer<BackwardTypeDomainFact, AnalyzerEvent, EtsMethod, EtsStmt> {
1814

19-
override val flowFunctions = BackwardFlowFunctions(graph, dominators, savedTypes, doAddKnownTypes)
15+
override val flowFunctions = BackwardFlowFunctions(doAddKnownTypes)
2016

2117
override fun handleCrossUnitCall(
2218
caller: Vertex<BackwardTypeDomainFact, EtsStmt>,
@@ -27,7 +23,7 @@ class BackwardAnalyzer(
2723

2824
override fun handleNewEdge(edge: Edge<BackwardTypeDomainFact, EtsStmt>): List<AnalyzerEvent> {
2925
val (startVertex, currentVertex) = edge
30-
val (current, currentFact) = currentVertex
26+
val (current, _) = currentVertex
3127

3228
val method = graph.methodOf(current)
3329
val currentIsExit = current in graph.exitPoints(method)

0 commit comments

Comments
 (0)