@@ -210,9 +210,28 @@ module Array {
210210 }
211211 }
212212
213+ private predicate isKnownRange ( RangeLiteral rl , int start , int end ) {
214+ (
215+ // Either an explicit, positive beginning index...
216+ start = rl .getBegin ( ) .getConstantValue ( ) .getInt ( ) and start >= 0
217+ or
218+ // Or a begin-less one, since `..n` is equivalent to `0..n`
219+ not exists ( rl .getBegin ( ) ) and start = 0
220+ ) and
221+ // There must be an explicit end. An end-less range like `2..` is not
222+ // treated as a known range, since we don't track the length of the array.
223+ exists ( int e | e = rl .getEnd ( ) .getConstantValue ( ) .getInt ( ) and e >= 0 |
224+ rl .isInclusive ( ) and end = e
225+ or
226+ rl .isExclusive ( ) and end = e - 1
227+ )
228+ }
229+
213230 /**
214231 * A call to `[]` with an unknown argument, which could be either an index or
215- * a range.
232+ * a range. To avoid spurious flow, we are going to ignore the possibility
233+ * that the argument might be a range (unless it is an explicit range literal,
234+ * see `ElementReferenceRangeReadUnknownSummary`).
216235 */
217236 private class ElementReferenceReadUnknownSummary extends ElementReferenceReadSummary {
218237 ElementReferenceReadUnknownSummary ( ) {
@@ -223,7 +242,7 @@ module Array {
223242
224243 override predicate propagatesFlowExt ( string input , string output , boolean preservesValue ) {
225244 input = "Argument[self].Element[any]" and
226- output = [ "ReturnValue" , "ReturnValue.Element[?]" ] and
245+ output = "ReturnValue" and
227246 preservesValue = true
228247 }
229248 }
@@ -242,24 +261,8 @@ module Array {
242261 )
243262 or
244263 mc .getNumberOfArguments ( ) = 1 and
245- exists ( RangeLiteral rl |
246- rl = mc .getArgument ( 0 ) and
247- (
248- // Either an explicit, positive beginning index...
249- start = rl .getBegin ( ) .getConstantValue ( ) .getInt ( ) and start >= 0
250- or
251- // Or a begin-less one, since `..n` is equivalent to `0..n`
252- not exists ( rl .getBegin ( ) ) and start = 0
253- ) and
254- // There must be an explicit end. An end-less range like `2..` is not
255- // treated as a known range, since we don't track the length of the array.
256- exists ( int e | e = rl .getEnd ( ) .getConstantValue ( ) .getInt ( ) and e >= 0 |
257- rl .isInclusive ( ) and end = e
258- or
259- rl .isExclusive ( ) and end = e - 1
260- ) and
261- this = methodName + "(" + start + ".." + end + ")"
262- )
264+ isKnownRange ( mc .getArgument ( 0 ) , start , end ) and
265+ this = methodName + "(" + start + ".." + end + ")"
263266 }
264267
265268 override predicate propagatesFlowExt ( string input , string output , boolean preservesValue ) {
@@ -291,12 +294,7 @@ module Array {
291294 )
292295 or
293296 mc .getNumberOfArguments ( ) = 1 and
294- exists ( RangeLiteral rl | rl = mc .getArgument ( 0 ) |
295- exists ( rl .getBegin ( ) ) and
296- not exists ( int b | b = rl .getBegin ( ) .getConstantValue ( ) .getInt ( ) and b >= 0 )
297- or
298- not exists ( int e | e = rl .getEnd ( ) .getConstantValue ( ) .getInt ( ) and e >= 0 )
299- )
297+ mc .getArgument ( 0 ) = any ( RangeLiteral range | not isKnownRange ( range , _, _) )
300298 )
301299 }
302300
0 commit comments