C++: Speed up analysis on 'Samate' by avoiding the 'Variable' column in the dataflow stages of the query.

Author: MathiasVP

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

@@ -78,28 +78,39 @@ predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string
   )
 }
 
+predicate arrayTypeCand(ArrayType arrayType) { any(Variable v).getUnspecifiedType() = arrayType }
+
 pragma[nomagic]
 predicate arrayTypeHasSizes(ArrayType arr, int baseTypeSize, int arraySize) {
+  arrayTypeCand(arr) and
   arr.getBaseType().getSize() = baseTypeSize and
   arr.getArraySize() = arraySize
 }
 
-predicate pointerArithOverflow0(
-  PointerArithmeticInstruction pai, Variable v, int size, int bound, int delta
-) {
-  not v.getNamespace() instanceof StdNamespace and
-  arrayTypeHasSizes(v.getUnspecifiedType(), pai.getElementSize(), size) and
-  semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), bound, true, _) and
+bindingset[pai]
+pragma[inline_late]
+predicate constantUpperBounded(PointerArithmeticInstruction pai, int delta) {
+  semBounded(getSemanticExpr(pai.getRight()), any(SemZeroBound b), delta, true, _)
+}
+
+bindingset[pai, size]
+predicate pointerArithOverflow0Impl(PointerArithmeticInstruction pai, int size, int bound, int delta) {
+  constantUpperBounded(pai, bound) and
   delta = bound - size and
   delta >= 0 and
   size != 0 and
   size != 1
 }
 
+predicate pointerArithOverflow0(PointerArithmeticInstruction pai, int delta) {
+  exists(int size, int bound |
+    arrayTypeHasSizes(_, pai.getElementSize(), size) and
+    pointerArithOverflow0Impl(pai, size, bound, delta)
+  )
+}
+
 module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
-  predicate isSource(DataFlow::Node source) {
-    pointerArithOverflow0(source.asInstruction(), _, _, _, _)
-  }
+  predicate isSource(DataFlow::Node source) { pointerArithOverflow0(source.asInstruction(), _) }
 
   predicate isBarrierIn(DataFlow::Node node) { isSource(node) }
 
@@ -110,30 +121,38 @@ module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
 
 module PointerArithmeticToDerefFlow = DataFlow::Global<PointerArithmeticToDerefConfig>;
 
