@@ -118,11 +118,11 @@ private module SizeBarrier {
118
118
predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
119
119
}
120
120
121
- private import DataFlow:: Global< SizeBarrierConfig >
121
+ module SizeBarrierFlow = DataFlow:: Global< SizeBarrierConfig > ;
122
122
123
123
private int getASizeAddend ( DataFlow:: Node node ) {
124
124
exists ( DataFlow:: Node source |
125
- flow ( source , node ) and
125
+ SizeBarrierFlow :: flow ( source , node ) and
126
126
hasSize ( _, source , result )
127
127
)
128
128
}
@@ -133,7 +133,7 @@ private module SizeBarrier {
133
133
private predicate operandGuardChecks (
134
134
IRGuardCondition g , Operand left , DataFlow:: Node right , int k , boolean edge
135
135
) {
136
- flowTo ( right ) and
136
+ SizeBarrierFlow :: flowTo ( right ) and
137
137
SizeBarrierConfig:: isSink ( DataFlow:: operandNode ( left ) , right , g , k , edge )
138
138
}
139
139
@@ -174,27 +174,15 @@ private module SizeBarrier {
174
174
)
175
175
}
176
176
177
- private module ValidForStateConfig implements DataFlow:: ConfigSig {
178
- predicate isSource ( DataFlow:: Node source ) { hasSize ( _, source , _) }
179
-
180
- predicate isSink ( DataFlow:: Node sink ) { isSink ( sink , _, _) }
181
-
182
- additional predicate isSink ( DataFlow:: Node sink , int delta , int k ) {
183
- sink .asOperand ( ) = SizeBarrier:: getABarrierInstruction0 ( delta , k ) .getAUse ( )
184
- }
185
- }
186
-
187
- private module ValidForStateFlow = DataFlow:: Global< ValidForStateConfig > ;
188
-
189
177
/**
190
178
* Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
191
179
* the value of the node is upper-bounded by size of some allocation.
192
180
*/
193
181
DataFlow:: Node getABarrierNode ( int state ) {
194
182
exists ( DataFlow:: Node source , int delta , int k |
195
- ValidForStateFlow :: flow ( source , result ) and
183
+ SizeBarrierFlow :: flow ( source , result ) and
196
184
hasSize ( _, source , state ) and
197
- ValidForStateConfig :: isSink ( result , delta , k ) and
185
+ result . asInstruction ( ) = SizeBarrier :: getABarrierInstruction0 ( delta , k ) and
198
186
state > k + delta
199
187
// so now we have:
200
188
// result <= "size of allocation" + delta + k
0 commit comments