diff --git a/tools/hermes/src/main.rs b/tools/hermes/src/main.rs index f0de1ca4ef..c59dc02aa3 100644 --- a/tools/hermes/src/main.rs +++ b/tools/hermes/src/main.rs @@ -38,7 +38,9 @@ fn main() -> anyhow::Result<()> { let roots = resolve::resolve_roots(&resolve_args)?; let packages = scanner::scan_workspace(&roots)?; if packages.is_empty() { - log::warn!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify."); + log::warn!( + "No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify." + ); return Ok(()); } charon::run_charon(&resolve_args, &roots, &packages)?; diff --git a/tools/hermes/src/parse/attr.rs b/tools/hermes/src/parse/attr.rs new file mode 100644 index 0000000000..e80f8df824 --- /dev/null +++ b/tools/hermes/src/parse/attr.rs @@ -0,0 +1,889 @@ +use proc_macro2::Span; +use syn::{ExprLit, MetaNameValue}; + +use super::*; + +/// Represents a parsed attribute from a Hermes info string on a function. +#[derive(Debug, Clone, PartialEq, Eq)] +enum FunctionAttribute { + /// `spec`: Indicates a function specification and proof. + Spec, + /// `unsafe(axiom)`: Indicates an axiomatization of an unsafe function. + UnsafeAxiom, +} + +/// A parsed Hermes documentation block attached to a function. +#[derive(Debug, Clone)] +pub struct FunctionHermesBlock { + pub common: HermesBlockCommon, + pub requires: Vec, + pub ensures: Vec, + pub inner: FunctionBlockInner, +} + +#[derive(Debug, Clone)] +pub enum FunctionBlockInner { + Proof(Vec), + Axiom(Vec), +} + +/// A parsed Hermes documentation block attached to a struct, enum, or union. +#[derive(Debug, Clone)] +pub struct TypeHermesBlock { + pub common: HermesBlockCommon, + pub is_valid: Vec, +} + +/// A parsed Hermes documentation block attached to a trait. +#[derive(Debug, Clone)] +pub struct TraitHermesBlock { + pub common: HermesBlockCommon, + pub is_safe: Vec, +} + +/// A parsed Hermes documentation block attached to an impl. +#[derive(Debug, Clone)] +pub struct ImplHermesBlock { + pub common: HermesBlockCommon, +} + +#[derive(Debug, Clone)] +pub struct HermesBlockCommon { + pub header: Vec, + /// The span of the entire block, including the opening and closing ` ``` ` + /// lines. + pub content_span: Span, + /// The span of the opening ` ``` ` line. + pub start_span: Span, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +enum ParsedInfoString { + FunctionMode(FunctionAttribute), + GenericMode, +} + +/// Parses the info string of a code block. +/// +/// * `info`: The info string text (e.g. "lean, hermes, spec"). +/// +/// Returns: +/// * `Ok(Some(Some(attr)))` if `hermes` was found and had valid arguments. +/// * `Ok(Some(None))` if `hermes` was found but had no arguments. +/// * `Ok(None)` if `hermes` was not found. +/// * `Err(msg)` if `hermes` was found but had invalid arguments. +fn parse_hermes_info_string(info: &str) -> Result, String> { + let mut tokens = info.split(',').map(str::trim).filter(|s| !s.is_empty()); + + // Find and consume the `hermes` token. + if tokens.find(|&t| t == "hermes").is_none() { + return Ok(None); + } + + let first_arg = tokens.next(); + let second_arg = tokens.next(); + match (first_arg, second_arg) { + (Some(first), Some(second)) => { + return Err(format!( + "Multiple attributes specified after 'hermes' ('{first}', '{second}'). Only one attribute is allowed." + )); + } + (None, None) => return Ok(Some(ParsedInfoString::GenericMode)), + (Some("spec"), None) => { + return Ok(Some(ParsedInfoString::FunctionMode(FunctionAttribute::Spec))); + } + (Some("unsafe(axiom)"), None) => { + return Ok(Some(ParsedInfoString::FunctionMode(FunctionAttribute::UnsafeAxiom))); + } + (Some(token), None) if token.starts_with("unsafe") => { + return Err(format!( + "Unknown or malformed attribute: '{token}'. Did you mean 'unsafe(axiom)'?" + )); + } + (Some(token), None) => { + return Err(format!( + "Unrecognized Hermes attribute: '{token}'. Supported attributes are 'spec', 'unsafe(axiom)'." + )); + } + (None, Some(_)) => unreachable!(), + } +} + +/// Helper to extract the string content and span from a `#[doc = "..."]` attribute. +/// +/// Returns `Some((content, span))` if the attribute is a doc comment. +fn extract_doc_line(attr: &Attribute) -> Option<(String, Span)> { + if !attr.path().is_ident("doc") { + return None; + } + + match &attr.meta { + Meta::NameValue(MetaNameValue { + value: Expr::Lit(ExprLit { lit: Lit::Str(s), .. }), + .. + }) => Some((s.value(), s.span())), + _ => None, + } +} + +// Common parsing logic extracted +fn parse_block_lines<'a, I>( + iter: &mut I, + start: Span, +) -> Result<(String, Vec, Span), Error> +where + I: Iterator, +{ + let mut content = String::new(); + let mut lines = Vec::new(); + let mut end = start; + let mut closed = false; + + for next in iter { + let Some((line, span)) = extract_doc_line(next) else { break }; + + if line.trim().starts_with("```") { + closed = true; + break; + } + + content.push_str(&line); + content.push('\n'); + lines.push(SpannedLine { content: line, span: span_to_miette(span), raw_span: span }); + end = span; + } + + if !closed { + return Err(Error::new(start, "Unclosed Hermes block in documentation.")); + } + + Ok((content, lines, end)) +} + +fn parse_hermes_block_common( + attrs: &[Attribute], + check_info: impl Fn(&ParsedInfoString, Span) -> Result<(), Error>, +) -> Result, Error> { + let mut iter = attrs.iter(); + let mut block = None; + + while let Some(attr) = iter.next() { + let Some((text, start)) = extract_doc_line(attr) else { continue }; + let Some(info) = text.trim().strip_prefix("```") else { continue }; + + let parsed_info = match parse_hermes_info_string(info.trim()) { + Ok(Some(a)) => a, + Ok(None) => continue, + Err(msg) => return Err(Error::new(start, msg)), + }; + + check_info(&parsed_info, start)?; + + if block.is_some() { + return Err(Error::new(start, "Multiple Hermes blocks found on a single item.")); + } + + let (_, lines, end) = parse_block_lines(&mut iter, start)?; + + let body = match RawHermesSpecBody::parse(&lines) { + Ok(body) => body, + Err((err_span, msg)) => { + let raw_span = + lines.iter().find(|l| l.span == err_span).map(|l| l.raw_span).unwrap_or(start); + return Err(Error::new(raw_span, msg)); + } + }; + block = Some(( + ParsedHermesBody { + body, + content_span: start.join(end).unwrap_or(start), + start_span: start, + }, + parsed_info, + )); + } + Ok(block) +} + +/// Returns an error containing `msg` if `lines` is non-empty. +fn reject_section(lines: &[SpannedLine], msg: &str) -> Result<(), Error> { + if let Some(line) = lines.first() { + Err(Error::new(line.raw_span, msg)) + } else { + Ok(()) + } +} + +fn parse_item_block_common( + attrs: &[Attribute], + context_name: &str, +) -> Result, Error> { + let Some((item, info)) = parse_hermes_block_common(attrs, |_, _| Ok(()))? else { + return Ok(None); + }; + if !matches!(info, ParsedInfoString::GenericMode) { + return Err(Error::new( + item.start_span, + format!("Functions attributes (like `spec`) are not permitted on {context_name}."), + )); + } + + let mut body = item.body; + reject_section(&body.requires, "`requires` sections are only permitted on functions.")?; + reject_section(&body.ensures, "`ensures` sections are only permitted on functions.")?; + reject_section(&body.proof, "`proof` sections are only permitted on `spec` functions.")?; + reject_section( + &body.axiom, + "`axiom` sections are only permitted on `unsafe(axiom)` functions.", + )?; + + let common = HermesBlockCommon { + header: std::mem::take(&mut body.header), + content_span: item.content_span, + start_span: item.start_span, + }; + + Ok(Some((common, body))) +} + +impl FunctionHermesBlock { + pub fn parse_from_attrs(attrs: &[Attribute]) -> Result, Error> { + let Some((item, parsed_info)) = parse_hermes_block_common(attrs, |_, _| Ok(()))? else { + return Ok(None); + }; + + let attribute = match parsed_info { + ParsedInfoString::FunctionMode(attr) => attr, + ParsedInfoString::GenericMode => FunctionAttribute::Spec, // Implicit `spec` for functions + }; + + let body = item.body; + reject_section(&body.is_valid, "`isValid` sections are only permitted on types.")?; + reject_section(&body.is_safe, "`isSafe` sections are only permitted on traits.")?; + + let inner = match attribute { + FunctionAttribute::Spec => { + reject_section( + &body.axiom, + "`axiom` sections are only permitted on `unsafe(axiom)` functions.", + )?; + FunctionBlockInner::Proof(body.proof) + } + FunctionAttribute::UnsafeAxiom => { + reject_section( + &body.proof, + "`proof` sections are only permitted on `spec` functions.", + )?; + FunctionBlockInner::Axiom(body.axiom) + } + }; + + Ok(Some(Self { + common: HermesBlockCommon { + header: body.header, + content_span: item.content_span, + start_span: item.start_span, + }, + requires: body.requires, + ensures: body.ensures, + inner, + })) + } +} + +impl TypeHermesBlock { + pub fn parse_from_attrs(attrs: &[Attribute]) -> Result, Error> { + let Some((common, body)) = parse_item_block_common(attrs, "types")? else { + return Ok(None); + }; + + reject_section(&body.is_safe, "`isSafe` sections are only permitted on traits.")?; + + if body.is_valid.is_empty() { + return Err(Error::new( + common.start_span, + "Hermes blocks on types must define an `isValid` type invariant.", + )); + } + + Ok(Some(Self { common, is_valid: body.is_valid })) + } +} + +impl TraitHermesBlock { + pub fn parse_from_attrs(attrs: &[Attribute]) -> Result, Error> { + let Some((common, body)) = parse_item_block_common(attrs, "traits")? else { + return Ok(None); + }; + + reject_section(&body.is_valid, "`isValid` sections are only permitted on types.")?; + + if body.is_safe.is_empty() { + return Err(Error::new( + common.start_span, + "Hermes blocks on traits must define an `isSafe` trait invariant. Did you misspell it?", + )); + } + + Ok(Some(Self { common, is_safe: body.is_safe })) + } +} + +impl ImplHermesBlock { + pub fn parse_from_attrs(attrs: &[Attribute]) -> Result, Error> { + let Some((common, body)) = parse_item_block_common(attrs, "impl items")? else { + return Ok(None); + }; + + reject_section(&body.is_valid, "`isValid` sections are only permitted on types.")?; + reject_section(&body.is_safe, "`isSafe` sections are only permitted on traits.")?; + + Ok(Some(Self { common })) + } +} + +/// A single parsed line from a documentation block, retaining structural layout info. +#[derive(Debug, Clone)] +pub struct SpannedLine { + pub content: String, + pub span: SourceSpan, + pub raw_span: Span, +} + +/// The structured content of a completely unvalidated Hermes specification block. +#[derive(Debug, Default, Clone)] +pub(super) struct RawHermesSpecBody { + /// Content before any keyword (e.g., Lean imports, let bindings, type invariants) + pub(super) header: Vec, + pub(super) requires: Vec, + pub(super) ensures: Vec, + pub(super) proof: Vec, + pub(super) axiom: Vec, + pub(super) is_valid: Vec, + pub(super) is_safe: Vec, +} + +pub(super) struct ParsedHermesBody { + pub(super) body: RawHermesSpecBody, + pub(super) content_span: Span, + pub(super) start_span: Span, +} + +impl RawHermesSpecBody { + /// Parses a sequence of raw documentation lines into structured sections. + fn parse<'a, I>(lines: I) -> Result + where + I: IntoIterator, + { + let mut spec = RawHermesSpecBody::default(); + + #[derive(Debug, Clone, Copy, PartialEq)] + enum Section { + Header, + Requires, + Ensures, + Proof, + Axiom, + IsValid, + IsSafe, + } + let mut current_section = Section::Header; + let mut baseline_indent: Option = None; + + fn get_vec(section: Section, spec: &mut RawHermesSpecBody) -> &mut Vec { + match section { + Section::Header => &mut spec.header, + Section::Requires => &mut spec.requires, + Section::Ensures => &mut spec.ensures, + Section::Proof => &mut spec.proof, + Section::Axiom => &mut spec.axiom, + Section::IsValid => &mut spec.is_valid, + Section::IsSafe => &mut spec.is_safe, + } + } + + // Matches exact keywords or keywords followed by any whitespace. + fn starts_with_keyword(line: &str, keyword: &str) -> bool { + if let Some(rest) = line.strip_prefix(keyword) { + rest.is_empty() || rest.starts_with(char::is_whitespace) + } else { + false + } + } + + let keywords = [ + ("requires", Section::Requires), + ("ensures", Section::Ensures), + ("proof", Section::Proof), + ("axiom", Section::Axiom), + ("isValid", Section::IsValid), + ("isSafe", Section::IsSafe), + ]; + + for line in lines { + let trimmed = line.content.trim(); + let span = line.span; + let raw_span = line.raw_span; + + if trimmed.is_empty() { + get_vec(current_section, &mut spec).push(SpannedLine { + content: line.content.clone(), + span, + raw_span, + }); + continue; + } + + let indent = line.content.len() - line.content.trim_start().len(); + + if let Some(&(keyword, section)) = + keywords.iter().find(|(k, _)| starts_with_keyword(trimmed, k)) + { + current_section = section; + baseline_indent = Some(indent); + if let Some(arg) = trimmed.strip_prefix(keyword) { + if !arg.trim().is_empty() { + get_vec(current_section, &mut spec).push(SpannedLine { + content: arg.to_string(), + span, + raw_span, + }); + } + } + continue; + } + + if current_section != Section::Header { + if indent <= baseline_indent.unwrap() { + return Err(( + span, + "Invalid indentation: expected an indented continuation or a valid Hermes keyword (requires, ensures, proof, axiom, isValid, isSafe). Did you misspell a keyword?".to_string() + )); + } + } + // Not a new keyword; continuation of the current section. + get_vec(current_section, &mut spec).push(SpannedLine { + content: line.content.clone(), + span, + raw_span, + }); + } + + Ok(spec) + } +} + +#[cfg(test)] +mod tests { + use syn::parse_quote; + + use super::*; + + #[test] + fn test_parse_hermes_info_string() { + // Not hermes + assert_eq!(parse_hermes_info_string(""), Ok(None)); + assert_eq!(parse_hermes_info_string("rust"), Ok(None)); + assert_eq!(parse_hermes_info_string("lean"), Ok(None)); + + // Just hermes + assert_eq!( + parse_hermes_info_string("lean, hermes"), + Ok(Some(ParsedInfoString::GenericMode)) + ); + assert_eq!(parse_hermes_info_string(" hermes "), Ok(Some(ParsedInfoString::GenericMode))); + assert_eq!( + parse_hermes_info_string("lean , hermes "), + Ok(Some(ParsedInfoString::GenericMode)) + ); + + // Valid attributes + assert!(matches!( + parse_hermes_info_string("hermes, spec"), + Ok(Some(ParsedInfoString::FunctionMode(FunctionAttribute::Spec))) + )); + assert!(matches!( + parse_hermes_info_string("lean,hermes,unsafe(axiom)"), + Ok(Some(ParsedInfoString::FunctionMode(FunctionAttribute::UnsafeAxiom))) + )); + + // Invalid attributes + assert!(parse_hermes_info_string("hermes, unknown").is_err()); + assert!(parse_hermes_info_string("hermes, unsafe").is_err()); + assert!(parse_hermes_info_string("hermes, spec, other").is_err()); + } + + #[test] + fn test_extract_doc_line() { + // Valid doc attribute + let attr: syn::Attribute = parse_quote!(#[doc = " test line"]); + let result = extract_doc_line(&attr).unwrap(); + assert_eq!(result.0, " test line"); + + // Non-doc attribute + let attr: syn::Attribute = parse_quote!(#[derive(Clone)]); + assert!(extract_doc_line(&attr).is_none()); + + // Alternate doc syntax (e.g., hidden) + let attr: syn::Attribute = parse_quote!(#[doc(hidden)]); + assert!(extract_doc_line(&attr).is_none()); + } + + #[test] + fn test_parse_from_attrs_valid_spec() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```lean, hermes, spec"]), + parse_quote!(#[doc = " body 1"]), + parse_quote!(#[doc = " body 2"]), + parse_quote!(#[doc = " ```"]), + ]; + let block = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap().unwrap(); + match block { + FunctionHermesBlock { + common: HermesBlockCommon { header, .. }, + inner: FunctionBlockInner::Proof(_), + .. + } => { + assert_eq!(header[0].content, " body 1"); + assert_eq!(header[1].content, " body 2"); + } + _ => panic!("Expected block with Proof inner"), + } + } + + #[test] + fn test_parse_from_attrs_valid_axiom() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```lean, hermes, unsafe(axiom)"]), + parse_quote!(#[doc = " body 1"]), + parse_quote!(#[doc = " body 2"]), + parse_quote!(#[doc = " ```"]), + ]; + let block = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap().unwrap(); + match block { + FunctionHermesBlock { + common: HermesBlockCommon { header, .. }, + inner: FunctionBlockInner::Axiom(_), + .. + } => { + assert_eq!(header[0].content, " body 1"); + assert_eq!(header[1].content, " body 2"); + } + _ => panic!("Expected block with Axiom inner"), + } + } + + #[test] + fn test_parse_from_attrs_unclosed() { + let attrs: Vec = + vec![parse_quote!(#[doc = " ```hermes"]), parse_quote!(#[doc = " no end fence"])]; + let err = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "Unclosed Hermes block in documentation."); + } + + #[test] + fn test_parse_from_attrs_interrupted() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " line 1"]), + parse_quote!(#[derive(Clone)]), // Interrupts contiguous doc lines + parse_quote!(#[doc = " ```"]), + ]; + let err = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "Unclosed Hermes block in documentation."); + } + + #[test] + fn test_parse_from_attrs_multiple_blocks() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " ```"]), + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " ```"]), + ]; + let err = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "Multiple Hermes blocks found on a single item."); + } + + fn mk_lines(lines: &[&str]) -> Vec { + lines + .iter() + .map(|l| SpannedLine { + content: (*l).to_string(), + span: miette::SourceSpan::new(0.into(), 0), + raw_span: proc_macro2::Span::call_site(), + }) + .collect() + } + + #[test] + fn test_hermes_spec_body_parse_empty() { + let lines = mk_lines(&[]); + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert!(spec.header.is_empty()); + assert!(spec.requires.is_empty()); + assert!(spec.ensures.is_empty()); + assert!(spec.proof.is_empty()); + assert!(spec.axiom.is_empty()); + } + + #[test] + fn test_hermes_spec_body_parse_header_only() { + let lines = mk_lines(&["import Foo", "def bar := 1"]); + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.header.len(), 2); + assert_eq!(spec.header[0].content, "import Foo"); + assert_eq!(spec.header[1].content, "def bar := 1"); + assert!(spec.requires.is_empty()); + } + + #[test] + fn test_hermes_spec_body_parse_strict_keywords() { + let lines = mk_lines(&[ + "requires_foo a", + "ensuresbar", + "proof_of_concept", + "axiomatic", + " requires ", // valid keyword + " genuine requirements ", + ]); + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + // The first four are headers because they don't match keywords strictly. + assert_eq!(spec.header.len(), 4); + assert_eq!(spec.header[0].content, "requires_foo a"); + assert_eq!(spec.header[1].content, "ensuresbar"); + assert_eq!(spec.header[2].content, "proof_of_concept"); + assert_eq!(spec.header[3].content, "axiomatic"); + + // " requires " switches section but adds no lines because its arg is empty. + // Following line is added verbatim to requires section. + assert_eq!(spec.requires.len(), 1); + assert_eq!(spec.requires[0].content, " genuine requirements "); + assert!(spec.ensures.is_empty()); + } + + #[test] + fn test_hermes_spec_body_parse_arguments_vs_continuation() { + let lines = mk_lines(&[ + "requires a > 0", + " and b < 0", // Continuation: keeps original whitespace + "ensures c == 1", + "proof", // standalone keyword + " trivial", + ]); + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert!(spec.header.is_empty()); + + assert_eq!(spec.requires.len(), 2); + // Prefix argument keeps its exact text post-"requires" (which is " a > 0"). + assert_eq!(spec.requires[0].content, " a > 0"); + // Continuation line keeps full exact original text. + assert_eq!(spec.requires[1].content, " and b < 0"); + + assert_eq!(spec.ensures.len(), 1); + assert_eq!(spec.ensures[0].content, " c == 1"); + + assert_eq!(spec.proof.len(), 1); + assert_eq!(spec.proof[0].content, " trivial"); + } + + #[test] + fn test_hermes_spec_body_parse_multiple_same_section() { + // Check that it can interleave sections or repeat them + let lines = mk_lines(&["requires a", "ensures b", "requires c", "axiom d"]); + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.requires.len(), 2); + assert_eq!(spec.requires[0].content, " a"); + assert_eq!(spec.requires[1].content, " c"); + + assert_eq!(spec.ensures.len(), 1); + assert_eq!(spec.ensures[0].content, " b"); + + assert_eq!(spec.axiom.len(), 1); + assert_eq!(spec.axiom[0].content, " d"); + } + + fn dummy_line(content: &str) -> SpannedLine { + SpannedLine { + content: content.to_string(), + span: (0, 0).into(), + raw_span: Span::call_site(), + } + } + + #[test] + fn test_parse_spec_valid_indentation() { + let lines = vec![ + dummy_line("open Aeneas"), + dummy_line("requires"), + dummy_line(" x > 0"), + dummy_line(" && y > 0"), + ]; + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.header.len(), 1); + assert_eq!(spec.requires.len(), 2); + assert_eq!(spec.requires[0].content, " x > 0"); + } + + #[test] + fn test_parse_spec_inline_args_valid() { + let lines = vec![ + dummy_line("requires a > 0"), + dummy_line("ensures\tb > 0"), // Tests tab whitespace + ]; + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.requires.len(), 1); + assert_eq!(spec.requires[0].content, " a > 0"); + assert_eq!(spec.ensures.len(), 1); + assert_eq!(spec.ensures[0].content, "\tb > 0"); + } + + #[test] + fn test_parse_spec_blank_lines() { + let lines = vec![ + dummy_line("requires"), + dummy_line(" a > 0"), + dummy_line(""), + dummy_line(" b > 0"), + ]; + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.requires.len(), 3); // 2 content lines + 1 blank line + } + + #[test] + fn test_parse_spec_header_no_indent_rules() { + let lines = vec![ + dummy_line("no indent"), + dummy_line(" four spaces"), + dummy_line("back to zero"), + dummy_line("requires x"), + ]; + let spec = RawHermesSpecBody::parse(&lines).unwrap(); + assert_eq!(spec.header.len(), 3); + assert_eq!(spec.requires.len(), 1); + } + + #[test] + fn test_parse_spec_err_typo_keyword() { + let lines = vec![ + dummy_line("requires"), + dummy_line(" a > 0"), + dummy_line("ensure"), // Typo, missing 's'. Indentation is 0. + dummy_line(" b > 0"), + ]; + let err = RawHermesSpecBody::parse(&lines).unwrap_err(); + assert!(err.1.contains("Invalid indentation")); + } + + #[test] + fn test_parse_spec_err_under_indented_continuation() { + let lines = vec![ + dummy_line(" requires"), // baseline is 2 + dummy_line(" a > 0"), // indent is 1 (1 <= 2) + ]; + let err = RawHermesSpecBody::parse(&lines).unwrap_err(); + assert!(err.1.contains("Invalid indentation")); + } + + #[test] + fn test_parse_from_attrs_not_hermes() { + let attrs: Vec = + vec![parse_quote!(#[doc = " ```lean"]), parse_quote!(#[doc = " ```"])]; + let block_func = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap(); + assert!(block_func.is_none()); + let block_item = TypeHermesBlock::parse_from_attrs(&attrs).unwrap(); + assert!(block_item.is_none()); + } + + #[test] + fn test_type_block_valid() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " isValid"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let block = TypeHermesBlock::parse_from_attrs(&attrs).unwrap().unwrap(); + assert_eq!(block.is_valid.len(), 1); + assert_eq!(block.is_valid[0].content, " val == true"); + } + + #[test] + fn test_trait_block_valid() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " isSafe"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let block = TraitHermesBlock::parse_from_attrs(&attrs).unwrap().unwrap(); + assert_eq!(block.is_safe.len(), 1); + assert_eq!(block.is_safe[0].content, " val == true"); + } + + #[test] + fn test_type_block_missing_is_valid() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " isVaild"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let err = TypeHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!( + err.to_string(), + "Hermes blocks on types must define an `isValid` type invariant." + ); + } + + #[test] + fn test_trait_block_missing_is_safe() { + let attrs: Vec = + vec![parse_quote!(#[doc = " ```hermes"]), parse_quote!(#[doc = " ```"])]; + let err = TraitHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!( + err.to_string(), + "Hermes blocks on traits must define an `isSafe` trait invariant. Did you misspell it?" + ); + } + + #[test] + fn test_function_rejects_invariants() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes, spec"]), + parse_quote!(#[doc = " isValid"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let err = FunctionHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "`isValid` sections are only permitted on types."); + } + + #[test] + fn test_type_rejects_function_clauses() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " requires"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " isValid"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let err = TypeHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "`requires` sections are only permitted on functions."); + } + + #[test] + fn test_type_rejects_is_safe() { + let attrs: Vec = vec![ + parse_quote!(#[doc = " ```hermes"]), + parse_quote!(#[doc = " isValid"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " isSafe"]), + parse_quote!(#[doc = " val == true"]), + parse_quote!(#[doc = " ```"]), + ]; + let err = TypeHermesBlock::parse_from_attrs(&attrs).unwrap_err(); + assert_eq!(err.to_string(), "`isSafe` sections are only permitted on traits."); + } +} diff --git a/tools/hermes/src/parse.rs b/tools/hermes/src/parse/mod.rs similarity index 53% rename from tools/hermes/src/parse.rs rename to tools/hermes/src/parse/mod.rs index 9a16be1f25..b75fcf0095 100644 --- a/tools/hermes/src/parse.rs +++ b/tools/hermes/src/parse/mod.rs @@ -1,17 +1,18 @@ +pub mod attr; + use std::{ - convert::Infallible, fs, io, path::{Path, PathBuf}, }; use log::{debug, trace}; use miette::{NamedSource, SourceSpan}; -use proc_macro2::Span; use syn::{ spanned::Spanned, visit::Visit, Attribute, Error, Expr, ImplItemFn, ItemEnum, ItemFn, ItemImpl, ItemMod, ItemStruct, ItemTrait, ItemUnion, Lit, Meta, TraitItemFn, }; +use self::attr::{FunctionHermesBlock, ImplHermesBlock, TraitHermesBlock, TypeHermesBlock}; use crate::errors::HermesError; /// A custom error type that associates a `syn::Error` with the file path @@ -84,17 +85,17 @@ impl TypeItem { } #[derive(Clone, Debug)] -pub struct HermesDecorated { +pub struct HermesDecorated { pub item: T, - pub hermes: HermesBlock, + pub hermes: B, } #[derive(Clone, Debug)] pub enum ParsedItem { - Function(HermesDecorated), - Type(HermesDecorated), - Trait(HermesDecorated), - Impl(HermesDecorated), + Function(HermesDecorated), + Type(HermesDecorated), + Trait(HermesDecorated), + Impl(HermesDecorated), } impl ParsedItem { @@ -116,42 +117,6 @@ impl ParsedItem { Self::Impl(x) => &x.item.attrs, } } - - /// Returns the content of the Hermes block. - pub fn hermes_content(&self) -> &str { - match self { - Self::Function(x) => &x.hermes.content, - Self::Type(x) => &x.hermes.content, - Self::Trait(x) => &x.hermes.content, - Self::Impl(x) => &x.hermes.content, - } - } -} - -/// Converts from a pair of `item` and `block: HermesBlock` to a -/// `HermesDecorated`, erroring if the `block` has an attribute. -/// -/// On success, passes the `HermesDecorate` to `f`. -fn try_from_raw_reject_attr) -> ParsedItem>( - item: T, - block: HermesBlock, - f: F, -) -> Result { - if let Some(_attr) = block.attribute { - return Err(( - span_to_miette(block.start_span), - "This item does not support Hermes attributes (like `spec` or `unsafe(axiom)`). Only generic `hermes` blocks are allowed.".to_string(), - )); - } - Ok(f(HermesDecorated { - item, - hermes: HermesBlock { - attribute: None, - content: block.content, - content_span: block.content_span, - start_span: block.start_span, - }, - })) } /// A complete parsed item including its module path and source file. @@ -281,43 +246,39 @@ where { /// Processes an `item` that may have a Hermes annotation. /// - /// If the `item` has a Hermes annotation, it is passed to `f` along with the - /// parsed `HermesBlock`. `f` may accept or reject the item (currently, - /// rejection can only happen when a Hermes attribute is preesnt on the - /// annotation (e.g., `spec` or `unsafe(axiom)`) and the item type does not - /// support attributes). - /// - /// If the item does not have a Hermes annotation, it is skipped. + /// If the `item` has a Hermes annotation, it is parsed by `parse` and + /// handed off to `wrap` to wrap it in the corresponding `ParsedItem` + /// variant. fn process_item< - T, - F: FnOnce(T, HermesBlock) -> Result, + T: Spanned + Clone, + B, + P: FnOnce(&[Attribute]) -> Result, Error>, + W: FnOnce(T, B) -> ParsedItem, >( &mut self, item: T, attrs: &[Attribute], - span: Span, - f: F, + parse: P, + wrap: W, ) { - let item_res = match HermesBlock::parse_from_attrs(attrs) { + let block_res = parse(attrs); + let item_res = match block_res { // This item doesn't have a Hermes annotation; skip it. Ok(None) => return, Ok(Some(_block)) if self.inside_block => Err(HermesError::NestedItemError { src: self.named_source.clone(), - span: span_to_miette(span), + span: span_to_miette(item.span()), msg: "Hermes cannot verify items defined inside function bodies or other blocks." .to_string(), }), - Ok(Some(block)) => f(item, block) - .map(|item| ParsedLeanItem { - item, + Ok(Some(block)) => { + let parsed_item = wrap(item.clone(), block); + Ok(ParsedLeanItem { + item: parsed_item, module_path: self.current_path.clone(), source_file: self.source_file.clone(), }) - .map_err(|(span, msg)| HermesError::DocBlockError { - src: self.named_source.clone(), - span, - msg, - }), + } Err(e) => { log::trace!("Error extracting ```lean block: {}", e); Err(HermesError::DocBlockError { @@ -328,7 +289,7 @@ where } }; - let source = &self.source_code.as_str()[span.byte_range()]; + let source = &self.source_code.as_str()[item.span().byte_range()]; (self.item_cb)(source, item_res); } } @@ -368,62 +329,68 @@ where trace!("Exiting module: {}", popped.unwrap_or_default()); } - fn visit_item_fn(&mut self, node: &'ast ItemFn) { - trace!("Visiting Fn {}", node.sig.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - Ok(ParsedItem::Function(HermesDecorated { - item: FunctionItem::Free(item), - hermes: block, - })) - }); - syn::visit::visit_item_fn(self, node); - } - - fn visit_item_struct(&mut self, node: &'ast ItemStruct) { - trace!("Visiting Struct {}", node.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - try_from_raw_reject_attr(item, block, |d| { - ParsedItem::Type(HermesDecorated { - item: TypeItem::Struct(d.item), - hermes: d.hermes, - }) - }) - }); - syn::visit::visit_item_struct(self, node); - } - - fn visit_item_enum(&mut self, node: &'ast ItemEnum) { - trace!("Visiting Enum {}", node.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - try_from_raw_reject_attr(item, block, |d| { - ParsedItem::Type(HermesDecorated { item: TypeItem::Enum(d.item), hermes: d.hermes }) - }) - }); - syn::visit::visit_item_enum(self, node); + fn visit_item_fn(&mut self, i: &'ast ItemFn) { + trace!("Visiting Fn {}", i.sig.ident); + self.process_item( + i.clone(), + &i.attrs, + FunctionHermesBlock::parse_from_attrs, + |item, hermes| { + ParsedItem::Function(HermesDecorated { item: FunctionItem::Free(item), hermes }) + }, + ); + syn::visit::visit_item_fn(self, i); + } + + fn visit_item_struct(&mut self, i: &'ast ItemStruct) { + trace!("Visiting Struct {}", i.ident); + self.process_item( + i.clone(), + &i.attrs, + TypeHermesBlock::parse_from_attrs, + |item, hermes| { + ParsedItem::Type(HermesDecorated { item: TypeItem::Struct(item), hermes }) + }, + ); + syn::visit::visit_item_struct(self, i); } - fn visit_item_union(&mut self, node: &'ast ItemUnion) { - trace!("Visiting Union {}", node.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - try_from_raw_reject_attr(item, block, |d| { - ParsedItem::Type(HermesDecorated { - item: TypeItem::Union(d.item), - hermes: d.hermes, - }) - }) - }); - syn::visit::visit_item_union(self, node); + fn visit_item_enum(&mut self, i: &'ast ItemEnum) { + trace!("Visiting Enum {}", i.ident); + self.process_item( + i.clone(), + &i.attrs, + TypeHermesBlock::parse_from_attrs, + |item, hermes| ParsedItem::Type(HermesDecorated { item: TypeItem::Enum(item), hermes }), + ); + syn::visit::visit_item_enum(self, i); + } + + fn visit_item_union(&mut self, i: &'ast ItemUnion) { + trace!("Visiting Union {}", i.ident); + self.process_item( + i.clone(), + &i.attrs, + TypeHermesBlock::parse_from_attrs, + |item, hermes| { + ParsedItem::Type(HermesDecorated { item: TypeItem::Union(item), hermes }) + }, + ); + syn::visit::visit_item_union(self, i); } - fn visit_item_trait(&mut self, node: &'ast ItemTrait) { - let name = node.ident.to_string(); + fn visit_item_trait(&mut self, i: &'ast ItemTrait) { + let name = i.ident.to_string(); trace!("Visiting Trait {}", name); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - try_from_raw_reject_attr(item, block, ParsedItem::Trait) - }); + self.process_item( + i.clone(), + &i.attrs, + TraitHermesBlock::parse_from_attrs, + |item, hermes| ParsedItem::Trait(HermesDecorated { item, hermes }), + ); self.current_path.push(name); - syn::visit::visit_item_trait(self, node); + syn::visit::visit_item_trait(self, i); self.current_path.pop(); } @@ -434,34 +401,41 @@ where self.inside_block = old_inside; } - fn visit_item_impl(&mut self, node: &'ast ItemImpl) { + fn visit_item_impl(&mut self, i: &'ast ItemImpl) { trace!("Visiting Impl"); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - try_from_raw_reject_attr(item, block, ParsedItem::Impl) - }); - syn::visit::visit_item_impl(self, node); - } - - fn visit_impl_item_fn(&mut self, node: &'ast ImplItemFn) { - trace!("Visiting ImplItemFn {}", node.sig.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - Ok(ParsedItem::Function(HermesDecorated { - item: FunctionItem::Impl(item), - hermes: block, - })) - }); - syn::visit::visit_impl_item_fn(self, node); - } - - fn visit_trait_item_fn(&mut self, node: &'ast TraitItemFn) { - trace!("Visiting TraitItemFn {}", node.sig.ident); - self.process_item(node.clone(), node.attrs.as_slice(), node.span(), |item, block| { - Ok(ParsedItem::Function(HermesDecorated { - item: FunctionItem::Trait(item), - hermes: block, - })) - }); - syn::visit::visit_trait_item_fn(self, node); + self.process_item( + i.clone(), + &i.attrs, + ImplHermesBlock::parse_from_attrs, + |item, hermes| ParsedItem::Impl(HermesDecorated { item, hermes }), + ); + syn::visit::visit_item_impl(self, i); + } + + fn visit_impl_item_fn(&mut self, i: &'ast ImplItemFn) { + trace!("Visiting ImplItemFn {}", i.sig.ident); + self.process_item( + i.clone(), + &i.attrs, + FunctionHermesBlock::parse_from_attrs, + |item, hermes| { + ParsedItem::Function(HermesDecorated { item: FunctionItem::Impl(item), hermes }) + }, + ); + syn::visit::visit_impl_item_fn(self, i); + } + + fn visit_trait_item_fn(&mut self, i: &'ast TraitItemFn) { + trace!("Visiting TraitItemFn {}", i.sig.ident); + self.process_item( + i.clone(), + &i.attrs, + FunctionHermesBlock::parse_from_attrs, + |item, hermes| { + ParsedItem::Function(HermesDecorated { item: FunctionItem::Trait(item), hermes }) + }, + ); + syn::visit::visit_trait_item_fn(self, i); } } @@ -518,249 +492,6 @@ fn span_to_miette(span: proc_macro2::Span) -> SourceSpan { SourceSpan::new(range.start.into(), range.end - range.start) } -use attr::*; -mod attr { - use proc_macro2::Span; - use syn::{ExprLit, MetaNameValue}; - - use super::*; - - /// Represents a parsed attribute from a Hermes info string. - #[derive(Debug, Clone, PartialEq, Eq)] - pub enum HermesAttr { - /// `spec`: Indicates a function specification and proof. - Spec, - /// `unsafe(axiom)`: Indicates an axiomatization of an unsafe function. - UnsafeAxiom, - } - - /// A fully parsed Hermes documentation block. - #[derive(Debug, Clone)] - pub struct HermesBlock { - /// The Hermes attribute parsed from the info string, if any. - pub attribute: Option, - /// The opaque content of the code block. - pub content: String, - /// The span covering the entire content (merged from start to end line). - pub content_span: Span, - /// The span of the opening ` ``` ` line. - pub start_span: Span, - } - - /// Parses the info string of a code block. - /// - /// * `info`: The info string text (e.g. "lean, hermes, spec"). - /// - /// Returns: - /// * `Ok(Some(Some(attr)))` if `hermes` was found and had valid arguments. - /// * `Ok(Some(None))` if `hermes` was found but had no arguments. - /// * `Ok(None)` if `hermes` was not found. - /// * `Err(msg)` if `hermes` was found but had invalid arguments. - fn parse_hermes_info_string(info: &str) -> Result>, String> { - let mut tokens = info.split(',').map(str::trim).filter(|s| !s.is_empty()); - - // Find and consume the `hermes` token. - if tokens.find(|&t| t == "hermes").is_none() { - return Ok(None); - } - - let first_arg = tokens.next(); - let second_arg = tokens.next(); - match (first_arg, second_arg) { - (Some(first), Some(second)) => return Err(format!( - "Multiple attributes specified after 'hermes' ('{first}', '{second}'). Only one attribute is allowed." - )), - (None, None) => return Ok(Some(None)), - (Some("spec"), None) => return Ok(Some(Some(HermesAttr::Spec))), - (Some("unsafe(axiom)"), None) => return Ok(Some(Some(HermesAttr::UnsafeAxiom))), - (Some(token), None) if token.starts_with("unsafe") => return Err(format!( - "Unknown or malformed attribute: '{token}'. Did you mean 'unsafe(axiom)'?" - )), - (Some(token), None) => return Err(format!( - "Unrecognized Hermes attribute: '{token}'. Supported attributes are 'spec', 'unsafe(axiom)'." - )), - (None, Some(_)) => unreachable!(), - } - } - - /// Helper to extract the string content and span from a `#[doc = "..."]` attribute. - /// - /// Returns `Some((content, span))` if the attribute is a doc comment. - fn extract_doc_line(attr: &Attribute) -> Option<(String, Span)> { - if !attr.path().is_ident("doc") { - return None; - } - - match &attr.meta { - Meta::NameValue(MetaNameValue { - value: Expr::Lit(ExprLit { lit: Lit::Str(s), .. }), - .. - }) => Some((s.value(), s.span())), - _ => None, - } - } - - impl HermesBlock { - pub fn parse_from_attrs( - attrs: &[Attribute], - ) -> Result>, Error> { - let mut iter = attrs.iter(); - let mut block = None; - - while let Some(attr) = iter.next() { - // Identify start of potential Hermes block. - let Some((text, start)) = extract_doc_line(attr) else { continue }; - let Some(info) = text.trim().strip_prefix("```") else { continue }; - - // Parse info string (skip if not `hermes`; err if invalid). - let attribute = match parse_hermes_info_string(info.trim()) { - Ok(Some(a)) => a, - Ok(None) => continue, - Err(msg) => return Err(Error::new(start, msg)), - }; - - if block.is_some() { - return Err(Error::new( - start, - "Multiple Hermes blocks found on a single item.", - )); - } - - // Consume body, ensuring strict contiguity (ie, rejecting - // interleaved attributes). - let (mut content, mut end, mut closed) = (String::new(), start, false); - for next in iter.by_ref() { - // Break on non-doc attr (triggers unclosed error below). - let Some((line, span)) = extract_doc_line(next) else { break }; - - if line.trim().starts_with("```") { - closed = true; - break; - } - - content.push_str(&line); - content.push('\n'); - end = span; - } - - if !closed { - return Err(Error::new(start, "Unclosed Hermes block in documentation.")); - } - - block = Some(HermesBlock { - attribute, - content, - content_span: start.join(end).unwrap_or(start), - start_span: start, - }); - } - - Ok(block) - } - } - - #[cfg(test)] - mod tests { - use syn::parse_quote; - - use super::*; - - #[test] - fn test_parse_hermes_info_string() { - // Not hermes - assert_eq!(parse_hermes_info_string(""), Ok(None)); - assert_eq!(parse_hermes_info_string("rust"), Ok(None)); - assert_eq!(parse_hermes_info_string("lean"), Ok(None)); - - // Just hermes - assert_eq!(parse_hermes_info_string("lean, hermes"), Ok(Some(None))); - assert_eq!(parse_hermes_info_string(" hermes "), Ok(Some(None))); - assert_eq!(parse_hermes_info_string("lean , hermes "), Ok(Some(None))); - - // Valid attributes - assert_eq!(parse_hermes_info_string("hermes, spec"), Ok(Some(Some(HermesAttr::Spec)))); - assert_eq!( - parse_hermes_info_string("lean,hermes,unsafe(axiom)"), - Ok(Some(Some(HermesAttr::UnsafeAxiom))) - ); - - // Invalid attributes - assert!(parse_hermes_info_string("hermes, unknown").is_err()); - assert!(parse_hermes_info_string("hermes, unsafe").is_err()); - assert!(parse_hermes_info_string("hermes, spec, other").is_err()); - } - - #[test] - fn test_extract_doc_line() { - // Valid doc attribute - let attr: syn::Attribute = parse_quote!(#[doc = " test line"]); - let result = extract_doc_line(&attr).unwrap(); - assert_eq!(result.0, " test line"); - - // Non-doc attribute - let attr: syn::Attribute = parse_quote!(#[derive(Clone)]); - assert!(extract_doc_line(&attr).is_none()); - - // Alternate doc syntax (e.g., hidden) - let attr: syn::Attribute = parse_quote!(#[doc(hidden)]); - assert!(extract_doc_line(&attr).is_none()); - } - - #[test] - fn test_parse_from_attrs_valid() { - let attrs: Vec = vec![ - parse_quote!(#[doc = " ```lean, hermes, spec"]), - parse_quote!(#[doc = " body 1"]), - parse_quote!(#[doc = " body 2"]), - parse_quote!(#[doc = " ```"]), - ]; - let block = HermesBlock::parse_from_attrs(&attrs).unwrap().unwrap(); - assert_eq!(block.attribute, Some(HermesAttr::Spec)); - assert_eq!(block.content, " body 1\n body 2\n"); - } - - #[test] - fn test_parse_from_attrs_unclosed() { - let attrs: Vec = - vec![parse_quote!(#[doc = " ```hermes"]), parse_quote!(#[doc = " no end fence"])]; - let err = HermesBlock::parse_from_attrs(&attrs).unwrap_err(); - assert_eq!(err.to_string(), "Unclosed Hermes block in documentation."); - } - - #[test] - fn test_parse_from_attrs_interrupted() { - let attrs: Vec = vec![ - parse_quote!(#[doc = " ```hermes"]), - parse_quote!(#[doc = " line 1"]), - parse_quote!(#[derive(Clone)]), // Interrupts contiguous doc lines - parse_quote!(#[doc = " ```"]), - ]; - let err = HermesBlock::parse_from_attrs(&attrs).unwrap_err(); - assert_eq!(err.to_string(), "Unclosed Hermes block in documentation."); - } - - #[test] - fn test_parse_from_attrs_multiple_blocks() { - let attrs: Vec = vec![ - parse_quote!(#[doc = " ```hermes"]), - parse_quote!(#[doc = " ```"]), - parse_quote!(#[doc = " ```hermes"]), - parse_quote!(#[doc = " ```"]), - ]; - let err = HermesBlock::parse_from_attrs(&attrs).unwrap_err(); - assert_eq!(err.to_string(), "Multiple Hermes blocks found on a single item."); - } - - #[test] - fn test_parse_from_attrs_not_hermes() { - let attrs: Vec = - vec![parse_quote!(#[doc = " ```lean"]), parse_quote!(#[doc = " ```"])]; - let block = HermesBlock::parse_from_attrs(&attrs).unwrap(); - assert!(block.is_none()); - } - } -} - #[cfg(test)] mod tests { use super::*; @@ -771,6 +502,18 @@ mod tests { items } + impl ParsedItem { + /// Returns the header of the Hermes block. + fn hermes_header(&self) -> &[attr::SpannedLine] { + match self { + Self::Function(f) => &f.hermes.common.header, + Self::Type(t) => &t.hermes.common.header, + Self::Trait(t) => &t.hermes.common.header, + Self::Impl(i) => &i.hermes.common.header, + } + } + } + #[test] fn test_parse_lean_block() { let code = r#" @@ -790,7 +533,7 @@ mod tests { fn foo() {}" ); assert!(matches!(item.item, ParsedItem::Function(_))); - assert_eq!(item.item.hermes_content(), " theorem foo : True := by trivial\n"); + assert_eq!(item.item.hermes_header()[0].content.trim(), "theorem foo : True := by trivial"); assert!(item.source_file.is_none()); } @@ -897,8 +640,8 @@ mod tests { let i2 = item2.as_ref().unwrap(); // Verify we got the right blocks for the right items - assert!(i1.item.hermes_content().contains("theorem a")); - assert!(i2.item.hermes_content().contains("theorem b")); + assert!(i1.item.hermes_header()[0].content.contains("theorem a")); + assert!(i2.item.hermes_header()[0].content.contains("theorem b")); // Verify source snippets match the function definition + doc comment assert!(src1.contains("theorem a")); diff --git a/tools/hermes/src/resolve.rs b/tools/hermes/src/resolve.rs index d9a85e55d7..fe40e243c6 100644 --- a/tools/hermes/src/resolve.rs +++ b/tools/hermes/src/resolve.rs @@ -262,7 +262,9 @@ fn resolve_packages<'a>( } } } else { - return Err(anyhow!("Could not determine package from current directory. Please use -p or --workspace.")); + return Err(anyhow!( + "Could not determine package from current directory. Please use -p or --workspace." + )); } } }