Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
6c45307
DeepMarkExclusion
Saloed Jul 24, 2026
87f89cf
Handle deep exclusion in exclusion set
Saloed Jul 24, 2026
8ae1347
Handle deep exclusion in exclusion set
Saloed Jul 24, 2026
534b86b
Handle deep ex in summary
Saloed Jul 24, 2026
9a7a212
Tree set
Saloed Jul 25, 2026
111a37a
Automata set
Saloed Jul 25, 2026
7863a8a
Interner
Saloed Jul 25, 2026
cbe070a
Deep prepend
Saloed Jul 25, 2026
08225aa
Cactus set
Saloed Jul 25, 2026
1e41084
ban deep ex
Saloed Jul 25, 2026
81b7690
Tree abstraction
Saloed Jul 25, 2026
e92f80d
Automata abstraction
Saloed Jul 25, 2026
b4e0a4d
Ban deep ex
Saloed Jul 25, 2026
1e43db2
Ban deep ex
Saloed Jul 25, 2026
fbaa657
Delta
Saloed Jul 25, 2026
ca2be51
ban
Saloed Jul 25, 2026
1d65ca2
split delta
Saloed Jul 25, 2026
129a19f
automata delta
Saloed Jul 25, 2026
0e2ed01
summary storage
Saloed Jul 25, 2026
5c522ba
summary handler
Saloed Jul 25, 2026
21412cc
ban
Saloed Jul 25, 2026
5e905d6
minor
Saloed Jul 25, 2026
bc9f731
serializer
Saloed Jul 25, 2026
0f4b9e1
minor
Saloed Jul 25, 2026
8920999
exclude deep
Saloed Jul 25, 2026
4707021
ban
Saloed Jul 25, 2026
71d5d96
serializer
Saloed Jul 25, 2026
8926db1
Cleaner
Saloed Jul 25, 2026
077707a
minor
Saloed Jul 25, 2026
2d225c9
tests
Saloed Jul 25, 2026
c7484b7
minor
Saloed Jul 25, 2026
89741f9
fix(dataflow): deep mark exclusions survive summary application
misonijnik Jul 28, 2026
3e638af
test(dataflow): isolate what decides a cleaner's field sensitivity
misonijnik Jul 28, 2026
677533c
refactor(dataflow): AccessNode abstraction carries an excluded-mark a…
misonijnik Jul 28, 2026
a9e3ba3
feat(dataflow): structural deep clean on the tree, with its laws pinned
misonijnik Jul 28, 2026
25cc84c
fix(dataflow): the starred clean is field-sensitive across summaries …
misonijnik Jul 28, 2026
5e4ded4
refactor(dataflow): tree merge sites assert the deep-free invariant
misonijnik Jul 28, 2026
d0f4740
feat(dataflow): persist the abstraction annotation; version the summa…
misonijnik Jul 28, 2026
2e6fe72
refactor(dataflow): prune dead annotation API; defaults no longer hid…
misonijnik Jul 28, 2026
d767b7b
fix(dataflow): the deep-clean claim survives partitions and abstract …
misonijnik Jul 28, 2026
f283fd6
Refactor cleaner effects out of analysis exclusions
misonijnik Jul 28, 2026
3526e2b
Separate demand state from cleaner representations
misonijnik Jul 28, 2026
b17833f
Model cleaners with position access
misonijnik Jul 28, 2026
8e62869
Add exhaustive cleaner DSL analysis tests
misonijnik Jul 28, 2026
db454a4
Add cleaner control-flow scenarios
misonijnik Jul 28, 2026
ba2fdd0
test(dataflow): expose cleaner abstraction leaks
misonijnik Jul 28, 2026
dffa44c
fix(dataflow): preserve cleaner and wildcard semantics
misonijnik Jul 28, 2026
03e574a
test(dataflow): reject exact sources for wildcard demand
misonijnik Jul 28, 2026
878ec79
test(dataflow): distinguish exact and AnyField cleanup reach
misonijnik Jul 28, 2026
6a9e099
fix(dataflow): reject exact sources for wildcard demand
misonijnik Jul 28, 2026
8cb6b8a
fix(dataflow): separate automaton cleanup reach
misonijnik Jul 28, 2026
6c2f09b
fix(dataflow): preserve cleanup reach in summaries
misonijnik Jul 28, 2026
0cec5d1
refactor(dataflow): separate AnyField mark exclusions
misonijnik Jul 29, 2026
4050182
refactor(dataflow): remove Cactus exclusion wrapper
misonijnik Jul 29, 2026
7e22d5f
refactor(dataflow): store cleaner state in access values
misonijnik Jul 29, 2026
97473a0
refactor(dataflow): remove stale cleaner compatibility code
misonijnik Jul 29, 2026
5361e30
fix(dataflow): preserve empty automata summaries
misonijnik Jul 29, 2026
43d453b
feat(querylang): parse the star operator and thread it through the pi…
misonijnik Jul 23, 2026
c79fc90
feat(querylang): starred source, sanitizer and sink semantics
misonijnik Jul 23, 2026
f556149
feat(go-querylang): star operator parity for Go, and real any-field r…
misonijnik Jul 23, 2026
14653b5
refactor(querylang): settle on the $*VAR star syntax
misonijnik Jul 23, 2026
6df4a58
test(querylang): exhaustive star-operator matrix and root-cause analysis
misonijnik Jul 23, 2026
dc0f545
test(querylang): deep-exclusion composition samples for starred cleans
misonijnik Jul 23, 2026
0953c43
test(querylang): cover starred sanitizer assignments
misonijnik Jul 29, 2026
a555f61
test(dataflow): align cleaner coverage with access DSL
misonijnik Jul 29, 2026
d5139a1
test(dataflow): isolate cleaner matrix from object sink compatibility
misonijnik Jul 30, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
package org.opentaint.dataflow.configuration

