From fed674ca8bdf6a5b77a38e8c3df8b18a57990f57 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 20 Apr 2022 15:07:28 -0400 Subject: [PATCH] Assume an x86_64 architecture for the machine model (#1054) * Assume an x86_64 architecture for the machine model * Add checks for arch spec/options * Check platform instead of architecture * Add debug statement * print platform * Use `starts_with` for apple platforms * minor comment change * Make code simpler --- .../compiler_interface.rs | 41 +++++++++++++++++++ .../codegen_cprover_gotoc/context/goto_ctx.rs | 30 ++++++++++---- 2 files changed, 63 insertions(+), 8 deletions(-) diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 32a3ebd98a900..c1c2af5256153 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -21,6 +21,7 @@ use rustc_middle::ty::{self, TyCtxt}; use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::Session; +use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use std::collections::BTreeMap; use std::io::BufWriter; @@ -57,6 +58,7 @@ impl CodegenBackend for GotocCodegenBackend { ) -> Box { super::utils::init(); + check_target(&tcx.sess); check_options(&tcx.sess, need_metadata_module); let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1; @@ -184,7 +186,46 @@ impl CodegenBackend for GotocCodegenBackend { } } +fn check_target(session: &Session) { + // The requirement below is needed to build a valid CBMC machine model + // in function `machine_model_from_session` from + // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs + let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; + // Comparison with `x86_64-apple-darwin` does not work well because the LLVM + // target may become `x86_64-apple-macosx10.7.0` (or similar) and fail + let is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); + + if !is_linux_target && !is_darwin_target { + let err_msg = format!( + "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`, but it is {}", + &session.target.llvm_target + ); + session.err(&err_msg); + } + + session.abort_if_errors(); +} + fn check_options(session: &Session, need_metadata_module: bool) { + // The requirements for `min_global_align` and `endian` are needed to build + // a valid CBMC machine model in function `machine_model_from_session` from + // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs + match session.target.options.min_global_align { + Some(1) => (), + Some(align) => { + let err_msg = format!( + "Kani requires the target architecture option `min_global_align` to be 1, but it is {}.", + align + ); + session.err(&err_msg); + } + _ => (), + } + + if session.target.options.endian != Endian::Little { + session.err("Kani requires the target architecture option `endian` to be `little`."); + } + if !session.overflow_checks() { session.err("Kani requires overflow checks in order to provide a sound analysis."); } diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index df2fd10b36a3c..f3db47bb48d65 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -345,27 +345,41 @@ impl MetadataLoader for GotocMetadataLoader { } } +/// Builds a machine model which is required by CBMC fn machine_model_from_session(sess: &Session) -> MachineModel { - // TODO: Hardcoded values from from the ones currently used in env.rs - // We may wish to get more of them from the session. - let alignment = sess.target.options.min_global_align.unwrap_or(1); + // The model assumes a `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin` + // platform. We check the target platform in function `check_target` from + // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs and + // error if it is not any of the ones we expect. let architecture = &sess.target.arch; + let pointer_width = sess.target.pointer_width.into(); + + // The model assumes the following values for session options: + // * `min_global_align`: 1 + // * `endian`: `Endian::Little` + // + // We check these options in function `check_options` from + // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs + // and error if their values are not the ones we expect. + let alignment = sess.target.options.min_global_align.unwrap_or(1); + let is_big_endian = match sess.target.options.endian { + Endian::Little => false, + Endian::Big => true, + }; + + // The values below cannot be obtained from the session so they are + // hardcoded using standard ones for the supported platforms let bool_width = 8; let char_is_unsigned = false; let char_width = 8; let double_width = 64; let float_width = 32; let int_width = 32; - let is_big_endian = match sess.target.options.endian { - Endian::Little => false, - Endian::Big => true, - }; let long_double_width = 128; let long_int_width = 64; let long_long_int_width = 64; let memory_operand_size = 4; let null_is_zero = true; - let pointer_width = sess.target.pointer_width.into(); let short_int_width = 16; let single_width = 32; let wchar_t_is_unsigned = false;