Merge pull request #566 from Nadrieril/remove-units

charon/src/ast/expressions_utils.rs

@@ -43,6 +43,20 @@ impl Place {
     }
 }
 
+impl Rvalue {
+    pub fn unit_value() -> Self {
+        Rvalue::Aggregate(
+            AggregateKind::Adt(
+                TypeId::Tuple,
+                None,
+                None,
+                GenericArgs::empty(GenericsSource::Builtin),
+            ),
+            Vec::new(),
+        )
+    }
+}
+
 impl BorrowKind {
     pub fn mutable(x: bool) -> Self {
         if x {

charon/src/ast/gast_utils.rs

@@ -63,6 +63,11 @@ impl Locals {
     pub fn return_place(&self) -> Place {
         self.place_for_var(VarId::new(0))
     }
+
+    /// Locals that aren't arguments or return values.
+    pub fn non_argument_locals(&self) -> impl Iterator<Item = (VarId, &Var)> {
+        self.vars.iter_indexed().skip(1 + self.arg_count)
+    }
 }
 
 impl std::ops::Index<VarId> for Locals {

charon/src/transform/insert_assign_return_unit.rs

@@ -17,18 +17,9 @@ impl UllbcPass for Transform {
                 for block in &mut body.body {
                     if let RawTerminator::Return = block.terminator.content {
                         let return_place = body.locals.return_place();
-                        let unit_value = Rvalue::Aggregate(
-                            AggregateKind::Adt(
-                                TypeId::Tuple,
-                                None,
-                                None,
-                                GenericArgs::empty(GenericsSource::Builtin),
-                            ),
-                            Vec::new(),
-                        );
                         let assign_st = Statement::new(
                             block.terminator.span,
-                            RawStatement::Assign(return_place, unit_value),
+                            RawStatement::Assign(return_place, Rvalue::unit_value()),
                         );
                         block.statements.push(assign_st)
                     }

charon/src/transform/mod.rs

@@ -23,6 +23,7 @@ pub mod remove_drop_never;
 pub mod remove_dynamic_checks;
 pub mod remove_nops;
 pub mod remove_read_discriminant;
+pub mod remove_unit_locals;
 pub mod remove_unused_locals;
 pub mod remove_unused_methods;
 pub mod reorder_decls;
@@ -120,9 +121,9 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // of Aeneas, it means the return variable contains ⊥ upon returning.
     // For this reason, when the function has return type unit, we insert
     // an extra assignment just before returning.
-    // This also applies to globals (for checking or executing code before
-    // the main or at compile-time).
     UnstructuredBody(&insert_assign_return_unit::Transform),
+    // # Micro-pass: remove locals of type `()` which show up a lot.
+    UnstructuredBody(&remove_unit_locals::Transform),
     // # Micro-pass: remove the drops of locals whose type is `Never` (`!`). This
     // is in preparation of the next transformation.
     UnstructuredBody(&remove_drop_never::Transform),

charon/src/transform/remove_unit_locals.rs

@@ -0,0 +1,75 @@
+use derive_generic_visitor::*;
+use std::collections::HashSet;
+
+use crate::transform::TransformCtx;
+use crate::ullbc_ast::*;
+
+use super::ctx::UllbcPass;
+
+pub struct Transform;
+impl UllbcPass for Transform {
+    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ExprBody) {
+        // Replace any copy/move of a unit local to a plain const assignment. Note: we don't touch
+        // other `Rvalue`s as they might have side-effects (e.g. reading through a pointer).
+        body.visit_statements(|st| {
+            if let RawStatement::Assign(_, rvalue) = &mut st.content
+                && let Rvalue::Use(Operand::Move(from) | Operand::Copy(from)) = rvalue
+                && from.is_local()
+                && from.ty().is_unit()
+            {
+                *rvalue = Rvalue::unit_value()
+            }
+        });
+
+        // Find the unused locals of unit type.
+        #[derive(Visitor)]
+        struct UnitLocalsVisitor {
+            unused_unit_locals: HashSet<VarId>,
+        }
+        impl VisitBody for UnitLocalsVisitor {
+            fn enter_place(&mut self, x: &Place) {
+                if let Some(var_id) = x.as_local() {
+                    self.unused_unit_locals.remove(&var_id);
+                }
+            }
+            fn visit_ullbc_statement(
+                &mut self,
+                x: &ullbc_ast::Statement,
+            ) -> ControlFlow<Self::Break> {
+                match &x.content {
+                    RawStatement::Assign(place, rvalue) => {
+                        if place.is_local() && place.ty().is_unit() {
+                            // Don't count the assignment as a use.
+                        } else {
+                            self.visit(place)?;
+                        }
+                        self.visit(rvalue)?;
+                    }
+                    _ => self.visit_inner(x)?,
+                }
+                Continue(())
+            }
+        }
+        let unused_unit_locals = (UnitLocalsVisitor {
+            unused_unit_locals: body
+                .locals
+                .non_argument_locals()
+                .filter(|(_, var)| var.ty.is_unit())
+                .map(|(id, _)| id)
+                .collect(),
+        })
+        .visit_by_val_infallible(&*body)
+        .unused_unit_locals;
+
+        // Remove side-effect-free assignments into unused places.
+        body.visit_statements(|st| {
+            if let RawStatement::Assign(place, rvalue) = &st.content
+                && let Some(var_id) = place.as_local()
+                && unused_unit_locals.contains(&var_id)
+                && rvalue.is_aggregate()
+            {
+                st.content = RawStatement::Nop;
+            }
+        });
+    }
+}

charon/tests/cargo/build-script.out

@@ -13,10 +13,8 @@ global test_cargo_build_script::FOO: u8 = test_cargo_build_script::FOO()
 fn test_cargo_build_script::main()
 {
     let @0: (); // return
-    let @1: (); // anonymous local
 
-    @1 := ()
-    @0 := move (@1)
+    @0 := ()
     @0 := ()
     return
 }

charon/tests/cargo/dependencies.out

@@ -40,16 +40,14 @@ fn test_cargo_dependencies::silly_incr<'_0>(@1: &'_0 mut (u32))
     let @2: (); // anonymous local
     let @3: &'_ mut (u32); // anonymous local
     let @4: fn(u32) -> u32; // anonymous local
-    let @5: (); // anonymous local
 
     @3 := &two-phase-mut *(x@1)
     @4 := {test_cargo_dependencies::silly_incr::closure} {}
     @2 := take_mut::take<'_, u32, fn(u32) -> u32>[core::marker::Sized<u32>, core::marker::Sized<fn(u32) -> u32>, core::ops::function::FnOnce<fn(u32) -> u32, (u32)> where Output  = u32](move (@3), move (@4))
     drop @4
     drop @3
     drop @2
-    @5 := ()
-    @0 := move (@5)
+    @0 := ()
     @0 := ()
     return
 }
@@ -96,8 +94,6 @@ fn test_cargo_dependencies::main()
     let @19: &'_ (u32); // anonymous local
     let @20: &'_ (u32); // anonymous local
     let @21: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
-    let @22: (); // anonymous local
-    let @23: (); // anonymous local
 
     x@1 := const (0 : u32)
     @fake_read(x@1)
@@ -136,16 +132,13 @@ fn test_cargo_dependencies::main()
     }
     drop @14
     drop @13
-    @22 := ()
-    @5 := move (@22)
     drop @12
     drop right_val@11
     drop left_val@10
     drop @9
     drop @6
     drop @5
-    @23 := ()
-    @0 := move (@23)
+    @0 := ()
     drop x@1
     @0 := ()
     return

charon/tests/cargo/toml.out

@@ -35,7 +35,6 @@ fn test_cargo_toml::main()
     let @1: bool; // anonymous local
     let @2: &'_ (core::option::Option<bool>[core::marker::Sized<bool>]); // anonymous local
     let @3: core::option::Option<bool>[core::marker::Sized<bool>]; // anonymous local
-    let @4: (); // anonymous local
 
     @3 := core::option::Option::Some { 0: const (false) }
     @2 := &@3
@@ -44,8 +43,7 @@ fn test_cargo_toml::main()
     @fake_read(@1)
     drop @3
     drop @1
-    @4 := ()
-    @0 := move (@4)
+    @0 := ()
     @0 := ()
     return
 }