enum class TaintCleanReach {
Exact,
ExactAndAnyField,
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,10 +31,25 @@ sealed interface GoSerializedAssignAction : GoSerializedAction {
}
}

data class GoSerializedCleanAction(
val taintKind: String? = null,
val pos: PositionBaseWithModifiers,
) : GoSerializedAction
sealed interface GoSerializedCleanAction : GoSerializedAction {
val taintKind: String?
val pos: PositionBaseWithModifiers

data class Direct(
override val taintKind: String? = null,
override val pos: PositionBaseWithModifiers,
) : GoSerializedCleanAction

data class AnyAccessor(
override val taintKind: String? = null,
override val pos: PositionBaseWithModifiers,
) : GoSerializedCleanAction

companion object {
operator fun invoke(taintKind: String? = null, pos: PositionBaseWithModifiers): GoSerializedCleanAction =
Direct(taintKind, pos)
}
}

data class GoSerializedPassAction(
val taintKind: String? = null,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package org.opentaint.dataflow.configuration.jvm

import org.opentaint.dataflow.configuration.CommonTaintAction
import org.opentaint.dataflow.configuration.CommonTaintAssignAction
import org.opentaint.dataflow.configuration.TaintCleanReach

sealed interface Action: CommonTaintAction

Expand All @@ -28,4 +29,5 @@ data class RemoveAllMarks(
data class RemoveMark(
val mark: TaintMark,
val position: Position,
val reach: TaintCleanReach = TaintCleanReach.Exact,
) : Action
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package org.opentaint.dataflow.configuration.jvm.serialized

import kotlinx.serialization.Serializable
import org.opentaint.dataflow.configuration.TaintCleanReach

sealed interface SerializedAction

Expand All @@ -15,6 +16,7 @@ data class SerializedTaintAssignAction(
data class SerializedTaintCleanAction(
val taintKind: String? = null,
val pos: PositionBaseWithModifiers,
val reach: TaintCleanReach = TaintCleanReach.Exact,
): SerializedAction

@Serializable
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import com.charleskorn.kaml.YamlNode
import com.charleskorn.kaml.YamlScalar
import kotlinx.serialization.DeserializationStrategy
import kotlinx.serialization.KSerializer
import kotlinx.serialization.SerialName
import kotlinx.serialization.Serializable
import kotlinx.serialization.descriptors.PrimitiveKind
import kotlinx.serialization.descriptors.PrimitiveSerialDescriptor
Expand Down Expand Up @@ -141,6 +142,13 @@ sealed interface SerializedCondition {
val pos: PositionBaseWithModifiers,
): SerializedCondition

@Serializable
data class ContainsMarkOnAnyField(
@SerialName("taintedOnAnyField")
val tainted: String,
val pos: PositionBaseWithModifiers,
): SerializedCondition

@Serializable
data class NumberOfArgs(val numberOfArgs: Int): SerializedCondition

Expand Down Expand Up @@ -223,6 +231,7 @@ class SerializedConditionSerializer :
companion object {
private val serializerByProperty = mapOf(
"tainted" to SerializedCondition.ContainsMark.serializer(),
"taintedOnAnyField" to SerializedCondition.ContainsMarkOnAnyField.serializer(),
"anyOf" to SerializedCondition.Or.serializer(),
"allOf" to SerializedCondition.And.serializer(),
"not" to SerializedCondition.Not.serializer(),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ import org.opentaint.dataflow.ap.ifds.MethodAnalyzer.FactToFactSub
import org.opentaint.dataflow.ap.ifds.MethodAnalyzer.MethodCallHandler
import org.opentaint.dataflow.ap.ifds.MethodAnalyzer.MethodCallResolutionFailureHandler
import org.opentaint.dataflow.ap.ifds.MethodSummaryEdgeApplicationUtils.SummaryEdgeApplication
import org.opentaint.dataflow.ap.ifds.MethodSummaryEdgeApplicationUtils.SummaryEdgeApplication.SummaryExclusionRefinement
import org.opentaint.dataflow.ap.ifds.access.ApManager
import org.opentaint.dataflow.ap.ifds.access.FinalFactAp
import org.opentaint.dataflow.ap.ifds.access.InitialFactAp
Expand Down Expand Up @@ -1242,7 +1241,10 @@ class NormalMethodAnalyzer(
ndSummaryInitial.isEmpty() -> {
summaryHandler.handleZeroToFact(
currentEdgeFactAp,
SummaryExclusionRefinement(ExclusionSet.Universe),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = ExclusionSet.Universe,
),
summaryEdge.summaryEdge()
)
}
Expand All @@ -1252,7 +1254,10 @@ class NormalMethodAnalyzer(
summaryHandler.handleFactToFact(
initialFact,
currentEdgeFactAp,
SummaryExclusionRefinement(initialFact.exclusions),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = initialFact.exclusions,
),
summaryEdge.summaryEdge()
)
}
Expand All @@ -1261,7 +1266,10 @@ class NormalMethodAnalyzer(
summaryHandler.handleNDFactToFact(
ndSummaryInitial,
currentEdgeFactAp,
SummaryExclusionRefinement(ExclusionSet.Universe),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = ExclusionSet.Universe,
),
summaryEdge.summaryEdge()
)
}
Expand All @@ -1275,7 +1283,10 @@ class NormalMethodAnalyzer(
summaryHandler.handleFactToFact(
currentEdge.initialFactAp,
currentEdgeFactAp,
SummaryExclusionRefinement(currentEdge.initialFactAp.exclusions),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = currentEdge.initialFactAp.exclusions,
),
summaryEdge.summaryEdge()
)
}
Expand All @@ -1284,7 +1295,10 @@ class NormalMethodAnalyzer(
summaryHandler.handleNDFactToFact(
ndSummaryInitial,
currentEdgeFactAp,
SummaryExclusionRefinement(ExclusionSet.Universe),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = ExclusionSet.Universe,
),
summaryEdge.summaryEdge()
)
}
Expand All @@ -1295,7 +1309,10 @@ class NormalMethodAnalyzer(
summaryHandler.handleNDFactToFact(
ndSummaryInitial + currentEdge.initialFacts,
currentEdgeFactAp,
SummaryExclusionRefinement(ExclusionSet.Universe),
SummaryEdgeApplication(
accessDelta = null,
initialFactExclusions = ExclusionSet.Universe,
),
summaryEdge.summaryEdge()
)
}
Expand Down Expand Up @@ -1882,4 +1899,4 @@ private class TaintMarkGatherer: FactTypeChecker.FactApFilter {
else -> FactTypeChecker.FilterResult.FilterNext(this)
}
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,20 @@ import org.opentaint.dataflow.ap.ifds.access.FinalFactAp
import org.opentaint.dataflow.ap.ifds.access.InitialFactAp

object MethodSummaryEdgeApplicationUtils {
sealed interface SummaryEdgeApplication {
data class SummaryApRefinement(val delta: FinalFactAp.Delta) : SummaryEdgeApplication
data class SummaryExclusionRefinement(val exclusion: ExclusionSet) : SummaryEdgeApplication
/**
* The two independent refinements selected while matching a summary edge.
*
* [accessDelta] belongs to the access-path representation. [initialFactExclusions] belongs to
* demand analysis and is present only for an empty access delta. Synthetic ND applications
* may supply only [initialFactExclusions].
*/
data class SummaryEdgeApplication(
val accessDelta: FinalFactAp.Delta?,
val initialFactExclusions: ExclusionSet?,
) {
init {
require(accessDelta != null || initialFactExclusions != null)
}
}

fun tryApplySummaryEdge(
Expand All @@ -15,11 +26,16 @@ object MethodSummaryEdgeApplicationUtils {
): List<SummaryEdgeApplication> =
methodInitialFactAp.delta(methodSummaryInitialFactAp).map { delta ->
if (delta.isEmpty) {
SummaryEdgeApplication.SummaryExclusionRefinement(
methodInitialFactAp.exclusions.union(methodSummaryInitialFactAp.exclusions)
SummaryEdgeApplication(
accessDelta = delta,
initialFactExclusions =
methodInitialFactAp.exclusions.union(methodSummaryInitialFactAp.exclusions),
)
} else {
SummaryEdgeApplication.SummaryApRefinement(delta)
SummaryEdgeApplication(
accessDelta = delta,
initialFactExclusions = null,
)
}
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,160 @@
package org.opentaint.dataflow.ap.ifds.access

import org.opentaint.dataflow.ap.ifds.ExclusionSet
import org.opentaint.dataflow.ap.ifds.access.util.AccessorIdx

/**
* Marks excluded from future materialization of an AnyField abstraction.
*
* An AnyField cleaner removes every currently materialized matching mark and records here what
* must remain excluded if the fact later grows. Tree stores the value on abstract nodes; Automata
* and Cactus store it on their final access values. Initial facts never carry it.
*
* Each mark carries the minimum relative depth below the AnyField at which it is excluded:
*
* - [marksFromDepth1] applies to a direct mark child and everything deeper.
* - [marksFromDepth2] preserves a direct mark child and applies after one intervening accessor.
*
* Arrays are sorted and disjoint. [create] returns `null` for an empty tree annotation; root-only
* representations use [Empty] as their explicit neutral value.
*/
class AnyFieldMarkExclusions private constructor(
@JvmField val marksFromDepth1: IntArray,
@JvmField val marksFromDepth2: IntArray,
) {
private val hash: Int = marksFromDepth1.contentHashCode() * 31 + marksFromDepth2.contentHashCode()

override fun hashCode(): Int = hash

override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is AnyFieldMarkExclusions) return false
if (hash != other.hash) return false
return marksFromDepth1.contentEquals(other.marksFromDepth1)
&& marksFromDepth2.contentEquals(other.marksFromDepth2)
}

operator fun contains(mark: AccessorIdx): Boolean =
marksFromDepth1.binarySearch(mark) >= 0 || marksFromDepth2.binarySearch(mark) >= 0

val isEmpty: Boolean
get() = marksFromDepth1.isEmpty() && marksFromDepth2.isEmpty()

/** A base-level any-field clean starts applying below one concrete accessor. */
fun add(mark: AccessorIdx): AnyFieldMarkExclusions = addMarkFromDepth2(mark)

internal infix fun then(other: AnyFieldMarkExclusions): AnyFieldMarkExclusions =
then(this, other) ?: Empty

internal infix fun join(other: AnyFieldMarkExclusions): AnyFieldMarkExclusions =
join(this, other) ?: Empty

private fun allMarks(): IntArray = (marksFromDepth1 + marksFromDepth2).also { it.sort() }

/**
* The claim as seen from any position at least one accessor below the annotated node:
* everything below such a position is at depth >= 2 relative to the annotated node, so every
* claimed mark — depth-1 and depth-2 alike — applies from relative depth 1 there.
*/
fun collapseToDepth1(): AnyFieldMarkExclusions =
if (marksFromDepth2.isEmpty()) this else AnyFieldMarkExclusions(allMarks(), EMPTY)

override fun toString(): String = buildString {
append("!*{d1=")
append(marksFromDepth1.joinToString(","))
append(";d2=")
append(marksFromDepth2.joinToString(","))
append("}")
}

companion object {
private val EMPTY = IntArray(0)
val Empty = AnyFieldMarkExclusions(EMPTY, EMPTY)

/**
* [marksFromDepth1] and [marksFromDepth2] must each be sorted; a mark present in both is
* kept at depth 1. Alternative executions must instead combine through [join], which
* resolves the conflict in the weaker direction.
*/
fun create(marksFromDepth1: IntArray, marksFromDepth2: IntArray): AnyFieldMarkExclusions? {
val d2 = if (marksFromDepth2.any { marksFromDepth1.binarySearch(it) >= 0 }) {
marksFromDepth2.filter { marksFromDepth1.binarySearch(it) < 0 }.toIntArray()
} else {
marksFromDepth2
}

if (marksFromDepth1.isEmpty() && d2.isEmpty()) return null
return AnyFieldMarkExclusions(marksFromDepth1, d2)
}

private fun fromDepth1(mark: AccessorIdx): AnyFieldMarkExclusions = AnyFieldMarkExclusions(intArrayOf(mark), EMPTY)

private fun fromDepth2(mark: AccessorIdx): AnyFieldMarkExclusions = AnyFieldMarkExclusions(EMPTY, intArrayOf(mark))

fun AnyFieldMarkExclusions?.addMarkFromDepth1(mark: AccessorIdx): AnyFieldMarkExclusions {
if (this == null) return fromDepth1(mark)
if (marksFromDepth1.binarySearch(mark) >= 0) return this
// depth 1 is the stronger claim: it absorbs a depth-2 entry for the same mark
val d1 = (marksFromDepth1 + mark).also { it.sort() }
val d2 = if (marksFromDepth2.binarySearch(mark) >= 0) {
marksFromDepth2.filter { it != mark }.toIntArray()
} else {
marksFromDepth2
}
return AnyFieldMarkExclusions(d1, d2)
}

fun AnyFieldMarkExclusions?.addMarkFromDepth2(mark: AccessorIdx): AnyFieldMarkExclusions {
if (this == null) return fromDepth2(mark)
if (contains(mark)) return this
val d2 = (marksFromDepth2 + mark).also { it.sort() }
return AnyFieldMarkExclusions(marksFromDepth1, d2)
}

/**
* The join of two alternative executions meeting at the SAME abstract node: a mark
* survives only when both alternatives exclude it, and at the weaker of the two depths
* (max — a claim both alternatives make only from depth 2 cannot be strengthened to
* depth 1).
*
* The abstraction state itself joins with "not abstract" as the identity: when only one
* operand is abstract, all abstraction (and its annotation) comes from that operand —
* callers handle that case and reach here only with two abstract operands.
*/
fun join(a: AnyFieldMarkExclusions?, b: AnyFieldMarkExclusions?): AnyFieldMarkExclusions? {
if (a == null || b == null) return null
if (a == b) return a

val d1 = a.marksFromDepth1.filter { b.marksFromDepth1.binarySearch(it) >= 0 }.toIntArray()
val d2 = mutableListOf<Int>()
for (mark in a.allMarks()) {
if (d1.binarySearch(mark) >= 0) continue
if (b.contains(mark)) d2.add(mark)
}
return create(d1, d2.toIntArray())
}

/**
* Sequential composition of two claims that BOTH hold: the caller had already cleaned one
* mark when the callee's summary, whose exit abstraction continues the same object,
* cleaned another. Marks union; a mark claimed at both depths keeps the stronger (min —
* depth 1 covers everything depth 2 does).
*/
fun then(a: AnyFieldMarkExclusions?, b: AnyFieldMarkExclusions?): AnyFieldMarkExclusions? {
if (a == null) return b
if (b == null) return a
if (a == b) return a

val d1 = (a.marksFromDepth1.toSet() + b.marksFromDepth1.toSet()).toIntArray().also { it.sort() }
val d2 = (a.marksFromDepth2.toSet() + b.marksFromDepth2.toSet())
.filter { d1.binarySearch(it) < 0 }
.toIntArray().also { it.sort() }
return create(d1, d2)
}
}
}

internal fun AnyFieldMarkExclusions.forExclusions(
exclusions: ExclusionSet,
): AnyFieldMarkExclusions =
if (exclusions is ExclusionSet.Universe) AnyFieldMarkExclusions.Empty else this
Loading
Loading