-predicate pointerArithOverflow(
-  PointerArithmeticInstruction pai, Variable v, int size, int bound, int delta
-) {
-  pointerArithOverflow0(pai, v, size, bound, delta) and
+predicate pointerArithOverflow(PointerArithmeticInstruction pai, int delta) {
+  pointerArithOverflow0(pai, delta) and
   PointerArithmeticToDerefFlow::flow(DataFlow::instructionNode(pai), _)
 }
 
+bindingset[v]
+predicate finalPointerArithOverflow(Variable v, PointerArithmeticInstruction pai, int delta) {
+  exists(int size |
+    arrayTypeHasSizes(pragma[only_bind_out](v.getUnspecifiedType()), pai.getElementSize(), size) and
+    pointerArithOverflow0Impl(pai, size, _, delta)
+  )
+}
+
+predicate isSourceImpl(DataFlow::Node source, Variable v) {
+  (
+    source.asInstruction().(FieldAddressInstruction).getField() = v
+    or
+    source.asInstruction().(VariableAddressInstruction).getAstVariable() = v
+  ) and
+  exists(v.getUnspecifiedType().(ArrayType).getArraySize())
+}
+
 module ArrayAddressToDerefConfig implements DataFlow::StateConfigSig {
   newtype FlowState =
-    additional TArray(Variable v) { pointerArithOverflow(_, v, _, _, _) } or
+    additional TArray() or
     additional TOverflowArithmetic(PointerArithmeticInstruction pai) {
-      pointerArithOverflow(pai, _, _, _, _)
+      pointerArithOverflow(pai, _)
     }
 
   predicate isSource(DataFlow::Node source, FlowState state) {
-    exists(Variable v |
-      (
-        source.asInstruction().(FieldAddressInstruction).getField() = v
-        or
-        source.asInstruction().(VariableAddressInstruction).getAstVariable() = v
-      ) and
-      exists(v.getUnspecifiedType().(ArrayType).getArraySize()) and
-      state = TArray(v)
-    )
+    isSourceImpl(source, _) and
+    state = TArray()
   }
 
   predicate isSink(DataFlow::Node sink, FlowState state) {
@@ -152,12 +171,12 @@ module ArrayAddressToDerefConfig implements DataFlow::StateConfigSig {
   predicate isAdditionalFlowStep(
     DataFlow::Node node1, FlowState state1, DataFlow::Node node2, FlowState state2
   ) {
-    exists(PointerArithmeticInstruction pai, Variable v |
-      state1 = TArray(v) and
+    exists(PointerArithmeticInstruction pai |
+      state1 = TArray() and
       state2 = TOverflowArithmetic(pai) and
       pai.getLeft() = node1.asInstruction() and
       node2.asInstruction() = pai and
-      pointerArithOverflow(pai, v, _, _, _)
+      pointerArithOverflow(pai, _)
     )
   }
 }
@@ -168,11 +187,11 @@ from
   Variable v, ArrayAddressToDerefFlow::PathNode source, PointerArithmeticInstruction pai,
   ArrayAddressToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
 where
-  ArrayAddressToDerefFlow::flowPath(source, sink) and
+  ArrayAddressToDerefFlow::flowPath(pragma[only_bind_into](source), pragma[only_bind_into](sink)) and
   isInvalidPointerDerefSink2(sink.getNode(), deref, operation) and
-  source.getState() = ArrayAddressToDerefConfig::TArray(v) and
-  sink.getState() = ArrayAddressToDerefConfig::TOverflowArithmetic(pai) and
-  pointerArithOverflow(pai, v, _, _, delta)
+  pragma[only_bind_out](sink.getState()) = ArrayAddressToDerefConfig::TOverflowArithmetic(pai) and
+  isSourceImpl(source.getNode(), v) and
+  finalPointerArithOverflow(v, pai, delta)
 select pai, source, sink,
   "This pointer arithmetic may have an off-by-" + (delta + 1) +
     " error allowing it to overrun $@ at this $@.", v, v.getName(), deref, operation

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected

@@ -11,6 +11,8 @@ edges
 | test.cpp:77:32:77:34 | buf | test.cpp:77:26:77:44 | & ... |
 | test.cpp:79:27:79:34 | buf | test.cpp:70:33:70:33 | p |
 | test.cpp:79:32:79:34 | buf | test.cpp:79:27:79:34 | buf |
+| test.cpp:85:34:85:36 | buf | test.cpp:87:5:87:31 | access to array |
+| test.cpp:85:34:85:36 | buf | test.cpp:88:5:88:27 | access to array |
 | test.cpp:128:9:128:11 | arr | test.cpp:128:9:128:14 | access to array |
 | test.cpp:134:25:134:27 | arr | test.cpp:136:9:136:16 | ... += ... |
 | test.cpp:136:9:136:16 | ... += ... | test.cpp:138:13:138:15 | arr |
@@ -38,6 +40,9 @@ nodes
 | test.cpp:77:32:77:34 | buf | semmle.label | buf |
 | test.cpp:79:27:79:34 | buf | semmle.label | buf |
 | test.cpp:79:32:79:34 | buf | semmle.label | buf |
+| test.cpp:85:34:85:36 | buf | semmle.label | buf |
+| test.cpp:87:5:87:31 | access to array | semmle.label | access to array |
+| test.cpp:88:5:88:27 | access to array | semmle.label | access to array |
 | test.cpp:128:9:128:11 | arr | semmle.label | arr |
 | test.cpp:128:9:128:14 | access to array | semmle.label | access to array |
 | test.cpp:134:25:134:27 | arr | semmle.label | arr |