@@ -134,21 +134,23 @@ private module SizeBarrier {
134
134
* Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
135
135
*/
136
136
additional predicate isSink (
137
- DataFlow :: Node small , DataFlow :: Node large , IRGuardCondition g , int k , boolean testIsTrue
137
+ ValueNumber small , ValueNumber large , IRGuardCondition g , int k , boolean testIsTrue
138
138
) {
139
139
// The sink is any "large" side of a relational comparison. i.e., the `large` expression
140
140
// in a guard such as `small <= large + k`.
141
- g .comparesLt ( small . asOperand ( ) , large . asOperand ( ) , k + 1 , true , testIsTrue )
141
+ g .comparesLt ( small , large , k + 1 , true , testIsTrue )
142
142
}
143
143
144
- predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
144
+ predicate isSink ( DataFlow:: Node sink ) {
145
+ isSink ( _, valueNumberOfOperand ( sink .asOperand ( ) ) , _, _, _)
146
+ }
145
147
}
146
148
147
149
module SizeBarrierFlow = DataFlow:: Global< SizeBarrierConfig > ;
148
150
149
- private int getASizeAddend ( DataFlow :: Node node ) {
151
+ private int getASizeAddend ( ValueNumber node ) {
150
152
exists ( DataFlow:: Node source |
151
- SizeBarrierFlow:: flow ( source , node ) and
153
+ SizeBarrierFlow:: flow ( source , DataFlow :: operandNode ( node . getAUse ( ) ) ) and
152
154
hasSize ( _, source , result )
153
155
)
154
156
}
@@ -157,10 +159,10 @@ private module SizeBarrier {
157
159
* Holds if `small <= large + k` holds if `g` evaluates to `edge`.
158
160
*/
159
161
private predicate operandGuardChecks (
160
- IRGuardCondition g , Operand small , DataFlow :: Node large , int k , boolean edge
162
+ IRGuardCondition g , ValueNumber small , ValueNumber large , int k , boolean edge
161
163
) {
162
- SizeBarrierFlow:: flowTo ( large ) and
163
- SizeBarrierConfig:: isSink ( DataFlow :: operandNode ( small ) , large , g , k , edge )
164
+ SizeBarrierFlow:: flowTo ( DataFlow :: operandNode ( large . getAUse ( ) ) ) and
165
+ SizeBarrierConfig:: isSink ( small , large , g , k , edge )
164
166
}
165
167
166
168
/**
@@ -170,15 +172,15 @@ private module SizeBarrier {
170
172
*/
171
173
Instruction getABarrierInstruction0 ( int delta , int k ) {
172
174
exists (
173
- IRGuardCondition g , ValueNumber value , Operand small , boolean edge , DataFlow :: Node large
175
+ IRGuardCondition g , ValueNumber value , ValueNumber small , boolean edge , ValueNumber large
174
176
|
175
177
// We know:
176
178
// 1. result <= value + delta (by `bounded`)
177
179
// 2. value <= large + k (by `operandGuardChecks`).
178
180
// So:
179
181
// result <= value + delta (by 1.)
180
182
// <= large + k + delta (by 2.)
181
- small = value . getAUse ( ) and
183
+ small = value and
182
184
operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( small ) , large ,
183
185
pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( edge ) ) and
184
186
bounded ( result , value .getAnInstruction ( ) , delta ) and
0 commit comments