Add vtable well-formedness flag

This is a temporary workaround for the vtable duplicate field issue (rust-lang#30).
Since we can detect this case at translation time, we mark the vtable as
ill-formed. This is checked at proof-time so any code that relies on using an
ill-formed vtable function will fail.

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 2 people

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs

@@ -630,10 +630,24 @@ impl Type {
         StructTag(aggr_name(name))
     }
 
+    pub fn components_are_unique(components: &Vec<DatatypeComponent>) -> bool {
+        let mut names: Vec<_> = components.iter().map(|x| x.name()).collect();
+        names.sort();
+        names.dedup();
+        names.len() == components.len()
+    }
+
     /// struct name {
     ///     f1.typ f1.data; ...
     /// }
     pub fn struct_type(name: &str, components: Vec<DatatypeComponent>) -> Self {
+        // TODO: turn this on after fixing issue #30
+        // <https://github.com/model-checking/rmc/issues/30>
+        //assert!(
+        //    Type::components_are_unique(&components),
+        //    "Components contain duplicates: {:?}",
+        //    components
+        //);
         Struct { tag: name.to_string(), components }
     }
 
@@ -646,6 +660,11 @@ impl Type {
     ///     f1.typ f1.data; ...
     /// }
     pub fn union_type(name: &str, components: Vec<DatatypeComponent>) -> Self {
+        assert!(
+            Type::components_are_unique(&components),
+            "Components contain duplicates: {:?}",
+            components
+        );
         Union { tag: name.to_string(), components }
     }
 

compiler/rustc_codegen_llvm/src/gotoc/metadata.rs

@@ -24,6 +24,10 @@ use std::iter;
 use std::path::Path;
 use tracing::debug;
 
+// TODO: this is a temporary RMC-only flag used in vtables for issue #30
+// <https://github.com/model-checking/rmc/issues/30>
+pub static VTABLE_IS_WELL_FORMED_FIELD: &str = "is_vtable_well_formed";
+
 // #[derive(RustcEncodable, RustcDecodable)]
 pub struct GotocCodegenResult {
     pub symtab: SymbolTable,

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

@@ -884,13 +884,22 @@ impl<'tcx> GotocCtx<'tcx> {
             Location::none(),
             |ctx, var| {
                 // Build the vtable
+                // See compiler/rustc_codegen_llvm/src/gotoc/typ.rs `trait_vtable_field_types` for field order
                 let drop_irep = ctx.codegen_vtable_drop_in_place();
                 let (vt_size, vt_align) = ctx.codegen_vtable_size_and_align(&src_mir_type);
                 let mut vtable_fields = vec![drop_irep, vt_size, vt_align];
                 let concrete_type =
                     binders.principal().unwrap().with_self_ty(ctx.tcx, src_mir_type);
                 let mut methods = ctx.codegen_vtable_methods(concrete_type, trait_type);
                 vtable_fields.append(&mut methods);
+                let fields = ctx
+                    .symbol_table
+                    .lookup_fields_in_type(&Type::struct_tag(&vtable_name))
+                    .unwrap();
+                // TODO: this is a temporary RMC-only flag for issue #30
+                // <https://github.com/model-checking/rmc/issues/30>
+                let is_well_formed = Expr::c_bool_constant(Type::components_are_unique(fields));
+                vtable_fields.push(is_well_formed);
                 let vtable = Expr::struct_expr_from_values(
                     Type::struct_tag(&vtable_name),
                     vtable_fields,

compiler/rustc_codegen_llvm/src/gotoc/statement.rs

@@ -275,6 +275,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // TODO is there a better way to do this without needing the mut?
                 let mut funce = self.codegen_operand(func);
 
+                let mut stmts: Vec<Stmt> = vec![];
                 if let InstanceDef::Virtual(def_id, size) = instance.def {
                     debug!(
                         "Codegen a call through a virtual function. def_id: {:?} size: {:?}",
@@ -292,18 +293,29 @@ impl<'tcx> GotocCtx<'tcx> {
                     // 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);
+                    let fn_ptr = vtable.clone().member(&vtable_field_name, &self.symbol_table);
                     funce = fn_ptr.dereference();
 
                     //Update the argument from arg0 to arg0.data
                     fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
+
+                    // TODO: this is a temporary RMC-only flag for issue 30
+                    // <https://github.com/model-checking/rmc/issues/30>
+                    let is_well_formed = vtable
+                        .clone()
+                        .member(VTABLE_IS_WELL_FORMED_FIELD, &self.symbol_table)
+                        .cast_to(Type::bool());
+                    let assert_msg = format!("well formed vtable for type {:?}", &vtable.typ());
+                    let assert = Stmt::assert(is_well_formed, &assert_msg, loc.clone());
+                    stmts.push(assert);
                 }
 
                 // Actually generate the function call, and store the return value, if any.
-                Stmt::block(vec![
+                stmts.append(&mut vec![
                     self.codegen_expr_to_place(&p, funce.call(fargs)).with_location(loc.clone()),
                     Stmt::goto(self.find_label(&target), loc),
-                ])
+                ]);
+                Stmt::block(stmts)
             }
             ty::FnPtr(_) => {
                 let (p, target) = destination.unwrap();

compiler/rustc_codegen_llvm/src/gotoc/typ.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::cbmc::goto_program::{DatatypeComponent, Expr, Symbol, SymbolTable, Type};
 use super::cbmc::utils::aggr_name;
-use super::metadata::GotocCtx;
+use super::metadata::{GotocCtx, VTABLE_IS_WELL_FORMED_FIELD};
 use crate::btree_map;
 use rustc_ast::ast::Mutability;
 use rustc_index::vec::IndexVec;
@@ -138,6 +138,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ///      size_t align;
     ///      int (*f)(int) f1;
     ///      ...
+    ///      bool is_well_formed; //< TODO: this is a temporary RMC-only flag for issue #30
+    ///                           // <https://github.com/model-checking/rmc/issues/30>
     ///   }
     /// Ensures that the vtable is added to the symbol table.
     fn codegen_trait_vtable_type(&mut self, t: &'tcx ty::TyS<'tcx>) -> Type {
@@ -162,7 +164,13 @@ impl<'tcx> GotocCtx<'tcx> {
         })
     }
 
-    /// Given a trait of type `t`, determine the fields of the struct that will implement it's vtable.
+    /// Given a trait of type `t`, determine the fields of the struct that will implement its vtable.
+    ///
+    /// The order of fields (i.e., the layout of a vtable) is not guaranteed by the compiler.
+    /// We follow the order implemented by the compiler in compiler/rustc_codegen_ssa/src/meth.rs
+    /// `get_vtable`.
+    ///
+    /// Currently, we also add a well-formed flag field to the end of the struct.
     fn trait_vtable_field_types(&mut self, t: &'tcx ty::TyS<'tcx>) -> Vec<DatatypeComponent> {
         if let ty::Dynamic(binder, _region) = t.kind() {
             // the virtual methods on the trait ref
@@ -183,6 +191,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 Type::datatype_component("align", Type::size_t()),
             ];
             vtable_base.append(&mut flds);
+            // TODO: this is a temporary RMC-only flag for issue #30
+            // <https://github.com/model-checking/rmc/issues/30>
+            vtable_base.push(Type::datatype_component(VTABLE_IS_WELL_FORMED_FIELD, Type::c_bool()));
             vtable_base
         } else {
             unreachable!("Expected to get a dynamic object here");

rust-tests/cbmc-reg/DynTrait/vtable_duplicate_fields_fixme.rs

@@ -0,0 +1,47 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+trait A {
+    fn foo(&self) -> i32;
+}
+
+trait B {
+    fn foo(&self) -> i32;
+}
+
+trait T: A + B {}
+
+struct S {
+    x: i32,
+    y: i32,
+}
+
+impl S {
+    fn new(a: i32, b: i32) -> S {
+        S { x: a, y: b }
+    }
+    fn new_box(a: i32, b: i32) -> Box<dyn T> {
+        Box::new(S::new(a, b))
+    }
+}
+
+impl A for S {
+    fn foo(&self) -> i32 {
+        self.x
+    }
+}
+
+impl B for S {
+    fn foo(&self) -> i32 {
+        self.y
+    }
+}
+
+impl T for S {}
+
+fn main() {
+    let t = S::new_box(1, 2);
+    let a = <dyn T as A>::foo(&*t);
+    assert!(a == 1);
+    let b = <dyn T as B>::foo(&*t);
+    assert!(b == 2);
+}