diff --git a/src/assail/analyzer.rs b/src/assail/analyzer.rs index fb0af3a..c7eecc3 100644 --- a/src/assail/analyzer.rs +++ b/src/assail/analyzer.rs @@ -3668,25 +3668,18 @@ impl Analyzer { // matching so that doc-comments documenting "no sorry" do not produce // false positives. let code = strip_proof_comments(content, "--", Some(("/-", "-/"))); - // sorry — banned proof escape hatch: admits unproven propositions - let sorry_count = code.matches("sorry").count(); - if sorry_count > 0 { - stats.unsafe_blocks += sorry_count; - weak_points.push(WeakPoint { - file: None, - line: None, - category: WeakPointCategory::ProofDrift, - location: Some(file_path.to_string()), - severity: Severity::Critical, - description: format!( - "{} sorry (banned proof escape hatch — admits unproven proposition) in {}", - sorry_count, file_path - ), - recommended_attack: vec![AttackAxis::Cpu], - suppressed: false, - test_context: None, - }); - } + // sorry — banned proof escape hatch: admits unproven propositions. + // One finding per occurrence, anchored to its line, so an audited + // occurrence can carry an inline `panic-attack: accepted` marker + // without hiding any other sorry in the same file. + push_line_anchored_proof_drift( + &code, + "sorry", + "1 sorry (banned proof escape hatch — admits unproven proposition)", + file_path, + stats, + weak_points, + ); // unsafeNativeIO — bypasses IO monad discipline let unsafe_io_count = @@ -3847,25 +3840,16 @@ impl Analyzer { // proof-escape hatches. See #43. let without_blocks = strip_proof_comments(content, "", Some(("(*", "*)"))); let code = strip_isabelle_prose(&without_blocks); - // sorry — Isabelle's admitted-proof escape hatch (banned estate-wide) - let sorry_count = code.matches("sorry").count(); - if sorry_count > 0 { - stats.unsafe_blocks += sorry_count; - weak_points.push(WeakPoint { - file: None, - line: None, - category: WeakPointCategory::ProofDrift, - location: Some(file_path.to_string()), - severity: Severity::Critical, - description: format!( - "{} sorry (banned — unfinished Isabelle proof admitted without verification) in {}", - sorry_count, file_path - ), - recommended_attack: vec![AttackAxis::Cpu], - suppressed: false, - test_context: None, - }); - } + // sorry — Isabelle's admitted-proof escape hatch (banned estate-wide). + // One line-anchored finding per occurrence (see analyze_lean). + push_line_anchored_proof_drift( + &code, + "sorry", + "1 sorry (banned — unfinished Isabelle proof admitted without verification)", + file_path, + stats, + weak_points, + ); // oops — abandons an unfinished proof without even admitting it let oops_count = code.matches("oops").count(); @@ -5899,6 +5883,52 @@ fn strip_simple_double_quoted_strings(content: &str) -> String { out } +/// Append only the newlines of a span that is being removed, so text after +/// the span keeps its original line number. +fn push_newlines_of(out: &mut String, removed: &str) { + out.extend(removed.chars().filter(|c| *c == '\n')); +} + +/// 1-indexed line of every occurrence of `needle` in `code`. `code` must be +/// a position-preserving rewrite of the file (every newline kept), as +/// `strip_proof_comments` and `strip_isabelle_prose` produce. +fn occurrence_lines(code: &str, needle: &str) -> Vec { + code.match_indices(needle) + .map(|(at, _)| code[..at].matches('\n').count() as u32 + 1) + .collect() +} + +/// One Critical ProofDrift finding per occurrence of `needle` in `code`, each +/// anchored to its line so an inline `panic-attack: accepted` marker can +/// suppress exactly that occurrence. `code` must be position-preserving +/// (see `occurrence_lines`). +fn push_line_anchored_proof_drift( + code: &str, + needle: &str, + what: &str, + file_path: &str, + stats: &mut ProgramStatistics, + weak_points: &mut Vec, +) { + let lines = occurrence_lines(code, needle); + stats.unsafe_blocks += lines.len(); + for line in lines { + weak_points.push(WeakPoint { + file: None, + line: Some(line), + category: WeakPointCategory::ProofDrift, + location: Some(file_path.to_string()), + severity: Severity::Critical, + description: format!("{what} in {file_path}:{line}"), + recommended_attack: vec![AttackAxis::Cpu], + suppressed: false, + test_context: None, + }); + } +} + +/// Remove proof-language comments while keeping every newline, so a line +/// number taken from the result is a line number in `content`. fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, &str)>) -> String { // First strip block comments greedily, left-to-right. let mut without_blocks = String::with_capacity(content.len()); @@ -5908,9 +5938,11 @@ fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, & without_blocks.push_str(&rest[..start]); let after_open = &rest[start + open.len()..]; if let Some(end) = after_open.find(close) { + push_newlines_of(&mut without_blocks, &after_open[..end]); rest = &after_open[end + close.len()..]; } else { - // Unterminated block comment — drop the rest. + // Unterminated block comment — drop the rest, keep its lines. + push_newlines_of(&mut without_blocks, after_open); rest = ""; break; } @@ -5920,12 +5952,13 @@ fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, & without_blocks.push_str(content); } - // Then strip line comments. + // Then strip line comments. Split on '\n' (not `lines()`) so a trailing + // newline survives and the newline count is exactly preserved. if line_marker.is_empty() { return without_blocks; } let mut out = String::with_capacity(without_blocks.len()); - for (i, line) in without_blocks.lines().enumerate() { + for (i, line) in without_blocks.split('\n').enumerate() { let kept = match line.find(line_marker) { Some(idx) => &line[..idx], None => line, @@ -6050,6 +6083,7 @@ fn strip_isabelle_prose(content: &str) -> String { out.push_str(&rest[..next.0]); out.push(' '); + push_newlines_of(&mut out, &rest[next.0..next.1]); rest = &rest[next.1..]; } } @@ -8361,3 +8395,76 @@ pub fn safe_get_x() -> Option { ); } } + +#[cfg(test)] +mod proof_line_anchor_tests { + use super::*; + use proptest::prelude::*; + + /// Inputs built from the tokens the proof strippers react to, so the + /// generator actually reaches unterminated blocks, nested cartouches and + /// comments that span lines. + fn proof_source() -> impl Strategy { + let tokens = [ + "(*", + "*)", + "/-", + "-/", + "--", + "//", + "text ", + "\\", + "\\", + "@{text ", + "}", + "{", + "\n", + "\r\n", + "sorry", + "a", + " ", + ]; + proptest::collection::vec(proptest::sample::select(tokens.to_vec()), 0..60) + .prop_map(|parts| parts.concat()) + } + + proptest! { + // The invariant line anchoring rests on: stripping never adds, + // drops or reorders a newline, so the line of any surviving + // character is its line in the original file. + #[test] + fn proof_strippers_preserve_every_newline(src in proof_source()) { + let newlines = src.matches('\n').count(); + for (line_marker, block) in [ + ("--", Some(("/-", "-/"))), + ("", Some(("(*", "*)"))), + ("//", None), + ] { + let out = strip_proof_comments(&src, line_marker, block); + prop_assert_eq!(out.matches('\n').count(), newlines); + } + let isabelle = strip_isabelle_prose(&strip_proof_comments(&src, "", Some(("(*", "*)")))); + prop_assert_eq!(isabelle.matches('\n').count(), newlines); + } + } + + #[test] + fn occurrence_lines_are_one_indexed_per_occurrence() { + assert_eq!( + occurrence_lines("sorry\nx\n sorry sorry\n", "sorry"), + vec![1, 3, 3] + ); + assert!(occurrence_lines("no escape here\n", "sorry").is_empty()); + } + + #[test] + fn sorry_after_multiline_comment_keeps_its_line() { + let lean = "/- a\n b -/\ntheorem t : True := by\n sorry\n"; + let code = strip_proof_comments(lean, "--", Some(("/-", "-/"))); + assert_eq!(occurrence_lines(&code, "sorry"), vec![4]); + + let thy = "(* a\n b *)\ntext \\prose\n sorry in prose\\\nlemma l: True\n sorry\n"; + let code = strip_isabelle_prose(&strip_proof_comments(thy, "", Some(("(*", "*)")))); + assert_eq!(occurrence_lines(&code, "sorry"), vec![6]); + } +} diff --git a/src/assail/mod.rs b/src/assail/mod.rs index 3a62846..5e56161 100644 --- a/src/assail/mod.rs +++ b/src/assail/mod.rs @@ -436,6 +436,15 @@ pub fn apply_v255_context_suppression(report: &mut AssailReport) -> usize { let mut newly_suppressed = 0usize; let mut content_cache: std::collections::HashMap> = std::collections::HashMap::new(); + // Finding locations are relative to the scan root, not to the process + // working directory, so resolve them against the root. Without this, + // `assail ` run from anywhere but silently ignored every + // inline marker. + let scan_root: Option = if report.program_path.is_dir() { + Some(report.program_path.clone()) + } else { + report.program_path.parent().map(Path::to_path_buf) + }; for wp in &mut report.weak_points { // Determine the file path; prefer the structured `file` field, @@ -455,7 +464,14 @@ pub fn apply_v255_context_suppression(report: &mut AssailReport) -> usize { // None so we don't repeatedly retry. let content_opt = content_cache .entry(file.clone()) - .or_insert_with(|| std::fs::read_to_string(&file).ok()) + .or_insert_with(|| { + let rel = Path::new(&file); + scan_root + .as_deref() + .filter(|_| rel.is_relative()) + .and_then(|root| std::fs::read_to_string(root.join(rel)).ok()) + .or_else(|| std::fs::read_to_string(rel).ok()) + }) .clone(); // Always set test_context — even when the finding isn't a @@ -891,3 +907,63 @@ mod v255_context_suppression_tests { ); } } + +#[cfg(test)] +mod proof_marker_tests { + use super::*; + use crate::types::WeakPointCategory; + use std::fs; + use tempfile::TempDir; + + /// End to end through `analyze()`: each `sorry` is its own finding on + /// its own line, an inline marker suppresses only the occurrence it sits + /// above, and markers resolve against the scan root rather than the + /// process working directory (the test runs from the crate root). + #[test] + fn sorry_markers_suppress_only_the_marked_occurrence() { + let tmp = TempDir::new().unwrap(); + fs::write( + tmp.path().join("Fix.lean"), + "theorem a : True := by\n -- panic-attack: accepted (detector fixture)\n sorry\n\n\ + /- a\n multi-line\n comment -/\ntheorem b : True := by\n sorry\n", + ) + .unwrap(); + fs::write( + tmp.path().join("Fix.thy"), + "theory Fix imports Main begin\n(* a\n multi-line comment *)\n\ + text \\prose\n over lines\\\nlemma a: True\n \ + (* panic-attack: accepted (detector fixture) *)\n sorry\nlemma b: True\n sorry\nend\n", + ) + .unwrap(); + + let report = analyze(tmp.path()).unwrap(); + let mut got: Vec<(String, u32, bool)> = report + .weak_points + .iter() + .filter(|w| matches!(w.category, WeakPointCategory::ProofDrift)) + .filter(|w| w.description.contains("sorry")) + .map(|w| { + let loc = w.location.clone().unwrap_or_default(); + let name = Path::new(&loc) + .file_name() + .map(|n| n.to_string_lossy().into_owned()) + .unwrap_or(loc); + ( + name, + w.line.expect("sorry findings are line-anchored"), + w.suppressed, + ) + }) + .collect(); + got.sort(); + assert_eq!( + got, + vec![ + ("Fix.lean".to_string(), 3, true), + ("Fix.lean".to_string(), 9, false), + ("Fix.thy".to_string(), 8, true), + ("Fix.thy".to_string(), 10, false), + ] + ); + } +} diff --git a/src/comment_marker.rs b/src/comment_marker.rs index eab824e..81a9144 100644 --- a/src/comment_marker.rs +++ b/src/comment_marker.rs @@ -21,6 +21,8 @@ //! `;` Lisp / Scheme / Racket / Clojure / Common Lisp / Assembly //! `--` Haskell / Idris / SQL / Lua / Ada / Elm //! `%` Erlang / Prolog / MATLAB / LaTeX +//! `(*` Isabelle / Coq / Rocq / OCaml / SML / F* (start of line only; +//! a trailing `*)` is dropped from the reason) //! //! After the comment leader, we accept (whitespace tolerant): //! @@ -157,6 +159,12 @@ fn strip_to_after_comment_leader(line: &str) -> Option<&str> { if let Some(rest) = trimmed_start.strip_prefix("%") { return Some(rest); } + // ML-family block comment: Isabelle, Coq/Rocq, OCaml, SML, F*. + // Start-of-line only, like the leaders above: mid-line `(*` is also a + // C dereference or a Python splat. + if let Some(rest) = trimmed_start.strip_prefix("(*") { + return Some(rest); + } // Mid-line: only C-style `//` is safe — the others have non-comment // valid uses in expressions. @@ -196,6 +204,10 @@ fn strip_to_after_comment_leader(line: &str) -> Option<&str> { /// Clean the reason text: strip leading `:`, ` - `, parens, whitespace. fn clean_reason(s: &str) -> String { let mut s = s.trim(); + // A `(* ... *)` marker carries its closer on the same line. + if let Some(stripped) = s.strip_suffix("*)") { + s = stripped.trim(); + } if let Some(stripped) = s.strip_prefix(':') { s = stripped.trim(); } @@ -338,4 +350,36 @@ mod tests { assert!(is_suppressed_at(content, 0).is_none()); assert!(is_suppressed_at(content, 99).is_none()); } + + #[test] + fn ml_block_comment_marker_drops_its_closer() { + let m = parse_accepted_marker_in_line(" (* panic-attack: accepted (detector fixture) *)"); + assert_eq!(m, Some("(detector fixture)".to_string())); + let bare = parse_accepted_marker_in_line("(* panic-attack: accepted *)"); + assert_eq!(bare, Some(String::new())); + } + + #[test] + fn ml_block_comment_leader_is_start_of_line_only() { + // Mid-line `(*` is a C dereference or a Python splat, never a leader. + assert_eq!( + parse_accepted_marker_in_line(" sorry (* panic-attack: accepted *)"), + None + ); + assert_eq!( + parse_accepted_marker_in_line("x = (*p); /* panic-attack */"), + None + ); + assert_eq!( + parse_accepted_marker_in_line("(* an ordinary comment *)"), + None + ); + } + + #[test] + fn ml_marker_on_previous_line_suppresses() { + let content = "lemma a: True\n (* panic-attack: accepted *)\n sorry\n"; + assert!(is_suppressed_at(content, 3).is_some()); + assert!(is_suppressed_at(content, 1).is_none()); + } }