From bb268b10fa6ed0b65ad523eb829021ad5a49fe6a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Nov 2022 10:46:52 -0800 Subject: [PATCH 1/5] Remove old environment variables from cbmc (#1938) --- cprover_bindings/src/env.rs | 3 --- kani-driver/src/call_cbmc.rs | 17 ++++++----------- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs index 652cc7a9b67a..42080e52119a 100644 --- a/cprover_bindings/src/env.rs +++ b/cprover_bindings/src/env.rs @@ -74,9 +74,6 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec { pub fn additional_env_symbols() -> Vec { vec![ Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()), - // https://github.com/diffblue/cbmc/blob/b26d3479679574c6c179f911b488a314bc2f1085/src/util/config.h#L214 - int_constant("__CPROVER_malloc_failure_mode_assert_then_assume", 2), - int_constant("__CPROVER_malloc_failure_mode_return_null", 1), Symbol::typedef("__CPROVER_size_t", "__CPROVER_size_t", Type::size_t(), Location::none()), Symbol::static_variable( "__CPROVER_memory", diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 2a2367472b70..11475373ed8a 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -124,17 +124,12 @@ impl KaniSession { args.push("--validate-ssa-equation".into()); } - // Push `--slice-formula` argument. - // Previously, this would happen if the condition below was satisfied: - // ```rust - // if !self.args.visualize - // && self.args.concrete_playback.is_none() - // && !self.args.no_slice_formula - // ``` - // But for some reason, not pushing it causes a CBMC invariant violation - // since version 5.68.0. - // - args.push("--slice-formula".into()); + if !self.args.visualize + && self.args.concrete_playback.is_none() + && !self.args.no_slice_formula + { + args.push("--slice-formula".into()); + } if self.args.concrete_playback.is_some() { args.push("--trace".into()); From fc80db6d2a2f0cb729ebc440c1ad913a22316f64 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Nov 2022 11:37:29 -0800 Subject: [PATCH 2/5] Remove symbol table passes. (#1932) --- cprover_bindings/src/goto_program/mod.rs | 1 - .../gen_c_transformer/expr_transformer.rs | 264 ------ .../gen_c_transformer/mod.rs | 10 - .../gen_c_transformer/name_transformer.rs | 264 ------ .../gen_c_transformer/nondet_transformer.rs | 138 ---- .../identity_transformer.rs | 430 ---------- .../goto_program/symtab_transformer/mod.rs | 11 - .../goto_program/symtab_transformer/passes.rs | 27 - .../symtab_transformer/transformer.rs | 774 ------------------ kani-compiler/kani_queries/src/lib.rs | 12 - .../compiler_interface.rs | 10 +- kani-compiler/src/main.rs | 3 - kani-compiler/src/parser.rs | 12 - kani-driver/src/args.rs | 8 - 14 files changed, 3 insertions(+), 1961 deletions(-) delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/mod.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/passes.rs delete mode 100644 cprover_bindings/src/goto_program/symtab_transformer/transformer.rs diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index e72c66414f32..15c0282f9a40 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -13,7 +13,6 @@ mod location; mod stmt; mod symbol; mod symbol_table; -pub mod symtab_transformer; mod typ; pub use builtin::BuiltinFn; diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs deleted file mode 100644 index 54a0a2ab5f15..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs +++ /dev/null @@ -1,264 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::ops::{BitAnd, Shl, Shr}; - -use super::super::Transformer; -use crate::goto_program::{ - BinaryOperator, CIntType, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, SymbolValues, - Type, -}; -use crate::InternedString; -use num::bigint::BigInt; -use std::collections::HashMap; - -/// 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: HashMap, -} - -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: HashMap::default() } - .transform_symbol_table(original_symbol_table) - } - - /// Extract `empty_statics` map for final processing. - fn empty_statics_owned(&mut self) -> HashMap { - std::mem::take(&mut self.empty_statics) - } - - /// 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, name, 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: &BinaryOperator, - lhs: &Expr, - rhs: &Expr, - ) -> Expr { - let lhs = self.transform_expr(lhs); - let rhs = self.transform_expr(rhs); - - match op { - BinaryOperator::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/kani/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, 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_".into(); - new_symbol.base_name = Some("main_".into()); - new_symbol.pretty_name = Some("main_".into()); - - 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())), - "main", - Location::none(), - ); - - self.mut_symbol_table().insert(new_main); - } -} diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs deleted file mode 100644 index 7d54b791a296..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright Kani Contributors -// 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/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs deleted file mode 100644 index bfe1f84f588b..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.rs +++ /dev/null @@ -1,264 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use super::super::Transformer; -use crate::goto_program::{ - DatatypeComponent, Expr, Location, Parameter, Stmt, Symbol, SymbolTable, Type, -}; -use crate::InternedString; -use std::collections::{HashMap, HashSet}; -/// 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. - // TODO: use InternedString to save memory. - mapped_names: HashMap, - used_names: HashSet, -} - -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: HashMap::default(), - used_names: HashSet::default(), - } - .transform_symbol_table(original_symbol_table) - } - - fn normalize_identifier(&mut self, orig_name: InternedString) -> InternedString { - self.normalize_identifier_inner(&orig_name.to_string()).into() - } - - /// Converts an arbitrary identifier into a valid C identifier. - fn normalize_identifier_inner(&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 let Some(tag) = orig_name.strip_prefix("tag-") { - ("tag-", tag) - } 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/kani/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); - } - } - - 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 { - self.transform_type(parameter.typ()).as_parameter( - parameter.identifier().map(|name| self.normalize_identifier(name)), - parameter.base_name().map(|name| self.normalize_identifier(name)), - ) - } - - /// Normalize field names. - fn transform_expr_member(&mut self, _typ: &Type, lhs: &Expr, field: InternedString) -> 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: InternedString) -> 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: InternedString) -> 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: InternedString) -> Type { - Type::incomplete_struct(self.normalize_identifier(tag)) - } - - /// Normalize incomplete union tag name. - fn transform_type_incomplete_union(&mut self, tag: InternedString) -> 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(self.normalize_identifier(*name), self.transform_type(typ)) - } - DatatypeComponent::Padding { name, bits } => { - DatatypeComponent::padding(self.normalize_identifier(*name), *bits) - } - } - } - - /// Normalize struct type name. - fn transform_type_struct( - &mut self, - tag: InternedString, - 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: InternedString) -> Type { - Type::struct_tag_raw(self.normalize_identifier(tag)) - } - - /// Normalize union type name. - fn transform_type_union( - &mut self, - tag: InternedString, - 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: InternedString) -> Type { - Type::union_tag_raw(self.normalize_identifier(tag)) - } - - /// Normalize goto label name. - fn transform_stmt_goto(&mut self, label: InternedString) -> Stmt { - Stmt::goto(self.normalize_identifier(label), Location::none()) - } - - /// Normalize label name. - fn transform_stmt_label(&mut self, label: InternedString, 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/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs deleted file mode 100644 index 35533989ab8a..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs +++ /dev/null @@ -1,138 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use super::super::Transformer; -use crate::goto_program::{Expr, Location, Stmt, Symbol, SymbolTable, Type}; -use std::collections::HashMap; - -/// Struct for handling the nondet transformations for --gen-c-runnable. -pub struct NondetTransformer { - new_symbol_table: SymbolTable, - nondet_types: HashMap, -} - -// Note: this replaces every occurence of a Nondet expression by an equivalent function call. -// Since the introduction of StmtBody::Deinit, some Nondet expressions only appear -// at Irep generating time. Such expressions will not be substituted by this transformer. - -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: HashMap::default() } - .transform_symbol_table(original_symbol_table) - } - - /// Extract `nondet_types` map for final processing. - pub fn nondet_types_owned(&mut self) -> HashMap { - std::mem::take(&mut self.nondet_types) - } -} - -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 = transformed_typ.lookup_components(self.symbol_table()).unwrap().clone(); - let transformed_values: Vec<_> = fields - .into_iter() - .zip(values.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, 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), &identifier, Location::none()); - self.mut_symbol_table().insert(func_sym); - } - } -} diff --git a/cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs deleted file mode 100644 index 074117a0f548..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs +++ /dev/null @@ -1,430 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use super::Transformer; -use crate::goto_program::SymbolTable; -/// Struct for performing the identity transformation on a symbol table. -/// Mainly used as a demo/for testing. -pub struct IdentityTransformer { - new_symbol_table: SymbolTable, -} - -impl IdentityTransformer { - /// Perform an identity transformation on the given symbol table. - pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable { - let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone()); - IdentityTransformer { new_symbol_table }.transform_symbol_table(original_symbol_table) - } -} - -impl Transformer for IdentityTransformer { - /// 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 - } -} - -#[cfg(test)] -mod tests { - use super::{ - super::super::{ - DatatypeComponent, Expr, Location, Stmt, SwitchCase, Symbol, SymbolTable, Type, - }, - IdentityTransformer, - }; - use crate::machine_model::test_util::machine_model_test_stub; - - fn empty_symtab() -> SymbolTable { - SymbolTable::new(machine_model_test_stub()) - } - - fn assert_transform_eq(original: SymbolTable) { - let transformed = IdentityTransformer::transform(&original); - assert_eq!(original.to_irep(), transformed.to_irep()); - } - - #[test] - fn empty() { - let original = empty_symtab(); - assert_transform_eq(original); - } - - #[test] - fn types() { - let mut original = empty_symtab(); - let mut curr_var = 0; - { - let mut add_sym = |typ| { - let name = curr_var.to_string(); - original.insert(Symbol::typedef(&name, &name, typ, Location::none())); - curr_var += 1; - }; - add_sym(Type::bool().array_of(3)); - add_sym(Type::float().array_of(5)); - add_sym(Type::bool()); - add_sym(Type::signed_int(16).as_bitfield(8)); - add_sym(Type::c_int()); - add_sym(Type::c_bool()); - add_sym(Type::c_char()); - add_sym(Type::code_with_unnamed_parameters( - vec![Type::bool(), Type::c_int()], - Type::float(), - )); - add_sym(Type::constructor()); - add_sym(Type::double()); - add_sym(Type::empty()); - add_sym(Type::double().flexible_array_of()); - add_sym(Type::float()); - add_sym(Type::incomplete_struct("a")); - add_sym(Type::incomplete_union("b")); - add_sym(Type::float().infinite_array_of()); - add_sym(Type::double().to_pointer()); - add_sym(Type::signed_int(8)); - add_sym(Type::empty_struct("c")); - add_sym(Type::struct_tag("d")); - add_sym(Type::empty_union("e")); - add_sym(Type::union_tag("f")); - add_sym(Type::unsigned_int(8)); - add_sym(Type::variadic_code_with_unnamed_parameters( - vec![Type::float(), Type::c_int()], - Type::signed_int(8), - )); - add_sym(Type::vector(Type::double(), 6)); - } - - assert_transform_eq(original); - } - - #[test] - fn struct_types() { - let mut original = empty_symtab(); - let mut curr_var = 0; - { - let mut add_sym = |typ| { - let name = curr_var.to_string(); - original.insert(Symbol::typedef(&name, &name, typ, Location::none())); - curr_var += 1; - }; - - let struct_tag = Type::struct_tag("s-t"); - add_sym(struct_tag); - - let incomplete_struct = Type::incomplete_struct("i-s"); - add_sym(incomplete_struct); - - let struct_type = Type::struct_type( - "s", - vec![ - DatatypeComponent::field("a", Type::float()), - DatatypeComponent::padding("b", 4), - DatatypeComponent::field("c", Type::double()), - DatatypeComponent::padding("d", 5), - DatatypeComponent::field("e", Type::c_int()), - DatatypeComponent::padding("f", 6), - ], - ); - add_sym(struct_type); - } - - assert_transform_eq(original); - } - - #[test] - fn union_types() { - let mut original = empty_symtab(); - let mut curr_var = 0; - { - let mut add_sym = |typ| { - let name = curr_var.to_string(); - original.insert(Symbol::typedef(&name, &name, typ, Location::none())); - curr_var += 1; - }; - - let union_tag = Type::union_tag("u-t"); - add_sym(union_tag); - - let incomplete_union = Type::incomplete_union("i-u"); - add_sym(incomplete_union); - - let union_type = Type::union_type( - "u", - vec![ - DatatypeComponent::field("a", Type::float()), - DatatypeComponent::field("c", Type::double()), - DatatypeComponent::field("e", Type::c_int()), - ], - ); - add_sym(union_type); - } - - assert_transform_eq(original); - } - - #[test] - fn exprs() { - let mut original = empty_symtab(); - let mut curr_var = 0; - { - let mut add_sym = |value| { - let name = curr_var.to_string(); - original.insert(Symbol::constant(&name, &name, &name, value, Location::none())); - curr_var += 1; - }; - - add_sym(Expr::symbol_expression("a".to_string(), Type::c_int()).address_of()); - add_sym(Expr::int_constant(5, Type::c_int()).array_constant(10)); - add_sym(Expr::array_expr( - Type::bool().array_of(2), - vec![Expr::bool_true(), Expr::bool_false()], - )); - add_sym(Expr::bool_constant(true)); - add_sym(Expr::bool_false()); - add_sym(Expr::bool_true()); - add_sym(Expr::c_bool_constant(true)); - add_sym(Expr::c_false()); - add_sym(Expr::c_true()); - add_sym(Expr::c_true().cast_to(Type::c_int())); - add_sym( - Expr::symbol_expression("a".to_string(), Type::c_int()).address_of().dereference(), - ); - add_sym(Expr::double_constant(1.0)); - add_sym(Expr::float_constant(1.0)); - add_sym( - Expr::array_expr( - Type::bool().array_of(2), - vec![Expr::bool_true(), Expr::bool_false()], - ) - .index_array(Expr::int_constant(1, Type::c_int())), - ); - add_sym(Expr::int_constant(1, Type::c_int())); - add_sym( - Expr::symbol_expression( - "a".to_string(), - Type::code_with_unnamed_parameters( - vec![Type::bool(), Type::float()], - Type::double(), - ), - ) - .call(vec![Expr::bool_true(), Expr::float_constant(1.0)]), - ); - add_sym(Expr::nondet(Type::bool())); - add_sym(Expr::pointer_constant(128, Type::bool().to_pointer())); - add_sym(Expr::statement_expression( - vec![ - Stmt::skip(Location::none()), - Stmt::code_expression(Expr::float_constant(1.0), Location::none()), - ], - Type::float(), - )); - add_sym(Expr::symbol_expression("x".to_string(), Type::bool())); - add_sym( - Expr::bool_true().ternary(Expr::float_constant(1.0), Expr::float_constant(2.0)), - ); - add_sym( - Expr::int_constant(1, Type::c_int()) - .add_overflow_p(Expr::int_constant(2, Type::c_int())), - ); - add_sym(Expr::bool_true().and(Expr::bool_false())); - add_sym(Expr::int_constant(1, Type::c_int()).postincr()); - add_sym(Expr::bool_true().not()); - } - assert_transform_eq(original); - } - - #[test] - fn struct_exprs() { - let mut original = empty_symtab(); - - let struct_type = Symbol::struct_type( - "s", - "s".into(), - vec![ - DatatypeComponent::field("a", Type::float()), - DatatypeComponent::padding("b", 4), - DatatypeComponent::field("c", Type::double()), - DatatypeComponent::padding("d", 5), - DatatypeComponent::field("e", Type::c_int()), - DatatypeComponent::padding("f", 6), - ], - ); - original.insert(struct_type); - - let struct_expr = Expr::struct_expr_from_values( - Type::struct_tag("s"), - vec![ - Expr::float_constant(1.0), - Expr::double_constant(2.0), - Expr::int_constant(3, Type::c_int()), - ], - &original, - ); - - original.insert(Symbol::constant("se", "se", "se", struct_expr.clone(), Location::none())); - - let struct_member = struct_expr.member("a", &original); - original.insert(Symbol::constant("sm", "sm", "sm", struct_member, Location::none())); - - assert_transform_eq(original); - } - - #[test] - fn union_exprs() { - let mut original = empty_symtab(); - - let union_type = Symbol::union_type( - "u", - "u", - vec![ - DatatypeComponent::field("a", Type::float()), - DatatypeComponent::field("c", Type::double()), - DatatypeComponent::field("e", Type::c_int()), - ], - ); - original.insert(union_type); - - let union_expr = - Expr::union_expr(Type::union_tag("u"), "a", Expr::float_constant(1.0), &original); - - original.insert(Symbol::constant("ue", "ue", "ue", union_expr.clone(), Location::none())); - - let union_member = union_expr.member("a", &original); - original.insert(Symbol::constant("um", "um", "um", union_member, Location::none())); - - assert_transform_eq(original); - } - - #[test] - fn transmute_to_expr() { - let mut original = empty_symtab(); - let sym = Symbol::constant( - "transmuted", - "transmuted", - "transmuted", - Expr::array_expr(Type::c_int().array_of(1), vec![Expr::int_constant(3, Type::c_int())]) - .transmute_to(Type::c_int(), &original), - Location::none(), - ); - original.insert(sym); - - assert_transform_eq(original); - } - - #[test] - fn stmts() { - let mut original = empty_symtab(); - let mut curr_var = 0; - { - let mut add_sym = |body| { - let name = curr_var.to_string(); - original.insert(Symbol::function( - &name, - Type::code_with_unnamed_parameters(vec![], Type::empty()), - Some(body), - &name, - Location::none(), - )); - curr_var += 1; - }; - - add_sym(Stmt::assign( - Expr::symbol_expression("a".to_string(), Type::bool()), - Expr::bool_true(), - Location::none(), - )); - add_sym(Stmt::assert(Expr::bool_true(), "a", "a", Location::none())); - add_sym(Stmt::assume(Expr::bool_false(), Location::none())); - add_sym(Stmt::atomic_block( - vec![Stmt::assert_false("a", "a", Location::none())], - Location::none(), - )); - add_sym(Stmt::block( - vec![Stmt::assert_false("a", "a", Location::none())], - Location::none(), - )); - add_sym(Stmt::break_stmt(Location::none())); - add_sym(Stmt::continue_stmt(Location::none())); - add_sym(Stmt::decl( - Expr::symbol_expression("a".to_string(), Type::bool()), - Some(Expr::bool_true()), - Location::none(), - )); - add_sym(Stmt::code_expression(Expr::bool_true(), Location::none())); - add_sym(Stmt::for_loop( - Stmt::decl( - Expr::symbol_expression("a".to_string(), Type::bool()), - Some(Expr::bool_true()), - Location::none(), - ), - Expr::bool_true(), - Stmt::assign( - Expr::symbol_expression("a".to_string(), Type::bool()), - Expr::bool_false(), - Location::none(), - ), - Stmt::continue_stmt(Location::none()), - Location::none(), - )); - add_sym(Stmt::function_call( - Some(Expr::symbol_expression("a".to_string(), Type::bool())), - Expr::symbol_expression( - "b".to_string(), - Type::code_with_unnamed_parameters(vec![Type::c_int()], Type::bool()), - ), - vec![Expr::int_constant(5, Type::c_int())], - Location::none(), - )); - add_sym(Stmt::goto("tag1".to_string(), Location::none())); - add_sym(Stmt::if_then_else( - Expr::bool_true(), - Stmt::continue_stmt(Location::none()), - Some(Stmt::continue_stmt(Location::none())), - Location::none(), - )); - add_sym(Stmt::ret(Some(Expr::bool_true()), Location::none())); - add_sym(Stmt::skip(Location::none())); - add_sym(Stmt::switch( - Expr::int_constant(3, Type::c_int()), - vec![ - SwitchCase::new( - Expr::int_constant(1, Type::c_int()), - Stmt::ret(None, Location::none()), - ), - SwitchCase::new( - Expr::int_constant(2, Type::c_int()), - Stmt::ret(None, Location::none()), - ), - SwitchCase::new( - Expr::int_constant(3, Type::c_int()), - Stmt::ret(None, Location::none()), - ), - SwitchCase::new( - Expr::int_constant(4, Type::c_int()), - Stmt::ret(None, Location::none()), - ), - ], - Some(Stmt::goto("tag1".to_string(), Location::none())), - Location::none(), - )); - add_sym(Stmt::while_loop( - Expr::bool_true(), - Stmt::skip(Location::none()), - Location::none(), - )); - add_sym( - Stmt::assert_false("tag1", "tag1", Location::none()).with_label("tag1".to_string()), - ); - } - - assert_transform_eq(original); - } -} diff --git a/cprover_bindings/src/goto_program/symtab_transformer/mod.rs b/cprover_bindings/src/goto_program/symtab_transformer/mod.rs deleted file mode 100644 index 1ffa48f0f156..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/mod.rs +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright Kani Contributors -// 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; - -pub use passes::do_passes; -use transformer::Transformer; diff --git a/cprover_bindings/src/goto_program/symtab_transformer/passes.rs b/cprover_bindings/src/goto_program/symtab_transformer/passes.rs deleted file mode 100644 index 9211e6025066..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/passes.rs +++ /dev/null @@ -1,27 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use super::gen_c_transformer::{ExprTransformer, NameTransformer, NondetTransformer}; -use super::identity_transformer::IdentityTransformer; -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 { - 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); - NameTransformer::transform(&symtab) - } - "identity" => IdentityTransformer::transform(&symtab), - _ => panic!("Invalid symbol table transformation: {pass_name}"), - } - } - - symtab -} diff --git a/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs deleted file mode 100644 index 0518633a78ed..000000000000 --- a/cprover_bindings/src/goto_program/symtab_transformer/transformer.rs +++ /dev/null @@ -1,774 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use crate::goto_program::{ - BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, - SelfOperator, Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type, - UnaryOperator, -}; -use crate::InternedString; -use num::bigint::BigInt; -use std::collections::HashSet; - -/// The `Transformer` trait is a visitor pattern for the `SymbolTable`. -/// To use it, you just need to implement the three symbol table accessor methods, -/// and then override any methods that you want to change the behavior of. -/// -/// The entry point is `transform_symbol_table`. The transformer then: -/// - calls `preprocess` -/// - transforms and inserts type symbols -/// - transforms and inserts expr/stmt symbols -/// - calls `postprocess` -/// -/// To transform a symbol, we call `transform_type` on its type, -/// and then `transform_value` on its value, which redirects to -/// either `transform_expr` or `transform_stmt`. -/// -/// The three methods `transform_type`, `transform_expr`, and `transform_stmt` -/// perform a recursive descent on their corresponding structures. -/// They default to just reconstruct the structure, but can be overridden. -pub trait Transformer: Sized { - /// Get reference to symbol table. - fn symbol_table(&self) -> &SymbolTable; - /// Get mutable reference to symbol table. - fn mut_symbol_table(&mut self) -> &mut SymbolTable; - /// Get owned symbol table. - fn extract_symbol_table(self) -> SymbolTable; - - /// 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(&mut self, typ: &Type) -> Type { - match typ { - Type::Array { typ, size } => self.transform_type_array(typ, size), - Type::Bool => self.transform_type_bool(), - Type::CBitField { typ, width } => self.transform_type_c_bit_field(typ, width), - Type::CInteger(c_int_type) => self.transform_type_c_integer(c_int_type), - Type::Code { parameters, return_type } => { - self.transform_type_code(parameters, return_type) - } - Type::Constructor => self.transform_type_constructor(), - Type::Double => self.transform_type_double(), - Type::Empty => self.transform_type_empty(), - Type::FlexibleArray { typ } => self.transform_type_flexible_array(typ), - Type::Float => self.transform_type_float(), - Type::IncompleteStruct { tag } => self.transform_type_incomplete_struct(*tag), - Type::IncompleteUnion { tag } => self.transform_type_incomplete_union(*tag), - Type::InfiniteArray { typ } => self.transform_type_infinite_array(typ), - Type::Integer => self.transform_type_integer(), - Type::Pointer { typ } => self.transform_type_pointer(typ), - 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), - Type::VariadicCode { parameters, return_type } => { - self.transform_type_variadic_code(parameters, return_type) - } - Type::Vector { typ, size } => self.transform_type_vector(typ, size), - } - } - - /// Transforms an array type (`typ x[size]`) - fn transform_type_array(&mut self, typ: &Type, size: &u64) -> Type { - let transformed_typ = self.transform_type(typ); - transformed_typ.array_of(*size) - } - - /// Transforms a CPROVER boolean type (`__CPROVER_bool x`) - fn transform_type_bool(&mut self) -> Type { - Type::bool() - } - - /// Transforms a c bit field type (`typ x : width`) - fn transform_type_c_bit_field(&mut self, typ: &Type, width: &u64) -> Type { - let transformed_typ = self.transform_type(typ); - transformed_typ.as_bitfield(*width) - } - - /// Transforms a machine-dependent integer type (`bool`, `char`, `int`, `size_t`) - 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(), - CIntType::Int => Type::c_int(), - CIntType::SizeT => Type::size_t(), - CIntType::SSizeT => Type::ssize_t(), - } - } - - /// Transforms a parameter for a function - fn transform_type_parameter(&mut self, parameter: &Parameter) -> Parameter { - self.transform_type(parameter.typ()) - .as_parameter(parameter.identifier(), parameter.base_name()) - } - - /// Transforms a function type (`return_type x(parameters)`) - fn transform_type_code(&mut self, parameters: &[Parameter], return_type: &Type) -> Type { - let transformed_parameters = - parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect(); - let transformed_return_type = self.transform_type(return_type); - Type::code(transformed_parameters, transformed_return_type) - } - - /// Transforms a constructor type (`__attribute__(constructor)`) - fn transform_type_constructor(&mut self) -> Type { - Type::constructor() - } - - /// Transforms a double type (`double`) - fn transform_type_double(&mut self) -> Type { - Type::double() - } - - /// Transforms an empty type (`void`) - fn transform_type_empty(&mut self) -> Type { - Type::empty() - } - - /// Transforms a flexible array type (`typ x[]`) - fn transform_type_flexible_array(&mut self, typ: &Type) -> Type { - let transformed_typ = self.transform_type(typ); - Type::flexible_array_of(transformed_typ) - } - - /// Transforms a float type (`float`) - fn transform_type_float(&mut self) -> Type { - Type::float() - } - - /// Transforms an incomplete struct type (`struct x {}`) - fn transform_type_incomplete_struct(&mut self, tag: InternedString) -> Type { - Type::incomplete_struct(tag) - } - - /// Transforms an incomplete union type (`union x {}`) - fn transform_type_incomplete_union(&mut self, tag: InternedString) -> Type { - Type::incomplete_union(tag) - } - - /// Transforms an infinite array type (`typ x[__CPROVER_infinity()]`) - fn transform_type_infinite_array(&mut self, typ: &Type) -> Type { - let transformed_typ = self.transform_type(typ); - transformed_typ.infinite_array_of() - } - - /// Transforms a CPROVER integer type - fn transform_type_integer(&mut self) -> Type { - Type::integer() - } - - /// Transforms a pointer type (`typ*`) - fn transform_type_pointer(&mut self, typ: &Type) -> Type { - let transformed_typ = self.transform_type(typ); - transformed_typ.to_pointer() - } - - /// Transforms a signed bitvector type (`int_t`) - fn transform_type_signedbv(&mut self, width: &u64) -> Type { - Type::signed_int(*width) - } - - /// Transforms a datatype component - fn transform_datatype_component(&mut self, component: &DatatypeComponent) -> DatatypeComponent { - match component { - DatatypeComponent::Field { name, typ } => { - DatatypeComponent::field(*name, self.transform_type(typ)) - } - DatatypeComponent::Padding { name, bits } => DatatypeComponent::padding(*name, *bits), - } - } - - /// Transforms a struct type (`struct tag {component1.typ component1.name; component2.typ component2.name ... }`) - fn transform_type_struct( - &mut self, - tag: InternedString, - components: &[DatatypeComponent], - ) -> Type { - let transformed_components = components - .iter() - .map(|component| self.transform_datatype_component(component)) - .collect(); - Type::struct_type(tag, transformed_components) - } - - /// Transforms a struct tag type (`tag-`) - fn transform_type_struct_tag(&mut self, tag: InternedString) -> Type { - Type::struct_tag_raw(tag) - } - - /// Transforms a union type (`union tag {component1.typ component1.name; component2.typ component2.name ... }`) - fn transform_type_union( - &mut self, - tag: InternedString, - components: &[DatatypeComponent], - ) -> Type { - let transformed_components = components - .iter() - .map(|component| self.transform_datatype_component(component)) - .collect(); - Type::union_type(tag, transformed_components) - } - - /// Transforms a union tag type (`tag-`) - fn transform_type_union_tag(&mut self, tag: InternedString) -> Type { - Type::union_tag_raw(tag) - } - - /// Transforms an unsigned bitvector type (`uint_t`) - 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( - &mut self, - parameters: &[Parameter], - return_type: &Type, - ) -> Type { - let transformed_parameters = - parameters.iter().map(|parameter| self.transform_type_parameter(parameter)).collect(); - let transformed_return_type = self.transform_type(return_type); - Type::variadic_code(transformed_parameters, transformed_return_type) - } - - /// Transforms a vector type (`typ __attribute__((vector_size (size * sizeof(typ)))) var;`) - fn transform_type_vector(&mut self, typ: &Type, size: &u64) -> Type { - let transformed_typ = self.transform_type(typ); - Type::vector(transformed_typ, *size) - } - - /// Transforms a type def (`typedef typ tag`) - fn transform_type_def(&mut self, tag: InternedString, typ: &Type) -> Type { - let transformed_typ = self.transform_type(typ); - 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. - 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), - ExprValue::Array { elems } => self.transform_expr_array(typ, elems), - ExprValue::ArrayOf { elem } => self.transform_expr_array_of(typ, elem), - ExprValue::Assign { left, right } => self.transform_expr_assign(typ, left, right), - ExprValue::BinOp { op, lhs, rhs } => self.transform_expr_bin_op(typ, op, lhs, rhs), - ExprValue::BoolConstant(value) => self.transform_expr_bool_constant(typ, value), - ExprValue::ByteExtract { e, offset } => { - self.transform_expr_byte_extract(typ, e, offset) - } - ExprValue::CBoolConstant(value) => self.transform_expr_c_bool_constant(typ, value), - ExprValue::Dereference(child) => self.transform_expr_dereference(typ, child), - ExprValue::DoubleConstant(value) => self.transform_expr_double_constant(typ, value), - ExprValue::EmptyUnion => self.transform_expr_empty_union(typ), - ExprValue::FloatConstant(value) => self.transform_expr_float_constant(typ, value), - ExprValue::FunctionCall { function, arguments } => { - self.transform_expr_function_call(typ, function, arguments) - } - ExprValue::If { c, t, e } => self.transform_expr_if(typ, c, t, e), - ExprValue::Index { array, index } => self.transform_expr_index(typ, array, index), - ExprValue::IntConstant(value) => self.transform_expr_int_constant(typ, value), - ExprValue::Member { lhs, field } => self.transform_expr_member(typ, lhs, *field), - ExprValue::Nondet => self.transform_expr_nondet(typ), - ExprValue::PointerConstant(value) => self.transform_expr_pointer_constant(typ, value), - ExprValue::SelfOp { op, e } => self.transform_expr_self_op(typ, op, e), - ExprValue::StatementExpression { statements } => { - self.transform_expr_statement_expression(typ, statements) - } - ExprValue::StringConstant { s } => self.transform_expr_string_constant(typ, *s), - ExprValue::Struct { values } => self.transform_expr_struct(typ, values), - ExprValue::Symbol { identifier } => self.transform_expr_symbol(typ, *identifier), - ExprValue::Typecast(child) => self.transform_expr_typecast(typ, child), - ExprValue::Union { value, field } => self.transform_expr_union(typ, value, *field), - ExprValue::UnOp { op, e } => self.transform_expr_un_op(typ, op, e), - ExprValue::Vector { elems } => self.transform_expr_vector(typ, elems), - } - .with_location(*e.location()) - } - - /// Transforms a reference expr (`&self`) - 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(&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(&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(&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 { - transformed_elem.array_constant(size) - } else { - unreachable!() - } - } - - /// Transform an assign expr (`left = right`) - /// Currently not able to be constructed, as does not exist in Rust - 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( - &mut self, - _typ: &Type, - op: &BinaryOperator, - lhs: &Expr, - rhs: &Expr, - ) -> Expr { - let lhs = self.transform_expr(lhs); - let rhs = self.transform_expr(rhs); - - lhs.binop(*op, rhs) - } - - /// Transforms a CPROVER boolean expression (`(__CPROVER_bool) >>> true/false <<<`) - 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(&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(&mut self, _typ: &Type, value: &bool) -> Expr { - Expr::c_bool_constant(*value) - } - - /// Transforms a deref expr (`*self`) - 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(&mut self, _typ: &Type, value: &f64) -> Expr { - Expr::double_constant(*value) - } - - /// Transforms an empty union expr (`{}`) - fn transform_expr_empty_union(&mut self, typ: &Type) -> Expr { - Expr::empty_union(typ.clone(), self.symbol_table()) - } - - /// Transforms a float constant expr (`1.0f`) - 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( - &mut self, - _typ: &Type, - function: &Expr, - arguments: &[Expr], - ) -> Expr { - let transformed_function = self.transform_expr(function); - let transformed_arguments = - arguments.iter().map(|argument| self.transform_expr(argument)).collect(); - transformed_function.call(transformed_arguments) - } - - /// Transforms an if expr (`c ? t : e`) - 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); - transformed_c.ternary(transformed_t, transformed_e) - } - - /// Transforms an array index expr (`array[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(&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(&mut self, _typ: &Type, lhs: &Expr, field: InternedString) -> Expr { - let transformed_lhs = self.transform_expr(lhs); - transformed_lhs.member(field, self.symbol_table()) - } - - 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(&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(&mut self, _typ: &Type, op: &SelfOperator, e: &Expr) -> Expr { - let transformed_e = self.transform_expr(e); - match op { - SelfOperator::Postdecrement => transformed_e.postdecr(), - SelfOperator::Postincrement => transformed_e.postincr(), - SelfOperator::Predecrement => transformed_e.predecr(), - SelfOperator::Preincrement => transformed_e.preincr(), - } - } - - /// Transforms a statement expr (({ stmt1; stmt2; ...})) - 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(); - Expr::statement_expression(transformed_statements, transformed_typ) - } - - /// Transforms a string constant expr (`"s"`) - fn transform_expr_string_constant(&mut self, _typ: &Type, value: InternedString) -> Expr { - Expr::raw_string_constant(value) - } - - /// Transforms a struct initializer expr (`struct foo the_foo = >>> {field1, field2, ... } <<<`) - 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 - ); - let transformed_values: Vec<_> = - values.iter().map(|value| self.transform_expr(value)).collect(); - Expr::struct_expr_from_padded_values( - transformed_typ, - transformed_values, - self.symbol_table(), - ) - } - - /// Transforms a symbol expr (`self`) - fn transform_expr_symbol(&mut self, typ: &Type, identifier: InternedString) -> Expr { - let transformed_typ = self.transform_type(typ); - Expr::symbol_expression(identifier, transformed_typ) - } - - /// Transforms a typecast expr (`(typ) self`) - 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(&mut self, typ: &Type, value: &Expr, field: InternedString) -> 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(&mut self, _typ: &Type, op: &UnaryOperator, e: &Expr) -> Expr { - let transformed_e = self.transform_expr(e); - match op { - UnaryOperator::Bitnot => transformed_e.bitnot(), - UnaryOperator::BitReverse => transformed_e.bitreverse(), - UnaryOperator::Bswap => transformed_e.bswap(), - UnaryOperator::IsDynamicObject => transformed_e.dynamic_object(), - UnaryOperator::IsFinite => transformed_e.is_finite(), - UnaryOperator::Not => transformed_e.not(), - UnaryOperator::ObjectSize => transformed_e.object_size(), - UnaryOperator::PointerObject => transformed_e.pointer_object(), - UnaryOperator::PointerOffset => transformed_e.pointer_offset(), - UnaryOperator::Popcount => transformed_e.popcount(), - UnaryOperator::CountTrailingZeros { allow_zero } => transformed_e.cttz(*allow_zero), - UnaryOperator::CountLeadingZeros { allow_zero } => transformed_e.ctlz(*allow_zero), - UnaryOperator::UnaryMinus => transformed_e.neg(), - } - } - - /// 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(&mut self, stmt: &Stmt) -> Stmt { - match stmt.body() { - StmtBody::Assign { lhs, rhs } => self.transform_stmt_assign(lhs, rhs), - StmtBody::Assert { cond, property_class, msg } => { - self.transform_stmt_assert(cond, *property_class, *msg) - } - StmtBody::Assume { cond } => self.transform_stmt_assume(cond), - StmtBody::AtomicBlock(block) => self.transform_stmt_atomic_block(block), - StmtBody::Block(block) => self.transform_stmt_block(block), - StmtBody::Break => self.transform_stmt_break(), - StmtBody::Continue => self.transform_stmt_continue(), - StmtBody::Decl { lhs, value } => self.transform_stmt_decl(lhs, value), - StmtBody::Deinit(place) => self.transform_stmt_deinit(place), - StmtBody::Expression(expr) => self.transform_stmt_expression(expr), - StmtBody::For { init, cond, update, body } => { - self.transform_stmt_for(init, cond, update, body) - } - StmtBody::FunctionCall { lhs, function, arguments } => { - self.transform_stmt_function_call(lhs, function, arguments) - } - StmtBody::Goto(label) => self.transform_stmt_goto(*label), - StmtBody::Ifthenelse { i, t, e } => self.transform_stmt_ifthenelse(i, t, e), - StmtBody::Label { label, body } => self.transform_stmt_label(*label, body), - StmtBody::Return(value) => self.transform_stmt_return(value), - StmtBody::Skip => self.transform_stmt_skip(), - StmtBody::Switch { control, cases, default } => { - self.transform_stmt_switch(control, cases, default) - } - StmtBody::While { cond, body } => self.transform_stmt_while(cond, body), - } - .with_location(*stmt.location()) - } - - /// Transforms an assign stmt (`lhs = rhs;`) - 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 assert stmt (`Assert(cond, property_class, message);`) - fn transform_stmt_assert( - &mut self, - cond: &Expr, - property_name: InternedString, - msg: InternedString, - ) -> Stmt { - let transformed_cond = self.transform_expr(cond); - Stmt::assert( - transformed_cond, - property_name.to_string().as_str(), - msg.to_string().as_str(), - Location::none(), - ) - } - - /// Transforms a CPROVER assume stmt (`__CPROVER_assume(cond);`) - 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(&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(&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(&mut self) -> Stmt { - Stmt::break_stmt(Location::none()) - } - - /// Transform a continue stmt (`continue;`) - 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(&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()) - } - - fn transform_stmt_deinit(&mut self, place: &Expr) -> Stmt { - let transformed_place = self.transform_expr(place); - Stmt::deinit(transformed_place, Location::none()) - } - - /// Transform an expression stmt (`e;`) - 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(&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); - let transformed_body = self.transform_stmt(body); - - Stmt::for_loop( - transformed_init, - transformed_cond, - transformed_update, - transformed_body, - Location::none(), - ) - } - - /// Transforms a function call stmt (`lhs = function(arguments);` or `function(arguments);`) - fn transform_stmt_function_call( - &mut self, - lhs: &Option, - function: &Expr, - arguments: &[Expr], - ) -> Stmt { - let transformed_lhs = lhs.as_ref().map(|lhs| self.transform_expr(lhs)); - let transformed_function = self.transform_expr(function); - let transformed_arguments = - arguments.iter().map(|argument| self.transform_expr(argument)).collect(); - Stmt::function_call( - transformed_lhs, - transformed_function, - transformed_arguments, - Location::none(), - ) - } - - /// Transforms a goto stmt (`goto dest;`) - fn transform_stmt_goto(&mut self, label: InternedString) -> Stmt { - Stmt::goto(label, Location::none()) - } - - /// Transforms an if-then-else stmt (`if (i) { t } else { e }`) - 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)); - - Stmt::if_then_else(transformed_i, transformed_t, transformed_e, Location::none()) - } - - /// Transforms a label stmt (`label: body`) - fn transform_stmt_label(&mut self, label: InternedString, body: &Stmt) -> Stmt { - let transformed_body = self.transform_stmt(body); - transformed_body.with_label(label) - } - - /// Transforms a return stmt (`return e;` or `return;`) - 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(&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( - &mut self, - control: &Expr, - cases: &[SwitchCase], - default: &Option, - ) -> Stmt { - let transformed_control = self.transform_expr(control); - let transformed_cases = cases - .iter() - .map(|case| { - SwitchCase::new(self.transform_expr(case.case()), self.transform_stmt(case.body())) - }) - .collect(); - let transformed_default = default.as_ref().map(|default| self.transform_stmt(default)); - - Stmt::switch(transformed_control, transformed_cases, transformed_default, Location::none()) - } - - /// Transforms a while loop stmt (`while (cond) { body }`) - 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(&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(); - new_symbol.value = new_value; - new_symbol.typ = new_typ; - new_symbol - } - - /// Transforms a symbol value - fn transform_value(&mut self, value: &SymbolValues) -> SymbolValues { - match value { - SymbolValues::None => SymbolValues::None, - SymbolValues::Expr(expr) => SymbolValues::Expr(self.transform_expr(expr)), - SymbolValues::Stmt(stmt) => SymbolValues::Stmt(self.transform_stmt(stmt)), - } - } - - /// Preprocessing to perform before adding transformed symbols - fn preprocess(&mut self) {} - - /// Postprocessing to perform after adding transformed symbols - fn postprocess(&mut self) {} - - /// Transforms the orig_symtab, producing a new one. - /// See `Transformer` trait documentation for details. - fn transform_symbol_table(mut self, orig_symtab: &SymbolTable) -> SymbolTable { - self.preprocess(); - - let mut added: HashSet = HashSet::default(); - - // New symbol tables come with some items in them by default. Skip over those. - for (name, _symbol) in self.symbol_table().iter() { - added.insert(*name); - } - - // Expr and Stmt symbols might depend on symbols representing types (e.g. struct type). - // Fill in the type symbols first so that these dependencies are in place. - for (name, symbol) in orig_symtab.iter() { - if !self.symbol_table().contains(*name) && symbol.value.is_none() { - let new_symbol = self.transform_symbol(symbol); - self.mut_symbol_table().insert(new_symbol); - added.insert(*name); - } - } - - // Then, fill in everything else. - for (name, symbol) in orig_symtab.iter() { - if !added.contains(name) { - assert!( - !symbol.value.is_none(), - "Symbol should have been inserted in first pass: {:?}", - symbol - ); - let new_symbol = self.transform_symbol(symbol); - self.mut_symbol_table().insert(new_symbol); - } - } - - self.postprocess(); - - self.extract_symbol_table() - } -} diff --git a/kani-compiler/kani_queries/src/lib.rs b/kani-compiler/kani_queries/src/lib.rs index 57cbad644e00..cfb0cff3c8ea 100644 --- a/kani-compiler/kani_queries/src/lib.rs +++ b/kani-compiler/kani_queries/src/lib.rs @@ -37,9 +37,6 @@ impl Default for ReachabilityType { } pub trait UserInput { - fn set_symbol_table_passes(&mut self, passes: Vec); - fn get_symbol_table_passes(&self) -> Vec; - fn set_emit_vtable_restrictions(&mut self, restrictions: bool); fn get_emit_vtable_restrictions(&self) -> bool; @@ -66,7 +63,6 @@ pub trait UserInput { pub struct QueryDb { check_assertion_reachability: AtomicBool, emit_vtable_restrictions: AtomicBool, - symbol_table_passes: Vec, json_pretty_print: AtomicBool, ignore_global_asm: AtomicBool, reachability_analysis: Mutex, @@ -76,14 +72,6 @@ pub struct QueryDb { } impl UserInput for QueryDb { - fn set_symbol_table_passes(&mut self, passes: Vec) { - self.symbol_table_passes = passes; - } - - fn get_symbol_table_passes(&self) -> Vec { - self.symbol_table_passes.clone() - } - fn set_emit_vtable_restrictions(&mut self, restrictions: bool) { self.emit_vtable_restrictions.store(restrictions, Ordering::Relaxed); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index b5a4e5d606c2..82446c72356d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -9,7 +9,7 @@ use crate::kani_middle::reachability::{ collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items, }; use bitflags::_core::any::Any; -use cbmc::goto_program::{symtab_transformer, Location}; +use cbmc::goto_program::Location; use cbmc::{InternedString, MachineModel}; use kani_metadata::KaniMetadata; use kani_queries::{QueryDb, ReachabilityType, UserInput}; @@ -138,10 +138,6 @@ impl CodegenBackend for GotocCodegenBackend { let unsupported_features = gcx.unsupported_metadata(); - // perform post-processing symbol table passes - let passes = self.queries.get_symbol_table_passes(); - let symtab = symtab_transformer::do_passes(gcx.symbol_table, &passes); - // Map MIR types to GotoC types let type_map: BTreeMap = BTreeMap::from_iter(gcx.type_map.into_iter().map(|(k, v)| (k, v.to_string().into()))); @@ -164,7 +160,7 @@ impl CodegenBackend for GotocCodegenBackend { let outputs = tcx.output_filenames(()); let base_filename = outputs.output_path(OutputType::Object); let pretty = self.queries.get_output_pretty_json(); - write_file(&base_filename, "symtab.json", &symtab, pretty); + write_file(&base_filename, "symtab.json", &gcx.symbol_table, pretty); write_file(&base_filename, "type_map.json", &type_map, pretty); write_file(&base_filename, "kani-metadata.json", &metadata, pretty); // If they exist, write out vtable virtual call function pointer restrictions @@ -173,7 +169,7 @@ impl CodegenBackend for GotocCodegenBackend { } symbol_table_to_gotoc(&tcx, &base_filename); } - codegen_results(tcx, rustc_metadata, symtab.machine_model()) + codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()) } fn join_codegen( diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index d9d904c9a551..5d6710f74357 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -92,9 +92,6 @@ fn main() -> Result<(), &'static str> { // Configure queries. let mut queries = QueryDb::default(); - if let Some(symbol_table_passes) = matches.get_raw(parser::SYM_TABLE_PASSES) { - queries.set_symbol_table_passes(symbol_table_passes.map(convert_arg).collect::>()); - } queries.set_emit_vtable_restrictions(matches.get_flag(parser::RESTRICT_FN_PTRS)); queries.set_check_assertion_reachability(matches.get_flag(parser::ASSERTION_REACH_CHECKS)); queries.set_output_pretty_json(matches.get_flag(parser::PRETTY_OUTPUT_FILES)); diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index 1cf3dc261494..4efc8bca2844 100644 --- a/kani-compiler/src/parser.rs +++ b/kani-compiler/src/parser.rs @@ -18,9 +18,6 @@ pub const GOTO_C: &str = "goto-c"; /// Option name used to override Kani library path. pub const KANI_LIB: &str = "kani-lib"; -/// Option name used to select symbol table passes. -pub const SYM_TABLE_PASSES: &str = "symbol-table-passes"; - /// Option name used to set the log output to a json file. pub const JSON_OUTPUT: &str = "json-output"; @@ -86,15 +83,6 @@ pub fn parser() -> Command { .help("Enables compilation to goto-c intermediate representation.") .action(ArgAction::SetTrue), ) - .arg( - Arg::new(SYM_TABLE_PASSES) - .long(SYM_TABLE_PASSES) - .value_name("PASS") - .help("Transformations to perform to the symbol table after it has been generated.") - .value_delimiter(',') - .value_parser(value_parser!(OsString)) // Allow invalid UTF-8 - .action(ArgAction::Append), - ) .arg( Arg::new(LOG_LEVEL) .long(LOG_LEVEL) diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 1a5bb00b6b45..3e3f9a0bdecf 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -241,14 +241,6 @@ pub struct KaniArgs { conflicts_with("concrete_playback") )] pub enable_stubbing: bool, - /* - The below is a "TODO list" of things not yet implemented from the kani_flags.py script. - - 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") - */ } impl KaniArgs { From 7299745141036fc89fdbb2dbc9604c993c7c748f Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 28 Nov 2022 16:17:56 -0500 Subject: [PATCH 3/5] Restore support for some SIMD arithmetic intrinsics (#1931) --- .../codegen/intrinsic.rs | 101 +++++++++++------- .../intrinsics/simd-arith-overflows/expected | 6 ++ .../intrinsics/simd-arith-overflows/main.rs | 30 ++++++ tests/kani/Intrinsics/SIMD/Operators/arith.rs | 39 +++++++ .../Intrinsics/SIMD/Operators/main_fixme.rs | 45 -------- .../Intrinsics/SIMD/Operators/overflow.rs | 40 ------- 6 files changed, 137 insertions(+), 124 deletions(-) create mode 100644 tests/expected/intrinsics/simd-arith-overflows/expected create mode 100644 tests/expected/intrinsics/simd-arith-overflows/main.rs create mode 100644 tests/kani/Intrinsics/SIMD/Operators/arith.rs delete mode 100644 tests/kani/Intrinsics/SIMD/Operators/main_fixme.rs delete mode 100644 tests/kani/Intrinsics/SIMD/Operators/overflow.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ed7529fcf626..9605267bb9db 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -274,40 +274,6 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // Intrinsics which encode a SIMD arithmetic operation with overflow check. - // We expand the overflow check because CBMC overflow operations don't accept array as - // argument. - macro_rules! _codegen_simd_with_overflow_check { - ($op:ident, $overflow:ident) => {{ - let a = fargs.remove(0); - let b = fargs.remove(0); - let mut check = Expr::bool_false(); - if let Type::Vector { size, .. } = a.typ() { - let a_size = size; - if let Type::Vector { size, .. } = b.typ() { - let b_size = size; - assert_eq!(a_size, b_size, "Expected same length vectors",); - for i in 0..*a_size { - // create expression - let index = Expr::int_constant(i, Type::ssize_t()); - let v_a = a.clone().index_array(index.clone()); - let v_b = b.clone().index_array(index); - check = check.or(v_a.$overflow(v_b)); - } - } - } - let check_stmt = self.codegen_assert( - check.not(), - PropertyClass::ArithmeticOverflow, - format!("attempt to compute {} which would overflow", intrinsic).as_str(), - loc, - ); - let res = a.$op(b); - let expr_place = self.codegen_expr_to_place(p, res); - Stmt::block(vec![expr_place, check_stmt], loc) - }}; - } - // Intrinsics which encode a simple wrapping arithmetic operation macro_rules! codegen_wrapping_op { ($f:ident) => {{ codegen_intrinsic_binop!($f) }}; @@ -606,9 +572,14 @@ impl<'tcx> GotocCtx<'tcx> { "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub), "sinf32" => codegen_simple_intrinsic!(Sinf), "sinf64" => codegen_simple_intrinsic!(Sin), - "simd_add" => { - unstable_codegen!(codegen_simd_with_overflow_check!(plus, add_overflow_p)) - } + "simd_add" => self.codegen_simd_op_with_overflow( + Expr::plus, + Expr::add_overflow_p, + fargs, + intrinsic, + p, + loc, + ), "simd_and" => codegen_intrinsic_binop!(bitand), "simd_div" => unstable_codegen!(codegen_intrinsic_binop!(div)), "simd_eq" => self.codegen_simd_cmp(Expr::vector_eq, fargs, p, span, farg_types, ret_ty), @@ -624,7 +595,14 @@ impl<'tcx> GotocCtx<'tcx> { } "simd_le" => self.codegen_simd_cmp(Expr::vector_le, fargs, p, span, farg_types, ret_ty), "simd_lt" => self.codegen_simd_cmp(Expr::vector_lt, fargs, p, span, farg_types, ret_ty), - "simd_mul" => unstable_codegen!(codegen_simd_with_overflow_check!(mul, mul_overflow_p)), + "simd_mul" => self.codegen_simd_op_with_overflow( + Expr::mul, + Expr::mul_overflow_p, + fargs, + intrinsic, + p, + loc, + ), "simd_ne" => { self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty) } @@ -642,7 +620,14 @@ impl<'tcx> GotocCtx<'tcx> { } } // "simd_shuffle#" => handled in an `if` preceding this match - "simd_sub" => unstable_codegen!(codegen_simd_with_overflow_check!(sub, sub_overflow_p)), + "simd_sub" => self.codegen_simd_op_with_overflow( + Expr::sub, + Expr::sub_overflow_p, + fargs, + intrinsic, + p, + loc, + ), "simd_xor" => codegen_intrinsic_binop!(bitxor), "size_of" => codegen_intrinsic_const!(), "size_of_val" => codegen_size_align!(size), @@ -1432,6 +1417,44 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place(p, e) } + /// Intrinsics which encode a SIMD arithmetic operation with overflow check. + /// We expand the overflow check because CBMC overflow operations don't accept array as + /// argument. + fn codegen_simd_op_with_overflow Expr, G: Fn(Expr, Expr) -> Expr>( + &mut self, + op_fun: F, + overflow_fun: G, + mut fargs: Vec, + intrinsic: &str, + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let a = fargs.remove(0); + let b = fargs.remove(0); + + let a_size = a.typ().len().unwrap(); + let b_size = b.typ().len().unwrap(); + assert_eq!(a_size, b_size, "expected same length vectors"); + + let mut check = Expr::bool_false(); + for i in 0..a_size { + // create expression + let index = Expr::int_constant(i, Type::ssize_t()); + let v_a = a.clone().index_array(index.clone()); + let v_b = b.clone().index_array(index); + check = check.or(overflow_fun(v_a, v_b)); + } + let check_stmt = self.codegen_assert_assume( + check.not(), + PropertyClass::ArithmeticOverflow, + format!("attempt to compute {} which would overflow", intrinsic).as_str(), + loc, + ); + let res = op_fun(a, b); + let expr_place = self.codegen_expr_to_place(p, res); + Stmt::block(vec![expr_place, check_stmt], loc) + } + /// simd_shuffle constructs a new vector from the elements of two input vectors, /// choosing values according to an input array of indexes. /// diff --git a/tests/expected/intrinsics/simd-arith-overflows/expected b/tests/expected/intrinsics/simd-arith-overflows/expected new file mode 100644 index 000000000000..55d4cf4c3a72 --- /dev/null +++ b/tests/expected/intrinsics/simd-arith-overflows/expected @@ -0,0 +1,6 @@ +FAILURE\ +attempt to compute simd_add which would overflow +FAILURE\ +attempt to compute simd_sub which would overflow +FAILURE\ +attempt to compute simd_mul which would overflow \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-arith-overflows/main.rs b/tests/expected/intrinsics/simd-arith-overflows/main.rs new file mode 100644 index 000000000000..74cfe8ae878f --- /dev/null +++ b/tests/expected/intrinsics/simd-arith-overflows/main.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test ensures we detect overflows in SIMD arithmetic operations +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub struct i8x2(i8, i8); + +extern "platform-intrinsic" { + fn simd_add(x: T, y: T) -> T; + fn simd_sub(x: T, y: T) -> T; + fn simd_mul(x: T, y: T) -> T; +} + +#[kani::proof] +fn main() { + let a = kani::any(); + let b = kani::any(); + let simd_a = i8x2(a, a); + let simd_b = i8x2(b, b); + + unsafe { + let _ = simd_add(simd_a, simd_b); + let _ = simd_sub(simd_a, simd_b); + let _ = simd_mul(simd_a, simd_b); + } +} diff --git a/tests/kani/Intrinsics/SIMD/Operators/arith.rs b/tests/kani/Intrinsics/SIMD/Operators/arith.rs new file mode 100644 index 000000000000..6af147b826e0 --- /dev/null +++ b/tests/kani/Intrinsics/SIMD/Operators/arith.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test doesn't work because support for SIMD intrinsics isn't available +//! at the moment in Kani. Support to be added in +//! +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, Eq)] +pub struct i8x2(i8, i8); + +extern "platform-intrinsic" { + fn simd_add(x: T, y: T) -> T; + fn simd_sub(x: T, y: T) -> T; + fn simd_mul(x: T, y: T) -> T; +} + +macro_rules! verify_no_overflow { + ($cf: ident, $uf: ident) => {{ + let a: i8 = kani::any(); + let b: i8 = kani::any(); + let checked = a.$cf(b); + kani::assume(checked.is_some()); + let simd_a = i8x2(a, a); + let simd_b = i8x2(b, b); + let unchecked: i8x2 = unsafe { $uf(simd_a, simd_b) }; + assert!(checked.unwrap() == unchecked.0); + assert!(checked.unwrap() == unchecked.1); + }}; +} + +#[kani::proof] +fn test_simd_ops() { + verify_no_overflow!(checked_add, simd_add); + verify_no_overflow!(checked_sub, simd_sub); + verify_no_overflow!(checked_mul, simd_mul); +} diff --git a/tests/kani/Intrinsics/SIMD/Operators/main_fixme.rs b/tests/kani/Intrinsics/SIMD/Operators/main_fixme.rs deleted file mode 100644 index d73e73fa0c4e..000000000000 --- a/tests/kani/Intrinsics/SIMD/Operators/main_fixme.rs +++ /dev/null @@ -1,45 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test doesn't work because support for SIMD intrinsics isn't available -//! at the moment in Kani. Support to be added in -//! -#![feature(repr_simd, platform_intrinsics)] - -#[repr(simd)] -#[allow(non_camel_case_types)] -#[derive(Clone, Copy, PartialEq, Eq)] -pub struct i64x2(i64, i64); - -extern "platform-intrinsic" { - fn simd_add(x: T, y: T) -> T; - fn simd_sub(x: T, y: T) -> T; - fn simd_mul(x: T, y: T) -> T; - fn simd_div(x: T, y: T) -> T; - fn simd_rem(x: T, y: T) -> T; -} - -macro_rules! assert_op { - ($res_op: ident, $simd_op: ident, $x: expr, $y: expr, $($res: expr),+) => { - let $res_op: i64x2 = $simd_op($x, $y); - assert!($res_op == i64x2($($res),+)) - }; -} - -// Tests inspired by Rust's examples in -// https://github.com/rust-lang/rust/blob/0d97f7a96877a96015d70ece41ad08bb7af12377/src/test/ui/simd-intrinsic/simd-intrinsic-generic-arithmetic.rs -#[kani::proof] -fn main() { - let x = i64x2(0, 0); - let y = i64x2(0, 1); - let z = i64x2(1, 2); - let v = i64x2(1, 3); - - unsafe { - assert_op!(res_add, simd_add, x, y, 0, 1); - assert_op!(res_sub, simd_sub, x, y, 0, -1); - assert_op!(res_mul, simd_mul, y, z, 0, 2); - assert_op!(res_div, simd_div, v, z, 1, 1); - assert_op!(res_rem, simd_rem, v, z, 0, 1); - } -} diff --git a/tests/kani/Intrinsics/SIMD/Operators/overflow.rs b/tests/kani/Intrinsics/SIMD/Operators/overflow.rs deleted file mode 100644 index 6747ec708753..000000000000 --- a/tests/kani/Intrinsics/SIMD/Operators/overflow.rs +++ /dev/null @@ -1,40 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-verify-fail -// -// This test ensures that overflow in SIMD operations are detected by Kani. -#![feature(repr_simd, platform_intrinsics)] - -#[repr(simd)] -#[allow(non_camel_case_types)] -#[derive(Clone, Copy, PartialEq, Eq, Debug)] -pub struct i8x2(i8, i8); - -extern "platform-intrinsic" { - fn simd_add(x: T, y: T) -> T; - fn simd_sub(x: T, y: T) -> T; - fn simd_mul(x: T, y: T) -> T; -} - -macro_rules! assert_op { - ($simd_op: ident, $wrap_op: ident, $x: expr, $y: expr) => { - let result = $simd_op($x, $y); - assert!(result.0 == $x.0.$wrap_op($y.0)); - assert!(result.1 == $x.1.$wrap_op($y.1)); - }; -} - -// Tests inspired by Rust's examples in -// https://github.com/rust-lang/rust/blob/0d97f7a96877a96015d70ece41ad08bb7af12377/src/test/ui/simd-intrinsic/simd-intrinsic-generic-arithmetic.rs -#[kani::proof] -fn main() { - let v1 = i8x2(2, 2); - let max_min = i8x2(i8::MIN, i8::MAX); - - unsafe { - assert_op!(simd_add, wrapping_add, v1, max_min); - assert_op!(simd_sub, wrapping_sub, v1, max_min); - assert_op!(simd_mul, wrapping_mul, v1, max_min); - } -} From 79e7795dda0efd85e33b517606f1d6b924b94862 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 28 Nov 2022 14:59:54 -0800 Subject: [PATCH 4/5] Add proof annotation for smack harnesses (#1939) A bunch of the harnesses from the smack testsuite were missing kani::proof annotation. They have the kani-verify-fail tag on them, and because of #1910, they would fail but with a different error than expected. Add #[kani::proof] to them. --- tests/smack/basic/add.rs | 1 + tests/smack/basic/arith_assume3.rs | 1 + tests/smack/basic/div.rs | 1 + tests/smack/basic/mod.rs | 1 + tests/smack/basic/mul.rs | 1 + tests/smack/basic/sub.rs | 1 + tests/smack/functions/closure_fail.rs | 1 + tests/smack/functions/double_fail.rs | 1 + tests/smack/generics/generic_function1.rs | 1 + tests/smack/generics/generic_function2.rs | 1 + tests/smack/generics/generic_function3.rs | 1 + tests/smack/generics/generic_function4.rs | 1 + tests/smack/generics/generic_function5.rs | 1 + tests/smack/overflow/add_overflow.rs | 1 + tests/smack/overflow/mul_overflow.rs | 1 + tests/smack/overflow/sub_overflow.rs | 1 + tests/smack/recursion/fac_fail.rs | 1 + tests/smack/recursion/fib_fail.rs | 1 + tests/smack/structures/option_fail.rs | 1 + tests/smack/structures/point_fail.rs | 1 + tests/smack/vector/vec11.rs | 1 + tests/smack/vector/vec12.rs | 1 + tests/smack/vector/vec13.rs | 1 + tests/smack/vector/vec_resize_fail.rs | 1 + 24 files changed, 24 insertions(+) diff --git a/tests/smack/basic/add.rs b/tests/smack/basic/add.rs index 615142108924..3b463d427dc3 100644 --- a/tests/smack/basic/add.rs +++ b/tests/smack/basic/add.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = 2; let b = 3; diff --git a/tests/smack/basic/arith_assume3.rs b/tests/smack/basic/arith_assume3.rs index ae3cfd4f9caf..042dad7dc8c3 100644 --- a/tests/smack/basic/arith_assume3.rs +++ b/tests/smack/basic/arith_assume3.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = kani::any(); let b = kani::any(); diff --git a/tests/smack/basic/div.rs b/tests/smack/basic/div.rs index ae02844e79af..7e9eb3a79e14 100644 --- a/tests/smack/basic/div.rs +++ b/tests/smack/basic/div.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = 2; let b = 3; diff --git a/tests/smack/basic/mod.rs b/tests/smack/basic/mod.rs index 6aff4d23341d..894b9488c795 100644 --- a/tests/smack/basic/mod.rs +++ b/tests/smack/basic/mod.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = 2; let b = 3; diff --git a/tests/smack/basic/mul.rs b/tests/smack/basic/mul.rs index ba3812797566..e2386cb730aa 100644 --- a/tests/smack/basic/mul.rs +++ b/tests/smack/basic/mul.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = 2; let b = 3; diff --git a/tests/smack/basic/sub.rs b/tests/smack/basic/sub.rs index ec30b339cb7c..be7ec8888b1d 100644 --- a/tests/smack/basic/sub.rs +++ b/tests/smack/basic/sub.rs @@ -3,6 +3,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let a = 2; let b = 3; diff --git a/tests/smack/functions/closure_fail.rs b/tests/smack/functions/closure_fail.rs index 68028c8348e8..f06f7810b3d0 100644 --- a/tests/smack/functions/closure_fail.rs +++ b/tests/smack/functions/closure_fail.rs @@ -11,6 +11,7 @@ where some_closure(1); } +#[kani::proof] pub fn main() { let mut num: i32 = kani::any(); if num <= std::i32::MAX - 10 { diff --git a/tests/smack/functions/double_fail.rs b/tests/smack/functions/double_fail.rs index ac7b4d23ff16..a9e90cd83b8b 100644 --- a/tests/smack/functions/double_fail.rs +++ b/tests/smack/functions/double_fail.rs @@ -7,6 +7,7 @@ fn double(a: u32) -> u32 { a * 2 } +#[kani::proof] pub fn main() { let a = kani::any(); if a <= std::u32::MAX / 2 { diff --git a/tests/smack/generics/generic_function1.rs b/tests/smack/generics/generic_function1.rs index 40957be0e923..b149b6b6aa65 100644 --- a/tests/smack/generics/generic_function1.rs +++ b/tests/smack/generics/generic_function1.rs @@ -34,6 +34,7 @@ fn swapem>(s: U) -> U { s.swap_items() } +#[kani::proof] pub fn main() { let x2 = kani::any(); let y2 = kani::any(); diff --git a/tests/smack/generics/generic_function2.rs b/tests/smack/generics/generic_function2.rs index 752c69eedaf8..7bcc281a5d17 100644 --- a/tests/smack/generics/generic_function2.rs +++ b/tests/smack/generics/generic_function2.rs @@ -34,6 +34,7 @@ fn swapem>(s: U) -> U { s.swap_items() } +#[kani::proof] pub fn main() { let x2 = kani::any(); let y2 = kani::any(); diff --git a/tests/smack/generics/generic_function3.rs b/tests/smack/generics/generic_function3.rs index dea8972bb833..f0bc9ffb02e4 100644 --- a/tests/smack/generics/generic_function3.rs +++ b/tests/smack/generics/generic_function3.rs @@ -34,6 +34,7 @@ fn swapem>(s: U) -> U { s.swap_items() } +#[kani::proof] pub fn main() { let x2 = kani::any(); let y2 = kani::any(); diff --git a/tests/smack/generics/generic_function4.rs b/tests/smack/generics/generic_function4.rs index 2ad59ce9dd24..e0cc8347c461 100644 --- a/tests/smack/generics/generic_function4.rs +++ b/tests/smack/generics/generic_function4.rs @@ -34,6 +34,7 @@ fn swapem>(s: U) -> U { s.swap_items() } +#[kani::proof] pub fn main() { let x2 = kani::any(); let y2 = kani::any(); diff --git a/tests/smack/generics/generic_function5.rs b/tests/smack/generics/generic_function5.rs index 0ac33b952efa..68f4269223cc 100644 --- a/tests/smack/generics/generic_function5.rs +++ b/tests/smack/generics/generic_function5.rs @@ -34,6 +34,7 @@ fn swapem>(s: U) -> U { s.swap_items() } +#[kani::proof] pub fn main() { let x2 = kani::any(); let y2 = kani::any(); diff --git a/tests/smack/overflow/add_overflow.rs b/tests/smack/overflow/add_overflow.rs index fbb830180c27..896941a25f62 100644 --- a/tests/smack/overflow/add_overflow.rs +++ b/tests/smack/overflow/add_overflow.rs @@ -8,6 +8,7 @@ pub fn get128() -> u8 { 128 } +#[kani::proof] pub fn main() { let a: u8 = get128(); let b: u8 = get128(); diff --git a/tests/smack/overflow/mul_overflow.rs b/tests/smack/overflow/mul_overflow.rs index 74bd36a1a923..cf35d42d84d2 100644 --- a/tests/smack/overflow/mul_overflow.rs +++ b/tests/smack/overflow/mul_overflow.rs @@ -8,6 +8,7 @@ fn get128() -> u8 { 128 } +#[kani::proof] pub fn main() { let a: u8 = get128(); let b: u8 = 2; diff --git a/tests/smack/overflow/sub_overflow.rs b/tests/smack/overflow/sub_overflow.rs index 5066be45b482..9dc7a2e0dc39 100644 --- a/tests/smack/overflow/sub_overflow.rs +++ b/tests/smack/overflow/sub_overflow.rs @@ -8,6 +8,7 @@ fn get128() -> u8 { 128 } +#[kani::proof] pub fn main() { let a: u8 = get128(); let b: u8 = 129; diff --git a/tests/smack/recursion/fac_fail.rs b/tests/smack/recursion/fac_fail.rs index 371e0a95915b..c276bd1381f6 100644 --- a/tests/smack/recursion/fac_fail.rs +++ b/tests/smack/recursion/fac_fail.rs @@ -11,6 +11,7 @@ fn fac(n: u64, acc: u64) -> u64 { } } +#[kani::proof] pub fn main() { let x = fac(5, 1); assert!(x != 120); diff --git a/tests/smack/recursion/fib_fail.rs b/tests/smack/recursion/fib_fail.rs index f8fd03b9a388..d502190576a8 100644 --- a/tests/smack/recursion/fib_fail.rs +++ b/tests/smack/recursion/fib_fail.rs @@ -12,6 +12,7 @@ fn fib(x: u64) -> u64 { } } +#[kani::proof] pub fn main() { let x = fib(6); assert!(x != 8); diff --git a/tests/smack/structures/option_fail.rs b/tests/smack/structures/option_fail.rs index db61bcc400da..5b251bde95a7 100644 --- a/tests/smack/structures/option_fail.rs +++ b/tests/smack/structures/option_fail.rs @@ -7,6 +7,7 @@ fn safe_div(x: u32, y: u32) -> Option { if y != 0 { Some(x / y) } else { None } } +#[kani::proof] pub fn main() { let x = kani::any(); if x > 0 && x <= 100 { diff --git a/tests/smack/structures/point_fail.rs b/tests/smack/structures/point_fail.rs index a9cc26820c58..cae5be564ba1 100644 --- a/tests/smack/structures/point_fail.rs +++ b/tests/smack/structures/point_fail.rs @@ -37,6 +37,7 @@ impl AddAssign for Point { } } +#[kani::proof] pub fn main() { let w = kani::any(); let x = kani::any(); diff --git a/tests/smack/vector/vec11.rs b/tests/smack/vector/vec11.rs index 9a058352293c..4816b2f42a91 100644 --- a/tests/smack/vector/vec11.rs +++ b/tests/smack/vector/vec11.rs @@ -4,6 +4,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let mut v: Vec = Vec::new(); v.push(0); diff --git a/tests/smack/vector/vec12.rs b/tests/smack/vector/vec12.rs index d00e517e25a3..cc66376e8f7d 100644 --- a/tests/smack/vector/vec12.rs +++ b/tests/smack/vector/vec12.rs @@ -4,6 +4,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let mut v: Vec = Vec::new(); v.push(0); diff --git a/tests/smack/vector/vec13.rs b/tests/smack/vector/vec13.rs index 969a4637b819..53b23943923f 100644 --- a/tests/smack/vector/vec13.rs +++ b/tests/smack/vector/vec13.rs @@ -4,6 +4,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let mut v: Vec = Vec::new(); v.push(0); diff --git a/tests/smack/vector/vec_resize_fail.rs b/tests/smack/vector/vec_resize_fail.rs index 430c47fc6bea..1b5958e14f11 100644 --- a/tests/smack/vector/vec_resize_fail.rs +++ b/tests/smack/vector/vec_resize_fail.rs @@ -4,6 +4,7 @@ // @expect error // kani-verify-fail +#[kani::proof] pub fn main() { let mut v1: Vec = vec![0]; let mut v2: Vec = vec![3]; From 68693242c21f5d476ea9ada832434845b03eb821 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Mon, 28 Nov 2022 17:45:52 -0600 Subject: [PATCH 5/5] Comment operand.rs (#1930) --- .../codegen_cprover_gotoc/codegen/operand.rs | 315 +++++++++++------- .../codegen_cprover_gotoc/codegen/place.rs | 4 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 17 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 2 +- 4 files changed, 212 insertions(+), 126 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 91a35e86b5eb..47c45efdef72 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -23,6 +23,11 @@ enum AllocData<'a> { } impl<'tcx> GotocCtx<'tcx> { + /// Generate a goto expression from a MIR operand. + /// + /// A MIR operand is either a constant (literal or `const` declaration) or a place + /// (being moved or copied for this operation). + /// An "operand" in MIR is the argument to an "Rvalue" (and is also used by some statements.) pub fn codegen_operand(&mut self, o: &Operand<'tcx>) -> Expr { trace!(operand=?o, "codegen_operand"); match o { @@ -45,6 +50,12 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate a goto expression from a MIR constant operand. + /// + /// There are three possibile constants: + /// 1. `Ty` means e.g. that it's a const generic parameter. (See `codegen_const`) + /// 2. `Val` means it's a constant value of various kinds. (See `codegen_const_value`) + /// 3. `Unevaluated` means we need to run the interpreter, to get a `ConstValue`. (See `codegen_const_unevaluated`) fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { trace!(constant=?c, "codegen_constant"); let span = Some(&c.span); @@ -57,6 +68,7 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Runs the interpreter to get a `ConstValue`, then call `codegen_const_value` fn codegen_const_unevaluated( &mut self, unevaluated: UnevaluatedConst<'tcx>, @@ -69,6 +81,12 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_const_value(const_val, ty, span) } + /// Generate a goto expression from a MIR `Const`. + /// + /// `Const` are special constant values that (only?) come from the type system, + /// and consequently only need monomorphization to produce a value. + /// + /// Not to be confused with the more general MIR `Constant` which may need interpretation. pub fn codegen_const(&mut self, lit: Const<'tcx>, span: Option<&Span>) -> Expr { debug!("found literal: {:?}", lit); let lit = self.monomorphize(lit); @@ -93,6 +111,44 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate a goto expression from a MIR `ConstValue`. + /// + /// A `ConstValue` is the result of evaluation of a constant (of various original forms). + /// All forms of constant code generation ultimately land here, where we have an actual value + /// that we now just need to translate based on its kind. + pub fn codegen_const_value( + &mut self, + v: ConstValue<'tcx>, + lit_ty: Ty<'tcx>, + span: Option<&Span>, + ) -> Expr { + trace!(val=?v, ?lit_ty, "codegen_const_value"); + match v { + ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span), + ConstValue::Slice { data, start, end } => { + self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end) + } + ConstValue::ByRef { alloc, offset } => { + debug!("ConstValue by ref {:?} {:?}", alloc, offset); + let mem_var = self + .codegen_allocation_auto_imm_name(alloc.inner(), |tcx| tcx.next_global_name()); + mem_var + .cast_to(Type::unsigned_int(8).to_pointer()) + .plus(Expr::int_constant(offset.bytes(), Type::unsigned_int(64))) + .cast_to(self.codegen_ty(lit_ty).to_pointer()) + .dereference() + } + ConstValue::ZeroSized => match lit_ty.kind() { + // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) + ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span), + _ => unimplemented!(), + }, + } + } + + /// Generate a goto expression from a MIR `ConstValue::Slice`. + /// + /// A constant slice is an internal reference to another constant allocation. fn codegen_slice_value( &mut self, v: ConstValue<'tcx>, @@ -164,8 +220,9 @@ impl<'tcx> GotocCtx<'tcx> { // TODO: Handle cases with other types such as tuples and larger integers. let loc = self.codegen_span_option(span.cloned()); let typ = self.codegen_ty(lit_ty); + let operation_name = format!("Constant slice for type {}", slice_ty); return self.codegen_unimplemented_expr( - "Constant slice value with 2+ bytes", + &operation_name, typ, loc, "https://github.com/model-checking/kani/issues/1339", @@ -178,35 +235,14 @@ impl<'tcx> GotocCtx<'tcx> { unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span); } - pub fn codegen_const_value( - &mut self, - v: ConstValue<'tcx>, - lit_ty: Ty<'tcx>, - span: Option<&Span>, - ) -> Expr { - trace!(val=?v, ?lit_ty, "codegen_const_value"); - match v { - ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span), - ConstValue::Slice { data, start, end } => { - self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end) - } - ConstValue::ByRef { alloc, offset } => { - debug!("ConstValue by ref {:?} {:?}", alloc, offset); - let mem_var = self - .codegen_allocation_auto_imm_name(alloc.inner(), |tcx| tcx.next_global_name()); - mem_var - .cast_to(Type::unsigned_int(8).to_pointer()) - .plus(Expr::int_constant(offset.bytes(), Type::unsigned_int(64))) - .cast_to(self.codegen_ty(lit_ty).to_pointer()) - .dereference() - } - ConstValue::ZeroSized => match lit_ty.kind() { - ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span), - _ => unimplemented!(), - }, - } - } - + /// Generate a goto expression from a MIR `ConstValue::Scalar`. + /// + /// A `Scalar` is a constant too small/simple to require an `Allocation` such as: + /// 1. integers + /// 2. ZST, or transparent structs of one (scalar) value + /// 3. enums that don't carry data + /// 4. unit, 1-ary tuples, or size-0 arrays + /// 5. pointers to an allocation fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Expr { debug!(scalar=?s, ?ty, kind=?ty.kind(), ?span, "codegen_scalar"); match (s, &ty.kind()) { @@ -384,17 +420,29 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_fndef( + /// A private helper for `codegen_scalar`. Many "scalars" are more complex types, but get treated as scalars + /// because they only have one (small) field. We still translated them as struct types, however. + fn codegen_single_variant_single_field( &mut self, - d: DefId, - substs: ty::subst::SubstsRef<'tcx>, + s: Scalar, span: Option<&Span>, + overall_t: Type, + fty: Ty<'tcx>, ) -> Expr { - let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap(); - self.codegen_fn_item(instance, span) + if fty.is_unit() { + // TODO: It's not clear if this case is reachable. It's not covered by our test suite at least. + Expr::struct_expr_from_values(overall_t, vec![], &self.symbol_table) + } else { + Expr::struct_expr_from_values( + overall_t, + vec![self.codegen_scalar(s, fty, span)], + &self.symbol_table, + ) + } } + /// A private helper function that ensures `alloc_id` is "allocated" (exists in the global symbol table and is + /// initialized), and just returns a pointer to somewhere (using `offset`) inside it. fn codegen_alloc_pointer( &mut self, res_t: Type, @@ -404,7 +452,7 @@ impl<'tcx> GotocCtx<'tcx> { ) -> Expr { let base_addr = match self.tcx.global_alloc(alloc_id) { GlobalAlloc::Function(instance) => { - // here we have a function pointer + // We want to return the function pointer (not to be confused with function item) self.codegen_func_expr(instance, span).address_of() } GlobalAlloc::Static(def_id) => self.codegen_static_pointer(def_id, false), @@ -442,9 +490,10 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Generates a pointer to a static or thread-local variable. + /// Generate a goto expression for a pointer to a static or thread-local variable. + /// + /// These are not initialized here, see `codegen_static`. pub fn codegen_static_pointer(&mut self, def_id: DefId, is_thread_local: bool) -> Expr { - // here we have a potentially unevaluated static let instance = Instance::mono(self.tcx, def_id); let sym = self.ensure(&self.symbol_name(instance), |ctx, name| { @@ -474,7 +523,11 @@ impl<'tcx> GotocCtx<'tcx> { sym.clone().to_expr().address_of() } - pub fn codegen_allocation_auto_imm_name) -> String>( + /// `codegen_allocation` but without an `imm_name` + /// + /// TODO: This could use some refactoring. This function is only ever invoked as: + /// `self.codegen_allocation_auto_imm_name(alloc, |tcx| tcx.next_global_name())` + fn codegen_allocation_auto_imm_name) -> String>( &mut self, alloc: &'tcx Allocation, mut_name: F, @@ -482,6 +535,21 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_allocation(alloc, mut_name, None) } + /// Add a new static allocation to the symbol table (if not already present) and + /// generate a goto expression that points to it. + /// + /// This is *the* mechanism for generating (and ensuring the intialization of) a global + /// (often but not necessarily immutable) variable in the symbol table. + /// + /// We need to codegen allocations from two sources: + /// 1. `codegen_static` which supplies the initialization code for top-level statics. + /// 2. Constants, scattered throughout the source, which need to be initialized statically, + /// so those functions can reference them. (These should always be immutable.) + /// (These also require de-duplication.) + /// + /// TODO: This function could use some refactoring. Outside of `codegen_allocation_auto_imm_name` + /// above, this function is only ever invoked as: + /// `self.codegen_allocation(alloc, |_| name.clone(), Some(name.clone()))` pub fn codegen_allocation) -> String>( &mut self, alloc: &'tcx Allocation, @@ -501,45 +569,11 @@ impl<'tcx> GotocCtx<'tcx> { mem_var.address_of() } - fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec> { - let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1); - let pointer_size = - Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); - - let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.provenance().iter() { - if offset > next_offset { - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( - next_offset.bytes_usize()..offset.bytes_usize(), - ); - alloc_vals.push(AllocData::Bytes(bytes)); - } - let ptr_offset = { - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( - offset.bytes_usize()..(offset + pointer_size).bytes_usize(), - ); - read_target_uint(self.tcx.sess.target.options.endian, bytes) - } - .unwrap(); - alloc_vals.push(AllocData::Expr(self.codegen_alloc_pointer( - Type::signed_int(8).to_pointer(), - alloc_id, - Size::from_bytes(ptr_offset), - None, - ))); - - next_offset = offset + pointer_size; - } - if alloc.len() >= next_offset.bytes_usize() { - let range = next_offset.bytes_usize()..alloc.len(); - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range); - alloc_vals.push(AllocData::Bytes(bytes)); - } - - alloc_vals - } - - /// since it's immutable, we only allocate one location for it + /// Generate a goto expression for an immutable (constant) allocation. + /// + /// This function's primary purpose is to de-duplicate immutable global constants. + /// If it already has been codegen'd, use that. + /// If not, we otherwise proceed identically to the mutable case and call `codegen_alloc_in_memory` fn codegen_immutable_allocation( &mut self, alloc: &'tcx Allocation, @@ -553,7 +587,12 @@ impl<'tcx> GotocCtx<'tcx> { self.symbol_table.lookup(&self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr() } - /// Codegen alloc as a static global variable with initial value + /// Insert an allocation into the goto symbol table, and generate a goto function that will + /// initialize it. + /// + /// This function is ultimately responsible for creating new statically initialized global variables + /// in our goto binaries. These may be actual (potentially mutable) globals or (more often) constants + /// that were encountered during code generation (that are of course immutable). fn codegen_alloc_in_memory(&mut self, alloc: &'tcx Allocation, name: String) { debug!("codegen_alloc_in_memory name: {}", name); let struct_name = &format!("{name}::struct"); @@ -624,36 +663,70 @@ impl<'tcx> GotocCtx<'tcx> { self.alloc_map.insert(alloc, name); } - fn codegen_single_variant_single_field( - &mut self, - s: Scalar, - span: Option<&Span>, - overall_t: Type, - fty: Ty<'tcx>, - ) -> Expr { - if fty.is_unit() { - Expr::struct_expr_from_values(overall_t, vec![], &self.symbol_table) - } else { - Expr::struct_expr_from_values( - overall_t, - vec![self.codegen_scalar(s, fty, span)], - &self.symbol_table, - ) + /// This is an internal helper function for `codegen_alloc_in_memory` and you should understand + /// it by starting there. + /// + /// We codegen global statics as their own unique struct types, and this creates a field-by-field + /// representation of what those fields should be initialized with. + /// (A field is either bytes, or initialized with an expression.) + fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec> { + let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1); + let pointer_size = + Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); + + let mut next_offset = Size::ZERO; + for &(offset, alloc_id) in alloc.provenance().iter() { + if offset > next_offset { + let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( + next_offset.bytes_usize()..offset.bytes_usize(), + ); + alloc_vals.push(AllocData::Bytes(bytes)); + } + let ptr_offset = { + let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( + offset.bytes_usize()..(offset + pointer_size).bytes_usize(), + ); + read_target_uint(self.tcx.sess.target.options.endian, bytes) + } + .unwrap(); + alloc_vals.push(AllocData::Expr(self.codegen_alloc_pointer( + Type::signed_int(8).to_pointer(), + alloc_id, + Size::from_bytes(ptr_offset), + None, + ))); + + next_offset = offset + pointer_size; + } + if alloc.len() >= next_offset.bytes_usize() { + let range = next_offset.bytes_usize()..alloc.len(); + let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range); + alloc_vals.push(AllocData::Bytes(bytes)); } + + alloc_vals } - /// fetch the niche value (as both left and right value) - pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr { - if offset == Size::ZERO { - v.reinterpret_cast(niche_ty) - } else { - v // t: T - .address_of() // &t: T* - .cast_to(Type::unsigned_int(8).to_pointer()) // (u8 *)&t: u8 * - .plus(Expr::int_constant(offset.bytes(), Type::size_t())) // ((u8 *)&t) + offset: u8 * - .cast_to(niche_ty.to_pointer()) // (N *)(((u8 *)&t) + offset): N * - .dereference() // *(N *)(((u8 *)&t) + offset): N - } + /// Generate a goto expression for a MIR "function item" reference. + /// + /// A "function item" is a ZST that corresponds to a specific single function. + /// This is not the closure, nor a function pointer. + /// + /// Unlike closures or pointers, which can point to anything of the correct type, + /// a function item is a type associated with a unique function. + /// This type has impls for e.g. Fn, FnOnce, etc, which is how it safely converts to other + /// function types. + /// + /// See + pub fn codegen_fndef( + &mut self, + d: DefId, + substs: ty::subst::SubstsRef<'tcx>, + span: Option<&Span>, + ) -> Expr { + let instance = + Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap(); + self.codegen_fn_item(instance, span) } /// Ensure that the given instance is in the symbol table, returning the symbol. @@ -662,10 +735,10 @@ impl<'tcx> GotocCtx<'tcx> { /// because the symbol should have the type. The problem is that the type in the symbol table /// sometimes subtly differs from the type that codegen_function_sig returns. /// This is tracked in . - pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) { + fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) { let func = self.symbol_name(instance); let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance)); - // make sure the functions imported from other modules are in the symbol table + // make sure the functions imported from other modules (or externs) are in the symbol table let sym = self.ensure(&func, |ctx, _| { Symbol::function( &func, @@ -679,34 +752,32 @@ impl<'tcx> GotocCtx<'tcx> { (sym, funct) } - /// For a given function instance, generates an expression for the function symbol of type `Code`. + /// Generate a goto expression that references the function identified by `instance`. /// - /// Note: use `codegen_func_expr_zst` in the general case because GotoC does not allow functions to be used in all contexts - /// (e.g. struct fields). + /// Note: In general with this `Expr` you should immediately either `.address_of()` or `.call(...)`. /// - /// For details, see + /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`) pub fn codegen_func_expr(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr { let (func_symbol, func_typ) = self.codegen_func_symbol(instance); Expr::symbol_expression(func_symbol.name, func_typ) .with_location(self.codegen_span_option(span.cloned())) } - /// For a given function instance, generates a zero-sized dummy symbol of type `Struct`. - /// - /// This is often necessary because GotoC does not allow functions to be used in all contexts (e.g. struct fields). - /// For details, see + /// Generate a goto expression referencing the singleton value for a MIR "function item". /// - /// Note: use `codegen_func_expr` instead if you want to call the function immediately. + /// For a given function instance, generate a ZST struct and return a singleton reference to that. + /// This is the Rust "function item". See + /// This is not the function pointer, for that use `codegen_func_expr`. fn codegen_fn_item(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr { let (func_symbol, _) = self.codegen_func_symbol(instance); - let func = func_symbol.name; - let fn_struct_ty = self.codegen_fndef_type(instance); + let mangled_name = func_symbol.name; + let fn_item_struct_ty = self.codegen_fndef_type(instance); // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object. - let fn_singleton_name = format!("{func}::FnDefSingleton"); + let fn_singleton_name = format!("{mangled_name}::FnDefSingleton"); let fn_singleton = self.ensure_global_var( &fn_singleton_name, false, - fn_struct_ty, + fn_item_struct_ty, Location::none(), |_, _| None, // zero-sized, so no initialization necessary ); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 4f5efc7f10c0..1e8b570f23c3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -310,7 +310,7 @@ impl<'tcx> GotocCtx<'tcx> { /// a named variable. /// /// Recursively finds the actual FnDef from a pointer or box. - pub fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option { + fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option { match ty.kind() { // A local that is itself a FnDef, like Fn::call_once ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)), @@ -329,7 +329,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegen for a local - pub fn codegen_local(&mut self, l: Local) -> Expr { + fn codegen_local(&mut self, l: Local) -> Expr { // Check if the local is a function definition (see comment above) if let Some(fn_def) = self.codegen_local_fndef(self.local_ty(l)) { return fn_def; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 35a2fbee2003..f5e3cbc6d222 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -17,7 +17,7 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; -use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; +use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants}; use std::collections::BTreeMap; use tracing::{debug, warn}; @@ -579,6 +579,21 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Extract the niche value from `v`. This value should be of type `niche_ty` and located + /// at byte offset `offset` + pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr { + if offset == Size::ZERO { + v.reinterpret_cast(niche_ty) + } else { + v // t: T + .address_of() // &t: T* + .cast_to(Type::unsigned_int(8).to_pointer()) // (u8 *)&t: u8 * + .plus(Expr::int_constant(offset.bytes(), Type::size_t())) // ((u8 *)&t) + offset: u8 * + .cast_to(niche_ty.to_pointer()) // (N *)(((u8 *)&t) + offset): N * + .dereference() // *(N *)(((u8 *)&t) + offset): N + } + } + fn codegen_fat_ptr_to_fat_ptr_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr { debug!("codegen_fat_ptr_to_fat_ptr_cast |{:?}| |{:?}|", src, dst_t); let src_goto_expr = self.codegen_operand(src); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index cd73955c81d2..ba6aef0c40f8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -304,7 +304,7 @@ impl<'tcx> GotocCtx<'tcx> { Type::union_tag(union_name) } - /// Makes a __attribute__((constructor)) fnname() {body} initalizer function + /// Makes a `__attribute__((constructor)) fnname() {body}` initalizer function pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol { let fn_name = Self::initializer_fn_name(var_name); let pretty_name = format!("{var_name}::init");