From e1e1e785d0d3da376b7003d925cd558117920557 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 12 Sep 2024 15:42:13 +0200 Subject: [PATCH] Uplift some passes to ullbc --- charon/src/ast/ullbc_ast_utils.rs | 22 ++++++++++++++++++- charon/src/transform/mod.rs | 16 +++++++------- charon/src/transform/ops_to_function_calls.rs | 8 +++---- .../remove_arithmetic_overflow_checks.rs | 8 +++---- .../transform/update_closure_signatures.rs | 6 ++--- 5 files changed, 40 insertions(+), 20 deletions(-) diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs index 23a31aa1..5269648d 100644 --- a/charon/src/ast/ullbc_ast_utils.rs +++ b/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(&mut self, f: &mut F) + where + F: FnMut(&mut Vector, &mut [Statement]) -> Vec<(usize, Vec)>, + { + 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(&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. diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index a2076b60..65ac6ffa 100644 --- a/charon/src/transform/mod.rs +++ b/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.) diff --git a/charon/src/transform/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs index c58c0ff0..5e559b33 100644 --- a/charon/src/transform/ops_to_function_calls.rs +++ b/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); } } diff --git a/charon/src/transform/remove_arithmetic_overflow_checks.rs b/charon/src/transform/remove_arithmetic_overflow_checks.rs index 7d74b6b4..0404634e 100644 --- a/charon/src/transform/remove_arithmetic_overflow_checks.rs +++ b/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() }) diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index 613c4a36..ea8111e9 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/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,