Skip to content

[WIP] Overwrite panic macros directly in libstd #4321

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

[WIP] Overwrite panic macros directly in libstd #4321

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
105 changes: 105 additions & 0 deletions kani-compiler/src/kani_compiler.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,19 @@ use crate::kani_middle::check_crate_items;
use crate::kani_queries::QueryDb;
use crate::session::init_session;
use clap::Parser;
use rustc_ast::{ItemKind, UseTreeKind};
use rustc_codegen_ssa::traits::CodegenBackend;
use rustc_driver::{Callbacks, Compilation, run_compiler};
use rustc_interface::Config;
use rustc_middle::ty::TyCtxt;
use rustc_public::rustc_internal;
use rustc_session::config::ErrorOutputType;
use rustc_session::parse::ParseSess;
use rustc_span::edition::Edition;
use rustc_span::source_map::{FileLoader, RealFileLoader};
use rustc_span::{FileName, RealFileName};
use std::io;
use std::path::Path;
use std::sync::{Arc, Mutex};
use tracing::debug;

Expand Down Expand Up @@ -75,6 +82,70 @@ fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
compile_error!("No backend is available. Use `cprover` or `llbc`.");
}

struct KaniFileLoader;

impl FileLoader for KaniFileLoader {
fn file_exists(&self, path: &Path) -> bool {
RealFileLoader.file_exists(path)
}

fn read_file(&self, path: &Path) -> io::Result<String> {
struct AstNoAnn;
impl rustc_ast_pretty::pprust::PpAnn for AstNoAnn {}

if path.ends_with("library/std/src/macros.rs") {
let psess = ParseSess::new(vec![]);
let filename = FileName::Real(RealFileName::LocalPath(path.to_owned()));

let mut module = rustc_parse::new_parser_from_source_str(
&psess,
filename.clone(),
RealFileLoader.read_file(path)?,
)
.unwrap()
.parse_crate_mod()
.unwrap();

// Remove definitions of macros we will overwrite.
module.items.retain(|item| match item.kind {
ItemKind::MacroDef(name, _) => {
!matches!(name.as_str(), "print" | "eprint" | "println" | "eprintln" | "panic")
}
_ => true,
});

// Parse the macro definition overwrites and append them to the current std::macros module.
let macros_mod = rustc_parse::new_parser_from_source_str(
&psess,
FileName::Custom("kani-macros".to_owned()),
include_str!("../../library/std/src/macros.rs").to_owned(),
)
.unwrap()
.parse_crate_mod()
.unwrap()
.items;
module.items.extend(macros_mod);

Ok(rustc_ast_pretty::pprust::print_crate(
psess.source_map(),
&module,
filename,
"".to_owned(),
&AstNoAnn,
false,
Edition::Edition2024,
&psess.attr_id_generator,
))
} else {
RealFileLoader.read_file(path)
}
}

fn read_binary_file(&self, path: &Path) -> io::Result<Arc<[u8]>> {
RealFileLoader.read_binary_file(path)
}
}

/// This object controls the compiler behavior.
///
/// It is responsible for initializing the query database, as well as controlling the compiler
Expand Down Expand Up @@ -120,6 +191,40 @@ impl Callbacks for KaniCompiler {
let queries = &mut (*self.queries.lock().unwrap());
queries.set_args(args);
debug!(?queries, "config end");

config.file_loader = Some(Box::new(KaniFileLoader));
}

fn after_crate_root_parsing(
&mut self,
compiler: &rustc_interface::interface::Compiler,
krate: &mut rustc_ast::Crate,
) -> Compilation {
if compiler.sess.opts.crate_name.as_deref() == Some("std") {
for item in &mut krate.items {
if let ItemKind::Use(use_) = &mut item.kind
&& let [root] = &*use_.prefix.segments
&& root.ident.as_str() == "core"
&& let UseTreeKind::Nested { items, .. } = &mut use_.kind
{
// Remove all re-exports of core macros that we overwrite to prevent conflicts.
items.retain(|item| {
!matches!(
item.0.ident().as_str(),
"assert"
| "assert_eq"
| "assert_ne"
| "debug_assert"
| "debug_assert_eq"
| "debug_assert_ne"
| "unreachable"
)
});
}
}
}

Compilation::Continue
}

/// After analysis, we check the crate items for Kani API misuse or configuration issues.
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ extern crate rustc_interface;
extern crate rustc_metadata;
extern crate rustc_middle;
extern crate rustc_mir_dataflow;
extern crate rustc_parse;
extern crate rustc_public;
extern crate rustc_public_bridge;
extern crate rustc_session;
Expand Down
219 changes: 2 additions & 217 deletions library/std/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,220 +16,5 @@ pub use std::*;
// Override process calls with stubs.
pub mod process;

