Merge pull request #357 from Nadrieril/move-passes-to-ullbc

charon/src/ast/ullbc_ast_utils.rs

@@ -2,7 +2,7 @@
 use crate::ids::Vector;
 use crate::meta::Span;
 use crate::ullbc_ast::*;
-use derive_visitor::{visitor_enter_fn_mut, DriveMut};
+use derive_visitor::{visitor_enter_fn_mut, visitor_fn_mut, DriveMut, Event};
 use take_mut::take;
 
 impl SwitchTargets {
@@ -103,6 +103,26 @@ impl BlockData {
     }
 }
 
+impl ExprBody {
+    pub fn transform_sequences<F>(&mut self, f: &mut F)
+    where
+        F: FnMut(&mut Vector<VarId, Var>, &mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
+    {
+        for block in &mut self.body {
+            block.transform_sequences(&mut |seq| f(&mut self.locals, seq));
+        }
+    }
+
+    /// Apply a function to all the statements, in a bottom-up manner.
+    pub fn visit_statements<F: FnMut(&mut Statement)>(&mut self, f: &mut F) {
+        self.drive_mut(&mut visitor_fn_mut(|st: &mut Statement, e: Event| {
+            if matches!(e, Event::Exit) {
+                f(st)
+            }
+        }))
+    }
+}
+
 /// Transform a body by applying a function to its operands, and
 /// inserting the statements generated by the operands at the end of the
 /// block.

charon/src/transform/mod.rs

@@ -55,26 +55,26 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // # Micro-pass: desugar the constants to other values/operands as much
     // as possible.
     UnstructuredBody(&simplify_constants::Transform),
-];
-
-pub static LLBC_PASSES: &[Pass] = &[
     // # Micro-pass: the first local variable of closures is the
     // closure itself. This is not consistent with the closure signature,
     // which ignores this first variable. This micro-pass updates this.
-    StructuredBody(&update_closure_signatures::Transform),
+    UnstructuredBody(&update_closure_signatures::Transform),
     // # Micro-pass: remove the dynamic checks we couldn't remove in [`remove_dynamic_checks`].
     // **WARNING**: this pass uses the fact that the dynamic checks
     // introduced by Rustc use a special "assert" construct. Because of
     // this, it must happen *before* the [reconstruct_asserts] pass.
-    StructuredBody(&remove_arithmetic_overflow_checks::Transform),
+    UnstructuredBody(&remove_arithmetic_overflow_checks::Transform),
+    // # Micro-pass: replace some unops/binops and the array aggregates with
+    // function calls (introduces: ArrayToSlice, etc.)
+    UnstructuredBody(&ops_to_function_calls::Transform),
+];
+
+pub static LLBC_PASSES: &[Pass] = &[
     // # Micro-pass: reconstruct the asserts
     StructuredBody(&reconstruct_asserts::Transform),
     // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans
     // those up.
     StructuredBody(&inline_local_panic_functions::Transform),
-    // # Micro-pass: replace some unops/binops and the array aggregates with
-    // function calls (introduces: ArrayToSlice, etc.)
-    StructuredBody(&ops_to_function_calls::Transform),
     // # Micro-pass: replace the arrays/slices index operations with function
     // calls.
     // (introduces: ArrayIndexShared, ArrayIndexMut, etc.)

charon/src/transform/ops_to_function_calls.rs

@@ -2,10 +2,10 @@
 //! For instance, we desugar ArrayToSlice from an unop to a function call.
 //! This allows a more uniform treatment later on.
 //! TODO: actually transform all the unops and binops to function calls?
-use crate::llbc_ast::*;
 use crate::transform::TransformCtx;
+use crate::ullbc_ast::*;
 
-use super::ctx::LlbcPass;
+use super::ctx::UllbcPass;
 
 fn transform_st(s: &mut Statement) {
     match &s.content {
@@ -55,8 +55,8 @@ fn transform_st(s: &mut Statement) {
 }
 
 pub struct Transform;
-impl LlbcPass for Transform {
+impl UllbcPass for Transform {
     fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) {
-        b.body.visit_statements(&mut transform_st);
+        b.visit_statements(&mut transform_st);
     }
 }

charon/src/transform/remove_arithmetic_overflow_checks.rs

@@ -1,9 +1,9 @@
 //! # Micro-pass: remove the overflow checks for arithmetic operations we couldn't remove in
 //! [`remove_dynamic_checks`]. See comments there for more details.
-use crate::llbc_ast::*;
 use crate::transform::TransformCtx;
+use crate::ullbc_ast::*;
 
-use super::ctx::LlbcPass;
+use super::ctx::UllbcPass;
 
 pub struct Transform;
 
@@ -78,9 +78,9 @@ impl Transform {
     }
 }
 
-impl LlbcPass for Transform {
+impl UllbcPass for Transform {
     fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) {
-        b.body.transform_sequences(&mut |seq| {
+        b.transform_sequences(&mut |_, seq| {
             Transform::update_statements(seq);
             Vec::new()
         })

charon/src/transform/update_closure_signatures.rs

@@ -5,10 +5,10 @@ use derive_visitor::{visitor_enter_fn_mut, DriveMut, VisitorMut};
 
 use crate::common::*;
 use crate::ids::Vector;
-use crate::llbc_ast::*;
 use crate::transform::TransformCtx;
+use crate::ullbc_ast::*;
 
-use super::ctx::LlbcPass;
+use super::ctx::UllbcPass;
 
 #[derive(VisitorMut)]
 #[visitor(Region(exit), Ty(enter, exit))]
@@ -150,7 +150,7 @@ fn transform_function(
 }
 
 pub struct Transform;
-impl LlbcPass for Transform {
+impl UllbcPass for Transform {
     fn transform_function(
         &self,
         ctx: &mut TransformCtx,