@@ -151,12 +151,31 @@ deprecated class ConversionWithoutBoundsCheckConfig extends TaintTracking::Confi
151
151
}
152
152
}
153
153
154
+ private int validBitsize ( ) { result = [ 7 , 8 , 15 , 16 , 31 , 32 , 63 , 64 ] }
155
+
156
+ private newtype TMaxValueState =
157
+ TMkConcrete ( int bitSize ) { bitSize = validBitsize ( ) } or
158
+ TMkArchitectureDependent ( boolean isSigned ) { isSigned = [ true , false ] }
159
+
154
160
/** Flow state for ConversionWithoutBoundsCheckConfig. */
155
- newtype IntegerConversionFlowState =
156
- TFlowstate ( int bitSize , boolean isSigned ) {
157
- bitSize = [ 0 , 8 , 16 , 32 , 64 ] and
158
- isSigned = [ true , false ]
161
+ private class MaxValueState extends TMaxValueState {
162
+ /**
163
+ * Gets the smallest valid bitsize `result` where the maximum value that
164
+ * could have been parsed fits into an integer type whose maximum value is
165
+ * 2^(result) - 1.
166
+ */
167
+ int getConcreteBitsize ( ) { this = TMkConcrete ( result ) }
168
+
169
+ /** Gets the signedness of an architecture-dependent flow state. */
170
+ boolean getArchictureDependentSignedness ( ) { this = TMkArchitectureDependent ( result ) }
171
+
172
+ string toString ( ) {
173
+ result = "Concrete MaxValueState(max value <= 2^(" + this .getConcreteBitsize ( ) + ")-1)" or
174
+ result =
175
+ "Architecture-dependent MaxValueState(signed = " + this .getArchictureDependentSignedness ( ) +
176
+ ")"
159
177
}
178
+ }
160
179
161
180
/**
162
181
* The integer type with bit size `bitSize` and signedness `isSigned` has
@@ -172,21 +191,13 @@ private int f(int bitSize, boolean isSigned, int bitSizeForZero) {
172
191
}
173
192
174
193
private module ConversionWithoutBoundsCheckConfig implements DataFlow:: StateConfigSig {
175
- class FlowState extends IntegerConversionFlowState {
176
- /** Gets the signedness of the flow state. */
177
- boolean getIsSigned ( ) { this = TFlowstate ( _, result ) }
178
-
179
- /** Gets the bit size of the flow state. */
180
- int getBitSize ( ) { this = TFlowstate ( result , _) }
181
-
182
- string toString ( ) { result = "FlowState(" + this .getBitSize ( ) + "," + this .getIsSigned ( ) + ")" }
183
- }
194
+ class FlowState = MaxValueState ;
184
195
185
196
predicate isSource ( DataFlow:: Node source , FlowState state ) {
186
197
exists (
187
198
DataFlow:: CallNode c , IntegerParser:: Range ip , int apparentBitSize , int effectiveBitSize
188
199
|
189
- c . getTarget ( ) = ip and
200
+ c = ip . getACall ( ) and
190
201
source = c .getResult ( 0 ) and
191
202
(
192
203
apparentBitSize = ip .getTargetBitSize ( )
@@ -208,8 +219,8 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
208
219
// if assigned the maximum value that can be parsed by `ip`. If both the
209
220
// source and the sink are `int` or `uint` then overflow can only happen
210
221
// if we are converting from `uint` to `int`.
211
- if state . getBitSize ( ) = 0 and effectiveBitSize = 0
212
- then ip . isSigned ( ) = false and state . getIsSigned ( ) = true
222
+ if effectiveBitSize = 0
223
+ then state . getArchictureDependentSignedness ( ) = ip . isSigned ( )
213
224
else
214
225
// The maximum value for a signed type with n bits is 2^(n - 1) - 1.
215
226
// The maximum value for an unsigned type with n bits is 2^n - 1. To
@@ -219,7 +230,13 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
219
230
// catch that flow from `int64` to `int` is incorrect on a 32-bit
220
231
// architecture), and we have already dealt with the case that both
221
232
// source and sink are `int` or `uint`.
222
- f ( state .getBitSize ( ) , state .getIsSigned ( ) , 32 ) < f ( effectiveBitSize , ip .isSigned ( ) , 64 )
233
+ state .getConcreteBitsize ( ) =
234
+ min ( int bitsize |
235
+ bitsize = validBitsize ( ) and
236
+ f ( effectiveBitSize , ip .isSigned ( ) , 64 ) <= state .getConcreteBitsize ( )
237
+ |
238
+ bitsize
239
+ )
223
240
)
224
241
}
225
242
0 commit comments