From c06d5c360f7ac0766ab0da7405ccb7e867a1c7b1 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 17 Apr 2023 19:43:47 -0700 Subject: [PATCH] Implement check for kani::unstable attribute --- .../compiler_interface.rs | 2 + kani-compiler/src/kani_compiler.rs | 4 + kani-compiler/src/kani_middle/attributes.rs | 143 ++++++++++++++++-- kani-compiler/src/kani_middle/mod.rs | 23 ++- kani-compiler/src/main.rs | 1 + kani-driver/src/args.rs | 3 +- kani-driver/src/args_toml.rs | 36 ++++- kani-driver/src/call_single_file.rs | 4 + tests/cargo-ui/unstable-attr/defs/Cargo.toml | 12 ++ tests/cargo-ui/unstable-attr/defs/src/lib.rs | 13 ++ .../cargo-ui/unstable-attr/enabled/Cargo.toml | 12 ++ tests/cargo-ui/unstable-attr/enabled/expected | 4 + .../cargo-ui/unstable-attr/enabled/src/lib.rs | 10 ++ .../cargo-ui/unstable-attr/invalid/Cargo.toml | 10 ++ tests/cargo-ui/unstable-attr/invalid/expected | 31 ++++ .../cargo-ui/unstable-attr/invalid/src/lib.rs | 24 +++ .../unstable_reachable/Cargo.toml | 15 ++ .../unstable-attr/unstable_reachable/expected | 9 ++ .../unstable_reachable/src/lib.rs | 11 ++ 19 files changed, 351 insertions(+), 16 deletions(-) create mode 100644 tests/cargo-ui/unstable-attr/defs/Cargo.toml create mode 100644 tests/cargo-ui/unstable-attr/defs/src/lib.rs create mode 100644 tests/cargo-ui/unstable-attr/enabled/Cargo.toml create mode 100644 tests/cargo-ui/unstable-attr/enabled/expected create mode 100644 tests/cargo-ui/unstable-attr/enabled/src/lib.rs create mode 100644 tests/cargo-ui/unstable-attr/invalid/Cargo.toml create mode 100644 tests/cargo-ui/unstable-attr/invalid/expected create mode 100644 tests/cargo-ui/unstable-attr/invalid/src/lib.rs create mode 100644 tests/cargo-ui/unstable-attr/unstable_reachable/Cargo.toml create mode 100644 tests/cargo-ui/unstable-attr/unstable_reachable/expected create mode 100644 tests/cargo-ui/unstable-attr/unstable_reachable/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 100fba0ef281..c6c56362849f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -8,6 +8,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::attributes::is_test_harness_description; use crate::kani_middle::check_crate_items; +use crate::kani_middle::check_reachable_items; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items, @@ -107,6 +108,7 @@ impl CodegenBackend for GotocCodegenBackend { return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); } dump_mir_items(tcx, &items); + check_reachable_items(gcx.tcx, &gcx.queries, &items); with_timer( || { diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 20576d370022..b35137495f3d 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -146,6 +146,10 @@ impl Callbacks for KaniCompiler { ); queries.set_reachability_analysis(matches.reachability_type()); + if let Some(features) = matches.get_many::(parser::UNSTABLE_FEATURE) { + queries.set_unstable_features(&features.cloned().collect::>()); + } + // If appropriate, collect and set the stub mapping. if matches.get_flag(parser::ENABLE_STUBBING) && queries.get_reachability_analysis() == ReachabilityType::Harnesses diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 3ddb58922b23..69e7fe756a40 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -31,23 +31,41 @@ enum KaniAttributeKind { Unwind, } +impl KaniAttributeKind { + /// Returns whether an item is only relevant for harnesses. + pub fn is_harness_only(self) -> bool { + match self { + KaniAttributeKind::Proof + | KaniAttributeKind::ShouldPanic + | KaniAttributeKind::Solver + | KaniAttributeKind::Stub + | KaniAttributeKind::Unwind => true, + KaniAttributeKind::Unstable => false, + } + } +} + /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { let attributes = extract_kani_attributes(tcx, def_id); - tracing::info!(?def_id, ?attributes, "check_attributes"); + + // Check proof attribute correctness. if let Some(proof_attributes) = attributes.get(&KaniAttributeKind::Proof) { check_proof_attribute(tcx, def_id, proof_attributes); - } else if let Some((kind, attrs)) = attributes.first_key_value() { - tcx.sess.span_err( - attrs[0].span, - format!( - "the `{}` attribute also requires the '#[kani::proof]' attribute", - kind.as_ref() - ) - .as_str(), - ); + } else { + // Emit an error if a harness only attribute is used outside of a harness. + for (attr, attrs) in attributes.iter().filter(|(attr, _)| attr.is_harness_only()) { + tcx.sess.span_err( + attrs[0].span, + format!( + "the `{}` attribute also requires the '#[kani::proof]' attribute", + attr.as_ref() + ) + .as_str(), + ); + } } } @@ -129,6 +147,55 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option { + if !enabled_features.contains(&unstable_attr.feature) { + let fn_name = tcx.def_path_str(def_id); + let reason = + unstable_attr.reason.map_or(String::default(), |r| format!(": {r}")); + let mut err = tcx.sess.struct_err(format!( + "Use of unstable feature `{}`{reason}", + unstable_attr.feature + )); + err.span_note( + tcx.def_span(def_id), + format!("the function `{fn_name}` is unstable:"), + ); + if let Some(link) = unstable_attr.issue { + err.note(format!("see issue {link} for more information")); + } + err.help(format!( + "use `-Z {}` to enable use this API.", + unstable_attr.feature + )); + err.emit(); + } + } + Err(msg) => { + tcx.sess + .struct_span_err( + attr.span, + format!("failed to parse `#[kani::unstable]`: {msg}"), + ) + .note(format!( + "expected format: `#[kani::unstable({}, {}, {})]`", + r#"feature="""#, + r#"issue="""#, + r#"reason="""# + )) + .emit(); + } + } + } + } +} + fn expect_single<'a>( tcx: TyCtxt, kind: KaniAttributeKind, @@ -183,6 +250,45 @@ fn extract_kani_attributes( }) } +/// Attribute used to mark a Kani lib API unstable. +#[derive(Debug)] +struct UnstableAttribute { + /// The feature identifier. + feature: String, + /// A link to the stabilization tracking issue. + issue: Option, + /// A user friendly message that describes the reason why this feature is marked as unstable. + reason: Option, +} + +/// Parse an unstable attribute into an UnstableAttribute structure. +/// Errors will be reported to the user but aborting the execution is delayed. +impl TryFrom<&Attribute> for UnstableAttribute { + type Error = String; + fn try_from(attr: &Attribute) -> Result { + let args = parse_key_values(attr)?; + let invalid_keys = args + .iter() + .filter_map(|(key, _)| { + (!matches!(key.as_str(), "feature" | "issue" | "reason")).then_some(key) + }) + .cloned() + .collect::>(); + if !invalid_keys.is_empty() { + Err(format!("unexpected argument `{}`", invalid_keys.join("`, `"))) + } else { + Ok(UnstableAttribute { + feature: args + .get("feature") + .ok_or("missing feature identifier".to_string())? + .clone(), + issue: args.get("issue").cloned(), + reason: args.get("reason").cloned(), + }) + } + } +} + /// Return the unwind value from the given attribute. fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { // Get Attribute value and if it's not none, assign it to the metadata @@ -348,6 +454,23 @@ fn parse_path(meta_item: &MetaItem) -> Option { } } +/// Parse the arguments of the attribute into a (key, value) map. +fn parse_key_values(attr: &Attribute) -> Result, String> { + trace!(list=?attr.meta_item_list(), ?attr, "parse_key_values"); + let args = attr.meta_item_list().ok_or("malformed attribute input")?; + args.iter() + .map(|arg| match arg.meta_item() { + Some(MetaItem { path: key, kind: MetaItemKind::NameValue(val), .. }) => { + Ok((key.segments.first().unwrap().ident.to_string(), val.symbol.to_string())) + } + _ => Err(format!( + r#"expected "key = value" pair, but found `{}`"#, + rustc_ast_pretty::pprust::meta_list_item_to_string(arg) + )), + }) + .collect() +} + /// If the attribute is named `kanitool::name`, this extracts `name` fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { match &attr.kind { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index ccef03a5bced..2c717d89213f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -3,7 +3,11 @@ //! This module contains code that are backend agnostic. For example, MIR analysis //! and transformations. +use std::collections::HashSet; + +use kani_queries::{QueryDb, UserInput}; use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; +use rustc_middle::mir::mono::MonoItem; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, @@ -15,7 +19,7 @@ use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use self::attributes::check_attributes; +use self::attributes::{check_attributes, check_unstable_features}; pub mod attributes; pub mod coercion; @@ -50,6 +54,23 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { tcx.sess.abort_if_errors(); } +/// Check that all given items are supported and there's no misconfiguration. +/// This method will exhaustively print any error / warning and it will abort at the end if any +/// error was found. +pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { + // Avoid printing the same error multiple times for different instantiations of the same item. + let mut def_ids = HashSet::new(); + for item in items { + let def_id = item.def_id(); + if !def_ids.contains(&def_id) { + // Check if any unstable attribute was reached. + check_unstable_features(tcx, queries.get_unstable_features(), def_id); + def_ids.insert(def_id); + } + } + tcx.sess.abort_if_errors(); +} + struct CompilerHelpers<'tcx> { tcx: TyCtxt<'tcx>, } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index d89521719dd7..599806f8de2b 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -15,6 +15,7 @@ #![feature(more_qualified_paths)] #![feature(iter_intersperse)] extern crate rustc_ast; +extern crate rustc_ast_pretty; extern crate rustc_codegen_ssa; extern crate rustc_data_structures; extern crate rustc_driver; diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 1e6a65802127..171712e9de4c 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -347,7 +347,8 @@ pub enum ConcretePlaybackMode { InPlace, } -#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] +#[strum(serialize_all = "kebab-case")] pub enum UnstableFeatures { /// Allow replace certain items with stubs (mocks). /// See (RFC-0002)[https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html] diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index c6ab7dc65c28..1ad2a4c55f8f 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -87,20 +87,40 @@ fn cargo_locate_project(input_args: &[OsString]) -> Result { /// Parse a config toml string and extract the cargo-kani arguments we should try injecting. /// This returns two different vectors since all cbmc-args have to be at the end. +/// We currently support the following entries: +/// - flags: Flags that get directly passed to Kani. +/// - unstable: Unstable features (it will be passed using `-Z` flag). +/// The tables supported are: +/// "workspace.metadata.kani", "package.metadata.kani", "kani" fn toml_to_args(tomldata: &str) -> Result<(Vec, Vec)> { let config = tomldata.parse::()?; // To make testing easier, our function contract is to produce a stable ordering of flags for a given input. // Consequently, we use BTreeMap instead of HashMap here. let mut map: BTreeMap = BTreeMap::new(); - let tables = ["workspace.metadata.kani.flags", "package.metadata.kani.flags", "kani.flags"]; + let tables = ["workspace.metadata.kani", "package.metadata.kani", "kani"]; + let mut args = Vec::new(); for table in tables { - if let Some(val) = get_table(&config, table) { - map.extend(val.iter().map(|(x, y)| (x.to_owned(), y.to_owned()))); + if let Some(table) = get_table(&config, table) { + if let Some(entry) = table.get("flags") { + if let Some(val) = entry.as_table() { + map.extend(val.iter().map(|(x, y)| (x.to_owned(), y.to_owned()))); + } + } + + if let Some(entry) = table.get("unstable") { + if let Some(val) = entry.as_table() { + args.append( + &mut val + .iter() + .filter_map(|(k, v)| unstable_entry(k, v).transpose()) + .collect::>>()?, + ); + } + } } } - let mut args = Vec::new(); let mut cbmc_args = Vec::new(); for (flag, value) in map { @@ -116,6 +136,14 @@ fn toml_to_args(tomldata: &str) -> Result<(Vec, Vec)> { Ok((args, cbmc_args)) } +fn unstable_entry(name: &String, value: &Value) -> Result> { + match value { + Value::Boolean(b) if *b => Ok(Some(OsString::from(format!("-Z{name}")))), + Value::Boolean(b) if !b => Ok(None), + _ => bail!("Expected no arguments for unstable feature `{name}` but found {value}"), + } +} + /// Translates one toml entry (flag, value) into arguments and inserts it into `args` fn insert_arg_from_toml(flag: &str, value: &Value, args: &mut Vec) -> Result<()> { match value { diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index a2ee55ca901c..79349aaf2eca 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -99,6 +99,10 @@ impl KaniSession { flags.push(format!("--harness={harness}")); } + flags.extend( + self.args.unstable_features.iter().map(|feature| format!("--unstable={feature}")), + ); + // This argument will select the Kani flavour of the compiler. It will be removed before // rustc driver is invoked. flags.push("--goto-c".into()); diff --git a/tests/cargo-ui/unstable-attr/defs/Cargo.toml b/tests/cargo-ui/unstable-attr/defs/Cargo.toml new file mode 100644 index 000000000000..a93dc8f22bde --- /dev/null +++ b/tests/cargo-ui/unstable-attr/defs/Cargo.toml @@ -0,0 +1,12 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "defs" +version = "0.1.0" +edition = "2021" +description = "define a few fake unstable APIs used in other tests" + +[dependencies] + +[package.metadata.kani.flags] +only-codegen = true diff --git a/tests/cargo-ui/unstable-attr/defs/src/lib.rs b/tests/cargo-ui/unstable-attr/defs/src/lib.rs new file mode 100644 index 000000000000..9515cf1d48a8 --- /dev/null +++ b/tests/cargo-ui/unstable-attr/defs/src/lib.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::unstable(feature = "always_fails", reason = "do not enable", issue = "")] +pub fn always_fails() { + assert!(false, "don't call me"); +} + +/// We use "gen-c" since it has to be an existing feature. +#[kani::unstable(feature = "gen-c", reason = "internal fake api", issue = "")] +pub fn no_op() { + kani::cover!(true); +} diff --git a/tests/cargo-ui/unstable-attr/enabled/Cargo.toml b/tests/cargo-ui/unstable-attr/enabled/Cargo.toml new file mode 100644 index 000000000000..46e446649435 --- /dev/null +++ b/tests/cargo-ui/unstable-attr/enabled/Cargo.toml @@ -0,0 +1,12 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "enabled" +version = "0.1.0" +edition = "2021" + +[dependencies] +defs = {path = "../defs"} + +[package.metadata.kani.unstable] +gen-c = true diff --git a/tests/cargo-ui/unstable-attr/enabled/expected b/tests/cargo-ui/unstable-attr/enabled/expected new file mode 100644 index 000000000000..da24544987af --- /dev/null +++ b/tests/cargo-ui/unstable-attr/enabled/expected @@ -0,0 +1,4 @@ +Checking harness harness... +defs::no_op.cover\ +Status: SATISFIED +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-ui/unstable-attr/enabled/src/lib.rs b/tests/cargo-ui/unstable-attr/enabled/src/lib.rs new file mode 100644 index 000000000000..c706ad4ed0c6 --- /dev/null +++ b/tests/cargo-ui/unstable-attr/enabled/src/lib.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This is just to test that we can call an unstable feature. +//! We also ensure that non-reachable unstable features do not affect our analysis. + +#[kani::proof] +pub fn harness() { + defs::no_op(); +} diff --git a/tests/cargo-ui/unstable-attr/invalid/Cargo.toml b/tests/cargo-ui/unstable-attr/invalid/Cargo.toml new file mode 100644 index 000000000000..aa19d10effc3 --- /dev/null +++ b/tests/cargo-ui/unstable-attr/invalid/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "invalid" +version = "0.1.0" +edition = "2021" +description = "check error messages due to invalid kani::unstable args" + +[dependencies] + diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected new file mode 100644 index 000000000000..daf33aa8a5b1 --- /dev/null +++ b/tests/cargo-ui/unstable-attr/invalid/expected @@ -0,0 +1,31 @@ +error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")` +lib.rs\ +|\ +| #[kani::unstable(reason = "just checking", issue = "")]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +|\ += note: expected format: `#[kani::unstable(feature="", issue="", reason="")]` + +error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `1010` +lib.rs\ +|\ +| #[kani::unstable(feature("invalid_args"))]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +|\ += note: expected format: `#[kani::unstable(feature="", issue="", reason="")]` + +error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature` +lib.rs\ +|\ +| #[kani::unstable(feature, issue)]\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +|\ += note: expected format: `#[kani::unstable(feature="", issue="", reason="")]` + +error: failed to parse `#[kani::unstable]`: missing feature identifier +lib.rs\ +|\ +| #[kani::unstable(1010)]\ +| ^^^^^^^^^^^^^^^^^^^^^^^\ +|\ += note: expected format: `#[kani::unstable(feature="", issue="", reason="")]` diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs new file mode 100644 index 000000000000..f6f55bc112ef --- /dev/null +++ b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::unstable(reason = "just checking", issue = "")] +pub fn missing_feature() { + todo!() +} + +#[kani::unstable(feature("invalid_args"))] +pub fn invalid_fn_style() {} + +#[kani::unstable(feature, issue)] +pub fn invalid_list() {} + +#[kani::unstable(1010)] +pub fn invalid_argument() {} + +#[kani::proof] +pub fn harness() { + missing_feature(); + invalid_fn_style(); + invalid_list(); + invalid_argument(); +} diff --git a/tests/cargo-ui/unstable-attr/unstable_reachable/Cargo.toml b/tests/cargo-ui/unstable-attr/unstable_reachable/Cargo.toml new file mode 100644 index 000000000000..27c07982c2cc --- /dev/null +++ b/tests/cargo-ui/unstable-attr/unstable_reachable/Cargo.toml @@ -0,0 +1,15 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "enabled" +version = "0.1.0" +edition = "2021" + +[dependencies] +defs = {path = "../defs"} + +[package.metadata.kani.flags] +only-codegen = true + +[package.metadata.kani.unstable] +gen-c = true diff --git a/tests/cargo-ui/unstable-attr/unstable_reachable/expected b/tests/cargo-ui/unstable-attr/unstable_reachable/expected new file mode 100644 index 000000000000..e51b760c438b --- /dev/null +++ b/tests/cargo-ui/unstable-attr/unstable_reachable/expected @@ -0,0 +1,9 @@ +error: Use of unstable feature `always_fails`: do not enable\ +|\ +note: the function `defs::always_fails` is unstable:\ +lib.rs:5:1\ +|\ +| pub fn always_fails() {\ +| ^^^^^^^^^^^^^^^^^^^^^\ += note: see issue for more information\ += help: use `-Z always_fails` to enable use this API. diff --git a/tests/cargo-ui/unstable-attr/unstable_reachable/src/lib.rs b/tests/cargo-ui/unstable-attr/unstable_reachable/src/lib.rs new file mode 100644 index 000000000000..45163b4101df --- /dev/null +++ b/tests/cargo-ui/unstable-attr/unstable_reachable/src/lib.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This is just to test that compilation fais if we don't enable all unstable features that +//! are reachable from a harness to be verified. + +#[kani::proof] +pub fn harness() { + defs::no_op(); + defs::always_fails(); +}