Fill missing fields in vtables

charon/src/ast/gast_utils.rs

@@ -74,6 +74,11 @@ impl Locals {
         Place::new(local_id, ty)
     }
 
+    /// Returns whether this local is the special return local or one of the input argument locals.
+    pub fn is_return_or_arg(&self, lid: LocalId) -> bool {
+        lid.index() <= self.arg_count
+    }
+
     /// The place where we write the return value.
     pub fn return_place(&self) -> Place {
         self.place_for_var(LocalId::new(0))

charon/src/ast/ullbc_ast_utils.rs

@@ -209,3 +209,91 @@ impl ExprBody {
         }
     }
 }
+
+/// Helper to construct a small ullbc body.
+pub struct BodyBuilder {
+    /// The span to use for everything.
+    pub span: Span,
+    /// Body under construction.
+    pub body: ExprBody,
+    /// Block onto which we're adding statements. Its terminator is always `Return`.
+    pub current_block: BlockId,
+    /// Block to unwind to; created on demand.
+    pub unwind_block: Option<BlockId>,
+}
+
+fn mk_block(span: Span, term: TerminatorKind) -> BlockData {
+    BlockData {
+        statements: vec![],
+        terminator: Terminator::new(span, term),
+    }
+}
+
+impl BodyBuilder {
+    pub fn new(span: Span, arg_count: usize) -> Self {
+        let mut body: ExprBody = GExprBody {
+            span,
+            locals: Locals::new(arg_count),
+            comments: vec![],
+            body: Vector::new(),
+        };
+        let current_block = body.body.push(BlockData {
+            statements: Default::default(),
+            terminator: Terminator::new(span, TerminatorKind::Return),
+        });
+        Self {
+            span,
+            body,
+            current_block,
+            unwind_block: None,
+        }
+    }
+
+    /// Finalize the builder by returning the built body.
+    pub fn build(self) -> ExprBody {
+        self.body
+    }
+
+    /// Create a new local. Adds a `StorageLive` statement if the local is not one of the special
+    /// ones (return or function argument).
+    pub fn new_var(&mut self, name: Option<String>, ty: Ty) -> Place {
+        let place = self.body.locals.new_var(name, ty);
+        let local_id = place.as_local().unwrap();
+        if !self.body.locals.is_return_or_arg(local_id) {
+            self.push_statement(StatementKind::StorageLive(local_id));
+        }
+        place
+    }
+
+    /// Helper.
+    fn current_block(&mut self) -> &mut BlockData {
+        &mut self.body.body[self.current_block]
+    }
+
+    pub fn push_statement(&mut self, kind: StatementKind) {
+        let st = Statement::new(self.span, kind);
+        self.current_block().statements.push(st);
+    }
+
+    fn unwind_block(&mut self) -> BlockId {
+        *self.unwind_block.get_or_insert_with(|| {
+            self.body
+                .body
+                .push(mk_block(self.span, TerminatorKind::UnwindResume))
+        })
+    }
+
+    pub fn call(&mut self, call: Call) {
+        let next_block = self
+            .body
+            .body
+            .push(mk_block(self.span, TerminatorKind::Return));
+        let term = TerminatorKind::Call {
+            target: next_block,
+            call,
+            on_unwind: self.unwind_block(),
+        };
+        self.current_block().terminator.kind = term;
+        self.current_block = next_block;
+    }
+}

charon/src/bin/charon-driver/translate/get_mir.rs

