Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
97f23dc
Type accessors
Saloed Apr 30, 2026
80803ed
Handle type accessors in tree
Saloed Apr 30, 2026
f767299
Handle type accessors in cactus and automata
Saloed Apr 30, 2026
42fd707
Handle type accessors in analyzer creation
Saloed Apr 30, 2026
579ce8a
Handle type accessors in type checker
Saloed Apr 30, 2026
90ba941
Handle type accessors in summaries feature
Saloed Apr 30, 2026
4e33a28
Initial lambda resolver impl
Saloed Apr 30, 2026
e94fe5b
Fix lambda resolver
Saloed May 5, 2026
c203f31
Cleanup
Saloed May 5, 2026
421312f
Abstraction test 0
Saloed May 5, 2026
c1e8cd1
Abstraction test 1
Saloed May 5, 2026
6c2700b
Abstraction test 2
Saloed May 5, 2026
3dd8a28
Abstraction test 3
Saloed May 5, 2026
e2c6571
Abstraction test 4
Saloed May 5, 2026
4717eab
Abstraction test 5
Saloed May 5, 2026
e41c64f
Abstraction test 6
Saloed May 5, 2026
47ee296
Abstraction test 7
Saloed May 5, 2026
8b29be3
Refactor
Saloed May 5, 2026
a171762
Some work on automata test
Saloed May 5, 2026
be6cff4
Handle unroll next in automata
Saloed May 5, 2026
d0c995a
Better messages
Saloed May 5, 2026
6b9e9cf
Fix any accessor handling
Saloed May 5, 2026
8aaf4fd
Remove incorrect test cases
Saloed May 5, 2026
0274ade
Remove incorrect test cases
Saloed May 5, 2026
511d9de
Add vulnerability ordering
Saloed May 6, 2026
a06a085
Keep all vulnerability facts and resolve multiple traces
Saloed May 6, 2026
6b49b3a
Allow small amount of facts over the limit
Saloed May 6, 2026
097feca
Iterative trace resolver
Saloed May 7, 2026
0a18db2
Fix TraceResolver state processing
Saloed May 7, 2026
3037a08
Add more cancellation points
Saloed May 7, 2026
36c5559
Reuse trace builder
Saloed May 7, 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
Expand Up @@ -61,6 +61,8 @@ sealed interface AccessPathBase {
}
}

sealed interface AbstractionAlwaysUnrollNextAccessor

sealed class Accessor : Comparable<Accessor> {
abstract fun toSuffix(): String
protected abstract val accessorClassId: Int
Expand All @@ -71,15 +73,16 @@ sealed class Accessor : Comparable<Accessor> {
}

return when (this) {
ElementAccessor, FinalAccessor, AnyAccessor, ValueAccessor -> 0 // Definitely equal
ElementAccessor, FinalAccessor, AnyAccessor, ValueAccessor, TypeInfoGroupAccessor -> 0 // Definitely equal
is FieldAccessor -> this.compareToFieldAccessor(other as FieldAccessor)
is TaintMarkAccessor -> this.compareToTaintMarkAccessor(other as TaintMarkAccessor)
is ClassStaticAccessor -> this.compareToClassStaticAccessor(other as ClassStaticAccessor)
is TypeInfoAccessor -> this.compareToTypeInfoAccessor(other as TypeInfoAccessor)
}
}
}