/// This assert macro calls kani's assert function passing it down the condition
/// as well as a message that will be used when reporting the assertion result.
///
/// For the first form that does not involve a message, the macro will generate the following message:
/// assertion failed: cond
/// where `cond` is the stringified condition. For example, for
/// ```rust
/// assert!(1 + 1 == 2);
/// ```
/// the message will be:
/// assertion failed: 1 + 1 == 2
///
/// For the second form that involves a custom message possibly with arguments,
/// the macro will generate a message that is a concat of the custom message
/// along with all the arguments. For example, for
/// ```rust
/// assert!(a + b == c, "The sum of {} and {} is {}", a, b, c);
/// ```
/// the assert message will be:
/// "The sum of {} and {} is {}", a, b, c
#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! assert {
($cond:expr $(,)?) => {
// The double negation is to resolve https://github.com/model-checking/kani/issues/2108
kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
};
// Before edition 2021, the `assert!` macro could take a single argument
// that wasn't a string literal. This is not supported in edition 2021 and above.
// Because we reexport the 2021 edition macro, we need to support this
// case. For this, if there is a single argument we do the following:
// If it is a literal: Just pass it through and stringify it.
// If it isn't a literal: We add a default format
// specifier to the macro (see https://github.com/model-checking/kani/issues/1375).
($cond:expr, $first:literal $(,)?) => {{
kani::assert(!!$cond, stringify!($first));
// Process the arguments of the assert inside an unreachable block. This
// is to make sure errors in the arguments (e.g. an unknown variable or
// an argument that does not implement the Display or Debug traits) are
// reported, without creating any overhead on verification performance
// that may arise from processing strings involved in the arguments.
// Note that this approach is only correct with the "abort" panic
// strategy, but is unsound with the "unwind" panic strategy which
// requires evaluating the arguments (because they might have side
// effects). This is fine until we add support for the "unwind" panic
// strategy, which is tracked in
// https://github.com/model-checking/kani/issues/692
if false {
kani::__kani__workaround_core_assert!(true, "{}", $first);
}
}};
($cond:expr, $first:expr $(,)?) => {{
kani::assert(!!$cond, stringify!($first));
// See comment above
if false {
kani::__kani__workaround_core_assert!(true, "{}", $first);
}
}};
($cond:expr, $($arg:tt)+) => {{
kani::assert(!!$cond, concat!(stringify!($($arg)+)));
// See comment above
if false {
kani::__kani__workaround_core_assert!(true, $($arg)+);
}
}};
}

// Override the assert_eq and assert_ne macros to
// 1. Bypass the formatting-related code in the standard library implementation,
// which is not relevant for verification (see
// https://github.com/model-checking/kani/issues/14)
// 2. Generate a suitable message for the assert of the form:
// assertion failed: $left == $right
// instead of the uninformative:
// a panicking function core::panicking::assert_failed is invoked
// (see https://github.com/model-checking/kani/issues/13)
// 3. Call kani::assert so that any instrumentation that it does (e.g. injecting
// reachability checks) is done for assert_eq and assert_ne
#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! assert_eq {
($left:expr, $right:expr $(,)?) => ({
// Add parentheses around the operands to avoid a "comparison operators
// cannot be chained" error, but exclude the parentheses in the message
kani::assert(($left) == ($right), concat!("assertion failed: ", stringify!($left == $right)));
});
($left:expr, $right:expr, $($arg:tt)+) => ({
assert!(($left) == ($right), $($arg)+);
});
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! assert_ne {
($left:expr, $right:expr $(,)?) => ({
// Add parentheses around the operands to avoid a "comparison operators
// cannot be chained" error, but exclude the parentheses in the message
kani::assert(($left) != ($right), concat!("assertion failed: ", stringify!($left != $right)));
});
($left:expr, $right:expr, $($arg:tt)+) => ({
assert!(($left) != ($right), $($arg)+);
});
}

// Treat the debug assert macros same as non-debug ones
#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! debug_assert {
($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert!($($x)*); } })
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! debug_assert_eq {
($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_eq!($($x)*); } })
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! debug_assert_ne {
($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_ne!($($x)*); } })
}

// Override the print macros to skip all the printing functionality (which
// is not relevant for verification)
#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! print {
($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! eprint {
($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! println {
() => { $crate::print!("\n") };
($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! eprintln {
() => { $crate::eprint!("\n") };
($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! unreachable {
// The argument, if present, is a literal that represents the error message, i.e.:
// `unreachable!("Error message")` or `unreachable!()`
($($msg:literal)? $(,)?) => (
kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
);
// The argument is an expression, such as a variable.
// ```
// let msg = format!("Error: {}", code);
// unreachable!(msg);
// ```
// This was supported for 2018 and older rust editions.
// TODO: Is it possible to trigger an error if 2021 and above?
// https://github.com/model-checking/kani/issues/1375
($($msg:expr)? $(,)?) => (
kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
);
// The first argument is the format and the rest contains tokens to be included in the msg.
// `unreachable!("Error: {}", code);`
// We have the same issue as with panic!() described bellow where we over-approx what we can
// handle.
($fmt:expr, $($arg:tt)*) => {{
if false {
kani::__kani__workaround_core_assert!(true, $fmt, $($arg)+);
}
kani::panic(concat!("internal error: entered unreachable code: ",
stringify!($fmt, $($arg)*)))}};
}

#[cfg(not(feature = "concrete_playback"))]
#[macro_export]
macro_rules! panic {
// No argument is given.
() => (
kani::panic("explicit panic")
);
// The argument is a literal that represents the error message, i.e.:
// `panic!("Error message")`
($msg:literal $(,)?) => ({
if false {
kani::__kani__workaround_core_assert!(true, $msg);
}
kani::panic(concat!($msg))
});
// The argument is an expression, such as a variable.
// ```
// let msg = format!("Error: {}", code);
// panic!(msg);
// ```
// This was supported for 2018 and older rust editions.
// TODO: Is it possible to trigger an error if 2021 and above?
// https://github.com/model-checking/kani/issues/1375
($msg:expr $(,)?) => ({
kani::panic(stringify!($msg));
});
// All other cases, e.g.:
// `panic!("Error: {}", code);`
($($arg:tt)+) => {{
if false {
kani::__kani__workaround_core_assert!(true, $($arg)+);
}
kani::panic(stringify!($($arg)+));
}};
}
#[macro_use]
mod macros;
Loading
Loading