Skip to content

Commit e8800a6

Browse files
committed
C++: Move the new range-analysis library out of experimental and into an 'internal' directory.
1 parent 53de9ae commit e8800a6

27 files changed

+4552
-0
lines changed
Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
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 semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound
9+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
10+
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.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) {
84+
defMightOverflowNegatively(def, v) or
85+
defMightOverflowPositively(def, v)
86+
}
87+
88+
/**
89+
* Holds if the expression might overflow negatively. This predicate
90+
* does not consider the possibility that the expression might overflow
91+
* due to a conversion.
92+
*/
93+
predicate exprMightOverflowNegatively(Expr expr) { none() }
94+
95+
/**
96+
* Holds if the expression might overflow negatively. Conversions
97+
* are also taken into account. For example the expression
98+
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
99+
* due to the addition.
100+
*/
101+
predicate convertedExprMightOverflowNegatively(Expr expr) {
102+
exprMightOverflowNegatively(expr) or
103+
convertedExprMightOverflowNegatively(expr.getConversion())
104+
}
105+
106+
/**
107+
* Holds if the expression might overflow positively. This predicate
108+
* does not consider the possibility that the expression might overflow
109+
* due to a conversion.
110+
*/
111+
predicate exprMightOverflowPositively(Expr expr) { none() }
112+
113+
/**
114+
* Holds if the expression might overflow positively. Conversions
115+
* are also taken into account. For example the expression
116+
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
117+
* due to the addition.
118+
*/
119+
predicate convertedExprMightOverflowPositively(Expr expr) {
120+
exprMightOverflowPositively(expr) or
121+
convertedExprMightOverflowPositively(expr.getConversion())
122+
}
123+
124+
/**
125+
* Holds if the expression might overflow (either positively or
126+
* negatively). The possibility that the expression might overflow
127+
* due to an implicit or explicit cast is also considered.
128+
*/
129+
predicate convertedExprMightOverflow(Expr expr) {
130+
convertedExprMightOverflowNegatively(expr) or
131+
convertedExprMightOverflowPositively(expr)
132+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
import SemanticExpr
2+
import SemanticBound
3+
import SemanticSSA
4+
import SemanticGuard
5+
import SemanticCFG
6+
import SemanticType
7+
import SemanticOpcode
Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
/**
2+
* Semantic wrapper around the language-specific bounds library.
3+
*/
4+
5+
private import SemanticExpr
6+
private import SemanticExprSpecific::SemanticExprConfig as Specific
7+
private import SemanticSSA
8+
private import SemanticLocation
9+
10+
/**
11+
* A valid base for an expression bound.
12+
*
13+
* Can be either a variable (`SemSsaBound`) or zero (`SemZeroBound`).
14+
*/
15+
class SemBound instanceof Specific::Bound {
16+
final string toString() { result = super.toString() }
17+
18+
final SemLocation getLocation() { result = super.getLocation() }
19+
20+
final SemExpr getExpr(int delta) { result = Specific::getBoundExpr(this, delta) }
21+
}
22+
23+
/**
24+
* A bound that is a constant zero.
25+
*/
26+
class SemZeroBound extends SemBound {
27+
SemZeroBound() { Specific::zeroBound(this) }
28+
}
29+
30+
/**
31+
* A bound that is an SSA definition.
32+
*/
33+
class SemSsaBound extends SemBound {
34+
/**
35+
* The variables whose value is used as the bound.
36+
*
37+
* Can be multi-valued in some implementations. If so, all variables will be equivalent.
38+
*/
39+
SemSsaVariable var;
40+
41+
SemSsaBound() { Specific::ssaBound(this, var) }
42+
43+
/** Gets a variable whose value is used as the bound. */
44+
final SemSsaVariable getAVariable() { result = var }
45+
}
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/**
2+
* Semantic interface to the control flow graph.
3+
*/
4+
5+
private import Semantic
6+
private import SemanticExprSpecific::SemanticExprConfig as Specific
7+
8+
/**
9+
* A basic block in the control-flow graph.
10+
*/
11+
class SemBasicBlock extends Specific::BasicBlock {
12+
/** Holds if this block (transitively) dominates `otherblock`. */
13+
final predicate bbDominates(SemBasicBlock otherBlock) { Specific::bbDominates(this, otherBlock) }
14+
15+
/** Holds if this block has dominance information. */
16+
final predicate hasDominanceInformation() { Specific::hasDominanceInformation(this) }
17+
18+
/** Gets an expression that is evaluated in this basic block. */
19+
final SemExpr getAnExpr() { result.getBasicBlock() = this }
20+
21+
final int getUniqueId() { result = Specific::getBasicBlockUniqueId(this) }
22+
}

0 commit comments

Comments
 (0)