@@ -137,6 +137,17 @@ class GuardCondition extends Expr {
137
137
*/
138
138
cached
139
139
predicate ensuresEq ( Expr left , Expr right , int k , BasicBlock block , boolean areEqual ) { none ( ) }
140
+
141
+ /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
142
+ cached
143
+ predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) { none ( ) }
144
+
145
+ /**
146
+ * Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
147
+ * If `areEqual = false` then this implies `e != k`.
148
+ */
149
+ cached
150
+ predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) { none ( ) }
140
151
}
141
152
142
153
/**
@@ -184,6 +195,20 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
184
195
this .comparesEq ( left , right , k , areEqual , testIsTrue ) and this .controls ( block , testIsTrue )
185
196
)
186
197
}
198
+
199
+ override predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) {
200
+ exists ( boolean partIsTrue , GuardCondition part |
201
+ this .( BinaryLogicalOperation ) .impliesValue ( part , partIsTrue , testIsTrue )
202
+ |
203
+ part .comparesEq ( e , k , areEqual , partIsTrue )
204
+ )
205
+ }
206
+
207
+ override predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) {
208
+ exists ( boolean testIsTrue |
209
+ this .comparesEq ( e , k , areEqual , testIsTrue ) and this .controls ( block , testIsTrue )
210
+ )
211
+ }
187
212
}
188
213
189
214
/**
@@ -245,6 +270,21 @@ private class GuardConditionFromIR extends GuardCondition {
245
270
)
246
271
}
247
272
273
+ override predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) {
274
+ exists ( Instruction i |
275
+ i .getUnconvertedResultExpression ( ) = e and
276
+ ir .comparesEq ( i .getAUse ( ) , k , areEqual , testIsTrue )
277
+ )
278
+ }
279
+
280
+ override predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) {
281
+ exists ( Instruction i , boolean testIsTrue |
282
+ i .getUnconvertedResultExpression ( ) = e and
283
+ ir .comparesEq ( i .getAUse ( ) , k , areEqual , testIsTrue ) and
284
+ this .controls ( block , testIsTrue )
285
+ )
286
+ }
287
+
248
288
/**
249
289
* Holds if this condition controls `block`, meaning that `block` is only
250
290
* entered if the value of this condition is `v`. This helper
0 commit comments