Skip to content

Commit 094d735

Browse files
committed
removed old backward flow functions
1 parent bbe3a1b commit 094d735

File tree

6 files changed

+187
-862
lines changed

6 files changed

+187
-862
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ data class ForwardSummaryAnalyzerEvent(
1717

1818
data class BackwardSummaryAnalyzerEvent(
1919
val method: EtsMethod,
20-
val initialVertex: Vertex<BackwardPathTypeDomainFact, EtsStmt>,
21-
val exitVertex: Vertex<BackwardPathTypeDomainFact, EtsStmt>,
20+
val initialVertex: Vertex<BackwardTypeDomainFact, EtsStmt>,
21+
val exitVertex: Vertex<BackwardTypeDomainFact, EtsStmt>,
2222
) : AnalyzerEvent {
2323
val initialFact get() = initialVertex.fact
2424
val exitFact get() = exitVertex.fact

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

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2,32 +2,28 @@ 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,
17-
) : Analyzer<BackwardPathTypeDomainFact, AnalyzerEvent, EtsMethod, EtsStmt> {
13+
) : Analyzer<BackwardTypeDomainFact, AnalyzerEvent, EtsMethod, EtsStmt> {
1814

19-
override val flowFunctions = BackwardPathFlowFunctions(doAddKnownTypes)
15+
override val flowFunctions = BackwardFlowFunctions(doAddKnownTypes)
2016

2117
override fun handleCrossUnitCall(
22-
caller: Vertex<BackwardPathTypeDomainFact, EtsStmt>,
23-
callee: Vertex<BackwardPathTypeDomainFact, EtsStmt>,
18+
caller: Vertex<BackwardTypeDomainFact, EtsStmt>,
19+
callee: Vertex<BackwardTypeDomainFact, EtsStmt>,
2420
): List<AnalyzerEvent> {
2521
error("No cross unit calls")
2622
}
2723

28-
override fun handleNewEdge(edge: Edge<BackwardPathTypeDomainFact, EtsStmt>): List<AnalyzerEvent> {
24+
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)