feat: Enhance summary rewriter and enable alias analysis by default

seqradev · seqradev · commit 5c4eb4b8f5b9 · 2025-11-08T07:41:47.000Z
diff --git a/gradle.properties b/gradle.properties
@@ -3,5 +3,5 @@ seqraOrg=seqra
 seqraBuildVersion=2025.10.01.6b66511
 
 seqraIrVersion=2025.10.09.8af579a
-seqraConfigVersion=2025.10.28.c6855e5
+seqraConfigVersion=2025.11.08.5fe2c2b
 seqraUtilVersion=2025.10.28.b93c206
diff --git a/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/analysis/MethodCallSummaryHandler.kt b/seqra-dataflow/src/main/kotlin/org/seqra/dataflow/ap/ifds/analysis/MethodCallSummaryHandler.kt
@@ -32,7 +32,11 @@ interface MethodCallSummaryHandler {
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact
+        summaryFact,
+        createSideEffectRequirement = {
+            check(it is ExclusionSet.Universe) { "Incorrect refinement" }
+            null
+        }
     ) { initialFactRefinement: ExclusionSet?, summaryFactAp ->
         check(initialFactRefinement == null || initialFactRefinement is ExclusionSet.Universe) {
             "Incorrect refinement"
@@ -49,7 +53,10 @@ interface MethodCallSummaryHandler {
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact
+        summaryFact,
+        createSideEffectRequirement = { refinement ->
+            Sequent.SideEffectRequirement(initialFactAp.refine(refinement))
+        }
     ) { initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp ->
         Sequent.FactToFact(initialFactAp.refine(initialFactRefinement), summaryFactAp, TraceInfo.ApplySummary)
     }
@@ -64,7 +71,11 @@ interface MethodCallSummaryHandler {
     ): Set<Sequent> = handleSummary(
         currentFactAp,
         summaryEffect,
-        summaryFact
+        summaryFact,
+        createSideEffectRequirement = {
+            check(it is ExclusionSet.Universe) { "Incorrect refinement" }
+            null
+        }
     ) { initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp ->
         check(initialFactRefinement == null || initialFactRefinement is ExclusionSet.Universe) {
             "Incorrect refinement"
@@ -86,6 +97,7 @@ interface MethodCallSummaryHandler {
         currentFactAp: FinalFactAp,
         summaryEffect: SummaryEdgeApplication,
         summaryFact: FinalFactAp,
+        createSideEffectRequirement: (refinement: ExclusionSet) -> Sequent?,
         handleSummaryEdge: (initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp) -> Sequent
     ): Set<Sequent> {
         val mappedSummaryFacts = mapMethodExitToReturnFlowFact(summaryFact)
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRAnalysisManager.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRAnalysisManager.kt
@@ -44,7 +44,7 @@ import org.seqra.util.analysis.ApplicationGraph
 
 class JIRAnalysisManager(
     cp: JIRClasspath,
-    private val applyAliasInfo: Boolean = false,
+    private val applyAliasInfo: Boolean = true,
 ) : JIRLanguageManager(cp), TaintAnalysisManager {
     private val lambdaTracker = JIRLambdaTracker()
     private val factTypeChecker = JIRFactTypeChecker(cp)
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallFlowFunction.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallFlowFunction.kt
@@ -310,9 +310,6 @@ class JIRMethodCallFlowFunction(
                     addCallToReturn(factReaderAfterCleaner, aliased, trace)
                 }
             }
-
-            // Skip method invocation
-            return
         }
 
         val cleanedFact = factReaderAfterCleaner.factAp
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallRuleBasedSummaryRewriter.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallRuleBasedSummaryRewriter.kt
@@ -1,17 +1,18 @@
 package org.seqra.dataflow.jvm.ap.ifds.analysis
 
-import mu.KotlinLogging
 import org.seqra.dataflow.ap.ifds.access.ApManager
 import org.seqra.dataflow.ap.ifds.access.FinalFactAp
-import org.seqra.dataflow.configuration.jvm.AssignMark
-import org.seqra.dataflow.configuration.jvm.ContainsMark
+import org.seqra.dataflow.configuration.jvm.Position
+import org.seqra.dataflow.configuration.jvm.RemoveMark
+import org.seqra.dataflow.configuration.jvm.TaintConfigurationItem
+import org.seqra.dataflow.configuration.jvm.TaintMark
 import org.seqra.dataflow.jvm.ap.ifds.CallPositionToJIRValueResolver
-import org.seqra.dataflow.jvm.ap.ifds.JIRMarkAwareConditionExpr
 import org.seqra.dataflow.jvm.ap.ifds.JIRMarkAwareConditionRewriter
-import org.seqra.dataflow.jvm.ap.ifds.removeTrueLiterals
+import org.seqra.dataflow.jvm.ap.ifds.taint.EvaluatedCleanAction
 import org.seqra.dataflow.jvm.ap.ifds.taint.FinalFactReader
+import org.seqra.dataflow.jvm.ap.ifds.taint.TaintCleanActionEvaluator
 import org.seqra.dataflow.jvm.ap.ifds.taint.TaintRulesProvider
-import org.seqra.dataflow.jvm.ap.ifds.taint.resolveAp
+import org.seqra.dataflow.jvm.ap.ifds.taint.UserDefinedRuleInfo
 import org.seqra.ir.api.jvm.cfg.JIRAssignInst
 import org.seqra.ir.api.jvm.cfg.JIRImmediate
 import org.seqra.ir.api.jvm.cfg.JIRInst
@@ -37,61 +38,56 @@ class JIRMethodCallRuleBasedSummaryRewriter(
         )
     }
 
-    private val conditionedActions: List<Pair<List<AssignMark>, JIRMarkAwareConditionExpr?>> by lazy {
+    private data class UserRuleDefinedAction(
+        val rule: TaintConfigurationItem,
+        val positions: List<Position>,
+        val controlledMarks: Set<String>
+    )
+
+    private val userRuleDefinedActions: List<UserRuleDefinedAction> by lazy {
         val method = callExpr.method.method
-        val sourceRules = config.sourceRulesForMethod(method, statement).toList()
-        if (sourceRules.isEmpty()) return@lazy emptyList()
-
-        val conditionedActions = mutableListOf<Pair<List<AssignMark>, JIRMarkAwareConditionExpr?>>()
-
-        for (rule in sourceRules) {
-            val ruleCondition = rule.condition
-            val simplifiedCondition = conditionRewriter.rewrite(ruleCondition)
-            val conditionExpr = when {
-                simplifiedCondition.isFalse -> continue
-                simplifiedCondition.isTrue -> null
-                else -> simplifiedCondition.expr
-            }
 
-            conditionedActions.add(rule.actionsAfter to conditionExpr)
+        val result = mutableListOf<UserRuleDefinedAction>()
+        for (sourceRule in config.sourceRulesForMethod(method, statement)) {
+            val ruleInfo = sourceRule.info as? UserDefinedRuleInfo ?: continue
+
+            val simplifiedCondition = conditionRewriter.rewrite(sourceRule.condition)
+            if (simplifiedCondition.isFalse) continue
+
+            val positions = sourceRule.actionsAfter.map { it.position }
+            result += UserRuleDefinedAction(sourceRule, positions, ruleInfo.relevantTaintMarks)
         }
 
-        conditionedActions
-    }
+        for (cleanRule in config.cleanerRulesForMethod(method, statement)) {
+            val ruleInfo = cleanRule.info as? UserDefinedRuleInfo ?: continue
 
-    fun rewriteSummaryFact(fact: FinalFactAp): Pair<FinalFactAp, FinalFactReader>? {
-        val factReader = FinalFactReader(fact, apManager)
-        for ((actions, cond) in conditionedActions) {
-            val relevantPositiveConditions = hashSetOf<ContainsMark>()
-            cond?.removeTrueLiterals {
-                if (!it.negated) {
-                    relevantPositiveConditions.add(it.condition)
-                }
-                false
-            }
+            val simplifiedCondition = conditionRewriter.rewrite(cleanRule.condition)
+            if (simplifiedCondition.isFalse) continue
 
-            val allRelevantMarks = relevantPositiveConditions.mapTo(hashSetOf()) { it.mark }
+            val positions = cleanRule.actionsAfter.filterIsInstance<RemoveMark>().map { it.position }
+            result += UserRuleDefinedAction(cleanRule, positions, ruleInfo.relevantTaintMarks)
+        }
 
-            for (action in actions) {
-                val markToExclude = allRelevantMarks.toHashSet()
-                markToExclude.remove(action.mark)
+        result
+    }
 
-                val pos = action.position.resolveAp()
-                for (mark in markToExclude) {
-                    if (!factReader.containsPositionWithTaintMark(pos, mark)) {
-                        continue
-                    }
+    fun rewriteSummaryFact(fact: FinalFactAp): Pair<FinalFactAp, FinalFactReader>? {
+        val startFactReader = FinalFactReader(fact, apManager)
 
-                    logger.error("Summary fact handled unproperly due to conflict with rule")
-                    return null
+        val cleanEvaluator = TaintCleanActionEvaluator()
+        var cleanedFact = EvaluatedCleanAction.initial(startFactReader)
+
+        for (ruleDefinedAction in userRuleDefinedActions) {
+            val markToExclude = ruleDefinedAction.controlledMarks.map { TaintMark(it) }
+            for (mark in markToExclude) {
+                for (pos in ruleDefinedAction.positions) {
+                    val removeAction = RemoveMark(mark, pos)
+                    cleanedFact = cleanEvaluator.evaluate(cleanedFact, ruleDefinedAction.rule, removeAction)
                 }
             }
         }
 
-        return fact to factReader
-    }
-
-    companion object {
-        private val logger = KotlinLogging.logger {}
+        val resultFact = cleanedFact.fact ?: return null
+        return resultFact.factAp to resultFact
     }
 }
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallSummaryHandler.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/analysis/JIRMethodCallSummaryHandler.kt
@@ -29,15 +29,21 @@ class JIRMethodCallSummaryHandler(
         currentFactAp: FinalFactAp,
         summaryEffect: MethodSummaryEdgeApplicationUtils.SummaryEdgeApplication,
         summaryFact: FinalFactAp,
+        createSideEffectRequirement: (refinement: ExclusionSet) -> Sequent?,
         handleSummaryEdge: (initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp) -> Sequent
     ): Set<Sequent> {
         val result = hashSetOf<Sequent>()
 
         result += super.handleSummary(
             currentFactAp,
             summaryEffect,
-            summaryFact
+            summaryFact,
+            createSideEffectRequirement,
         ) { initialFactRefinement: ExclusionSet?, summaryFactAp: FinalFactAp ->
+            if (initialFactRefinement != null) {
+                createSideEffectRequirement(initialFactRefinement)?.also { result.add(it) }
+            }
+
             analysisContext.aliasAnalysis?.forEachAliasAfterStatement(statement, summaryFactAp) { aliased ->
                 handleSummaryEdge(initialFactRefinement, aliased)
             }
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/taint/TaintEvaluator.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/taint/TaintEvaluator.kt
@@ -1,5 +1,6 @@
 package org.seqra.dataflow.jvm.ap.ifds.taint
 
+import mu.KotlinLogging
 import org.seqra.dataflow.ap.ifds.AccessPathBase
 import org.seqra.dataflow.ap.ifds.Accessor
 import org.seqra.dataflow.ap.ifds.AnyAccessor
@@ -172,7 +173,8 @@ class TaintCleanActionEvaluator {
         if (!fact.containsPosition(from)) return evc
 
         if (from !is PositionAccess.Simple) {
-            TODO("Remove from complex: $from")
+            logger.error("Unsupported Remove from complex: $from")
+            return evc
         }
 
         val actionInfo = EvaluatedCleanAction.ActionInfo(rule, action)
@@ -190,16 +192,44 @@ class TaintCleanActionEvaluator {
 
         if (!fact.containsPositionWithTaintMark(from, markRestriction)) return evc
 
-        if (from !is PositionAccess.Simple) {
-            TODO("Remove from complex: $from")
-        }
+        val cleanAccessors = from.accessorList() + TaintMarkAccessor(markRestriction.name)
+        val cleanedFacts = clearPosition(cleanAccessors, fact.factAp)
 
-        val factWithoutFinal = fact.factAp.clearAccessor(TaintMarkAccessor(markRestriction.name))
-        val resultFact = factWithoutFinal?.let { fact.replaceFact(it) }
+        if (cleanedFacts.size > 1) {
+            logger.error("Unsupported Remove from complex: $from")
+            return evc
+        }
 
+        val cleanedFact = cleanedFacts.firstOrNull()
+        val resultFact = cleanedFact?.let { fact.replaceFact(it) }
         val actionInfo = EvaluatedCleanAction.ActionInfo(rule, action)
         return EvaluatedCleanAction(resultFact, actionInfo, evc)
     }
+
+    private fun clearPosition(accessors: List<Accessor>, fact: FinalFactAp): List<FinalFactAp> {
+        val head = accessors.first()
+        val tail = accessors.drop(1)
+        if (tail.isEmpty()) {
+            return listOfNotNull(fact.clearAccessor(head))
+        }
+
+        val remaining = listOfNotNull(fact.clearAccessor(head))
+
+        val child = fact.readAccessor(head)
+        val cleanChild = child?.let { clearPosition(tail, it) }
+        val cleanChildWithAccessor = cleanChild?.map { it.prependAccessor(head) }
+
+        return remaining + cleanChildWithAccessor.orEmpty()
+    }
+
+    private fun PositionAccess.accessorList(): List<Accessor> = when (this) {
+        is PositionAccess.Simple -> emptyList()
+        is PositionAccess.Complex -> base.accessorList() + accessor
+    }
+
+    companion object {
+        private val logger = KotlinLogging.logger {}
+    }
 }
 
 class TaintPassActionPreconditionEvaluator(
diff --git a/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/taint/UserDefinedRuleInfo.kt b/seqra-jvm-dataflow/src/main/kotlin/org/seqra/dataflow/jvm/ap/ifds/taint/UserDefinedRuleInfo.kt
@@ -0,0 +1,7 @@
+package org.seqra.dataflow.jvm.ap.ifds.taint
+
+import org.seqra.dataflow.configuration.jvm.serialized.ItemInfo
+
+interface UserDefinedRuleInfo: ItemInfo {
+    val relevantTaintMarks: Set<String>
+}

Original file line number	Diff line number	Diff line change
`@@ -310,9 +310,6 @@ class JIRMethodCallFlowFunction(`
`310`	`310`	`addCallToReturn(factReaderAfterCleaner, aliased, trace)`
`311`	`311`	`}`
`312`	`312`	`}`
`313`		`-`
`314`		`- // Skip method invocation`
`315`		`- return`
`316`	`313`	`}`
`317`	`314`
`318`	`315`	`val cleanedFact = factReaderAfterCleaner.factAp`