|
24 | 24 | //! - The bottom state denotes uninitialized memory. Because we are only doing a sound approximation
|
25 | 25 | //! of the actual execution, we can also use this state for places where access would be UB.
|
26 | 26 | //!
|
27 |
| -//! - The assignment logic in `State::assign_place_idx` assumes that the places are non-overlapping, |
| 27 | +//! - The assignment logic in `State::insert_place_idx` assumes that the places are non-overlapping, |
28 | 28 | //! or identical. Note that this refers to place expressions, not memory locations.
|
29 | 29 | //!
|
30 | 30 | //! - Currently, places that have their reference taken cannot be tracked. Although this would be
|
@@ -470,59 +470,68 @@ impl<V: Clone + HasTop + HasBottom> State<V> {
|
470 | 470 | self.flood_discr_with(place, map, V::top())
|
471 | 471 | }
|
472 | 472 |
|
| 473 | + /// Low-level method that assigns to a place. |
| 474 | + /// This does nothing if the place is not tracked. |
| 475 | + /// |
| 476 | + /// The target place must have been flooded before calling this method. |
| 477 | + pub fn insert_idx(&mut self, target: PlaceIndex, result: ValueOrPlace<V>, map: &Map) { |
| 478 | + match result { |
| 479 | + ValueOrPlace::Value(value) => self.insert_value_idx(target, value, map), |
| 480 | + ValueOrPlace::Place(source) => self.insert_place_idx(target, source, map), |
| 481 | + } |
| 482 | + } |
| 483 | + |
| 484 | + /// Low-level method that assigns a value to a place. |
| 485 | + /// This does nothing if the place is not tracked. |
| 486 | + /// |
| 487 | + /// The target place must have been flooded before calling this method. |
| 488 | + pub fn insert_value_idx(&mut self, target: PlaceIndex, value: V, map: &Map) { |
| 489 | + let StateData::Reachable(values) = &mut self.0 else { return }; |
| 490 | + if let Some(value_index) = map.places[target].value_index { |
| 491 | + values[value_index] = value; |
| 492 | + } |
| 493 | + } |
| 494 | + |
473 | 495 | /// Copies `source` to `target`, including all tracked places beneath.
|
474 | 496 | ///
|
475 | 497 | /// If `target` contains a place that is not contained in `source`, it will be overwritten with
|
476 | 498 | /// Top. Also, because this will copy all entries one after another, it may only be used for
|
477 | 499 | /// places that are non-overlapping or identical.
|
478 | 500 | ///
|
479 | 501 | /// The target place must have been flooded before calling this method.
|
480 |
| - fn assign_place_idx(&mut self, target: PlaceIndex, source: PlaceIndex, map: &Map) { |
| 502 | + fn insert_place_idx(&mut self, target: PlaceIndex, source: PlaceIndex, map: &Map) { |
481 | 503 | let StateData::Reachable(values) = &mut self.0 else { return };
|
482 | 504 |
|
483 |
| - // If both places are tracked, we copy the value to the target. If the target is tracked, |
484 |
| - // but the source is not, we have to invalidate the value in target. If the target is not |
485 |
| - // tracked, then we don't have to do anything. |
| 505 | + // If both places are tracked, we copy the value to the target. |
| 506 | + // If the target is tracked, but the source is not, we do nothing, as invalidation has |
| 507 | + // already been performed. |
486 | 508 | if let Some(target_value) = map.places[target].value_index {
|
487 | 509 | if let Some(source_value) = map.places[source].value_index {
|
488 | 510 | values[target_value] = values[source_value].clone();
|
489 |
| - } else { |
490 |
| - values[target_value] = V::top(); |
491 | 511 | }
|
492 | 512 | }
|
493 | 513 | for target_child in map.children(target) {
|
494 | 514 | // Try to find corresponding child and recurse. Reasoning is similar as above.
|
495 | 515 | let projection = map.places[target_child].proj_elem.unwrap();
|
496 | 516 | if let Some(source_child) = map.projections.get(&(source, projection)) {
|
497 |
| - self.assign_place_idx(target_child, *source_child, map); |
| 517 | + self.insert_place_idx(target_child, *source_child, map); |
498 | 518 | }
|
499 | 519 | }
|
500 | 520 | }
|
501 | 521 |
|
| 522 | + /// Helper method to interpret `target = result`. |
502 | 523 | pub fn assign(&mut self, target: PlaceRef<'_>, result: ValueOrPlace<V>, map: &Map) {
|
503 | 524 | self.flood(target, map);
|
504 | 525 | if let Some(target) = map.find(target) {
|
505 |
| - self.assign_idx(target, result, map); |
| 526 | + self.insert_idx(target, result, map); |
506 | 527 | }
|
507 | 528 | }
|
508 | 529 |
|
| 530 | + /// Helper method for assignments to a discriminant. |
509 | 531 | pub fn assign_discr(&mut self, target: PlaceRef<'_>, result: ValueOrPlace<V>, map: &Map) {
|
510 | 532 | self.flood_discr(target, map);
|
511 | 533 | if let Some(target) = map.find_discr(target) {
|
512 |
| - self.assign_idx(target, result, map); |
513 |
| - } |
514 |
| - } |
515 |
| - |
516 |
| - /// The target place must have been flooded before calling this method. |
517 |
| - pub fn assign_idx(&mut self, target: PlaceIndex, result: ValueOrPlace<V>, map: &Map) { |
518 |
| - match result { |
519 |
| - ValueOrPlace::Value(value) => { |
520 |
| - let StateData::Reachable(values) = &mut self.0 else { return }; |
521 |
| - if let Some(value_index) = map.places[target].value_index { |
522 |
| - values[value_index] = value; |
523 |
| - } |
524 |
| - } |
525 |
| - ValueOrPlace::Place(source) => self.assign_place_idx(target, source, map), |
| 534 | + self.insert_idx(target, result, map); |
526 | 535 | }
|
527 | 536 | }
|
528 | 537 |
|
|
0 commit comments