Data flow: Update documentation on array flow modeling

Author: hvitved

docs/ql-libraries/dataflow/dataflow.md

@@ -419,20 +419,31 @@ class Content extends TContent {
 
 newtype TContentSet =
   TSingletonContent(Content c) or
+  TKnownOrUnknownArrayElementContent(TKnownArrayElementContent c) or
   TAnyArrayElementContent()
 
 class ContentSet extends TContentSet {
   Content getAStoreContent() {
     this = TSingletonContent(result)
     or
     // for reverse stores
+    this = TKnownOrUnknownArrayElementContent(result)
+    or
+    // for reverse stores
     this = TAnyArrayElementContent() and
     result = TUnknownArrayElementContent()
   }
 
   Content getAReadContent() {
     this = TSingletonContent(result)
     or
+    exists(TKnownArrayElementContent c |
+      this = TKnownOrUnknownArrayElementContent(c) |
+      result = c
+      or
+      result = TUnknownArrayElementContent()
+    )
+    or
     this = TAnyArrayElementContent() and
     (result = TUnknownArrayElementContent() or result = TKnownArrayElementContent(_))
   }
@@ -447,12 +458,10 @@ a[0] = tainted
 # storeStep(not_tainted, TSingletonContent(TKnownArrayElementContent(1)), [post update] a)
 a[1] = not_tainted
 
-# readStep(a, TSingletonContent(TKnownArrayElementContent(0)), a[0])
-# readStep(a, TSingletonContent(TUnknownArrayElementContent()), a[0])
+# readStep(a, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), a[0])
 sink(a[0]) # bad
 
-# readStep(a, TSingletonContent(TKnownArrayElementContent(1)), a[1])
-# readStep(a, TSingletonContent(TUnknownArrayElementContent()), a[1])
+# readStep(a, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(1)), a[1])
 sink(a[1]) # good
 
 # readStep(a, TAnyArrayElementContent(), a[unknown])
@@ -461,26 +470,24 @@ sink(a[unknown]) # bad; unknown may be 0
 # storeStep(tainted, TSingletonContent(TUnknownArrayElementContent()), [post update] b)
 b[unknown] = tainted
 
-# readStep(b, TSingletonContent(TKnownArrayElementContent(0)), b[0])
-# readStep(b, TSingletonContent(TUnknownArrayElementContent()), b[0])
+# readStep(b, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), b[0])
 sink(b[0]) # bad; unknown may be 0
 
-# storeStep(tainted, TSingletonContent(TKnownArrayElementContent(0)), [post update] c[unknown])
-# storeStep(not_tainted, TSingletonContent(TKnownArrayElementContent(1)), [post update] c[unknown])
-# readStep(c, TAnyArrayElementContent(), c[unknown])
-# storeStep([post update] c[unknown], TAnyArrayElementContent(), [post update] c) # auto-generated reverse store (see Example 2)
-c[unknown][0] = tainted
-c[unknown][1] = not_tainted
-
-
-# readStep(c[0], TSingletonContent(TKnownArrayElementContent(0)), c[0][0])
-# readStep(c[0], TSingletonContent(TUnknownArrayElementContent()), c[0][0])
-# readStep(c[0], TSingletonContent(TKnownArrayElementContent(1)), c[0][1])
-# readStep(c[0], TSingletonContent(TUnknownArrayElementContent()), c[0][1])
-# readStep(c, TSingletonContent(TKnownArrayElementContent(0)), c[0])
-# readStep(c, TSingletonContent(TUnknownArrayElementContent()), c[0])
+# storeStep(tainted, TSingletonContent(TUnknownArrayElementContent()), [post update] c[0])
+# storeStep(not_tainted, TSingletonContent(TUnknownArrayElementContent()), [post update] c[1])
+# readStep(c, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), c[0])
+# readStep(c, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(1)), c[1])
+# storeStep([post update] c[0], TSingletonContent(TKnownArrayElementContent(0)), [post update] c) # auto-generated reverse store (see Example 2)
+# storeStep([post update] c[1], TSingletonContent(TKnownArrayElementContent(1)), [post update] c) # auto-generated reverse store (see Example 2)
+c[0][unknown] = tainted
+c[1][unknown] = not_tainted
+
+# readStep(c[0], TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), c[0][0])
+# readStep(c[1], TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), c[1][0])
+# readStep(c, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(0)), c[0])
+# readStep(c, TKnownOrUnknownArrayElementContent(TKnownArrayElementContent(1)), c[1])
 sink(c[0][0]) # bad; unknown may be 0
-sink(c[0][1]) # good
+sink(c[1][0]) # good
 ```
 
 ### Field flow barriers