@@ -83,6 +83,17 @@ predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
83
83
/**
84
84
* A product-flow configuration for flow from an (allocation, size) pair to a
85
85
* pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
86
+ *
87
+ * The goal of this query is to find patterns such as:
88
+ * ```cpp
89
+ * char* p = (char*)malloc(size);
90
+ * char* end = p + size;
91
+ * use(*end);
92
+ * ```
93
+ *
94
+ * We do this by splitting the task up into two configurations:
95
+ * 1. `AllocToInvalidPointerConf` find flow from `malloc(size)` to `p + size`, and
96
+ * 2. `InvalidPointerToDerefConf` finds flow from `p + size` to `*end`.
86
97
*/
87
98
class AllocToInvalidPointerConf extends ProductFlow:: Configuration {
88
99
AllocToInvalidPointerConf ( ) { this = "AllocToInvalidPointerConf" }
@@ -115,8 +126,18 @@ predicate pointerAddInstructionHasOperands(
115
126
}
116
127
117
128
/**
118
- * Holds if `pai` is non-strictly upper bounded by `b + delta` and `sink1` is the
119
- * non-constant operand of the pointer-arithmetic operation.
129
+ * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
130
+ * left operand of the pointer-arithmetic operation.
131
+ *
132
+ * For example in,
133
+ * ```cpp
134
+ * char* end = p + (size + 1);
135
+ * ```
136
+ * We will have:
137
+ * - `pai` is `p + (size + 1)`,
138
+ * - `sink1` is `p`
139
+ * - `sink2` is `size`
140
+ * - `delta` is `1`.
120
141
*/
121
142
pragma [ nomagic]
122
143
predicate pointerAddInstructionHasBounds (
@@ -130,7 +151,9 @@ predicate pointerAddInstructionHasBounds(
130
151
131
152
/**
132
153
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
133
- * non-constant operand of the pointer-arithmetic operation.
154
+ * left operand of the pointer-arithmetic operation.
155
+ *
156
+ * See `pointerAddInstructionHasBounds` for an example.
134
157
*/
135
158
predicate isSinkImpl (
136
159
PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
@@ -169,6 +192,14 @@ class InvalidPointerToDerefConf extends DataFlow3::Configuration {
169
192
override predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
170
193
}
171
194
195
+ /**
196
+ * Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
197
+ * pointer-value that is non-strictly upper bounded by `pai + delta`.
198
+ *
199
+ * For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
200
+ * as `(p + size) + 1` and `source` is the node representing `(p + size) + 1`. In this
201
+ * case `delta` is 1.
202
+ */
172
203
predicate invalidPointerToDerefSource (
173
204
PointerArithmeticInstruction pai , DataFlow:: Node source , int delta
174
205
) {
0 commit comments