diff --git a/gradle.properties b/gradle.properties index bf91833..5f7f049 100644 --- a/gradle.properties +++ b/gradle.properties @@ -2,6 +2,6 @@ seqraOrg=seqra seqraBuildVersion=2025.10.01.6b66511 -seqraIrVersion=2025.12.26.4ec7091 -seqraConfigVersion=2025.12.26.ed75e18 -seqraUtilVersion=2025.12.26.25f1014 +seqraIrVersion=2026.01.15.1f3bbc2 +seqraConfigVersion=2026.01.15.7ea9c38 +seqraUtilVersion=2026.01.15.c5a77a9 diff --git a/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/trace/MethodTraceResolver.kt b/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/trace/MethodTraceResolver.kt index 8ba6cd4..6f8d03b 100644 --- a/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/trace/MethodTraceResolver.kt +++ b/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/trace/MethodTraceResolver.kt @@ -6,6 +6,7 @@ import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap import org.seqra.dataflow.ap.ifds.AccessPathBase import org.seqra.dataflow.ap.ifds.AnalysisRunner import org.seqra.dataflow.ap.ifds.AnalysisUnitRunnerManager +import org.seqra.dataflow.ap.ifds.Edge import org.seqra.dataflow.ap.ifds.Edge.FactToFact import org.seqra.dataflow.ap.ifds.ExclusionSet import org.seqra.dataflow.ap.ifds.MethodAnalyzerEdgeSearcher @@ -1316,8 +1317,10 @@ class MethodTraceResolver( val resolvedCallSummaries = mutableListOf() val methodSummaries = manager.findFactToFactSummaryEdges(callee, startFact.startFactBase) + val applicableMethodSummaries = methodSummaries.filter { isApplicableExitToReturnEdge(it) } + val callerFact = startFact.callerFact - for (summaryEdge in methodSummaries) { + for (summaryEdge in applicableMethodSummaries) { val mappedSummaryFact = summaryEdge.factAp.rebase(callerFact.base) val deltas = callerFact.splitDelta(mappedSummaryFact) @@ -1353,7 +1356,9 @@ class MethodTraceResolver( this += weakestCallSummaries val methodNdSummaries = manager.findFactNDSummaryEdges(callee, startFact.startFactBase) - for (summaryEdge in methodNdSummaries) { + val applicableNDSummaries = methodNdSummaries.filter { isApplicableExitToReturnEdge(it) } + + for (summaryEdge in applicableNDSummaries) { val mappedSummaryFact = summaryEdge.factAp.rebase(callerFact.base) if (!mappedSummaryFact.contains(callerFact)) continue @@ -1402,7 +1407,9 @@ class MethodTraceResolver( startFact: CallPreconditionFact.CallToStart ) { val relevantSummaryEdges = manager.findZeroToFactSummaryEdges(callee, startFact.startFactBase) - for (summaryEdge in relevantSummaryEdges) { + val applicableSummaryEdges = relevantSummaryEdges.filter { isApplicableExitToReturnEdge(it) } + + for (summaryEdge in applicableSummaryEdges) { val mappedSummaryFact = summaryEdge.factAp.rebase(startFact.callerFact.base) if (!mappedSummaryFact.contains(startFact.callerFact)) continue @@ -1418,12 +1425,22 @@ class MethodTraceResolver( } } - private fun selectWeakestEntries(entries: List): List { - val selectedEntries = LinkedList() - for (summary in entries) { - addWeakestEntry(summary, selectedEntries) - } - return selectedEntries + private fun isApplicableExitToReturnEdge(edge: Edge): Boolean { + return !analysisManager.producesExceptionalControlFlow(edge.statement) + } + + private fun selectWeakestEntries(allSummaries: List): List { + val result = mutableListOf() + allSummaries + .groupBy { it.summaryTrace.final.statement } + .values.forEach { entries -> + val selectedEntries = LinkedList() + for (summary in entries) { + addWeakestEntry(summary, selectedEntries) + } + result += selectedEntries + } + return result } private fun addWeakestEntry(entry: CallSummary, selectedEntries: LinkedList) {