use std::path::{Path, PathBuf};
use regex::Regex;
use walkdir::WalkDir;
use super::types::*;
#[derive(Debug, Clone)]
struct AttributeUsage {
file: PathBuf,
id: String,
requires: Vec<String>,
ensures: Vec<String>,
}
fn attribute_parser() -> (Regex, Regex, Regex, Regex) {
let attr = Regex::new(r"(?m)^[ \t]*#\[pmat_work_contract\(([^)]*)\)\]")
.expect("static regex must compile");
let id = Regex::new(r#"id\s*=\s*"([^"]+)""#).expect("static regex must compile");
let requires = Regex::new(r#"require\s*=\s*"([^"]+)""#).expect("static regex must compile");
let ensures = Regex::new(r#"ensure\s*=\s*"([^"]+)""#).expect("static regex must compile");
(attr, id, requires, ensures)
}
fn is_self_reference(path: &Path) -> bool {
let s = path.to_string_lossy();
s.contains("check_codegen.rs")
}
fn collect_attribute_usages(project_path: &Path) -> Vec<AttributeUsage> {
let src = project_path.join("src");
if !src.exists() {
return Vec::new();
}
let (attr, id_rx, req_rx, ens_rx) = attribute_parser();
let mut out = Vec::new();
for entry in WalkDir::new(&src)
.into_iter()
.filter_map(|e| e.ok())
.filter(|e| e.path().extension().and_then(|s| s.to_str()) == Some("rs"))
.filter(|e| !is_self_reference(e.path()))
{
let Ok(text) = std::fs::read_to_string(entry.path()) else {
continue;
};
for cap in attr.captures_iter(&text) {
let body = cap.get(1).map(|m| m.as_str()).unwrap_or("");
let Some(id) = id_rx.captures(body).and_then(|c| c.get(1)) else {
continue;
};
let requires: Vec<String> = req_rx
.captures_iter(body)
.filter_map(|c| c.get(1))
.map(|m| m.as_str().to_string())
.collect();
let ensures: Vec<String> = ens_rx
.captures_iter(body)
.filter_map(|c| c.get(1))
.map(|m| m.as_str().to_string())
.collect();
out.push(AttributeUsage {
file: entry.path().to_path_buf(),
id: id.as_str().to_string(),
requires,
ensures,
});
}
}
out
}
fn load_contract_json(project_path: &Path, ticket_id: &str) -> Option<serde_json::Value> {
let path = project_path
.join(".pmat-work")
.join(ticket_id)
.join("contract.json");
let text = std::fs::read_to_string(&path).ok()?;
serde_json::from_str::<serde_json::Value>(&text).ok()
}
fn iter_clauses(contract: &serde_json::Value) -> impl Iterator<Item = &serde_json::Value> {
["require", "ensure", "invariant"]
.into_iter()
.filter_map(|s| contract.get(s).and_then(|v| v.as_array()))
.flatten()
}
fn contract_level_at_least(contract: &serde_json::Value, target: u8) -> bool {
let Some(s) = contract.get("verification_level").and_then(|v| v.as_str()) else {
return false;
};
let token = s.split_whitespace().next().unwrap_or("");
let trimmed = token.trim();
let after_l = trimmed
.strip_prefix(|c: char| c == 'L' || c == 'l')
.unwrap_or(trimmed);
let digits: String = after_l.chars().take_while(|c| c.is_ascii_digit()).collect();
digits.parse::<u8>().map(|n| n >= target).unwrap_or(false)
}
enum ReceiptOutcome {
Pass,
Fail(String),
}
fn sha256_hex(bytes: &[u8]) -> String {
use sha2::{Digest, Sha256};
let mut h = Sha256::new();
h.update(bytes);
let d = h.finalize();
let mut s = String::with_capacity(d.len() * 2);
for b in d {
use std::fmt::Write;
let _ = write!(&mut s, "{:02x}", b);
}
s
}
fn resolve_binds_to_candidates(path: &str) -> Vec<String> {
let without_crate = path.strip_prefix("crate::").unwrap_or(path);
let mut parts: Vec<&str> = without_crate.split("::").collect();
if parts.len() > 1 {
parts.pop();
}
let mut out = Vec::new();
while !parts.is_empty() {
let joined = parts.join("/");
out.push(format!("src/{}.rs", joined));
out.push(format!("src/{}/mod.rs", joined));
parts.pop();
}
out.push("src/lib.rs".into());
out.push("src/main.rs".into());
out
}
fn load_modified_files(project_path: &Path, ticket_id: &str) -> Option<Vec<String>> {
let p = project_path
.join(".pmat-work")
.join(ticket_id)
.join("modified-files.json");
let text = std::fs::read_to_string(&p).ok()?;
let v: serde_json::Value = serde_json::from_str(&text).ok()?;
if let Some(arr) = v.as_array() {
return Some(
arr.iter()
.filter_map(|x| x.as_str().map(str::to_string))
.collect(),
);
}
for key in ["files", "modified"] {
if let Some(arr) = v.get(key).and_then(|x| x.as_array()) {
return Some(
arr.iter()
.filter_map(|x| x.as_str().map(str::to_string))
.collect(),
);
}
}
None
}
include!("check_codegen_attribute.rs");
include!("check_codegen_clauses.rs");
include!("check_codegen_receipts.rs");
include!("check_codegen_manifest_sha.rs");
include!("check_codegen_binds_modified.rs");
include!("check_codegen_compile_profiles.rs");
include!("check_codegen_pub_fn_coverage.rs");
include!("check_codegen_harness_refs.rs");
include!("check_codegen_tests_attribute.rs");
include!("check_codegen_tests_manifest.rs");
include!("check_codegen_tests_receipts.rs");
include!("check_codegen_tests_harness.rs");