Late toolchain upgrade to use nightly-2022-08-02

cprover_bindings/src/goto_program/expr.rs

@@ -484,7 +484,7 @@ impl Expr {
 
     /// `(typ) self`.
     pub fn cast_to(self, typ: Type) -> Self {
-        assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?}\n\n{:?}", self, typ);
+        assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?} ({:?})\n\n{:?}", self, self.typ, typ);
         if self.typ == typ {
             self
         } else if typ.is_bool() {

kani-compiler/src/codegen_cprover_gotoc/archive.rs

@@ -20,7 +20,7 @@ use std::fs::File;
 use std::io::{self, Read, Seek};
 use std::path::{Path, PathBuf};
 
-use rustc_codegen_ssa::back::archive::ArchiveBuilder;
+use rustc_codegen_ssa::back::archive::{ArchiveBuilder, ArchiveBuilderBuilder};
 use rustc_session::Session;
 
 use object::read::archive::ArchiveFile;
@@ -34,7 +34,6 @@ enum ArchiveEntry {
 
 pub(crate) struct ArArchiveBuilder<'a> {
     sess: &'a Session,
-    dst: PathBuf,
     use_gnu_style_archive: bool,
 
     src_archives: Vec<File>,
@@ -44,27 +43,18 @@ pub(crate) struct ArArchiveBuilder<'a> {
 }
 
 impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
-    fn new(sess: &'a Session, output: &Path) -> Self {
-        ArArchiveBuilder {
-            sess,
-            dst: output.to_path_buf(),
-            use_gnu_style_archive: sess.target.archive_format == "gnu",
-            src_archives: vec![],
-            entries: vec![],
-        }
-    }
-
     fn add_file(&mut self, file: &Path) {
         self.entries.push((
             file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
             ArchiveEntry::File(file.to_owned()),
         ));
     }
 
-    fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
-    where
-        F: FnMut(&str) -> bool + 'static,
-    {
+    fn add_archive(
+        &mut self,
+        archive_path: &Path,
+        mut skip: Box<dyn FnMut(&str) -> bool + 'static>,
+    ) -> std::io::Result<()> {
         let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
         let archive = ArchiveFile::parse(&read_cache).unwrap();
         let archive_index = self.src_archives.len();
@@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
         Ok(())
     }
 
-    fn build(mut self) -> bool {
+    fn build(mut self: Box<Self>, output: &Path) -> bool {
         enum BuilderKind {
             Bsd(ar::Builder<File>),
             Gnu(ar::GnuBuilder<File>),
@@ -122,7 +112,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
 
         let mut builder = if self.use_gnu_style_archive {
             BuilderKind::Gnu(ar::GnuBuilder::new(
-                File::create(&self.dst).unwrap_or_else(|err| {
+                File::create(&output).unwrap_or_else(|err| {
                     sess.fatal(&format!(
                         "error opening destination during archive building: {}",
                         err
@@ -131,7 +121,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
                 entries.iter().map(|(name, _)| name.clone()).collect(),
             ))
         } else {
-            BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
+            BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| {
                 sess.fatal(&format!("error opening destination during archive building: {}", err));
             })))
         };
@@ -150,13 +140,27 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
         std::mem::drop(builder);
         any_members
     }
+}
 
-    fn inject_dll_import_lib(
-        &mut self,
+pub(crate) struct ArArchiveBuilderBuilder;
+
+impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
+    fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder<'a> + 'a> {
+        Box::new(ArArchiveBuilder {
+            sess,
+            use_gnu_style_archive: sess.target.archive_format == "gnu",
+            src_archives: vec![],
+            entries: vec![],
+        })
+    }
+
+    fn create_dll_import_lib(
+        &self,
+        _sess: &Session,
         _lib_name: &str,
         _dll_imports: &[rustc_session::cstore::DllImport],
-        _tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
-    ) {
+        _tmpdir: &Path,
+    ) -> PathBuf {
         unimplemented!("injecting dll imports is not supported");
     }
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
-use super::typ::pointee_type;
+use super::typ::{self, pointee_type};
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{
@@ -35,6 +35,11 @@ struct SizeAlign {
     align: Expr,
 }
 
+enum VTableInfo {
+    Size,
+    Align,
+}
+
 impl<'tcx> GotocCtx<'tcx> {
     fn binop<F: FnOnce(Expr, Expr) -> Expr>(
         &mut self,
@@ -703,6 +708,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 assert!(self.place_ty(p).is_unit());
                 self.codegen_volatile_store(fargs, farg_types, loc)
             }
+            "vtable_size" => self.vtable_info(VTableInfo::Size, fargs, p, loc),
+            "vtable_align" => self.vtable_info(VTableInfo::Align, fargs, p, loc),
             "wrapping_add" => codegen_wrapping_op!(plus),
             "wrapping_mul" => codegen_wrapping_op!(mul),
             "wrapping_sub" => codegen_wrapping_op!(sub),
@@ -1201,6 +1208,26 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place(p, e)
     }
 
+    fn vtable_info(
+        &mut self,
+        info: VTableInfo,
+        mut fargs: Vec<Expr>,
+        place: &Place<'tcx>,
+        _loc: Location,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1, "vtable intrinsics expects one raw pointer argument");
+        let vtable_obj = fargs
+            .pop()
+            .unwrap()
+            .cast_to(self.codegen_ty_common_vtable().to_pointer())
+            .dereference();
+        let expr = match info {
+            VTableInfo::Size => vtable_obj.member(typ::VTABLE_SIZE_FIELD, &self.symbol_table),
+            VTableInfo::Align => vtable_obj.member(typ::VTABLE_ALIGN_FIELD, &self.symbol_table),
+        };
+        self.codegen_expr_to_place(place, expr)
+    }
+
     /// This function computes the size and alignment of a dynamically-sized type.
     /// The implementations follows closely the SSA implementation found in
     /// rustc_codegen_ssa::glue::size_and_align_of_dst.

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -379,6 +379,14 @@ impl<'tcx> GotocCtx<'tcx> {
                 let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
                 self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
             }
+            GlobalAlloc::VTable(ty, trait_ref) => {
+                // This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
+                // requires a bit more logic to get information about the allocation.
+                let alloc_id = self.tcx.vtable_allocation((ty, trait_ref));
+                let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
+                let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
+                self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
+            }
         };
         assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
         let offset_addr = base_addr

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -6,6 +6,7 @@
 //! in [GotocCtx::codegen_place] below.
 
 use super::typ::TypeExt;
+use crate::codegen_cprover_gotoc::codegen::typ::{pointee_type, std_pointee_type};
 use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Type};
@@ -360,31 +361,30 @@ impl<'tcx> GotocCtx<'tcx> {
                     before.goto_expr
                 };
 
-                let inner_mir_typ_and_mut = base_type.builtin_deref(true).unwrap();
-                let fat_ptr_mir_typ = if self.is_box_of_unsized(base_type) {
-                    // If we have a box, its fat pointer typ is a pointer to the boxes inner type.
-                    Some(self.tcx.mk_ptr(inner_mir_typ_and_mut))
-                } else if self.is_ref_of_unsized(base_type) {
-                    Some(before.mir_typ_or_variant.expect_type())
+                let inner_mir_typ = std_pointee_type(base_type).unwrap();
+                let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self.use_thin_pointer(inner_mir_typ) {
+                    (before.fat_ptr_mir_typ, before.fat_ptr_goto_expr)
                 } else {
-                    before.fat_ptr_mir_typ
+                    (Some(before.mir_typ_or_variant.expect_type()), Some(inner_goto_expr.clone()))
                 };
-                let fat_ptr_goto_expr =
-                    if self.is_box_of_unsized(base_type) || self.is_ref_of_unsized(base_type) {
-                        Some(inner_goto_expr.clone())
-                    } else {
-                        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)
+                            || fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table),
+                        "Unexpected type: {:?} -- {:?}",
+                        fat_ptr.typ(),
+                        pointee_type(fat_ptr_mir_typ.unwrap()).unwrap().kind(),
+                    );
+                    assert!(
+                        self.use_fat_pointer(pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()),
+                        "Unexpected type: {:?} -- {:?}",
+                        fat_ptr.typ(),
+                        fat_ptr_mir_typ,
                     );
                 };
 
-                let inner_mir_typ = inner_mir_typ_and_mut.ty;
                 let expr = match inner_mir_typ.kind() {
                     ty::Slice(_) | ty::Str | ty::Dynamic(..) => {
                         inner_goto_expr.member("data", &self.symbol_table)
@@ -547,13 +547,6 @@ impl<'tcx> GotocCtx<'tcx> {
                     self,
                 )
             }
-            ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
-                before.goto_expr.cast_to(self.codegen_ty(ty)),
-                TypeOrVariant::Type(ty),
-                before.fat_ptr_goto_expr,
-                before.fat_ptr_mir_typ,
-                self,
-            ),
         }
     }
 

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -43,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let left_typ = self.operand_ty(left_op);
         let right_typ = self.operand_ty(left_op);
         assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types");
-        assert!(self.is_ref_of_unsized(left_typ));
+        assert!(self.is_fat_pointer(left_typ));
 
         if self.is_vtable_fat_pointer(left_typ) {
             // Codegen an assertion failure since vtable comparison is not stable.
@@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
             BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
-                if self.is_ref_of_unsized(self.operand_ty(e1)) {
+                if self.is_fat_pointer(self.operand_ty(e1)) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
                 } else {
                     self.codegen_comparison(op, e1, e2)
@@ -628,11 +628,11 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         // Cast between fat pointers
-        if self.is_ref_of_unsized(src_t) && self.is_ref_of_unsized(dst_t) {
+        if self.is_fat_pointer(src_t) && self.is_fat_pointer(dst_t) {
             return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t);
         }
 
-        if self.is_ref_of_unsized(src_t) && self.is_ref_of_sized(dst_t) {
+        if self.is_fat_pointer(src_t) && !self.is_fat_pointer(dst_t) {
             return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t);
         }
 
@@ -760,14 +760,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 dst_mir_type,
             )
         } else {
-            // Check that the source is either not a pointer, or a thin or a slice pointer
-            assert!(
-                pointee_type(src_mir_type)
-                    .map_or(true, |p| self.use_thin_pointer(p) || self.use_slice_fat_pointer(p))
-            );
-
-            // Sized to unsized cast
-            self.cast_sized_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
+            // Recursively cast the source expression into an unsized expression.
+            // This will include thin pointers, slices, and Adt.
+            self.cast_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
         }
     }
 