@@ -42,17 +42,17 @@ impl ItemTransCtx<'_, '_> {
         let def_id = &item_ref.def_id;
         Ok(match get_mir_for_def_id_and_level(tcx, def_id, mir_level) {
             Some(body) => {
-                let state = self.hax_state_with_id();
+                let s = self.hax_state_with_id();
                 let body = if self.monomorphize() {
-                    let typing_env = state.typing_env();
-                    let args = item_ref.rustc_args(&state);
+                    let typing_env = s.typing_env();
+                    let args = item_ref.rustc_args(s);
                     hax::substitute(tcx, typing_env, Some(args), body)
                 } else {
                     body
                 };
                 // Here, we have to create a MIR state, which contains the body.
                 let body = Rc::new(body);
-                let state = state.with_mir(body.clone());
+                let state = s.with_mir(body.clone());
                 // Translate
                 let body: hax::MirBody<hax::mir_kinds::Unknown> =
                     self.t_ctx.catch_sinto(&state, span, body.as_ref())?;

charon/src/bin/charon-driver/translate/translate_closures.rs

@@ -44,6 +44,7 @@ use crate::translate::translate_bodies::BodyTransCtx;
 
 use super::translate_crate::TransItemSourceKind;
 use super::translate_ctx::*;
+use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
 use charon_lib::ast::*;
 use charon_lib::ids::Vector;
 use charon_lib::ullbc_ast::*;
@@ -350,14 +351,6 @@ impl ItemTransCtx<'_, '_> {
     ) -> Result<Result<Body, Opaque>, Error> {
         use ClosureKind::*;
         let closure_kind = translate_closure_kind(&args.kind);
-        let mk_stt = |content| Statement::new(span, content);
-        let mk_block = |statements, terminator| -> BlockData {
-            BlockData {
-                statements,
-                terminator: Terminator::new(span, terminator),
-            }
-        };
-
         Ok(match (target_kind, closure_kind) {
             (Fn, Fn) | (FnMut, FnMut) | (FnOnce, FnOnce) => {
                 // Translate the function's body normally
@@ -379,9 +372,8 @@ impl ItemTransCtx<'_, '_> {
                         } = body.as_unstructured_mut().unwrap();
 
                         blocks.dyn_visit_mut(|local: &mut LocalId| {
-                            let idx = local.index();
-                            if idx >= 2 {
-                                *local = LocalId::new(idx + 1)
+                            if local.index() >= 2 {
+                                *local += 1;
                             }
                         });
 
@@ -406,10 +398,14 @@ impl ItemTransCtx<'_, '_> {
                                 ),
                                 ty,
                             );
-                            mk_stt(StatementKind::Assign(
-                                locals.place_for_var(LocalId::new(i + 3)),
-                                Rvalue::Use(Operand::Move(nth_field)),
-                            ))
+                            let local_id = LocalId::new(i + 3);
+                            Statement::new(
+                                span,
+                                StatementKind::Assign(
+                                    locals.place_for_var(local_id),
+                                    Rvalue::Use(Operand::Move(nth_field)),
+                                ),
+                            )
                         });
                         blocks[BlockId::ZERO].statements.splice(0..0, new_stts);
 
@@ -467,49 +463,33 @@ impl ItemTransCtx<'_, '_> {
                     })),
                 });
 
-                let mut locals = Locals::new(2);
-                let mut statements = vec![];
-                let mut blocks = Vector::default();
+                let mut builder = BodyBuilder::new(span, 2);
 
-                let output = locals.new_var(None, signature.output.clone());
-                let state = locals.new_var(Some("state".to_string()), signature.inputs[0].clone());
-                let args = locals.new_var(Some("args".to_string()), signature.inputs[1].clone());
+                let output = builder.new_var(None, signature.output.clone());
+                let state = builder.new_var(Some("state".to_string()), signature.inputs[0].clone());
+                let args = builder.new_var(Some("args".to_string()), signature.inputs[1].clone());
                 let deref_state = state.deref();
                 let reborrow_ty =
                     TyKind::Ref(Region::Erased, deref_state.ty.clone(), RefKind::Shared).into_ty();
-                let reborrow = locals.new_var(None, reborrow_ty);
+                let reborrow = builder.new_var(None, reborrow_ty);
 
-                statements.push(mk_stt(StatementKind::Assign(
+                builder.push_statement(StatementKind::Assign(
                     reborrow.clone(),
                     // the state must be Sized, hence `()` as ptr-metadata
                     Rvalue::Ref {
                         place: deref_state,
                         kind: BorrowKind::Shared,
                         ptr_metadata: Operand::mk_const_unit(),
                     },
-                )));
-
-                let start_block = blocks.reserve_slot();
-                let ret_block = blocks.push(mk_block(vec![], TerminatorKind::Return));
-                let unwind_block = blocks.push(mk_block(vec![], TerminatorKind::UnwindResume));
-                let call = TerminatorKind::Call {
-                    target: ret_block,
-                    call: Call {
-                        func: fn_op,
-                        args: vec![Operand::Move(reborrow), Operand::Move(args)],
-                        dest: output,
-                    },
-                    on_unwind: unwind_block,
-                };
-                blocks.set_slot(start_block, mk_block(statements, call));
+                ));
 
-                let body: ExprBody = GExprBody {
-                    span,
-                    locals,
-                    comments: vec![],
-                    body: blocks,
-                };
-                Ok(Body::Unstructured(body))
+                builder.call(Call {
+                    func: fn_op,
+                    args: vec![Operand::Move(reborrow), Operand::Move(args)],
+                    dest: output,
+                });
+
+                Ok(Body::Unstructured(builder.build()))
             }
             (Fn, FnOnce) | (Fn, FnMut) | (FnMut, FnOnce) => {
                 panic!(
@@ -700,13 +680,6 @@ impl ItemTransCtx<'_, '_> {
             //   let args = (arg0, ..., argN);
             //   closure.call(args)
             // }
-            let mk_stt = |content| Statement::new(span, content);
-            let mk_block = |statements, terminator| -> BlockData {
-                BlockData {
-                    statements,
-                    terminator: Terminator::new(span, terminator),
-                }
-            };
             let fun_id: FunDeclId = self.register_item(
                 span,
                 def.this(),
@@ -718,55 +691,39 @@ impl ItemTransCtx<'_, '_> {
                 generics: impl_ref.generics.clone(),
             });
 
-            let mut locals = Locals::new(signature.inputs.len());
-            let mut statements = vec![];
-            let mut blocks = Vector::default();
+            let mut builder = BodyBuilder::new(span, signature.inputs.len());
 
-            let output = locals.new_var(None, signature.output.clone());
+            let output = builder.new_var(None, signature.output.clone());
             let args: Vec<Place> = signature
                 .inputs
                 .iter()
                 .enumerate()
-                .map(|(i, ty)| locals.new_var(Some(format!("arg{}", i + 1)), ty.clone()))
+                .map(|(i, ty)| builder.new_var(Some(format!("arg{}", i + 1)), ty.clone()))
                 .collect();
-            let args_tupled = locals.new_var(Some("args".to_string()), args_tuple_ty.clone());
-            let state = locals.new_var(Some("state".to_string()), state_ty.clone());
+            let args_tupled = builder.new_var(Some("args".to_string()), args_tuple_ty.clone());
+            let state = builder.new_var(Some("state".to_string()), state_ty.clone());
 
-            statements.push(mk_stt(StatementKind::Assign(
+            builder.push_statement(StatementKind::Assign(
                 args_tupled.clone(),
                 Rvalue::Aggregate(
                     AggregateKind::Adt(args_tuple_ty.as_adt().unwrap().clone(), None, None),
                     args.into_iter().map(Operand::Move).collect(),
                 ),
-            )));
+            ));
 
             let state_ty_adt = state_ty.as_adt().unwrap();
-            statements.push(mk_stt(StatementKind::Assign(
+            builder.push_statement(StatementKind::Assign(
                 state.clone(),
                 Rvalue::Aggregate(AggregateKind::Adt(state_ty_adt.clone(), None, None), vec![]),
-            )));
-
-            let start_block = blocks.reserve_slot();
-            let ret_block = blocks.push(mk_block(vec![], TerminatorKind::Return));
-            let unwind_block = blocks.push(mk_block(vec![], TerminatorKind::UnwindResume));
-            let call = TerminatorKind::Call {
-                target: ret_block,
-                call: Call {
-                    func: fn_op,
-                    args: vec![Operand::Move(state), Operand::Move(args_tupled)],
-                    dest: output,
-                },
-                on_unwind: unwind_block,
-            };
-            blocks.set_slot(start_block, mk_block(statements, call));
+            ));
 
-            let body: ExprBody = GExprBody {
-                span,
-                locals,
-                comments: vec![],
-                body: blocks,
-            };
-            Ok(Body::Unstructured(body))
+            builder.call(Call {
+                func: fn_op,
+                args: vec![Operand::Move(state), Operand::Move(args_tupled)],
+                dest: output,
+            });
+
+            Ok(Body::Unstructured(builder.build()))
         };
 
         Ok(FunDecl {

charon/src/bin/charon-driver/translate/translate_crate.rs

@@ -402,7 +402,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         kind: TransItemSourceKind,
     ) -> T {
         let item = if self.monomorphize() && item.has_param {
-            item.erase(&self.hax_state_with_id())
+            item.erase(self.hax_state_with_id())
         } else {
             item.clone()
         };