Split out source and sinks into their cases

Author: jeongsoolee09

cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql

@@ -26,12 +26,21 @@ class ArrayDeclaration extends VariableDeclarationEntry {
    * Gets the declared length of this array.
    */
   int getLength() { result = length }
+
+  /**
+   * Gets the expression that the variable declared is initialized to, given there is such one.
+   */
+  Expr getInitExpr() { result = this.getVariable().getInitializer().getExpr() }
 }
 
 newtype TArrayAllocation =
   TStackAllocation(ArrayDeclaration arrayDecl) or
   TDynamicAllocation(AllocationFunction alloc)
 
+newtype TPointerFormation =
+  TArrayExpr(ArrayExprBA arrayExpr) or
+  TPointerArithmetic(PointerArithmeticOperation pointerArithmetic)
+
 class ArrayAllocation extends TArrayAllocation {
   ArrayDeclaration asStackAllocation() { this = TStackAllocation(result) }
 
@@ -48,44 +57,81 @@ class ArrayAllocation extends TArrayAllocation {
   }
 }
 
+class PointerFormation extends TPointerFormation {
+  ArrayExprBA asArrayExpr() { this = TArrayExpr(result) }
+
+  PointerArithmeticOperation asPointerArithmetic() { this = TPointerArithmetic(result) }
+
+  string toString() {
+    result = this.asArrayExpr().toString() or
+    result = this.asPointerArithmetic().toString()
+  }
+
+  int getOffset() {
+    result = this.asArrayExpr().getArrayOffset().getValue().toInt()
+    or
+    exists(PointerAddExpr pointerAddition | pointerAddition = this.asPointerArithmetic() |
+      result = pointerAddition.getAnOperand().getValue().toInt() // TODO: only get the number being added
+    )
+    or
+    exists(PointerSubExpr pointerSubtraction | pointerSubtraction = this.asPointerArithmetic() |
+      result = -pointerSubtraction.getAnOperand().getValue().toInt()
+    )
+  }
+
+  Expr asExpr() {
+    result = this.asArrayExpr() or
+    result = this.asPointerArithmetic()
+  }
+
+  DataFlow::Node getNode() {
+    result.asExpr() = this.asExpr() or
+    result.asIndirectExpr() = this.asExpr()
+  }
+}
+
 module TrackArrayConfig implements DataFlow::ConfigSig {
   predicate isSource(DataFlow::Node node) {
     /* 1. Declaring / Initializing an array-type variable */
-    exists(ArrayDeclaration arrayDecl |
-      node.asExpr() = arrayDecl.getVariable().getInitializer().getExpr()
+    exists(ArrayAllocation arrayAllocation |
+      node.asExpr() = arrayAllocation.asStackAllocation().getInitExpr()
     )
     or
     /* 2. Allocating dynamic memory as an array */
     none() // TODO
   }
 
   predicate isSink(DataFlow::Node node) {
-    /* 1. Pointer arithmetic */
-    exists(PointerArithmeticOperation pointerArithmetic |
-      node.asIndirectExpr() = pointerArithmetic.getAnOperand()
-    )
-    or
-    /* 2. Array access */
-    node.asExpr() instanceof ArrayExprBA
+    exists(PointerFormation pointerFormation | node = pointerFormation.getNode())
   }
 }
 
 module TrackArray = DataFlow::Global<TrackArrayConfig>;
 
 private predicate arrayDeclarationAndAccess(
-  DataFlow::Node arrayDeclaration, DataFlow::Node arrayAccess
+  DataFlow::Node arrayDeclarationNode, DataFlow::Node arrayAccessNode
 ) {
-  TrackArray::flow(arrayDeclaration, arrayAccess)
+  TrackArray::flow(arrayDeclarationNode, arrayAccessNode)
 }
 
 private predicate arrayIndexExceedsOutOfBounds(
-  DataFlow::Node arrayDeclaration, DataFlow::Node arrayAccess
+  DataFlow::Node arrayDeclarationNode, DataFlow::Node arrayAccessNode
 ) {
-  arrayDeclarationAndAccess(arrayDeclaration, arrayAccess) and
-  // exists(int declaredLength |
-  //   declaredLength = arrayDeclaration
-  // )
-  any() // TODO
+  /* 1. Ensure the array access is reachable from the array declaration. */
+  arrayDeclarationAndAccess(arrayDeclarationNode, arrayAccessNode) and
+  exists(ArrayAllocation arrayAllocation, PointerFormation pointerFormation |
+    arrayDeclarationNode.asExpr() = arrayAllocation.asStackAllocation().getInitExpr() and
+    arrayAccessNode = pointerFormation.getNode()
+  |
+    /* 2. Cases where a pointer formation becomes illegal. */
+    (
+      /* 2-1. An offset cannot be negative. */
+      pointerFormation.getOffset() < 0
+      or
+      /* 2-2. The offset should be at most (number of elements) + 1 = (the declared length). */
+      arrayAllocation.getLength() < pointerFormation.getOffset()
+    )
+  )
 }
 
 from Expr expr