Merge pull request #18485 from MathiasVP/speed-up-cpp-unbounded-write

C++: Speed up the `cpp/unbounded-write` query for an upcoming change
This commit is contained in:
Mathias Vorreiter Pedersen
2025-01-14 10:39:03 +00:00
committed by GitHub
2 changed files with 53 additions and 0 deletions

View File

@@ -1453,3 +1453,25 @@ private module Cached {
}
private import Cached
/**
* Holds if `left < right + k` evaluates to `isLt` given that some guard
* evaluates to `value`.
*
* To find the specific guard that performs the comparison
* use `IRGuards.comparesLt`.
*/
predicate comparesLt(Operand left, Operand right, int k, boolean isLt, AbstractValue value) {
compares_lt(_, left, right, k, isLt, value)
}
/**
* Holds if `left = right + k` evaluates to `isLt` given that some guard
* evaluates to `value`.
*
* To find the specific guard that performs the comparison
* use `IRGuards.comparesEq`.
*/
predicate comparesEq(Operand left, Operand right, int k, boolean isLt, AbstractValue value) {
compares_eq(_, left, right, k, isLt, value)
}

View File

@@ -73,11 +73,42 @@ predicate isSink(DataFlow::Node sink, BufferWrite bw, boolean qualifier) {
unboundedWriteSource(sink.asDefiningArgument(), bw, qualifier)
}
/**
* A configuration that specifies flow from a `FlowSource` to a relational
* comparison.
*
* This configuration is used to speed up the barrier computations in Config.
*/
module BarrierConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) { isSource(source, _) }
predicate isSink(DataFlow::Node sink) {
comparesEq(sink.asOperand(), _, _, true, _) or
comparesLt(sink.asOperand(), _, _, true, _)
}
}
module BarrierFlow = TaintTracking::Global<BarrierConfig>;
import semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon as DataFlowImplCommon
/**
* Holds if `left` is a left operand of some relational comparison that may
* depend on user input.
*/
predicate interestingLessThanOrEqual(Operand left) {
exists(DataFlowImplCommon::NodeEx node |
node.asNode().asOperand() = left and
BarrierFlow::Stages::Stage1::sinkNode(node, _)
)
}
predicate lessThanOrEqual(IRGuardCondition g, Expr e, boolean branch) {
exists(Operand left |
g.comparesLt(left, _, _, true, branch) or
g.comparesEq(left, _, _, true, branch)
|
interestingLessThanOrEqual(left) and
left.getDef().getUnconvertedResultExpression() = e
)
}