Add support to typedef in cprover bindings crate (rust-lang#1035)

* Add support to typedef in cprover bindings crate

* Address comments + more tests

Author: celinval

cprover_bindings/src/goto_program/expr.rs

@@ -303,6 +303,8 @@ impl Expr {
     /// that don't appear in the standard, like `bool`
     /// https://docs.microsoft.com/en-us/cpp/c-language/type-cast-conversions?view=msvc-160
     pub fn can_cast_from(source: &Type, target: &Type) -> bool {
+        let source = source.unwrap_typedef();
+        let target = target.unwrap_typedef();
         if source == target {
             true
         } else if target.is_bool() {

cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs

@@ -38,39 +38,14 @@ impl Transformer for IdentityTransformer {
 mod tests {
     use super::{
         super::super::{
-            super::{MachineModel, RoundingMode},
             DatatypeComponent, Expr, Location, Stmt, SwitchCase, Symbol, SymbolTable, Type,
         },
         IdentityTransformer,
     };
-    fn default_machine_model() -> MachineModel {
-        MachineModel::new(
-            1,
-            "x86_64",
-            8,
-            false,
-            8,
-            64,
-            32,
-            32,
-            false,
-            128,
-            64,
-            64,
-            4,
-            true,
-            64,
-            RoundingMode::ToNearest,
-            16,
-            32,
-            false,
-            32,
-            32,
-        )
-    }
+    use crate::machine_model::test_util::machine_model_test_stub;
 
     fn empty_symtab() -> SymbolTable {
-        SymbolTable::new(default_machine_model())
+        SymbolTable::new(machine_model_test_stub())
     }
 
     fn assert_transform_eq(original: SymbolTable) {

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -58,6 +58,7 @@ pub trait Transformer: Sized {
             Type::Signedbv { width } => self.transform_type_signedbv(width),
             Type::Struct { tag, components } => self.transform_type_struct(*tag, components),
             Type::StructTag(tag) => self.transform_type_struct_tag(*tag),
+            Type::TypeDef { name: tag, typ } => self.transform_type_def(*tag, typ),
             Type::Union { tag, components } => self.transform_type_union(*tag, components),
             Type::UnionTag(tag) => self.transform_type_union_tag(*tag),
             Type::Unsignedbv { width } => self.transform_type_unsignedbv(width),
@@ -232,6 +233,12 @@ pub trait Transformer: Sized {
         Type::vector(transformed_typ, *size)
     }
 
+    /// Transforms a type def (`typedef typ tag`)
+    fn transform_type_def(&mut self, tag: InternedString, typ: &Box<Type>) -> Type {
+        let transformed_typ = self.transform_type(typ.as_ref());
+        transformed_typ.to_typedef(tag)
+    }
+
     /// Perform recursive descent on a `Expr` data structure.
     /// Extracts the variant's field data, and passes them into
     /// the corresponding expr transformer method along with the expr type.