C++: Fix spurious ExprNode fanout in DataFlowIntegration.

This commit is contained in:
Anders Schack-Mulligen
2025-03-11 14:15:48 +01:00
parent b5a2f5d3ff
commit ecb5e7ad07
2 changed files with 64 additions and 20 deletions

View File

@@ -1897,6 +1897,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
signature predicate guardChecksSig(
DfInput::Guard g, DfInput::Expr e, boolean branch, State state
);
/**
* Holds if the guard `g` validates the SSA definition `def` upon
* evaluating to `branch`, blocking flow in the given `state`.
*/
signature predicate guardChecksDefSig(
DfInput::Guard g, Definition def, boolean branch, State state
);
}
/**
@@ -1933,6 +1941,20 @@ module Make<LocationSig Location, InputSig<Location> Input> {
guardChecks(g, DfInput::getARead(def), branch, state)
}
private module Barrier = BarrierGuardDefWithState<State, guardChecksSsaDef/4>;
predicate getABarrierNode = Barrier::getABarrierNode/1;
}
/**
* Provides a set of barrier nodes for a guard that validates an expression.
*
* This is expected to be used in `isBarrier`/`isSanitizer` definitions
* in data flow and taint tracking.
*/
module BarrierGuardDefWithState<
StateSig State, WithState<State>::guardChecksDefSig/4 guardChecksSsaDef>
{
/** Gets a node that is safely guarded by the given guard check. */
pragma[nomagic]
Node getABarrierNode(State state) {