Handle boxed closures as arguments (fix RMC std lib crash) (rust-lang#278)

* Support boxed closures

* More comments

* Review comments

* Whitespace and test typo

* Cleanup

Author: avanhatt

Diff for: compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

@@ -453,7 +453,6 @@ impl<'tcx> GotocCtx<'tcx> {
             "prefetch_read_instruction" => unimplemented!(),
             "prefetch_write_data" => unimplemented!(),
             "prefetch_write_instruction" => unimplemented!(),
-            "try" => unimplemented!(),
             "unaligned_volatile_store" => unimplemented!(),
             "va_arg" => unimplemented!(),
             "va_copy" => unimplemented!(),

Diff for: compiler/rustc_codegen_llvm/src/gotoc/mod.rs

@@ -105,14 +105,8 @@ impl<'tcx> GotocCtx<'tcx> {
             x if x.ends_with("__getit") => true,
             // https://github.com/model-checking/rmc/issues/205
             "panic::Location::<'a>::caller" => true,
-            // https://github.com/model-checking/rmc/issues/206
-            "core::sync::atomic::atomic_swap" => true,
             // https://github.com/model-checking/rmc/issues/207
             "core::slice::<impl [T]>::split_first" => true,
-            // https://github.com/model-checking/rmc/issues/208
-            "panicking::take_hook" => true,
-            // https://github.com/model-checking/rmc/issues/209
-            "panicking::r#try" => true,
             _ => false,
         }
     }

Diff for: compiler/rustc_codegen_llvm/src/gotoc/operand.rs

@@ -28,7 +28,16 @@ impl<'tcx> GotocCtx<'tcx> {
             Operand::Copy(d) | Operand::Move(d) =>
             // TODO: move shouldn't be the same as copy
             {
-                self.codegen_place(d).goto_expr
+                let projection = self.codegen_place(d);
+                // If the operand itself is a Dynamic (like when passing a boxed closure),
+                // we need to pull off the fat pointer. In that case, the rustc kind() on
+                // both the operand and the inner type are Dynamic.
+                // Consider moving this check elsewhere in:
+                // https://github.com/model-checking/rmc/issues/277
+                match self.operand_ty(o).kind() {
+                    ty::Dynamic(..) => projection.fat_ptr_goto_expr.unwrap(),
+                    _ => projection.goto_expr,
+                }
             }
             Operand::Constant(c) => self.codegen_constant(&c),
         }

Diff for: compiler/rustc_codegen_llvm/src/gotoc/place.rs

@@ -13,7 +13,7 @@ use rustc_middle::{
     ty::{self, Ty, TyS, VariantDef},
 };
 use rustc_target::abi::{LayoutOf, TagEncoding, Variants};
-use tracing::debug;
+use tracing::{debug, warn};
 
 /// A projection in RMC can either be to a type (the normal case),
 /// or a variant in the case of a downcast.
@@ -63,7 +63,7 @@ impl<'tcx> ProjectedPlace<'tcx> {
 
 /// Constructor
 impl<'tcx> ProjectedPlace<'tcx> {
-    fn _check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool {
+    fn check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool {
         match typ {
             TypeOrVariant::Type(t) => &ctx.codegen_ty(t) == expr.typ(),
             TypeOrVariant::Variant(_) => true, //TODO, what to do here?
@@ -102,12 +102,14 @@ impl<'tcx> ProjectedPlace<'tcx> {
         }
         // TODO: these assertions fail on a few regressions. Figure out why.
         // I think it may have to do with boxed fat pointers.
-        // assert!(
-        //     Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx),
-        //     "\n{:?}\n{:?}",
-        //     &goto_expr,
-        //     &mir_typ_or_variant
-        // );
+        // https://github.com/model-checking/rmc/issues/277
+        if !Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx) {
+            warn!(
+                "Unexpected type mismatch in projection: \n{:?}\n{:?}",
+                &goto_expr, &mir_typ_or_variant
+            );
+        };
+
         assert!(
             Self::check_fat_ptr_typ(&fat_ptr_goto_expr, &fat_ptr_mir_typ, ctx),
             "\n{:?}\n{:?}",
@@ -252,6 +254,14 @@ impl<'tcx> GotocCtx<'tcx> {
                         before.fat_ptr_goto_expr
                     };
 
+                // Check that we have a valid trait or slice fat pointer
+                if let Some(fat_ptr) = fat_ptr_goto_expr.clone() {
+                    assert!(
+                        fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)
+                            || fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table)
+                    );
+                };
+
                 let inner_mir_typ = inner_mir_typ_and_mut.ty;
                 let expr = match inner_mir_typ.kind() {
                     ty::Slice(_) | ty::Str | ty::Dynamic(..) => {

Diff for: compiler/rustc_codegen_llvm/src/gotoc/statement.rs

@@ -3,6 +3,7 @@
 use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use super::metadata::*;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
+use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
     BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
@@ -276,79 +277,101 @@ impl<'tcx> GotocCtx<'tcx> {
 
                 let (p, target) = destination.unwrap();
 
-                if let ty::InstanceDef::DropGlue(_, None) = instance.def {
-                    // here an empty drop glue is invoked. we just ignore it.
-                    return Stmt::goto(self.current_fn().find_label(&target), Location::none());
-                }
-
-                // Handle the case of a virtual function call via vtable lookup.
-                let mut stmts = if let InstanceDef::Virtual(def_id, size) = instance.def {
-                    debug!(
-                        "Codegen a call through a virtual function. def_id: {:?} size: {:?}",
-                        def_id, size
-                    );
-
-                    // The first argument to a virtual function is a fat pointer for the trait
-                    let trait_fat_ptr = fargs[0].to_owned();
-                    let vtable_field_name = self.vtable_field_name(def_id);
-
-                    // Now that we have all the stuff we need, we can actually build the dynamic call
-                    // If the original call was of the form
-                    // f(arg0, arg1);
-                    // The new call should be of the form
-                    // arg0.vtable->f(arg0.data,arg1);
-                    let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table);
-                    let vtable = vtable_ref.dereference();
-                    let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table);
-
-                    // Update the argument from arg0 to arg0.data
-                    fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
+                let mut stmts: Vec<Stmt> = match instance.def {
+                    // Here an empty drop glue is invoked; we just ignore it.
+                    InstanceDef::DropGlue(_, None) => {
+                        return Stmt::goto(self.current_fn().find_label(&target), Location::none());
+                    }
+                    // Handle a virtual function call via a vtable lookup
+                    InstanceDef::Virtual(def_id, _) => {
+                        // We must have at least one argument, and the first one
+                        // should be a fat pointer for the trait
+                        let trait_fat_ptr = fargs[0].to_owned();
 
-                    // For soundness, add an assertion that the vtable function call is not null.
-                    // Otherwise, CBMC might treat this as an assert(0) and later user-added assertions
-                    // could be vacuously true.
-                    let call_is_nonnull = fn_ptr.clone().is_nonnull();
-                    let assert_msg =
-                        format!("Non-null virtual function call for {:?}", vtable_field_name);
-                    let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone());
+                        //Check the Gotoc-level fat pointer type
+                        assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table));
 
-                    // Virtual function call and corresponding nonnull assertion.
-                    let func_exp: Expr = fn_ptr.dereference();
-                    vec![
-                        assert_nonnull,
-                        self.codegen_expr_to_place(&p, func_exp.call(fargs))
-                            .with_location(loc.clone()),
-                    ]
-                } else {
-                    // Non-virtual function call.
-                    let func_exp = self.codegen_operand(func);
-                    vec![
-                        self.codegen_expr_to_place(&p, func_exp.call(fargs))
-                            .with_location(loc.clone()),
-                    ]
+                        self.codegen_virtual_funcall(
+                            trait_fat_ptr,
+                            def_id,
+                            &p,
+                            &mut fargs,
+                            loc.clone(),
+                        )
+                    }
+                    // Normal, non-virtual function calls
+                    InstanceDef::Item(..)
+                    | InstanceDef::DropGlue(_, Some(_))
+                    | InstanceDef::Intrinsic(..)
+                    | InstanceDef::FnPtrShim(.., _)
+                    | InstanceDef::VtableShim(..)
+                    | InstanceDef::ReifyShim(..)
+                    | InstanceDef::ClosureOnceShim { call_once: _ }
+                    | InstanceDef::CloneShim(..) => {
+                        let func_exp = self.codegen_operand(func);
+                        vec![
+                            self.codegen_expr_to_place(&p, func_exp.call(fargs))
+                                .with_location(loc.clone()),
+                        ]
+                    }
                 };
-
-                // Add return jump.
                 stmts.push(Stmt::goto(self.current_fn().find_label(&target), loc.clone()));
-
-                // Produce the full function call block.
-                Stmt::block(stmts, loc)
+                return Stmt::block(stmts, loc);
             }
+            // Function call through a pointer
             ty::FnPtr(_) => {
                 let (p, target) = destination.unwrap();
                 let func_expr = self.codegen_operand(func).dereference();
-                // Actually generate the function call, and store the return value, if any.
-                Stmt::block(
+                // Actually generate the function call and return.
+                return Stmt::block(
                     vec![
                         self.codegen_expr_to_place(&p, func_expr.call(fargs))
                             .with_location(loc.clone()),
                         Stmt::goto(self.current_fn().find_label(&target), loc.clone()),
                     ],
                     loc,
-                )
+                );
             }
             x => unreachable!("Function call where the function was of unexpected type: {:?}", x),
-        }
+        };
+    }
+
+    fn codegen_virtual_funcall(
+        &mut self,
+        trait_fat_ptr: Expr,
+        def_id: DefId,
+        place: &Place<'tcx>,
+        fargs: &mut Vec<Expr>,
+        loc: Location,
+    ) -> Vec<Stmt> {
+        let vtable_field_name = self.vtable_field_name(def_id);
+
+        // Now that we have all the stuff we need, we can actually build the dynamic call
+        // If the original call was of the form
+        // f(arg0, arg1);
+        // The new call should be of the form
+        // arg0.vtable->f(arg0.data,arg1);
+        let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table);
+        let vtable = vtable_ref.dereference();
+        let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table);
+
+        // Update the argument from arg0 to arg0.data
+        fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
+
+        // For soundness, add an assertion that the vtable function call is not null.
+        // Otherwise, CBMC might treat this as an assert(0) and later user-added assertions
+        // could be vacuously true.
+        let call_is_nonnull = fn_ptr.clone().is_nonnull();
+        let assert_msg = format!("Non-null virtual function call for {:?}", vtable_field_name);
+        let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone());
+
+        // Virtual function call and corresponding nonnull assertion.
+        let func_exp: Expr = fn_ptr.dereference();
+        vec![
+            assert_nonnull,
+            self.codegen_expr_to_place(place, func_exp.call(fargs.to_vec()))
+                .with_location(loc.clone()),
+        ]
     }
 
     /// A place is similar to the C idea of a LHS. For example, the returned value of a function call is stored to a place.

