charon_lib/transform/simplify_output/
index_intermediate_assigns.rs

1//! This micro-pass introduces intermediate assignments in preparation of
2//! [`crate::transform::simplify_output::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::transform::ctx::{BodyTransformCtx, UllbcPass};
38use crate::ullbc_ast::*;
39
40fn contains_index_proj<T: BodyVisitable>(x: &T) -> bool {
41    let mut contains_index = false;
42    x.dyn_visit_in_body(|proj: &ProjectionElem| {
43        use ProjectionElem::*;
44        if let Index { .. } | Subslice { .. } = proj {
45            contains_index = true;
46        }
47    });
48    contains_index
49}
50
51impl Place {
52    fn contains_index_proj(&self) -> bool {
53        contains_index_proj(self)
54    }
55}
56
57impl Rvalue {
58    fn contains_index_proj(&self) -> bool {
59        contains_index_proj(self)
60    }
61}
62
63pub struct Transform;
64
65impl UllbcPass for Transform {
66    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
67        decl.transform_ullbc_statements(ctx, |ctx, st: &mut Statement| {
68            // Introduce an intermediate statement if both the rhs and the lhs contain an
69            // "index" projection element (to avoid introducing too many intermediate
70            // assignments).
71            if let StatementKind::Assign(lhs, rhs) = &mut st.kind
72                && lhs.contains_index_proj()
73                && rhs.contains_index_proj()
74            {
75                // Fresh local variable for the temporary assignment
76                let tmp_var = ctx.fresh_var(None, lhs.ty().clone());
77                let tmp_rhs = std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone())));
78                // Introduce the intermediate let-binding
79                ctx.insert_assn_stmt(tmp_var, tmp_rhs)
80            }
81        });
82    }
83}
charon_lib/transform/simplify_output/index_intermediate_assigns.rs

charon_lib/transform/simplify_output/
index_intermediate_assigns.rs
