@@ -105,14 +105,14 @@ private module SizeBarrier {
105
105
}
106
106
107
107
/**
108
- * Holds if `left <= right + k` holds if `g` evaluates to `testIsTrue`.
108
+ * Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
109
109
*/
110
110
additional predicate isSink (
111
- DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , int k , boolean testIsTrue
111
+ DataFlow:: Node small , DataFlow:: Node large , IRGuardCondition g , int k , boolean testIsTrue
112
112
) {
113
- // The sink is any "large" side of a relational comparison. i.e., the `right ` expression
114
- // in a guard such as `left <= right + k`.
115
- g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , k + 1 , true , testIsTrue )
113
+ // The sink is any "large" side of a relational comparison. i.e., the `large ` expression
114
+ // in a guard such as `small <= large + k`.
115
+ g .comparesLt ( small .asOperand ( ) , large .asOperand ( ) , k + 1 , true , testIsTrue )
116
116
}
117
117
118
118
predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
@@ -128,34 +128,36 @@ private module SizeBarrier {
128
128
}
129
129
130
130
/**
131
- * Holds if `left <= nRight + k` holds if `g` evaluates to `edge`.
131
+ * Holds if `small <= large + k` holds if `g` evaluates to `edge`.
132
132
*/
133
133
private predicate operandGuardChecks (
134
- IRGuardCondition g , Operand left , DataFlow:: Node right , int k , boolean edge
134
+ IRGuardCondition g , Operand small , DataFlow:: Node large , int k , boolean edge
135
135
) {
136
- SizeBarrierFlow:: flowTo ( right ) and
137
- SizeBarrierConfig:: isSink ( DataFlow:: operandNode ( left ) , right , g , k , edge )
136
+ SizeBarrierFlow:: flowTo ( large ) and
137
+ SizeBarrierConfig:: isSink ( DataFlow:: operandNode ( small ) , large , g , k , edge )
138
138
}
139
139
140
140
/**
141
- * Gets an instruction `instr` that is guarded by a check such as `instr <= left + delta` where
142
- * `left <= _ + k` and `left ` is the "small side" of of a relational comparison that checks
143
- * whether `left <= size` where `size` is the size of an allocation.
141
+ * Gets an instruction `instr` that is guarded by a check such as `instr <= small + delta` where
142
+ * `small <= _ + k` and `small ` is the "small side" of of a relational comparison that checks
143
+ * whether `small <= size` where `size` is the size of an allocation.
144
144
*/
145
145
Instruction getABarrierInstruction0 ( int delta , int k ) {
146
- exists ( IRGuardCondition g , ValueNumber value , Operand left , boolean edge , DataFlow:: Node right |
146
+ exists (
147
+ IRGuardCondition g , ValueNumber value , Operand small , boolean edge , DataFlow:: Node large
148
+ |
147
149
// We know:
148
150
// 1. result <= value + delta (by `bounded`)
149
- // 2. value <= right + k (by `operandGuardChecks`).
151
+ // 2. value <= large + k (by `operandGuardChecks`).
150
152
// So:
151
153
// result <= value + delta (by 1.)
152
- // <= right + k + delta (by 2.)
153
- left = value .getAUse ( ) and
154
- operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( left ) , right ,
154
+ // <= large + k + delta (by 2.)
155
+ small = value .getAUse ( ) and
156
+ operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( small ) , large ,
155
157
pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( edge ) ) and
156
158
bounded ( result , value .getAnInstruction ( ) , delta ) and
157
159
g .controls ( result .getBlock ( ) , edge ) and
158
- k < getASizeAddend ( right )
160
+ k < getASizeAddend ( large )
159
161
)
160
162
}
161
163
0 commit comments