Skip to content

Commit 0e45c99

Browse files
committed
C++: Introduce wrapper for the semantic range analysis mimicking the simple one
1 parent 3481652 commit 0e45c99

File tree

1 file changed

+120
-0
lines changed

1 file changed

+120
-0
lines changed
Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
/**
2+
* Wrapper for the semantic range analysis library that mimics the
3+
* interface of the simple range analysis library.
4+
*/
5+
6+
private import cpp
7+
private import semmle.code.cpp.ir.IR
8+
private import experimental.semmle.code.cpp.semantic.SemanticBound
9+
private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
10+
private import RangeAnalysis
11+
12+
/**
13+
* Gets the lower bound of the expression.
14+
*
15+
* Note: expressions in C/C++ are often implicitly or explicitly cast to a
16+
* different result type. Such casts can cause the value of the expression
17+
* to overflow or to be truncated. This predicate computes the lower bound
18+
* of the expression without including the effect of the casts. To compute
19+
* the lower bound of the expression after all the casts have been applied,
20+
* call `lowerBound` like this:
21+
*
22+
* `lowerBound(expr.getFullyConverted())`
23+
*/
24+
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+
)
28+
}
29+
30+
/**
31+
* Gets the upper bound of the expression.
32+
*
33+
* Note: expressions in C/C++ are often implicitly or explicitly cast to a
34+
* different result type. Such casts can cause the value of the expression
35+
* to overflow or to be truncated. This predicate computes the upper bound
36+
* of the expression without including the effect of the casts. To compute
37+
* the upper bound of the expression after all the casts have been applied,
38+
* call `upperBound` like this:
39+
*
40+
* `upperBound(expr.getFullyConverted())`
41+
*/
42+
float upperBound(Expr expr) {
43+
exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
44+
semBounded(getSemanticExpr(i), b, result, true, _)
45+
)
46+
}
47+
48+
/**
49+
* Holds if the upper bound of `expr` may have been widened. This means the
50+
* upper bound is in practice likely to be overly wide.
51+
*/
52+
predicate upperBoundMayBeWidened(Expr e) { none() }
53+
54+
/**
55+
* Holds if `expr` has a provably empty range. For example:
56+
*
57+
* 10 < expr and expr < 5
58+
*
59+
* The range of an expression can only be empty if it can never be
60+
* executed. For example:
61+
*
62+
* ```cpp
63+
* if (10 < x) {
64+
* if (x < 5) {
65+
* // Unreachable code
66+
* return x; // x has an empty range: 10 < x && x < 5
67+
* }
68+
* }
69+
* ```
70+
*/
71+
predicate exprWithEmptyRange(Expr expr) { lowerBound(expr) > upperBound(expr) }
72+
73+
/** Holds if the definition might overflow negatively. */
74+
predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) { none() }
75+
76+
/** Holds if the definition might overflow positively. */
77+
predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) { none() }
78+
79+
/**
80+
* Holds if the definition might overflow (either positively or
81+
* negatively).
82+
*/
83+
predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) { none() }
84+
85+
/**
86+
* Holds if the expression might overflow negatively. This predicate
87+
* does not consider the possibility that the expression might overflow
88+
* due to a conversion.
89+
*/
90+
predicate exprMightOverflowNegatively(Expr expr) { none() }
91+
92+
/**
93+
* Holds if the expression might overflow negatively. Conversions
94+
* are also taken into account. For example the expression
95+
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
96+
* due to the addition.
97+
*/
98+
predicate convertedExprMightOverflowNegatively(Expr expr) { none() }
99+
100+
/**
101+
* Holds if the expression might overflow positively. This predicate
102+
* does not consider the possibility that the expression might overflow
103+
* due to a conversion.
104+
*/
105+
predicate exprMightOverflowPositively(Expr expr) { none() }
106+
107+
/**
108+
* Holds if the expression might overflow positively. Conversions
109+
* are also taken into account. For example the expression
110+
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
111+
* due to the addition.
112+
*/
113+
predicate convertedExprMightOverflowPositively(Expr expr) { none() }
114+
115+
/**
116+
* Holds if the expression might overflow (either positively or
117+
* negatively). The possibility that the expression might overflow
118+
* due to an implicit or explicit cast is also considered.
119+
*/
120+
predicate convertedExprMightOverflow(Expr expr) { none() }

0 commit comments

Comments
 (0)