@@ -496,29 +496,40 @@ impl<V: Clone> State<V> {
496
496
values. raw . fill ( value) ;
497
497
}
498
498
499
+ /// Assign `value` to all places that are contained in `place` or may alias one.
499
500
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)
501
502
}
502
503
504
+ /// Assign `TOP` to all places that are contained in `place` or may alias one.
503
505
pub fn flood ( & mut self , place : PlaceRef < ' _ > , map : & Map )
504
506
where
505
507
V : HasTop ,
506
508
{
507
509
self . flood_with ( place, map, V :: TOP )
508
510
}
509
511
512
+ /// Assign `value` to the discriminant of `place` and all places that may alias it.
510
513
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)
512
515
}
513
516
517
+ /// Assign `TOP` to the discriminant of `place` and all places that may alias it.
514
518
pub fn flood_discr ( & mut self , place : PlaceRef < ' _ > , map : & Map )
515
519
where
516
520
V : HasTop ,
517
521
{
518
522
self . flood_discr_with ( place, map, V :: TOP )
519
523
}
520
524
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 (
522
533
& mut self ,
523
534
place : PlaceRef < ' _ > ,
524
535
tail_elem : Option < TrackElem > ,
@@ -602,62 +613,79 @@ impl<V: Clone> State<V> {
602
613
}
603
614
}
604
615
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.
606
617
pub fn try_get ( & self , place : PlaceRef < ' _ > , map : & Map ) -> Option < V > {
607
618
let place = map. find ( place) ?;
608
619
self . try_get_idx ( place, map)
609
620
}
610
621
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.
612
623
pub fn try_get_discr ( & self , place : PlaceRef < ' _ > , map : & Map ) -> Option < V > {
613
624
let place = map. find_discr ( place) ?;
614
625
self . try_get_idx ( place, map)
615
626
}
616
627
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.
618
635
pub fn try_get_idx ( & self , place : PlaceIndex , map : & Map ) -> Option < V > {
619
636
match & self . 0 {
620
637
StateData :: Reachable ( values) => {
621
638
map. places [ place] . value_index . map ( |v| values[ v] . clone ( ) )
622
639
}
623
- StateData :: Unreachable => {
624
- // Because this is unreachable, we can return any value we want.
625
- None
626
- }
640
+ StateData :: Unreachable => None ,
627
641
}
628
642
}
629
643
630
644
/// 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.
631
647
pub fn get ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
632
648
where
633
649
V : HasBottom + HasTop ,
634
650
{
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
+ }
636
656
}
637
657
638
658
/// Retrieve the value stored for a place, or ⊤ if it is not tracked.
659
+ ///
660
+ /// This method returns ⊥ the current state is unreachable.
639
661
pub fn get_discr ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
640
662
where
641
663
V : HasBottom + HasTop ,
642
664
{
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 ,
646
669
}
647
670
}
648
671
649
672
/// Retrieve the value stored for a place, or ⊤ if it is not tracked.
673
+ ///
674
+ /// This method returns ⊥ the current state is unreachable.
650
675
pub fn get_len ( & self , place : PlaceRef < ' _ > , map : & Map ) -> V
651
676
where
652
677
V : HasBottom + HasTop ,
653
678
{
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 ,
657
683
}
658
684
}
659
685
660
686
/// Retrieve the value stored for a place index, or ⊤ if it is not tracked.
687
+ ///
688
+ /// This method returns ⊥ the current state is unreachable.
661
689
pub fn get_idx ( & self , place : PlaceIndex , map : & Map ) -> V
662
690
where
663
691
V : HasBottom + HasTop ,
0 commit comments