data class TaintMarkAccessor(val mark: String): Accessor() {
data class TaintMarkAccessor(val mark: String): Accessor(), AbstractionAlwaysUnrollNextAccessor {
override fun toSuffix(): String = "![$mark]"
override fun toString(): String = "![$mark]"

Expand Down Expand Up @@ -126,7 +129,7 @@ data object ElementAccessor : Accessor() {
override val accessorClassId: Int = 0
}

data object FinalAccessor : Accessor() {
data object FinalAccessor : Accessor(), AbstractionAlwaysUnrollNextAccessor {
override fun toSuffix(): String = ".\$"
override fun toString(): String = "\$"

Expand All @@ -153,7 +156,7 @@ data class ClassStaticAccessor(val typeName: String) : Accessor() {
}
}

object ValueAccessor : Accessor() {
object ValueAccessor : Accessor(), AbstractionAlwaysUnrollNextAccessor {
override fun toString(): String = "[value]"
override fun toSuffix(): String = ".[value]"

Expand All @@ -165,3 +168,21 @@ inline fun <T : Any> ApManager.tryAnyAccessorOrNull(accessor: Accessor, body: ()
if (!anyAccessorUnrollStrategy.unrollAccessor(accessor)) return null
return body()
}

object TypeInfoGroupAccessor : Accessor(), AbstractionAlwaysUnrollNextAccessor {
override fun toString(): String = "[type]"
override fun toSuffix(): String = ".[type]"

override val accessorClassId: Int = 7
}

data class TypeInfoAccessor(val typeName: String) : Accessor(), AbstractionAlwaysUnrollNextAccessor {
override fun toString(): String = "{$typeName}"
override fun toSuffix(): String = ".{$typeName}"

override val accessorClassId: Int = 8

fun compareToTypeInfoAccessor(other: TypeInfoAccessor): Int {
return typeName.compareTo(other.typeName)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ import org.opentaint.dataflow.ap.ifds.taint.CommonTaintAnalysisContext
import org.opentaint.dataflow.ap.ifds.taint.TaintAnalysisUnitStorage
import org.opentaint.dataflow.ap.ifds.taint.TaintSinkTracker
import org.opentaint.dataflow.ap.ifds.taint.TaintSinkTracker.TaintVulnerability
import org.opentaint.dataflow.ap.ifds.taint.TaintSinkTracker.TaintVulnerabilityWithEndFactRequirement
import org.opentaint.dataflow.ap.ifds.trace.ParallelProcessingContext
import org.opentaint.dataflow.ap.ifds.trace.TraceResolver
import org.opentaint.dataflow.ap.ifds.trace.VulnerabilityChecker
Expand Down Expand Up @@ -219,11 +218,30 @@ class TaintAnalysisUnitRunnerManager(
cancellationTimeout: Duration,
): List<VulnerabilityWithTrace> {
val traceResolver = TraceResolver(entryPoints, this, resolverParams, cancellation)
val traceResolutionContext = object : ParallelProcessingContext<TaintVulnerability, VulnerabilityWithTrace>(
analyzerDispatcher, name = "Trace resolution", vulnerabilities

val states = vulnerabilities.map { TraceResolver.State.Initial(it) }
val traceResolutionContext = object : ParallelProcessingContext<TraceResolver.State, VulnerabilityWithTrace>(
analyzerDispatcher, name = "Trace resolution", states
) {
override fun createUnprocessed(item: TaintVulnerability) =
VulnerabilityWithTrace(item, trace = null)
override fun processItem(item: TraceResolver.State): ProcessingResult<TraceResolver.State, VulnerabilityWithTrace> {
val res = traceResolver.resolveTrace(item)
return when (res) {
is TraceResolver.TraceResolutionResult.InProgress -> {
ProcessingResult.Running(res.state)
}

is TraceResolver.TraceResolutionResult.NoTrace -> {
ProcessingResult.Done(VulnerabilityWithTrace(res.vulnerability, trace = null))
}

is TraceResolver.TraceResolutionResult.Resolved -> {
ProcessingResult.Done(VulnerabilityWithTrace(res.vulnerability, res.trace))
}
}
}

override fun createUnprocessed(item: TraceResolver.State): VulnerabilityWithTrace =
VulnerabilityWithTrace(item.vulnerability, trace = null)

private var prevStats: MethodStats? = null

Expand Down Expand Up @@ -254,10 +272,7 @@ class TaintAnalysisUnitRunnerManager(

return traceResolutionContext.processAll(
progressScope, timeout, cancellationTimeout, cancellation
) { vulnerability ->
val trace = traceResolver.resolveTrace(vulnerability)
VulnerabilityWithTrace(vulnerability, trace)
}
)
}

fun confirmVulnerabilities(
Expand All @@ -269,13 +284,13 @@ class TaintAnalysisUnitRunnerManager(
cancellation.activate()

val confirmed = mutableListOf<TaintVulnerability>()
val unconfirmedVulnerabilities = mutableListOf<TaintVulnerabilityWithEndFactRequirement>()
val unconfirmedVulnerabilities = mutableListOf<TaintVulnerability>()

for (vulnerability in vulnerabilities) {
when (vulnerability) {
is TaintSinkTracker.TaintVulnerabilityUnconditional -> confirmed.add(vulnerability)
is TaintSinkTracker.TaintVulnerabilityWithFact -> confirmed.add(vulnerability)
is TaintVulnerabilityWithEndFactRequirement -> unconfirmedVulnerabilities.add(vulnerability)
if (VulnerabilityChecker.needVerification(vulnerability)) {
unconfirmedVulnerabilities.add(vulnerability)
} else {
confirmed.add(vulnerability)
}
}

Expand Down Expand Up @@ -311,25 +326,27 @@ class TaintAnalysisUnitRunnerManager(

private fun confirmVulnerabilitiesWithCancellation(
entryPoints: Set<CommonMethod>,
vulnerabilities: List<TaintVulnerabilityWithEndFactRequirement>,
vulnerabilities: List<TaintVulnerability>,
timeout: Duration,
cancellationTimeout: Duration,
): List<VerifiedVulnerability> {
val checker = VulnerabilityChecker(entryPoints, this, cancellation)
val vulnConfirmationContext =
object : ParallelProcessingContext<TaintVulnerabilityWithEndFactRequirement, VerifiedVulnerability>(
object : ParallelProcessingContext<TaintVulnerability, VerifiedVulnerability>(
analyzerDispatcher, name = "Vulnerability confirmation", vulnerabilities
) {
override fun createUnprocessed(item: TaintVulnerabilityWithEndFactRequirement): VerifiedVulnerability =
VerifiedVulnerability(
item.vulnerability,
status = VulnerabilityVerificationStatus.UNKNOWN
)
override fun processItem(item: TaintVulnerability): ProcessingResult<TaintVulnerability, VerifiedVulnerability> {
val result = checker.verifyVulnerability(item)
return ProcessingResult.Done(result)
}

override fun createUnprocessed(item: TaintVulnerability): VerifiedVulnerability =
VerifiedVulnerability(item, status = VulnerabilityVerificationStatus.UNKNOWN)
}

return vulnConfirmationContext.processAll(
progressScope, timeout, cancellationTimeout, cancellation
) { checker.verifyVulnerability(it) }
)
}

fun methodCallers(method: CommonMethod): Set<UnitType> =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ import org.opentaint.dataflow.ap.ifds.FactTypeChecker.CompatibilityFilterResult
import org.opentaint.dataflow.ap.ifds.FieldAccessor
import org.opentaint.dataflow.ap.ifds.FinalAccessor
import org.opentaint.dataflow.ap.ifds.TaintMarkAccessor
import org.opentaint.dataflow.ap.ifds.TypeInfoAccessor
import org.opentaint.dataflow.ap.ifds.TypeInfoGroupAccessor
import org.opentaint.dataflow.ap.ifds.ValueAccessor
import org.opentaint.dataflow.util.forEach
import kotlin.collections.plusAssign
Expand Down Expand Up @@ -37,6 +39,8 @@ fun AutomataApManager.createFilter(
is FinalAccessor -> FactTypeChecker.AlwaysRejectFilter
is TaintMarkAccessor -> OnlyFinalAccessorAllowedFilter
is ValueAccessor -> OnlyTaintMarkAccessorAllowedFilter
is TypeInfoGroupAccessor -> FactTypeChecker.AlwaysAcceptFilter
is TypeInfoAccessor -> FactTypeChecker.AlwaysAcceptFilter
else -> error("Unexpected single accessor")
}
},
Expand All @@ -63,6 +67,8 @@ private inline fun <T> AutomataApManager.createFilter(

is TaintMarkAccessor -> filters += singleAccessorFilter(accessor)
is ValueAccessor -> filters += singleAccessorFilter(accessor)
is TypeInfoGroupAccessor -> filters += singleAccessorFilter(accessor)
is TypeInfoAccessor -> filters += singleAccessorFilter(accessor)
is FieldAccessor,
is ClassStaticAccessor -> filters += accessorListFilter(listOf(accessor))

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

import org.opentaint.ir.api.common.cfg.CommonInst
import it.unimi.dsi.fastutil.ints.IntArrayList
import org.opentaint.dataflow.ap.ifds.ExclusionSet
import org.opentaint.dataflow.ap.ifds.FactTypeChecker
import org.opentaint.dataflow.ap.ifds.MethodAnalyzerEdges
import org.opentaint.dataflow.ap.ifds.access.FinalFactAp
import org.opentaint.dataflow.ap.ifds.access.InitialFactAbstraction
import org.opentaint.dataflow.ap.ifds.access.InitialFactAp
import org.opentaint.dataflow.ap.ifds.access.util.AccessorIdx
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.ANY_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.isAlwaysUnrollNext
import org.opentaint.dataflow.ap.ifds.tryAnyAccessorOrNull
import org.opentaint.dataflow.util.ConcurrentReadSafeObject2IntMap
import org.opentaint.dataflow.util.contains
import org.opentaint.dataflow.util.filter
import org.opentaint.dataflow.util.forEach
import org.opentaint.dataflow.util.forEachIntEntry
import org.opentaint.dataflow.util.getOrCreateIndex
import org.opentaint.dataflow.util.getValue
import org.opentaint.dataflow.util.int2ObjectMap
import org.opentaint.dataflow.util.object2IntMap
import org.opentaint.dataflow.util.reversedForEachInt
import org.opentaint.dataflow.util.toBitSet
import org.opentaint.ir.api.common.cfg.CommonInst
import java.util.BitSet

class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFactAbstraction {
Expand Down Expand Up @@ -50,7 +57,7 @@ class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFact
fact: AccessGraphInitialFactAp,
typeChecker: FactTypeChecker
): List<Pair<InitialFactAp, FinalFactAp>> {
val addedBasedFacts = addedFacts.find(fact.base) ?: return emptyList()
val addedBasedFacts = addedFacts.getOrCreate(fact.base)
return addedBasedFacts.registerNew(fact.access, fact.exclusions, typeChecker).map {
Pair(
AccessGraphInitialFactAp(fact.base, it, ExclusionSet.Empty),
Expand All @@ -77,7 +84,7 @@ class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFact
private val analyzedExclusionIndex = int2ObjectMap<BitSet>()

fun addAndAbstract(graph: AccessGraph, typeChecker: FactTypeChecker): List<AccessGraph> = with(graph.manager) {
if (added.isEmpty()) {
if (added.isEmpty() && analyzed.isEmpty()) {
added.put(graph, 0)
addedGraphs.add(graph)
addedIndex.add(graph, 0)
Expand Down Expand Up @@ -107,7 +114,12 @@ class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFact
): List<AccessGraph> = with(graph.manager) {
if (exclusion !is ExclusionSet.Concrete) return emptyList()

val analyzedGraphIdx = analyzed.getValue(graph)
var analyzedGraphIdx = analyzed.getInt(graph)
if (analyzedGraphIdx == ConcurrentReadSafeObject2IntMap.NO_VALUE) {
graph.registerNewAnalyzed()
analyzedGraphIdx = analyzed.getValue(graph)
}

val analyzedGraphExclusion = analyzedExclusion[analyzedGraphIdx]
val newAccessors = exclusion.set.toBitSet { it.idx }.filter { it !in analyzedGraphExclusion }

Expand All @@ -127,6 +139,14 @@ class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFact
): List<AccessGraph> {
val relevantAnalyzedGraphIndices = BitSet()
addedGraph.accessors().forEach { accessor ->
if (accessor == ANY_ACCESSOR_IDX) {
analyzedExclusionIndex.forEachIntEntry { excludedAccessor, graphs ->
if (tryAnyAccessorOrNull(excludedAccessor.accessor) { true } != true) return@forEachIntEntry
relevantAnalyzedGraphIndices.or(graphs)
}
return@forEach
}

val graphsWithAccessorExcluded = analyzedExclusionIndex.get(accessor) ?: return@forEach
relevantAnalyzedGraphIndices.or(graphsWithAccessorExcluded)
}
Expand Down Expand Up @@ -196,12 +216,61 @@ class AutomataInitialFactAbstraction(initialStatement: CommonInst) : InitialFact
}
}

val singleAccessorGraph = emptyGraph().prepend(accessor)
val newGraph = analyzedGraph.concat(singleAccessorGraph)
if (accessor.isAlwaysUnrollNext()) {
val graphs = mutableListOf<AccessGraph>()
unrollNext(graphs, IntArrayList(), delta, accessor)

graphs.forEach { g ->
val newGraph = analyzedGraph.concat(g)
newAnalyzedGraphs.add(newGraph)
}
} else {
val singleAccessorGraph = emptyGraph().prepend(accessor)
val newGraph = analyzedGraph.concat(singleAccessorGraph)

newAnalyzedGraphs.add(newGraph)
}
}
}
}

private fun AutomataApManager.unrollNext(
dst: MutableList<AccessGraph>,
path: IntArrayList,
graph: AccessGraph,
accessor: AccessorIdx
) {
if (path.contains(accessor)) return // note: we don't expect long accessor chains here
path.add(accessor)

try {
val nextGraph = graph.read(accessor)
?: return

newAnalyzedGraphs.add(newGraph)
if (nextGraph.initialNodeIsFinal()) {
dst += rebuildGraph(path)
}

nextGraph.stateSuccessors(nextGraph.initial).forEach { nextAccessor ->
if (nextAccessor.isAlwaysUnrollNext()) {
unrollNext(dst, path, nextGraph, nextAccessor)
} else {
path.add(nextAccessor)
dst += rebuildGraph(path)
path.removeInt(path.lastIndex)
}
}
} finally {
path.removeInt(path.lastIndex)
}
}

private fun AutomataApManager.rebuildGraph(path: IntArrayList): AccessGraph {
var res = emptyGraph()
path.reversedForEachInt { accessor ->
res = res.prepend(accessor)
}
return res
}

private fun AccessGraph.registerNewAnalyzed(): AccessGraph? {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ import org.opentaint.dataflow.ap.ifds.FactTypeChecker
import org.opentaint.dataflow.ap.ifds.FieldAccessor
import org.opentaint.dataflow.ap.ifds.FinalAccessor
import org.opentaint.dataflow.ap.ifds.TaintMarkAccessor
import org.opentaint.dataflow.ap.ifds.TypeInfoAccessor
import org.opentaint.dataflow.ap.ifds.TypeInfoGroupAccessor
import org.opentaint.dataflow.ap.ifds.ValueAccessor
import org.opentaint.dataflow.ap.ifds.access.FinalFactAp
import org.opentaint.dataflow.ap.ifds.access.InitialFactAp
Expand Down Expand Up @@ -1202,6 +1204,8 @@ class AccessCactus(
FinalAccessor -> error("Unexpected FinalAccessor")
AnyAccessor -> low === AnyAccessor
ValueAccessor -> TODO()
is TypeInfoAccessor -> TODO()
TypeInfoGroupAccessor -> TODO()
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,12 @@ import org.opentaint.dataflow.ap.ifds.access.util.AccessorIdx
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.ANY_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.ELEMENT_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.FINAL_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.TYPE_INFO_GROUP_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.VALUE_ACCESSOR_IDX
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.isFieldAccessor
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.isStaticAccessor
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.isTaintMarkAccessor
import org.opentaint.dataflow.ap.ifds.access.util.AccessorInterner.Companion.isTypeInfoAccessor
import org.opentaint.dataflow.util.reversedForEachInt

class AccessPath(
Expand Down Expand Up @@ -291,6 +293,10 @@ class AccessPath(
}

accessor == ANY_ACCESSOR_IDX -> this // todo: All accessors are not supported in tree base ap

accessor == TYPE_INFO_GROUP_ACCESSOR_IDX -> AccessNode(manager, accessor, this)
accessor.isTypeInfoAccessor() -> AccessNode(manager, accessor, this)

else -> error("Unsupported accessor $accessor")
}
}
Expand Down
Loading
Loading