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

Merge branch 'rc/3.2' into mergeback-2021-07-21

Browse Source
This commit is contained in:
Mathias Vorreiter Pedersen
2021-07-21 10:23:58 +02:00
parent 46fbb2a3cc 2d9600de4a
commit 6d0290809d
20 changed files with 166 additions and 682 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
cpp/ql/src/semmle/code/cpp/controlflow/DefinitionsAndUses.qll
View File

@@ -208,7 +208,7 @@ private predicate bbSuccessorEntryReachesDefOrUse(
boolean skipsFirstLoopAlwaysTrueUponEntry
) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant0(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
bbSuccessorEntryReachesLoopInvariant(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry)
|
bbEntryReachesDefOrUseLocally(succ, v, defOrUse) and

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

@@ -3,250 +3,7 @@
* reachability involving stack variables.
*/
private import semmle.code.cpp.controlflow.Guards
private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
/** A `GuardCondition` which appear in a control-flow path to a sink. */
abstract private class LogicalGuardCondition extends GuardCondition {
LogicalGuardCondition() {
// Either the `GuardCondition` is part of the path from a source to a sink
revBbSuccessorEntryReaches0(_, this.getBasicBlock(), _, _, _)
or
// or it controls the basic block that contains the source node.
this.controls(any(BasicBlock bb | fwdBbEntryReachesLocally(bb, _, _, _)), _)
}
/**
* Holds if the truth of this logical expression having value `wholeIsTrue`
* implies that the truth of the child expression `part` has truth value `partIsTrue`.
*/
abstract predicate impliesCondition(
LogicalGuardCondition e, boolean testIsTrue, boolean condIsTrue
);
}
private class BinaryLogicalGuardCondition extends LogicalGuardCondition, BinaryLogicalOperation {
override predicate impliesCondition(
LogicalGuardCondition e, boolean testIsTrue, boolean condIsTrue
) {
this.impliesValue(e, testIsTrue, condIsTrue)
}
}
private class VariableGuardCondition extends LogicalGuardCondition, VariableAccess {
override predicate impliesCondition(
LogicalGuardCondition e, boolean testIsTrue, boolean condIsTrue
) {
this = e and
(
testIsTrue = true and condIsTrue = true
or
testIsTrue = false and condIsTrue = false
)
}
}
private class NotGuardCondition extends LogicalGuardCondition, NotExpr {
override predicate impliesCondition(
LogicalGuardCondition e, boolean testIsTrue, boolean condIsTrue
) {
e = this.getOperand() and
(
testIsTrue = true and
condIsTrue = false
or
testIsTrue = false and
condIsTrue = true
)
}
}
private newtype TCondition =
MkCondition(LogicalGuardCondition guard, boolean testIsTrue) { testIsTrue = [false, true] }
private class Condition extends MkCondition {
boolean testIsTrue;
LogicalGuardCondition guard;
Condition() { this = MkCondition(guard, testIsTrue) }
/**
* Holds if this condition having the value `this.getTruthValue()` implies that `cond` has truth
* value `cond.getTruthValue()`.
*/
string toString() { result = guard.toString() + " == " + testIsTrue.toString() }
/** Gets the value of this `Condition`. */
boolean getTruthValue() { result = testIsTrue }
LogicalGuardCondition getCondition() { result = guard }
pragma[nomagic]
predicate impliesCondition(Condition cond) {
exists(LogicalGuardCondition other |
other = cond.getCondition() and
this.getCondition()
.impliesCondition(globalValueNumber(other).getAnExpr(),
pragma[only_bind_into](pragma[only_bind_out](testIsTrue)),
pragma[only_bind_into](pragma[only_bind_out](cond.getTruthValue())))
)
}
/** Gets the negated expression represented by this `Condition`, if any. */
private Condition negate() {
result.getCondition() = guard and
result.getTruthValue() = testIsTrue.booleanNot()
}
/**
* Holds if this condition having the value `this.getTruthValue()` implies that `cond` cannot have
* the truth value `cond.getTruthValue()`.
*/
final predicate refutesCondition(Condition cond) { this.impliesCondition(cond.negate()) }
/** Gets the `Location` of the expression that generated this `Condition`. */
Location getLocation() { result = guard.getLocation() }
}
/**
* Gets a `Condition` that controls `b`. That is, to enter `b` the condition must hold.
*/
private Condition getADirectCondition(BasicBlock b) {
result.getCondition().controls(b, result.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
) {
fwdBbEntryReachesLocally(bb, v, source, config) and
skipsFirstLoopAlwaysTrueUponEntry = false
or
exists(BasicBlock pred, boolean predSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant0(pred, bb, predSkipsFirstLoopAlwaysTrueUponEntry,
skipsFirstLoopAlwaysTrueUponEntry)
|
// Note we cannot filter out barriers at this point.
// See the comment in `revBbSuccessorEntryReaches0` for an explanation why,
fwdBbSuccessorEntryReaches0(source, pred, v, predSkipsFirstLoopAlwaysTrueUponEntry, config)
)
}
/**
* 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
) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
fwdBbSuccessorEntryReaches0(source, bb, v, skipsFirstLoopAlwaysTrueUponEntry, config) and
bbSuccessorEntryReachesLoopInvariant0(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry)
|
revBbEntryReachesLocally(succ, v, _, config) and
succSkipsFirstLoopAlwaysTrueUponEntry = false
or
// Note: We cannot rule out a successor block that contain a barrier here (like we do later in
// `bbSuccessorEntryReaches`) as we might later discover that the only way to get through a piece of
// code is through that barrier, and we want to discover this in
// `bbSuccessorEntryReachesLoopInvariant`. As an example, consider this piece of code:
// ```
// if(b) { (1) source(); }
// (2) if(b) { (3) barrier(); }
// (4) sink();
// ```
// here, we want the successor relation to contain:
// 1 -> {2}, 2 -> {3, 4}
// since the second stage will deduce that the edge (2) -> (3) is unconditional (as b is always true
// if we start at `source()`), and so there is actually no path from (1) to (4) without going through
// a barrier.
revBbSuccessorEntryReaches0(source, succ, v, succSkipsFirstLoopAlwaysTrueUponEntry, config)
)
}
private predicate successorExitsLoop(BasicBlock pred, BasicBlock succ, Loop loop) {
pred.getASuccessor() = succ and
bbDominates(loop.getStmt(), pred) and
not bbDominates(loop.getStmt(), succ)
}
private predicate successorExitsFirstDisjunct(BasicBlock pred, BasicBlock succ) {
exists(LogicalOrExpr orExpr | orExpr instanceof GuardCondition |
pred.getAFalseSuccessor() = succ and
pred.contains(orExpr.getLeftOperand())
)
}
/**
* When we exit a loop, we filter out the conditions that arise from the loop's guard.
* To see why this is necessary, consider this example:
* ```
* (1) source();
* while (b) { (2) ... }
* (3) sink();
* ```
* If we keep all the conditions when we transition from (2) to (3) we learn that `b` is true at
* (3), but since we exited the loop we also learn that `b` is false at 3.
* Thus, when we transition from (2) to (3) we discard all those conditions that are true at (2),
* but NOT true at (3).
*/
private predicate isLoopCondition(LogicalGuardCondition cond, BasicBlock pred, BasicBlock bb) {
exists(Loop loop, boolean testIsTrue | successorExitsLoop(pred, bb, loop) |
// the resulting `Condition` holds inside the loop
cond.controls(pred, testIsTrue) and
// but not prior to the loop.
not cond.controls(loop.getBasicBlock(), testIsTrue)
)
}
/**
* When we leave the first disjunct we throw away the condition that says the the first disjunct is
* false. To see why this is necessary, consider this example:
* ```
* if((1) b1 || (2) b2) { (3) ... }
* ```
* it holds that `b1 == false` controls (2), and since (2) steps to (3) we learn that `b1 == false `
* holds at (3). So we filter out the conditions that we learn from leaving taking the false
* branch in a disjunction.
*/
private predicate isDisjunctionCondition(LogicalGuardCondition cond, BasicBlock pred, BasicBlock bb) {
exists(boolean testIsTrue | successorExitsFirstDisjunct(pred, bb) |
// the resulting `Condition` holds after evaluating the left-hand side
cond.controls(bb, testIsTrue) and
// but not before evaluating the left-hand side.
not cond.controls(pred, testIsTrue)
)
}
private predicate isLoopVariantCondition(LogicalGuardCondition cond, BasicBlock pred, BasicBlock bb) {
exists(Loop loop |
bb.getEnd() = loop.getCondition() and
pred.getASuccessor() = bb and
bbDominates(bb, pred) and
loopVariant(cond.getAChild*(), loop)
)
}
private predicate loopVariant(VariableAccess e, Loop loop) {
exists(SsaDefinition d | d.getAUse(e.getTarget()) = e |
d.getAnUltimateDefiningValue(e.getTarget()) = loop.getCondition().getAChild*() or
d.getAnUltimateDefiningValue(e.getTarget()).getEnclosingStmt().getParent*() = loop.getStmt() or
d.getAnUltimateDefiningValue(e.getTarget()) = loop.(ForStmt).getUpdate().getAChild*()
)
}
import cpp
/**
* A reachability analysis for control-flow nodes involving stack variables.
@@ -303,8 +60,7 @@ abstract class StackVariableReachability extends string {
* ```
*
* In addition to using a better performing implementation, this analysis
* accounts for loops where the condition is provably true upon entry, and discards paths that require
* an infeasible combination of guard conditions (for example, `if(b) { ... }` and `if(!b) { ... }`).
* accounts for loops where the condition is provably true upon entry.
*/
predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
/*
@@ -324,184 +80,46 @@ abstract class StackVariableReachability extends string {
j > i and
sink = bb.getNode(j) and
isSink(sink, v) and
not isBarrier(bb.getNode(pragma[only_bind_into]([i + 1 .. j - 1])), v)
not exists(int k | isBarrier(bb.getNode(k), v) | k in [i + 1 .. j - 1])
)
or
not exists(int k | isBarrier(bb.getNode(k), v) | k > i) and
bbSuccessorEntryReaches(source, bb, v, sink, _)
)
}
private Condition getASinkCondition(SemanticStackVariable v) {
exists(BasicBlock bb |
revBbEntryReachesLocally(bb, v, _, this) and
result.getCondition().controls(bb, result.getTruthValue())
)
}
private Condition getABarrierCondition(SemanticStackVariable v) {
exists(BasicBlock bb |
isBarrier(bb.getANode(), v) and
result.getCondition().controls(bb, result.getTruthValue())
)
}
/**
* 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:
* revBbSuccessorEntryReaches0(bb) -> getASuccessor -> prev_delta ->
* revBbSuccessorEntryReaches0(pred) -> {isLoopCondition, isDisjunctionCondition, isLoopVariantCondition}
*/
pragma[noopt]
private Condition getACondition(ControlFlowNode source, SemanticStackVariable v, BasicBlock bb) {
revBbSuccessorEntryReaches0(source, bb, v, _, this) and
(
result = getADirectCondition(bb) and
(
exists(Condition c |
c = getASinkCondition(v) and
result.refutesCondition(c)
)
or
exists(Condition c |
c = getABarrierCondition(v) and
result.impliesCondition(c)
)
)
or
exists(BasicBlock pred |
pred.getASuccessor() = bb and
result = getACondition(source, v, pred) and
revBbSuccessorEntryReaches0(source, pred, v, _, this) and
exists(LogicalGuardCondition c | c = result.getCondition() |
not isLoopCondition(c, pred, bb) and
not isDisjunctionCondition(c, pred, bb) and
not isLoopVariantCondition(c, pred, bb)
)
)
)
}
pragma[nomagic]
private predicate bbSuccessorEntryReachesLoopInvariantSucc(
ControlFlowNode source, BasicBlock pred, SemanticStackVariable v, BasicBlock succ,
boolean predSkipsFirstLoopAlwaysTrueUponEntry
) {
revBbSuccessorEntryReaches0(source, pragma[only_bind_into](pred), v,
predSkipsFirstLoopAlwaysTrueUponEntry, this) and
pred.getASuccessor() = succ
}
pragma[nomagic]
private predicate bbSuccessorEntryReachesLoopInvariantCand(
ControlFlowNode source, BasicBlock pred, SemanticStackVariable v, BasicBlock succ,
boolean predSkipsFirstLoopAlwaysTrueUponEntry, boolean succSkipsFirstLoopAlwaysTrueUponEntry
) {
bbSuccessorEntryReachesLoopInvariantSucc(source, pragma[only_bind_into](pred), v, succ,
predSkipsFirstLoopAlwaysTrueUponEntry) and
bbSuccessorEntryReachesLoopInvariant0(pred, succ, predSkipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry)
}
/**
* Holds if `pred`, `succ`, `predSkipsFirstLoopAlwaysTrueUponEntry` and
* `succSkipsFirstLoopAlwaysTrueUponEntry` satisfy the loop invariants specified in the QLDoc
* for `bbSuccessorEntryReachesLoopInvariant0`.
*
* In addition, this predicate:
* 1. Rules out successor blocks that are unreachable due to contradictory path conditions.
* 2. Refines the successor relation when the edge `pred -> succ` is a conditional edge whose truth
* value is known.
*/
pragma[nomagic]
private predicate bbSuccessorEntryReachesLoopInvariant(
ControlFlowNode source, BasicBlock pred, SemanticStackVariable v, BasicBlock succ,
boolean predSkipsFirstLoopAlwaysTrueUponEntry, boolean succSkipsFirstLoopAlwaysTrueUponEntry
) {
bbSuccessorEntryReachesLoopInvariantCand(source, pred, v, succ,
predSkipsFirstLoopAlwaysTrueUponEntry, succSkipsFirstLoopAlwaysTrueUponEntry) and
not exists(Condition cond, Condition direct |
cond = getACondition(source, v, pred) and
direct = pragma[only_bind_out](getADirectCondition(succ)) and
cond.refutesCondition(direct)
) and
(
// If we picked the successor edge corresponding to a condition being true, there must not be
// another path condition that refutes that the condition is true.
not exists(Condition cond | cond = getACondition(source, v, pred) |
succ = pred.getATrueSuccessor() and
cond.refutesCondition(pragma[only_bind_out](MkCondition(pred.getEnd(), true)))
) and
// If we picked the successor edge corresponding to a condition being false, there must not be
// another path condition that refutes that the condition is false.
not exists(Condition cond | cond = getACondition(source, v, pred) |
succ = pred.getAFalseSuccessor() and
cond.refutesCondition(pragma[only_bind_out](MkCondition(pred.getEnd(), false)))
)
bbSuccessorEntryReaches(bb, v, sink, _)
)
}
private predicate bbSuccessorEntryReaches(
ControlFlowNode source, BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
boolean skipsFirstLoopAlwaysTrueUponEntry
) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant(source, bb, v, succ, skipsFirstLoopAlwaysTrueUponEntry,
bbSuccessorEntryReachesLoopInvariant(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry)
|
revBbEntryReachesLocally(succ, v, node, this) and
bbEntryReachesLocally(succ, v, node) and
succSkipsFirstLoopAlwaysTrueUponEntry = false
or
bbSuccessorEntryReachesLoopInvariant(source, bb, v, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry) and
not isBarrier(pragma[only_bind_out](succ.getANode()), v) and
pragma[only_bind_into](this)
.bbSuccessorEntryReaches(source, succ, v, node, succSkipsFirstLoopAlwaysTrueUponEntry)
not isBarrier(succ.getNode(_), v) and
bbSuccessorEntryReaches(succ, v, node, succSkipsFirstLoopAlwaysTrueUponEntry)
)
}
}
private predicate fwdBbEntryReachesLocally(
BasicBlock bb, SemanticStackVariable v, ControlFlowNode node, StackVariableReachability config
) {
exists(int n |
node = bb.getNode(n) and
config.isSource(node, v) and
(
not exists(lastBarrierIndexIn(bb, v, config))
private predicate bbEntryReachesLocally(
BasicBlock bb, SemanticStackVariable v, ControlFlowNode node
) {
exists(int n |
node = bb.getNode(n) and
isSink(node, v)
|
not exists(this.firstBarrierIndexIn(bb, v))
or
lastBarrierIndexIn(bb, v, config) <= n
n <= this.firstBarrierIndexIn(bb, v)
)
)
}
}
private predicate revBbEntryReachesLocally(
BasicBlock bb, SemanticStackVariable v, ControlFlowNode node, StackVariableReachability config
) {
exists(int n |
node = bb.getNode(n) and
config.isSink(node, v)
|
not exists(firstBarrierIndexIn(bb, v, config))
or
n <= firstBarrierIndexIn(bb, v, config)
)
}
private int firstBarrierIndexIn(
BasicBlock bb, SemanticStackVariable v, StackVariableReachability config
) {
result = min(int m | config.isBarrier(bb.getNode(m), v))
}
private int lastBarrierIndexIn(
BasicBlock bb, SemanticStackVariable v, StackVariableReachability config
) {
result = max(int m | config.isBarrier(bb.getNode(m), v))
private int firstBarrierIndexIn(BasicBlock bb, SemanticStackVariable v) {
result = min(int m | isBarrier(bb.getNode(m), v))
}
}
/**
@@ -564,7 +182,7 @@ private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor(
* is provably true upon entry, then `succ` is not allowed to skip
* that loop (`succSkipsFirstLoopAlwaysTrueUponEntry = false`).
*/
predicate bbSuccessorEntryReachesLoopInvariant0(
predicate bbSuccessorEntryReachesLoopInvariant(
BasicBlock pred, BasicBlock succ, boolean predSkipsFirstLoopAlwaysTrueUponEntry,
boolean succSkipsFirstLoopAlwaysTrueUponEntry
) {
@@ -678,52 +296,10 @@ abstract class StackVariableReachabilityWithReassignment extends StackVariableRe
)
}
private predicate bbSuccessorEntryReaches(
BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
boolean skipsFirstLoopAlwaysTrueUponEntry
) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant0(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry)
|
revBbEntryReachesLocally(succ, v, node, this) and
succSkipsFirstLoopAlwaysTrueUponEntry = false
or
not isBarrier(succ.getNode(_), v) and
bbSuccessorEntryReaches(succ, v, node, succSkipsFirstLoopAlwaysTrueUponEntry)
)
}
private predicate reaches0(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
/*
* Implementation detail: the predicates in this class are a generalization of
* those in DefinitionsAndUses.qll, and should be kept in sync.
*
* Unfortunately, caching of abstract predicates does not work well, so the
* predicates in DefinitionsAndUses.qll cannot use this library.
*/
exists(BasicBlock bb, int i |
isSource(source, v) and
bb.getNode(i) = source and
not bb.isUnreachable()
|
exists(int j |
j > i and
sink = bb.getNode(j) and
isSink(sink, v) and
not isBarrier(bb.getNode(pragma[only_bind_into]([i + 1 .. j - 1])), v)
)
or
not exists(int k | isBarrier(bb.getNode(k), v) | k > i) and
bbSuccessorEntryReaches(bb, v, sink, _)
)
}
private predicate reassignment(
ControlFlowNode source, SemanticStackVariable v, ControlFlowNode def, SemanticStackVariable v0
) {
reaches0(source, v, def) and
StackVariableReachability.super.reaches(source, v, def) and
exprDefinition(v0, def, v.getAnAccess())
}
@@ -789,11 +365,11 @@ abstract class StackVariableReachabilityExt extends string {
boolean skipsFirstLoopAlwaysTrueUponEntry
) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant0(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
bbSuccessorEntryReachesLoopInvariant(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
succSkipsFirstLoopAlwaysTrueUponEntry) and
not isBarrier(source, bb.getEnd(), succ.getStart(), v)
|
this.bbEntryReachesLocally(source, succ, v, node) and
bbEntryReachesLocally(source, succ, v, node) and
succSkipsFirstLoopAlwaysTrueUponEntry = false
or
not exists(int k | isBarrier(source, succ.getNode(k), succ.getNode(k + 1), v)) and