Java: Introduce index validation.

Author: michaelnebel

java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll

@@ -233,6 +233,8 @@ module ModelValidation {
         or
         part = input.(AccessPath).getToken(0) and
         parseParam(part, _)
+        or
+        invalidIndexComponent(input, part)
       ) and
       result = "Unrecognized input specification \"" + part + "\" in " + pred + " model."
     )
@@ -244,9 +246,13 @@ module ModelValidation {
       or
       summaryModel(_, _, _, _, _, _, _, output, _, _) and pred = "summary"
     |
-      invalidSpecComponent(output, part) and
-      not part = "" and
-      not (part = ["Argument", "Parameter"] and pred = "source") and
+      (
+        invalidSpecComponent(output, part) and
+        not part = "" and
+        not (part = ["Argument", "Parameter"] and pred = "source")
+        or
+        invalidIndexComponent(output, part)
+      ) and
       result = "Unrecognized output specification \"" + part + "\" in " + pred + " model."
     )
   }

java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll

@@ -1050,6 +1050,16 @@ module Private {
       not exists(interpretComponent(c))
     }
 
+    /**
+     * Holds if token `part` of specification `spec` has an invalid index.
+     * E.g., `Argument[-1]`.
+     */
+    predicate invalidIndexComponent(AccessPath spec, AccessPathToken part) {
+      part = spec.getToken(_) and
+      part.getName() = ["Parameter", "Argument"] and
+      AccessPath::parseInt(part.getArgumentList()) < 0
+    }
+
     private predicate inputNeedsReference(AccessPathToken c) {
       c.getName() = "Argument" or
       inputNeedsReferenceSpecific(c)