@@ -329,11 +329,28 @@ class ContentSet extends TContentSet {
329329 /** Holds if this content set represents all `ElementContent`s. */
330330 predicate isAnyElement ( ) { this = TAnyElementContent ( ) }
331331
332+ /**
333+ * Holds if this content set represents a specific known element index, or an
334+ * unknown element index.
335+ */
336+ predicate isKnownOrUnknownElement ( Content:: KnownElementContent c ) {
337+ this = TKnownOrUnknownElementContent ( c )
338+ }
339+
332340 /**
333341 * Holds if this content set represents all `KnownElementContent`s where
334342 * the index is an integer greater than or equal to `lower`.
335343 */
336- predicate isElementLowerBound ( int lower ) { this = TElementLowerBoundContent ( lower ) }
344+ predicate isElementLowerBound ( int lower ) { this = TElementLowerBoundContent ( lower , false ) }
345+
346+ /**
347+ * Holds if this content set represents `UnknownElementContent` unioned with
348+ * all `KnownElementContent`s where the index is an integer greater than or
349+ * equal to `lower`.
350+ */
351+ predicate isElementLowerBoundOrUnknown ( int lower ) {
352+ this = TElementLowerBoundContent ( lower , true )
353+ }
337354
338355 /** Gets a textual representation of this content set. */
339356 string toString ( ) {
@@ -345,8 +362,18 @@ class ContentSet extends TContentSet {
345362 this .isAnyElement ( ) and
346363 result = "any element"
347364 or
348- exists ( int lower |
349- this .isElementLowerBound ( lower ) and
365+ exists ( Content:: KnownElementContent c |
366+ this .isKnownOrUnknownElement ( c ) and
367+ result = c + " or unknown"
368+ )
369+ or
370+ exists ( int lower , boolean includeUnknown |
371+ this = TElementLowerBoundContent ( lower , includeUnknown )
372+ |
373+ includeUnknown = false and
374+ result = lower + "..!"
375+ or
376+ includeUnknown = true and
350377 result = lower + ".."
351378 )
352379 }
@@ -355,9 +382,18 @@ class ContentSet extends TContentSet {
355382 Content getAStoreContent ( ) {
356383 this .isSingleton ( result )
357384 or
385+ // For reverse stores, `a[unknown][0] = x`, it is important that the read-step
386+ // from `a` to `a[unknown]` (which can read any element), gets translated into
387+ // a reverse store step that store only into `?`
358388 this .isAnyElement ( ) and
359389 result = TUnknownElementContent ( )
360390 or
391+ // For reverse stores, `a[1][0] = x`, it is important that the read-step
392+ // from `a` to `a[1]` (which can read both elements stored at exactly index `1`
393+ // and elements stored at unknown index), gets translated into a reverse store
394+ // step that store only into `1`
395+ this .isKnownOrUnknownElement ( result )
396+ or
361397 this .isElementLowerBound ( _) and
362398 result = TUnknownElementContent ( )
363399 }
@@ -369,10 +405,21 @@ class ContentSet extends TContentSet {
369405 this .isAnyElement ( ) and
370406 result instanceof Content:: ElementContent
371407 or
372- exists ( int lower , int i |
373- this .isElementLowerBound ( lower ) and
374- result .( Content:: KnownElementContent ) .getIndex ( ) .isInt ( i ) and
375- i >= lower
408+ exists ( Content:: KnownElementContent c | this .isKnownOrUnknownElement ( c ) |
409+ result = c or
410+ result = TUnknownElementContent ( )
411+ )
412+ or
413+ exists ( int lower , boolean includeUnknown |
414+ this = TElementLowerBoundContent ( lower , includeUnknown )
415+ |
416+ exists ( int i |
417+ result .( Content:: KnownElementContent ) .getIndex ( ) .isInt ( i ) and
418+ i >= lower
419+ )
420+ or
421+ includeUnknown = true and
422+ result = TUnknownElementContent ( )
376423 )
377424 }
378425}
0 commit comments