Merge pull request #601 from Nadrieril/no-pass-sysroot

Don't manage the sysroot ourselves

Author: Nadrieril

charon/src/bin/charon-driver/driver.rs

@@ -9,14 +9,11 @@ use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface::Compiler, Queries};
 use std::fmt;
 use std::ops::Deref;
-use std::path::PathBuf;
 use std::sync::atomic::{AtomicBool, Ordering};
 
 /// The callbacks for Charon
 pub struct CharonCallbacks {
     pub options: options::CliOpts,
-    /// The root of the toolchain.
-    pub sysroot: PathBuf,
     /// This is to be filled during the extraction; it contains the translated crate.
     transform_ctx: Option<TransformCtx>,
     pub error_count: usize,
@@ -46,10 +43,9 @@ impl fmt::Display for CharonFailure {
 }
 
 impl CharonCallbacks {
-    pub fn new(options: options::CliOpts, sysroot: PathBuf) -> Self {
+    pub fn new(options: options::CliOpts) -> Self {
         Self {
             options,
-            sysroot,
             transform_ctx: None,
             error_count: 0,
         }
@@ -141,15 +137,19 @@ impl Callbacks for CharonCallbacks {
     /// "built" MIR (which results from the conversion to HIR to MIR) to become unaccessible.
     /// Because we require built MIR at the moment, we hook ourselves before MIR-based analysis
     /// passes.
-    fn after_expansion<'tcx>(&mut self, _: &Compiler, queries: &'tcx Queries<'tcx>) -> Compilation {
+    fn after_expansion<'tcx>(
+        &mut self,
+        compiler: &Compiler,
+        queries: &'tcx Queries<'tcx>,
+    ) -> Compilation {
         // Set up our own `DefId` debug routine.
         rustc_hir::def_id::DEF_ID_DEBUG
             .swap(&(def_id_debug as fn(_, &mut fmt::Formatter<'_>) -> _));
 
-        let tranform_ctx = queries.global_ctxt().unwrap().get_mut().enter(|tcx| {
-            translate_crate_to_ullbc::translate(&self.options, tcx, self.sysroot.clone())
+        let transform_ctx = queries.global_ctxt().unwrap().get_mut().enter(|tcx| {
+            translate_crate_to_ullbc::translate(&self.options, tcx, compiler.sess.sysroot.clone())
         });
-        self.transform_ctx = Some(tranform_ctx);
+        self.transform_ctx = Some(transform_ctx);
         Compilation::Continue
     }
     fn after_analysis<'tcx>(

charon/src/bin/charon-driver/main.rs

@@ -51,23 +51,6 @@ fn main() {
     );
     trace!("original arguments (computed by cargo): {:?}", origin_args);
 
-    // Compute the sysroot (the path to the executable of the compiler):
-    // - if it is already in the command line arguments, just retrieve it from there
-    // - otherwise retrieve the sysroot from a call to rustc
-    let sysroot_arg = arg_values(&origin_args, "--sysroot").next();
-    let has_sysroot_arg = sysroot_arg.is_some();
-    let sysroot = if has_sysroot_arg {
-        sysroot_arg.unwrap().to_string()
-    } else {
-        let out = std::process::Command::new("rustc")
-            .arg("--print=sysroot")
-            .current_dir(".")
-            .output()
-            .unwrap();
-        let sysroot = std::str::from_utf8(&out.stdout).unwrap().trim();
-        sysroot.to_string()
-    };
-
     // Compute the compiler arguments for Rustc.
     // We first use all the arguments received by charon-driver, except the first two.
     // Rem.: the first argument is the path to the charon-driver executable.
@@ -97,9 +80,6 @@ fn main() {
         }
     };
 
-    if !has_sysroot_arg {
-        compiler_args.extend(vec!["--sysroot".to_string(), sysroot.clone()]);
-    }
     if options.use_polonius {
         compiler_args.push("-Zpolonius".to_string());
     }
@@ -252,7 +232,7 @@ fn main() {
     trace!("Compiler arguments: {:?}", compiler_args);
 
     // Call the Rust compiler with our custom callback.
-    let mut callback = CharonCallbacks::new(options, sysroot.into());
+    let mut callback = CharonCallbacks::new(options);
     let mut callback_ = panic::AssertUnwindSafe(&mut callback);
     let res = panic::catch_unwind(move || callback_.run_compiler(compiler_args))
         .map_err(|_| CharonFailure::Panic)

docs/limitations.md

@@ -23,6 +23,8 @@ Tracked here: https://github.com/AeneasVerif/charon/issues/142
 
 ## Missing information in the translated output
 
+- Bodies of functions in foreign crates often cause errors (https://github.com/AeneasVerif/charon/issues/543);
+- Bodies of std functions (https://github.com/AeneasVerif/charon/issues/545);
 - Drops (https://github.com/AeneasVerif/charon/issues/152);
 - Layout information (https://github.com/AeneasVerif/charon/issues/581);
 - Lifetime information inside function bodies (not planned).