Skip to content

Commit cad0244

Browse files
MathiasVPMathiasVP
committed
Merge branch 'main' into overrun-write-only-one-alert
2 parents de08ada + 09ba9a7 commit cad0244

File tree

170 files changed

+8825
-1406
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

170 files changed

+8825
-1406
lines changed

‎.github/workflows/tree-sitter-extractor-test.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,4 +43,4 @@ jobs:
4343
steps:
4444
- uses: actions/checkout@v3
4545
- name: Run clippy
46-
run: cargo clippy -- --no-deps # -D warnings
46+
run: cargo clippy -- --no-deps -D warnings -A clippy::new_without_default -A clippy::too_many_arguments

‎cpp/ql/lib/change-notes/2023-05-02-range-analysis-wrapper.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: feature
3+
---
4+
* Added an AST-based interface (`semmle.code.cpp.rangeanalysis.new.RangeAnalysis`) for the relative range analysis library.

‎cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll

Lines changed: 97 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
import semmle.code.cpp.ir.dataflow.DataFlow
2+
private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
3+
private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
4+
private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon
25
private import codeql.util.Unit
36

47
module ProductFlow {
@@ -352,32 +355,119 @@ module ProductFlow {
352355
pragma[only_bind_out](succ.getNode().getEnclosingCallable())
353356
}
354357

358+
private newtype TKind =
359+
TInto(DataFlowCall call) {
360+
intoImpl1(_, _, call) or
361+
intoImpl2(_, _, call)
362+
} or
363+
TOutOf(DataFlowCall call) {
364+
outImpl1(_, _, call) or
365+
outImpl2(_, _, call)
366+
} or
367+
TJump()
368+
369+
private predicate intoImpl1(Flow1::PathNode pred1, Flow1::PathNode succ1, DataFlowCall call) {
370+
Flow1::PathGraph::edges(pred1, succ1) and
371+
pred1.getNode().(ArgumentNode).getCall() = call and
372+
succ1.getNode() instanceof ParameterNode
373+
}
374+
375+
private predicate into1(Flow1::PathNode pred1, Flow1::PathNode succ1, TKind kind) {
376+
exists(DataFlowCall call |
377+
kind = TInto(call) and
378+
intoImpl1(pred1, succ1, call)
379+
)
380+
}
381+
382+
private predicate outImpl1(Flow1::PathNode pred1, Flow1::PathNode succ1, DataFlowCall call) {
383+
Flow1::PathGraph::edges(pred1, succ1) and
384+
exists(ReturnKindExt returnKind |
385+
succ1.getNode() = returnKind.getAnOutNode(call) and
386+
pred1.getNode().(ReturnNodeExt).getKind() = returnKind
387+
)
388+
}
389+
390+
private predicate out1(Flow1::PathNode pred1, Flow1::PathNode succ1, TKind kind) {
391+
exists(DataFlowCall call |
392+
outImpl1(pred1, succ1, call) and
393+
kind = TOutOf(call)
394+
)
395+
}
396+
397+
private predicate intoImpl2(Flow2::PathNode pred2, Flow2::PathNode succ2, DataFlowCall call) {
398+
Flow2::PathGraph::edges(pred2, succ2) and
399+
pred2.getNode().(ArgumentNode).getCall() = call and
400+
succ2.getNode() instanceof ParameterNode
401+
}
402+
403+
private predicate into2(Flow2::PathNode pred2, Flow2::PathNode succ2, TKind kind) {
404+
exists(DataFlowCall call |
405+
kind = TInto(call) and
406+
intoImpl2(pred2, succ2, call)
407+
)
408+
}
409+
410+
private predicate outImpl2(Flow2::PathNode pred2, Flow2::PathNode succ2, DataFlowCall call) {
411+
Flow2::PathGraph::edges(pred2, succ2) and
412+
exists(ReturnKindExt returnKind |
413+
succ2.getNode() = returnKind.getAnOutNode(call) and
414+
pred2.getNode().(ReturnNodeExt).getKind() = returnKind
415+
)
416+
}
417+
418+
private predicate out2(Flow2::PathNode pred2, Flow2::PathNode succ2, TKind kind) {
419+
exists(DataFlowCall call |
420+
kind = TOutOf(call) and
421+
outImpl2(pred2, succ2, call)
422+
)
423+
}
424+
355425
pragma[nomagic]
356426
private predicate interprocEdge1(
357-
Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1
427+
Declaration predDecl, Declaration succDecl, Flow1::PathNode pred1, Flow1::PathNode succ1,
428+
TKind kind
358429
) {
359430
Flow1::PathGraph::edges(pred1, succ1) and
360431
predDecl != succDecl and
361432
pred1.getNode().getEnclosingCallable() = predDecl and
362-
succ1.getNode().getEnclosingCallable() = succDecl
433+
succ1.getNode().getEnclosingCallable() = succDecl and
434+
(
435+
into1(pred1, succ1, kind)
436+
or
437+
out1(pred1, succ1, kind)
438+
or
439+
kind = TJump() and
440+
not into1(pred1, succ1, _) and
441+
not out1(pred1, succ1, _)
442+
)
363443
}
364444

365445
pragma[nomagic]
366446
private predicate interprocEdge2(
367-
Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2
447+
Declaration predDecl, Declaration succDecl, Flow2::PathNode pred2, Flow2::PathNode succ2,
448+
TKind kind
368449
) {
369450
Flow2::PathGraph::edges(pred2, succ2) and
370451
predDecl != succDecl and
371452
pred2.getNode().getEnclosingCallable() = predDecl and
372-
succ2.getNode().getEnclosingCallable() = succDecl
453+
succ2.getNode().getEnclosingCallable() = succDecl and
454+
(
455+
into2(pred2, succ2, kind)
456+
or
457+
out2(pred2, succ2, kind)
458+
or
459+
kind = TJump() and
460+
not into2(pred2, succ2, _) and
461+
not out2(pred2, succ2, _)
462+
)
373463
}
374464

375465
private predicate interprocEdgePair(
376466
Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
377467
) {
378-
exists(Declaration predDecl, Declaration succDecl |
379-
interprocEdge1(predDecl, succDecl, pred1, succ1) and
380-
interprocEdge2(predDecl, succDecl, pred2, succ2)
468+
exists(Declaration predDecl, Declaration succDecl, TKind kind |
469+
interprocEdge1(predDecl, succDecl, pred1, succ1, kind) and
470+
interprocEdge2(predDecl, succDecl, pred2, succ2, kind)
381471
)
382472
}
383473

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,9 @@ module Consistency {
5858
predicate uniqueParameterNodePositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
5959
none()
6060
}
61+
62+
/** Holds if `n` should be excluded from the consistency test `identityLocalStep`. */
63+
predicate identityLocalStepExclude(Node n) { none() }
6164
}
6265

6366
private class RelevantNode extends Node {
@@ -287,4 +290,10 @@ module Consistency {
287290
not exists(unique(ContentApprox approx | approx = getContentApprox(c))) and
288291
msg = "Non-unique content approximation."
289292
}
293+
294+
query predicate identityLocalStep(Node n, string msg) {
295+
simpleLocalFlowStep(n, n) and
296+
not any(ConsistencyConfiguration c).identityLocalStepExclude(n) and
297+
msg = "Node steps to itself"
298+
}
290299
}

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,9 @@ module Consistency {
5858
predicate uniqueParameterNodePositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
5959
none()
6060
}
61+
62+
/** Holds if `n` should be excluded from the consistency test `identityLocalStep`. */
63+
predicate identityLocalStepExclude(Node n) { none() }
6164
}
6265

