Assume an x86_64 architecture for the machine model (rust-lang#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

Author: adpaco-aws

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<dyn Any> {
         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.");
     }

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;