@@ -118,11 +118,11 @@ private module SizeBarrier {
118118 predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
119119 }
120120
121- private import DataFlow:: Global< SizeBarrierConfig >
121+ module SizeBarrierFlow = DataFlow:: Global< SizeBarrierConfig > ;
122122
123123 private int getASizeAddend ( DataFlow:: Node node ) {
124124 exists ( DataFlow:: Node source |
125- flow ( source , node ) and
125+ SizeBarrierFlow :: flow ( source , node ) and
126126 hasSize ( _, source , result )
127127 )
128128 }
@@ -133,7 +133,7 @@ private module SizeBarrier {
133133 private predicate operandGuardChecks (
134134 IRGuardCondition g , Operand left , DataFlow:: Node right , int k , boolean edge
135135 ) {
136- flowTo ( right ) and
136+ SizeBarrierFlow :: flowTo ( right ) and
137137 SizeBarrierConfig:: isSink ( DataFlow:: operandNode ( left ) , right , g , k , edge )
138138 }
139139
@@ -174,27 +174,15 @@ private module SizeBarrier {
174174 )
175175 }
176176
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-
189177 /**
190178 * Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
191179 * the value of the node is upper-bounded by size of some allocation.
192180 */
193181 DataFlow:: Node getABarrierNode ( int state ) {
194182 exists ( DataFlow:: Node source , int delta , int k |
195- ValidForStateFlow :: flow ( source , result ) and
183+ SizeBarrierFlow :: flow ( source , result ) and
196184 hasSize ( _, source , state ) and
197- ValidForStateConfig :: isSink ( result , delta , k ) and
185+ result . asInstruction ( ) = SizeBarrier :: getABarrierInstruction0 ( delta , k ) and
198186 state > k + delta
199187 // so now we have:
200188 // result <= "size of allocation" + delta + k
0 commit comments