charon_lib::transform

Module index_intermediate_assigns

source
Expand description

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:

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:

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:

tmp = copy x[0] + 1;
x[0] = move tmp;

Which then allows us to transform it to:

// RHS:
src = & x[0];
tmp = copy (*src) + 1;
// LHS:
dest = &mut x[0];
*dest = move tmp;

Structs§

Functions§