diff --git a/charon/src/cli_options.rs b/charon/src/cli_options.rs index bf29b3772..07027ab3b 100644 --- a/charon/src/cli_options.rs +++ b/charon/src/cli_options.rs @@ -11,7 +11,7 @@ use std::path::PathBuf; // Note that because we need to transmit the options to the charon driver, // we store them in a file before calling this driver (hence the `Serialize`, // `Deserialize` options). -#[derive(Parser, Default, Serialize, Deserialize)] +#[derive(Debug, Default, Clone, Parser, Serialize, Deserialize)] #[clap(name = "Charon")] pub struct CliOpts { /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow) @@ -110,6 +110,11 @@ performs: `y := (x as E2).1`). Producing a better reconstruction is non-trivial. #[clap(long = "opaque")] #[serde(default)] pub opaque_modules: Vec, + /// Usually we skip the bodies of foreign methods and structs with private fields. When this + /// flag is on, we don't. + #[clap(long = "extract-opaque-bodies")] + #[serde(default)] + pub extract_opaque_bodies: bool, /// Do not provide a Rust version argument to Cargo (e.g., `+nightly-2022-01-29`). /// This is for Nix: outside of Nix, we use Rustup to call the proper version /// of Cargo (and thus need this argument), but within Nix we build and call a very diff --git a/charon/src/get_mir.rs b/charon/src/get_mir.rs index fc2c7001f..68e67aabb 100644 --- a/charon/src/get_mir.rs +++ b/charon/src/get_mir.rs @@ -1,7 +1,7 @@ //! Various utilities to load MIR. //! Allow to easily load the MIR code generated by a specific pass. -use rustc_hir::def_id::{DefId, LocalDefId}; +use rustc_hir::def_id::DefId; use rustc_middle::mir::Body; use rustc_middle::ty::TyCtxt; @@ -39,32 +39,40 @@ pub fn boxes_are_desugared(level: MirLevel) -> bool { } } -/// Query the MIR for a function at a specific level +/// Query the MIR for a function at a specific level. Return `None` in the case of a foreign body +/// with no MIR available (e.g. because it is not available for inlining). pub fn get_mir_for_def_id_and_level( tcx: TyCtxt<'_>, - def_id: LocalDefId, + def_id: DefId, level: MirLevel, -) -> Body<'_> { +) -> Option> { // Below: we **clone** the bodies to make sure we don't have issues with // locked values (we had in the past). - match level { - MirLevel::Built => { - let body = tcx.mir_built(def_id); - // We clone to be sure there are no problems with locked values - body.borrow().clone() - } - MirLevel::Promoted => { - let (body, _) = tcx.mir_promoted(def_id); - // We clone to be sure there are no problems with locked values - body.borrow().clone() + let body = if let Some(local_def_id) = def_id.as_local() { + match level { + MirLevel::Built => { + let body = tcx.mir_built(local_def_id); + // We clone to be sure there are no problems with locked values + body.borrow().clone() + } + MirLevel::Promoted => { + let (body, _) = tcx.mir_promoted(local_def_id); + // We clone to be sure there are no problems with locked values + body.borrow().clone() + } + MirLevel::Optimized => tcx.optimized_mir(def_id).clone(), } - MirLevel::Optimized => { - let def_id = DefId { - krate: rustc_hir::def_id::LOCAL_CRATE, - index: def_id.local_def_index, - }; - // We clone to be sure there are no problems with locked values + } else { + // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and + // const fns, and optimized MIR for inlinable functions. The rest don't have MIR in the + // rlib. + if tcx.is_mir_available(def_id) { tcx.optimized_mir(def_id).clone() + } else if tcx.is_ctfe_mir_available(def_id) { + tcx.mir_for_ctfe(def_id).clone() + } else { + return None; } - } + }; + Some(body) } diff --git a/charon/src/translate_crate_to_ullbc.rs b/charon/src/translate_crate_to_ullbc.rs index f079c6a5a..f98cefdfb 100644 --- a/charon/src/translate_crate_to_ullbc.rs +++ b/charon/src/translate_crate_to_ullbc.rs @@ -255,6 +255,7 @@ pub fn translate<'tcx, 'ctx>( errors_as_warnings: options.errors_as_warnings, error_count: 0, no_code_duplication: options.no_code_duplication, + extract_opaque_bodies: options.extract_opaque_bodies, all_ids: LinkedHashSet::new(), stack: BTreeSet::new(), def_id: None, diff --git a/charon/src/translate_ctx.rs b/charon/src/translate_ctx.rs index f78e1e805..d26b8013a 100644 --- a/charon/src/translate_ctx.rs +++ b/charon/src/translate_ctx.rs @@ -218,6 +218,8 @@ pub struct TransCtx<'tcx, 'ctx> { /// reconstruction (note that because several patterns in a match may lead /// to the same branch, it is node always possible not to duplicate code). pub no_code_duplication: bool, + /// Whether to extract the bodies of foreign methods and structs with private fields. + pub extract_opaque_bodies: bool, /// All the ids, in the order in which we encountered them pub all_ids: LinkedHashSet, /// The declarations we came accross and which we haven't translated yet. diff --git a/charon/src/translate_functions_to_ullbc.rs b/charon/src/translate_functions_to_ullbc.rs index 693064a7b..020f2ffa4 100644 --- a/charon/src/translate_functions_to_ullbc.rs +++ b/charon/src/translate_functions_to_ullbc.rs @@ -15,7 +15,7 @@ use crate::ullbc_ast::*; use crate::values::*; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; -use rustc_hir::def_id::{DefId, LocalDefId}; +use rustc_hir::def_id::DefId; use rustc_middle::mir::START_BLOCK; use rustc_middle::ty; use translate_types::translate_bound_region_kind_name; @@ -1429,16 +1429,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let mut t_args: Vec = Vec::new(); for arg in args { - // There should only be moved arguments, or constants - match arg { - hax::Operand::Move(_) | hax::Operand::Constant(_) => { - // OK - } - hax::Operand::Copy(_) => { - unreachable!(); - } - } - // Translate let op = self.translate_operand(span, arg)?; t_args.push(op); @@ -1447,11 +1437,26 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(t_args) } - fn translate_body(mut self, local_id: LocalDefId, arg_count: usize) -> Result { + /// Translate a function body if we can (it has MIR) and we want to (we don't translate bodies + /// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set). + fn translate_body( + mut self, + rust_id: DefId, + arg_count: usize, + ) -> Result, Error> { let tcx = self.t_ctx.tcx; + if !self.t_ctx.id_is_transparent(rust_id)? { + return Ok(None); + } + if !rust_id.is_local() && !self.t_ctx.extract_opaque_bodies { + // We only extract non-local bodies if the `extract_opaque_bodies` option is set. + return Ok(None); + } + // Retrive the body - let body = get_mir_for_def_id_and_level(tcx, local_id, self.t_ctx.mir_level); + let Some(body) = get_mir_for_def_id_and_level(tcx, rust_id, self.t_ctx.mir_level) + else { return Ok(None) }; // Here, we have to create a MIR state, which contains the body let state = hax::state::State::new_from_mir( @@ -1462,7 +1467,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Yes, we have to clone, this is annoying: we end up cloning the body twice body.clone(), // Owner id - local_id.to_def_id(), + rust_id, ); // Translate let body: hax::MirBody<()> = body.sinto(&state); @@ -1488,12 +1493,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } // Create the body - Ok(ExprBody { + Ok(Some(ExprBody { meta, arg_count, locals: self.vars, body: blocks, - }) + })) } /// Translate a function's signature, and initialize a body translation context @@ -1766,7 +1771,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { pub fn translate_function_aux(&mut self, rust_id: DefId) -> Result<(), Error> { trace!("About to translate function:\n{:?}", rust_id); let def_id = self.translate_fun_decl_id(&None, rust_id); - let is_transparent = self.id_is_transparent(rust_id)?; let def_span = self.tcx.def_span(rust_id); // Compute the meta information @@ -1794,19 +1798,16 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { trace!("Translating function signature"); let signature = bt_ctx.translate_function_signature(rust_id)?; - // Check if the type is opaque or transparent - let is_local = rust_id.is_local(); - - let body = if !is_transparent || !is_local || is_trait_method_decl { - None - } else { - match bt_ctx.translate_body(rust_id.expect_local(), signature.inputs.len()) { - Ok(body) => Some(body), - Err(_) => { - // Error case: we could have a variant for this - None - } + let body = if !is_trait_method_decl { + // Translate the body. This returns `None` if we can't/decide not to translate this + // body. + match bt_ctx.translate_body(rust_id, signature.inputs.len()) { + Ok(body) => body, + // Error case: we could have a variant for this + Err(_) => None, } + } else { + None }; // Save the new function @@ -1816,7 +1817,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { meta, def_id, rust_id, - is_local, + is_local: rust_id.is_local(), name, signature, kind, @@ -1854,7 +1855,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { // Compute the meta information let meta = self.translate_meta_from_rid(rust_id); - let is_transparent = self.id_is_transparent(rust_id)?; // Initialize the body translation context let mut bt_ctx = BodyTransCtx::new(rust_id, self); @@ -1887,18 +1887,12 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { let generics = bt_ctx.get_generics(); let preds = bt_ctx.get_predicates(); - let body = if rust_id.is_local() && is_transparent { - // It's a local and transparent global: we extract its body as for functions. - match bt_ctx.translate_body(rust_id.expect_local(), 0) { - Err(_) => { - // Error case: we could have a specific variant - None - } - Ok(body) => Some(body), - } - } else { - // Otherwise do nothing - None + // Translate its body like the body of a function. This returns `None` if we can't/decide + // not to translate this body. + let body = match bt_ctx.translate_body(rust_id, 0) { + Ok(body) => body, + // Error case: we could have a specific variant + Err(_) => None, }; // Save the new global diff --git a/charon/src/translate_traits.rs b/charon/src/translate_traits.rs index ce4a5c135..2d61766a5 100644 --- a/charon/src/translate_traits.rs +++ b/charon/src/translate_traits.rs @@ -301,10 +301,10 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { let span = tcx.def_span(rust_id); let method_name = bt_ctx.t_ctx.translate_trait_item_name(item.def_id)?; // Skip the provided methods for the *external* trait declarations, - // but still remember their name. + // but still remember their name (unless `extract_opaque_bodies` is set). if has_default_value { // This is a *provided* method - if rust_id.is_local() { + if rust_id.is_local() || bt_ctx.t_ctx.extract_opaque_bodies { let fun_id = bt_ctx.translate_fun_decl_id(span, item.def_id); provided_methods.push((method_name, Some(fun_id))); } else { diff --git a/charon/src/translate_types.rs b/charon/src/translate_types.rs index 0dbfbc47c..cab69f5c7 100644 --- a/charon/src/translate_types.rs +++ b/charon/src/translate_types.rs @@ -500,11 +500,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// struct with only public fields). fn translate_type_body( &mut self, - is_local: bool, trans_id: TypeDeclId::Id, rust_id: DefId, ) -> Result { use rustc_middle::ty::AdtKind; + let is_local = rust_id.is_local(); let def_span = self.t_ctx.tcx.def_span(rust_id); // Don't use `hax::AdtDef` because it loses `VariantIdx` information. let adt: rustc_middle::ty::AdtDef = self.t_ctx.tcx.adt_def(rust_id); @@ -514,7 +514,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // transparent (i.e., extract its body). If it is an enumeration, then yes // (because the variants of public enumerations are public, together with their // fields). If it is a structure, we check if all the fields are public. - let is_transparent = is_local + let is_transparent = self.t_ctx.extract_opaque_bodies + || is_local || match adt.adt_kind() { AdtKind::Enum => true, AdtKind::Struct => { @@ -717,7 +718,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { fn translate_type_aux(&mut self, rust_id: DefId) -> Result<(), Error> { let trans_id = self.translate_type_decl_id(&None, rust_id); let is_transparent = self.id_is_transparent(rust_id)?; - let mut bt_ctx = BodyTransCtx::new(rust_id, self); // Check and translate the generics @@ -733,11 +733,10 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { // For instance, because `core::option::Option` is public, we can // manipulate its variants. If we encounter this type, we must retrieve // its definition. - let is_local = rust_id.is_local(); let kind = if !is_transparent { TypeDeclKind::Opaque } else { - match bt_ctx.translate_type_body(is_local, trans_id, rust_id) { + match bt_ctx.translate_type_body(trans_id, rust_id) { Ok(kind) => kind, Err(err) => TypeDeclKind::Error(err.msg), } @@ -753,7 +752,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { let type_def = TypeDecl { def_id: trans_id, meta, - is_local, + is_local: rust_id.is_local(), name, generics, preds: bt_ctx.get_predicates(), diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs index 1feae0047..833bd86f6 100644 --- a/charon/tests/ui.rs +++ b/charon/tests/ui.rs @@ -4,8 +4,8 @@ //! //! Files can start with special comments that affect the test behavior. Supported magic comments: //! see [`HELP_STRING`]. -use anyhow::bail; -use assert_cmd::prelude::CommandCargoExt; +use anyhow::{anyhow, bail}; +use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt}; use indoc::indoc as unindent; use libtest_mimic::{Outcome, Test}; use std::{ @@ -18,38 +18,80 @@ use walkdir::{DirEntry, WalkDir}; use charon_lib::cli_options::{CliOpts, CHARON_ARGS}; +static TESTS_DIR: &str = "tests/ui"; + enum TestKind { PrettyLlbc, + KnownFailure, KnownPanic, - Unspecified, + Skip, } struct MagicComments { test_kind: TestKind, + /// The options with which to run charon. + cli_opts: CliOpts, + /// Whether we should store the test output in a file and check it. + check_output: bool, + /// A list of paths to files that must be compiled as dependencies for this test. + auxiliary_crates: Vec, } static HELP_STRING: &str = unindent!( - "Test must start with a magic comment that determines its kind. Options are: - - `//@ output=pretty-llbc`: record the pretty-printed llbc; + "Options are: + - `//@ output=pretty-llbc`: record the pretty-printed llbc (default); + - `//@ known-failure`: a test that is expected to fail. - `//@ known-panic`: a test that is expected to panic. + - `//@ skip`: skip the test. + + Other comments can be used to control the behavior of charon: + - `//@ charon-args=` + - `//@ no-check-output`: don't store the output in a file; useful if the output is unstable or + differs between debug and release mode. + - `//@ aux-crate=`: compile this file as a crate dependency. " ); fn parse_magic_comments(input_path: &std::path::Path) -> anyhow::Result { // Parse the magic comments. - let mut kind = TestKind::Unspecified; + let mut comments = MagicComments { + test_kind: TestKind::PrettyLlbc, + cli_opts: CliOpts::default(), + check_output: true, + auxiliary_crates: Vec::new(), + }; for line in read_to_string(input_path)?.lines() { - if !line.starts_with("//@") { - break; - } - let line = line[3..].trim(); + let Some(line) = line.strip_prefix("//@") else { break }; + let line = line.trim(); if line == "known-panic" { - kind = TestKind::KnownPanic; + comments.test_kind = TestKind::KnownPanic; + } else if line == "known-failure" { + comments.test_kind = TestKind::KnownFailure; } else if line == "output=pretty-llbc" { - kind = TestKind::PrettyLlbc; + comments.test_kind = TestKind::PrettyLlbc; + } else if line == "skip" { + comments.test_kind = TestKind::Skip; + } else if line == "no-check-output" { + comments.check_output = false; + } else if let Some(charon_opts) = line.strip_prefix("charon-args=") { + use clap::Parser; + // The first arg is normally the command name. + let args = ["dummy"].into_iter().chain(charon_opts.split_whitespace()); + comments.cli_opts.update_from(args); + } else if let Some(crate_path) = line.strip_prefix("aux-crate=") { + let crate_path: PathBuf = crate_path.into(); + let crate_path = input_path.parent().unwrap().join(crate_path); + comments.auxiliary_crates.push(crate_path) + } else { + return Err( + anyhow!("Unknown magic comment: `{line}`. {HELP_STRING}").context(format!( + "While processing file {}", + input_path.to_string_lossy() + )), + ); } } - Ok(MagicComments { test_kind: kind }) + Ok(comments) } struct Case { @@ -59,13 +101,20 @@ struct Case { } fn setup_test(input_path: PathBuf) -> anyhow::Result> { - let name = input_path.file_name().unwrap().to_str().unwrap().to_owned(); + let name = input_path + .to_str() + .unwrap() + .strip_prefix(TESTS_DIR) + .unwrap() + .strip_prefix("/") + .unwrap() + .to_owned(); let expected = input_path.with_extension("out"); let magic_comments = parse_magic_comments(&input_path)?; Ok(Test { name: name.clone(), kind: "".into(), - is_ignored: false, + is_ignored: matches!(magic_comments.test_kind, TestKind::Skip), is_bench: false, data: Case { input_path, @@ -81,44 +130,100 @@ enum Action { Overwrite, } +fn path_to_crate_name(path: &Path) -> Option { + Some( + path.file_name()? + .to_str()? + .strip_suffix(".rs")? + .replace(['-'], "_"), + ) +} + fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { - if matches!(test_case.magic_comments.test_kind, TestKind::Unspecified) { - bail!(HELP_STRING); + // Dependencies + // Vec of (crate name, path to crate.rs, path to libcrate.rlib). + let deps: Vec<(String, PathBuf, String)> = test_case + .magic_comments + .auxiliary_crates + .iter() + .cloned() + .map(|path| { + let crate_name = path_to_crate_name(&path).unwrap(); + let rlib_file_name = format!("lib{crate_name}.rlib"); // yep it must start with "lib" + let rlib_path = path.parent().unwrap().join(rlib_file_name); + let rlib_path = rlib_path.to_str().unwrap().to_owned(); + (crate_name, path, rlib_path) + }) + .collect(); + for (crate_name, rs_path, rlib_path) in deps.iter() { + Command::new("rustc") + .arg("--crate-type=rlib") + .arg(format!("--crate-name={crate_name}")) + .arg("-o") + .arg(rlib_path) + .arg(rs_path) + .output()? + .assert() + .try_success() + .map_err(|e| anyhow!(e.to_string()))?; } // Call the charon driver. - let mut options = CliOpts::default(); + let mut options = test_case.magic_comments.cli_opts.clone(); options.print_llbc = true; options.no_serialize = true; options.crate_name = Some("test_crate".into()); - let output = Command::cargo_bin("charon-driver")? - .arg("rustc") - .arg(test_case.input_path.to_string_lossy().into_owned()) - .env(CHARON_ARGS, serde_json::to_string(&options).unwrap()) - .output()?; + let mut cmd = Command::cargo_bin("charon-driver")?; + cmd.env(CHARON_ARGS, serde_json::to_string(&options).unwrap()); + cmd.arg("rustc"); + cmd.arg(test_case.input_path.to_string_lossy().into_owned()); + cmd.arg("--edition=2021"); // To avoid needing `extern crate` + for (crate_name, _, rlib_path) in deps { + cmd.arg(format!("--extern={crate_name}={rlib_path}")); + } + let output = cmd.output()?; let stderr = String::from_utf8(output.stderr.clone())?; - if matches!(test_case.magic_comments.test_kind, TestKind::KnownPanic) { - if output.status.code() != Some(101) { - let status = if output.status.success() { - "succeeded" - } else { - "errored" - }; - bail!("Compilation was expected to panic but instead {status}: {stderr}"); - // We don't commit the panic message to a file because it can differ between debug and - // release modes. + match test_case.magic_comments.test_kind { + TestKind::KnownPanic => { + if output.status.code() != Some(101) { + let status = if output.status.success() { + "succeeded" + } else { + "errored" + }; + bail!("Compilation was expected to panic but instead {status}: {stderr}"); + } } - } else { - if !output.status.success() { - bail!("Compilation failed: {stderr}") + TestKind::KnownFailure => { + if output.status.code() != Some(1) { + let status = if output.status.success() { + "succeeded" + } else { + "panicked" + }; + bail!("Compilation was expected to fail but instead {status}: {stderr}"); + } + } + TestKind::PrettyLlbc => { + if !output.status.success() { + bail!("Compilation failed: {stderr}") + } } + TestKind::Skip => unreachable!(), + } + if test_case.magic_comments.check_output { let actual = snapbox::Data::text(stderr).map_text(snapbox::utils::normalize_lines); match action { Action::Verify => expect_file_contents(&test_case.expected, actual)?, Action::Overwrite => actual.write_to(&test_case.expected)?, } + } else { + // Remove the `out` file if there's one from a previous run. + if test_case.expected.exists() { + std::fs::remove_file(&test_case.expected)?; + } } Ok(()) @@ -155,13 +260,15 @@ fn ui() -> Result<(), Box> { Action::Overwrite }; - let root: PathBuf = "tests/ui".into(); + let root: PathBuf = TESTS_DIR.into(); let file_filter = |e: &DirEntry| e.file_name().to_str().is_some_and(|s| s.ends_with(".rs")); let tests: Vec<_> = WalkDir::new(root) .min_depth(1) - .max_depth(1) .into_iter() - .filter_entry(file_filter) + .filter_map(|entry| match entry { + Ok(entry) if !file_filter(&entry) => None, + res => Some(res), + }) .map(|entry| { let entry = entry?; let test = setup_test(entry.into_path())?; diff --git a/charon/tests/ui/.gitignore b/charon/tests/ui/.gitignore new file mode 100644 index 000000000..e9e98e15f --- /dev/null +++ b/charon/tests/ui/.gitignore @@ -0,0 +1 @@ +*.rlib diff --git a/charon/tests/ui/issue-114-opaque-bodies-aux.rs b/charon/tests/ui/issue-114-opaque-bodies-aux.rs new file mode 100644 index 000000000..5d86f0ae1 --- /dev/null +++ b/charon/tests/ui/issue-114-opaque-bodies-aux.rs @@ -0,0 +1,21 @@ +//@ skip +#[inline(always)] +pub fn inline_always() -> u32 { + 42 +} + +#[inline] +pub fn inline_sometimes() -> u32 { + 42 +} + +#[inline(never)] +pub fn inline_never() -> u32 { + 42 +} + +// Generics always have MIR in the crate data. +#[inline(never)] +pub fn inline_generic() -> u32 { + 42 +} diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out new file mode 100644 index 000000000..2d00f6510 --- /dev/null +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -0,0 +1,229 @@ +[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: + +fn issue_114_opaque_bodies_aux::inline_always() -> u32 +{ + let @0: u32; // return + + @0 := const (42 : u32) + return +} + +fn issue_114_opaque_bodies_aux::inline_sometimes() -> u32 +{ + let @0: u32; // return + + @0 := const (42 : u32) + return +} + +fn issue_114_opaque_bodies_aux::inline_never() -> u32 + +fn issue_114_opaque_bodies_aux::inline_generic() -> u32 +{ + let @0: u32; // return + + @0 := const (42 : u32) + return +} + +fn test_crate::use_inlines() -> u32 +{ + let @0: u32; // return + let @1: u32; // anonymous local + let @2: u32; // anonymous local + let @3: u32; // anonymous local + let @4: u32; // anonymous local + let @5: u32; // anonymous local + let @6: u32; // anonymous local + + @3 := issue_114_opaque_bodies_aux::inline_always() + @4 := issue_114_opaque_bodies_aux::inline_sometimes() + @2 := copy (@3) + copy (@4) + drop @4 + drop @3 + @5 := issue_114_opaque_bodies_aux::inline_never() + @1 := copy (@2) + copy (@5) + drop @5 + drop @2 + @6 := issue_114_opaque_bodies_aux::inline_generic() + @0 := copy (@1) + copy (@6) + drop @6 + drop @1 + return +} + +enum core::option::Option = +| None() +| Some(T) + + +fn core::bool::{bool}::then_some(@1: bool, @2: T) -> core::option::Option +{ + let @0: core::option::Option; // return + let self@1: bool; // arg #1 + let t@2: T; // arg #2 + let @3: T; // anonymous local + let @4: bool; // anonymous local + + @4 := const (true) + if copy (self@1) { + @3 := move (t@2) + @0 := core::option::Option::Some { 0: move (@3) } + drop @3 + } + else { + @0 := core::option::Option::None { } + if copy (@4) { + drop t@2 + } + else { + nop + } + } + return +} + +fn test_crate::bool_to_opt(@1: bool) -> core::option::Option<()> +{ + let @0: core::option::Option<()>; // return + let b@1: bool; // arg #1 + let @2: bool; // anonymous local + let @3: (); // anonymous local + + @2 := copy (b@1) + @3 := () + @0 := core::bool::{bool}::then_some<()>(move (@2), move (@3)) + drop @3 + drop @2 + return +} + +trait core::convert::From +{ + fn from : core::convert::From::from +} + +fn core::convert::num::{impl core::convert::From for i64#59}::from(@1: i32) -> i64 +{ + let @0: i64; // return + let small@1: i32; // arg #1 + + @0 := cast(copy (small@1)) + return +} + +impl core::convert::num::{impl core::convert::From for i64#59} : core::convert::From +{ + fn from = core::convert::num::{impl core::convert::From for i64#59}::from +} + +fn core::convert::From::from(@1: T) -> Self + +fn test_crate::convert(@1: i32) -> i64 +{ + let @0: i64; // return + let x@1: i32; // arg #1 + let @2: i32; // anonymous local + + @2 := copy (x@1) + @0 := core::convert::num::{impl core::convert::From for i64#59}::from(move (@2)) + drop @2 + return +} + +struct core::ptr::non_null::NonNull = +{ + pointer: *mut T +} + +struct core::marker::PhantomData = {} + +struct core::ptr::unique::Unique = +{ + pointer: core::ptr::non_null::NonNull, + _marker: core::marker::PhantomData +} + +struct alloc::raw_vec::RawVec = +{ + ptr: core::ptr::unique::Unique, + cap: usize, + alloc: A +} + +struct alloc::vec::Vec = +{ + buf: alloc::raw_vec::RawVec, + len: usize +} + +struct alloc::alloc::Global = {} + +fn test_crate::vec(@1: alloc::vec::Vec) +{ + let @0: (); // return + let _x@1: alloc::vec::Vec; // arg #1 + let @2: (); // anonymous local + + @2 := () + @0 := move (@2) + drop _x@1 + @0 := () + return +} + +global core::num::{usize#11}::MAX { + let @0: usize; // return + + @0 := const (18446744073709551615 : usize) + return +} + +fn test_crate::max() -> usize +{ + let @0: usize; // return + let @1: usize; // anonymous local + + @1 := core::num::{usize#11}::MAX + @0 := move (@1) + return +} + +trait core::cmp::PartialEq +{ + fn eq : core::cmp::PartialEq::eq + fn ne : core::cmp::PartialEq::ne +} + +fn test_crate::partial_eq(@1: T) +where + [@TraitClause0]: core::cmp::PartialEq, +{ + let @0: (); // return + let _x@1: T; // arg #1 + let @2: (); // anonymous local + + @2 := () + @0 := move (@2) + drop _x@1 + @0 := () + return +} + +fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool + +fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +{ + let @0: bool; // return + let self@1: &'_ (Self); // arg #1 + let other@2: &'_ (Rhs); // arg #2 + let @3: bool; // anonymous local + + @3 := Self::eq(copy (self@1), copy (other@2)) + @0 := ~(move (@3)) + drop @3 + return +} + + + diff --git a/charon/tests/ui/issue-114-opaque-bodies.rs b/charon/tests/ui/issue-114-opaque-bodies.rs new file mode 100644 index 000000000..aac5d5372 --- /dev/null +++ b/charon/tests/ui/issue-114-opaque-bodies.rs @@ -0,0 +1,23 @@ +//@ charon-args=--extract-opaque-bodies +//@ aux-crate=issue-114-opaque-bodies-aux.rs + +fn use_inlines() -> u32 { + use issue_114_opaque_bodies_aux::*; + inline_always() + inline_sometimes() + inline_never() + inline_generic::() +} + +fn bool_to_opt(b: bool) -> Option<()> { + b.then_some(()) +} + +fn convert(x: i32) -> i64 { + i64::from(x) +} + +fn vec(_x: Vec) {} + +fn max() -> usize { + usize::MAX +} + +fn partial_eq(_x: T) {} diff --git a/charon/tests/ui/issue-118-generic-copy.rs b/charon/tests/ui/issue-118-generic-copy.rs index 99c951a8c..c4e1ffb5a 100644 --- a/charon/tests/ui/issue-118-generic-copy.rs +++ b/charon/tests/ui/issue-118-generic-copy.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc #![allow(unused)] #[derive(Clone, Copy)] diff --git a/charon/tests/ui/issue-4-traits.rs b/charon/tests/ui/issue-4-traits.rs index fbd8f87bc..846a41312 100644 --- a/charon/tests/ui/issue-4-traits.rs +++ b/charon/tests/ui/issue-4-traits.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc use std::convert::TryInto; fn trait_error(s: &[u8]) { let _array: [u8; 4] = s.try_into().unwrap(); diff --git a/charon/tests/ui/issue-45-misc.rs b/charon/tests/ui/issue-45-misc.rs index 248020af7..59069cc76 100644 --- a/charon/tests/ui/issue-45-misc.rs +++ b/charon/tests/ui/issue-45-misc.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc pub fn map(x: [i32; 256]) -> [i32; 256] { x.map(|v| v) } diff --git a/charon/tests/ui/issue-72-hash-missing-impl.rs b/charon/tests/ui/issue-72-hash-missing-impl.rs index 3ec1f6a96..7e3554533 100644 --- a/charon/tests/ui/issue-72-hash-missing-impl.rs +++ b/charon/tests/ui/issue-72-hash-missing-impl.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc pub trait Hasher {} pub struct DefaultHasher; diff --git a/charon/tests/ui/issue-73-extern.rs b/charon/tests/ui/issue-73-extern.rs index f62c1f1c7..84a7485e7 100644 --- a/charon/tests/ui/issue-73-extern.rs +++ b/charon/tests/ui/issue-73-extern.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc #![feature(extern_types)] extern "C" { fn foo(x: i32); diff --git a/charon/tests/ui/issue-92-nonpositive-variant-indices.rs b/charon/tests/ui/issue-92-nonpositive-variant-indices.rs index 8ac6d35a3..ae3e6b329 100644 --- a/charon/tests/ui/issue-92-nonpositive-variant-indices.rs +++ b/charon/tests/ui/issue-92-nonpositive-variant-indices.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc enum Ordering { Less = -1, Equal = 0, diff --git a/charon/tests/ui/issue-97-missing-parent-item-clause.rs b/charon/tests/ui/issue-97-missing-parent-item-clause.rs index f41f2d5d2..b1deed81a 100644 --- a/charon/tests/ui/issue-97-missing-parent-item-clause.rs +++ b/charon/tests/ui/issue-97-missing-parent-item-clause.rs @@ -1,4 +1,3 @@ -//@ output=pretty-llbc pub trait Ord {} pub struct AVLTree { diff --git a/charon/tests/ui/issue-79-bound-regions.rs b/charon/tests/ui/unsupported/issue-79-bound-regions.rs similarity index 82% rename from charon/tests/ui/issue-79-bound-regions.rs rename to charon/tests/ui/unsupported/issue-79-bound-regions.rs index f36bb1193..aa9e43062 100644 --- a/charon/tests/ui/issue-79-bound-regions.rs +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.rs @@ -1,4 +1,5 @@ //@ known-panic +//@ no-check-output fn main() { let slice: &[i32] = &[0]; let _ = slice.iter().next(); diff --git a/charon/tests/ui/unsupported/issue-94-recursive-trait-defns.out b/charon/tests/ui/unsupported/issue-94-recursive-trait-defns.out new file mode 100644 index 000000000..ceb20bd88 --- /dev/null +++ b/charon/tests/ui/unsupported/issue-94-recursive-trait-defns.out @@ -0,0 +1,4 @@ +thread 'rustc' panicked at 'Invalid trait decl group: +test_crate::Trait1 +test_crate::Trait2', src/reorder_decls.rs:116:9 +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace diff --git a/charon/tests/ui/issue-94-recursive-trait-defns.rs b/charon/tests/ui/unsupported/issue-94-recursive-trait-defns.rs similarity index 100% rename from charon/tests/ui/issue-94-recursive-trait-defns.rs rename to charon/tests/ui/unsupported/issue-94-recursive-trait-defns.rs diff --git a/charon/tests/ui/unsupported/option-is_some.out b/charon/tests/ui/unsupported/option-is_some.out new file mode 100644 index 000000000..6771e9aba --- /dev/null +++ b/charon/tests/ui/unsupported/option-is_some.out @@ -0,0 +1,42 @@ +error: A discriminant read must be followed by a `SwitchInt` + --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs:598:5 + +[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: + +enum core::option::Option = +| None() +| Some(T) + + +fn core::option::{core::option::Option}::is_some<'_0, T>(@1: &'_0 (core::option::Option)) -> bool +{ + let @0: bool; // return + let self@1: &'_ (core::option::Option); // arg #1 + + nop +} + +fn test_crate::my_is_some(@1: core::option::Option) -> bool +{ + let @0: bool; // return + let opt@1: core::option::Option; // arg #1 + let @2: &'_ (core::option::Option); // anonymous local + + @2 := &opt@1 + @0 := core::option::{core::option::Option}::is_some(move (@2)) + drop @2 + drop opt@1 + return +} + + + +error: The external definition DefId(2:7981 ~ core[6c80]::option::{impl#0}::is_some) triggered errors. It is (transitively) used at the following location(s): + --> tests/ui/unsupported/option-is_some.rs:6:5 + | +6 | opt.is_some() + | ^^^^^^^^^^^^^ + +error: aborting due to 2 previous errors + +[ ERROR charon_driver:262] The extraction encountered 1 errors diff --git a/charon/tests/ui/unsupported/option-is_some.rs b/charon/tests/ui/unsupported/option-is_some.rs new file mode 100644 index 000000000..b95da6e0b --- /dev/null +++ b/charon/tests/ui/unsupported/option-is_some.rs @@ -0,0 +1,7 @@ +//@ known-failure +//@ charon-args=--extract-opaque-bodies + +// Panics because the optimized MIR has a discriminant read not followed by a SwitchInt. +fn my_is_some(opt: Option) -> bool { + opt.is_some() +} diff --git a/charon/tests/ui/unsupported/result-unwrap.rs b/charon/tests/ui/unsupported/result-unwrap.rs new file mode 100644 index 000000000..75f39da5f --- /dev/null +++ b/charon/tests/ui/unsupported/result-unwrap.rs @@ -0,0 +1,8 @@ +//@ known-failure +//@ no-check-output +//@ charon-args=--extract-opaque-bodies + +// Errors because dyn types are not supported. +fn unwrap(res: Result) -> u32 { + res.unwrap() +} diff --git a/charon/tests/ui/unsupported/slice_index.rs b/charon/tests/ui/unsupported/slice_index.rs new file mode 100644 index 000000000..5c4c76bd0 --- /dev/null +++ b/charon/tests/ui/unsupported/slice_index.rs @@ -0,0 +1,8 @@ +//@ known-panic +//@ no-check-output +//@ charon-args=--extract-opaque-bodies + +// hax panics when lowering a place expression. +fn slice_index(slice: &[u8]) { + let _ = &slice[0..=10]; +} diff --git a/charon/tests/ui/unsupported/vec-push.out b/charon/tests/ui/unsupported/vec-push.out new file mode 100644 index 000000000..cd0cbefbc --- /dev/null +++ b/charon/tests/ui/unsupported/vec-push.out @@ -0,0 +1,17 @@ +error[HaxFront]: Supposely unreachable place in the Rust AST. The label is "PlaceDerefNotRefNorBox". + This error report happend because some assumption about the Rust AST was broken. + + Context: + - current_ty: *mut T + - current_kind: Local( + Local( + 10, + ), + ) + - elem: Deref + | + = note: ⚠️ This is a bug in Hax's frontend. + Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! + +error: aborting due to previous error + diff --git a/charon/tests/ui/unsupported/vec-push.rs b/charon/tests/ui/unsupported/vec-push.rs new file mode 100644 index 000000000..100e44a02 --- /dev/null +++ b/charon/tests/ui/unsupported/vec-push.rs @@ -0,0 +1,6 @@ +//@ known-panic +//@ charon-args=--extract-opaque-bodies + +fn vec(x: &mut Vec) { + x.push(42) +} diff --git a/flake.nix b/flake.nix index 3dedc92f8..ff636764a 100644 --- a/flake.nix +++ b/flake.nix @@ -52,7 +52,8 @@ in craneLibWithExt.buildPackage { src = ./charon; inherit cargoArtifacts; - IN_CI = 1; # Check the `ui_llbc` files are correct instead of overwriting them. + # Check the `ui_llbc` files are correct instead of overwriting them. + cargoTestCommand = "IN_CI=1 cargo test --profile release"; }; tests = let cargoArtifacts = craneLibNoExt.buildDepsOnly { src = ./tests; };