charon_lib/transform/
index_intermediate_assigns.rs

1//! This micro-pass introduces intermediate assignments in preparation of
2//! [`index_to_function_calls`], so as to avoid borrow-checking errors.
3//!
4//! The problem comes from "and assignments" like in the snippet of code below:
5//! ```text
6//! x[0] += 1; // Desugars to: x[0] = copy x[0] + 1
7//! ```
8//!
9//! If we don't introduce an intermediate assignment, then the micro-pass which
10//! transforms the index operations into function calls generates the following
11//! LLBC:
12//! ```text
13//! dest = &mut x[0];
14//! src = & x[0]; // Invalidates dest
15//! *dest = copy (*src) + 1; // Can't dereference dest!
16//! ```
17//! (also note that the problem remains if we introduce `src` *then* `dest`).
18//!
19//! Our solution is to introduce a temporary variable for the assignment.
20//! We first transform the code to:
21//! ```text
22//! tmp = copy x[0] + 1;
23//! x[0] = move tmp;
24//! ```
25//!
26//! Which then allows us to transform it to:
27//! ```text
28//! // RHS:
29//! src = & x[0];
30//! tmp = copy (*src) + 1;
31//! // LHS:
32//! dest = &mut x[0];
33//! *dest = move tmp;
34//! ```
35
36use crate::transform::TransformCtx;
37use crate::ullbc_ast::*;
38
39use super::ctx::UllbcPass;
40
41fn contains_index_proj<T: BodyVisitable>(x: &T) -> bool {
42    let mut contains_index = false;
43    x.dyn_visit_in_body(|proj: &ProjectionElem| {
44        use ProjectionElem::*;
45        if let Index { .. } | Subslice { .. } = proj {
46            contains_index = true;
47        }
48    });
49    contains_index
50}
51
52impl Place {
53    fn contains_index_proj(&self) -> bool {
54        contains_index_proj(self)
55    }
56}
57
58impl Rvalue {
59    fn contains_index_proj(&self) -> bool {
60        contains_index_proj(self)
61    }
62}
63
64pub struct Transform;
65
66impl UllbcPass for Transform {
67    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
68        for block in &mut b.body {
69            block.transform(|st: &mut Statement| {
70                match &mut st.content {
71                    // Introduce an intermediate statement if both the rhs and the lhs contain an
72                    // "index" projection element (to avoid introducing too many intermediate
73                    // assignments).
74                    RawStatement::Assign(lhs, rhs)
75                        if lhs.contains_index_proj() && rhs.contains_index_proj() =>
76                    {
77                        // Fresh local variable for the temporary assignment
78                        let tmp_var = b.locals.new_var(None, lhs.ty().clone());
79                        let tmp_rhs =
80                            std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone())));
81                        // Introduce the intermediate let-binding
82                        vec![Statement::new(
83                            st.span,
84                            RawStatement::Assign(tmp_var, tmp_rhs),
85                        )]
86                    }
87                    _ => vec![],
88                }
89            });
90        }
91    }
92}
charon_lib/transform/index_intermediate_assigns.rs

charon_lib/transform/
index_intermediate_assigns.rs
