charon_lib::transform

Module simplify_constants

source
Expand description

The MIR constant expressions lead to a lot of duplication: there are for instance constant ADTs which duplicate the “regular” aggregated ADTs in the operands, constant references, etc. This reduces the number of cases to handle and eases the function translation in Aeneas.

This pass removes all those occurrences so that only the [ConstantExpression::Literal]. It does so by introducing intermediate statements.

A small remark about the intermediate statements we introduce for the globals: we do so because, when evaluating the code in “concrete” mode, it allows to handle the globals like function calls.

Structs§

Functions§

  • If the constant value is a constant ADT, push Assign::Aggregate statements to the vector of statements, that bind new variables to the ADT parts and the variable assigned to the complete ADT.