@@ -42,59 +42,57 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
42
42
* ```
43
43
* In this case, the sink pair identified by the product flow library (without any additional barriers)
44
44
* would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
45
- * instruction `pai` such that:
46
- * 1. The left-hand of `pai` flows from the allocation , and
47
- * 2. The right-hand of `pai` is non-strictly upper bounded by ` n` ( where `n` is the `n` in `p[n]`)
45
+ * instruction `pai = a + b ` such that:
46
+ * 1. the allocation flows to `a` , and
47
+ * 2. `b <= n` where `n` is the `n` in `p[n]`
48
48
* but because there's a strict comparison that compares `n` against the size of the allocation this
49
49
* snippet is fine.
50
50
*/
51
- module Barrier2 {
52
- private class FlowState2 = int ;
53
-
54
- private module BarrierConfig2 implements DataFlow:: ConfigSig {
51
+ module SizeBarrier {
52
+ private module SizeBarrierConfig implements DataFlow:: ConfigSig {
55
53
predicate isSource ( DataFlow:: Node source ) {
56
54
// The sources is the same as in the sources for the second
57
55
// projection in the `AllocToInvalidPointerConfig` module.
58
56
hasSize ( _, source , _)
59
57
}
60
58
61
59
additional predicate isSink (
62
- DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , FlowState2 state ,
63
- boolean testIsTrue
60
+ DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , int k , boolean testIsTrue
64
61
) {
65
- // The sink is any "large" side of a relational comparison.
66
- g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , state , true , testIsTrue )
62
+ // The sink is any "large" side of a relational comparison. i.e., the `right` expression
63
+ // in a guard such as `left < right + k`.
64
+ g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , k , true , testIsTrue )
67
65
}
68
66
69
67
predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
70
68
}
71
69
72
- private import DataFlow:: Global< BarrierConfig2 >
70
+ private import DataFlow:: Global< SizeBarrierConfig >
73
71
74
- private FlowState2 getAFlowStateForNode ( DataFlow:: Node node ) {
72
+ private int getAFlowStateForNode ( DataFlow:: Node node ) {
75
73
exists ( DataFlow:: Node source |
76
74
flow ( source , node ) and
77
75
hasSize ( _, source , result )
78
76
)
79
77
}
80
78
81
79
private predicate operandGuardChecks (
82
- IRGuardCondition g , Operand left , Operand right , FlowState2 state , boolean edge
80
+ IRGuardCondition g , Operand left , Operand right , int state , boolean edge
83
81
) {
84
- exists ( DataFlow:: Node nLeft , DataFlow:: Node nRight , FlowState2 state0 |
82
+ exists ( DataFlow:: Node nLeft , DataFlow:: Node nRight , int k |
85
83
nRight .asOperand ( ) = right and
86
84
nLeft .asOperand ( ) = left and
87
- BarrierConfig2 :: isSink ( nLeft , nRight , g , state0 , edge ) and
85
+ SizeBarrierConfig :: isSink ( nLeft , nRight , g , k , edge ) and
88
86
state = getAFlowStateForNode ( nRight ) and
89
- state0 <= state
87
+ k <= state
90
88
)
91
89
}
92
90
93
91
/**
94
92
* Gets an instruction that is guarded by a guard condition which ensures that
95
93
* the value of the instruction is upper-bounded by size of some allocation.
96
94
*/
97
- Instruction getABarrierInstruction ( FlowState2 state ) {
95
+ Instruction getABarrierInstruction ( int state ) {
98
96
exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge |
99
97
use = value .getAUse ( ) and
100
98
operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) , _,
@@ -108,17 +106,15 @@ module Barrier2 {
108
106
* Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
109
107
* the value of the node is upper-bounded by size of some allocation.
110
108
*/
111
- DataFlow:: Node getABarrierNode ( FlowState2 state ) {
109
+ DataFlow:: Node getABarrierNode ( int state ) {
112
110
result .asOperand ( ) = getABarrierInstruction ( state ) .getAUse ( )
113
111
}
114
112
115
113
/**
116
114
* Gets the block of a node that is guarded (see `getABarrierInstruction` or
117
115
* `getABarrierNode` for the definition of what it means to be guarded).
118
116
*/
119
- IRBlock getABarrierBlock ( FlowState2 state ) {
120
- result .getAnInstruction ( ) = getABarrierInstruction ( state )
121
- }
117
+ IRBlock getABarrierBlock ( int state ) { result .getAnInstruction ( ) = getABarrierInstruction ( state ) }
122
118
}
123
119
124
120
private module InterestingPointerAddInstruction {
@@ -151,8 +147,8 @@ private module InterestingPointerAddInstruction {
151
147
}
152
148
153
149
/**
154
- * A product-flow configuration for flow from an (allocation, size) pair to a
155
- * pointer-arithmetic operation that is non-strictly upper-bounded by ` allocation + size`.
150
+ * A product-flow configuration for flow from an ` (allocation, size)` pair to a
151
+ * pointer-arithmetic operation `pai` such that `pai <= allocation + size`.
156
152
*
157
153
* The goal of this query is to find patterns such as:
158
154
* ```cpp
@@ -176,29 +172,29 @@ private module Config implements ProductFlow::StateConfigSig {
176
172
class FlowState2 = int ;
177
173
178
174
predicate isSourcePair (
179
- DataFlow:: Node source1 , FlowState1 state1 , DataFlow:: Node source2 , FlowState2 state2
175
+ DataFlow:: Node allocSource , FlowState1 unit , DataFlow:: Node sizeSource , FlowState2 sizeAddend
180
176
) {
181
177
// In the case of an allocation like
182
178
// ```cpp
183
179
// malloc(size + 1);
184
180
// ```
185
181
// we use `state2` to remember that there was an offset (in this case an offset of `1`) added
186
182
// to the size of the allocation. This state is then checked in `isSinkPair`.
187
- exists ( state1 ) and
188
- hasSize ( source1 .asConvertedExpr ( ) , source2 , state2 )
183
+ exists ( unit ) and
184
+ hasSize ( allocSource .asConvertedExpr ( ) , sizeSource , sizeAddend )
189
185
}
190
186
191
187
predicate isSinkPair (
192
- DataFlow:: Node sink1 , FlowState1 state1 , DataFlow:: Node sink2 , FlowState2 state2
188
+ DataFlow:: Node allocSink , FlowState1 unit , DataFlow:: Node sizeSink , FlowState2 sizeAddend
193
189
) {
194
- exists ( state1 ) and
190
+ exists ( unit ) and
195
191
// We check that the delta computed by the range analysis matches the
196
192
// state value that we set in `isSourcePair`.
197
- pointerAddInstructionHasBounds0 ( _, sink1 , sink2 , state2 )
193
+ pointerAddInstructionHasBounds0 ( _, allocSink , sizeSink , sizeAddend )
198
194
}
199
195
200
196
predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) {
201
- node = Barrier2 :: getABarrierNode ( state )
197
+ node = SizeBarrier :: getABarrierNode ( state )
202
198
}
203
199
204
200
predicate isBarrierIn1 ( DataFlow:: Node node ) { isSourcePair ( node , _, _, _) }
@@ -211,7 +207,7 @@ private module Config implements ProductFlow::StateConfigSig {
211
207
private module AllocToInvalidPointerFlow = ProductFlow:: GlobalWithState< Config > ;
212
208
213
209
/**
214
- * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1 ` is the
210
+ * Holds if `pai` is non-strictly upper bounded by `sizeSink + delta` and `allocSink ` is the
215
211
* left operand of the pointer-arithmetic operation.
216
212
*
217
213
* For example in,
@@ -220,37 +216,37 @@ private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<Config>;
220
216
* ```
221
217
* We will have:
222
218
* - `pai` is `p + (size + 1)`,
223
- * - `sink1 ` is `p`
224
- * - `sink2 ` is `size`
219
+ * - `allocSink ` is `p`
220
+ * - `sizeSink ` is `size`
225
221
* - `delta` is `1`.
226
222
*/
227
223
pragma [ nomagic]
228
224
private predicate pointerAddInstructionHasBounds0 (
229
- PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
225
+ PointerAddInstruction pai , DataFlow:: Node allocSink , DataFlow:: Node sizeSink , int delta
230
226
) {
231
227
InterestingPointerAddInstruction:: isInteresting ( pragma [ only_bind_into ] ( pai ) ) and
232
- exists ( Instruction right , Instruction instr2 |
228
+ exists ( Instruction right , Instruction sizeInstr |
233
229
pai .getRight ( ) = right and
234
- pai .getLeft ( ) = sink1 .asInstruction ( ) and
235
- instr2 = sink2 .asInstruction ( ) and
236
- // pai.getRight() <= sink2 + delta
237
- bounded1 ( right , instr2 , delta ) and
238
- not right = Barrier2 :: getABarrierInstruction ( delta ) and
239
- not instr2 = Barrier2 :: getABarrierInstruction ( delta )
230
+ pai .getLeft ( ) = allocSink .asInstruction ( ) and
231
+ sizeInstr = sizeSink .asInstruction ( ) and
232
+ // pai.getRight() <= sizeSink + delta
233
+ bounded1 ( right , sizeInstr , delta ) and
234
+ not right = SizeBarrier :: getABarrierInstruction ( delta ) and
235
+ not sizeInstr = SizeBarrier :: getABarrierInstruction ( delta )
240
236
)
241
237
}
242
238
243
239
/**
244
- * Holds if `allocation` flows to `sink1 ` and `sink1 ` represents the left-hand
245
- * side of the pointer-arithmetic instruction `pai`, and the right-hand side of `pai`
246
- * is non-strictly upper bounded by the size of `alllocation` + ` delta`.
240
+ * Holds if `allocation` flows to `allocSink ` and `allocSink ` represents the left operand
241
+ * of the pointer-arithmetic instruction `pai = a + b` (i.e., `allocSink = a`), and
242
+ * `b <= allocation + delta`.
247
243
*/
248
244
pragma [ nomagic]
249
245
predicate pointerAddInstructionHasBounds (
250
- DataFlow:: Node allocation , PointerAddInstruction pai , DataFlow:: Node sink1 , int delta
246
+ DataFlow:: Node allocation , PointerAddInstruction pai , DataFlow:: Node allocSink , int delta
251
247
) {
252
- exists ( DataFlow:: Node sink2 |
253
- AllocToInvalidPointerFlow:: flow ( allocation , _, sink1 , sink2 ) and
254
- pointerAddInstructionHasBounds0 ( pai , sink1 , sink2 , delta )
248
+ exists ( DataFlow:: Node sizeSink |
249
+ AllocToInvalidPointerFlow:: flow ( allocation , _, allocSink , sizeSink ) and
250
+ pointerAddInstructionHasBounds0 ( pai , allocSink , sizeSink , delta )
255
251
)
256
252
}
0 commit comments