6366
private class RelevantNode extends Node {
@@ -287,4 +290,10 @@ module Consistency {
287290
not exists(unique(ContentApprox approx | approx = getContentApprox(c))) and
288291
msg = "Non-unique content approximation."
289292
}
293+
294+
query predicate identityLocalStep(Node n, string msg) {
295+
simpleLocalFlowStep(n, n) and
296+
not any(ConsistencyConfiguration c).identityLocalStepExclude(n) and
297+
msg = "Node steps to itself"
298+
}
290299
}

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/RangeAnalysis.qll

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
/**
2+
* Provides an AST-based interface to the relative range analysis, which tracks bounds of the form
3+
* `a <= b + delta` for expressions `a` and `b` and an integer offset `delta`.
4+
*/
5+
6+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
7+
private import cpp
8+
private import semmle.code.cpp.ir.IR
9+
private import semmle.code.cpp.controlflow.IRGuards
10+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
11+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
12+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.Bound as IRBound
13+
private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
14+
15+
/**
16+
* Holds if e is bounded by `b + delta`. The bound is an upper bound if
17+
* `upper` is true, and can be traced back to a guard represented by `reason`.
18+
*/
19+
predicate bounded(Expr e, Bound b, float delta, boolean upper, Reason reason) {
20+
exists(SemanticExprConfig::Expr semExpr |
21+
semExpr.getUnconverted().getUnconvertedResultExpression() = e
22+
|
23+
semBounded(semExpr, b, delta, upper, reason)
24+
)
25+
}
26+
27+
/**
28+
* Holds if e is bounded by `b + delta`. The bound is an upper bound if
29+
* `upper` is true, and can be traced back to a guard represented by `reason`.
30+
* The `Expr` may be a conversion.
31+
*/
32+
predicate convertedBounded(Expr e, Bound b, float delta, boolean upper, Reason reason) {
33+
exists(SemanticExprConfig::Expr semExpr |
34+
semExpr.getConverted().getConvertedResultExpression() = e
35+
|
36+
semBounded(semExpr, b, delta, upper, reason)
37+
)
38+
}
39+
40+
/**
41+
* A reason for an inferred bound. This can either be `CondReason` if the bound
42+
* is due to a specific condition, or `NoReason` if the bound is inferred
43+
* without going through a bounding condition.
44+
*/
45+
class Reason instanceof SemReason {
46+
/** Gets a string representation of this reason */
47+
string toString() { none() }
48+
}
49+
50+
/**
51+
* A reason for an inferred bound that indicates that the bound is inferred
52+
* without going through a bounding condition.
53+
*/
54+
class NoReason extends Reason instanceof SemNoReason {
55+
override string toString() { result = "NoReason" }
56+
}
57+
58+
/** A reason for an inferred bound pointing to a condition. */
59+
class CondReason extends Reason instanceof SemCondReason {
60+
override string toString() { result = SemCondReason.super.toString() }
61+
62+
/** Gets the guard condition that caused the inferred bound */
63+
GuardCondition getCond() {
64+
result = super.getCond().(IRGuardCondition).getUnconvertedResultExpression()
65+
}
66+
}
67+
68+
/**
69+
* A bound that may be inferred for an expression plus/minus an integer delta.
70+
*/
71+
class Bound instanceof IRBound::Bound {
72+
/** Gets a string representation of this bound. */
73+
string toString() { none() }
74+
75+
/** Gets an expression that equals this bound. */
76+
Expr getAnExpr() { none() }
77+
78+
/** Gets an expression that equals this bound plus `delta`. */
79+
Expr getAnExpr(int delta) { none() }
80+
81+
/** Gets a representative locaiton for this bound */
82+
Location getLocation() { none() }
83+
}
84+
85+
/**
86+
* The bound that corresponds to the integer 0. This is used to represent all
87+
* integer bounds as bounds are always accompanied by an added integer delta.
88+
*/
89+
class ZeroBound extends Bound instanceof IRBound::ZeroBound {
90+
override string toString() { result = "0" }
91+
92+
override Expr getAnExpr(int delta) {
93+
result = super.getInstruction(delta).getUnconvertedResultExpression()
94+
}
95+
96+
override Location getLocation() { result instanceof UnknownDefaultLocation }
97+
}
98+
99+
/**
100+
* A bound corresponding to the value of an `Instruction`.
101+
*/
102+
class ValueNumberBound extends Bound instanceof IRBound::ValueNumberBound {
103+
override string toString() { result = "ValueNumberBound" }
104+
105+
override Expr getAnExpr(int delta) {
106+
result = super.getInstruction(delta).getUnconvertedResultExpression()
107+
}
108+
109+
override Location getLocation() { result = IRBound::ValueNumberBound.super.getLocation() }
110+
111+
/** Gets the value number that equals this bound. */
112+
GVN getValueNumber() { result = super.getValueNumber() }
113+
}

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll

