Symbol table transformer (#321)

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

Author: vecchiot-aws

compiler/rustc_codegen_llvm/Cargo.toml

@@ -4,7 +4,7 @@ version = "0.0.0"
 edition = "2018"
 
 [lib]
-test = false
+test = true
 doctest = false
 
 [dependencies]

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

@@ -584,7 +584,7 @@ impl Expr {
         // Check that each formal field has an value
         assert!(
             fields.iter().zip(values.iter()).all(|(f, v)| f.typ() == *v.typ()),
-            "Error in struct_expr\n\t{:?}\n\t{:?}",
+            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
             typ,
             values
         );
@@ -593,20 +593,25 @@ impl Expr {
 
     /// Struct initializer  
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
-    /// Note that only the NON padding fields should be explicitiy given.
+    /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
     pub fn struct_expr(
         typ: Type,
         mut components: BTreeMap<String, Expr>,
         symbol_table: &SymbolTable,
     ) -> Self {
-        assert!(typ.is_struct_tag(), "Error in struct_expr\n\t{:?}\n\t{:?}", typ, components);
+        assert!(
+            typ.is_struct_tag(),
+            "Error in struct_expr; must be given a struct_tag.\n\t{:?}\n\t{:?}",
+            typ,
+            components
+        );
         let fields = symbol_table.lookup_fields_in_type(&typ).unwrap();
         let non_padding_fields: Vec<_> = fields.iter().filter(|x| !x.is_padding()).collect();
         assert_eq!(
             non_padding_fields.len(),
             components.len(),
-            "Error in struct_expr\n\t{:?}\n\t{:?}",
+            "Error in struct_expr; mismatch in number of fields and components.\n\t{:?}\n\t{:?}",
             typ,
             components
         );
@@ -658,7 +663,7 @@ impl Expr {
 
     /// Struct initializer  
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
-    /// Note that only the NON padding fields should be explicitiy given.
+    /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
     pub fn struct_expr_from_values(
         typ: Type,
@@ -667,7 +672,7 @@ impl Expr {
     ) -> Self {
         assert!(
             typ.is_struct_tag(),
-            "Error in struct_expr\n\t{:?}\n\t{:?}",
+            "Error in struct_expr; must be given struct_tag.\n\t{:?}\n\t{:?}",
             typ,
             non_padding_values
         );
@@ -676,7 +681,7 @@ impl Expr {
         assert_eq!(
             non_padding_fields.len(),
             non_padding_values.len(),
-            "Error in struct_expr\n\t{:?}\n\t{:?}",
+            "Error in struct_expr; mismatch in number of fields and values.\n\t{:?}\n\t{:?}",
             typ,
             non_padding_values
         );
@@ -685,7 +690,7 @@ impl Expr {
                 .iter()
                 .zip(non_padding_values.iter())
                 .all(|(f, v)| f.field_typ().unwrap() == v.typ()),
-            "Error in struct_expr\n\t{:?}\n\t{:?}",
+            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
             typ,
             non_padding_values
         );
@@ -698,6 +703,40 @@ impl Expr {
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
     }
 
+    /// Struct initializer  
+    /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<`
+    /// Note that padding fields should be explicitly given.
+    /// This would be used when the values and padding have already been combined,
+    /// e.g. when extracting the values out of an existing struct expr (see transformer.rs)
+    pub fn struct_expr_from_padded_values(
+        typ: Type,
+        values: Vec<Expr>,
+        symbol_table: &SymbolTable,
+    ) -> Self {
+        assert!(
+            typ.is_struct_tag(),
+            "Error in struct_expr; must be given struct_tag.\n\t{:?}\n\t{:?}",
+            typ,
+            values
+        );
+        let fields = symbol_table.lookup_fields_in_type(&typ).unwrap();
+        assert_eq!(
+            fields.len(),
+            values.len(),
+            "Error in struct_expr; mismatch in number of padded fields and padded values.\n\t{:?}\n\t{:?}",
+            typ,
+            values
+        );
+        assert!(
+            fields.iter().zip(values.iter()).all(|(f, v)| &f.typ() == v.typ()),
+            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
+            typ,
+            values
+        );
+
+        Expr::struct_expr_with_explicit_padding(typ, fields, values)
+    }
+
     /// `identifier`
     pub fn symbol_expression(identifier: String, typ: Type) -> Self {
         expr!(Symbol { identifier }, typ)
@@ -1205,6 +1244,12 @@ impl Expr {
         res.overflowed.ternary(saturating_val, res.result)
     }
 
+    /// `"s"`
+    /// only to be used when manually wrapped in `.array_to_ptr()`
+    pub fn raw_string_constant(s: &str) -> Self {
+        expr!(StringConstant { s: s.to_string() }, Type::c_char().array_of(s.len() + 1))
+    }
+
     /// `"s"`
     pub fn string_constant(s: &str) -> Self {
         // Internally, CBMC distinguishes between the string constant, and the pointer to it.

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

@@ -8,6 +8,7 @@ mod location;
 mod stmt;
 mod symbol;
 mod symbol_table;
+pub mod symtab_transformer;
 mod typ;
 
 pub use builtin::BuiltinFn;

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

@@ -6,7 +6,7 @@ use std::collections::BTreeMap;
 /// This is a typesafe implementation of the CBMC symbol table, based on the CBMC code at:
 /// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol_table.h
 /// Since the field is kept private, with only immutable references handed out, elements can only
-#[derive(Debug)]
+#[derive(Clone, Debug)]
 pub struct SymbolTable {
     symbol_table: BTreeMap<String, Symbol>,
     machine_model: MachineModel,