|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | +//! Idris2 `escape-hatch` (warn) — surface soundness escape hatches. |
| 5 | +//! |
| 6 | +//! The Idris2 analogue of the Agda [`super::escape_hatch::EscapeHatch`]. It |
| 7 | +//! shares the rule *name* `escape-hatch` deliberately: the reasoning graph |
| 8 | +//! (`crate::reason`) caps any `escape-hatch` node at amber, so a `believe_me` |
| 9 | +//! in Idris2 and a `believe_me` in Agda get the same honest treatment. |
| 10 | +//! |
| 11 | +//! Flags the Idris2 trust/escape primitives `believe_me`, `assert_total`, |
| 12 | +//! `assert_smaller`, `idris_crash`, and the `%default partial` directive. |
| 13 | +//! Idris2 `--check` exits 0 even when these are present, so without this rule |
| 14 | +//! they would silently ride along in an otherwise-green verdict — exactly the |
| 15 | +//! silent-failure class arghda exists to surface. Totality holes (`?name`) |
| 16 | +//! and per-def `partial` modifiers are a documented follow-on. |
| 17 | +
|
| 18 | +use super::{LintContext, LintRule}; |
| 19 | +use crate::diagnostic::{Diagnostic, LintReport, Severity}; |
| 20 | +use anyhow::{Context, Result}; |
| 21 | +use std::fs; |
| 22 | +use std::path::Path; |
| 23 | + |
| 24 | +pub struct Idris2EscapeHatch; |
| 25 | + |
| 26 | +const ESCAPE_TOKENS: &[&str] = &[ |
| 27 | + "believe_me", |
| 28 | + "assert_total", |
| 29 | + "assert_smaller", |
| 30 | + "idris_crash", |
| 31 | +]; |
| 32 | + |
| 33 | +impl LintRule for Idris2EscapeHatch { |
| 34 | + fn name(&self) -> &'static str { |
| 35 | + // Shared with the Agda rule on purpose — the reasoning graph's |
| 36 | + // lint→verdict cap keys on this name. |
| 37 | + "escape-hatch" |
| 38 | + } |
| 39 | + |
| 40 | + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { |
| 41 | + let contents = |
| 42 | + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; |
| 43 | + for (i, line) in contents.lines().enumerate() { |
| 44 | + let trimmed = line.trim_start(); |
| 45 | + if trimmed.starts_with("--") { |
| 46 | + continue; // whole-line comment |
| 47 | + } |
| 48 | + // The `%default partial` directive turns off totality checking. |
| 49 | + if trimmed.starts_with("%default") && trimmed.contains("partial") { |
| 50 | + report.push(warn( |
| 51 | + self.name(), |
| 52 | + file, |
| 53 | + i + 1, |
| 54 | + "totality escape directive `%default partial`".to_string(), |
| 55 | + )); |
| 56 | + } |
| 57 | + // Trust/escape primitives, ignoring any trailing line comment. |
| 58 | + let code = line.split(" --").next().unwrap_or(line); |
| 59 | + for tok in ESCAPE_TOKENS { |
| 60 | + if has_token(code, tok) { |
| 61 | + report.push(warn( |
| 62 | + self.name(), |
| 63 | + file, |
| 64 | + i + 1, |
| 65 | + format!("escape primitive `{tok}`"), |
| 66 | + )); |
| 67 | + } |
| 68 | + } |
| 69 | + } |
| 70 | + Ok(()) |
| 71 | + } |
| 72 | +} |
| 73 | + |
| 74 | +fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic { |
| 75 | + Diagnostic { |
| 76 | + rule: rule.to_string(), |
| 77 | + severity: Severity::Warn, |
| 78 | + file: file.to_path_buf(), |
| 79 | + message, |
| 80 | + line: Some(line), |
| 81 | + } |
| 82 | +} |
| 83 | + |
| 84 | +/// `tok` appears in `s` as a delimited token (so `assert_totally` or |
| 85 | +/// `believe_me_helper` do not match). |
| 86 | +fn has_token(s: &str, tok: &str) -> bool { |
| 87 | + s.split(|c: char| c.is_whitespace() || "(){};,".contains(c)) |
| 88 | + .any(|w| w == tok) |
| 89 | +} |
| 90 | + |
| 91 | +#[cfg(test)] |
| 92 | +mod tests { |
| 93 | + use super::*; |
| 94 | + use crate::lint::run_lints; |
| 95 | + use std::path::PathBuf; |
| 96 | + |
| 97 | + fn lint_str(body: &str) -> LintReport { |
| 98 | + let tmp = tempfile::NamedTempFile::new().unwrap(); |
| 99 | + std::fs::write(tmp.path(), body).unwrap(); |
| 100 | + let roots: [PathBuf; 0] = []; |
| 101 | + let ctx = LintContext { |
| 102 | + include_root: tmp.path().parent().unwrap(), |
| 103 | + entry_modules: &roots, |
| 104 | + }; |
| 105 | + let rules: Vec<Box<dyn LintRule>> = vec![Box::new(Idris2EscapeHatch)]; |
| 106 | + run_lints(tmp.path(), &ctx, &rules).unwrap() |
| 107 | + } |
| 108 | + |
| 109 | + #[test] |
| 110 | + fn believe_me_is_warned_under_the_escape_hatch_name() { |
| 111 | + let r = lint_str("module M\n\nx : Nat\nx = believe_me 0\n"); |
| 112 | + assert_eq!(r.warns().count(), 1); |
| 113 | + assert_eq!(r.diagnostics[0].rule, "escape-hatch"); |
| 114 | + assert!(r.diagnostics[0].message.contains("believe_me")); |
| 115 | + } |
| 116 | + |
| 117 | + #[test] |
| 118 | + fn assert_total_and_default_partial_are_warned() { |
| 119 | + let r = lint_str("%default partial\n\nf : Nat -> Nat\nf x = assert_total (f x)\n"); |
| 120 | + assert_eq!(r.warns().count(), 2); |
| 121 | + } |
| 122 | + |
| 123 | + #[test] |
| 124 | + fn escape_token_in_comment_is_ignored() { |
| 125 | + let r = lint_str("module M\n\nx : Nat\nx = 0 -- avoid believe_me here\n"); |
| 126 | + assert!(r.diagnostics.is_empty()); |
| 127 | + } |
| 128 | + |
| 129 | + #[test] |
| 130 | + fn longer_identifier_does_not_match() { |
| 131 | + let r = lint_str("module M\n\nbelieve_me_helper : Nat\nbelieve_me_helper = 0\n"); |
| 132 | + assert!(r.diagnostics.is_empty()); |
| 133 | + } |
| 134 | + |
| 135 | + #[test] |
| 136 | + fn clean_idris_file_is_silent() { |
| 137 | + let r = lint_str("module M\n\ngreeting : String\ngreeting = \"hi\"\n"); |
| 138 | + assert!(r.diagnostics.is_empty()); |
| 139 | + } |
| 140 | +} |
0 commit comments