Skip to content

Commit 5a5240d

Browse files
authored
Merge pull request #12865 from rdmarsh2/rdmarsh2/range-analysis-ast-wrapper
C++: AST-based wrapper for new range analysis
2 parents b511c5f + 8c992fb commit 5a5240d

File tree

2 files changed

+117
-0
lines changed

2 files changed

+117
-0
lines changed
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.
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+
}

0 commit comments

Comments
 (0)