Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
5e04c39
recognizing sniff-test attrs on functions
AlexanderPortland Sep 26, 2025
4231b15
'bad' function detection
AlexanderPortland Sep 26, 2025
115bb48
small cleanup
AlexanderPortland Sep 28, 2025
4589e69
snapshot testing
AlexanderPortland Oct 3, 2025
ea2ad40
early safety axioms
AlexanderPortland Oct 22, 2025
a435f56
detecting safety axioms & reporting errors
AlexanderPortland Oct 22, 2025
9ac5ab8
add proper readme
AlexanderPortland Oct 22, 2025
019f7d6
display of axiom issues
AlexanderPortland Oct 22, 2025
2b4a81d
fix sniff-test macro expansion when building normally
AlexanderPortland Oct 23, 2025
ea89266
rework annotation logic to use macros
AlexanderPortland Oct 23, 2025
29f5c3a
also detect calls to bad functions
AlexanderPortland Oct 23, 2025
11b9af0
make clippy happy
AlexanderPortland Oct 23, 2025
e376599
annotation consistency working for local crate
AlexanderPortland Oct 23, 2025
12b4bdb
actual snapshot testing now
AlexanderPortland Oct 24, 2025
43d74cf
add support for single-file snapshot tests
AlexanderPortland Oct 24, 2025
34ae713
Merge branch 'origin/main' into reachability
AlexanderPortland Oct 24, 2025
73d650d
update test workflow to build first
AlexanderPortland Oct 24, 2025
ef72847
make snapshot tests agnostic to install directory
AlexanderPortland Oct 24, 2025
ac34e4e
no color
AlexanderPortland Oct 24, 2025
c1bdcfe
remove binaries and don't do codegen
AlexanderPortland Oct 24, 2025
47f214c
register sniff-tool within the plugin
AlexanderPortland Oct 24, 2025
8741fff
ignore vscode settings
Yash-Agrawal10 Nov 6, 2025
d05c87e
reads toml file properly
Yash-Agrawal10 Nov 6, 2025
4c19e3c
attempt to actually use parsed toml
Yash-Agrawal10 Nov 6, 2025
5899cb4
toml working?
Yash-Agrawal10 Nov 6, 2025
801384b
added basic test for toml file
Yash-Agrawal10 Nov 6, 2025
2ebf569
logging improvements
AlexanderPortland Nov 7, 2025
c66b82d
added toml module
Yash-Agrawal10 Nov 10, 2025
44846e1
updated toml module and integrated with plugin
Yash-Agrawal10 Nov 10, 2025
913c37e
reworked and simplified parsing
AlexanderPortland Nov 11, 2025
ad6fb9f
error reporting again
AlexanderPortland Nov 11, 2025
e4a2555
cleanup toml module
Yash-Agrawal10 Nov 11, 2025
f2203fd
support for crate root attrs
AlexanderPortland Nov 11, 2025
f0bebd3
more documentation on sniff-test-attrs
AlexanderPortland Nov 11, 2025
af65504
code refactor and support for all pub fns
AlexanderPortland Nov 12, 2025
3f97d9d
allow justifications directly on axioms
AlexanderPortland Nov 12, 2025
bcca23b
merged reachability
Yash-Agrawal10 Nov 12, 2025
3588a19
temporary toml solution without proper string parsing
Yash-Agrawal10 Nov 12, 2025
641459d
parsing seems to not work
Yash-Agrawal10 Nov 13, 2025
fbf92ee
toml is working
Yash-Agrawal10 Nov 13, 2025
fd53659
added a test for toml
Yash-Agrawal10 Nov 13, 2025
6e23aef
fixed function safety documentation
Yash-Agrawal10 Nov 13, 2025
1cfbcde
Merge branch 'main' into yash-toml-file
AlexanderPortland Nov 13, 2025
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
73 changes: 64 additions & 9 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions crates/sniff-test/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ serde = { version = "1", features = ["derive"] }
regex = "1.11.2"
anyhow = "1.0.100"
itertools = "0.14.0"
toml = "0.9.8"
log = "0.4.28"

