Make a seperate crate for CBMC (rust-lang#512)

Author: danielsn

Cargo.lock

@@ -455,6 +455,37 @@ dependencies = [
 name = "cargotest2"
 version = "0.1.0"
 
+[[package]]
+name = "cbmc"
+version = "0.0.0"
+dependencies = [
+ "bitflags",
+ "cstr",
+ "libc",
+ "measureme",
+ "num",
+ "rustc-demangle",
+ "rustc_arena",
+ "rustc_ast",
+ "rustc_attr",
+ "rustc_codegen_ssa",
+ "rustc_data_structures",
+ "rustc_errors",
+ "rustc_fs_util",
+ "rustc_hir",
+ "rustc_index",
+ "rustc_llvm",
+ "rustc_metadata",
+ "rustc_middle",
+ "rustc_serialize",
+ "rustc_session",
+ "rustc_span",
+ "rustc_target",
+ "smallvec",
+ "snap",
+ "tracing",
+]
+
 [[package]]
 name = "cc"
 version = "1.0.69"
@@ -3766,6 +3797,7 @@ name = "rustc_codegen_rmc"
 version = "0.0.0"
 dependencies = [
  "bitflags",
+ "cbmc",
  "cstr",
  "libc",
  "measureme",

compiler/cbmc/Cargo.toml

@@ -0,0 +1,38 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cbmc"
+version = "0.0.0"
+edition = "2018"
+
+[lib]
+test = true
+doctest = false
+
+[dependencies]
+bitflags = "1.0"
+cstr = "0.2"
+libc = "0.2"
+measureme = "9.1.0"
+num = "0.4.0"
+snap = "1"
+tracing = "0.1"
+rustc_middle = { path = "../rustc_middle" }
+rustc-demangle = "0.1.21"
+rustc_arena = { path = "../rustc_arena" }
+rustc_attr = { path = "../rustc_attr" }
+rustc_codegen_ssa = { path = "../rustc_codegen_ssa" }
+rustc_data_structures = { path = "../rustc_data_structures" }
+rustc_errors = { path = "../rustc_errors" }
+rustc_fs_util = { path = "../rustc_fs_util" }
+rustc_hir = { path = "../rustc_hir" }
+rustc_index = { path = "../rustc_index" }
+rustc_llvm = { path = "../rustc_llvm" }
+rustc_metadata = { path = "../rustc_metadata" }
+rustc_session = { path = "../rustc_session" }
+rustc_serialize = { path = "../rustc_serialize" }
+rustc_target = { path = "../rustc_target" }
+smallvec = { version = "1.6.1", features = ["union", "may_dangle"] }
+rustc_ast = { path = "../rustc_ast" }
+rustc_span = { path = "../rustc_span" }

compiler/rustc_codegen_rmc/src/cbmc/env.rs renamed to compiler/cbmc/src/env.rs

@@ -4,7 +4,7 @@
 use std::ops::{BitAnd, Shl, Shr};
 
 use super::super::Transformer;
-use crate::cbmc::goto_program::{
+use crate::goto_program::{
     BinaryOperand, CIntType, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, SymbolValues,
     Type,
 };

compiler/rustc_codegen_rmc/src/cbmc/goto_program/builtin.rs renamed to compiler/cbmc/src/goto_program/builtin.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use super::super::Transformer;
-use crate::cbmc::goto_program::{
+use crate::goto_program::{
     DatatypeComponent, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, Type,
 };
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};

compiler/rustc_codegen_rmc/src/cbmc/goto_program/expr.rs renamed to compiler/cbmc/src/goto_program/expr.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use super::super::Transformer;
-use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type};
+use crate::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use rustc_data_structures::fx::FxHashMap;
 
 /// Struct for handling the nondet transformations for --gen-c-runnable.

compiler/rustc_codegen_rmc/src/cbmc/goto_program/location.rs renamed to compiler/cbmc/src/goto_program/location.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use super::Transformer;
-use crate::cbmc::goto_program::SymbolTable;
+use crate::goto_program::SymbolTable;
 
 /// Struct for performing the identity transformation on a symbol table.
 /// Mainly used as a demo/for testing.

compiler/rustc_codegen_rmc/src/cbmc/goto_program/mod.rs renamed to compiler/cbmc/src/goto_program/mod.rs

@@ -3,7 +3,7 @@
 
 use super::gen_c_transformer::{ExprTransformer, NameTransformer, NondetTransformer};
 use super::identity_transformer::IdentityTransformer;
-use crate::cbmc::goto_program::SymbolTable;
+use crate::goto_program::SymbolTable;
 
 /// Performs each pass provided on the given symbol table.
 pub fn do_passes(mut symtab: SymbolTable, pass_names: &[String]) -> SymbolTable {

compiler/rustc_codegen_rmc/src/cbmc/goto_program/stmt.rs renamed to compiler/cbmc/src/goto_program/stmt.rs

@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::cbmc::goto_program::{
+use crate::goto_program::{
     BinaryOperand, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, SelfOperand,
     Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type, UnaryOperand,
 };

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symbol.rs renamed to compiler/cbmc/src/goto_program/symbol.rs

@@ -12,6 +12,7 @@ doctest = false
 
 [dependencies]
 bitflags = "1.0"
+cbmc = { path = "../cbmc" }
 cstr = "0.2"
 libc = "0.2"
 measureme = "9.1.0"

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symbol_table.rs renamed to compiler/cbmc/src/goto_program/symbol_table.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module defines functions which impose data invariant on generated data types.
 
-use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use rustc_middle::mir::interpret::{ConstValue, Scalar};
 use rustc_middle::ty;
 use rustc_middle::ty::layout::LayoutOf;

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs

@@ -3,7 +3,7 @@
 
 //! This file contains functions related to codegenning MIR blocks into gotoc
 
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
 
 impl<'tcx> GotocCtx<'tcx> {

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/gen_c_transformer/mod.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs

@@ -3,8 +3,8 @@
 
 //! This file contains functions related to codegenning MIR functions into gotoc
 
-use crate::cbmc::goto_program::{Expr, Stmt, Symbol};
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::{Expr, Stmt, Symbol};
 use rustc_middle::mir::{HasLocalDecls, Local};
 use rustc_middle::ty::{self, Instance, TyS};
 use tracing::{debug, warn};

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs

@@ -3,8 +3,8 @@
 //! this module handles intrinsics
 use tracing::{debug, warn};
 
-use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::mir::Place;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::Instance;

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs

@@ -15,3 +15,5 @@ mod span;
 mod statement;
 mod static_var;
 mod typ;
+
+pub use typ::TypeExt;

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/identity_transformer.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/identity_transformer.rs

@@ -1,8 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
-use crate::mir_to_goto::utils::slice_fat_ptr;
-use crate::mir_to_goto::GotocCtx;
+use crate::utils::slice_fat_ptr;
+use crate::GotocCtx;
+use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use rustc_ast::ast::Mutability;
 use rustc_middle::mir::interpret::{
     read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar,

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/mod.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/mod.rs

@@ -5,9 +5,10 @@
 //! a place is an expression of specifying a location in memory, like a left value. check the cases
 //! in [codegen_place] below.
 
-use crate::cbmc::goto_program::{Expr, Type};
-use crate::mir_to_goto::utils::slice_fat_ptr;
-use crate::mir_to_goto::GotocCtx;
+use super::typ::TypeExt;
+use crate::utils::slice_fat_ptr;
+use crate::GotocCtx;
+use cbmc::goto_program::{Expr, Type};
 use rustc_hir::Mutability;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::{

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/passes.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/passes.rs

@@ -1,12 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use super::typ::{is_pointer, pointee_type};
-use crate::btree_string_map;
-use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
-use crate::cbmc::utils::{aggr_name, BUG_REPORT_URL};
-use crate::cbmc::MachineModel;
-use crate::mir_to_goto::utils::{dynamic_fat_ptr, slice_fat_ptr};
-use crate::mir_to_goto::GotocCtx;
+use super::typ::{is_pointer, pointee_type, TypeExt};
+use crate::utils::{dynamic_fat_ptr, slice_fat_ptr};
+use crate::GotocCtx;
+use cbmc::btree_string_map;
+use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
+use cbmc::utils::{aggr_name, BUG_REPORT_URL};
+use cbmc::MachineModel;
 use num::bigint::BigInt;
 use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
 use rustc_middle::ty::adjustment::PointerCast;

compiler/rustc_codegen_rmc/src/cbmc/goto_program/symtab_transformer/transformer.rs renamed to compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs

@@ -3,8 +3,8 @@
 
 //! MIR Span related functions
 
-use crate::cbmc::goto_program::Location;
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::Location;
 use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
 use rustc_span::Span;
 

compiler/rustc_codegen_rmc/src/cbmc/goto_program/typ.rs renamed to compiler/cbmc/src/goto_program/typ.rs

@@ -1,8 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
-use crate::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{

compiler/rustc_codegen_rmc/src/cbmc/irep/from_irep.rs renamed to compiler/cbmc/src/irep/from_irep.rs

@@ -3,8 +3,8 @@
 
 //! This file contains functions related to codegenning MIR static variables into gotoc
 
-use crate::cbmc::goto_program::Symbol;
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::goto_program::Symbol;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::mono::MonoItem;
 use tracing::debug;

compiler/rustc_codegen_rmc/src/cbmc/irep/irep.rs renamed to compiler/cbmc/src/irep/irep.rs

@@ -1,9 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::btree_map;
-use crate::cbmc::goto_program::{DatatypeComponent, Expr, Parameter, Symbol, SymbolTable, Type};
-use crate::cbmc::utils::aggr_name;
-use crate::mir_to_goto::GotocCtx;
+use crate::GotocCtx;
+use cbmc::btree_map;
+use cbmc::goto_program::{DatatypeComponent, Expr, Parameter, Symbol, SymbolTable, Type};
+use cbmc::utils::aggr_name;
 use rustc_ast::ast::Mutability;
 use rustc_index::vec::IndexVec;
 use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue};
@@ -36,38 +36,82 @@ use ty::layout::HasParamEnv;
 const UNIT_TYPE_EMPTY_STRUCT_NAME: &str = "Unit";
 pub const FN_RETURN_VOID_VAR_NAME: &str = "VoidUnit";
 
-impl Type {
-    pub fn unit() -> Self {
+pub trait TypeExt {
+    fn is_rust_fat_ptr(&self, st: &SymbolTable) -> bool;
+    fn is_rust_slice_fat_ptr(&self, st: &SymbolTable) -> bool;
+    fn is_rust_trait_fat_ptr(&self, st: &SymbolTable) -> bool;
+    fn is_unit(&self) -> bool;
+    fn is_unit_pointer(&self) -> bool;
+    fn unit() -> Self;
+}
+
+impl TypeExt for Type {
+    fn is_rust_slice_fat_ptr(&self, st: &SymbolTable) -> bool {
+        match self {
+            Type::Struct { components, .. } => {
+                components.len() == 2
+                    && components.iter().any(|x| x.name() == "data" && x.typ().is_pointer())
+                    && components.iter().any(|x| x.name() == "len" && x.typ().is_integer())
+            }
+            Type::StructTag(tag) => st.lookup(tag).unwrap().typ.is_rust_slice_fat_ptr(st),
+            _ => false,
+        }
+    }
+
+    fn is_rust_trait_fat_ptr(&self, st: &SymbolTable) -> bool {
+        match self {
+            Type::Struct { components, .. } => {
+                components.len() == 2
+                    && components.iter().any(|x| x.name() == "data" && x.typ().is_pointer())
+                    && components.iter().any(|x| x.name() == "vtable" && x.typ().is_pointer())
+            }
+            Type::StructTag(tag) => st.lookup(tag).unwrap().typ.is_rust_trait_fat_ptr(st),
+            _ => false,
+        }
+    }
+
+    fn is_rust_fat_ptr(&self, st: &SymbolTable) -> bool {
+        self.is_rust_slice_fat_ptr(st) || self.is_rust_trait_fat_ptr(st)
+    }
+
+    fn unit() -> Self {
         // We depend on GotocCtx::codegen_ty_unit() to put the type in the symbol table.
         // We don't have access to the symbol table here to do it ourselves.
         Type::struct_tag(UNIT_TYPE_EMPTY_STRUCT_NAME)
     }
 
-    pub fn is_unit(&self) -> bool {
+    fn is_unit(&self) -> bool {
         match self {
             Type::StructTag(name) => *name == aggr_name(UNIT_TYPE_EMPTY_STRUCT_NAME),
             _ => false,
         }
     }
 
-    pub fn is_unit_pointer(&self) -> bool {
+    fn is_unit_pointer(&self) -> bool {
         match self {
             Type::Pointer { typ } => typ.is_unit(),
             _ => false,
         }
     }
 }
+trait ExprExt {
+    fn unit(symbol_table: &SymbolTable) -> Self;
+
+    fn is_unit(&self) -> bool;
+
+    fn is_unit_pointer(&self) -> bool;
+}
 
-impl Expr {
-    pub fn unit(symbol_table: &SymbolTable) -> Self {
+impl ExprExt for Expr {
+    fn unit(symbol_table: &SymbolTable) -> Self {
         Expr::struct_expr(Type::unit(), btree_map![], symbol_table)
     }
 
-    pub fn is_unit(&self) -> bool {
+    fn is_unit(&self) -> bool {
         self.typ().is_unit()
     }
 
-    pub fn is_unit_pointer(&self) -> bool {
+    fn is_unit_pointer(&self) -> bool {
         self.typ().is_unit_pointer()
     }
 }

compiler/rustc_codegen_rmc/src/cbmc/irep/irep_id.rs renamed to compiler/cbmc/src/irep/irep_id.rs

@@ -3,11 +3,11 @@
 
 //! This file contains the code necessary to interface with the compiler backend
 
-use crate::cbmc::goto_program::symtab_transformer;
-use crate::cbmc::goto_program::SymbolTable;
-use crate::mir_to_goto::overrides::skip_monomorphize;
-use crate::mir_to_goto::GotocCtx;
+use crate::overrides::skip_monomorphize;
+use crate::GotocCtx;
 use bitflags::_core::any::Any;
+use cbmc::goto_program::symtab_transformer;
+use cbmc::goto_program::SymbolTable;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorReported;