C++: Use range analysis to properly deduce the initial 'state2' instead of traversing the AST. Also fix state-passing related to negative states.

cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql

@@ -39,49 +39,27 @@ predicate bounded(Instruction i, Instruction b, int delta) {
   )
 }
 
-/**
- * Holds if the combination of `n` and `state` represents an appropriate
- * source for the expression `e` suitable for use-use flow.
- */
-private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
-  // The simple case: If the size is a variable access with no qualifier we can just use the
-  // dataflow node for that expression and no state.
-  exists(VariableAccess va |
-    va = e and
-    not va instanceof FieldAccess and
-    n.asConvertedExpr() = va.getFullyConverted() and
-    state = "0"
-  )
-  or
-  // If the size is a choice between two expressions we allow both to be nodes representing the size.
-  exists(ConditionalExpr cond | cond = e | hasSizeImpl([cond.getThen(), cond.getElse()], n, state))
-  or
-  // If the size is an expression plus a constant, we pick the dataflow node of the expression and
-  // remember the constant in the state.
-  exists(Expr const, Expr nonconst |
-    e.(AddExpr).hasOperands(const, nonconst) and
-    state = const.getValue() and
-    hasSizeImpl(nonconst, n, _)
-  )
-  or
-  exists(Expr const, Expr nonconst |
-    e.(SubExpr).hasOperands(const, nonconst) and
-    state = "-" + const.getValue() and
-    hasSizeImpl(nonconst, n, _)
-  )
-}
+VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
 
 /**
  * Holds if `(n, state)` pair represents the source of flow for the size
  * expression associated with `alloc`.
  */
 predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
-  hasSizeImpl(alloc.getSizeExpr(), n, state)
+  exists(VariableAccess va, Expr size, int delta |
+    size = alloc.getSizeExpr() and
+    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
+    va = unique( | | getAVariableAccess(size)) and
+    // Compute `delta` as the constant difference between `x` and `x + 1`.
+    bounded(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
+      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
+    n.asConvertedExpr() = va.getFullyConverted() and
+    state = delta.toString()
+  )
 }
 
 predicate isSinkPairImpl(
-  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf,
-  Expr eSize
+  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
 ) {
   exists(int bufIndex, int sizeIndex, Instruction sizeInstr, Instruction bufInstr |
     bufInstr = bufSink.asInstruction() and
@@ -89,9 +67,7 @@ predicate isSinkPairImpl(
     sizeInstr = sizeSink.asInstruction() and
     c.getStaticCallTarget().(ArrayFunction).hasArrayWithVariableSize(bufIndex, sizeIndex) and
     bounded(c.getArgument(sizeIndex), sizeInstr, delta) and
-    eSize = sizeInstr.getUnconvertedResultExpression() and
-    eBuf = bufInstr.getUnconvertedResultExpression() and
-    delta >= 1
+    eBuf = bufInstr.getUnconvertedResultExpression()
   )
 }
 
@@ -117,9 +93,9 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
     DataFlow::FlowState state2
   ) {
     state1 instanceof DataFlow::FlowStateEmpty and
-    state2 = [0 .. 32].toString() and // An arbitrary bound because we need to bound `state2`
+    state2 = [-32 .. 32].toString() and // An arbitrary bound because we need to bound `state2`
     exists(int delta |
-      isSinkPairImpl(_, bufSink, sizeSink, delta, _, _) and
+      isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
       delta > state2.toInt()
     )
   }
@@ -129,7 +105,7 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
     DataFlow::FlowState state2
   ) {
     exists(AddInstruction add, Operand op, int delta, int s1, int s2 |
-      s1 = [0 .. 32] and // An arbitrary bound because we need to bound `state`
+      s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state`
       state1 = s1.toString() and
       state2 = s2.toString() and
       add.hasOperands(node1.asOperand(), op) and
@@ -142,13 +118,14 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
 
 from
   StringSizeConfiguration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
-  DataFlow::PathNode sink1, DataFlow2::PathNode sink2, int k, CallInstruction c,
-  DataFlow::Node sourceNode, Expr bound, Expr buffer, string element
+  DataFlow::PathNode sink1, DataFlow2::PathNode sink2, int overflow, int sinkState,
+  CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element
 where
   conf.hasFlowPath(source1, source2, sink1, sink2) and
-  k > sink2.getState().toInt() and
-  isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), k, buffer, bound) and
+  sinkState = sink2.getState().toInt() and
+  isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
+  overflow > 0 and
   sourceNode = source1.getNode() and
-  if k = 1 then element = " element." else element = " elements."
+  if overflow = 1 then element = " element." else element = " elements."
 select c.getUnconvertedResultExpression(), source1, sink1,
-  "This write may overflow $@ by " + k + element, buffer, buffer.toString()
+  "This write may overflow $@ by " + overflow + element, buffer, buffer.toString()