[build-dependencies]
Expand Down
35 changes: 28 additions & 7 deletions crates/sniff-test/src/annotations/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
//! The utilities needed to find and parse code annotations.
use crate::{
annotations::doc::{Attributeable, DocStr, get_doc_str},
annotations::{
doc::{Attributeable, DocStr, get_doc_str},
toml::TomlAnnotation,
},
properties::Property,
};
use regex::Regex;
Expand All @@ -18,6 +21,7 @@ use std::{any::TypeId, borrow::Borrow, collections::HashMap, fmt::Debug, hash::H

mod doc;
mod span;
pub mod toml;

#[derive(Debug)]
pub enum PropertyViolation {
Expand Down Expand Up @@ -67,17 +71,22 @@ impl DefAnnotation {
/// annotated.
pub fn parse_fn_def<P: Property>(
tcx: TyCtxt<'_>,
toml_annotation: &TomlAnnotation,
fn_def: impl Into<rustc_span::def_id::DefId>,
property: P,
) -> Option<DefAnnotation> {
// TODO: add yash's logic here for checking the override toml file first.

// 1. get the doc string
// 1. Get the DefId
let fn_def: rustc_span::def_id::DefId = fn_def.into();
let doc_str = get_doc_str(fn_def, tcx)?;

// 2. parse the doc string based on the property
parse_fn_def_src(doc_str, property)
// 2. Check if we have a TOML override for this function
if let Some(toml_str) = toml_annotation.get_requirements_string(&tcx.def_path_str(fn_def)) {
parse_fn_def_toml(toml_str, property)
} else {
// 3. No TOML override found, get the doc string from source code
let doc_str = get_doc_str(fn_def, tcx)?;
// 4. parse the doc string based on the property
parse_fn_def_src(doc_str, property)
}
}

fn parent_block_expr<'tcx>(
Expand Down Expand Up @@ -136,3 +145,15 @@ fn parse_fn_def_src<P: Property>(doc_str: DocStr, property: P) -> Option<DefAnno
source: AnnotationSource::DocComment(doc_str.span_of_chars(found.range())),
})
}

fn parse_fn_def_toml<P: Property>(toml_str: &str, property: P) -> Option<DefAnnotation> {
property
.fn_def_regex()
.find(toml_str)
.map(|found| DefAnnotation {
property_name: P::property_name(),
local_violation_annotation: PropertyViolation::Unconditional,
text: toml_str[found.end()..].to_string(),
source: AnnotationSource::TomlOverride,
})
}
104 changes: 104 additions & 0 deletions crates/sniff-test/src/annotations/toml.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
//! Module for parsing annotations from TOML files.
//! Each top-level TOML table key is a function name with a `requirements` string.
//! ```toml
//! [function_name]
//! requirements = """
//! # Safety
//! * 'requirement 1': Description of requirement 1
//! * 'requirement 2': Description of requirement 2
//! """
//! ```

use std::collections::HashMap;

use rustc_span::{
DUMMY_SP,
source_map::{Spanned, respan},
};

use crate::annotations::DefAnnotation;

/// Struct encapsulating annotations parsed from a TOML file.
#[derive(Default)]
pub struct TomlAnnotation {
function_to_requirements_string: HashMap<String, String>,
}

/// Errors that can occur when parsing TOML annotations.
#[derive(Debug)]
pub enum TomlParseError {
Io(std::io::Error),
Toml(toml::de::Error),
Schema(String),
}

impl From<std::io::Error> for TomlParseError {
fn from(err: std::io::Error) -> Self {
TomlParseError::Io(err)
}
}

impl From<toml::de::Error> for TomlParseError {
fn from(err: toml::de::Error) -> Self {
TomlParseError::Toml(err)
}
}

