diff --git a/README.md b/README.md index 6a072ed77751..6ac5f1c9ae80 100644 --- a/README.md +++ b/README.md @@ -144,6 +144,13 @@ For example, consider the `CopyIntrinsics` regression test: rmc --gen-c main.rs ``` This generates a file `main.c` which contains a "C" like formatting of the CBMC IR. +1. The `--gen-c` flag does not produce runnable C code due to differences in the Rust and C languages. + To produce a runnable C program, try passing the `--gen-c-runnable` flag to RMC + ``` + rmc --gen-c-runnable main.rs + ``` + This generates a file `main_runnable.c`. + Note that this makes some compromises to produce runnable C code, so you should not expect exact semantic equivalence. 1. You can also view the raw CBMC internal representation using the `--keep-temps` option. ### Experimental Cargo integration diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs index 19d54af75668..a9e91ec98d65 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs @@ -878,7 +878,7 @@ impl Expr { } } /// self op right; - fn binop(self, op: BinaryOperand, rhs: Expr) -> Expr { + pub fn binop(self, op: BinaryOperand, rhs: Expr) -> Expr { assert!( Expr::typecheck_binop_args(op, &self, &rhs), "BinaryOperation Expression does not typecheck {:?} {:?} {:?}", diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs new file mode 100644 index 000000000000..3bec5fbf732c --- /dev/null +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs @@ -0,0 +1,268 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use std::ops::{BitAnd, Shl, Shr}; + +use super::super::Transformer; +use crate::gotoc::cbmc::goto_program::{ + BinaryOperand, CIntType, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, SymbolValues, + Type, +}; +use num::bigint::BigInt; +use rustc_data_structures::fx::FxHashMap; + +/// Create an expr from an int constant using only values <= u64::MAX; +/// this is needed because gcc allows 128 bit int variables, but not 128 bit constants +fn bignum_to_expr(num: &BigInt, typ: &Type) -> Expr { + // CInteger types should already be valid in C + if typ.is_c_integer() { + return Expr::int_constant(num.clone(), typ.clone()); + } + + // Only need to handle type wider than 64 bits + if let Some(width) = typ.width() { + if width <= 64 { + return Expr::int_constant(num.clone(), typ.clone()); + } + } + + // Only types that should be left are i128 and u128 + assert_eq!(typ.width(), Some(128), "Unexpected int width: {:?}", typ.width()); + + // Work with unsigned ints, and cast to original type at end + let unsigned_typ = Type::unsigned_int(128); + + // To transform a 128 bit num, we break it into two 64 bit nums + + // left_mask = 11..1100..00 (64 1's followed by 64 0's) + // left_mask = 00..0011..11 (64 0's followed by 64 1's) + let left_mask = BigInt::from(u64::MAX).shl(64); + let right_mask = BigInt::from(u64::MAX); + + // Construct the two 64 bit ints such that + // num = (left_half << 64) | right_half + // = (left_half * 2^64) + right_half + let left_half = { + // Split into two parts to help type inference + let temp: BigInt = num.bitand(left_mask); + temp.shr(64) + }; + let right_half = num.bitand(right_mask); + + // Create CBMC constants for the left and right halfs + let left_constant = Expr::int_constant(left_half, unsigned_typ.clone()); + let right_constant = Expr::int_constant(right_half, unsigned_typ); + + // Construct CBMC expression: (typ) ((left << 64) | right) + left_constant + .shl(Expr::int_constant(64, Type::c_int())) + .bitor(right_constant) + .cast_to(typ.clone()) +} + +/// Struct for handling the expression replacement transformations for --gen-c-runnable. +pub struct ExprTransformer { + new_symbol_table: SymbolTable, + /// The `empty_statics` field is used to track extern static variables; + /// when such a symbol is encountered, we add it to this map; + /// in postprocessing, we initialize each of these variables + /// with a default value to emphasize that these are externally defined. + empty_statics: FxHashMap, +} + +impl ExprTransformer { + /// Replace expressions which lead to invalid C with alternatives. + pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable { + let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone()); + ExprTransformer { new_symbol_table, empty_statics: FxHashMap::default() } + .transform_symbol_table(original_symbol_table) + } + + /// Extract `empty_statics` map for final processing. + fn empty_statics_owned(&mut self) -> FxHashMap { + std::mem::replace(&mut self.empty_statics, FxHashMap::default()) + } + + /// Add identifier to a transformed parameter if it's missing; + /// necessary when function wasn't originally a definition, e.g. extern functions, + /// so that we can give them a function body. + fn add_parameter_identifier(&mut self, parameter: &Parameter) -> Parameter { + if parameter.identifier().is_some() { + parameter.clone() + } else { + let name = format!("__{}", parameter.typ().to_identifier()); + let parameter_sym = self.mut_symbol_table().ensure(&name, |_symtab, name| { + Symbol::variable( + name.to_string(), + name.to_string(), + parameter.typ().clone(), + Location::none(), + ) + }); + parameter_sym.to_function_parameter() + } + } +} + +impl Transformer for ExprTransformer { + /// Get reference to symbol table. + fn symbol_table(&self) -> &SymbolTable { + &self.new_symbol_table + } + + /// Get mutable reference to symbol table. + fn mut_symbol_table(&mut self) -> &mut SymbolTable { + &mut self.new_symbol_table + } + + /// Get owned symbol table. + fn extract_symbol_table(self) -> SymbolTable { + self.new_symbol_table + } + + /// Translate Implies into Or/Not. + fn transform_expr_bin_op( + &mut self, + _typ: &Type, + op: &BinaryOperand, + lhs: &Expr, + rhs: &Expr, + ) -> Expr { + let lhs = self.transform_expr(lhs); + let rhs = self.transform_expr(rhs); + + match op { + BinaryOperand::Implies => lhs.not().bitor(rhs).cast_to(Type::bool()), + _ => lhs.binop(*op, rhs), + } + } + + /// Prevent error for too large constants with u128. + fn transform_expr_int_constant(&mut self, typ: &Type, value: &BigInt) -> Expr { + let transformed_typ = self.transform_type(typ); + bignum_to_expr(value, &transformed_typ) + } + + /// When indexing into a SIMD vector, cast to a pointer first to make legal indexing in C. + /// `typ __attribute__((vector_size (size * sizeof(typ)))) var;` + /// `((typ*) &var)[index]` + /// Tracking issue: https://github.com/model-checking/rmc/issues/444 + fn transform_expr_index(&mut self, _typ: &Type, array: &Expr, index: &Expr) -> Expr { + let transformed_array = self.transform_expr(array); + let transformed_index = self.transform_expr(index); + if transformed_array.typ().is_vector() { + let base_type = transformed_array.typ().base_type().unwrap().clone(); + transformed_array.address_of().cast_to(base_type.to_pointer()).index(transformed_index) + } else { + transformed_array.index(transformed_index) + } + } + + /// Replace `extern` functions and values with `nondet` so linker doesn't break. + fn transform_symbol(&mut self, symbol: &Symbol) -> Symbol { + let mut new_symbol = symbol.clone(); + + if symbol.is_extern { + if symbol.typ.is_code() || symbol.typ.is_variadic_code() { + // Replace `extern` function with one which returns `nondet` + assert!(symbol.value.is_none(), "Extern function should have no body."); + + let transformed_typ = self.transform_type(&symbol.typ); + + // Fill missing parameter names with dummy name + let parameters = transformed_typ + .parameters() + .unwrap() + .iter() + .map(|parameter| self.add_parameter_identifier(parameter)) + .collect(); + let ret_typ = transformed_typ.return_type().unwrap().clone(); + let new_typ = if transformed_typ.is_code() { + Type::code(parameters, ret_typ.clone()) + } else { + Type::variadic_code(parameters, ret_typ.clone()) + }; + + // Create body, which returns nondet + let ret_e = if ret_typ.is_empty() { None } else { Some(Expr::nondet(ret_typ)) }; + let body = Stmt::ret(ret_e, Location::none()); + let new_value = SymbolValues::Stmt(body); + + new_symbol.is_extern = false; + new_symbol.typ = new_typ; + new_symbol.value = new_value; + } else { + // Replace `extern static`s and initialize in `main` + assert!( + symbol.is_static_lifetime, + "Extern objects that aren't functions should be static variables." + ); + let new_typ = self.transform_type(&symbol.typ); + self.empty_statics.insert(symbol.name.clone(), Expr::nondet(new_typ.clone())); + + // Symbol is no longer extern + new_symbol.is_extern = false; + + // Set location to none so that it is a global static + new_symbol.location = Location::none(); + + new_symbol.typ = new_typ; + new_symbol.value = SymbolValues::None; + } + } else if &symbol.name == "main" { + // Replace `main` with `main_` since it has the wrong return type + new_symbol.name = "main_".to_string(); + new_symbol.base_name = Some("main_".to_string()); + new_symbol.pretty_name = Some("main_".to_string()); + + let new_typ = self.transform_type(&symbol.typ); + let new_value = self.transform_value(&symbol.value); + + new_symbol.typ = new_typ; + new_symbol.value = new_value; + } else { + // Handle all other symbols normally + let new_typ = self.transform_type(&symbol.typ); + let new_value = self.transform_value(&symbol.value); + new_symbol.typ = new_typ; + new_symbol.value = new_value; + } + + new_symbol + } + + /// Move `main` to `main_`, and create a wrapper `main` to initialize statics and return `int`. + fn postprocess(&mut self) { + // The body of the new `main` function + let mut main_body = Vec::new(); + + // Initialize statics + for (name, value) in self.empty_statics_owned() { + let sym_expr = Expr::symbol_expression(name, value.typ().clone()); + main_body.push(Stmt::assign(sym_expr, value, Location::none())); + } + + // `main_();`, if it is present + if let Some(main_) = self.symbol_table().lookup("main_") { + main_body + .push(Stmt::code_expression(main_.to_expr().call(Vec::new()), Location::none())); + } + + // `return 0;` + main_body.push(Stmt::ret( + Some(Expr::int_constant(0, Type::CInteger(CIntType::Int))), + Location::none(), + )); + + // Create `main` symbol + let new_main = Symbol::function( + "main", + Type::code(Vec::new(), Type::CInteger(CIntType::Int)), + Some(Stmt::block(main_body, Location::none())), + Some("main".to_string()), + Location::none(), + ); + + self.mut_symbol_table().insert(new_main); + } +} diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/mod.rs new file mode 100644 index 000000000000..c3f623426bde --- /dev/null +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/mod.rs @@ -0,0 +1,10 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +mod expr_transformer; +mod name_transformer; +mod nondet_transformer; + +pub use expr_transformer::ExprTransformer; +pub use name_transformer::NameTransformer; +pub use nondet_transformer::NondetTransformer; diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs new file mode 100644 index 000000000000..41a70f14f4a5 --- /dev/null +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs @@ -0,0 +1,253 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use super::super::Transformer; +use crate::gotoc::cbmc::goto_program::{ + DatatypeComponent, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, Type, +}; +use rustc_data_structures::fx::{FxHashMap, FxHashSet}; + +/// Struct for replacing names with valid C identifiers for --gen-c-runnable. +pub struct NameTransformer { + new_symbol_table: SymbolTable, + /// We want to ensure that the `normalize_identifier` function is both + /// functional (each Rust name always maps to the same C name) and + /// injective (two distinct Rust names map to two distinct C names). + /// To do this, `mapped_names` remembers what each Rust name gets transformed to, + /// and `used_names` keeps track of what C names have been used. + mapped_names: FxHashMap, + used_names: FxHashSet, +} + +impl NameTransformer { + /// Transform all identifiers in the symbol table to be valid C identifiers. + pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable { + let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone()); + NameTransformer { + new_symbol_table, + mapped_names: FxHashMap::default(), + used_names: FxHashSet::default(), + } + .transform_symbol_table(original_symbol_table) + } + + /// Converts an arbitrary identifier into a valid C identifier. + fn normalize_identifier(&mut self, orig_name: &str) -> String { + assert!(!orig_name.is_empty(), "Received empty identifier."); + + // If name already encountered, return same result; + // this is necessary for correctness to avoid a single name + // being mapped to two different names later on + if let Some(result) = self.mapped_names.get(orig_name) { + return result.clone(); + } + + // Don't tranform the `tag-` prefix of identifiers + let (prefix, name) = if orig_name.starts_with("tag-") { + (&orig_name[..4], &orig_name[4..]) + } else { + ("", orig_name) + }; + + // Separate function name from variable name for CBMC + let (name, suffix) = { + let mut parts = name.split("::1::"); + let name = parts.next().unwrap(); + let suffix = parts.next(); + assert!(parts.next().is_none(), "Found multiple occurrences of '::1::' in identifier."); + (name, suffix) + }; + + // We separately call fix_name on the main part of the name + // and the suffix. This allows us to use the :: separator + // between the two parts, and also ensure that the + // base name of a variable stays as the suffix of the unique name. + fn fix_name(name: &str) -> String { + // Convert non-(alphanumeric + underscore) characters to underscore + let valid_chars = + name.replace(|ch: char| !(ch.is_alphanumeric() || ch == '_' || ch == '$'), "_"); + + // If the first character is a number, prefix with underscore + let new_name = match valid_chars.chars().next() { + Some(first) => { + if first.is_numeric() { + let mut name = "_".to_string(); + name.push_str(&valid_chars); + name + } else { + valid_chars + } + } + None => "".to_string(), + }; + + // Replace reserved names with alternatives + // This should really handle *all* reserved C names. + // Tracking issue: https://github.com/model-checking/rmc/issues/439 + let illegal_names = [("case", "case_"), ("default", "default_")]; + for (illegal, replacement) in illegal_names { + if new_name.ends_with(illegal) { + return new_name.replace(illegal, replacement); + } + } + return new_name; + } + + let name = fix_name(name); + let suffix = suffix.map(fix_name); + + // Add `tag-` back in if it was present + let with_prefix = format!("{}{}", prefix, name); + + // Reattach the variable name + let result = match suffix { + None => with_prefix, + Some(suffix) => format!("{}::{}", with_prefix, suffix), + }; + + // Ensure result has not been used before + let result = if self.used_names.contains(&result) { + let mut suffix = 0; + loop { + let result = format!("{}_{}", result, suffix); + if !self.used_names.contains(&result) { + break result; + } + suffix += 1; + } + } else { + result + }; + + // Remember result and return + self.used_names.insert(result.clone()); + self.mapped_names.insert(orig_name.to_string(), result); + self.mapped_names.get(orig_name).unwrap().clone() + } +} + +impl Transformer for NameTransformer { + /// Get reference to symbol table. + fn symbol_table(&self) -> &SymbolTable { + &self.new_symbol_table + } + + /// Get mutable reference to symbol table. + fn mut_symbol_table(&mut self) -> &mut SymbolTable { + &mut self.new_symbol_table + } + + /// Get owned symbol table. + fn extract_symbol_table(self) -> SymbolTable { + self.new_symbol_table + } + + /// Normalize parameter identifier. + fn transform_type_parameter(&mut self, parameter: &Parameter) -> Parameter { + Type::parameter( + parameter.identifier().map(|name| self.normalize_identifier(name)), + parameter.base_name().map(|name| self.normalize_identifier(name)), + self.transform_type(parameter.typ()), + ) + } + + /// Normalize field names. + fn transform_expr_member(&mut self, _typ: &Type, lhs: &Expr, field: &str) -> Expr { + let transformed_lhs = self.transform_expr(lhs); + transformed_lhs.member(&self.normalize_identifier(field), self.symbol_table()) + } + + /// Normalize name in identifier expression. + fn transform_expr_symbol(&mut self, typ: &Type, identifier: &str) -> Expr { + let transformed_typ = self.transform_type(typ); + Expr::symbol_expression(self.normalize_identifier(identifier), transformed_typ) + } + + /// Normalize union field names. + fn transform_expr_union(&mut self, typ: &Type, value: &Expr, field: &str) -> Expr { + let transformed_typ = self.transform_type(typ); + let transformed_value = self.transform_expr(value); + Expr::union_expr( + transformed_typ, + &self.normalize_identifier(field), + transformed_value, + self.symbol_table(), + ) + } + + /// Normalize incomplete struct tag name. + fn transform_type_incomplete_struct(&mut self, tag: &str) -> Type { + Type::incomplete_struct(&self.normalize_identifier(tag)) + } + + /// Normalize incomplete union tag name. + fn transform_type_incomplete_union(&mut self, tag: &str) -> Type { + Type::incomplete_union(&self.normalize_identifier(tag)) + } + + /// Normalize union/struct component name. + fn transform_datatype_component(&mut self, component: &DatatypeComponent) -> DatatypeComponent { + match component { + DatatypeComponent::Field { name, typ } => DatatypeComponent::Field { + name: self.normalize_identifier(name), + typ: self.transform_type(typ), + }, + DatatypeComponent::Padding { name, bits } => { + DatatypeComponent::Padding { name: self.normalize_identifier(name), bits: *bits } + } + } + } + + /// Normalize struct type name. + fn transform_type_struct(&mut self, tag: &str, components: &[DatatypeComponent]) -> Type { + let transformed_components = components + .iter() + .map(|component| self.transform_datatype_component(component)) + .collect(); + Type::struct_type(&self.normalize_identifier(tag), transformed_components) + } + + /// Normalize struct tag name. + fn transform_type_struct_tag(&mut self, tag: &str) -> Type { + Type::struct_tag_raw(&self.normalize_identifier(tag)) + } + + /// Normalize union type name. + fn transform_type_union(&mut self, tag: &str, components: &[DatatypeComponent]) -> Type { + let transformed_components = components + .iter() + .map(|component| self.transform_datatype_component(component)) + .collect(); + Type::union_type(&self.normalize_identifier(tag), transformed_components) + } + + /// Normalize union tag name. + fn transform_type_union_tag(&mut self, tag: &str) -> Type { + Type::union_tag_raw(&self.normalize_identifier(tag)) + } + + /// Normalize goto label name. + fn transform_stmt_goto(&mut self, label: &str) -> Stmt { + Stmt::goto(self.normalize_identifier(label), Location::none()) + } + + /// Normalize label name. + fn transform_stmt_label(&mut self, label: &str, body: &Stmt) -> Stmt { + let transformed_body = self.transform_stmt(body); + transformed_body.with_label(self.normalize_identifier(label)) + } + + /// Normalize symbol names. + fn transform_symbol(&mut self, symbol: &Symbol) -> Symbol { + let mut new_symbol = symbol.clone(); + new_symbol.typ = self.transform_type(&symbol.typ); + new_symbol.value = self.transform_value(&symbol.value); + + new_symbol.name = self.normalize_identifier(&new_symbol.name); + new_symbol.base_name = new_symbol.base_name.map(|name| self.normalize_identifier(&name)); + new_symbol.pretty_name = + new_symbol.pretty_name.map(|name| self.normalize_identifier(&name)); + + new_symbol + } +} diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs new file mode 100644 index 000000000000..5776d1907df0 --- /dev/null +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs @@ -0,0 +1,139 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use super::super::Transformer; +use crate::gotoc::cbmc::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type}; +use rustc_data_structures::fx::FxHashMap; + +/// Struct for handling the nondet transformations for --gen-c-runnable. +pub struct NondetTransformer { + new_symbol_table: SymbolTable, + nondet_types: FxHashMap, +} + +impl NondetTransformer { + /// Transform all identifiers in the symbol table to be valid C identifiers; + /// perform other clean-up operations to make valid C code. + pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable { + let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone()); + NondetTransformer { new_symbol_table, nondet_types: FxHashMap::default() } + .transform_symbol_table(original_symbol_table) + } + + /// Extract `nondet_types` map for final processing. + pub fn nondet_types_owned(&mut self) -> FxHashMap { + std::mem::replace(&mut self.nondet_types, FxHashMap::default()) + } +} + +impl Transformer for NondetTransformer { + /// Get reference to symbol table. + fn symbol_table(&self) -> &SymbolTable { + &self.new_symbol_table + } + + /// Get mutable reference to symbol table. + fn mut_symbol_table(&mut self) -> &mut SymbolTable { + &mut self.new_symbol_table + } + + /// Get owned symbol table. + fn extract_symbol_table(self) -> SymbolTable { + self.new_symbol_table + } + + /// Transform nondets to create default values for the expected type. + /// Given: `let x: u32 = __nondet();` + /// Transformed: + /// ``` + /// unsigned int x = non_det_unsigned_bv_32(); + /// ... + /// unsigned int non_det_unsigned_bv_32(void) { + /// unsigned int ret; + /// return ret; + /// } + /// ``` + fn transform_expr_nondet(&mut self, typ: &Type) -> Expr { + let transformed_typ = self.transform_type(typ); + + let identifier = format!("non_det_{}", transformed_typ.to_identifier()); + let function_type = Type::code(vec![], transformed_typ); + + // Create non_det function which returns default value in postprocessing + self.nondet_types.insert(identifier.clone(), function_type.clone()); + + Expr::symbol_expression(identifier, function_type).call(vec![]) + } + + /// Don't transform padding fields so that they are ignored by CBMC --dump-c. + /// If we don't ignore padding fields, we get code that looks like + /// ``` + /// var_7 = size; + /// var_8 = l; + /// unsigned __CPROVER_bitvector[56] return_value_non_det_unsigned_bv_56=non_det_unsigned_bv_56(); + /// var_9 = (struct _usize__bool_){ ._0=var_7 * var_8, ._1=overflow("*", unsigned long int, var_7, var_8) }; + /// ``` + /// If we do ignore the padding fields, the third line is removed. + fn transform_expr_struct(&mut self, typ: &Type, values: &[Expr]) -> Expr { + let transformed_typ = self.transform_type(typ); + assert!( + transformed_typ.is_struct_tag(), + "Transformed StructTag must be StructTag; got {:?}", + transformed_typ + ); + + // Instead of just mapping `self.transform_expr` over the values, + // only transform those which are true fields, not padding + let fields = self.symbol_table().lookup_fields_in_type(&transformed_typ).unwrap().clone(); + let transformed_values: Vec<_> = fields + .into_iter() + .zip(values.into_iter()) + .map( + |(field, value)| { + if field.is_padding() { value.clone() } else { self.transform_expr(value) } + }, + ) + .collect(); + + Expr::struct_expr_from_padded_values( + transformed_typ, + transformed_values, + self.symbol_table(), + ) + } + + /// Create non_det functions which return default value for type. + fn postprocess(&mut self) { + for (identifier, typ) in self.nondet_types_owned() { + // Create function body which initializes variable and returns it + let ret_type = typ.return_type().unwrap(); + assert!(!ret_type.is_empty(), "Cannot generate nondet of type `void`."); + let ret_name = format!("{}_ret", &identifier); + let ret_expr = Expr::symbol_expression(ret_name.clone(), ret_type.clone()); + let body = Stmt::block( + vec![ + // var_ret; + Stmt::decl(ret_expr.clone(), None, Location::none()), + // return var_ret; + Stmt::ret(Some(ret_expr), Location::none()), + ], + Location::none(), + ); + + // Add return variable to symbol table + let ret_sym = + Symbol::variable(ret_name, "ret".to_string(), ret_type.clone(), Location::none()); + self.mut_symbol_table().insert(ret_sym); + + // Add function to symbol table + let func_sym = Symbol::function( + &identifier, + typ, + Some(body), + Some(identifier.clone()), + Location::none(), + ); + self.mut_symbol_table().insert(func_sym); + } + } +} diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/identity_transformer.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/identity_transformer.rs index 4a54b998ba6a..8d57ae0c12d4 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/identity_transformer.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/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 super::super::SymbolTable; use super::Transformer; +use crate::gotoc::cbmc::goto_program::SymbolTable; /// Struct for performing the identity transformation on a symbol table. /// Mainly used as a demo/for testing. diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/mod.rs index 910f5ea40e84..c3aa6da1a742 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/mod.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/mod.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains the structures used for symbol table transformations. +mod gen_c_transformer; mod identity_transformer; mod passes; mod transformer; diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/passes.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/passes.rs index 712fa9824afa..a08fa33755c4 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/passes.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/passes.rs @@ -1,13 +1,24 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -use super::super::SymbolTable; +use super::gen_c_transformer::{ExprTransformer, NameTransformer, NondetTransformer}; use super::identity_transformer::IdentityTransformer; +use crate::gotoc::cbmc::goto_program::SymbolTable; /// Performs each pass provided on the given symbol table. pub fn do_passes(mut symtab: SymbolTable, pass_names: &[String]) -> SymbolTable { for pass_name in pass_names { symtab = match &pass_name[..] { + "gen-c" => { + // Note: the order of these DOES matter; + // ExprTransformer expects the NondetTransformer to happen after, and + // NameTransformer should clean up any identifiers introduced by + // the other two identifiers + let symtab = ExprTransformer::transform(&symtab); + let symtab = NondetTransformer::transform(&symtab); + let symtab = NameTransformer::transform(&symtab); + symtab + } "identity" => IdentityTransformer::transform(&symtab), _ => panic!("Invalid symbol table transformation: {}", pass_name), } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs index f2cb5f55d3a6..0acbce1f3793 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -use super::super::{ +use crate::gotoc::cbmc::goto_program::{ BinaryOperand, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, SelfOperand, Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type, UnaryOperand, }; @@ -36,7 +36,7 @@ pub trait Transformer: Sized { /// Perform recursive descent on a `Type` data structure. /// Extracts the variant's field data, and passes them into /// the corresponding type transformer method. - fn transform_type(&self, typ: &Type) -> Type { + fn transform_type(&mut self, typ: &Type) -> Type { match typ { Type::Array { typ, size } => self.transform_type_array(typ, size), Type::Bool => self.transform_type_bool(), @@ -68,24 +68,24 @@ pub trait Transformer: Sized { } /// Transforms an array type (`typ x[size]`) - fn transform_type_array(&self, typ: &Box, size: &u64) -> Type { + fn transform_type_array(&mut self, typ: &Box, size: &u64) -> Type { let transformed_typ = self.transform_type(typ.as_ref()); transformed_typ.array_of(*size) } /// Transforms a CPROVER boolean type (`__CPROVER_bool x`) - fn transform_type_bool(&self) -> Type { + fn transform_type_bool(&mut self) -> Type { Type::bool() } /// Transforms a c bit field type (`typ x : width`) - fn transform_type_c_bit_field(&self, typ: &Box, width: &u64) -> Type { + fn transform_type_c_bit_field(&mut self, typ: &Box, width: &u64) -> Type { let transformed_typ = self.transform_type(typ.as_ref()); transformed_typ.as_bitfield(*width) } /// Transforms a machine-dependent integer type (`bool`, `char`, `int`, `size_t`) - fn transform_type_c_integer(&self, c_int_type: &CIntType) -> Type { + fn transform_type_c_integer(&mut self, c_int_type: &CIntType) -> Type { match c_int_type { CIntType::Bool => Type::c_bool(), CIntType::Char => Type::c_char(), @@ -96,7 +96,7 @@ pub trait Transformer: Sized { } /// Transforms a parameter for a function - fn transform_type_parameter(&self, parameter: &Parameter) -> Parameter { + fn transform_type_parameter(&mut self, parameter: &Parameter) -> Parameter { Type::parameter( parameter.identifier().cloned(), parameter.base_name().cloned(), @@ -105,7 +105,7 @@ pub trait Transformer: Sized { } /// Transforms a function type (`return_type x(parameters)`) - fn transform_type_code(&self, parameters: &[Parameter], return_type: &Box) -> Type { + fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Box) -> Type { let transformed_parameters = parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect(); let transformed_return_type = self.transform_type(return_type); @@ -113,60 +113,60 @@ pub trait Transformer: Sized { } /// Transforms a constructor type (`__attribute__(constructor)`) - fn transform_type_constructor(&self) -> Type { + fn transform_type_constructor(&mut self) -> Type { Type::constructor() } /// Transforms a double type (`double`) - fn transform_type_double(&self) -> Type { + fn transform_type_double(&mut self) -> Type { Type::double() } /// Transforms an empty type (`void`) - fn transform_type_empty(&self) -> Type { + fn transform_type_empty(&mut self) -> Type { Type::empty() } /// Transforms a flexible array type (`typ x[]`) - fn transform_type_flexible_array(&self, typ: &Box) -> Type { + fn transform_type_flexible_array(&mut self, typ: &Box) -> Type { let transformed_typ = self.transform_type(typ); Type::flexible_array_of(transformed_typ) } /// Transforms a float type (`float`) - fn transform_type_float(&self) -> Type { + fn transform_type_float(&mut self) -> Type { Type::float() } /// Transforms an incomplete struct type (`struct x {}`) - fn transform_type_incomplete_struct(&self, tag: &str) -> Type { + fn transform_type_incomplete_struct(&mut self, tag: &str) -> Type { Type::incomplete_struct(tag) } /// Transforms an incomplete union type (`union x {}`) - fn transform_type_incomplete_union(&self, tag: &str) -> Type { + fn transform_type_incomplete_union(&mut self, tag: &str) -> Type { Type::incomplete_union(tag) } /// Transforms an infinite array type (`typ x[__CPROVER_infinity()]`) - fn transform_type_infinite_array(&self, typ: &Box) -> Type { + fn transform_type_infinite_array(&mut self, typ: &Box) -> Type { let transformed_typ = self.transform_type(typ.as_ref()); transformed_typ.infinite_array_of() } /// Transforms a pointer type (`typ*`) - fn transform_type_pointer(&self, typ: &Box) -> Type { + fn transform_type_pointer(&mut self, typ: &Box) -> Type { let transformed_typ = self.transform_type(typ.as_ref()); transformed_typ.to_pointer() } /// Transforms a signed bitvector type (`int_t`) - fn transform_type_signedbv(&self, width: &u64) -> Type { + fn transform_type_signedbv(&mut self, width: &u64) -> Type { Type::signed_int(*width) } /// Transforms a datatype component - fn transform_datatype_component(&self, component: &DatatypeComponent) -> DatatypeComponent { + fn transform_datatype_component(&mut self, component: &DatatypeComponent) -> DatatypeComponent { match component { DatatypeComponent::Field { name, typ } => { DatatypeComponent::Field { name: name.to_string(), typ: self.transform_type(typ) } @@ -178,7 +178,7 @@ pub trait Transformer: Sized { } /// Transforms a struct type (`struct tag {component1.typ component1.name; component2.typ component2.name ... }`) - fn transform_type_struct(&self, tag: &str, components: &[DatatypeComponent]) -> Type { + fn transform_type_struct(&mut self, tag: &str, components: &[DatatypeComponent]) -> Type { let transformed_components = components .iter() .map(|component| self.transform_datatype_component(component)) @@ -187,12 +187,12 @@ pub trait Transformer: Sized { } /// Transforms a struct tag type (`tag-`) - fn transform_type_struct_tag(&self, tag: &str) -> Type { + fn transform_type_struct_tag(&mut self, tag: &str) -> Type { Type::struct_tag_raw(tag) } /// Transforms a union type (`union tag {component1.typ component1.name; component2.typ component2.name ... }`) - fn transform_type_union(&self, tag: &str, components: &[DatatypeComponent]) -> Type { + fn transform_type_union(&mut self, tag: &str, components: &[DatatypeComponent]) -> Type { let transformed_components = components .iter() .map(|component| self.transform_datatype_component(component)) @@ -201,18 +201,18 @@ pub trait Transformer: Sized { } /// Transforms a union tag type (`tag-`) - fn transform_type_union_tag(&self, tag: &str) -> Type { + fn transform_type_union_tag(&mut self, tag: &str) -> Type { Type::union_tag_raw(tag) } /// Transforms an unsigned bitvector type (`uint_t`) - fn transform_type_unsignedbv(&self, width: &u64) -> Type { + fn transform_type_unsignedbv(&mut self, width: &u64) -> Type { Type::unsigned_int(*width) } /// Transforms a variadic function type (`return_type x(parameters, ...)`) fn transform_type_variadic_code( - &self, + &mut self, parameters: &[Parameter], return_type: &Box, ) -> Type { @@ -223,7 +223,7 @@ pub trait Transformer: Sized { } /// Transforms a vector type (`typ __attribute__((vector_size (size * sizeof(typ)))) var;`) - fn transform_type_vector(&self, typ: &Box, size: &u64) -> Type { + fn transform_type_vector(&mut self, typ: &Box, size: &u64) -> Type { let transformed_typ = self.transform_type(typ.as_ref()); Type::vector(transformed_typ, *size) } @@ -231,7 +231,7 @@ pub trait Transformer: Sized { /// 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. - fn transform_expr(&self, e: &Expr) -> Expr { + fn transform_expr(&mut self, e: &Expr) -> Expr { let typ = e.typ(); match e.value() { ExprValue::AddressOf(child) => self.transform_expr_address_of(typ, child), @@ -272,26 +272,26 @@ pub trait Transformer: Sized { } /// Transforms a reference expr (`&self`) - fn transform_expr_address_of(&self, _typ: &Type, child: &Expr) -> Expr { + fn transform_expr_address_of(&mut self, _typ: &Type, child: &Expr) -> Expr { self.transform_expr(child).address_of() } /// Transform an array expr (`typ x[] = >>> {elems0, elems1 ...} <<<`) - fn transform_expr_array(&self, typ: &Type, elems: &[Expr]) -> Expr { + fn transform_expr_array(&mut self, typ: &Type, elems: &[Expr]) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_elems = elems.iter().map(|elem| self.transform_expr(elem)).collect(); Expr::array_expr(transformed_typ, transformed_elems) } /// Transform a vector expr (`vec_typ x[] = >>> {elems0, elems1 ...} <<<`) - fn transform_expr_vector(&self, typ: &Type, elems: &[Expr]) -> Expr { + fn transform_expr_vector(&mut self, typ: &Type, elems: &[Expr]) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_elems = elems.iter().map(|elem| self.transform_expr(elem)).collect(); Expr::vector_expr(transformed_typ, transformed_elems) } /// Transforms an array of expr (`typ x[width] = >>> {elem} <<<`) - fn transform_expr_array_of(&self, typ: &Type, elem: &Expr) -> Expr { + fn transform_expr_array_of(&mut self, typ: &Type, elem: &Expr) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_elem = self.transform_expr(elem); if let Type::Array { typ: _typ, size } = transformed_typ { @@ -303,13 +303,13 @@ pub trait Transformer: Sized { /// Transform an assign expr (`left = right`) /// Currently not able to be constructed, as does not exist in Rust - fn transform_expr_assign(&self, _typ: &Type, _left: &Expr, _right: &Expr) -> Expr { + fn transform_expr_assign(&mut self, _typ: &Type, _left: &Expr, _right: &Expr) -> Expr { unreachable!() } /// Transform a binary operation expr (`lhs op rhs`) fn transform_expr_bin_op( - &self, + &mut self, _typ: &Type, op: &BinaryOperand, lhs: &Expr, @@ -318,74 +318,45 @@ pub trait Transformer: Sized { let lhs = self.transform_expr(lhs); let rhs = self.transform_expr(rhs); - match op { - BinaryOperand::And => lhs.and(rhs), - BinaryOperand::Ashr => lhs.ashr(rhs), - BinaryOperand::Bitand => lhs.bitand(rhs), - BinaryOperand::Bitor => lhs.bitor(rhs), - BinaryOperand::Bitxor => lhs.bitxor(rhs), - BinaryOperand::Div => lhs.div(rhs), - BinaryOperand::Equal => lhs.eq(rhs), - BinaryOperand::Ge => lhs.ge(rhs), - BinaryOperand::Gt => lhs.gt(rhs), - BinaryOperand::IeeeFloatEqual => lhs.feq(rhs), - BinaryOperand::IeeeFloatNotequal => lhs.fneq(rhs), - BinaryOperand::Implies => lhs.implies(rhs), - BinaryOperand::Le => lhs.le(rhs), - BinaryOperand::Lshr => lhs.lshr(rhs), - BinaryOperand::Lt => lhs.lt(rhs), - BinaryOperand::Minus => lhs.sub(rhs), - BinaryOperand::Mod => lhs.rem(rhs), - BinaryOperand::Mult => lhs.mul(rhs), - BinaryOperand::Notequal => lhs.neq(rhs), - BinaryOperand::Or => lhs.or(rhs), - BinaryOperand::OverflowMinus => lhs.sub_overflow_p(rhs), - BinaryOperand::OverflowMult => lhs.mul_overflow_p(rhs), - BinaryOperand::OverflowPlus => lhs.add_overflow_p(rhs), - BinaryOperand::Plus => lhs.plus(rhs), - BinaryOperand::Rol => lhs.rol(rhs), - BinaryOperand::Ror => lhs.ror(rhs), - BinaryOperand::Shl => lhs.shl(rhs), - BinaryOperand::Xor => lhs.xor(rhs), - } + lhs.binop(*op, rhs) } /// Transforms a CPROVER boolean expression (`(__CPROVER_bool) >>> true/false <<<`) - fn transform_expr_bool_constant(&self, _typ: &Type, value: &bool) -> Expr { + fn transform_expr_bool_constant(&mut self, _typ: &Type, value: &bool) -> Expr { Expr::bool_constant(*value) } /// Transforms a byte extraction expr (e as type self.typ) - fn transform_expr_byte_extract(&self, typ: &Type, e: &Expr, _offset: &u64) -> Expr { + fn transform_expr_byte_extract(&mut self, typ: &Type, e: &Expr, _offset: &u64) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_e = self.transform_expr(e); transformed_e.transmute_to(transformed_typ, self.symbol_table()) } /// Transforms a C boolean constant expr (`(bool) 1`) - fn transform_expr_c_bool_constant(&self, _typ: &Type, value: &bool) -> Expr { + fn transform_expr_c_bool_constant(&mut self, _typ: &Type, value: &bool) -> Expr { Expr::c_bool_constant(*value) } /// Transforms a deref expr (`*self`) - fn transform_expr_dereference(&self, _typ: &Type, child: &Expr) -> Expr { + fn transform_expr_dereference(&mut self, _typ: &Type, child: &Expr) -> Expr { let transformed_child = self.transform_expr(child); transformed_child.dereference() } /// Transforms a double constant expr (`1.0`) - fn transform_expr_double_constant(&self, _typ: &Type, value: &f64) -> Expr { + fn transform_expr_double_constant(&mut self, _typ: &Type, value: &f64) -> Expr { Expr::double_constant(*value) } /// Transforms a float constant expr (`1.0f`) - fn transform_expr_float_constant(&self, _typ: &Type, value: &f32) -> Expr { + fn transform_expr_float_constant(&mut self, _typ: &Type, value: &f32) -> Expr { Expr::float_constant(*value) } /// Transforms a function call expr (`function(arguments)`) fn transform_expr_function_call( - &self, + &mut self, _typ: &Type, function: &Expr, arguments: &[Expr], @@ -397,7 +368,7 @@ pub trait Transformer: Sized { } /// Transforms an if expr (`c ? t : e`) - fn transform_expr_if(&self, _typ: &Type, c: &Expr, t: &Expr, e: &Expr) -> Expr { + fn transform_expr_if(&mut self, _typ: &Type, c: &Expr, t: &Expr, e: &Expr) -> Expr { let transformed_c = self.transform_expr(c); let transformed_t = self.transform_expr(t); let transformed_e = self.transform_expr(e); @@ -405,38 +376,38 @@ pub trait Transformer: Sized { } /// Transforms an array index expr (`array[expr]`) - fn transform_expr_index(&self, _typ: &Type, array: &Expr, index: &Expr) -> Expr { + fn transform_expr_index(&mut self, _typ: &Type, array: &Expr, index: &Expr) -> Expr { let transformed_array = self.transform_expr(array); let transformed_index = self.transform_expr(index); transformed_array.index(transformed_index) } /// Transforms an int constant expr (`123`) - fn transform_expr_int_constant(&self, typ: &Type, value: &BigInt) -> Expr { + fn transform_expr_int_constant(&mut self, typ: &Type, value: &BigInt) -> Expr { let transformed_typ = self.transform_type(typ); Expr::int_constant(value.clone(), transformed_typ) } /// Transforms a member access expr (`lhs.field`) - fn transform_expr_member(&self, _typ: &Type, lhs: &Expr, field: &str) -> Expr { + fn transform_expr_member(&mut self, _typ: &Type, lhs: &Expr, field: &str) -> Expr { let transformed_lhs = self.transform_expr(lhs); transformed_lhs.member(field, self.symbol_table()) } /// Transforms a CPROVER nondet call (`__nondet()`) - fn transform_expr_nondet(&self, typ: &Type) -> Expr { + fn transform_expr_nondet(&mut self, typ: &Type) -> Expr { let transformed_typ = self.transform_type(typ); Expr::nondet(transformed_typ) } /// Transforms a pointer constant expr (`NULL`) - fn transform_expr_pointer_constant(&self, typ: &Type, value: &u64) -> Expr { + fn transform_expr_pointer_constant(&mut self, typ: &Type, value: &u64) -> Expr { let transformed_typ = self.transform_type(typ); Expr::pointer_constant(*value, transformed_typ) } /// Transforms a self-op expr (`op++`, etc.) - fn transform_expr_self_op(&self, _typ: &Type, op: &SelfOperand, e: &Expr) -> Expr { + fn transform_expr_self_op(&mut self, _typ: &Type, op: &SelfOperand, e: &Expr) -> Expr { let transformed_e = self.transform_expr(e); match op { SelfOperand::Postdecrement => transformed_e.postdecr(), @@ -447,7 +418,7 @@ pub trait Transformer: Sized { } /// Transforms a statement expr (({ stmt1; stmt2; ...})) - fn transform_expr_statement_expression(&self, typ: &Type, statements: &[Stmt]) -> Expr { + fn transform_expr_statement_expression(&mut self, typ: &Type, statements: &[Stmt]) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_statements = statements.iter().map(|stmt| self.transform_stmt(stmt)).collect(); @@ -455,12 +426,12 @@ pub trait Transformer: Sized { } /// Transforms a string constant expr (`"s"`) - fn transform_expr_string_constant(&self, _typ: &Type, value: &str) -> Expr { + fn transform_expr_string_constant(&mut self, _typ: &Type, value: &str) -> Expr { Expr::raw_string_constant(value) } /// Transforms a struct initializer expr (`struct foo the_foo = >>> {field1, field2, ... } <<<`) - fn transform_expr_struct(&self, typ: &Type, values: &[Expr]) -> Expr { + fn transform_expr_struct(&mut self, typ: &Type, values: &[Expr]) -> Expr { let transformed_typ = self.transform_type(typ); assert!( transformed_typ.is_struct_tag(), @@ -477,27 +448,27 @@ pub trait Transformer: Sized { } /// Transforms a symbol expr (`self`) - fn transform_expr_symbol(&self, typ: &Type, identifier: &str) -> Expr { + fn transform_expr_symbol(&mut self, typ: &Type, identifier: &str) -> Expr { let transformed_typ = self.transform_type(typ); Expr::symbol_expression(identifier.to_string(), transformed_typ) } /// Transforms a typecast expr (`(typ) self`) - fn transform_expr_typecast(&self, typ: &Type, child: &Expr) -> Expr { + fn transform_expr_typecast(&mut self, typ: &Type, child: &Expr) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_child = self.transform_expr(child); transformed_child.cast_to(transformed_typ) } /// Transforms a union initializer expr (`union foo the_foo = >>> {.field = value } <<<`) - fn transform_expr_union(&self, typ: &Type, value: &Expr, field: &str) -> Expr { + fn transform_expr_union(&mut self, typ: &Type, value: &Expr, field: &str) -> Expr { let transformed_typ = self.transform_type(typ); let transformed_value = self.transform_expr(value); Expr::union_expr(transformed_typ, field, transformed_value, self.symbol_table()) } /// Transforms a unary operator expr (`op self`) - fn transform_expr_un_op(&self, _typ: &Type, op: &UnaryOperand, e: &Expr) -> Expr { + fn transform_expr_un_op(&mut self, _typ: &Type, op: &UnaryOperand, e: &Expr) -> Expr { let transformed_e = self.transform_expr(e); match op { UnaryOperand::Bitnot => transformed_e.bitnot(), @@ -517,7 +488,7 @@ pub trait Transformer: Sized { /// Perform recursive descent on a `Stmt` data structure. /// Extracts the variant's field data, and passes them into /// the corresponding stmt transformer method. - fn transform_stmt(&self, stmt: &Stmt) -> Stmt { + fn transform_stmt(&mut self, stmt: &Stmt) -> Stmt { match stmt.body() { StmtBody::Assign { lhs, rhs } => self.transform_stmt_assign(lhs, rhs), StmtBody::Assume { cond } => self.transform_stmt_assume(cond), @@ -547,55 +518,55 @@ pub trait Transformer: Sized { } /// Transforms an assign stmt (`lhs = rhs;`) - fn transform_stmt_assign(&self, lhs: &Expr, rhs: &Expr) -> Stmt { + fn transform_stmt_assign(&mut self, lhs: &Expr, rhs: &Expr) -> Stmt { let transformed_lhs = self.transform_expr(lhs); let transformed_rhs = self.transform_expr(rhs); transformed_lhs.assign(transformed_rhs, Location::none()) } /// Transforms a CPROVER assume stmt (`__CPROVER_assume(cond);`) - fn transform_stmt_assume(&self, cond: &Expr) -> Stmt { + fn transform_stmt_assume(&mut self, cond: &Expr) -> Stmt { let transformed_cond = self.transform_expr(cond); Stmt::assume(transformed_cond, Location::none()) } /// Transforms an atomic block stmt (`{ ATOMIC_BEGIN stmt1; stmt2; ... ATOMIC_END }`) - fn transform_stmt_atomic_block(&self, block: &[Stmt]) -> Stmt { + fn transform_stmt_atomic_block(&mut self, block: &[Stmt]) -> Stmt { let transformed_block = block.iter().map(|stmt| self.transform_stmt(stmt)).collect(); Stmt::atomic_block(transformed_block, Location::none()) } /// Transforms a block stmt (`{ stmt1; stmt2; ... }`) - fn transform_stmt_block(&self, block: &[Stmt]) -> Stmt { + fn transform_stmt_block(&mut self, block: &[Stmt]) -> Stmt { let transformed_block = block.iter().map(|stmt| self.transform_stmt(stmt)).collect(); Stmt::block(transformed_block, Location::none()) } /// Transform a break stmt (`break;`) - fn transform_stmt_break(&self) -> Stmt { + fn transform_stmt_break(&mut self) -> Stmt { Stmt::break_stmt(Location::none()) } /// Transform a continue stmt (`continue;`) - fn transform_stmt_continue(&self) -> Stmt { + fn transform_stmt_continue(&mut self) -> Stmt { Stmt::continue_stmt(Location::none()) } /// Transform a decl stmt (`lhs.typ lhs = value;` or `lhs.typ lhs;`) - fn transform_stmt_decl(&self, lhs: &Expr, value: &Option) -> Stmt { + fn transform_stmt_decl(&mut self, lhs: &Expr, value: &Option) -> Stmt { let transformed_lhs = self.transform_expr(lhs); let transformed_value = value.as_ref().map(|value| self.transform_expr(value)); Stmt::decl(transformed_lhs, transformed_value, Location::none()) } /// Transform an expression stmt (`e;`) - fn transform_stmt_expression(&self, expr: &Expr) -> Stmt { + fn transform_stmt_expression(&mut self, expr: &Expr) -> Stmt { let transformed_expr = self.transform_expr(expr); transformed_expr.as_stmt(Location::none()) } /// Transform a for loop stmt (`for (init; cond; update) {body}`) - fn transform_stmt_for(&self, init: &Stmt, cond: &Expr, update: &Stmt, body: &Stmt) -> Stmt { + fn transform_stmt_for(&mut self, init: &Stmt, cond: &Expr, update: &Stmt, body: &Stmt) -> Stmt { let transformed_init = self.transform_stmt(init); let transformed_cond = self.transform_expr(cond); let transformed_update = self.transform_stmt(update); @@ -612,7 +583,7 @@ pub trait Transformer: Sized { /// Transforms a function call stmt (`lhs = function(arguments);` or `function(arguments);`) fn transform_stmt_function_call( - &self, + &mut self, lhs: &Option, function: &Expr, arguments: &[Expr], @@ -630,12 +601,12 @@ pub trait Transformer: Sized { } /// Transforms a goto stmt (`goto dest;`) - fn transform_stmt_goto(&self, label: &str) -> Stmt { + fn transform_stmt_goto(&mut self, label: &str) -> Stmt { Stmt::goto(label.to_string(), Location::none()) } /// Transforms an if-then-else stmt (`if (i) { t } else { e }`) - fn transform_stmt_ifthenelse(&self, i: &Expr, t: &Stmt, e: &Option) -> Stmt { + fn transform_stmt_ifthenelse(&mut self, i: &Expr, t: &Stmt, e: &Option) -> Stmt { let transformed_i = self.transform_expr(i); let transformed_t = self.transform_stmt(t); let transformed_e = e.as_ref().map(|e| self.transform_stmt(e)); @@ -644,25 +615,25 @@ pub trait Transformer: Sized { } /// Transforms a label stmt (`label: body`) - fn transform_stmt_label(&self, label: &str, body: &Stmt) -> Stmt { + fn transform_stmt_label(&mut self, label: &str, body: &Stmt) -> Stmt { let transformed_body = self.transform_stmt(body); transformed_body.with_label(label.to_string()) } /// Transforms a return stmt (`return e;` or `return;`) - fn transform_stmt_return(&self, value: &Option) -> Stmt { + fn transform_stmt_return(&mut self, value: &Option) -> Stmt { let transformed_value = value.as_ref().map(|value| self.transform_expr(value)); Stmt::ret(transformed_value, Location::none()) } /// Transforms a skip stmt (`;`) - fn transform_stmt_skip(&self) -> Stmt { + fn transform_stmt_skip(&mut self) -> Stmt { Stmt::skip(Location::none()) } /// Transforms a switch stmt (`switch (control) { case1.case: cast1.body; case2.case: case2.body; ... }`) fn transform_stmt_switch( - &self, + &mut self, control: &Expr, cases: &[SwitchCase], default: &Option, @@ -680,14 +651,14 @@ pub trait Transformer: Sized { } /// Transforms a while loop stmt (`while (cond) { body }`) - fn transform_stmt_while(&self, cond: &Expr, body: &Stmt) -> Stmt { + fn transform_stmt_while(&mut self, cond: &Expr, body: &Stmt) -> Stmt { let transformed_cond = self.transform_expr(cond); let transformed_body = self.transform_stmt(body); Stmt::while_loop(transformed_cond, transformed_body, Location::none()) } /// Transforms a symbol's type and value - fn transform_symbol(&self, symbol: &Symbol) -> Symbol { + fn transform_symbol(&mut self, symbol: &Symbol) -> Symbol { let new_typ = self.transform_type(&symbol.typ); let new_value = self.transform_value(&symbol.value); let mut new_symbol = symbol.clone(); @@ -697,7 +668,7 @@ pub trait Transformer: Sized { } /// Transforms a symbol value - fn transform_value(&self, value: &SymbolValues) -> SymbolValues { + fn transform_value(&mut self, value: &SymbolValues) -> SymbolValues { match value { SymbolValues::None => SymbolValues::None, SymbolValues::Expr(expr) => SymbolValues::Expr(self.transform_expr(expr)), diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs index 19a6383731b7..847240ad7f35 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs @@ -401,6 +401,13 @@ impl Type { } } + pub fn is_c_integer(&self) -> bool { + match self { + CInteger(_) => true, + _ => false, + } + } + /// Whether the current type is an integer with finite width pub fn is_integer(&self) -> bool { match self { @@ -838,4 +845,61 @@ impl Type { } types } + + /// Generate a string which uniquely identifies the given type + /// while also being a valid variable/funcion name + pub fn to_identifier(&self) -> String { + match self { + Type::Array { typ, size } => { + format!("array_of_{}_{}", size, typ.to_identifier()) + } + Type::Bool => format!("bool"), + Type::CBitField { width, typ } => { + format!("cbitfield_of_{}_{}", width, typ.to_identifier()) + } + Type::CInteger(int_kind) => format!("c_int_{:?}", int_kind), + // e.g. `int my_func(double x, float_y) {` + // => "code_from_double_float_to_int" + Type::Code { parameters, return_type } => { + let parameter_string = parameters + .iter() + .map(|param| param.typ().to_identifier()) + .collect::>() + .join("_"); + let return_string = return_type.to_identifier(); + format!("code_from_{}_to_{}", parameter_string, return_string) + } + Type::Constructor => format!("constructor"), + Type::Double => format!("double"), + Type::Empty => format!("empty"), + Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()), + Type::Float => format!("float"), + Type::IncompleteStruct { tag } => tag.clone(), + Type::IncompleteUnion { tag } => tag.clone(), + Type::InfiniteArray { typ } => { + format!("infinite_array_of_{}", typ.to_identifier()) + } + Type::Pointer { typ } => format!("pointer_to_{}", typ.to_identifier()), + Type::Signedbv { width } => format!("signed_bv_{}", width), + Type::Struct { tag, .. } => format!("struct_{}", tag), + Type::StructTag(tag) => format!("struct_tag_{}", tag), + Type::Union { tag, .. } => format!("union_{}", tag), + Type::UnionTag(tag) => format!("union_tag_{}", tag), + Type::Unsignedbv { width } => format!("unsigned_bv_{}", width), + // e.g. `int my_func(double x, float_y, ..) {` + // => "variadic_code_from_double_float_to_int" + Type::VariadicCode { parameters, return_type } => { + let parameter_string = parameters + .iter() + .map(|param| param.typ().to_identifier()) + .collect::>() + .join("_"); + let return_string = return_type.to_identifier(); + format!("variadic_code_from_{}_to_{}", parameter_string, return_string) + } + Type::Vector { size, typ } => { + format!("vec_of_{}_{}", size, typ.to_identifier()) + } + } + } } diff --git a/library/rmc/gen_c_lib.c b/library/rmc/gen_c_lib.c new file mode 100644 index 000000000000..0ee4989b0b67 --- /dev/null +++ b/library/rmc/gen_c_lib.c @@ -0,0 +1,58 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This file contains stubs that we link to the produced C file +//! from --gen-c-runnable to make it executable. + +#include +#include +#include +#include +#include + +// By default, don't do anything; +// user can add an assert if they so desire. +void __CPROVER_assume(int condition) { +} + +// We can ignore atomics for simplicity +void __CPROVER_atomic_begin(void) { +} + +void __CPROVER_atomic_end(void) { +} + +// These need to be manually defined for some reason +double powi(double base, int expt) { + return pow(base, (double) expt); +} + +float powif(float base, int expt) { + return (float) powi((double) base, expt); +} + +// Used by cbmc invariants +typedef bool __CPROVER_bool; + +#define OBJECT_SIZE(value) sizeof(*value) + +// POINTER_OBJECT is used by Rust's offset_from to ensure +// the two pointers are from the same object. +// We can't do this in C. +// Tracking issue: https://github.com/model-checking/rmc/issues/440 +#define POINTER_OBJECT(value) 0 + +// Use built-in overflow operators +#define BUILTIN_ADD_OVERFLOW(var1, var2) ({int _tmp = 0; __builtin_add_overflow(var1, var2, &_tmp);}) +#define BUILTIN_SUB_OVERFLOW(var1, var2) ({int _tmp = 0; __builtin_sub_overflow(var1, var2, &_tmp);}) +#define BUILTIN_MUL_OVERFLOW(var1, var2) ({int _tmp = 0; __builtin_mul_overflow(var1, var2, &_tmp);}) + +#define overflow(op, typ, var1, var2) (\ + (op[0] == '+') ? BUILTIN_ADD_OVERFLOW(var1, var2) \ + : (op[0] == '-') ? BUILTIN_SUB_OVERFLOW(var1, var2) \ + : (op[0] == '*') ? BUILTIN_MUL_OVERFLOW(var1, var2) \ + : 1) + +// Only works on little endian machines. +#define byte_extract_little_endian(from_val, offset, to_type) \ + *((typeof(to_type)*) (((void*) &from_val) + (offset))) + diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 76a774c9d1fc..ebb020ab7c0b 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -21,6 +21,28 @@ def main(): rmc.ensure_dependencies_in_path() + if args.gen_c_runnable: + rmc.cargo_build(args.crate, args.target_dir, + args.verbose, args.debug, args.mangler, args.dry_run, ["gen-c"]) + + pattern = os.path.join(args.target_dir, "debug", "deps", "*.json") + jsons = glob.glob(pattern) + rmc.ensure(len(jsons) == 1, f"Unexpected number of json outputs: {len(jsons)}") + + cbmc_runnable_filename = os.path.join(args.target_dir, "cbmc_runnable.out") + c_runnable_filename = os.path.join(args.target_dir, "cbmc_runnable.c") + + if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_runnable_filename, args.verbose, args.keep_temps, args.dry_run): + return 1 + + if EXIT_CODE_SUCCESS != rmc.link_c_lib(cbmc_runnable_filename, cbmc_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run): + return 1 + + if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_runnable_filename, c_runnable_filename, args.verbose, args.dry_run): + return 1 + + rmc.gen_c_postprocess(c_runnable_filename, args.dry_run) + rmc.cargo_build(args.crate, args.target_dir, args.verbose, args.debug, args.mangler, args.dry_run, []) diff --git a/scripts/rmc b/scripts/rmc index c2fae101f7f4..6e1ec91b7c86 100755 --- a/scripts/rmc +++ b/scripts/rmc @@ -22,6 +22,24 @@ def main(): base, ext = os.path.splitext(args.input) rmc.ensure(ext == ".rs", "Expecting .rs input file.") + if args.gen_c_runnable: + json_runnable_filename = base + "_runnable.json" + goto_runnable_filename = base + "_runnable.goto" + c_runnable_filename = base + "_runnable.c" + if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_runnable_filename, args.verbose, args.debug, args.keep_temps, args.mangler, args.dry_run, ["gen-c"]): + return 1 + + if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_runnable_filename, goto_runnable_filename, args.verbose, args.keep_temps, args.dry_run): + return 1 + + if EXIT_CODE_SUCCESS != rmc.link_c_lib(goto_runnable_filename, goto_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run): + return 1 + + if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_runnable_filename, c_runnable_filename, args.verbose, args.dry_run): + return 1 + + rmc.gen_c_postprocess(c_runnable_filename, args.dry_run) + json_filename = base + ".json" goto_filename = base + ".goto" c_filename = base + ".c" diff --git a/scripts/rmc.py b/scripts/rmc.py index 6bd5b2eee187..faebc5fac0a5 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -7,10 +7,13 @@ import os.path import sys import re +import pathlib RMC_CFG = "rmc" RMC_RUSTC_EXE = "rmc-rustc" +MY_PATH = pathlib.Path(__file__).parent.parent.absolute() +GEN_C_LIB = MY_PATH / "library" / "rmc" / "gen_c_lib.c" EXIT_CODE_SUCCESS = 0 CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10 @@ -249,12 +252,86 @@ def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property # Handler for calling goto-instrument def run_goto_instrument(input_filename, output_filename, args, verbose=False, dry_run=False): - cmd = ["goto-instrument"] + args + [input_filename] - return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename, dry_run=dry_run) + cmd = ["goto-instrument"] + args + [input_filename, output_filename] + return run_cmd(cmd, label="goto-instrument", verbose=verbose, dry_run=dry_run) # Generates a C program from a goto program def goto_to_c(goto_filename, c_filename, verbose=False, dry_run=False): return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose, dry_run=dry_run) + +# Fix remaining issues with output of --gen-c-runnable +def gen_c_postprocess(c_filename, dry_run=False): + if not dry_run: + with open(c_filename, "r") as f: + lines = f.read().splitlines() + + # Import gen_c_lib.c + lines.insert(0, f"#include \"{GEN_C_LIB}\"") + + # Convert back to string + string_contents = "\n".join(lines) + + # Remove builtin macros + to_remove = [ + # memcmp + """// memcmp +// file function memcmp +int memcmp(void *, void *, unsigned long int);""", + + # memcpy + """// memcpy +// file function memcpy +void * memcpy(void *, void *, unsigned long int);""", + + # memmove + """// memmove +// file function memmove +void * memmove(void *, void *, unsigned long int);""", + + # sputc + """// __sputc +// file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdio.h line 260 +inline signed int __sputc(signed int _c, FILE *_p);""", + + """// __sputc +// file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdio.h line 260 +inline signed int __sputc(signed int _c, FILE *_p) +{ + signed int tmp_pre=_p->_w - 1; + _p->_w = tmp_pre; + __CPROVER_bool tmp_if_expr; + if(tmp_pre >= 0) + tmp_if_expr = 1; + + else + tmp_if_expr = (_p->_w >= _p->_lbfsize ? ((signed int)(char)_c != 10 ? 1 : 0) : 0) ? 1 : 0; + unsigned char *tmp_post; + unsigned char tmp_assign; + signed int return_value___swbuf; + if(tmp_if_expr) + { + tmp_post = _p->_p; + _p->_p = _p->_p + 1l; + tmp_assign = (unsigned char)_c; + *tmp_post = tmp_assign; + return (signed int)tmp_assign; + } + + else + { + return_value___swbuf=__swbuf(_c, _p); + return return_value___swbuf; + } +}""" + ] + + for block in to_remove: + string_contents = string_contents.replace(block, "") + + # Print back to file + with open(c_filename, "w") as f: + f.write(string_contents) + # Generates the CMBC symbol table from a goto program def goto_to_symbols(goto_filename, symbols_filename, verbose=False, dry_run=False): diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py index 2e40f34dfeb5..3509dc496e16 100644 --- a/scripts/rmc_flags.py +++ b/scripts/rmc_flags.py @@ -78,6 +78,10 @@ def add_artifact_flags(make_group, add_flag, config): "Artifact flags", "Produce artifacts in addition to a basic RMC report.") add_flag(group, "--gen-c", default=False, action=BooleanOptionalAction, help="Generate C file equivalent to inputted program") + add_flag(group, "--gen-c-runnable", default=False, action=BooleanOptionalAction, + help="Generate C file equivalent to inputted program; " + "performs additional processing to produce valid C code " + "at the cost of some readability") add_flag(group, "--gen-symbols", default=False, action=BooleanOptionalAction, help="Generate a goto symbol table") add_flag(group, "--keep-temps", default=False, action=BooleanOptionalAction, diff --git a/src/test/cbmc/CodegenConstValue/bigints.rs b/src/test/cbmc/CodegenConstValue/bigints.rs new file mode 100644 index 000000000000..0e79f39b3fe2 --- /dev/null +++ b/src/test/cbmc/CodegenConstValue/bigints.rs @@ -0,0 +1,37 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn main() { + let x: u128 = u128::MAX; + let x2: u128 = { + // u128::MAX = 2^128 - 1; + // = (2^64 - 1) * (2^64 + 1) + // = u64::MAX + (u64::MAX + 2) + let u64_max = u64::MAX; + let u64_max_u128 = u64_max as u128; + u64_max_u128 * (u64_max_u128 + 2) + }; + assert!(x == x2); + + let y: i128 = i128::MAX; + let y2: i128 = { + // i128::MAX = 2^127 - 1 + // = (2^63 * 2^63) + (2^63 * 2^63 - 1) + let u64_2_63 = 2u64.pow(63); + let i128_2_63 = u64_2_63 as i128; + let i128_2_64 = i128_2_63 * i128_2_63; + i128_2_64 + (i128_2_64 - 1) + }; + assert!(y == y2); + + let z: i128 = i128::MIN; + let z2: i128 = { + // i128::MAX = -2^127 + // = 0 - (2^63 * 2^63) - (2^63 * 2^63) + let u64_2_63 = 2u64.pow(63); + let i128_2_63 = u64_2_63 as i128; + let i128_2_64 = i128_2_63 * i128_2_63; + 0i128 - i128_2_64 - i128_2_64 + }; + assert!(z == z2); +}