From 3f98dc78380a60ffea0e5849393a718a10f495b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jannis=20Christopher=20K=C3=B6hl?= Date: Thu, 1 Sep 2022 13:50:31 +0200 Subject: [PATCH] Clarify place expressions vs place objects --- .../rustc_mir_dataflow/src/value_analysis.rs | 25 ++++++++++++------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/compiler/rustc_mir_dataflow/src/value_analysis.rs b/compiler/rustc_mir_dataflow/src/value_analysis.rs index 8b913d70800..bc367de4baa 100644 --- a/compiler/rustc_mir_dataflow/src/value_analysis.rs +++ b/compiler/rustc_mir_dataflow/src/value_analysis.rs @@ -20,27 +20,34 @@ //! # Correctness //! //! 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 //! 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 //! 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 -//! for a given program point are marked with top (otherwise many assignments and function calls -//! would have no choice but to mark all tracked places with top). This leads us to an invariant: -//! For all possible program points where there could possibly exist a mutable reference or pointer -//! to a tracked place (in the concrete domain), this place must be assigned to top (in the +//! for a given program point are already marked with top in s (otherwise many assignments and +//! function calls would have no choice but to mark all tracked places with top). This leads us to +//! an invariant: For all possible program points where there could possibly exist means of mutable +//! 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 //! 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 -//! are not marked with top may be introduced. +//! data. However, by the invariant above, no mutable access to tracked places that are not marked +//! with top may be introduced. //! //! 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 //! 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) -//! must be invalidated. This is (hopefully) covered by Stacked Borrows. +//! assignment that is captured by the analysis, all mutable access to the underlying place (which +//! is not observable by the analysis) must be invalidated. This is (hopefully) covered by Stacked +//! Borrows. //! //! To be continued...