hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-29 02:35:15 +02:00
Code Issues Packages Projects Releases Wiki Activity

C++: Add more QLDoc.

Browse Source
This commit is contained in:
Mathias Vorreiter Pedersen
2021-06-24 09:57:25 +02:00
parent d70ea5f6e0
commit 656ff4aee9
1 changed files with 18 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
cpp/ql/src/semmle/code/cpp/controlflow/StackVariableReachability.qll
View File

@@ -145,6 +145,17 @@ private Condition getADirectCondition(BasicBlock b) {
result.(LogicalCondition).getCondition().controls(b, result.(LogicalCondition).getTruthValue())
}
/**
* Like the shared dataflow library, the reachability analysis is split into two stages:
* In the first stage, we compute an overapproximation of the possible control-flow paths where we don't
* reason about path conditions. This stage is split into phases: A forward phase (computed by the
* predicates prefixes with `fwd`), and a reverse phase (computed by the predicates prefixed with `rev`).
*
* The forward phease computes the set of control-flow nodes reachable from a given `source` and `v` such
* that `config.isSource(source, v)` holds.
*
* See the QLDoc on `revBbSuccessorEntryReaches0` for a description of what the reverse phase computes.
*/
private predicate fwdBbSuccessorEntryReaches0(
ControlFlowNode source, BasicBlock bb, SemanticStackVariable v,
boolean skipsFirstLoopAlwaysTrueUponEntry, StackVariableReachability config
@@ -162,6 +173,10 @@ private predicate fwdBbSuccessorEntryReaches0(
)
}
/**
* The second phase of the first stages computes, for each `source` and `v` pair such
* that `config.isSource(source, v)`, which sinks are reachable from that `(source, v)` pair.
*/
private predicate revBbSuccessorEntryReaches0(
ControlFlowNode source, BasicBlock bb, SemanticStackVariable v,
boolean skipsFirstLoopAlwaysTrueUponEntry, StackVariableReachability config
@@ -368,7 +383,9 @@ abstract class StackVariableReachability extends string {
}
/**
* Holds if `cond` is a condition with a known truth value in `bb`.
* Gets a condition with a known truth value in `bb` when the control-flow starts at the source
* node `source` and we're tracking reachability using variable `v` (that is,
* `this.isSource(source, v)` holds).
*
* This predicate is `pragma[noopt]` as it seems difficult to get the correct join order for the
* recursive case otherwise: