From 068a7c077de58f1f89b34ee8b8d190246cff6be2 Mon Sep 17 00:00:00 2001 From: Hiroki Date: Thu, 4 Jun 2026 23:47:49 -0400 Subject: [PATCH 1/2] add alignment_checker --- Cargo.lock | 11 + Cargo.toml | 1 + README.md | 8 +- src/alignment_checker.rs | 29 + src/alignment_checker_check.rs | 1055 ++++++++++++++++++++++++++ src/alignment_checker_cli.rs | 258 +++++++ src/alignment_checker_index.rs | 337 ++++++++ src/lib.rs | 1 + src/main.rs | 26 + templates/template.toml | 13 + templates/template.verification.toml | 29 + 11 files changed, 1767 insertions(+), 1 deletion(-) create mode 100644 src/alignment_checker.rs create mode 100644 src/alignment_checker_check.rs create mode 100644 src/alignment_checker_cli.rs create mode 100644 src/alignment_checker_index.rs create mode 100644 templates/template.toml create mode 100644 templates/template.verification.toml diff --git a/Cargo.lock b/Cargo.lock index 37839d4..497fb86 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1222,6 +1222,7 @@ dependencies = [ "toml", "toml_edit", "touch", + "verus_syn", "walkdir", ] @@ -1626,6 +1627,16 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "verus_syn" +version = "0.0.0-2026-05-31-0205" +source = "git+https://github.com/verus-lang/verus.git#2fbad8ad8a52ce7708e6e1607a63d9af095146f0" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "walkdir" version = "2.5.0" diff --git a/Cargo.toml b/Cargo.toml index 98dd320..1c08298 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -50,6 +50,7 @@ hex = { version = "*" } toml_edit = { version = "*" } syn = { version = "2", features = ["full", "extra-traits"] } +verus_syn = { git = "https://github.com/verus-lang/verus.git", features = ["full", "parsing", "printing", "clone-impls"] } quote = { version = "*" } proc-macro2 = { version = "*" } diff --git a/README.md b/README.md index 4830f54..cf57bed 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,13 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --" cargo dv verify --targets ... ``` +To check exec API alignment against an anchor repository, use the integrated +alignment checker: + +```bash +cargo dv alignment-check -i [path/to/config/toml] +``` + Optionally, if you want to use the pre-commit hook, you can add the rusty-hook to your project: ```bash @@ -37,4 +44,3 @@ pre-commit = "cargo pre-commit" [logging] verbose = true ``` - diff --git a/src/alignment_checker.rs b/src/alignment_checker.rs new file mode 100644 index 0000000..ee1a31e --- /dev/null +++ b/src/alignment_checker.rs @@ -0,0 +1,29 @@ +#[path = "alignment_checker_check.rs"] +mod check; +#[path = "alignment_checker_cli.rs"] +pub mod cli; +#[path = "alignment_checker_index.rs"] +mod index; + +pub use check::CheckSummary; + +pub fn check_consistency(args: &cli::Args) -> anyhow::Result { + let loaded_config = cli::LoadedConfig::from_path(&args.input)?; + loaded_config.check_consistency() +} + +pub fn plural(count: usize) -> &'static str { + if count == 1 { + "" + } else { + "s" + } +} + +pub fn entry_plural(count: usize) -> &'static str { + if count == 1 { + "y" + } else { + "ies" + } +} diff --git a/src/alignment_checker_check.rs b/src/alignment_checker_check.rs new file mode 100644 index 0000000..c691d06 --- /dev/null +++ b/src/alignment_checker_check.rs @@ -0,0 +1,1055 @@ +use std::collections::{BTreeMap, BTreeSet}; +use std::path::{Path, PathBuf}; + +use anyhow::{Context, Result}; +use git2::{ + build::{CheckoutBuilder, RepoBuilder}, + FetchOptions, Object, ObjectType, Repository, +}; + +use super::cli::{ + AnchorConfig, ItemKind, LoadedConfig, LoadedModule, ModuleVerificationConfig, + VerificationMethod, +}; +use super::index::{index_module, FunctionSnapshot, ModuleIndex}; + +#[derive(Debug, Default)] +pub struct CheckSummary { + pub modules_checked: usize, + pub declared_entries: usize, + pub actual_deltas: usize, +} + +impl LoadedConfig { + pub fn check_consistency(&self) -> Result { + let anchor_dir = self.check_and_clone_repo()?; + let mut errors = Vec::new(); + let mut summary = CheckSummary::default(); + + for module in &self.modules { + self.check_module(module, &anchor_dir, &mut errors, &mut summary)?; + } + + if !errors.is_empty() { + anyhow::bail!("{}", format_errors(&errors)); + } + + Ok(summary) + } + + fn check_and_clone_repo(&self) -> Result { + let anchor_repo_dir = prepare_anchor_repo(&self.anchor)?; + let anchor_dir = match self.anchor.path.as_ref() { + Some(dir) => anchor_repo_dir.join(dir), + None => anchor_repo_dir, + }; + + if !anchor_dir.exists() { + anyhow::bail!( + "anchor path `{}` does not exist in the cloned repository", + anchor_dir.display() + ); + } + + Ok(anchor_dir) + } + + fn check_module( + &self, + module: &LoadedModule, + anchor_dir: &Path, + errors: &mut Vec, + summary: &mut CheckSummary, + ) -> Result<()> { + summary.modules_checked += 1; + + let current_module_dir = std::fs::canonicalize(&module.source).with_context(|| { + format!( + "failed to canonicalize source directory for module `{}`: {}", + module.name, + module.source.display() + ) + })?; + let repo_dir = std::fs::canonicalize(std::env::current_dir()?) + .context("failed to canonicalize current working directory")?; + let module_rel_dir = current_module_dir + .strip_prefix(&repo_dir) + .with_context(|| { + format!( + "module `{}` directory `{}` is not under current repository `{}`", + module.name, + current_module_dir.display(), + repo_dir.display() + ) + })?; + let anchor_module_dir = anchor_dir.join(module_rel_dir); + + if !anchor_module_dir.exists() { + errors.push(format!( + "[module {}] anchor module directory does not exist: {}", + module.name, + anchor_module_dir.display() + )); + return Ok(()); + } + + let current_index = index_module(¤t_module_dir).with_context(|| { + format!( + "failed to index current module `{}` at {}", + module.name, + current_module_dir.display() + ) + })?; + let anchor_index = index_module(&anchor_module_dir).with_context(|| { + format!( + "failed to index anchor module `{}` at {}", + module.name, + anchor_module_dir.display() + ) + })?; + + for error in current_index + .errors + .iter() + .chain(anchor_index.errors.iter()) + { + errors.push(format!("[module {}] {error}", module.name)); + } + + let deltas = diff_indexes(¤t_index, &anchor_index); + summary.actual_deltas += deltas.len(); + summary.declared_entries += declarations(&module.verification).len(); + check_declarations(module, ¤t_index, &anchor_index, &deltas, errors); + + Ok(()) + } +} + +#[derive(Debug, Clone)] +enum FunctionDelta { + Added { + current: FunctionSnapshot, + }, + Removed { + anchor: FunctionSnapshot, + }, + SignatureChanged { + current: FunctionSnapshot, + anchor: FunctionSnapshot, + }, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum FunctionDeltaKind { + Added, + Removed, + SignatureChanged, +} + +impl FunctionDelta { + fn kind(&self) -> FunctionDeltaKind { + match self { + FunctionDelta::Added { .. } => FunctionDeltaKind::Added, + FunctionDelta::Removed { .. } => FunctionDeltaKind::Removed, + FunctionDelta::SignatureChanged { .. } => FunctionDeltaKind::SignatureChanged, + } + } + + fn kind_name(&self) -> &'static str { + self.kind().name() + } + + fn describe(&self, module: &str, key: &str, declared: bool) -> String { + let prefix = if declared { "declared" } else { "undeclared" }; + + match self { + FunctionDelta::Added { current } => format!( + "[module {module}] {prefix} added exec function `{key}`\n current: {}\n signature: {}", + current.file.display(), + current.signature + ), + FunctionDelta::Removed { anchor } => format!( + "[module {module}] {prefix} removed exec function `{key}`\n anchor: {}\n signature: {}", + anchor.file.display(), + anchor.signature + ), + FunctionDelta::SignatureChanged { current, anchor } => format!( + "[module {module}] {prefix} signature-changed exec function `{key}`\n current: {}\n anchor: {}\n current signature: {}\n anchor signature: {}", + current.file.display(), + anchor.file.display(), + current.signature, + anchor.signature + ), + } + } +} + +impl FunctionDeltaKind { + fn name(self) -> &'static str { + match self { + FunctionDeltaKind::Added => "added", + FunctionDeltaKind::Removed => "removed", + FunctionDeltaKind::SignatureChanged => "signature-changed", + } + } +} + +fn diff_indexes(current: &ModuleIndex, anchor: &ModuleIndex) -> BTreeMap { + let mut keys = BTreeSet::new(); + keys.extend(current.functions.keys().cloned()); + keys.extend(anchor.functions.keys().cloned()); + + let mut deltas = BTreeMap::new(); + for key in keys { + match (current.functions.get(&key), anchor.functions.get(&key)) { + (Some(current), None) => { + deltas.insert( + key, + FunctionDelta::Added { + current: current.clone(), + }, + ); + } + (None, Some(anchor)) => { + deltas.insert( + key, + FunctionDelta::Removed { + anchor: anchor.clone(), + }, + ); + } + (Some(current), Some(anchor)) if current.signature != anchor.signature => { + deltas.insert( + key, + FunctionDelta::SignatureChanged { + current: current.clone(), + anchor: anchor.clone(), + }, + ); + } + _ => {} + } + } + + deltas +} + +fn check_declarations( + module: &LoadedModule, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, + deltas: &BTreeMap, + errors: &mut Vec, +) { + let mut declared = BTreeSet::new(); + + for declaration in declarations(&module.verification) { + if !matches!(declaration.kind, &ItemKind::Function) { + errors.push(format!( + "[module {}] unsupported declaration type `{:?}` for `{}` in `{}`", + module.name, + declaration.kind, + declaration.name, + module.path.display() + )); + continue; + } + + match declaration.section { + DeclarationSection::Verified { .. } => { + check_verified_declaration( + module, + declaration, + current_index, + anchor_index, + deltas, + &mut declared, + errors, + ); + } + DeclarationSection::Unsupported { anchor: Some(_) } => { + check_mapped_delta_declaration( + module, + declaration, + current_index, + anchor_index, + deltas, + &mut declared, + errors, + ); + } + DeclarationSection::Unsupported { .. } | DeclarationSection::Planned => { + check_delta_declaration(module, declaration, deltas, &mut declared, errors); + } + } + } + + for (key, delta) in deltas { + if !declared.contains(key) { + errors.push(delta.describe(&module.name, key, false)); + } + } +} + +fn check_delta_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + deltas: &BTreeMap, + declared: &mut BTreeSet, + errors: &mut Vec, +) { + match resolve_delta_key(declaration.name, deltas) { + ResolveResult::Found(key) => { + let delta = deltas + .get(&key) + .expect("resolved delta key should exist in delta map"); + if !mark_declared(module, declaration, &key, declared, errors) { + return; + } + + if let Err(reason) = declaration.allows_delta(delta.kind()) { + errors.push(format!( + "[module {}] declaration `{}` in `{}` does not match actual {} exec function delta: {}", + module.name, + declaration.name, + module.path.display(), + delta.kind_name(), + reason + )); + } + } + ResolveResult::Missing => { + errors.push(format!( + "[module {}] stale declaration `{}` in `{}`: no exec function existence/signature delta was found", + module.name, + declaration.name, + module.path.display() + )); + } + ResolveResult::Ambiguous(matches) => { + errors.push(format!( + "[module {}] ambiguous declaration `{}` in `{}`; matches: {}", + module.name, + declaration.name, + module.path.display(), + matches.join(", ") + )); + } + } +} + +fn check_verified_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, + deltas: &BTreeMap, + declared: &mut BTreeSet, + errors: &mut Vec, +) { + if declaration.anchor_name().is_some() { + check_verified_mapped_declaration( + module, + declaration, + current_index, + anchor_index, + deltas, + declared, + errors, + ); + return; + } + + match resolve_function_key(declaration.name, current_index, anchor_index) { + ResolveResult::Found(key) => { + if !mark_declared(module, declaration, &key, declared, errors) { + return; + } + + if let Some(delta) = deltas.get(&key) { + match delta.kind() { + FunctionDeltaKind::Added => { + check_verified_added_declaration( + module, + declaration, + current_index, + &key, + errors, + ); + return; + } + FunctionDeltaKind::Removed => { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` does not match actual removed exec function delta: verified APIs must exist in the current repo. Use [[unsupported]] or [[planned]] for removed exec functions.", + module.name, + declaration.name, + module.path.display() + )); + return; + } + FunctionDeltaKind::SignatureChanged => {} + } + } + + check_verified_existing_declaration( + module, + declaration, + current_index, + anchor_index, + &key, + errors, + ); + } + ResolveResult::Ambiguous(matches) => { + errors.push(format!( + "[module {}] ambiguous declaration `{}` in `{}`; matches: {}", + module.name, + declaration.name, + module.path.display(), + matches.join(", ") + )); + } + ResolveResult::Missing => { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` does not match any exec function in current or anchor", + module.name, + declaration.name, + module.path.display() + )); + } + } +} + +fn check_verified_mapped_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, + deltas: &BTreeMap, + declared: &mut BTreeSet, + errors: &mut Vec, +) { + let Some((current_key, anchor_key)) = check_mapped_delta_declaration( + module, + declaration, + current_index, + anchor_index, + deltas, + declared, + errors, + ) else { + return; + }; + + let current = current_index + .functions + .get(¤t_key) + .expect("resolved current function key should exist in current index"); + let anchor = anchor_index + .functions + .get(&anchor_key) + .expect("resolved anchor function key should exist in anchor index"); + + check_verified_snapshot_pair(module, declaration, current, anchor, errors); +} + +fn check_mapped_delta_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, + deltas: &BTreeMap, + declared: &mut BTreeSet, + errors: &mut Vec, +) -> Option<(String, String)> { + let Some(anchor_name) = declaration.anchor_name() else { + return None; + }; + + let current_key = match resolve_current_function_key(declaration.name, current_index) { + ResolveResult::Found(key) => key, + ResolveResult::Missing => { + errors.push(format!( + "[module {}] {} declaration `{}` in `{}` does not match any current exec function", + module.name, + declaration.section_name(), + declaration.name, + module.path.display() + )); + return None; + } + ResolveResult::Ambiguous(matches) => { + errors.push(format!( + "[module {}] ambiguous current name `{}` in {} declaration in `{}`; matches: {}", + module.name, + declaration.name, + declaration.section_name(), + module.path.display(), + matches.join(", ") + )); + return None; + } + }; + + let anchor_key = match resolve_anchor_function_key(anchor_name, anchor_index) { + ResolveResult::Found(key) => key, + ResolveResult::Missing => { + errors.push(format!( + "[module {}] {} declaration `{}` with anchor `{}` in `{}` does not match any anchor exec function", + module.name, + declaration.section_name(), + declaration.name, + anchor_name, + module.path.display() + )); + return None; + } + ResolveResult::Ambiguous(matches) => { + errors.push(format!( + "[module {}] ambiguous anchor name `{}` for {} declaration `{}` in `{}`; matches: {}", + module.name, + anchor_name, + declaration.section_name(), + declaration.name, + module.path.display(), + matches.join(", ") + )); + return None; + } + }; + + if current_key == anchor_key { + if !mark_declared(module, declaration, ¤t_key, declared, errors) { + return None; + } + return Some((current_key.clone(), anchor_key)); + } + + let current_declared = mark_declared(module, declaration, ¤t_key, declared, errors); + let anchor_declared = mark_declared(module, declaration, &anchor_key, declared, errors); + if !(current_declared && anchor_declared) { + return None; + } + + check_expected_mapped_delta( + module, + declaration, + ¤t_key, + FunctionDeltaKind::Added, + "current", + deltas, + errors, + ); + check_expected_mapped_delta( + module, + declaration, + &anchor_key, + FunctionDeltaKind::Removed, + "anchor", + deltas, + errors, + ); + + Some((current_key, anchor_key)) +} + +fn check_verified_added_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + current_index: &ModuleIndex, + key: &str, + errors: &mut Vec, +) { + let Some(current) = current_index.functions.get(key) else { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` is missing from current repo", + module.name, + declaration.name, + module.path.display() + )); + return; + }; + + if current.has_external_body { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` points to an exec function with #[verifier::external_body]", + module.name, + declaration.name, + module.path.display() + )); + } + + match declaration.rewrite_method() { + Some(VerificationMethod::Rewrite) => {} + Some(other) => { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` uses unsupported method `{:?}` for an added exec function; use `how = \"rewrite\"` if this current-only API was verified through a rewrite, otherwise use [[planned]]", + module.name, + declaration.name, + module.path.display(), + other + )); + } + None => { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` matches an added exec function; add `how = \"rewrite\"` if this current-only API was verified through a rewrite, otherwise use [[planned]]", + module.name, + declaration.name, + module.path.display() + )); + } + } +} + +fn check_verified_existing_declaration( + module: &LoadedModule, + declaration: Declaration<'_>, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, + key: &str, + errors: &mut Vec, +) { + let Some(current) = current_index.functions.get(key) else { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` is missing from current repo", + module.name, + declaration.name, + module.path.display() + )); + return; + }; + let Some(anchor) = anchor_index.functions.get(key) else { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` is missing from anchor", + module.name, + declaration.name, + module.path.display() + )); + return; + }; + + check_verified_snapshot_pair(module, declaration, current, anchor, errors); +} + +fn check_verified_snapshot_pair( + module: &LoadedModule, + declaration: Declaration<'_>, + current: &FunctionSnapshot, + anchor: &FunctionSnapshot, + errors: &mut Vec, +) { + if current.has_external_body { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` points to an exec function with #[verifier::external_body]", + module.name, + declaration.name, + module.path.display() + )); + } + + match declaration.rewrite_method() { + Some(VerificationMethod::Rewrite) => { + if current.signature == anchor.signature { + errors.push(format!( + "[module {}] verified/rewrite declaration `{}` in `{}` has no exec signature delta", + module.name, + declaration.name, + module.path.display() + )); + } + } + Some(VerificationMethod::SameSignature) | None => { + if current.signature != anchor.signature { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` has an exec signature delta; use `how = \"rewrite\"` if this API was intentionally rewritten", + module.name, + declaration.name, + module.path.display() + )); + } + } + Some(other) => { + errors.push(format!( + "[module {}] verified declaration `{}` in `{}` uses unsupported method `{:?}`; omit `how` or use `how = \"same-signature\"` for matching signatures, or use `how = \"rewrite\"` for signature changes", + module.name, + declaration.name, + module.path.display(), + other + )); + } + } +} + +fn check_expected_mapped_delta( + module: &LoadedModule, + declaration: Declaration<'_>, + key: &str, + expected: FunctionDeltaKind, + side: &str, + deltas: &BTreeMap, + errors: &mut Vec, +) { + match deltas.get(key) { + Some(delta) if delta.kind() == expected => {} + Some(delta) => errors.push(format!( + "[module {}] {} declaration `{}` in `{}` maps {side} exec function `{key}`, but it has an actual {} delta; expected {}", + module.name, + declaration.section_name(), + declaration.name, + module.path.display(), + delta.kind_name(), + expected.name() + )), + None => errors.push(format!( + "[module {}] {} declaration `{}` in `{}` maps {side} exec function `{key}`, but no existence/signature delta was found; remove `anchor` if this API did not move", + module.name, + declaration.section_name(), + declaration.name, + module.path.display() + )), + } +} + +fn mark_declared( + module: &LoadedModule, + declaration: Declaration<'_>, + key: &str, + declared: &mut BTreeSet, + errors: &mut Vec, +) -> bool { + if declared.insert(key.to_string()) { + true + } else { + errors.push(format!( + "[module {}] duplicate declaration for exec function `{}` resolved as `{}` in `{}`", + module.name, + declaration.name, + key, + module.path.display() + )); + false + } +} + +#[derive(Clone, Copy)] +struct Declaration<'a> { + name: &'a str, + kind: &'a ItemKind, + section: DeclarationSection<'a>, +} + +#[derive(Clone, Copy)] +enum DeclarationSection<'a> { + Unsupported { + anchor: Option<&'a str>, + }, + Verified { + how: Option<&'a VerificationMethod>, + anchor: Option<&'a str>, + }, + Planned, +} + +impl Declaration<'_> { + fn allows_delta(&self, _delta: FunctionDeltaKind) -> std::result::Result<(), String> { + match &self.section { + DeclarationSection::Unsupported { .. } => Ok(()), + DeclarationSection::Verified { .. } => { + Err("verified declarations are checked against current and anchor signatures; they are not delta allowlist entries".to_string()) + } + DeclarationSection::Planned => Ok(()), + } + } + + fn rewrite_method(&self) -> Option<&VerificationMethod> { + match &self.section { + DeclarationSection::Verified { how, .. } => *how, + _ => None, + } + } + + fn anchor_name(&self) -> Option<&str> { + match &self.section { + DeclarationSection::Unsupported { anchor } => *anchor, + DeclarationSection::Verified { anchor, .. } => *anchor, + _ => None, + } + } + + fn section_name(&self) -> &'static str { + match &self.section { + DeclarationSection::Unsupported { .. } => "unsupported", + DeclarationSection::Verified { .. } => "verified", + DeclarationSection::Planned => "planned", + } + } +} + +fn declarations(config: &ModuleVerificationConfig) -> Vec> { + let mut declarations = Vec::new(); + + declarations.extend(config.unsupported.iter().map(|item| Declaration { + name: item.name.as_str(), + kind: &item.kind, + section: DeclarationSection::Unsupported { + anchor: item.anchor.as_deref(), + }, + })); + declarations.extend(config.verified.iter().map(|item| Declaration { + name: item.name.as_str(), + kind: &item.kind, + section: DeclarationSection::Verified { + how: item.how.as_ref(), + anchor: item.anchor.as_deref(), + }, + })); + declarations.extend(config.planned.iter().map(|item| Declaration { + name: item.name.as_str(), + kind: &item.kind, + section: DeclarationSection::Planned, + })); + + declarations +} + +enum ResolveResult { + Found(String), + Missing, + Ambiguous(Vec), +} + +fn resolve_delta_key(name: &str, deltas: &BTreeMap) -> ResolveResult { + resolve_key(name, deltas.keys()) +} + +fn resolve_current_function_key(name: &str, current_index: &ModuleIndex) -> ResolveResult { + resolve_key(name, current_index.functions.keys()) +} + +fn resolve_anchor_function_key(name: &str, anchor_index: &ModuleIndex) -> ResolveResult { + resolve_key(name, anchor_index.functions.keys()) +} + +fn resolve_function_key( + name: &str, + current_index: &ModuleIndex, + anchor_index: &ModuleIndex, +) -> ResolveResult { + let mut keys = BTreeSet::new(); + keys.extend(current_index.functions.keys().cloned()); + keys.extend(anchor_index.functions.keys().cloned()); + resolve_key(name, keys.iter()) +} + +fn resolve_key<'a>(name: &str, keys: impl Iterator) -> ResolveResult { + let keys = keys.cloned().collect::>(); + if keys.iter().any(|key| key == name) { + return ResolveResult::Found(name.to_string()); + } + + let matches = keys + .iter() + .filter(|key| declaration_matches_suffix(name, key)) + .cloned() + .collect::>(); + + match matches.as_slice() { + [key] => ResolveResult::Found(key.clone()), + [] => ResolveResult::Missing, + _ => ResolveResult::Ambiguous(matches), + } +} + +fn declaration_matches_suffix(name: &str, key: &str) -> bool { + key.ends_with(&format!("::{name}")) || { + let stripped = strip_type_generics(key); + stripped.ends_with(&format!("::{name}")) + } +} + +fn strip_type_generics(key: &str) -> String { + let mut out = String::new(); + let mut chars = key.chars().peekable(); + + while let Some(ch) = chars.next() { + if ch == '<' + && out + .chars() + .last() + .is_some_and(|prev| prev == '_' || prev.is_ascii_alphanumeric()) + { + let mut depth = 1usize; + for next in chars.by_ref() { + match next { + '<' => depth += 1, + '>' => { + depth -= 1; + if depth == 0 { + break; + } + } + _ => {} + } + } + } else { + out.push(ch); + } + } + + out +} + +fn format_errors(errors: &[String]) -> String { + let mut report = format!( + "found {} alignment consistency error{}", + errors.len(), + if errors.len() == 1 { "" } else { "s" } + ); + + for error in errors { + report.push_str("\n\n"); + report.push_str(error); + } + + report +} + +fn prepare_anchor_repo(anchor: &AnchorConfig) -> Result { + let repo_dir = anchor_checkout_dir(anchor)?; + + if repo_dir.exists() { + std::fs::remove_dir_all(&repo_dir).with_context(|| { + format!( + "failed to remove existing anchor checkout directory: {}", + repo_dir.display() + ) + })?; + } + + let parent = repo_dir + .parent() + .context("anchor checkout directory has no parent")?; + + std::fs::create_dir_all(parent).with_context(|| { + format!( + "failed to create anchor checkout parent directory: {}", + parent.display() + ) + })?; + + clone_anchor_repo(anchor, &repo_dir)?; + + Ok(repo_dir) +} + +fn clone_anchor_repo(anchor: &AnchorConfig, repo_dir: &Path) -> Result { + let mut fetch_options = FetchOptions::new(); + if !is_local_git_url(&anchor.git) { + fetch_options.depth(1); + } + + let mut builder = RepoBuilder::new(); + builder.fetch_options(fetch_options); + + let repo = builder.clone(&anchor.git, repo_dir).with_context(|| { + format!( + "failed to clone anchor git repository `{}` into `{}`", + anchor.git, + repo_dir.display() + ) + })?; + + checkout_tag(&repo, &anchor.tag).with_context(|| { + format!( + "failed to checkout anchor tag `{}` in repository `{}`", + anchor.tag, + repo_dir.display() + ) + })?; + + Ok(repo) +} + +fn is_local_git_url(git: &str) -> bool { + git.starts_with("file://") || Path::new(git).exists() +} + +fn checkout_tag(repo: &Repository, tag: &str) -> Result<()> { + let object = resolve_git_object(repo, tag).or_else(|_| { + fetch_git_tag(repo, tag)?; + resolve_git_object(repo, tag) + })?; + let object = object + .peel(ObjectType::Commit) + .or_else(|_| object.peel(ObjectType::Tree)) + .with_context(|| format!("failed to peel git tag `{tag}` to a commit or tree"))?; + + repo.checkout_tree( + &object, + Some( + CheckoutBuilder::new() + .force() + .remove_untracked(true) + .remove_ignored(true), + ), + ) + .with_context(|| format!("failed to checkout git tag `{tag}`"))?; + + repo.set_head_detached(object.id()) + .with_context(|| format!("failed to detach HEAD at git tag `{tag}`"))?; + + Ok(()) +} + +fn resolve_git_object<'repo>(repo: &'repo Repository, tag: &str) -> Result> { + repo.revparse_single(&format!("refs/tags/{tag}")) + .or_else(|_| repo.revparse_single(tag)) + .with_context(|| format!("failed to resolve git tag `{tag}`")) +} + +fn fetch_git_tag(repo: &Repository, tag: &str) -> Result<()> { + let mut remote = repo + .find_remote("origin") + .context("failed to find origin remote for anchor repository")?; + let refspec = format!("+refs/tags/{tag}:refs/tags/{tag}"); + let mut fetch_options = FetchOptions::new(); + fetch_options.depth(1); + remote + .fetch(&[refspec.as_str()], Some(&mut fetch_options), None) + .with_context(|| format!("failed to fetch git tag `{tag}` from origin"))?; + + Ok(()) +} + +fn anchor_checkout_dir(anchor: &AnchorConfig) -> Result { + let repo_name = repo_name_from_git_url(&anchor.git) + .context("failed to derive repository name from anchor git URL")?; + + Ok(PathBuf::from("/tmp") + .join("verification-anchor") + .join(format!( + "{}-{}", + sanitize_path_component(&repo_name), + sanitize_path_component(&anchor.tag) + ))) +} + +fn repo_name_from_git_url(git: &str) -> Option { + let last = git.rsplit('/').next()?; + let name = last.strip_suffix(".git").unwrap_or(last); + + if name.is_empty() { + None + } else { + Some(name.to_string()) + } +} + +fn sanitize_path_component(s: &str) -> String { + s.chars() + .map(|c| match c { + 'a'..='z' | 'A'..='Z' | '0'..='9' | '-' | '_' | '.' => c, + _ => '_', + }) + .collect() +} diff --git a/src/alignment_checker_cli.rs b/src/alignment_checker_cli.rs new file mode 100644 index 0000000..c27c6ef --- /dev/null +++ b/src/alignment_checker_cli.rs @@ -0,0 +1,258 @@ +use std::path::{Path, PathBuf}; + +use anyhow::{Context, Result}; +use clap::Parser; +use serde::Deserialize; + +#[derive(Parser, Debug)] +pub struct Args { + /// The path to the input configuration toml file. + #[arg(short, long)] + pub input: String, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct Config { + pub anchor: AnchorConfig, + + #[serde(default)] + pub modules: Vec, +} + +#[derive(Debug, Clone)] +pub struct LoadedConfig { + pub anchor: AnchorConfig, + pub modules: Vec, +} + +#[derive(Debug, Clone)] +pub struct LoadedModule { + pub name: String, + pub path: PathBuf, + pub source: PathBuf, + pub verification: ModuleVerificationConfig, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct AnchorConfig { + pub git: String, + pub tag: String, + #[serde(default)] + pub path: Option, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct ModuleEntry { + pub name: String, + pub path: PathBuf, + #[serde(default)] + pub source: Option, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct ModuleVerificationConfig { + #[serde(default)] + pub unsupported: Vec, + + #[serde(default)] + pub verified: Vec, + + #[serde(default)] + pub planned: Vec, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct UnsupportedItem { + pub name: String, + + #[serde(default)] + pub anchor: Option, + + #[serde(rename = "type")] + pub kind: ItemKind, + + #[allow(dead_code)] + pub reason: UnsupportedReason, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct VerifiedItem { + pub name: String, + + #[serde(default)] + pub anchor: Option, + + #[serde(rename = "type")] + pub kind: ItemKind, + + #[serde(default)] + #[allow(dead_code)] + pub how: Option, +} + +#[derive(Debug, Clone, Deserialize)] +pub struct PlannedItem { + pub name: String, + + #[serde(rename = "type")] + pub kind: ItemKind, +} + +#[derive(Debug, Clone, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum ItemKind { + Function, + Struct, + Trait, + Impl, + Module, + Type, + Const, + Static, +} + +#[derive(Debug, Clone, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum UnsupportedReason { + LackHardwareSupport, + UnsafeDependency, + ExternalDependency, + UnsupportedAbi, + UnsupportedArchitecture, + NotApplicable, + Other, +} + +#[derive(Debug, Clone, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum VerificationMethod { + Rewrite, + SameSignature, + Stub, + SpecOnly, +} + +impl Config { + #[allow(dead_code)] + pub fn from_args(args: Args) -> Result { + Self::from_path(&args.input) + } + + pub fn from_path(path: impl AsRef) -> Result { + let path = path.as_ref(); + + if !path.exists() { + anyhow::bail!("input file does not exist: {}", path.display()); + } + + if path.is_dir() { + anyhow::bail!( + "input path is a directory, expected a file: {}", + path.display() + ); + } + + let file_content = std::fs::read_to_string(path) + .with_context(|| format!("failed to read input file: {}", path.display()))?; + + let config: Config = toml::from_str(&file_content) + .with_context(|| format!("failed to parse input file as TOML: {}", path.display()))?; + + Ok(config) + } +} + +impl LoadedConfig { + pub fn from_args(args: Args) -> Result { + let config_path = PathBuf::from(args.input); + Self::from_path(config_path) + } + + pub fn from_path(path: impl AsRef) -> Result { + let path = path.as_ref(); + + let config = Config::from_path(path)?; + + let base_dir = path.parent().unwrap_or_else(|| Path::new(".")); + + let mut modules = Vec::new(); + + for module in config.modules { + let module_config_path = if module.path.is_absolute() { + module.path.clone() + } else { + base_dir.join(&module.path) + }; + let module_source_dir = match module.source { + Some(source) if source.is_absolute() => source, + Some(source) => base_dir.join(source), + None => module_config_path + .parent() + .unwrap_or(base_dir) + .to_path_buf(), + }; + + if !module_config_path.exists() { + anyhow::bail!( + "module verification config does not exist for module `{}`: {}", + module.name, + module_config_path.display() + ); + } + + if module_config_path.is_dir() { + anyhow::bail!( + "module verification config path is a directory for module `{}`: {}", + module.name, + module_config_path.display() + ); + } + + if !module_source_dir.exists() { + anyhow::bail!( + "module source directory does not exist for module `{}`: {}", + module.name, + module_source_dir.display() + ); + } + + if !module_source_dir.is_dir() { + anyhow::bail!( + "module source path is not a directory for module `{}`: {}", + module.name, + module_source_dir.display() + ); + } + + let module_content = + std::fs::read_to_string(&module_config_path).with_context(|| { + format!( + "failed to read verification config for module `{}`: {}", + module.name, + module_config_path.display() + ) + })?; + + let verification: ModuleVerificationConfig = toml::from_str(&module_content) + .with_context(|| { + format!( + "failed to parse verification config for module `{}` as TOML: {}", + module.name, + module_config_path.display() + ) + })?; + + modules.push(LoadedModule { + name: module.name, + path: module_config_path, + source: module_source_dir, + verification, + }); + } + + Ok(Self { + anchor: config.anchor, + modules, + }) + } +} diff --git a/src/alignment_checker_index.rs b/src/alignment_checker_index.rs new file mode 100644 index 0000000..b21f586 --- /dev/null +++ b/src/alignment_checker_index.rs @@ -0,0 +1,337 @@ +use std::collections::BTreeMap; +use std::path::{Component, Path, PathBuf}; + +use anyhow::{Context, Result}; +use quote::{quote, ToTokens}; +use verus_syn::punctuated::Punctuated; +use verus_syn::{ + Attribute, File, FnArg, FnArgKind, FnMode, GenericArgument, ImplItem, Item, Pat, + Path as SynPath, PathArguments, Signature, TraitItem, Type, Visibility, +}; + +#[derive(Debug, Clone)] +pub struct FunctionSnapshot { + pub signature: String, + pub file: PathBuf, + pub has_external_body: bool, +} + +#[derive(Debug, Default)] +pub struct ModuleIndex { + pub functions: BTreeMap, + pub errors: Vec, +} + +pub fn index_module(module_dir: &Path) -> Result { + let mut files = Vec::new(); + collect_rs_files(module_dir, &mut files)?; + files.sort(); + + let mut index = ModuleIndex::default(); + for file in files { + let source = std::fs::read_to_string(&file) + .with_context(|| format!("failed to read Rust source file: {}", file.display()))?; + match verus_syn::parse_file(&source) { + Ok(parsed) => { + let module_path = file_module_path(module_dir, &file); + collect_file_items(&mut index, &file, module_path, &parsed); + } + Err(err) => { + index.errors.push(format!( + "failed to parse Rust source file `{}`: {err}", + file.display() + )); + } + } + } + + Ok(index) +} + +fn collect_rs_files(dir: &Path, files: &mut Vec) -> Result<()> { + for entry in std::fs::read_dir(dir) + .with_context(|| format!("failed to read module directory: {}", dir.display()))? + { + let entry = + entry.with_context(|| format!("failed to read entry under: {}", dir.display()))?; + let path = entry.path(); + let file_type = entry + .file_type() + .with_context(|| format!("failed to read file type: {}", path.display()))?; + + if file_type.is_dir() { + collect_rs_files(&path, files)?; + } else if file_type.is_file() && path.extension().is_some_and(|ext| ext == "rs") { + files.push(path); + } + } + + Ok(()) +} + +fn file_module_path(module_dir: &Path, file: &Path) -> Vec { + let rel = file.strip_prefix(module_dir).unwrap_or(file); + let mut components = Vec::new(); + let file_name = rel.file_name().and_then(|name| name.to_str()).unwrap_or(""); + + for component in rel.components() { + let Component::Normal(raw) = component else { + continue; + }; + let component = raw.to_string_lossy(); + + if component == file_name { + match file.file_stem().and_then(|stem| stem.to_str()) { + Some("mod") | Some("lib") | Some("main") => {} + Some(stem) => components.push(stem.to_string()), + None => {} + } + } else { + components.push(component.to_string()); + } + } + + components +} + +fn collect_file_items( + index: &mut ModuleIndex, + file: &Path, + module_path: Vec, + file_ast: &File, +) { + collect_items(index, file, &module_path, &file_ast.items); +} + +fn collect_items(index: &mut ModuleIndex, file: &Path, module_path: &[String], items: &[Item]) { + for item in items { + match item { + Item::Fn(item_fn) => { + collect_function( + index, + file, + module_path, + None, + Some(&item_fn.vis), + &item_fn.attrs, + &item_fn.sig, + ); + } + Item::Impl(item_impl) => { + let owner = impl_owner_name(item_impl); + for impl_item in &item_impl.items { + if let ImplItem::Fn(item_fn) = impl_item { + collect_function( + index, + file, + module_path, + Some(&owner), + Some(&item_fn.vis), + &item_fn.attrs, + &item_fn.sig, + ); + } + } + } + Item::Trait(item_trait) => { + let owner = item_trait.ident.to_string(); + for trait_item in &item_trait.items { + if let TraitItem::Fn(item_fn) = trait_item { + collect_function( + index, + file, + module_path, + Some(&owner), + None, + &item_fn.attrs, + &item_fn.sig, + ); + } + } + } + Item::Mod(item_mod) => { + if let Some((_, nested_items)) = &item_mod.content { + let mut nested_path = module_path.to_vec(); + nested_path.push(item_mod.ident.to_string()); + collect_items(index, file, &nested_path, nested_items); + } + } + Item::Macro(item_macro) if is_verus_macro(&item_macro.mac.path) => { + match verus_syn::parse2::(item_macro.mac.tokens.clone()) { + Ok(file_ast) => collect_items(index, file, module_path, &file_ast.items), + Err(err) => index.errors.push(format!( + "failed to parse verus! block in `{}`: {err}", + file.display() + )), + } + } + _ => {} + } + } +} + +fn collect_function( + index: &mut ModuleIndex, + file: &Path, + module_path: &[String], + owner: Option<&str>, + vis: Option<&Visibility>, + attrs: &[Attribute], + sig: &Signature, +) { + if !is_exec_signature(sig) { + return; + } + + let key = function_key(module_path, owner, &sig.ident.to_string()); + let signature = canonical_signature(vis, sig); + let snapshot = FunctionSnapshot { + signature, + file: file.to_path_buf(), + has_external_body: has_external_body(attrs), + }; + + if let Some(existing) = index.functions.insert(key.clone(), snapshot) { + index.errors.push(format!( + "duplicate exec function key `{key}` in `{}` and `{}`", + existing.file.display(), + file.display() + )); + } +} + +fn is_exec_signature(sig: &Signature) -> bool { + matches!(sig.mode, FnMode::Default | FnMode::Exec(_)) +} + +fn canonical_signature(vis: Option<&Visibility>, sig: &Signature) -> String { + let mut sig = sig.clone(); + sig.erase_spec_fields(); + sig.mode = FnMode::Default; + sig.inputs = sig + .inputs + .iter() + .filter(|arg| !is_ghost_or_tracked_arg(arg)) + .cloned() + .collect::>(); + + let tokens = match vis { + Some(vis) => quote! { #vis #sig }, + None => quote! { #sig }, + }; + tokens.to_string() +} + +fn has_external_body(attrs: &[Attribute]) -> bool { + attrs.iter().any(|attr| { + let attr = normalize_tokens(attr); + attr.contains("verifier :: external_body") + || attr.contains("verifier::external_body") + || attr.contains("external_body") + }) +} + +fn is_ghost_or_tracked_arg(arg: &FnArg) -> bool { + if arg.tracked.is_some() { + return true; + } + + let FnArgKind::Typed(pat_type) = &arg.kind else { + return false; + }; + + is_wrapper_type(&pat_type.ty, "Tracked") + || is_wrapper_type(&pat_type.ty, "Ghost") + || is_wrapper_pat(&pat_type.pat, "Tracked") + || is_wrapper_pat(&pat_type.pat, "Ghost") +} + +fn is_wrapper_type(ty: &Type, wrapper: &str) -> bool { + match ty { + Type::Path(type_path) => type_path + .path + .segments + .last() + .is_some_and(|segment| segment.ident == wrapper), + Type::Paren(type_paren) => is_wrapper_type(&type_paren.elem, wrapper), + Type::Group(type_group) => is_wrapper_type(&type_group.elem, wrapper), + _ => false, + } +} + +fn is_wrapper_pat(pat: &Pat, wrapper: &str) -> bool { + match pat { + Pat::TupleStruct(tuple) => tuple + .path + .segments + .last() + .is_some_and(|segment| segment.ident == wrapper), + Pat::Paren(paren) => is_wrapper_pat(&paren.pat, wrapper), + _ => false, + } +} + +fn function_key(module_path: &[String], owner: Option<&str>, name: &str) -> String { + let mut parts = module_path.to_vec(); + if let Some(owner) = owner { + parts.push(owner.to_string()); + } + parts.push(name.to_string()); + parts.join("::") +} + +fn impl_owner_name(item_impl: &verus_syn::ItemImpl) -> String { + let self_ty = simplify_type_name(&item_impl.self_ty); + match &item_impl.trait_ { + Some((_, trait_path, _)) => { + format!("<{} as {}>", self_ty, simplify_path_name(trait_path)) + } + None => self_ty, + } +} + +fn simplify_type_name(ty: &Type) -> String { + match ty { + Type::Path(type_path) => simplify_path_name(&type_path.path), + Type::Reference(type_ref) => simplify_type_name(&type_ref.elem), + Type::Paren(type_paren) => simplify_type_name(&type_paren.elem), + Type::Group(type_group) => simplify_type_name(&type_group.elem), + _ => normalize_tokens(ty), + } +} + +fn simplify_path_name(path: &SynPath) -> String { + let Some(segment) = path.segments.last() else { + return normalize_tokens(path); + }; + + let ident = segment.ident.to_string(); + let PathArguments::AngleBracketed(args) = &segment.arguments else { + return ident; + }; + + let args = args + .args + .iter() + .filter_map(|arg| match arg { + GenericArgument::Lifetime(_) => None, + _ => Some(normalize_tokens(arg)), + }) + .collect::>(); + + if args.is_empty() { + ident + } else { + format!("{}<{}>", ident, args.join(",")) + } +} + +fn is_verus_macro(path: &SynPath) -> bool { + path.segments + .last() + .is_some_and(|segment| segment.ident == "verus") +} + +fn normalize_tokens(value: &T) -> String { + value.to_token_stream().to_string() +} diff --git a/src/lib.rs b/src/lib.rs index 5d5b739..97f8ddc 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,7 @@ pub mod executable; pub mod files; #[macro_use] pub mod console; +pub mod alignment_checker; pub mod commands; pub mod config; pub mod dep_tree; diff --git a/src/main.rs b/src/main.rs index 703e6b3..4d713bb 100644 --- a/src/main.rs +++ b/src/main.rs @@ -81,6 +81,13 @@ enum Commands { alias = "f" )] Format(FmtArgs), + + #[command( + name = "alignment-check", + about = "Check exec API alignment against an anchor repository", + alias = "align" + )] + AlignmentCheck(alignment_checker::cli::Args), } #[derive(Parser, Debug)] @@ -576,6 +583,24 @@ fn format(args: &FmtArgs) -> Result<(), DynError> { Ok(()) } +fn alignment_check(args: &alignment_checker::cli::Args) -> Result<(), DynError> { + match alignment_checker::check_consistency(args) { + Ok(summary) => { + println!( + "Configuration consistency check passed: checked {} module{}, {} declared entr{}, {} actual delta{}", + summary.modules_checked, + alignment_checker::plural(summary.modules_checked), + summary.declared_entries, + alignment_checker::entry_plural(summary.declared_entries), + summary.actual_deltas, + alignment_checker::plural(summary.actual_deltas), + ); + Ok(()) + } + Err(e) => Err(format!("Configuration consistency check failed: {e:#}").into()), + } +} + fn main() { let cli = Cli::parse(); if let Err(e) = match &cli.command { @@ -589,6 +614,7 @@ fn main() { Commands::ShowItem(args) => show_item(args), Commands::Format(args) => format(args), Commands::Clean(args) => clean(args), + Commands::AlignmentCheck(args) => alignment_check(args), } { error!("Error when executing command `{:?}`: {}", cli.command, e); } diff --git a/templates/template.toml b/templates/template.toml new file mode 100644 index 0000000..91b012c --- /dev/null +++ b/templates/template.toml @@ -0,0 +1,13 @@ +[anchor] +git = "https://github.com/asterinas/asterinas.git" +tag = "v0.16.0" + +[[modules]] +name = "mm" +path = "modules/mm.toml" +source = "../../ostd/src/mm" + +[[modules]] +name = "rcu" +path = "modules/rcu.toml" +source = "../../ostd/src/sync/rcu" diff --git a/templates/template.verification.toml b/templates/template.verification.toml new file mode 100644 index 0000000..70960b0 --- /dev/null +++ b/templates/template.verification.toml @@ -0,0 +1,29 @@ +# Initial checker semantics: +# These sections declare exec function existence/signature deltas against the anchor. +# Functions with only body/proof/spec changes should not be listed here. +# - [[planned]] allows added/removed/signature-changed deltas. +# - [[unsupported]] declares exec APIs that are intentionally not verified. It +# allows added/removed/signature-changed deltas and may use optional +# `anchor = "old::Api::name"` to map renamed/moved APIs. +# - [[verified]] declares a verified exec API. `name` is resolved in the +# current repo. Optional `anchor = "old::Api::name"` maps it to a differently +# named exec API in the anchor, e.g. trait method -> inherent method. +# Verified current functions must not have `#[verifier::external_body]`. +# Without `how`, or with `how = "same-signature"`, current and anchor +# signatures must match. `how = "rewrite"` is for intentional signature +# changes, including current-only APIs verified through a rewrite or +# replacement. + +[[unsupported]] +name = "VmSpace::activate" +type = "function" +reason = "lack-hardware-support" + +[[verified]] +name = "VmSpace::cursor_mut" +type = "function" +# how = "same-signature" + +[[planned]] +name = "VmSpace::deactivate" +type = "function" From 3f94d9635c62b1d8a677e7b071f1fc884f0f114f Mon Sep 17 00:00:00 2001 From: Hiroki Date: Thu, 4 Jun 2026 23:51:08 -0400 Subject: [PATCH 2/2] update templates --- templates/mm.toml | 1615 +++++++++++++++++++++++++++++++++++++++ templates/rcu.toml | 216 ++++++ templates/template.toml | 12 +- 3 files changed, 1837 insertions(+), 6 deletions(-) create mode 100644 templates/mm.toml create mode 100644 templates/rcu.toml diff --git a/templates/mm.toml b/templates/mm.toml new file mode 100644 index 0000000..4258a82 --- /dev/null +++ b/templates/mm.toml @@ -0,0 +1,1615 @@ +# Exec function existence/signature deltas against the configured anchor. +# +# Generated from the mm verification status table and alignment-checker output. + +[[planned]] +name = "PagingConstsTrait::ADDRESS_WIDTH" +type = "function" + +[[planned]] +name = "PagingConstsTrait::BASE_PAGE_SIZE" +type = "function" + +[[planned]] +name = "PagingConstsTrait::HIGHEST_TRANSLATION_LEVEL" +type = "function" + +[[planned]] +name = "PagingConstsTrait::NR_LEVELS" +type = "function" + +[[planned]] +name = "PagingConstsTrait::PTE_SIZE" +type = "function" + +[[planned]] +name = "PagingConstsTrait::VA_SIGN_EXT" +type = "function" + +[[planned]] +name = "dma::::daddr" +type = "function" + +[[planned]] +name = "dma::dma_coherent::::deref" +type = "function" + +[[verified]] +name = "dma::dma_coherent:: as HasDaddr>::daddr" +anchor = "dma::dma_coherent::::daddr" +type = "function" + +[[verified]] +name = "dma::dma_coherent:: as HasPaddr>::paddr" +anchor = "dma::dma_coherent::::paddr" +type = "function" + +[[verified]] +name = "dma::dma_coherent:: as VmIo>>::read" +anchor = "dma::dma_coherent::::read" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_coherent:: as VmIo>>::write" +anchor = "dma::dma_coherent::::write" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_coherent::::read_once" +type = "function" + +[[planned]] +name = "dma::dma_coherent::::write_once" +type = "function" + +[[planned]] +name = "dma::dma_coherent:: as Clone>::clone" +type = "function" + +[[planned]] +name = "dma::dma_coherent:: as VmIoOnce>::read_once" +type = "function" + +[[planned]] +name = "dma::dma_coherent:: as VmIoOnce>::write_once" +type = "function" + +[[planned]] +name = "dma::dma_coherent::::drop" +type = "function" + +[[verified]] +name = "dma::dma_coherent::DmaCoherent::map" +anchor = "dma::dma_coherent::DmaCoherent::map" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_coherent::DmaCoherent::nbytes" +anchor = "dma::dma_coherent::DmaCoherent::nbytes" +type = "function" + +[[verified]] +name = "dma::dma_coherent::DmaCoherent::reader" +anchor = "dma::dma_coherent::DmaCoherent::reader" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_coherent::DmaCoherent::writer" +anchor = "dma::dma_coherent::DmaCoherent::writer" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::daddr" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::daddr_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::nbytes_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::nframes" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::nframes_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::paddr" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::paddr_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::read_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::reader_inner" +type = "function" + +[[planned]] +name = "dma::dma_coherent::DmaCoherent::writer_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::>::as_ref" +type = "function" + +[[planned]] +name = "dma::dma_stream::::daddr" +type = "function" + +[[planned]] +name = "dma::dma_stream::::paddr" +type = "function" + +[[verified]] +name = "dma::dma_stream:: as VmIo>>::read" +anchor = "dma::dma_stream::::read" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_stream:: as VmIo>>::write" +anchor = "dma::dma_stream::::write" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_stream::::drop" +type = "function" + +[[verified]] +name = "dma::dma_stream:: as VmIo<()>>::read" +anchor = "dma::dma_stream:: as VmIo>::read" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_stream:: as VmIo<()>>::write" +anchor = "dma::dma_stream:: as VmIo>::write" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_stream:: as Clone>::clone" +type = "function" + +[[planned]] +name = "dma::dma_stream:: as HasDaddr>::daddr" +type = "function" + +[[planned]] +name = "dma::dma_stream:: as HasPaddr>::paddr" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::direction" +anchor = "dma::dma_stream::DmaStream::direction" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::map" +anchor = "dma::dma_stream::DmaStream::map" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_stream::DmaStream::nbytes" +anchor = "dma::dma_stream::DmaStream::nbytes" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::nframes" +anchor = "dma::dma_stream::DmaStream::nframes" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::reader" +anchor = "dma::dma_stream::DmaStream::reader" +type = "function" +how = "rewrite" + +# The status table marks DmaStream::segment as verified, but the current API is +# removed and the only direct RwArc access helper has external_body. +[[planned]] +name = "dma::dma_stream::DmaStream::segment" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::sync" +anchor = "dma::dma_stream::DmaStream::sync" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStream::writer" +anchor = "dma::dma_stream::DmaStream::writer" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_stream::DmaStream::daddr" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::daddr_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::direction_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::nbytes_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::nframes_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::paddr" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::paddr_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::read_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::read_inner_vmio" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::reader_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::write_inner_vmio" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStream::writer_inner" +type = "function" + +[[planned]] +name = "dma::dma_stream::DmaStreamSlice::daddr" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::nbytes" +anchor = "dma::dma_stream::DmaStreamSlice::nbytes" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::new" +anchor = "dma::dma_stream::DmaStreamSlice::new" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::offset" +anchor = "dma::dma_stream::DmaStreamSlice::offset" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::reader" +anchor = "dma::dma_stream::DmaStreamSlice::reader" +type = "function" +how = "rewrite" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::stream" +anchor = "dma::dma_stream::DmaStreamSlice::stream" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_stream::DmaStreamSlice::sync" +type = "function" + +[[verified]] +name = "dma::dma_stream::DmaStreamSlice::writer" +anchor = "dma::dma_stream::DmaStreamSlice::writer" +type = "function" +how = "rewrite" + +[[planned]] +name = "dma::dma_stream::DmaStreamSlice::sync" +type = "function" + +[[planned]] +name = "dma::remove_dma_mapping" +type = "function" + +[[verified]] +name = "frame:: as RCClone>::clone" +anchor = "frame:: as Clone>::clone" +type = "function" + +[[unsupported]] +name = "frame:: as Debug>::fmt" +type = "function" +reason = "other" + +[[verified]] +name = "frame:: as Drop>::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::Frame::eq" +anchor = "frame:: as PartialEq>::eq" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame:: as TryFrom>>::try_from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame:: as From>>::from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame:: as From>::from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::>>::try_from" +type = "function" +reason = "other" + +[[verified]] +name = "frame::Frame::borrow" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame::Frame::dyn_meta" +type = "function" +reason = "other" + +[[verified]] +name = "frame::Frame::from_in_use" +anchor = "frame::Frame::from_in_use" +type = "function" + +[[planned]] +name = "frame::Frame::into_dyn" +type = "function" + +[[verified]] +name = "frame::Frame::meta" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::Frame::slot" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::acquire_fence" +type = "function" + +[[unsupported]] +name = "frame::allocator::EarlyFrameAllocator::alloc" +type = "function" +reason = "other" + +[[planned]] +name = "frame::allocator::EarlyFrameAllocator::allocated_regions" +type = "function" + +[[unsupported]] +name = "frame::allocator::EarlyFrameAllocator::new" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::allocator::FrameAllocOptions::alloc_frame" +type = "function" +reason = "other" + +[[planned]] +name = "frame::allocator::FrameAllocOptions::alloc_frame_with" +type = "function" + +[[unsupported]] +name = "frame::allocator::FrameAllocOptions::alloc_segment" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::allocator::FrameAllocOptions::alloc_segment_with" +type = "function" +reason = "other" + +[[verified]] +name = "frame::allocator::FrameAllocOptions::zeroed" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::allocator::GlobalFrameAllocator::add_free_memory" +type = "function" + +[[planned]] +name = "frame::allocator::GlobalFrameAllocator::alloc" +type = "function" + +[[planned]] +name = "frame::allocator::GlobalFrameAllocator::dealloc" +type = "function" + +[[planned]] +name = "frame::allocator::early_alloc" +type = "function" + +[[planned]] +name = "frame::allocator::get_global_frame_allocator" +type = "function" + +[[planned]] +name = "frame::allocator::init" +type = "function" + +[[planned]] +name = "frame::allocator::init_early_allocator" +type = "function" + +[[planned]] +name = "frame::allocator::test_alloc_dealloc" +type = "function" + +[[planned]] +name = "frame::frame_ref:: as NonNullPtr>::ALIGN_BITS" +type = "function" + +[[verified]] +name = "frame::frame_ref:: as NonNullPtr>::from_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::frame_ref:: as NonNullPtr>::into_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::frame_ref:: as NonNullPtr>::raw_as_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::frame_ref:: as NonNullPtr>::ref_as_raw" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::frame_ref::NonNullPtr::ALIGN_BITS" +type = "function" + +[[planned]] +name = "frame::frame_ref::NonNullPtr::from_raw" +type = "function" + +[[planned]] +name = "frame::frame_ref::NonNullPtr::into_raw" +type = "function" + +[[planned]] +name = "frame::frame_ref::NonNullPtr::raw_as_ref" +type = "function" + +[[planned]] +name = "frame::frame_ref::NonNullPtr::ref_as_raw" +type = "function" + +[[verified]] +name = "frame::linked_list:: as Drop>::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::linked_list::CursorMut::current_meta" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::linked_list::CursorMut::take_current" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::linked_list::LinkedList::cursor_back_mut" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::linked_list::LinkedList::cursor_front_mut" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::linked_list::LinkedList::lazy_get_id" +type = "function" + +[[verified]] +name = "frame::linked_list::LinkedList::pop_back" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::linked_list::LinkedList::pop_front" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::max_paddr" +type = "function" + +[[verified]] +name = "frame::meta::AnyFrameMeta::on_drop" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::MetaSlot::addr_of" +type = "function" + +[[verified]] +name = "frame::meta::MetaSlot::as_meta_ptr" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::MetaSlot::cast_slot" +type = "function" + +[[planned]] +name = "frame::meta::MetaSlot::dyn_meta_ptr" +type = "function" + +[[verified]] +name = "frame::meta::MetaSlot::frame_paddr" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::meta::MetaSlot::get_from_in_use" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::MetaSlot::get_from_in_use_loop" +type = "function" + +[[verified]] +name = "frame::meta::MetaSlot::get_from_unused" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::meta::MetaSlot::write_meta" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::add_temp_linear_mapping" +type = "function" + +[[planned]] +name = "frame::meta::alloc_meta_frames" +type = "function" + +[[verified]] +name = "frame::meta::get_slot" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::init" +type = "function" + +[[planned]] +name = "frame::meta::is_initialized" +type = "function" + +[[verified]] +name = "frame::meta::mapping::frame_to_meta" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::meta::mapping::meta_to_frame" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::meta::mark_unusable_ranges" +type = "function" + +[[planned]] +name = "frame::meta::meta_slot_size" +type = "function" + +[[verified]] +name = "frame::segment:: as RCClone>::clone" +anchor = "frame::segment:: as Clone>::clone" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame::segment:: as Debug>::fmt" +type = "function" +reason = "other" + +[[verified]] +name = "frame::segment::Segment::drop" +anchor = "frame::segment:: as Drop>::drop" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame::segment:: as TryFrom>>::try_from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::segment:: as From>>::from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::segment::>>::from" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::segment::>>::try_from" +type = "function" +reason = "other" + +[[verified]] +name = "frame::segment::Segment::from_unused" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame::segment::Segment::next" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::unique:: as Debug>::fmt" +type = "function" +reason = "other" + +[[verified]] +name = "frame::unique::UniqueFrame::drop" +anchor = "frame::unique:: as Drop>::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::unique::Frame::from_unique" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "frame::unique::UniqueFrame::dyn_meta" +type = "function" +reason = "other" + +[[unsupported]] +name = "frame::unique::UniqueFrame::dyn_meta_mut" +type = "function" +reason = "other" + +[[verified]] +name = "frame::unique::UniqueFrame::from_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::unique::UniqueFrame::meta" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::unique::UniqueFrame::meta_mut" +type = "function" +how = "rewrite" + +[[verified]] +name = "frame::unique::UniqueFrame::repurpose" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::unique::UniqueFrame::slot" +type = "function" + +# The status table mentions UniqueFrame::reset_as_unused, which has no +# existence/signature delta. This current-only transmute helper has external_body. +[[planned]] +name = "frame::unique::UniqueFrame::transmute" +type = "function" + +[[verified]] +name = "frame::unique::UniqueFrame::try_from_shared" +type = "function" +how = "rewrite" + +[[planned]] +name = "frame::untyped::Segment::reader" +type = "function" + +[[planned]] +name = "frame::untyped::Segment::writer" +type = "function" + +[[planned]] +name = "io:: as From<& 'a [u8]>>::from" +type = "function" + +[[planned]] +name = "io:: as From<& 'a mut [u8]>>::from" +type = "function" + +[[planned]] +name = "io::<[u8] as AsVirtPtr>::as_virt_ptr" +type = "function" + +[[planned]] +name = "io::AsVirtPtr::as_virt_ptr" +type = "function" + +[[verified]] +name = "io::VmIo::read" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::read_bytes" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::read_slice" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::read_val" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::write" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::write_bytes" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::write_slice" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::write_val" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmIo::write_vals" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmReader::cursor" +type = "function" +how = "rewrite" + +[[planned]] +name = "io::VmReader::skip_in_place" +type = "function" + +[[verified]] +name = "io::VmReader::collect" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmReader::from_user_space" +type = "function" +how = "rewrite" + +[[planned]] +name = "io::VmReader::from" +type = "function" + +[[verified]] +name = "io::VmReader::from_kernel_space" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmReader::to_fallible" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmWriter::cursor" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::VmWriter::from_user_space" +type = "function" +how = "rewrite" + +[[planned]] +name = "io::VmWriter::from" +type = "function" + +[[verified]] +name = "io::VmWriter::from_kernel_space" +type = "function" +how = "rewrite" + +[[verified]] +name = "io::memcpy" +type = "function" +how = "rewrite" + +[[planned]] +name = "io::memcpy_fallible" +type = "function" + +[[planned]] +name = "io::memset_fallible" +type = "function" + +[[planned]] +name = "kspace::::TOP_LEVEL_CAN_UNMAP" +type = "function" + +[[planned]] +name = "kspace::::TOP_LEVEL_INDEX_RANGE" +type = "function" + +[[planned]] +name = "kspace::::item_from_raw" +type = "function" + +[[planned]] +name = "kspace::::item_into_raw" +type = "function" + +[[planned]] +name = "kspace::::clone" +type = "function" + +[[planned]] +name = "kspace::activate_kernel_page_table" +type = "function" + +[[planned]] +name = "kspace::init_kernel_page_table" +type = "function" + +[[planned]] +name = "kspace::kernel_loaded_offset" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::::drop" +type = "function" + +[[verified]] +name = "kspace::kvirt_area::KVirtArea::map_frames" +type = "function" +how = "rewrite" + +[[verified]] +name = "kspace::kvirt_area::KVirtArea::map_untracked_frames" +type = "function" +how = "rewrite" + +[[verified]] +name = "kspace::kvirt_area::KVirtArea::query" +type = "function" +how = "rewrite" + +[[planned]] +name = "kspace::kvirt_area::RangeAllocator::alloc" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::RangeAllocator::new" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::collect_largest_pages" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::disable_preempt" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::frame_into_dynframe" +type = "function" + +[[planned]] +name = "kspace::kvirt_area::get_kernel_page_table" +type = "function" + +[[planned]] +name = "nr_base_per_page" +type = "function" + +[[verified]] +name = "nr_subpage_per_huge" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_size" +type = "function" + +[[planned]] +name = "page_table::::ADDRESS_WIDTH" +type = "function" + +[[planned]] +name = "page_table::::BASE_PAGE_SIZE" +type = "function" + +[[planned]] +name = "page_table::::HIGHEST_TRANSLATION_LEVEL" +type = "function" + +[[planned]] +name = "page_table::::NR_LEVELS" +type = "function" + +[[planned]] +name = "page_table::::PTE_SIZE" +type = "function" + +[[planned]] +name = "page_table::::VA_SIGN_EXT" +type = "function" + +[[verified]] +name = "page_table::PageTable::cursor" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::PageTable::cursor_mut" +type = "function" + +[[planned]] +name = "page_table::PageTable::empty_with_owner" +type = "function" + +[[planned]] +name = "page_table::PageTable::root_paddr" +type = "function" + +[[planned]] +name = "page_table::PageTable::shallow_copy" +type = "function" + +[[verified]] +name = "page_table::PageTable::create_user_page_table" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::PageTable::protect_flush_tlb" +type = "function" + +[[planned]] +name = "page_table::PageTable::activate" +type = "function" + +[[planned]] +name = "page_table::PageTableConfig::TOP_LEVEL_CAN_UNMAP" +type = "function" + +[[planned]] +name = "page_table::PageTableConfig::TOP_LEVEL_INDEX_RANGE" +type = "function" + +[[verified]] +name = "page_table::PageTableConfig::item_into_raw" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::PageTableEntryTrait::as_usize" +type = "function" + +[[planned]] +name = "page_table::PageTableEntryTrait::default" +type = "function" + +[[verified]] +name = "page_table::PageTableEntryTrait::is_last" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::is_present" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::new_absent" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::new_page" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::new_pt" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::paddr" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::PageTableEntryTrait::prop" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::RCClone::clone" +type = "function" + +[[planned]] +name = "page_table::apply_sign_ext" +type = "function" + +[[planned]] +name = "page_table::boot_pt::dismiss" +type = "function" + +[[verified]] +name = "page_table::boot_pt::with_borrow" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::cursor:: as Iterator>::next" +type = "function" + +[[planned]] +name = "page_table::cursor:: as Drop>::drop" +type = "function" + +[[planned]] +name = "page_table::cursor:: as Iterator>::next" +type = "function" + +[[planned]] +name = "page_table::cursor::Cursor::clone_item" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::cur_entry" +anchor = "page_table::cursor::Cursor::cur_entry" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::Cursor::cur_va_range" +anchor = "page_table::cursor::Cursor::cur_va_range" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::Cursor::find_next" +anchor = "page_table::cursor::Cursor::find_next" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::Cursor::find_next_impl" +anchor = "page_table::cursor::Cursor::find_next_impl" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::Cursor::jump" +anchor = "page_table::cursor::Cursor::jump" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::move_forward" +anchor = "page_table::cursor::Cursor::move_forward" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::new" +anchor = "page_table::cursor::Cursor::new" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::Cursor::pop_level" +anchor = "page_table::cursor::Cursor::pop_level" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::push_level" +anchor = "page_table::cursor::Cursor::push_level" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::query" +anchor = "page_table::cursor::Cursor::query" +type = "function" + +[[verified]] +name = "page_table::cursor::Cursor::virt_addr" +anchor = "page_table::cursor::Cursor::virt_addr" +type = "function" + +[[verified]] +name = "page_table::cursor::CursorMut::find_next" +anchor = "page_table::cursor::CursorMut::find_next" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::jump" +anchor = "page_table::cursor::CursorMut::jump" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::map" +anchor = "page_table::cursor::CursorMut::map" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::cursor::CursorMut::map_branch_pt" +type = "function" + +[[planned]] +name = "page_table::cursor::CursorMut::map_loop" +type = "function" + +[[verified]] +name = "page_table::cursor::CursorMut::new" +anchor = "page_table::cursor::CursorMut::new" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::protect_next" +anchor = "page_table::cursor::CursorMut::protect_next" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::query" +anchor = "page_table::cursor::CursorMut::query" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::replace_cur_entry" +anchor = "page_table::cursor::CursorMut::replace_cur_entry" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::take_next" +anchor = "page_table::cursor::CursorMut::take_next" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::cursor::CursorMut::virt_addr" +anchor = "page_table::cursor::CursorMut::virt_addr" +type = "function" + +[[verified]] +name = "page_table::cursor::PageTableFrag::va_range" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::cursor::locking::dfs_acquire_lock" +type = "function" + +[[planned]] +name = "page_table::cursor::locking::dfs_mark_stray_and_unlock" +type = "function" + +[[planned]] +name = "page_table::cursor::locking::dfs_release_lock" +type = "function" + +[[verified]] +name = "page_table::cursor::locking::lock_range" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::cursor::locking::try_traverse_and_lock_subtree_root" +type = "function" + +[[planned]] +name = "page_table::cursor::locking::unlock_range" +type = "function" + +[[planned]] +name = "page_table::cursor::page_size" +type = "function" + +[[planned]] +name = "page_table::cursor::path_slot_as_mut" +type = "function" + +[[planned]] +name = "page_table::is_valid_range" +type = "function" + +[[planned]] +name = "page_table::largest_pages" +type = "function" + +[[planned]] +name = "page_table::load_pte" +type = "function" + +[[verified]] +name = "page_table::node::entry:: as Deref>::deref" +anchor = "page_table::node:: as Deref>::deref" +type = "function" + +[[planned]] +name = "page_table::node:: as Drop>::drop" +type = "function" + +[[planned]] +name = "page_table::node:: as AnyFrameMeta>::is_untyped" +type = "function" + +[[verified]] +name = "page_table::node:: as AnyFrameMeta>::on_drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::entry" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::nr_children" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::nr_children_mut" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::read_pte" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::stray_mut" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::PageTableGuard::write_pte" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::node::PageTableNode::activate" +type = "function" + +[[planned]] +name = "page_table::node::PageTableNode::alloc" +type = "function" + +[[planned]] +name = "page_table::node::PageTableNode::first_activate" +type = "function" + +[[planned]] +name = "page_table::node::PageTableNodeRef::lock" +type = "function" + +[[verified]] +name = "page_table::node::PageTableNodeRef::make_guard_unchecked" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::child::Child::from_pte" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::child::Child::into_pte" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::child::Child::is_none" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::child::ChildRef::from_pte" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::entry::Entry::alloc_if_none" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::node::entry::Entry::new" +type = "function" + +[[verified]] +name = "page_table::node::entry::Entry::new_at" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::entry::Entry::protect" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::entry::Entry::replace" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::entry::Entry::split_if_mapped_huge" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::node::entry::Entry::to_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::nr_pte_index_bits" +type = "function" +how = "rewrite" + +[[verified]] +name = "page_table::page_walk" +type = "function" +how = "rewrite" + +[[planned]] +name = "page_table::pt_va_range_end" +type = "function" + +[[planned]] +name = "page_table::pt_va_range_start" +type = "function" + +[[planned]] +name = "page_table::pte_index" +type = "function" + +[[planned]] +name = "page_table::pte_index_bit_offset" +type = "function" + +[[planned]] +name = "page_table::sign_bit_of_va" +type = "function" + +[[planned]] +name = "page_table::store_pte" +type = "function" + +[[planned]] +name = "page_table::top_level_index_width" +type = "function" + +[[verified]] +name = "page_table::vaddr_range" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "tlb::TlbFlusher::dispatch_tlb_flush" +anchor = "tlb::TlbFlusher::dispatch_tlb_flush" +type = "function" +reason = "lack-hardware-support" + +[[unsupported]] +name = "tlb::TlbFlusher::issue_tlb_flush" +anchor = "tlb::TlbFlusher::issue_tlb_flush" +type = "function" +reason = "lack-hardware-support" + +[[unsupported]] +name = "tlb::TlbFlusher::issue_tlb_flush_with" +anchor = "tlb::TlbFlusher::issue_tlb_flush_with" +type = "function" +reason = "lack-hardware-support" + +[[verified]] +name = "tlb::TlbFlusher::new" +anchor = "tlb::TlbFlusher::new" +type = "function" +how = "rewrite" + +[[unsupported]] +name = "tlb::TlbFlusher::sync_tlb_flush" +anchor = "tlb::TlbFlusher::sync_tlb_flush" +type = "function" +reason = "lack-hardware-support" + +[[planned]] +name = "vm_space::::next" +type = "function" + +[[planned]] +name = "vm_space::::clone" +type = "function" + +[[planned]] +name = "vm_space::::TOP_LEVEL_CAN_UNMAP" +type = "function" + +[[planned]] +name = "vm_space::::TOP_LEVEL_INDEX_RANGE" +type = "function" + +[[verified]] +name = "vm_space::VmSpace::default" +anchor = "vm_space::::default" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::Cursor::find_next" +anchor = "vm_space::Cursor::find_next" +type = "function" + +[[verified]] +name = "vm_space::Cursor::jump" +anchor = "vm_space::Cursor::jump" +type = "function" + +[[verified]] +name = "vm_space::Cursor::query" +anchor = "vm_space::Cursor::query" +type = "function" + +[[verified]] +name = "vm_space::Cursor::virt_addr" +anchor = "vm_space::Cursor::virt_addr" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::find_next" +anchor = "vm_space::CursorMut::find_next" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::flusher" +anchor = "vm_space::CursorMut::flusher" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::CursorMut::jump" +anchor = "vm_space::CursorMut::jump" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::map" +anchor = "vm_space::CursorMut::map" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::protect_next" +anchor = "vm_space::CursorMut::protect_next" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::CursorMut::query" +anchor = "vm_space::CursorMut::query" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::unmap" +anchor = "vm_space::CursorMut::unmap" +type = "function" + +[[verified]] +name = "vm_space::CursorMut::virt_addr" +anchor = "vm_space::CursorMut::virt_addr" +type = "function" + +[[unsupported]] +name = "vm_space::VmSpace::activate" +type = "function" +reason = "lack-hardware-support" + +[[verified]] +name = "vm_space::VmSpace::cursor" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::VmSpace::cursor_mut" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::VmSpace::new" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::VmSpace::reader" +type = "function" +how = "rewrite" + +[[verified]] +name = "vm_space::VmSpace::writer" +type = "function" +how = "rewrite" + +[[planned]] +name = "vm_space::get_activated_vm_space" +type = "function" diff --git a/templates/rcu.toml b/templates/rcu.toml new file mode 100644 index 0000000..fc76f42 --- /dev/null +++ b/templates/rcu.toml @@ -0,0 +1,216 @@ +# Exec function existence/signature deltas against the configured anchor. + +[[planned]] +name = " as Drop>::drop" +type = "function" + +[[planned]] +name = " as Drop>::drop" +type = "function" + +[[planned]] +name = "Rcu

::read_with" +type = "function" + +[[verified]] +name = "RcuInner

::load_read_token" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuInner

::new_none" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuInner

::read_with" +type = "function" +how = "rewrite" + +[[planned]] +name = "RcuOption

::read_with" +type = "function" + +[[verified]] +name = "RcuOptionReadGuard

::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuOptionReadGuard

::get" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuReadGuard

::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuReadGuard

::get" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuReadGuardInner

::drop" +type = "function" +how = "rewrite" + +[[verified]] +name = "RcuReadGuardInner

::get" +type = "function" +how = "rewrite" + +[[planned]] +name = "delay_drop" +type = "function" + +[[planned]] +name = "finish_grace_period" +type = "function" + +[[planned]] +name = "monitor::GracePeriod::finish_grace_period" +type = "function" + +[[planned]] +name = "monitor::GracePeriod::is_complete" +type = "function" + +[[verified]] +name = "monitor::GracePeriod::new" +type = "function" +how = "rewrite" + +[[planned]] +name = "monitor::GracePeriod::restart" +type = "function" + +[[planned]] +name = "monitor::GracePeriod::take_callbacks" +type = "function" + +[[planned]] +name = "monitor::RcuMonitor::after_grace_period" +type = "function" + +[[planned]] +name = "monitor::RcuMonitor::finish_grace_period" +type = "function" + +[[verified]] +name = "monitor::RcuMonitor::is_monitoring" +type = "function" +how = "rewrite" + +[[verified]] +name = "monitor::RcuMonitor::new_data" +type = "function" +how = "rewrite" + +[[verified]] +name = "monitor::RcuMonitor::set_monitoring" +type = "function" +how = "rewrite" + +[[verified]] +name = "monitor::State::new" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtr>::into_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtrRef>::raw_as_ref" +anchor = "non_null:: as NonNullPtr>::raw_as_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtrRef>::ref_as_raw" +anchor = "non_null:: as NonNullPtr>::ref_as_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtr>::into_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtrRef>::raw_as_ref" +anchor = "non_null:: as NonNullPtr>::raw_as_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null:: as NonNullPtrRef>::ref_as_raw" +anchor = "non_null:: as NonNullPtr>::ref_as_raw" +type = "function" +how = "rewrite" + +[[planned]] +name = "non_null:: as Deref>::deref" +type = "function" + +[[planned]] +name = "non_null:: as NonNullPtr>::from_raw" +type = "function" + +[[planned]] +name = "non_null:: as NonNullPtr>::into_raw" +type = "function" + +[[planned]] +name = "non_null:: as NonNullPtr>::raw_as_ref" +type = "function" + +[[planned]] +name = "non_null:: as NonNullPtr>::ref_as_raw" +type = "function" + +[[planned]] +name = "non_null:: as Deref>::deref" +type = "function" + +[[verified]] +name = "non_null::NonNullPtr::from_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::NonNullPtr::into_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::NonNullPtrRef::raw_as_ref" +anchor = "non_null::NonNullPtr::raw_as_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::NonNullPtrRef::ref_as_raw" +anchor = "non_null::NonNullPtr::ref_as_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::either:: as NonNullPtr>::into_raw" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::either:: as NonNullPtrRef>::raw_as_ref" +anchor = "non_null::either:: as NonNullPtr>::raw_as_ref" +type = "function" +how = "rewrite" + +[[verified]] +name = "non_null::either:: as NonNullPtrRef>::ref_as_raw" +anchor = "non_null::either:: as NonNullPtr>::ref_as_raw" +type = "function" +how = "rewrite" diff --git a/templates/template.toml b/templates/template.toml index 91b012c..3a99f77 100644 --- a/templates/template.toml +++ b/templates/template.toml @@ -3,11 +3,11 @@ git = "https://github.com/asterinas/asterinas.git" tag = "v0.16.0" [[modules]] -name = "mm" -path = "modules/mm.toml" -source = "../../ostd/src/mm" +name = "rcu" +path = "/home/xxx/asterinas-fv/tools/alignment-checker/modules/rcu.toml" +source = "/home/xxx/asterinas-fv/ostd/src/sync/rcu" [[modules]] -name = "rcu" -path = "modules/rcu.toml" -source = "../../ostd/src/sync/rcu" +name = "mm" +path = "/home/xxx/asterinas-fv/tools/alignment-checker/modules/mm.toml" +source = "/home/xxx/asterinas-fv/ostd/src/mm"