Skip to content

Commit 3c2b4e8

Browse files
committed
C++: AST-based wrapper for new range analysis
1 parent 9aca2d8 commit 3c2b4e8

File tree

1 file changed

+95
-0
lines changed

1 file changed

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

0 commit comments

Comments
 (0)