@@ -19,6 +19,8 @@ import cpp
19
19
import semmle.code.cpp.ir.dataflow.internal.ProductFlow
20
20
import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
21
21
import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
22
+ import semmle.code.cpp.ir.ValueNumbering
23
+ import semmle.code.cpp.controlflow.IRGuards
22
24
import semmle.code.cpp.ir.IR
23
25
import codeql.util.Unit
24
26
@@ -67,6 +69,84 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
67
69
)
68
70
}
69
71
72
+ /**
73
+ * A module that encapsulates a barrier guard to remove false positives from flow like:
74
+ * ```cpp
75
+ * char *p = new char[size];
76
+ * // ...
77
+ * unsigned n = size;
78
+ * // ...
79
+ * if(n < size) {
80
+ * use(*p[n]);
81
+ * }
82
+ * ```
83
+ * In this case, the sink pair identified by the product flow library (without any additional barriers)
84
+ * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
85
+ * instruction `pai` such that:
86
+ * 1. The left-hand of `pai` flows from the allocation, and
87
+ * 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
88
+ * but because there's a strict comparison that compares `n` against the size of the allocation this
89
+ * snippet is fine.
90
+ */
91
+ module Barrier2 {
92
+ private class FlowState2 = AllocToInvalidPointerConfig:: FlowState2 ;
93
+
94
+ private module BarrierConfig2 implements DataFlow:: ConfigSig {
95
+ predicate isSource ( DataFlow:: Node source ) {
96
+ // The sources is the same as in the sources for the second
97
+ // projection in the `AllocToInvalidPointerConfig` module.
98
+ hasSize ( _, source , _)
99
+ }
100
+
101
+ additional predicate isSink (
102
+ DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , FlowState2 state ,
103
+ boolean testIsTrue
104
+ ) {
105
+ // The sink is any "large" side of a relational comparison.
106
+ g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , state , true , testIsTrue )
107
+ }
108
+
109
+ predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
110
+ }
111
+
112
+ private import DataFlow:: Global< BarrierConfig2 >
113
+
114
+ private FlowState2 getAFlowStateForNode ( DataFlow:: Node node ) {
115
+ exists ( DataFlow:: Node source |
116
+ flow ( source , node ) and
117
+ hasSize ( _, source , result )
118
+ )
119
+ }
120
+
121
+ private predicate operandGuardChecks (
122
+ IRGuardCondition g , Operand left , Operand right , FlowState2 state , boolean edge
123
+ ) {
124
+ exists ( DataFlow:: Node nLeft , DataFlow:: Node nRight , FlowState2 state0 |
125
+ nRight .asOperand ( ) = right and
126
+ nLeft .asOperand ( ) = left and
127
+ BarrierConfig2:: isSink ( nLeft , nRight , g , state0 , edge ) and
128
+ state = getAFlowStateForNode ( nRight ) and
129
+ state0 <= state
130
+ )
131
+ }
132
+
133
+ Instruction getABarrierInstruction ( FlowState2 state ) {
134
+ exists ( IRGuardCondition g , Operand right , ValueNumber value , boolean edge |
135
+ operandGuardChecks ( g , value .getAUse ( ) , right , state , edge ) and
136
+ result = value .getAnInstruction ( ) and
137
+ g .controls ( result .getBlock ( ) , edge )
138
+ )
139
+ }
140
+
141
+ DataFlow:: Node getABarrierNode ( FlowState2 state ) {
142
+ result .asOperand ( ) = getABarrierInstruction ( state ) .getAUse ( )
143
+ }
144
+
145
+ IRBlock getABarrierBlock ( FlowState2 state ) {
146
+ result .getAnInstruction ( ) = getABarrierInstruction ( state )
147
+ }
148
+ }
149
+
70
150
/**
71
151
* A product-flow configuration for flow from an (allocation, size) pair to a
72
152
* pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
@@ -111,15 +191,14 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
111
191
exists ( state1 ) and
112
192
// We check that the delta computed by the range analysis matches the
113
193
// state value that we set in `isSourcePair`.
114
- exists ( int delta |
115
- isSinkImpl ( _, sink1 , sink2 , delta ) and
116
- state2 = delta
117
- )
194
+ isSinkImpl ( _, sink1 , sink2 , state2 )
118
195
}
119
196
120
197
predicate isBarrier1 ( DataFlow:: Node node , FlowState1 state ) { none ( ) }
121
198
122
- predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) { none ( ) }
199
+ predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
200
+ node = Barrier2:: getABarrierNode ( state )
201
+ }
123
202
124
203
predicate isBarrierIn1 ( DataFlow:: Node node ) { isSourcePair ( node , _, _, _) }
125
204
@@ -163,7 +242,8 @@ predicate pointerAddInstructionHasBounds(
163
242
exists ( Instruction right |
164
243
pai .getRight ( ) = right and
165
244
pai .getLeft ( ) = sink1 .asInstruction ( ) and
166
- bounded1 ( right , sink2 .asInstruction ( ) , delta )
245
+ bounded1 ( right , sink2 .asInstruction ( ) , delta ) and
246
+ not [ right , sink2 .asInstruction ( ) ] = Barrier2:: getABarrierInstruction ( delta )
167
247
)
168
248
}
169
249
@@ -246,12 +326,21 @@ module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>
246
326
predicate invalidPointerToDerefSource (
247
327
PointerArithmeticInstruction pai , DataFlow:: Node source , int delta
248
328
) {
249
- exists ( AllocToInvalidPointerFlow:: PathNode1 p , DataFlow:: Node sink1 |
250
- pragma [ only_bind_out ] ( p .getNode ( ) ) = sink1 and
251
- AllocToInvalidPointerFlow:: flowPath ( _, _, pragma [ only_bind_into ] ( p ) , _) and
252
- isSinkImpl ( pai , sink1 , _, _) and
329
+ exists (
330
+ AllocToInvalidPointerFlow:: PathNode1 p1 , AllocToInvalidPointerFlow:: PathNode2 p2 ,
331
+ DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta0
332
+ |
333
+ pragma [ only_bind_out ] ( p1 .getNode ( ) ) = sink1 and
334
+ pragma [ only_bind_out ] ( p2 .getNode ( ) ) = sink2 and
335
+ AllocToInvalidPointerFlow:: flowPath ( _, _, pragma [ only_bind_into ] ( p1 ) , pragma [ only_bind_into ] ( p2 ) ) and
336
+ // Note that `delta` is not necessarily equal to `delta0`:
337
+ // `delta0` is the constant offset added to the size of the allocation, and
338
+ // delta is the constant difference between the pointer-arithmetic instruction
339
+ // and the instruction computing the address for which we will search for a dereference.
340
+ isSinkImpl ( pai , sink1 , sink2 , delta0 ) and
253
341
bounded2 ( source .asInstruction ( ) , pai , delta ) and
254
- delta >= 0
342
+ delta >= 0 and
343
+ not source .getBasicBlock ( ) = Barrier2:: getABarrierBlock ( delta0 )
255
344
)
256
345
}
257
346
0 commit comments