@@ -273,87 +273,92 @@ impl<T> HasTop for FlatSet<T> {
273
273
const TOP : Self = Self :: Top ;
274
274
}
275
275
276
+ /// Extend a lattice with a bottom value to represent an unreachable execution.
277
+ ///
278
+ /// The only useful action on an unreachable state is joining it with a reachable one to make it
279
+ /// reachable. All other actions, gen/kill for instance, are no-ops.
276
280
#[ derive( PartialEq , Eq , Debug ) ]
277
- pub enum MaybeUnreachable < T > {
281
+ pub enum MaybeReachable < T > {
278
282
Unreachable ,
279
283
Reachable ( T ) ,
280
284
}
281
285
282
- impl < T > MaybeUnreachable < T > {
286
+ impl < T > MaybeReachable < T > {
283
287
pub fn is_reachable ( & self ) -> bool {
284
- matches ! ( self , MaybeUnreachable :: Reachable ( _) )
288
+ matches ! ( self , MaybeReachable :: Reachable ( _) )
285
289
}
286
290
}
287
291
288
- impl < T > HasBottom for MaybeUnreachable < T > {
289
- const BOTTOM : Self = MaybeUnreachable :: Unreachable ;
292
+ impl < T > HasBottom for MaybeReachable < T > {
293
+ const BOTTOM : Self = MaybeReachable :: Unreachable ;
290
294
}
291
295
292
- impl < T : HasTop > HasTop for MaybeUnreachable < T > {
293
- const TOP : Self = MaybeUnreachable :: Reachable ( T :: TOP ) ;
296
+ impl < T : HasTop > HasTop for MaybeReachable < T > {
297
+ const TOP : Self = MaybeReachable :: Reachable ( T :: TOP ) ;
294
298
}
295
299
296
- impl < S > MaybeUnreachable < S > {
300
+ impl < S > MaybeReachable < S > {
301
+ /// Return whether the current state contains the given element. If the state is unreachable,
302
+ /// it does no contain anything.
297
303
pub fn contains < T > ( & self , elem : T ) -> bool
298
304
where
299
305
S : BitSetExt < T > ,
300
306
{
301
307
match self {
302
- MaybeUnreachable :: Unreachable => false ,
303
- MaybeUnreachable :: Reachable ( set) => set. contains ( elem) ,
308
+ MaybeReachable :: Unreachable => false ,
309
+ MaybeReachable :: Reachable ( set) => set. contains ( elem) ,
304
310
}
305
311
}
306
312
}
307
313
308
- impl < T , S : BitSetExt < T > > BitSetExt < T > for MaybeUnreachable < S > {
314
+ impl < T , S : BitSetExt < T > > BitSetExt < T > for MaybeReachable < S > {
309
315
fn contains ( & self , elem : T ) -> bool {
310
316
self . contains ( elem)
311
317
}
312
318
313
319
fn union ( & mut self , other : & HybridBitSet < T > ) {
314
320
match self {
315
- MaybeUnreachable :: Unreachable => { }
316
- MaybeUnreachable :: Reachable ( set) => set. union ( other) ,
321
+ MaybeReachable :: Unreachable => { }
322
+ MaybeReachable :: Reachable ( set) => set. union ( other) ,
317
323
}
318
324
}
319
325
320
326
fn subtract ( & mut self , other : & HybridBitSet < T > ) {
321
327
match self {
322
- MaybeUnreachable :: Unreachable => { }
323
- MaybeUnreachable :: Reachable ( set) => set. subtract ( other) ,
328
+ MaybeReachable :: Unreachable => { }
329
+ MaybeReachable :: Reachable ( set) => set. subtract ( other) ,
324
330
}
325
331
}
326
332
}
327
333
328
- impl < V : Clone > Clone for MaybeUnreachable < V > {
334
+ impl < V : Clone > Clone for MaybeReachable < V > {
329
335
fn clone ( & self ) -> Self {
330
336
match self {
331
- MaybeUnreachable :: Reachable ( x) => MaybeUnreachable :: Reachable ( x. clone ( ) ) ,
332
- MaybeUnreachable :: Unreachable => MaybeUnreachable :: Unreachable ,
337
+ MaybeReachable :: Reachable ( x) => MaybeReachable :: Reachable ( x. clone ( ) ) ,
338
+ MaybeReachable :: Unreachable => MaybeReachable :: Unreachable ,
333
339
}
334
340
}
335
341
336
342
fn clone_from ( & mut self , source : & Self ) {
337
343
match ( & mut * self , source) {
338
- ( MaybeUnreachable :: Reachable ( x) , MaybeUnreachable :: Reachable ( y) ) => {
344
+ ( MaybeReachable :: Reachable ( x) , MaybeReachable :: Reachable ( y) ) => {
339
345
x. clone_from ( & y) ;
340
346
}
341
347
_ => * self = source. clone ( ) ,
342
348
}
343
349
}
344
350
}
345
351
346
- impl < T : JoinSemiLattice + Clone > JoinSemiLattice for MaybeUnreachable < T > {
352
+ impl < T : JoinSemiLattice + Clone > JoinSemiLattice for MaybeReachable < T > {
347
353
fn join ( & mut self , other : & Self ) -> bool {
354
+ // Unreachable acts as a bottom.
348
355
match ( & mut * self , & other) {
349
- ( _, MaybeUnreachable :: Unreachable ) => false ,
350
- ( MaybeUnreachable :: Unreachable , _) => {
356
+ ( _, MaybeReachable :: Unreachable ) => false ,
357
+ ( MaybeReachable :: Unreachable , _) => {
351
358
* self = other. clone ( ) ;
352
359
true
353
360
}
354
- ( MaybeUnreachable :: Reachable ( this) , MaybeUnreachable :: Reachable ( other) ) => {
355
- this. join ( other)
356
- }
361
+ ( MaybeReachable :: Reachable ( this) , MaybeReachable :: Reachable ( other) ) => this. join ( other) ,
357
362
}
358
363
}
359
364
}
0 commit comments