Merge pull request github#12800 from MathiasVP/fix-joins-in-constant-array-overflow

C++: Fix joins in `cpp/constant-array-overflow`

Author: MathiasVP

cpp/ql/src/experimental/Security/CWE/CWE-193/ConstantSizeArrayOffByOne.ql

@@ -25,16 +25,23 @@ Instruction getABoundIn(SemBound b, IRFunction func) {
 /**
  * Holds if `i <= b + delta`.
  */
-bindingset[i]
-pragma[inline_late]
-predicate bounded(Instruction i, Instruction b, int delta) {
+pragma[inline]
+predicate boundedImpl(Instruction i, Instruction b, int delta) {
   exists(SemBound bound, IRFunction func |
     semBounded(getSemanticExpr(i), bound, delta, true, _) and
     b = getABoundIn(bound, func) and
-    i.getEnclosingIRFunction() = func
+    pragma[only_bind_out](i.getEnclosingIRFunction()) = func
   )
 }
 
+bindingset[i]
+pragma[inline_late]
+predicate bounded1(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
+
+bindingset[b]
+pragma[inline_late]
+predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
+
 module FieldAddressToPointerArithmeticConfig implements DataFlow::ConfigSig {
   predicate isSource(DataFlow::Node source) { isFieldAddressSource(_, source) }
 
@@ -50,23 +57,39 @@ predicate isFieldAddressSource(Field f, DataFlow::Node source) {
   source.asInstruction().(FieldAddressInstruction).getField() = f
 }
 
+bindingset[delta]
+predicate isInvalidPointerDerefSinkImpl(
+  int delta, Instruction i, AddressOperand addr, string operation
+) {
+  delta >= 0 and
+  i.getAnOperand() = addr and
+  (
+    i instanceof StoreInstruction and
+    operation = "write"
+    or
+    i instanceof LoadInstruction and
+    operation = "read"
+  )
+}
+
 /**
  * Holds if `sink` is a sink for `InvalidPointerToDerefConf` and `i` is a `StoreInstruction` that
  * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
  * reads from an address that non-strictly upper-bounds `sink`.
  */
 pragma[inline]
-predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string operation) {
+predicate isInvalidPointerDerefSink1(DataFlow::Node sink, Instruction i, string operation) {
   exists(AddressOperand addr, int delta |
-    bounded(addr.getDef(), sink.asInstruction(), delta) and
-    delta >= 0 and
-    i.getAnOperand() = addr
-  |
-    i instanceof StoreInstruction and
-    operation = "write"
-    or
-    i instanceof LoadInstruction and
-    operation = "read"
+    bounded1(addr.getDef(), sink.asInstruction(), delta) and
+    isInvalidPointerDerefSinkImpl(delta, i, addr, operation)
+  )
+}
+
+pragma[inline]
+predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string operation) {
+  exists(AddressOperand addr, int delta |
+    bounded2(addr.getDef(), sink.asInstruction(), delta) and
+    isInvalidPointerDerefSinkImpl(delta, i, addr, operation)
   )
 }
 
@@ -90,7 +113,7 @@ module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
   }
 
   pragma[inline]
-  predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
+  predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink1(sink, _, _) }
 }
 
 module PointerArithmeticToDerefFlow = DataFlow::Global<PointerArithmeticToDerefConfig>;
@@ -100,7 +123,7 @@ from
   PointerArithmeticToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
 where
   PointerArithmeticToDerefFlow::flowPath(source, sink) and
-  isInvalidPointerDerefSink(sink.getNode(), deref, operation) and
+  isInvalidPointerDerefSink2(sink.getNode(), deref, operation) and
   isConstantSizeOverflowSource(f, source.getNode().asInstruction(), delta)
 select source, source, sink,
   "This pointer arithmetic may have an off-by-" + (delta + 1) +