Skip to content

Commit 7ea74df

Browse files
rdmarsh2rdmarsh2
committed
C++: SimpleRangeAnalysis wrapper uses constant stage
1 parent 204dbee commit 7ea74df

File tree

5 files changed

+177
-41
lines changed

5 files changed

+177
-41
lines changed

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ module FloatOverflow implements OverflowSig<FloatDelta> {
3333
predicate semExprDoesntOverflow(boolean positively, SemExpr expr) {
3434
exists(float lb, float ub, float delta |
3535
typeBounds(expr.getSemType(), lb, ub) and
36-
ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively.booleanNot(), _, _, _)
36+
ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, _, _)
3737
|
3838
positively = true and delta < ub
3939
or

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
1-
import RangeAnalysisImpl
21
import experimental.semmle.code.cpp.semantic.SemanticBound
2+
private import RangeAnalysisImpl as Impl
3+
import Impl::Public

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll

Lines changed: 38 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
2828
}
2929
}
3030

31-
private module RelativeBounds implements BoundSig<FloatDelta> {
31+
module RelativeBounds implements BoundSig<FloatDelta> {
3232
class SemBound instanceof SemanticBound::SemBound {
3333
SemBound() { not this instanceof SemanticBound::SemZeroBound }
3434

@@ -60,48 +60,52 @@ private newtype TSemReason =
6060
guard = any(RelativeStage::SemCondReason reason).getCond()
6161
}
6262

63-
/**
64-
* A reason for an inferred bound. This can either be `CondReason` if the bound
65-
* is due to a specific condition, or `NoReason` if the bound is inferred
66-
* without going through a bounding condition.
67-
*/
68-
abstract class SemReason extends TSemReason {
69-
/** Gets a textual representation of this reason. */
70-
abstract string toString();
71-
}
72-
73-
/**
74-
* A reason for an inferred bound that indicates that the bound is inferred
75-
* without going through a bounding condition.
76-
*/
77-
class SemNoReason extends SemReason, TSemNoReason {
78-
override string toString() { result = "NoReason" }
79-
}
80-
81-
/** A reason for an inferred bound pointing to a condition. */
82-
class SemCondReason extends SemReason, TSemCondReason {
83-
/** Gets the condition that is the reason for the bound. */
84-
SemGuard getCond() { this = TSemCondReason(result) }
8563

86-
override string toString() { result = getCond().toString() }
87-
}
88-
89-
private ConstantStage::SemReason constantReason(SemReason reason) {
64+
ConstantStage::SemReason constantReason(SemReason reason) {
9065
result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
9166
or
9267
result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
9368
}
9469

95-
private RelativeStage::SemReason relativeReason(SemReason reason) {
70+
RelativeStage::SemReason relativeReason(SemReason reason) {
9671
result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
9772
or
9873
result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
9974
}
75+
import Public
10076

101-
predicate semBounded(
102-
SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
103-
) {
104-
ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
105-
or
106-
RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
77+
module Public {
78+
predicate semBounded(
79+
SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
80+
) {
81+
ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
82+
or
83+
RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
84+
}
85+
86+
/**
87+
* A reason for an inferred bound. This can either be `CondReason` if the bound
88+
* is due to a specific condition, or `NoReason` if the bound is inferred
89+
* without going through a bounding condition.
90+
*/
91+
abstract class SemReason extends TSemReason {
92+
/** Gets a textual representation of this reason. */
93+
abstract string toString();
94+
}
95+
96+
/**
97+
* A reason for an inferred bound that indicates that the bound is inferred
98+
* without going through a bounding condition.
99+
*/
100+
class SemNoReason extends SemReason, TSemNoReason {
101+
override string toString() { result = "NoReason" }
102+
}
103+
104+
/** A reason for an inferred bound pointing to a condition. */
105+
class SemCondReason extends SemReason, TSemCondReason {
106+
/** Gets the condition that is the reason for the bound. */
107+
SemGuard getCond() { this = TSemCondReason(result) }
108+
109+
override string toString() { result = getCond().toString() }
110+
}
107111
}

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
/**
2+
* C++-specific implementation of range analysis.
3+
*/
4+
5+
private import experimental.semmle.code.cpp.semantic.Semantic
6+
private import RangeAnalysisStage
7+
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
8+
private import experimental.semmle.code.cpp.semantic.analysis.IntDelta
9+
private import RangeAnalysisImpl
10+
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
11+
12+
module CppLangImpl2 implements LangSig<FloatDelta> {
13+
/**
14+
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
15+
*
16+
* This predicate is to keep the results identical to the original Java implementation. It should be
17+
* removed once we have the new implementation matching the old results exactly.
18+
*/
19+
predicate ignoreSsaReadCopy(SemExpr e) { none() }
20+
21+
/**
22+
* Ignore the bound on this expression.
23+
*
24+
* This predicate is to keep the results identical to the original Java implementation. It should be
25+
* removed once we have the new implementation matching the old results exactly.
26+
*/
27+
predicate ignoreExprBound(SemExpr e) {
28+
exists(boolean upper, float delta, ConstantBounds::SemZeroBound b, float lb, float ub |
29+
ConstantStage::semBounded(e, b, delta, upper, _) and
30+
typeBounds(e.getSemType(), lb, ub) and
31+
(
32+
upper = false and
33+
delta < lb or
34+
upper = true and
35+
delta > ub
36+
)
37+
)
38+
}
39+
40+
41+
private predicate typeBounds(SemType t, float lb, float ub) {
42+
exists(SemIntegerType integralType, float limit |
43+
integralType = t and limit = 2.pow(8 * integralType.getByteSize())
44+
|
45+
if integralType instanceof SemBooleanType
46+
then lb = 0 and ub = 1
47+
else
48+
if integralType.isSigned()
49+
then (
50+
lb = -(limit / 2) and ub = (limit / 2) - 1
51+
) else (
52+
lb = 0 and ub = limit - 1
53+
)
54+
)
55+
or
56+
// This covers all floating point types. The range is (-Inf, +Inf).
57+
t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
58+
}
59+
60+
61+
/**
62+
* Ignore any inferred zero lower bound on this expression.
63+
*
64+
* This predicate is to keep the results identical to the original Java implementation. It should be
65+
* removed once we have the new implementation matching the old results exactly.
66+
*/
67+
predicate ignoreZeroLowerBound(SemExpr e) { none() }
68+
69+
/**
70+
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
71+
*
72+
* This predicate is to keep the results identical to the original Java implementation. It should be
73+
* removed once we have the new implementation matching the old results exactly.
74+
*/
75+
predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
76+
77+
/**
78+
* Holds if the specified variable should be excluded from the result of `ssaRead()`.
79+
*
80+
* This predicate is to keep the results identical to the original Java implementation. It should be
81+
* removed once we have the new implementation matching the old results exactly.
82+
*/
83+
predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() }
84+
85+
/**
86+
* Adds additional results to `ssaRead()` that are specific to Java.
87+
*
88+
* This predicate handles propagation of offsets for post-increment and post-decrement expressions
89+
* in exactly the same way as the old Java implementation. Once the new implementation matches the
90+
* old one, we should remove this predicate and propagate deltas for all similar patterns, whether
91+
* or not they come from a post-increment/decrement expression.
92+
*/
93+
SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() }
94+
95+
/**
96+
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
97+
*/
98+
predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
99+
100+
/**
101+
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
102+
*/
103+
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
104+
105+
/**
106+
* Holds if the value of `dest` is known to be `src + delta`.
107+
*/
108+
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() }
109+
110+
/**
111+
* Gets the type that range analysis should use to track the result of the specified expression,
112+
* if a type other than the original type of the expression is to be used.
113+
*
114+
* This predicate is commonly used in languages that support immutable "boxed" types that are
115+
* actually references but whose values can be tracked as the type contained in the box.
116+
*/
117+
SemType getAlternateType(SemExpr e) { none() }
118+
119+
/**
120+
* Gets the type that range analysis should use to track the result of the specified source
121+
* variable, if a type other than the original type of the expression is to be used.
122+
*
123+
* This predicate is commonly used in languages that support immutable "boxed" types that are
124+
* actually references but whose values can be tracked as the type contained in the box.
125+
*/
126+
SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() }
127+
}

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ private import cpp
77
private import semmle.code.cpp.ir.IR
88
private import experimental.semmle.code.cpp.semantic.SemanticBound
99
private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
10-
private import RangeAnalysis
10+
private import RangeAnalysisImpl
1111
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
1212

1313
/**
@@ -23,8 +23,10 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
2323
* `lowerBound(expr.getFullyConverted())`
2424
*/
2525
float lowerBound(Expr expr) {
26-
exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
27-
semBounded(getSemanticExpr(i), b, result, false, _)
26+
exists(Instruction i, ConstantBounds::SemBound b |
27+
i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
28+
|
29+
ConstantStage::semBounded(getSemanticExpr(i), b, result, false, _)
2830
)
2931
}
3032

@@ -41,8 +43,10 @@ float lowerBound(Expr expr) {
4143
* `upperBound(expr.getFullyConverted())`
4244
*/
4345
float upperBound(Expr expr) {
44-
exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
45-
semBounded(getSemanticExpr(i), b, result, true, _)
46+
exists(Instruction i, ConstantBounds::SemBound b |
47+
i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
48+
|
49+
ConstantStage::semBounded(getSemanticExpr(i), b, result, true, _)
4650
)
4751
}
4852

0 commit comments

Comments
 (0)