@@ -2,7 +2,7 @@ private import cpp
22private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr
33private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
44
5- float evaluateConstantExpr2 ( Expr e ) {
5+ float evaluateConstantExpr ( Expr e ) {
66 result = e .getValue ( ) .toFloat ( )
77 or
88 // This handles when a constant value is put into a variable
@@ -18,7 +18,6 @@ float evaluateConstantExpr2(Expr e) {
1818// architecture where the shift value is masked with 0b00011111, but we can't
1919// assume the architecture).
2020bindingset [ val]
21- pragma [ inline]
2221private predicate isValidShiftExprShift ( float val , Expr l ) {
2322 val >= 0 and
2423 // We use getFullyConverted because the spec says to use the *promoted* left operand
@@ -32,9 +31,121 @@ private predicate canLShiftOverflow(int val, int shift, int max_val) {
3231}
3332
3433/**
35- * This handles the `<<` and `<<=` operators when at least one operand is a constant (and if the right operand
36- * is a constant, it must be "valid" (see `isValidShiftExprShift`)). When handling any undefined behavior, it
37- * leaves the values unconstrained. From the C++ standard: "The behavior is undefined if the right
34+ * A range analysis expression consisting of the `>>` or `>>=` operator when at least
35+ * one operand is a constant (and if the right operand is a constant, it must be "valid"
36+ * (see `isValidShiftExprShift`)). When handling any undefined behavior, it leaves the
37+ * values unconstrained. From the C++ standard: "The behavior is undefined if the right
38+ * operand is negative, or greater than or equal to the length in bits of the promoted
39+ * left operand. The value of E1 >> E2 is E1 right-shifted E2 bit positions. If E1 has an
40+ * unsigned type or if E1 has a signed type and a non-negative value, the value of the
41+ * result is the integral part of the quotient of E1/2^E2. If E1 has a signed type and a
42+ * negative value, the resulting value is implementation-defined."
43+ */
44+ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
45+ /**
46+ * Holds for `a >> b` or `a >>= b` in one of the following two cases:
47+ * 1. `a` is a constant and `b` is not
48+ * 2. `b` is constant
49+ *
50+ * We don't handle the case where `a` and `b` are both non-constant values.
51+ */
52+ ConstantRShiftExprRange ( ) {
53+ getUnspecifiedType ( ) instanceof IntegralType and
54+ exists ( Expr l , Expr r |
55+ l = this .( RShiftExpr ) .getLeftOperand ( ) and
56+ r = this .( RShiftExpr ) .getRightOperand ( )
57+ or
58+ l = this .( AssignRShiftExpr ) .getLValue ( ) and
59+ r = this .( AssignRShiftExpr ) .getRValue ( )
60+ |
61+ l .getUnspecifiedType ( ) instanceof IntegralType and
62+ r .getUnspecifiedType ( ) instanceof IntegralType and
63+ (
64+ // If the left operand is a constant, verify that the right operand is not a constant
65+ exists ( evaluateConstantExpr ( l ) ) and not exists ( evaluateConstantExpr ( r ) )
66+ or
67+ // If the right operand is a constant, check if it is a valid shift expression
68+ exists ( float constROp |
69+ constROp = evaluateConstantExpr ( r ) and isValidShiftExprShift ( constROp , l )
70+ )
71+ )
72+ )
73+ }
74+
75+ Expr getLeftOperand ( ) {
76+ result = this .( RShiftExpr ) .getLeftOperand ( ) or
77+ result = this .( AssignRShiftExpr ) .getLValue ( )
78+ }
79+
80+ Expr getRightOperand ( ) {
81+ result = this .( RShiftExpr ) .getRightOperand ( ) or
82+ result = this .( AssignRShiftExpr ) .getRValue ( )
83+ }
84+
85+ override float getLowerBounds ( ) {
86+ exists ( int lLower , int lUpper , int rLower , int rUpper |
87+ lLower = getFullyConvertedLowerBounds ( getLeftOperand ( ) ) and
88+ lUpper = getFullyConvertedUpperBounds ( getLeftOperand ( ) ) and
89+ rLower = getFullyConvertedLowerBounds ( getRightOperand ( ) ) and
90+ rUpper = getFullyConvertedUpperBounds ( getRightOperand ( ) ) and
91+ lLower <= lUpper and
92+ rLower <= rUpper
93+ |
94+ if
95+ lLower < 0
96+ or
97+ not (
98+ isValidShiftExprShift ( rLower , getLeftOperand ( ) ) and
99+ isValidShiftExprShift ( rUpper , getLeftOperand ( ) )
100+ )
101+ then
102+ // We don't want to deal with shifting negative numbers at the moment,
103+ // and a negative shift is implementation defined, so we set the result
104+ // to the minimum value
105+ result = exprMinVal ( this )
106+ else
107+ // We can get the smallest value by shifting the smallest bound by the largest bound
108+ result = lLower .bitShiftRight ( rUpper )
109+ )
110+ }
111+
112+ override float getUpperBounds ( ) {
113+ exists ( int lLower , int lUpper , int rLower , int rUpper |
114+ lLower = getFullyConvertedLowerBounds ( getLeftOperand ( ) ) and
115+ lUpper = getFullyConvertedUpperBounds ( getLeftOperand ( ) ) and
116+ rLower = getFullyConvertedLowerBounds ( getRightOperand ( ) ) and
117+ rUpper = getFullyConvertedUpperBounds ( getRightOperand ( ) ) and
118+ lLower <= lUpper and
119+ rLower <= rUpper
120+ |
121+ if
122+ lLower < 0
123+ or
124+ not (
125+ isValidShiftExprShift ( rLower , getLeftOperand ( ) ) and
126+ isValidShiftExprShift ( rUpper , getLeftOperand ( ) )
127+ )
128+ then
129+ // We don't want to deal with shifting negative numbers at the moment,
130+ // and a negative shift is implementation defined, so we set the result
131+ // to the maximum value
132+ result = exprMaxVal ( this )
133+ else
134+ // We can get the largest value by shifting the largest bound by the smallest bound
135+ result = lUpper .bitShiftRight ( rLower )
136+ )
137+ }
138+
139+ override predicate dependsOnChild ( Expr child ) {
140+ child = getLeftOperand ( ) or child = getLeftOperand ( )
141+ }
142+ }
143+
144+ /**
145+ * A range analysis expression consisting of the `<<` or `<<=` operator when at least
146+ * one operand is a constant (and if the right operand is a constant, it must be "valid"
147+ * (see `isValidShiftExprShift`)). When handling any undefined behavior, it leaves the
148+ * values unconstrained. From the C++ standard: "The behavior is undefined if the right
38149 * operand is negative, or greater than or equal to the length in bits of the promoted left operand.
39150 * The value of E1 << E2 is E1 left-shifted E2 bit positions; vacated bits are zero-filled. If E1
40151 * has an unsigned type, the value of the result is E1 × 2 E2, reduced modulo one more than the
@@ -64,11 +175,11 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
64175 r .getUnspecifiedType ( ) instanceof IntegralType and
65176 (
66177 // If the left operand is a constant, verify that the right operand is not a constant
67- exists ( evaluateConstantExpr2 ( l ) ) and not exists ( evaluateConstantExpr2 ( r ) )
178+ exists ( evaluateConstantExpr ( l ) ) and not exists ( evaluateConstantExpr ( r ) )
68179 or
69180 // If the right operand is a constant, check if it is a valid shift expression
70181 exists ( float constROp |
71- constROp = evaluateConstantExpr2 ( r ) and isValidShiftExprShift ( constROp , l )
182+ constROp = evaluateConstantExpr ( r ) and isValidShiftExprShift ( constROp , l )
72183 )
73184 )
74185 )
@@ -109,7 +220,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
109220 // (a shift of 1) but doing a shift by the upper bound would give 0b01000000.
110221 // So if the left shift operation causes an overflow, we just assume the max value
111222 // If necessary, we may be able to improve this bound in the future
112- if canLShiftOverflow ( lUpper , rUpper , exprMaxVal ( this ) . ( int ) )
223+ if canLShiftOverflow ( lUpper , rUpper , exprMaxVal ( this ) )
113224 then result = exprMinVal ( this )
114225 else result = lLower .bitShiftLeft ( rLower )
115226 )
@@ -140,7 +251,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
140251 // (a shift of 1) but doing a shift by the upper bound would give 0b01000000.
141252 // So if the left shift operation causes an overflow, we just assume the max value
142253 // If necessary, we may be able to improve this bound in the future
143- if canLShiftOverflow ( lUpper , rUpper , exprMaxVal ( this ) . ( int ) )
254+ if canLShiftOverflow ( lUpper , rUpper , exprMaxVal ( this ) )
144255 then result = exprMaxVal ( this )
145256 else result = lUpper .bitShiftLeft ( rUpper )
146257 )
0 commit comments