Lines changed: 0 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -120,13 +120,6 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
120120
)
121121
}
122122

123-
/**
124-
* Holds if `rix` is the number of input edges to `phi`.
125-
*/
126-
private predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
127-
rix = max(int r | rankedPhiInput(phi, _, _, r))
128-
}
129-
130123
/**
131124
* Gets the remainder of `val` modulo `mod`.
132125
*
@@ -322,20 +315,4 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
322315
semExprModulus(rarg, b, val, mod) and isLeft = false
323316
)
324317
}
325-
326-
/**
327-
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
328-
* in an arbitrary 1-based numbering of the input edges to `phi`.
329-
*/
330-
private predicate rankedPhiInput(
331-
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
332-
) {
333-
edge.phiInput(phi, inp) and
334-
edge =
335-
rank[r](SemSsaReadPositionPhiInputEdge e |
336-
e.phiInput(phi, _)
337-
|
338-
e order by e.getOrigBlock().getUniqueId()
339-
)
340-
}
341318
}

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -877,6 +877,22 @@ module RangeStage<
877877
)
878878
}
879879

880+
pragma[assume_small_delta]
881+
pragma[nomagic]
882+
private predicate boundedPhiRankStep(
883+
SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
884+
D::Delta origdelta, SemReason reason, int rix
885+
) {
886+
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
887+
Utils::rankedPhiInput(phi, inp, edge, rix) and
888+
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
889+
|
890+
if rix = 1
891+
then any()
892+
else boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
893+
)
894+
}
895+
880896
/**
881897
* Holds if `b + delta` is a valid bound for `phi`.
882898
* - `upper = true` : `phi <= b + delta`
@@ -886,8 +902,9 @@ module RangeStage<
886902
SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
887903
D::Delta origdelta, SemReason reason
888904
) {
889-
forex(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
890-
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
905+
exists(int r |
906+
Utils::maxPhiInputRank(phi, r) and
907+
boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r)
891908
)
892909
}
893910

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,3 +138,26 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
138138
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
139139
}
140140
}
141+
142+
/**
143+
* Holds if `rix` is the number of input edges to `phi`.
144+
*/
145+
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
146+
rix = max(int r | rankedPhiInput(phi, _, _, r))
147+
}
148+
149+
/**
150+
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
151+
* in an arbitrary 1-based numbering of the input edges to `phi`.
152+
*/
153+
predicate rankedPhiInput(
154+
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
155+
) {
156+
edge.phiInput(phi, inp) and
157+
edge =
158+
rank[r](SemSsaReadPositionPhiInputEdge e |
159+
e.phiInput(phi, _)
160+
|
161+
e order by e.getOrigBlock().getUniqueId()
162+
)
163+
}

0 commit comments

Comments
 (0)