impl TomlAnnotation {
/// Parses a TOML annotation file and returns a [`TomlAnnotation`] struct.
/// Fails on any errors, never returning partial results.
/// If the file does not exist, returns an empty [`TomlAnnotation`].
/// TODO: Use real spans if possible.
pub fn from_file<P: AsRef<std::path::Path>>(path: P) -> Result<Self, TomlParseError> {
// Get the contents of the TOML file
let text = match std::fs::read_to_string(path) {
Ok(text) => text,
Err(e) if e.kind() == std::io::ErrorKind::NotFound => {
// File does not exist, return empty annotations
return Ok(TomlAnnotation::default());
}
Err(e) => return Err(TomlParseError::Io(e)),
};

// Parse the TOML file into a map from function names to requirement strings
let value: toml::Value = toml::from_str(&text)?;
let Some(table) = value.as_table() else {
return Err(TomlParseError::Schema(
"Expected a TOML table at the top level".to_string(),
));
};

// Parse each function's requirements
let mut function_to_requirements_string: HashMap<String, String> = HashMap::new();
for (function_name, value) in table {
let Some(inner_table) = value.as_table() else {
return Err(TomlParseError::Schema(format!(
"Expected a TOML table for function {function_name}"
)));
};
let Some(requirements_value) = inner_table.get("requirements") else {
return Err(TomlParseError::Schema(format!(
"Expected a 'requirements' string for function {function_name}"
)));
};
let Some(requirements_string) = requirements_value.as_str() else {
return Err(TomlParseError::Schema(format!(
"Expected 'requirements' to be a string for function {function_name}"
)));
};

function_to_requirements_string
.insert(function_name.clone(), requirements_string.to_string());
}

// Return the parsed annotations
Ok(TomlAnnotation {
function_to_requirements_string,
})
}

/// Retrieves the requirements for a given function name, if any.
pub fn get_requirements_string(&self, function_name: &str) -> Option<&String> {
self.function_to_requirements_string.get(function_name)
}
}
48 changes: 35 additions & 13 deletions crates/sniff-test/src/check/mod.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,21 @@
use itertools::Itertools;
use rustc_errors::{Diag, DiagCtxtHandle};
use rustc_hir::def_id::{DefId, LocalDefId};
use rustc_middle::ty::TyCtxt;
use rustc_span::{ErrorGuaranteed, source_map::Spanned, sym::todo_macro};

use crate::{
annotations::{self, parse_expr},
annotations::{
self, parse_expr,
toml::{TomlAnnotation, TomlParseError},
},
properties::{self, Axiom, FoundAxiom, Property},
reachability::{self, CallsWObligations, LocallyReachable},
utils::SniffTestDiagnostic,
};
use itertools::Itertools;
use rustc_errors::{Diag, DiagCtxtHandle};
use rustc_hir::def_id::{DefId, LocalDefId};
use rustc_middle::ty::TyCtxt;
use rustc_span::{
DUMMY_SP, ErrorGuaranteed,
source_map::{Spanned, respan},
sym::todo_macro,
};

mod err;
mod expr;
Expand All @@ -19,6 +25,20 @@ pub fn check_properly_annotated<P: Property>(
tcx: TyCtxt,
property: P,
) -> Result<(), ErrorGuaranteed> {
// Parse TOML annotations from file
let toml_path = "sniff-test.toml";
let toml_annotations = match TomlAnnotation::from_file(toml_path) {
Ok(annotations) => annotations,
Err(e) => {
tcx.dcx()
.struct_warn(format!(
"Failed to parse TOML annotations from {toml_path}: {e:?}"
))
.emit();
TomlAnnotation::default()
}
};

let entry = reachability::analysis_entry_points::<P>(tcx);

// Debug print all our entries and where they are in the src
Expand All @@ -40,19 +60,20 @@ pub fn check_properly_annotated<P: Property>(

// For all reachable local function definitions, ensure their axioms align with their annotations.
for func in reachable {
check_function_properties(tcx, func, property)?;
check_function_properties(tcx, &toml_annotations, func, property)?;
}

Ok(())
}

fn check_function_properties<P: Property>(
tcx: TyCtxt,
toml_annotations: &TomlAnnotation,
func: LocallyReachable,
property: P,
) -> Result<(), ErrorGuaranteed> {
// Look for the local annotation
let annotation = annotations::parse_fn_def(tcx, func.reach, property);
let annotation = annotations::parse_fn_def(tcx, toml_annotations, func.reach, property);

// If the function we're analyzing is directly annotated, we trust the user's annotation
// and don't need to analyze its body locally. Vitally, we'll still explore functions it calls
Expand All @@ -71,10 +92,11 @@ fn check_function_properties<P: Property>(
log::debug!("fn {:?} has obligations {:?}", func.reach, annotation);

// Find all calls that have obligations.
let unjustified_calls = reachability::find_calls_w_obligations(tcx, &func, property)
// Filter those with only callsites that haven't been justified.
.filter_map(only_unjustified_callsites(tcx, func.reach, property))
.collect::<Vec<_>>();
let unjustified_calls =
reachability::find_calls_w_obligations(tcx, toml_annotations, &func, property)
// Filter those with only callsites that haven't been justified.
.filter_map(only_unjustified_callsites(tcx, func.reach, property))
.collect::<Vec<_>>();

// If we have obligations, we've dismissed them

Expand Down
Loading
Loading