Skip to content

Commit bb8c3de

Browse files
MathiasVPMathiasVP
authored
Merge pull request #12599 from rdmarsh2/rdmarsh2/range-analysis-overflow
C++: add overflow detection to new range analysis
2 parents d975ceb + d833850 commit bb8c3de

14 files changed

Lines changed: 442 additions & 144 deletions

File tree

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

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ private import semmle.code.cpp.ir.IR
88
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound
99
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
1010
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
11+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisImpl
12+
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
1113

1214
/**
1315
* Gets the lower bound of the expression.
@@ -22,8 +24,10 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.Rang
2224
* `lowerBound(expr.getFullyConverted())`
2325
*/
2426
float lowerBound(Expr expr) {
25-
exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
26-
semBounded(getSemanticExpr(i), b, result, false, _)
27+
exists(Instruction i, ConstantBounds::SemBound b |
28+
i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
29+
|
30+
ConstantStage::semBounded(getSemanticExpr(i), b, result, false, _)
2731
)
2832
}
2933

@@ -40,8 +44,10 @@ float lowerBound(Expr expr) {
4044
* `upperBound(expr.getFullyConverted())`
4145
*/
4246
float upperBound(Expr expr) {
43-
exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
44-
semBounded(getSemanticExpr(i), b, result, true, _)
47+
exists(Instruction i, ConstantBounds::SemBound b |
48+
i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
49+
|
50+
ConstantStage::semBounded(getSemanticExpr(i), b, result, true, _)
4551
)
4652
}
4753

@@ -90,7 +96,15 @@ predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
9096
* does not consider the possibility that the expression might overflow
9197
* due to a conversion.
9298
*/
93-
predicate exprMightOverflowNegatively(Expr expr) { none() }
99+
predicate exprMightOverflowNegatively(Expr expr) {
100+
lowerBound(expr) < exprMinVal(expr)
101+
or
102+
exists(SemanticExprConfig::Expr semExpr |
103+
semExpr.getUnconverted().getAst() = expr and
104+
ConstantStage::potentiallyOverflowingExpr(false, semExpr) and
105+
not ConstantStage::initialBounded(semExpr, _, _, false, _, _, _)
106+
)
107+
}
94108

95109
/**
96110
* Holds if the expression might overflow negatively. Conversions
@@ -108,7 +122,15 @@ predicate convertedExprMightOverflowNegatively(Expr expr) {
108122
* does not consider the possibility that the expression might overflow
109123
* due to a conversion.
110124
*/
111-
predicate exprMightOverflowPositively(Expr expr) { none() }
125+
predicate exprMightOverflowPositively(Expr expr) {
126+
upperBound(expr) > exprMaxVal(expr)
127+
or
128+
exists(SemanticExprConfig::Expr semExpr |
129+
semExpr.getUnconverted().getAst() = expr and
130+
ConstantStage::potentiallyOverflowingExpr(true, semExpr) and
131+
not ConstantStage::initialBounded(semExpr, _, _, true, _, _, _)
132+
)
133+
}
112134

113135
/**
114136
* Holds if the expression might overflow positively. Conversions

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

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
private import RangeAnalysisStage
2+
private import RangeAnalysisImpl
23

34
module FloatDelta implements DeltaSig {
45
class Delta = float;
@@ -18,3 +19,36 @@ module FloatDelta implements DeltaSig {
1819
bindingset[f]
1920
Delta fromFloat(float f) { result = f }
2021
}
22+
23+
module FloatOverflow implements OverflowSig<FloatDelta> {
24+
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
25+
exists(float lb, float ub, float delta |
26+
typeBounds(expr.getSemType(), lb, ub) and
27+
ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _,
28+
_, _)
29+
|
30+
positively = true and delta < ub
31+
or
32+
positively = false and delta > lb
33+
)
34+
}
35+
36+
additional predicate typeBounds(SemType t, float lb, float ub) {
37+
exists(SemIntegerType integralType, float limit |
38+
integralType = t and limit = 2.pow(8 * integralType.getByteSize())
39+
|
40+
if integralType instanceof SemBooleanType
41+
then lb = 0 and ub = 1
42+
else
43+
if integralType.isSigned()
44+
then (
45+
lb = -(limit / 2) and ub = (limit / 2) - 1
46+
) else (
47+
lb = 0 and ub = limit - 1
48+
)
49+
)
50+
or
51+
// This covers all floating point types. The range is (-Inf, +Inf).
52+
t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
53+
}
54+
}

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/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 semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound
2+
private import RangeAnalysisImpl as Impl
3+
import Impl::Public

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisSpecific.qll renamed to cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
66
private import RangeAnalysisStage
77
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
88

9-
module CppLangImpl implements LangSig<FloatDelta> {
9+
module CppLangImplConstant implements LangSig<FloatDelta> {
1010
/**
1111
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
1212
*

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

Lines changed: 47 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
private import RangeAnalysisStage
2-
private import RangeAnalysisSpecific
2+
private import RangeAnalysisConstantSpecific
3+
private import RangeAnalysisRelativeSpecific
34
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
45
private import RangeUtils
56
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound as SemanticBound
@@ -28,7 +29,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
2829
}
2930
}
3031

31-
private module RelativeBounds implements BoundSig<FloatDelta> {
32+
module RelativeBounds implements BoundSig<FloatDelta> {
3233
class SemBound instanceof SemanticBound::SemBound {
3334
SemBound() { not this instanceof SemanticBound::SemZeroBound }
3435

@@ -46,11 +47,13 @@ private module RelativeBounds implements BoundSig<FloatDelta> {
4647
}
4748
}
4849

49-
private module ConstantStage =
50-
RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
50+
module ConstantStage =
51+
RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
52+
RangeUtil<FloatDelta, CppLangImplConstant>>;
5153

52-
private module RelativeStage =
53-
RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
54+
module RelativeStage =
55+
RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
56+
RangeUtil<FloatDelta, CppLangImplRelative>>;
5457

5558
private newtype TSemReason =
5659
TSemNoReason() or
@@ -60,48 +63,52 @@ private newtype TSemReason =
6063
guard = any(RelativeStage::SemCondReason reason).getCond()
6164
}
6265

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) }
85-
86-
override string toString() { result = getCond().toString() }
87-
}
88-
89-
private ConstantStage::SemReason constantReason(SemReason reason) {
66+
ConstantStage::SemReason constantReason(SemReason reason) {
9067
result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
9168
or
9269
result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
9370
}
9471

95-
private RelativeStage::SemReason relativeReason(SemReason reason) {
72+
RelativeStage::SemReason relativeReason(SemReason reason) {
9673
result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
9774
or
9875
result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
9976
}
10077

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

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

Lines changed: 126 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,126 @@
1+
/**
2+
* C++-specific implementation of range analysis.
3+
*/
4+
5+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
6+
private import RangeAnalysisStage
7+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
8+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
9+
private import RangeAnalysisImpl
10+
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
11+
12+
module CppLangImplRelative 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
34+
or
35+
upper = true and
36+
delta > ub
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+
* Ignore any inferred zero lower bound on this expression.
62+
*
63+
* This predicate is to keep the results identical to the original Java implementation. It should be
64+
* removed once we have the new implementation matching the old results exactly.
65+
*/
66+
predicate ignoreZeroLowerBound(SemExpr e) { none() }
67+
68+
/**
69+
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
70+
*
71+
* This predicate is to keep the results identical to the original Java implementation. It should be
72+
* removed once we have the new implementation matching the old results exactly.
73+
*/
74+
predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
75+
76+
/**
77+
* Holds if the specified variable should be excluded from the result of `ssaRead()`.
78+
*
79+
* This predicate is to keep the results identical to the original Java implementation. It should be
80+
* removed once we have the new implementation matching the old results exactly.
81+
*/
82+
predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() }
83+
84+
/**
85+
* Adds additional results to `ssaRead()` that are specific to Java.
86+
*
87+
* This predicate handles propagation of offsets for post-increment and post-decrement expressions
88+
* in exactly the same way as the old Java implementation. Once the new implementation matches the
89+
* old one, we should remove this predicate and propagate deltas for all similar patterns, whether
90+
* or not they come from a post-increment/decrement expression.
91+
*/
92+
SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() }
93+
94+
/**
95+
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
96+
*/
97+
predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
98+
99+
/**
100+
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
101+
*/
102+
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
103+
104+
/**
105+
* Holds if the value of `dest` is known to be `src + delta`.
106+
*/
107+
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() }
108+
109+
/**
110+
* Gets the type that range analysis should use to track the result of the specified expression,
111+
* if a type other than the original type of the expression is to be used.
112+
*
113+
* This predicate is commonly used in languages that support immutable "boxed" types that are
114+
* actually references but whose values can be tracked as the type contained in the box.
115+
*/
116+
SemType getAlternateType(SemExpr e) { none() }
117+
118+
/**
119+
* Gets the type that range analysis should use to track the result of the specified source
120+
* variable, if a type other than the original type of the expression is to be used.
121+
*
122+
* This predicate is commonly used in languages that support immutable "boxed" types that are
123+
* actually references but whose values can be tracked as the type contained in the box.
124+
*/
125+
SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() }
126+
}

0 commit comments

Comments
 (0)