@@ -273,87 +273,92 @@ impl<T> HasTop for FlatSet<T> {
273273 const TOP : Self = Self :: Top ;
274274}
275275
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.
276280#[ derive( PartialEq , Eq , Debug ) ]
277- pub enum MaybeUnreachable < T > {
281+ pub enum MaybeReachable < T > {
278282 Unreachable ,
279283 Reachable ( T ) ,
280284}
281285
282- impl < T > MaybeUnreachable < T > {
286+ impl < T > MaybeReachable < T > {
283287 pub fn is_reachable ( & self ) -> bool {
284- matches ! ( self , MaybeUnreachable :: Reachable ( _) )
288+ matches ! ( self , MaybeReachable :: Reachable ( _) )
285289 }
286290}
287291
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 ;
290294}
291295
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 ) ;
294298}
295299
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.
297303 pub fn contains < T > ( & self , elem : T ) -> bool
298304 where
299305 S : BitSetExt < T > ,
300306 {
301307 match self {
302- MaybeUnreachable :: Unreachable => false ,
303- MaybeUnreachable :: Reachable ( set) => set. contains ( elem) ,
308+ MaybeReachable :: Unreachable => false ,
309+ MaybeReachable :: Reachable ( set) => set. contains ( elem) ,
304310 }
305311 }
306312}
307313
308- impl < T , S : BitSetExt < T > > BitSetExt < T > for MaybeUnreachable < S > {
314+ impl < T , S : BitSetExt < T > > BitSetExt < T > for MaybeReachable < S > {
309315 fn contains ( & self , elem : T ) -> bool {
310316 self . contains ( elem)
311317 }
312318
313319 fn union ( & mut self , other : & HybridBitSet < T > ) {
314320 match self {
315- MaybeUnreachable :: Unreachable => { }
316- MaybeUnreachable :: Reachable ( set) => set. union ( other) ,
321+ MaybeReachable :: Unreachable => { }
322+ MaybeReachable :: Reachable ( set) => set. union ( other) ,
317323 }
318324 }
319325
320326 fn subtract ( & mut self , other : & HybridBitSet < T > ) {
321327 match self {
322- MaybeUnreachable :: Unreachable => { }
323- MaybeUnreachable :: Reachable ( set) => set. subtract ( other) ,
328+ MaybeReachable :: Unreachable => { }
329+ MaybeReachable :: Reachable ( set) => set. subtract ( other) ,
324330 }
325331 }
326332}
327333
328- impl < V : Clone > Clone for MaybeUnreachable < V > {
334+ impl < V : Clone > Clone for MaybeReachable < V > {
329335 fn clone ( & self ) -> Self {
330336 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 ,
333339 }
334340 }
335341
336342 fn clone_from ( & mut self , source : & Self ) {
337343 match ( & mut * self , source) {
338- ( MaybeUnreachable :: Reachable ( x) , MaybeUnreachable :: Reachable ( y) ) => {
344+ ( MaybeReachable :: Reachable ( x) , MaybeReachable :: Reachable ( y) ) => {
339345 x. clone_from ( & y) ;
340346 }
341347 _ => * self = source. clone ( ) ,
342348 }
343349 }
344350}
345351
346- impl < T : JoinSemiLattice + Clone > JoinSemiLattice for MaybeUnreachable < T > {
352+ impl < T : JoinSemiLattice + Clone > JoinSemiLattice for MaybeReachable < T > {
347353 fn join ( & mut self , other : & Self ) -> bool {
354+ // Unreachable acts as a bottom.
348355 match ( & mut * self , & other) {
349- ( _, MaybeUnreachable :: Unreachable ) => false ,
350- ( MaybeUnreachable :: Unreachable , _) => {
356+ ( _, MaybeReachable :: Unreachable ) => false ,
357+ ( MaybeReachable :: Unreachable , _) => {
351358 * self = other. clone ( ) ;
352359 true
353360 }
354- ( MaybeUnreachable :: Reachable ( this) , MaybeUnreachable :: Reachable ( other) ) => {
355- this. join ( other)
356- }
361+ ( MaybeReachable :: Reachable ( this) , MaybeReachable :: Reachable ( other) ) => this. join ( other) ,
357362 }
358363 }
359364}
0 commit comments