bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Clarify place expressions vs place objects

Browse source
This commit is contained in:
Jannis Christopher Köhl 2022-09-01 13:50:31 +02:00
parent 1da3033340
commit 3f98dc7838
1 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

25
compiler/rustc_mir_dataflow/src/value_analysis.rs
View file

@ -20,27 +20,34 @@
//! # Correctness //! # Correctness
//! //!
//! Warning: This is a semi-formal attempt to argue for the correctness of this analysis. If you //! Warning: This is a semi-formal attempt to argue for the correctness of this analysis. If you
//! find any weak spots, let me know! Recommended reading: Abstract Interpretation. //! find any weak spots, let me know! Recommended reading: Abstract Interpretation. We will use the
//! term "place" to refer to a place expression (like `mir::Place`), and we will call the
//! underlying entity "object". For instance, `*_1` and `*_2` are not the same place, but depending
//! on the value of `_1` and `_2`, they could refer to the same object. Also, the same place can
//! refer to different objects during execution. If `_1` is reassigned, then `*_1` may refer to
//! different objects before and after assignment. Additionally, when saying "access to a place",
//! what we really mean is "access to an object denoted by arbitrary projections of that place".
//! //!
//! In the following, we will assume a constant propagation analysis. Our analysis is correct if //! In the following, we will assume a constant propagation analysis. Our analysis is correct if
//! every transfer function is correct. This is the case if for every pair (f, f#) and abstract //! every transfer function is correct. This is the case if for every pair (f, f#) and abstract
//! state s, we have f(y(s)) <= y(f#(s)), where s is a mapping from tracked place to top, bottom or //! state s, we have f(y(s)) <= y(f#(s)), where s is a mapping from tracked place to top, bottom or
//! a constant. Since pointers (and mutable references) are not tracked, but can be used to change //! a constant. Since pointers (and mutable references) are not tracked, but can be used to change
//! values in the concrete domain, f# must assume that all places that can be affected in this way //! values in the concrete domain, f# must assume that all places that can be affected in this way
//! for a given program point are marked with top (otherwise many assignments and function calls //! for a given program point are already marked with top in s (otherwise many assignments and
//! would have no choice but to mark all tracked places with top). This leads us to an invariant: //! function calls would have no choice but to mark all tracked places with top). This leads us to
//! For all possible program points where there could possibly exist a mutable reference or pointer //! an invariant: For all possible program points where there could possibly exist means of mutable
//! to a tracked place (in the concrete domain), this place must be assigned to top (in the //! access to a tracked place (in the concrete domain), this place must be assigned to top (in the
//! abstract domain). The concretization function y can be defined as expected for the constant //! abstract domain). The concretization function y can be defined as expected for the constant
//! propagation analysis, although the concrete state of course contains all kinds of non-tracked //! propagation analysis, although the concrete state of course contains all kinds of non-tracked
//! data. However, by the invariant above, no mutable references or pointers to tracked places that //! data. However, by the invariant above, no mutable access to tracked places that are not marked
//! are not marked with top may be introduced. //! with top may be introduced.
//! //!
//! Note that we (at least currently) do not differentiate between "this place may assume different //! Note that we (at least currently) do not differentiate between "this place may assume different
//! values" and "a pointer to this place escaped the analysis". However, we still want to handle //! values" and "a pointer to this place escaped the analysis". However, we still want to handle
//! assignments to constants as usual for f#. This adds an assumption: Whenever we have an //! assignments to constants as usual for f#. This adds an assumption: Whenever we have an
//! assignment, all mutable access to the underlying place (which is not observed by the analysis) //! assignment that is captured by the analysis, all mutable access to the underlying place (which
//! must be invalidated. This is (hopefully) covered by Stacked Borrows. //! is not observable by the analysis) must be invalidated. This is (hopefully) covered by Stacked
//! Borrows.
//! //!
//! To be continued... //! To be continued...