@@ -496,29 +496,40 @@ impl<V: Clone> State<V> {
496496 values. raw . fill ( value) ;
497497 }
498498
499+ /// Assign `value` to all places that are contained in `place` or may alias one.
499500 pub fn flood_with ( & mut self , place : PlaceRef < ' _ > , map : & Map , value : V ) {
500- self . flood_with_extra ( place, None , map, value)
501+ self . flood_with_tail_elem ( place, None , map, value)
501502 }
502503
504+ /// Assign `TOP` to all places that are contained in `place` or may alias one.
503505 pub fn flood ( & mut self , place : PlaceRef < ' _ > , map : & Map )
504506 where
505507 V : HasTop ,
506508 {
507509 self . flood_with ( place, map, V :: TOP )
508510 }
509511
512+ /// Assign `value` to the discriminant of `place` and all places that may alias it.
510513 pub fn flood_discr_with ( & mut self , place : PlaceRef < ' _ > , map : & Map , value : V ) {
511- self . flood_with_extra ( place, Some ( TrackElem :: Discriminant ) , map, value)
514+ self . flood_with_tail_elem ( place, Some ( TrackElem :: Discriminant ) , map, value)
512515 }
513516
517+ /// Assign `TOP` to the discriminant of `place` and all places that may alias it.
514518 pub fn flood_discr ( & mut self , place : PlaceRef < ' _ > , map : & Map )
515519 where
516520 V : HasTop ,
517521 {
518522 self . flood_discr_with ( place, map, V :: TOP )
519523 }
520524
521- pub fn flood_with_extra (
525+ /// This method is the most general version of the `flood_*` method.
526+ ///
527+ /// Assign `value` on the given place and all places that may alias it. In particular, when
528+ /// the given place has a variant downcast, we invoke the function on all the other variants.
529+ ///
530+ /// `tail_elem` allows to support discriminants that are not a place in MIR, but that we track
531+ /// as such.
532+ pub fn flood_with_tail_elem (
522533 & mut self ,
523534 place : PlaceRef < ' _ > ,
524535 tail_elem : Option < TrackElem > ,
@@ -602,62 +613,79 @@ impl<V: Clone> State<V> {
602613 }
603614 }
604615
605- /// Retrieve the value stored for a place, or ⊤ if it is not tracked.
616+ /// Retrieve the value stored for a place, or `None` if it is not tracked.
606617 pub fn try_get ( & self , place : PlaceRef < ' _ > , map : & Map ) -> Option < V > {
607618 let place = map. find ( place) ?;
608619 self . try_get_idx ( place, map)
609620 }
610621
611- /// Retrieve the value stored for a place, or ⊤ if it is not tracked.
622+ /// Retrieve the discriminant stored for a place, or `None` if it is not tracked.
612623 pub fn try_get_discr ( & self , place : PlaceRef < ' _ > , map : & Map ) -> Option < V > {
613624 let place = map. find_discr ( place) ?;
614625 self . try_get_idx ( place, map)
615626 }
616627
617- /// Retrieve the value stored for a place index, or ⊤ if it is not tracked.
628+ /// Retrieve the slice length stored for a place, or `None` if it is not tracked.
629+ pub fn try_get_len ( & self , place : PlaceRef < ' _ > , map : & Map ) -> Option < V > {
630+ let place = map. find_len ( place) ?;
631+ self . try_get_idx ( place, map)
632+ }
633+
634+ /// Retrieve the value stored for a place index, or `None` if it is not tracked.
618635 pub fn try_get_idx ( & self , place : PlaceIndex , map : & Map ) -> Option < V > {
619636 match & self . 0 {
620637 StateData :: Reachable ( values) => {
621638 map. places [ place] . value_index . map ( |v| values[ v] . clone ( ) )
622639 }
623- StateData :: Unreachable => {
624- // Because this is unreachable, we can return any value we want.
625- None
626- }
640+ StateData :: Unreachable => None ,
627641 }
628642 }
629643
630644 /// Retrieve the value stored for a place, or ⊤ if it is not tracked.
645+ ///
646+ /// This method returns ⊥ if the place is tracked and the state is unreachable.
631647 pub fn get ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
632648 where
633649 V : HasBottom + HasTop ,
634650 {
635- map. find ( place) . map ( |place| self . get_idx ( place, map) ) . unwrap_or ( V :: TOP )
651+ match & self . 0 {
652+ StateData :: Reachable ( _) => self . try_get ( place, map) . unwrap_or ( V :: TOP ) ,
653+ // Because this is unreachable, we can return any value we want.
654+ StateData :: Unreachable => V :: BOTTOM ,
655+ }
636656 }
637657
638658 /// Retrieve the value stored for a place, or ⊤ if it is not tracked.
659+ ///
660+ /// This method returns ⊥ the current state is unreachable.
639661 pub fn get_discr ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
640662 where
641663 V : HasBottom + HasTop ,
642664 {
643- match map. find_discr ( place) {
644- Some ( place) => self . get_idx ( place, map) ,
645- None => V :: TOP ,
665+ match & self . 0 {
666+ StateData :: Reachable ( _) => self . try_get_discr ( place, map) . unwrap_or ( V :: TOP ) ,
667+ // Because this is unreachable, we can return any value we want.
668+ StateData :: Unreachable => V :: BOTTOM ,
646669 }
647670 }
648671
649672 /// Retrieve the value stored for a place, or ⊤ if it is not tracked.
673+ ///
674+ /// This method returns ⊥ the current state is unreachable.
650675 pub fn get_len ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
651676 where
652677 V : HasBottom + HasTop ,
653678 {
654- match map. find_len ( place) {
655- Some ( place) => self . get_idx ( place, map) ,
656- None => V :: TOP ,
679+ match & self . 0 {
680+ StateData :: Reachable ( _) => self . try_get_len ( place, map) . unwrap_or ( V :: TOP ) ,
681+ // Because this is unreachable, we can return any value we want.
682+ StateData :: Unreachable => V :: BOTTOM ,
657683 }
658684 }
659685
660686 /// Retrieve the value stored for a place index, or ⊤ if it is not tracked.
687+ ///
688+ /// This method returns ⊥ the current state is unreachable.
661689 pub fn get_idx ( & self , place : PlaceIndex , map : & Map ) -> V
662690 where
663691 V : HasBottom + HasTop ,
0 commit comments