fix: Improve alias handling and inter-proc analysis robustness

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/MethodAnalyzer.kt

@@ -17,6 +17,7 @@ import org.seqra.dataflow.ap.ifds.access.InitialFactAp
 import org.seqra.dataflow.ap.ifds.analysis.MethodCallFlowFunction
 import org.seqra.dataflow.ap.ifds.analysis.MethodCallFlowFunction.ZeroCallFact
 import org.seqra.dataflow.ap.ifds.analysis.MethodCallSummaryHandler
+import org.seqra.dataflow.ap.ifds.analysis.MethodCallSummaryHandler.SummaryEdge
 import org.seqra.dataflow.ap.ifds.analysis.MethodSequentFlowFunction.Sequent
 import org.seqra.dataflow.ap.ifds.analysis.MethodStartFlowFunction.StartFact
 import org.seqra.dataflow.ap.ifds.trace.MethodForwardTraceResolver
@@ -173,7 +174,9 @@ class NormalMethodAnalyzer(
     private var pendingSideEffectRequirements = arrayListOf<InitialFactAp>()
     private var pendingSideEffectSummaries = arrayListOf<SideEffectSummary>()
 
-    private val analysisContext = analysisManager.getMethodAnalysisContext(methodEntryPoint, runner.graph)
+    private val analysisContext = analysisManager.getMethodAnalysisContext(
+        methodEntryPoint, runner.graph, runner.methodCallResolver
+    )
 
     private var analyzerEnqueued = false
     private var unprocessedEdges = arrayListOf<Edge>()
@@ -903,8 +906,8 @@ class NormalMethodAnalyzer(
                 currentEdgeFactAp = sub.currentEdge.factAp,
                 methodInitialFactBase = sub.methodInitialFactBase,
                 methodSummaries = applicableSummaries,
-                handleSummaryEdge = { currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryFact: FinalFactAp ->
-                    handler.handleFactToFact(sub.currentEdge.initialFactAp, currentFactAp, summaryEffect, summaryFact)
+                handleSummaryEdge = { currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryEdge: SummaryEdge ->
+                    handler.handleFactToFact(sub.currentEdge.initialFactAp, currentFactAp, summaryEffect, summaryEdge)
                 }
             )
         }
@@ -938,8 +941,8 @@ class NormalMethodAnalyzer(
                 currentEdgeFactAp = sub.currentEdge.factAp,
                 methodInitialFactBase = sub.methodInitialFactBase,
                 methodSummaries = applicableSummaries,
-                handleSummaryEdge = { currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryFact: FinalFactAp ->
-                    handler.handleNDFactToFact(sub.currentEdge.initialFacts, currentFactAp, summaryEffect, summaryFact)
+                handleSummaryEdge = { currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryEdge: SummaryEdge ->
+                    handler.handleNDFactToFact(sub.currentEdge.initialFacts, currentFactAp, summaryEffect, summaryEdge)
                 }
             )
         }
@@ -960,7 +963,7 @@ class NormalMethodAnalyzer(
         currentEdgeFactAp: FinalFactAp,
         methodInitialFactBase: AccessPathBase,
         methodSummaries: List<FactToFact>,
-        handleSummaryEdge: (currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryFact: FinalFactAp) -> Set<Sequent>
+        handleSummaryEdge: (currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryEdge: SummaryEdge) -> Set<Sequent>
     ) {
         applyMethodAnySummaries(
             currentEdge,
@@ -969,7 +972,7 @@ class NormalMethodAnalyzer(
             methodSummaries,
             { it.initialFactAp }
         ) { currentFactAp, summaryEdgeEffect, methodSummary ->
-            handleSummaryEdge(currentFactAp, summaryEdgeEffect, methodSummary.factAp)
+            handleSummaryEdge(currentFactAp, summaryEdgeEffect, methodSummary.summaryEdge())
         }
     }
 
@@ -1100,7 +1103,7 @@ class NormalMethodAnalyzer(
                             summaryHandler.handleZeroToFact(
                                 currentEdgeFactAp,
                                 SummaryExclusionRefinement(ExclusionSet.Universe),
-                                summaryEdge.factAp
+                                summaryEdge.summaryEdge()
                             )
                         }
 
@@ -1110,7 +1113,7 @@ class NormalMethodAnalyzer(
                                 initialFact,
                                 currentEdgeFactAp,
                                 SummaryExclusionRefinement(initialFact.exclusions),
-                                summaryEdge.factAp
+                                summaryEdge.summaryEdge()
                             )
                         }
 
@@ -1119,7 +1122,7 @@ class NormalMethodAnalyzer(
                                 ndSummaryInitial,
                                 currentEdgeFactAp,
                                 SummaryExclusionRefinement(ExclusionSet.Universe),
-                                summaryEdge.factAp
+                                summaryEdge.summaryEdge()
                             )
                         }
                     }
