C++: Bring back StackVariableReachability.qll

This is now a copy of `LocalScopeVariableReachability.qll`, just with
`s/LocalScopeVariable/StackVariable/g`. It can be used as a drop-in
replacement since the `LocalScopeVariableReachability.qll` library
implementation was already restricted to `SemanticStackVariable`.
This commit is contained in:
Jonas Jensen
2019-11-18 14:11:53 +01:00
parent 8110039e0a
commit 01ca63ae92

View File

@@ -1,11 +1,24 @@
import cpp import cpp
/** /**
* DEPRECATED: use `LocalScopeVariableReachability` instead.
*
* A reachability analysis for control-flow nodes involving stack variables. * A reachability analysis for control-flow nodes involving stack variables.
* This defines sources, sinks, and any other configurable aspect of the
* analysis. Multiple analyses can coexist. To create an analysis, extend this
* class with a subclass whose characteristic predicate is a unique singleton
* string. For example, write
*
* ```
* class MyAnalysisConfiguration extends StackVariableReachability {
* MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
* // Override `isSource` and `isSink`.
* // Override `isBarrier`.
* }
* ```
*
* Then, to query whether there is flow between some source and sink, call the
* `reaches` predicate on an instance of `MyAnalysisConfiguration`.
*/ */
abstract deprecated class StackVariableReachability extends string { abstract class StackVariableReachability extends string {
bindingset[this] bindingset[this]
StackVariableReachability() { length() >= 0 } StackVariableReachability() { length() >= 0 }
@@ -24,13 +37,13 @@ abstract deprecated class StackVariableReachability extends string {
* uses basic blocks internally for better performance: * uses basic blocks internally for better performance:
* *
* ``` * ```
* predicate reaches(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { * predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
* reachesImpl(source, v, sink) * reachesImpl(source, v, sink)
* and * and
* isSink(sink, v) * isSink(sink, v)
* } * }
* *
* predicate reachesImpl(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { * predicate reachesImpl(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
* sink = source.getASuccessor() and isSource(source, v) * sink = source.getASuccessor() and isSource(source, v)
* or * or
* exists(ControlFlowNode mid | reachesImpl(source, v, mid) | * exists(ControlFlowNode mid | reachesImpl(source, v, mid) |
@@ -44,7 +57,7 @@ abstract deprecated class StackVariableReachability extends string {
* In addition to using a better performing implementation, this analysis * In addition to using a better performing implementation, this analysis
* accounts for loops where the condition is provably true upon entry. * accounts for loops where the condition is provably true upon entry.
*/ */
predicate reaches(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
/* /*
* Implementation detail: the predicates in this class are a generalization of * Implementation detail: the predicates in this class are a generalization of
* those in DefinitionsAndUses.qll, and should be kept in sync. * those in DefinitionsAndUses.qll, and should be kept in sync.
@@ -71,7 +84,8 @@ abstract deprecated class StackVariableReachability extends string {
} }
private predicate bbSuccessorEntryReaches( private predicate bbSuccessorEntryReaches(
BasicBlock bb, StackVariable v, ControlFlowNode node, boolean skipsFirstLoopAlwaysTrueUponEntry BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
boolean skipsFirstLoopAlwaysTrueUponEntry
) { ) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry | exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
bbSuccessorEntryReachesLoopInvariant(bb, succ, skipsFirstLoopAlwaysTrueUponEntry, bbSuccessorEntryReachesLoopInvariant(bb, succ, skipsFirstLoopAlwaysTrueUponEntry,
@@ -85,11 +99,22 @@ abstract deprecated class StackVariableReachability extends string {
) )
} }
private predicate bbEntryReachesLocally(BasicBlock bb, StackVariable v, ControlFlowNode node) { private predicate bbEntryReachesLocally(
exists(int n | node = bb.getNode(n) and isSink(node, v) | BasicBlock bb, SemanticStackVariable v, ControlFlowNode node
not exists(int m | m < n | isBarrier(bb.getNode(m), v)) ) {
exists(int n |
node = bb.getNode(n) and
isSink(node, v)
|
not exists(this.firstBarrierIndexIn(bb, v))
or
n <= this.firstBarrierIndexIn(bb, v)
) )
} }
private int firstBarrierIndexIn(BasicBlock bb, SemanticStackVariable v) {
result = min(int m | isBarrier(bb.getNode(m), v))
}
} }
/** /**
@@ -113,26 +138,32 @@ private predicate bbLoopEntryConditionAlwaysTrueAt(BasicBlock bb, int i, Control
} }
/** /**
* Basic block `pred` ends with a condition belonging to a loop, and that * Basic block `pred` contains all or part of the condition belonging to a loop,
* condition is provably true upon entry. Basic block `succ` is a successor * and there is an edge from `pred` to `succ` that concludes the condition.
* of `pred`, and `skipsLoop` indicates whether `succ` is the false-successor * If the edge corrseponds with the loop condition being found to be `true`, then
* of `pred`. * `skipsLoop` is `false`. Otherwise the edge corresponds with the loop condition
* being found to be `false` and `skipsLoop` is `true`. Non-concluding edges
* within a complex loop condition are not matched by this predicate.
*/ */
private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor( private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor(
BasicBlock pred, BasicBlock succ, boolean skipsLoop BasicBlock pred, BasicBlock succ, boolean skipsLoop
) { ) {
succ = pred.getASuccessor() and exists(Expr cond |
exists(ControlFlowNode last | loopConditionAlwaysTrueUponEntry(_, cond) and
last = pred.getEnd() and cond.getAChild*() = pred.getEnd() and
loopConditionAlwaysTrueUponEntry(_, last) and succ = pred.getASuccessor() and
if succ = pred.getAFalseSuccessor() then skipsLoop = true else skipsLoop = false not cond.getAChild*() = succ.getStart() and
(
succ = pred.getAFalseSuccessor() and
skipsLoop = true
or
succ = pred.getATrueSuccessor() and
skipsLoop = false
)
) )
} }
/** /**
* DEPRECATED: use the corresponding predicate in
* `LocalScopeVariableReachability` instead.
*
* Loop invariant for `bbSuccessorEntryReaches`: * Loop invariant for `bbSuccessorEntryReaches`:
* *
* - `succ` is a successor of `pred`. * - `succ` is a successor of `pred`.
@@ -146,7 +177,7 @@ private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor(
* is provably true upon entry, then `succ` is not allowed to skip * is provably true upon entry, then `succ` is not allowed to skip
* that loop (`succSkipsFirstLoopAlwaysTrueUponEntry = false`). * that loop (`succSkipsFirstLoopAlwaysTrueUponEntry = false`).
*/ */
deprecated predicate bbSuccessorEntryReachesLoopInvariant( predicate bbSuccessorEntryReachesLoopInvariant(
BasicBlock pred, BasicBlock succ, boolean predSkipsFirstLoopAlwaysTrueUponEntry, BasicBlock pred, BasicBlock succ, boolean predSkipsFirstLoopAlwaysTrueUponEntry,
boolean succSkipsFirstLoopAlwaysTrueUponEntry boolean succSkipsFirstLoopAlwaysTrueUponEntry
) { ) {
@@ -162,7 +193,7 @@ deprecated predicate bbSuccessorEntryReachesLoopInvariant(
// The edge from `pred` to `succ` is _not_ from a loop condition provably // The edge from `pred` to `succ` is _not_ from a loop condition provably
// true upon entry, so the values of `predSkipsFirstLoopAlwaysTrueUponEntry` // true upon entry, so the values of `predSkipsFirstLoopAlwaysTrueUponEntry`
// and `succSkipsFirstLoopAlwaysTrueUponEntry` must be the same. // and `succSkipsFirstLoopAlwaysTrueUponEntry` must be the same.
not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, _, _) and not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, succ, _) and
succSkipsFirstLoopAlwaysTrueUponEntry = predSkipsFirstLoopAlwaysTrueUponEntry and succSkipsFirstLoopAlwaysTrueUponEntry = predSkipsFirstLoopAlwaysTrueUponEntry and
// Moreover, if `pred` contains the entry point of a loop where the // Moreover, if `pred` contains the entry point of a loop where the
// condition is provably true upon entry, then `succ` is not allowed // condition is provably true upon entry, then `succ` is not allowed
@@ -176,13 +207,16 @@ deprecated predicate bbSuccessorEntryReachesLoopInvariant(
} }
/** /**
* DEPRECATED: use `LocalScopeVariableReachabilityWithReassignment` instead.
*
* Reachability analysis for control-flow nodes involving stack variables. * Reachability analysis for control-flow nodes involving stack variables.
* Unlike `StackVariableReachability`, this analysis takes variable * Unlike `StackVariableReachability`, this analysis takes variable
* reassignments into account. * reassignments into account.
*
* This class is used like `StackVariableReachability`, except that
* subclasses should override `isSourceActual` and `isSinkActual` instead of
* `isSource` and `isSink`, and that there is a `reachesTo` predicate in
* addition to `reaches`.
*/ */
abstract deprecated class StackVariableReachabilityWithReassignment extends StackVariableReachability { abstract class StackVariableReachabilityWithReassignment extends StackVariableReachability {
bindingset[this] bindingset[this]
StackVariableReachabilityWithReassignment() { length() >= 0 } StackVariableReachabilityWithReassignment() { length() >= 0 }
@@ -199,19 +233,19 @@ abstract deprecated class StackVariableReachabilityWithReassignment extends Stac
* performance: * performance:
* *
* ``` * ```
* predicate reaches(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { * predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
* reachesImpl(source, v, sink) * reachesImpl(source, v, sink)
* and * and
* isSinkActual(sink, v) * isSinkActual(sink, v)
* } * }
* *
* predicate reachesImpl(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { * predicate reachesImpl(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
* isSourceActual(source, v) * isSourceActual(source, v)
* and * and
* ( * (
* sink = source.getASuccessor() * sink = source.getASuccessor()
* or * or
* exists(ControlFlowNode mid, StackVariable v0 | reachesImpl(source, v0, mid) | * exists(ControlFlowNode mid, SemanticStackVariable v0 | reachesImpl(source, v0, mid) |
* // ordinary successor * // ordinary successor
* not isBarrier(mid, v) and * not isBarrier(mid, v) and
* sink = mid.getASuccessor() and * sink = mid.getASuccessor() and
@@ -228,7 +262,7 @@ abstract deprecated class StackVariableReachabilityWithReassignment extends Stac
* In addition to using a better performing implementation, this analysis * In addition to using a better performing implementation, this analysis
* accounts for loops where the condition is provably true upon entry. * accounts for loops where the condition is provably true upon entry.
*/ */
override predicate reaches(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { override predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
reachesTo(source, v, sink, _) reachesTo(source, v, sink, _)
} }
@@ -236,7 +270,7 @@ abstract deprecated class StackVariableReachabilityWithReassignment extends Stac
* As `reaches`, but also specifies the last variable it was reassigned to (`v0`). * As `reaches`, but also specifies the last variable it was reassigned to (`v0`).
*/ */
predicate reachesTo( predicate reachesTo(
ControlFlowNode source, StackVariable v, ControlFlowNode sink, StackVariable v0 ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink, SemanticStackVariable v0
) { ) {
exists(ControlFlowNode def | exists(ControlFlowNode def |
actualSourceReaches(source, v, def, v0) and actualSourceReaches(source, v, def, v0) and
@@ -246,17 +280,19 @@ abstract deprecated class StackVariableReachabilityWithReassignment extends Stac
} }
private predicate actualSourceReaches( private predicate actualSourceReaches(
ControlFlowNode source, StackVariable v, ControlFlowNode def, StackVariable v0 ControlFlowNode source, SemanticStackVariable v, ControlFlowNode def, SemanticStackVariable v0
) { ) {
isSourceActual(source, v) and def = source and v0 = v isSourceActual(source, v) and def = source and v0 = v
or or
exists(ControlFlowNode source1, StackVariable v1 | actualSourceReaches(source, v, source1, v1) | exists(ControlFlowNode source1, SemanticStackVariable v1 |
actualSourceReaches(source, v, source1, v1)
|
reassignment(source1, v1, def, v0) reassignment(source1, v1, def, v0)
) )
} }
private predicate reassignment( private predicate reassignment(
ControlFlowNode source, StackVariable v, ControlFlowNode def, StackVariable v0 ControlFlowNode source, SemanticStackVariable v, ControlFlowNode def, SemanticStackVariable v0
) { ) {
StackVariableReachability.super.reaches(source, v, def) and StackVariableReachability.super.reaches(source, v, def) and
exprDefinition(v0, def, v.getAnAccess()) exprDefinition(v0, def, v.getAnAccess())
@@ -278,13 +314,12 @@ abstract deprecated class StackVariableReachabilityWithReassignment extends Stac
} }
/** /**
* DEPRECATED: use `LocalScopeVariableReachabilityExt` instead.
*
* Same as `StackVariableReachability`, but `isBarrier` works on control-flow * Same as `StackVariableReachability`, but `isBarrier` works on control-flow
* edges rather than nodes and is therefore parameterized by the original * edges rather than nodes and is therefore parameterized by the original
* source node as well. * source node as well. Otherwise, this class is used like
* `StackVariableReachability`.
*/ */
abstract deprecated class StackVariableReachabilityExt extends string { abstract class StackVariableReachabilityExt extends string {
bindingset[this] bindingset[this]
StackVariableReachabilityExt() { length() >= 0 } StackVariableReachabilityExt() { length() >= 0 }
@@ -300,7 +335,7 @@ abstract deprecated class StackVariableReachabilityExt extends string {
); );
/** See `StackVariableReachability.reaches`. */ /** See `StackVariableReachability.reaches`. */
predicate reaches(ControlFlowNode source, StackVariable v, ControlFlowNode sink) { predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
exists(BasicBlock bb, int i | exists(BasicBlock bb, int i |
isSource(source, v) and isSource(source, v) and
bb.getNode(i) = source and bb.getNode(i) = source and
@@ -321,7 +356,7 @@ abstract deprecated class StackVariableReachabilityExt extends string {
} }
private predicate bbSuccessorEntryReaches( private predicate bbSuccessorEntryReaches(
ControlFlowNode source, BasicBlock bb, StackVariable v, ControlFlowNode node, ControlFlowNode source, BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
boolean skipsFirstLoopAlwaysTrueUponEntry boolean skipsFirstLoopAlwaysTrueUponEntry
) { ) {
exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry | exists(BasicBlock succ, boolean succSkipsFirstLoopAlwaysTrueUponEntry |
@@ -338,7 +373,7 @@ abstract deprecated class StackVariableReachabilityExt extends string {
} }
private predicate bbEntryReachesLocally( private predicate bbEntryReachesLocally(
ControlFlowNode source, BasicBlock bb, StackVariable v, ControlFlowNode node ControlFlowNode source, BasicBlock bb, SemanticStackVariable v, ControlFlowNode node
) { ) {
isSource(source, v) and isSource(source, v) and
exists(int n | node = bb.getNode(n) and isSink(node, v) | exists(int n | node = bb.getNode(n) and isSink(node, v) |