Diff for: compiler/rustc_codegen_llvm/src/gotoc/typ.rs

@@ -970,12 +970,11 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    /// whether a variable of type ty should be ignored
+    /// Whether a variable of type ty should be ignored as a parameter to a function
     pub fn ignore_var_ty(&self, ty: Ty<'tcx>) -> bool {
         match ty.kind() {
             ty::Tuple(substs) if substs.is_empty() => true,
             ty::FnDef(_, _) => true,
-            ty::Dynamic(_, _) => true, //DSN understand why
             _ => false,
         }
     }

Diff for: src/test/cbmc/DynTrait/boxed_closure.rs

@@ -0,0 +1,12 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can codegen a boxed dyn closure
+
+fn main() {
+    // Create a boxed once-callable closure
+    let f: Box<dyn FnOnce(i32)> = Box::new(|x| assert!(x == 1));
+
+    // Call it
+    f(1);
+}

Diff for: src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can codegen a boxed dyn closure and fail an inner assertion
+
+// This current verifies "successfully" because the closure is not actually
+// called in the resulting CotoC code.
+// https://github.com/model-checking/rmc/issues/240
+
+fn main() {
+    // Create a boxed once-callable closure
+    let f: Box<dyn FnOnce()> = Box::new(|x| {
+        __VERIFIER_expect_fail(x == 2, "Wrong int");
+    });
+
+    // Call it
+    f(1);
+}

Diff for: src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs

@@ -13,7 +13,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) {
     let x = fun();
     __VERIFIER_expect_fail(x != 5, "Wrong return");
     /* The closure captures `a` and thus is sized */
-    __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) == 8, "Wrong size");
+    __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 8, "Wrong size");
 }
 
 fn main() {