@@ -1133,7 +1136,7 @@ class NormalMethodAnalyzer(
                                     currentEdge.initialFactAp,
                                     currentEdgeFactAp,
                                     SummaryExclusionRefinement(currentEdge.initialFactAp.exclusions),
-                                    summaryEdge.factAp
+                                    summaryEdge.summaryEdge()
                                 )
                             }
 
@@ -1142,7 +1145,7 @@ class NormalMethodAnalyzer(
                                     ndSummaryInitial,
                                     currentEdgeFactAp,
                                     SummaryExclusionRefinement(ExclusionSet.Universe),
-                                    summaryEdge.factAp
+                                    summaryEdge.summaryEdge()
                                 )
                             }
                         }
@@ -1153,7 +1156,7 @@ class NormalMethodAnalyzer(
                             ndSummaryInitial + currentEdge.initialFacts,
                             currentEdgeFactAp,
                             SummaryExclusionRefinement(ExclusionSet.Universe),
-                            summaryEdge.factAp
+                            summaryEdge.summaryEdge()
                         )
                     }
                 }
@@ -1231,6 +1234,9 @@ class NormalMethodAnalyzer(
             }
         }
     }
+
+    private fun FactToFact.summaryEdge() = SummaryEdge.F2F(initialFactAp, factAp)
+    private fun NDFactToFact.summaryEdge() = SummaryEdge.NdF2F(initialFacts, factAp)
 }
 
 class EmptyMethodAnalyzer(

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/TaintAnalysisManager.kt

@@ -1,23 +1,26 @@
 package org.seqra.dataflow.ap.ifds
 
-import org.seqra.ir.api.common.CommonMethod
-import org.seqra.ir.api.common.cfg.CommonInst
-import org.seqra.util.analysis.ApplicationGraph
 import org.seqra.dataflow.ap.ifds.analysis.AnalysisManager
 import org.seqra.dataflow.ap.ifds.analysis.MethodAnalysisContext
+import org.seqra.dataflow.ap.ifds.analysis.MethodCallResolver
 import org.seqra.dataflow.ap.ifds.taint.TaintAnalysisContext
+import org.seqra.ir.api.common.CommonMethod
+import org.seqra.ir.api.common.cfg.CommonInst
+import org.seqra.util.analysis.ApplicationGraph
 
 interface TaintAnalysisManager : AnalysisManager {
     override fun getMethodAnalysisContext(
         methodEntryPoint: MethodEntryPoint,
-        graph: ApplicationGraph<CommonMethod, CommonInst>
+        graph: ApplicationGraph<CommonMethod, CommonInst>,
+        callResolver: MethodCallResolver,
     ): MethodAnalysisContext {
         error("Taint context required")
     }
 
     fun getMethodAnalysisContext(
         methodEntryPoint: MethodEntryPoint,
         graph: ApplicationGraph<CommonMethod, CommonInst>,
+        callResolver: MethodCallResolver,
         taintAnalysisContext: TaintAnalysisContext,
     ): MethodAnalysisContext
 }

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/TaintAnalysisUnitRunnerManager.kt

@@ -18,6 +18,7 @@ import kotlinx.coroutines.withTimeoutOrNull
 import mu.KotlinLogging
 import org.seqra.dataflow.ap.ifds.access.ApManager
 import org.seqra.dataflow.ap.ifds.analysis.MethodAnalysisContext
+import org.seqra.dataflow.ap.ifds.analysis.MethodCallResolver
 import org.seqra.dataflow.ap.ifds.serialization.SummarySerializationContext
 import org.seqra.dataflow.ap.ifds.taint.TaintAnalysisContext
 import org.seqra.dataflow.ap.ifds.taint.TaintAnalysisUnitStorage
@@ -331,9 +332,10 @@ class TaintAnalysisUnitRunnerManager(
     ) : TaintAnalysisManager by analysisManager {
         override fun getMethodAnalysisContext(
             methodEntryPoint: MethodEntryPoint,
-            graph: ApplicationGraph<CommonMethod, CommonInst>
+            graph: ApplicationGraph<CommonMethod, CommonInst>,
+            callResolver: MethodCallResolver
         ): MethodAnalysisContext = analysisManager.getMethodAnalysisContext(
-            methodEntryPoint, graph,
+            methodEntryPoint, graph, callResolver,
             TaintAnalysisContext(taintConfig, sinkTracker)
         )
     }

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/access/FactAp.kt

@@ -63,6 +63,7 @@ interface FinalFactAp : FactAp, ReadableAccessorList<FinalFactAp> {
     fun filterFact(filter: FactTypeChecker.FactApFilter): FinalFactAp?
 
     fun contains(factAp: InitialFactAp): Boolean
+    fun equalTo(factAp: InitialFactAp): Boolean
 
     fun hasEmptyDelta(other: InitialFactAp): Boolean =
         delta(other).any { it.isEmpty }

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/access/automata/AccessGraphFinalFactAp.kt

@@ -107,4 +107,11 @@ data class AccessGraphFinalFactAp(
         if (base != factAp.base) return false
         return access.containsAll(factAp.access)
     }
+
+    override fun equalTo(factAp: InitialFactAp): Boolean {
+        factAp as AccessGraphInitialFactAp
+
+        if (base != factAp.base) return false
+        return access == factAp.access
+    }
 }

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/access/cactus/AccessCactus.kt

@@ -73,6 +73,10 @@ class AccessCactus(
     override fun contains(factAp: InitialFactAp): Boolean =
         this.delta(factAp).any { it.isEmpty }
 
+    override fun equalTo(factAp: InitialFactAp): Boolean {
+        TODO("Not yet implemented")
+    }
+
     override fun getStartAccessors(): Set<Accessor> =
         access.allEdges.mapTo(hashSetOf()) { it.accessor }
 

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/access/tree/AccessTree.kt

@@ -84,6 +84,29 @@ class AccessTree(
         return node.isAbstract
     }
 
+    override fun equalTo(factAp: InitialFactAp): Boolean {
+        factAp as AccessPath
+
+        if (base != factAp.base) return false
+
+        val otherAccess = factAp.access
+        if (otherAccess == null) {
+            return access.isEmptyAbstract
+        }
+
+        var node = access
+        for (accessor in otherAccess) {
+            if (accessor == FinalAccessor) {
+                return node.isFinal && node.accessors == null
+            }
+
+            if (node.accessors?.size != 1) return false
+            node = node.getChild(apManager, accessor) ?: return false
+        }
+
+        return node.isEmptyAbstract
+    }
+
     private sealed interface AccessTreeDelta : FinalFactAp.Delta
 
     data object EmptyAccessTreeDelta : AccessTreeDelta {
@@ -273,6 +296,9 @@ class AccessTree(
         val isEmpty: Boolean
             get() = !isAbstract && !isFinal && accessors == null
 
+        val isEmptyAbstract: Boolean
+            get() = isAbstract && !isFinal && accessors == null
+
         private fun accessorIndex(accessor: Accessor): Int {
             if (accessors == null) return -1
             return accessors.binarySearch(accessor)

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/analysis/AnalysisManager.kt

@@ -24,7 +24,8 @@ interface AnalysisManager: LanguageManager {
 
     fun getMethodAnalysisContext(
         methodEntryPoint: MethodEntryPoint,
-        graph: ApplicationGraph<CommonMethod, CommonInst>
+        graph: ApplicationGraph<CommonMethod, CommonInst>,
+        callResolver: MethodCallResolver,
     ): MethodAnalysisContext
 
     fun getMethodCallResolver(

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/analysis/MethodCallSummaryHandler.kt

@@ -14,6 +14,13 @@ import org.seqra.dataflow.ap.ifds.analysis.MethodSequentFlowFunction.TraceInfo
 interface MethodCallSummaryHandler {
     val factTypeChecker: FactTypeChecker
 
+    sealed interface SummaryEdge {
+        val final: FinalFactAp
+
+        data class F2F(val initial: InitialFactAp, override val final: FinalFactAp) : SummaryEdge
+        data class NdF2F(val initial: Set<InitialFactAp>, override val final: FinalFactAp) : SummaryEdge
+    }
+
     fun mapMethodExitToReturnFlowFact(fact: FinalFactAp): List<FinalFactAp>
 
     fun handleZeroToZero(summaryFact: FinalFactAp?): Set<Sequent> {
@@ -28,11 +35,11 @@ interface MethodCallSummaryHandler {
     fun handleZeroToFact(
         currentFactAp: FinalFactAp,
         summaryEffect: SummaryEdgeApplication,
-        summaryFact: FinalFactAp
+        summaryEdge: SummaryEdge,
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact,
+        summaryEdge,
         createSideEffectRequirement = {
             check(it is ExclusionSet.Universe) { "Incorrect refinement" }
             null
@@ -49,11 +56,11 @@ interface MethodCallSummaryHandler {
         initialFactAp: InitialFactAp,
         currentFactAp: FinalFactAp,
         summaryEffect: SummaryEdgeApplication,
-        summaryFact: FinalFactAp
+        summaryEdge: SummaryEdge,
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact,
+        summaryEdge,
         createSideEffectRequirement = { refinement ->
             Sequent.SideEffectRequirement(initialFactAp.refine(refinement))
         }
@@ -67,11 +74,11 @@ interface MethodCallSummaryHandler {
         initialFacts: Set<InitialFactAp>,
         currentFactAp: FinalFactAp,
         summaryEffect: SummaryEdgeApplication,
-        summaryFact: FinalFactAp
+        summaryEdge: SummaryEdge,
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact,
+        summaryEdge,
         createSideEffectRequirement = {
             check(it is ExclusionSet.Universe) { "Incorrect refinement" }
             null
@@ -96,11 +103,11 @@ interface MethodCallSummaryHandler {
     fun handleSummary(
         currentFactAp: FinalFactAp,
         summaryEffect: SummaryEdgeApplication,
-        summaryFact: FinalFactAp,
+        summaryEdge: SummaryEdge,
         createSideEffectRequirement: (refinement: ExclusionSet) -> Sequent?,
         handleSummaryEdge: (initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp) -> Sequent
     ): Set<Sequent> {
-        val mappedSummaryFacts = mapMethodExitToReturnFlowFact(summaryFact)
+        val mappedSummaryFacts = mapMethodExitToReturnFlowFact(summaryEdge.final)
 
         return when (summaryEffect) {
             is SummaryApRefinement -> mappedSummaryFacts.mapNotNullTo(hashSetOf()) { mappedSummaryFact ->

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/trace/MethodForwardTraceResolver.kt

@@ -16,6 +16,7 @@ import org.seqra.dataflow.ap.ifds.analysis.AnalysisManager
 import org.seqra.dataflow.ap.ifds.analysis.MethodAnalysisContext
 import org.seqra.dataflow.ap.ifds.analysis.MethodCallFlowFunction
 import org.seqra.dataflow.ap.ifds.analysis.MethodCallFlowFunction.ZeroCallFact
+import org.seqra.dataflow.ap.ifds.analysis.MethodCallSummaryHandler.SummaryEdge
 import org.seqra.dataflow.ap.ifds.analysis.MethodSequentFlowFunction
 import org.seqra.dataflow.ap.ifds.analysis.MethodSequentFlowFunction.Sequent
 import org.seqra.dataflow.graph.MethodInstGraph
@@ -289,7 +290,7 @@ class MethodForwardTraceResolver(
         callerFact: FinalFactAp,
         methodInitialFactBase: AccessPathBase,
         methodSummaries: List<FactToFact>,
-        handleSummaryEdge: (currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryFact: FinalFactAp) -> Set<Sequent>,
+        handleSummaryEdge: (currentFactAp: FinalFactAp, summaryEffect: SummaryEdgeApplication, summaryEdge: SummaryEdge) -> Set<Sequent>,
     ): Boolean {
         var summaryApplied = false
         val methodInitialFact = callerFact.rebase(methodInitialFactBase)
@@ -302,7 +303,8 @@ class MethodForwardTraceResolver(
 
             for (summaryEdgeEffect in summaryEdgeEffects) {
                 for (methodSummary in summaryEdges) {
-                    val sf = handleSummaryEdge(callerFact, summaryEdgeEffect, methodSummary.factAp)
+                    val summaryEdge = SummaryEdge.F2F(methodSummary.initialFactAp, methodSummary.factAp)
+                    val sf = handleSummaryEdge(callerFact, summaryEdgeEffect, summaryEdge)
                     handleSequentFact(currentEdge, sf)
                     summaryApplied = true
                 }

seqra-dataflow/src/main/kotlin/org/seqra/dataflow/graph/CompactGraphSimulator.kt

@@ -14,9 +14,19 @@ inline fun <reified State : Any> simulateGraph(
     eval: (Int, State) -> State,
 ): Array<State?> {
     if (graph.size == 0) return emptyArray<State?>()
-
     val statesAfter = arrayOfNulls<State>(graph.size)
+    simulateGraph(statesAfter, graph, initialStmtIdx, initialState, merge, eval)
+    return statesAfter
+}
 
+inline fun <reified State : Any> simulateGraph(
+    statesAfter: Array<State?>,
+    graph: CompactGraph,
+    initialStmtIdx: Int,
+    initialState: State,
+    merge: (Int, Int2ObjectMap<State?>) -> State,
+    eval: (Int, State) -> State,
+) {
     val topOrderComparator = CompactGraphTopSort(graph).graphTopOrderNodeComparator(initialStmtIdx)
 
     val enqueuedStmts = BitSet()
@@ -61,6 +71,4 @@ inline fun <reified State : Any> simulateGraph(
             }
         }
     }
-
-    return statesAfter
 }