charon_lib/transform/
index_intermediate_assigns.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
//! This micro-pass introduces intermediate assignments in preparation of
//! [`index_to_function_calls`], so as to avoid borrow-checking errors.
//!
//! The problem comes from "and assignments" like in the snippet of code below:
//! ```text
//! x[0] += 1; // Desugars to: x[0] = copy x[0] + 1
//! ```
//!
//! If we don't introduce an intermediate assignment, then the micro-pass which
//! transforms the index operations into function calls generates the following
//! LLBC:
//! ```text
//! dest = &mut x[0];
//! src = & x[0]; // Invalidates dest
//! *dest = copy (*src) + 1; // Can't dereference dest!
//! ```
//! (also note that the problem remains if we introduce `src` *then* `dest`).
//!
//! Our solution is to introduce a temporary variable for the assignment.
//! We first transform the code to:
//! ```text
//! tmp = copy x[0] + 1;
//! x[0] = move tmp;
//! ```
//!
//! Which then allows us to transform it to:
//! ```text
//! // RHS:
//! src = & x[0];
//! tmp = copy (*src) + 1;
//! // LHS:
//! dest = &mut x[0];
//! *dest = move tmp;
//! ```

use crate::transform::TransformCtx;
use crate::ullbc_ast::*;

use super::ctx::UllbcPass;

fn contains_index_proj<T: BodyVisitable>(x: &T) -> bool {
    let mut contains_index = false;
    x.dyn_visit_in_body(|proj: &ProjectionElem| {
        use ProjectionElem::*;
        if let Index { .. } | Subslice { .. } = proj {
            contains_index = true;
        }
    });
    contains_index
}

impl Place {
    fn contains_index_proj(&self) -> bool {
        contains_index_proj(self)
    }
}

impl Rvalue {
    fn contains_index_proj(&self) -> bool {
        contains_index_proj(self)
    }
}

pub struct Transform;

impl UllbcPass for Transform {
    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
        for block in &mut b.body {
            block.transform(|st: &mut Statement| {
                match &mut st.content {
                    // Introduce an intermediate statement if both the rhs and the lhs contain an
                    // "index" projection element (to avoid introducing too many intermediate
                    // assignments).
                    RawStatement::Assign(lhs, rhs)
                        if lhs.contains_index_proj() && rhs.contains_index_proj() =>
                    {
                        // Fresh local variable for the temporary assignment
                        let tmp_var = b.locals.new_var(None, lhs.ty().clone());
                        let tmp_rhs =
                            std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone())));
                        // Introduce the intermediate let-binding
                        vec![Statement::new(
                            st.span,
                            RawStatement::Assign(tmp_var, tmp_rhs),
                        )]
                    }
                    _ => vec![],
                }
            });
        }
    }
}