@@ -1041,10 +1036,9 @@ impl<'tcx> GotocCtx<'tcx> {
         Some(dynamic_fat_ptr(dst_goto_type, data, vtable, &self.symbol_table))
     }
 
-    /// Cast a sized object to an unsized object: the result of the cast will be
-    /// a fat pointer or an ADT with a nested fat pointer.  Return the result of
-    /// the cast as Some(expr) and return None if no cast was required.
-    fn cast_sized_expr_to_unsized_expr(
+    /// Cast an object / thin pointer to a fat pointer or an ADT with a nested fat pointer.
+    /// Return the result of the cast as Some(expr) and return None if no cast was required.
+    fn cast_expr_to_unsized_expr(
         &mut self,
         src_goto_expr: Expr,
         src_mir_type: Ty<'tcx>,
@@ -1054,19 +1048,6 @@ impl<'tcx> GotocCtx<'tcx> {
             return None; // no cast required, nothing to do
         }
 
-        // The src type will be sized, but the dst type may not be unsized.  If
-        // the dst is an adt containing a pointer to a trait object nested
-        // within the adt, the trait object will be unsized and the pointer will
-        // be a fat pointer, but the adt (containing the fat pointer) will
-        // itself be sized.
-        assert!(
-            src_mir_type.is_sized(self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all())
-        );
-
-        // The src type cannot be a pointer to a dynamic trait object, otherwise
-        // we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
-        assert!(!self.is_vtable_fat_pointer(src_mir_type));
-
         match (src_mir_type.kind(), dst_mir_type.kind()) {
             (ty::Ref(..), ty::Ref(..)) => {
                 self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
@@ -1081,7 +1062,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
             }
             (ty::Adt(..), ty::Adt(..)) => {
-                self.cast_sized_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
+                self.cast_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
             }
             (src_kind, dst_kind) => {
                 unreachable!(
@@ -1095,6 +1076,11 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Cast a pointer to a sized object to a fat pointer to an unsized object.
     /// Return the result of the cast as Some(expr) and return None if no cast
     /// was required.
+    /// Note: This seems conceptually wrong. If we are converting sized to unsized, how come
+    /// source and destination can have the same type? Also, how come destination can be a thin
+    /// pointer?
+    /// TODO: Fix the cast code structure:
+    /// <https://github.com/model-checking/kani/issues/1531>
     fn cast_sized_pointer_to_fat_pointer(
         &mut self,
         src_goto_expr: Expr,
@@ -1106,6 +1092,10 @@ impl<'tcx> GotocCtx<'tcx> {
             return None;
         };
 
+        // The src type cannot be a pointer to a dynamic trait object, otherwise
+        // we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
+        assert!(!self.is_vtable_fat_pointer(src_mir_type));
+
         // extract pointee types from pointer types, panic if type is not a
         // pointer type.
         let src_pointee_type = pointee_type(src_mir_type).unwrap();
@@ -1192,10 +1182,10 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    /// Cast a sized ADT to an unsized ADT (an ADT with a nested fat pointer).
+    /// Cast an ADT (sized or unsized) to an unsized ADT (an ADT with a nested fat pointer).
     /// Return the result of the cast as Some(expr) and return None if no cast
     /// was required.
-    fn cast_sized_adt_to_unsized_adt(
+    fn cast_adt_to_unsized_adt(
         &mut self,
         src_goto_expr: Expr,
         src_mir_type: Ty<'tcx>,

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     | InstanceDef::DropGlue(_, Some(_))
                     | InstanceDef::Intrinsic(..)
                     | InstanceDef::FnPtrShim(..)
-                    | InstanceDef::VtableShim(..)
+                    | InstanceDef::VTableShim(..)
                     | InstanceDef::ReifyShim(..)
                     | InstanceDef::ClosureOnceShim { .. }
                     | InstanceDef::CloneShim(..) => {