C++: Clean up the ProductFlow FlowStates

Author: jketema

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

@@ -20,6 +20,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 import StringSizeFlow::PathGraph1
+import codeql.util.Unit
 
 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -46,7 +47,7 @@ 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) {
+predicate hasSize(AllocationExpr alloc, DataFlow::Node n, int 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)`.
@@ -55,7 +56,7 @@ predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
     bounded(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
       any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
     n.asConvertedExpr() = va.getFullyConverted() and
-    state = delta.toString()
+    state = delta
   )
 }
 
@@ -78,9 +79,9 @@ predicate isSinkPairImpl(
 }
 
 module StringSizeConfig implements ProductFlow::StateConfigSig {
-  class FlowState1 = string;
+  class FlowState1 = Unit;
 
-  class FlowState2 = string;
+  class FlowState2 = int;
 
   predicate isSourcePair(
     DataFlow::Node bufSource, FlowState1 state1, DataFlow::Node sizeSource, FlowState2 state2
@@ -91,18 +92,18 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
     // ```
     // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
     // to the size of the allocation. This state is then checked in `isSinkPair`.
-    state1 instanceof DataFlow::FlowStateEmpty and
+    exists(state1) and
     hasSize(bufSource.asConvertedExpr(), sizeSource, state2)
   }
 
   predicate isSinkPair(
     DataFlow::Node bufSink, FlowState1 state1, DataFlow::Node sizeSink, FlowState2 state2
   ) {
-    state1 instanceof DataFlow::FlowStateEmpty and
-    state2 = [-32 .. 32].toString() and // An arbitrary bound because we need to bound `state2`
+    exists(state1) and
+    state2 = [-32 .. 32] and // An arbitrary bound because we need to bound `state2`
     exists(int delta |
       isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
-      delta > state2.toInt()
+      delta > state2
     )
   }
 
@@ -111,18 +112,18 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
   predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
 
   predicate isAdditionalFlowStep1(
-    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2
+    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
   ) {
     none()
   }
 
   predicate isAdditionalFlowStep2(
-    DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState2 state2
+    DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
   ) {
     exists(AddInstruction add, Operand op, int delta, int s1, int s2 |
       s1 = [-32 .. 32] and // An arbitrary bound because we need to bound `state`
-      state1 = s1.toString() and
-      state2 = s2.toString() and
+      state1 = s1 and
+      state2 = s2 and
       add.hasOperands(node1.asOperand(), op) and
       semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
       node2.asInstruction() = add and
@@ -139,7 +140,7 @@ from
   CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element
 where
   StringSizeFlow::hasFlowPath(source1, source2, sink1, sink2) and
-  sinkState = sink2.getState().toInt() and
+  sinkState = sink2.getState() and
   isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
   overflow > 0 and
   sourceNode = source1.getNode() and

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

@@ -20,6 +20,7 @@ import experimental.semmle.code.cpp.dataflow.ProductFlow
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 import semmle.code.cpp.ir.IR
+import codeql.util.Unit
 
 pragma[nomagic]
 Instruction getABoundIn(SemBound b, IRFunction func) {
@@ -51,14 +52,14 @@ predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b,
  * 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) {
+private predicate hasSizeImpl(Expr e, DataFlow::Node n, int 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"
+    state = 0
   )
   or
   // If the size is a choice between two expressions we allow both to be nodes representing the size.
@@ -68,13 +69,13 @@ private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
   // remember the constant in the state.
   exists(Expr const, Expr nonconst |
     e.(AddExpr).hasOperands(const, nonconst) and
-    state = const.getValue() and
+    state = const.getValue().toInt() and
     hasSizeImpl(nonconst, n, _)
   )
   or
   exists(Expr const, Expr nonconst |
     e.(SubExpr).hasOperands(const, nonconst) and
-    state = "-" + const.getValue() and
+    state = -const.getValue().toInt() and
     hasSizeImpl(nonconst, n, _)
   )
 }
@@ -83,7 +84,7 @@ private predicate hasSizeImpl(Expr e, DataFlow::Node n, string state) {
  * Holds if `(n, state)` pair represents the source of flow for the size
  * expression associated with `alloc`.
  */
-predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, string state) {
+predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
   hasSizeImpl(alloc.getSizeExpr(), n, state)
 }
 
@@ -108,9 +109,9 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, string state)
  * is non-strictly upper-bounded by `end` (which in this case is `*p`).
  */
 module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
-  class FlowState1 = string;
+  class FlowState1 = Unit;
 
-  class FlowState2 = string;
+  class FlowState2 = int;
 
   predicate isSourcePair(
     DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
@@ -121,19 +122,19 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
     // ```
     // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
     // to the size of the allocation. This state is then checked in `isSinkPair`.
-    state1 = "" and
+    exists(state1) and
     hasSize(source1.asConvertedExpr(), source2, state2)
   }
 
   predicate isSinkPair(
     DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
   ) {
-    state1 = "" and
+    exists(state1) and
     // We check that the delta computed by the range analysis matches the
     // state value that we set in `isSourcePair`.
     exists(int delta |
       isSinkImpl(_, sink1, sink2, delta) and
-      state2 = delta.toString()
+      state2 = delta
     )
   }