Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
36 changes: 36 additions & 0 deletions crates/ruff_charon/build.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
//! Records the commit of the Charon checkout this crate is built against
//! (the path dependency `../../../charon/charon`), so `rows.bin` provenance can
//! name it. Any failure yields an empty value, which the store reads as UNKNOWN;
//! this script never fails the build.

use std::path::PathBuf;
use std::process::Command;

#[expect(
clippy::disallowed_methods,
reason = "a build script reads the real filesystem; the ty System abstraction does not apply"
)]
fn main() {
println!("cargo:rerun-if-changed=build.rs");
let manifest = std::env::var_os("CARGO_MANIFEST_DIR").map(PathBuf::from);
let repo = manifest.map(|m| m.join("../../../charon"));
let mut commit = String::new();
if let Some(repo) = repo {
for rel in [".git/HEAD", ".git/refs/heads"] {
let p = repo.join(rel);
if p.exists() {
println!("cargo:rerun-if-changed={}", p.display());
}
}
if let Ok(out) = Command::new("git")
.arg("-C")
.arg(&repo)
.args(["rev-parse", "HEAD"])
.output()
&& out.status.success()
{
commit = String::from_utf8_lossy(&out.stdout).trim().to_owned();
}
}
println!("cargo:rustc-env=RUFF_CHARON_CHARON_COMMIT={commit}");
}
25 changes: 25 additions & 0 deletions crates/ruff_charon/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,13 @@
//! is inferred from names.

pub mod store;
pub mod store_bin;

use std::fmt::Write as _;
use std::path::Path;

use anyhow::Context as _;

use charon_lib::ast::llbc_ast::{Statement, StatementKind};
use charon_lib::ast::visitor::AstVisitable;
use charon_lib::ast::*;
Expand All @@ -47,14 +50,27 @@ pub struct Llbc {
/// Charon reported errors: the crate description is partial.
pub has_errors: bool,
pub krate: TranslatedCrate,
/// The version of Charon that wrote the file (`CrateData::charon_version`).
pub charon_version: String,
/// [`store_bin::digest`] over the bytes of the LLBC file.
pub llbc_digest: u64,
}

/// Read an LLBC file written by `charon ... --dest-file`.
pub fn load(path: &Path) -> anyhow::Result<Llbc> {
// Charon offers no deserialize-from-bytes API (only `deserialize_from_file`,
// which also needs `serde_stacker` for deep ASTs), so the file is read twice:
// once for the digest, once by Charon.
let bytes = std::fs::read(path)
.with_context(|| format!("Failed to read llbc file {}", path.display()))?;
let llbc_digest = store_bin::digest(&bytes);
drop(bytes);
let data = CrateData::deserialize_from_file(path, SerializationFormat::Json)?;
Ok(Llbc {
has_errors: data.has_errors,
krate: data.translated,
charon_version: data.charon_version.0,
llbc_digest,
})
}

Expand Down Expand Up @@ -359,6 +375,10 @@ pub struct Relation {
/// What a Kythe `ref/call` points at when it is not `object`: the plain
/// trait name for `MAY_DISPATCH`, which Kythe reads as the declaration.
pub kythe_target: Option<String>,
/// The Charon `FunDeclId` of the function the row was harvested from. It
/// indexes the `fun_decls` of ONE LLBC file, so it is never an identity on
/// its own: identity is `(artifact, FunDeclId)`.
pub fun: Option<FunDeclId>,
}

/// Something Charon gave that no relation represents, with the reason.
Expand Down Expand Up @@ -400,6 +420,7 @@ pub fn relations(
object: f.qualified.clone(),
site: f.site.clone(),
kythe_target: None,
fun: Some(f.id),
});
let decl = krate.fun_decls.get(f.id);
let mut marker = |predicate: &'static str, object: String| {
Expand All @@ -410,6 +431,7 @@ pub fn relations(
object,
site: f.site.clone(),
kythe_target: None,
fun: Some(f.id),
});
};
if let Some(d) = decl {
Expand Down Expand Up @@ -449,6 +471,7 @@ pub fn relations(
object,
site: f.site.clone(),
kythe_target: None,
fun: Some(f.id),
}),
None => residual.push(Residual {
reason: "TRAIT_METHOD_NOT_FOUND",
Expand Down Expand Up @@ -529,6 +552,7 @@ pub fn relations(
object,
site: c.site,
kythe_target,
fun: Some(f.id),
});
}
for r in f.refs {
Expand All @@ -547,6 +571,7 @@ pub fn relations(
object,
site: r.site,
kythe_target: None,
fun: Some(f.id),
}),
None => residual.push(Residual {
reason: "REFERENCE_NOT_NAMED",
Expand Down
181 changes: 177 additions & 4 deletions crates/ruff_charon/src/store.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ use std::io::{self, BufRead, BufReader, Write};
use std::path::{Path, PathBuf};
use std::sync::atomic::{AtomicU64, Ordering};

use crate::store_bin::{self, BinRow, Prov};
use crate::{GRADE, Llbc, relations};

/// The version of the rows artifact this crate writes and reads.
Expand Down Expand Up @@ -147,16 +148,53 @@ fn read_table(
Ok(rows)
}

/// Provenance the store cannot know. The caller supplies it, or it is recorded
/// as UNKNOWN (`None`); it is never guessed.
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct SourceProv {
/// The commit of the rustc that Charon ran on.
pub rustc_commit: Option<String>,
/// The revision of the analysed source tree.
pub source_revision: Option<String>,
}

/// A directory of per-crate artifacts.
#[derive(Debug, Clone)]
pub struct Store {
dir: PathBuf,
tsv_export: bool,
}

fn invalid(m: impl ToString) -> io::Error {
io::Error::new(io::ErrorKind::InvalidData, m.to_string())
}

/// The Charon commit this crate was built against (`build.rs`); empty or
/// absent is UNKNOWN.
fn built_charon_commit() -> Option<String> {
option_env!("RUFF_CHARON_CHARON_COMMIT")
.filter(|c| !c.is_empty())
.map(str::to_owned)
}

impl Store {
/// A store that writes `rows.bin` and, for now, `rows.tsv` as well.
#[must_use]
pub fn new(dir: impl Into<PathBuf>) -> Self {
Self { dir: dir.into() }
Self {
dir: dir.into(),
tsv_export: true,
}
}

/// Whether `import` also writes `<crate>.rows.tsv`. On by default in this
/// release (transitional): the lance-graph codegraph reader still reads
/// `rows.tsv` until its binary reader lands, at which point the default
/// flips to off. `rows.bin` is always written.
#[must_use]
pub fn with_tsv_export(mut self, on: bool) -> Self {
self.tsv_export = on;
self
}

fn path(&self, crate_name: &str, suffix: &str) -> PathBuf {
Expand Down Expand Up @@ -213,8 +251,43 @@ impl Store {
///
/// # Errors
/// I/O errors, or `InvalidData` when the receipt does not conserve.
#[expect(clippy::disallowed_methods, reason = "see `replace`")]
pub fn import(&self, llbc: &Llbc, crate_name: &str) -> io::Result<crate::Receipt> {
self.import_with(llbc, crate_name, &SourceProv::default())
}

/// [`Store::import`] with the provenance only the caller knows.
///
/// # Errors
/// I/O errors, or `InvalidData` when the receipt does not conserve or the
/// rows cannot be encoded.
pub fn import_with(
&self,
llbc: &Llbc,
crate_name: &str,
src: &SourceProv,
) -> io::Result<crate::Receipt> {
self.import_inner(llbc, crate_name, src, built_charon_commit())
}

/// [`Store::import`] with a fixed provenance (no Charon commit, no rustc
/// commit, no source revision), so the bytes written do not depend on the
/// machine that built this crate. Only for the golden-file test.
///
/// # Errors
/// As [`Store::import`].
#[doc(hidden)]
pub fn import_for_golden(&self, llbc: &Llbc, crate_name: &str) -> io::Result<crate::Receipt> {
self.import_inner(llbc, crate_name, &SourceProv::default(), None)
}

#[expect(clippy::disallowed_methods, reason = "see `replace`")]
fn import_inner(
&self,
llbc: &Llbc,
crate_name: &str,
src: &SourceProv,
charon_commit: Option<String>,
) -> io::Result<crate::Receipt> {
let (rows, residual, receipt) = relations(&llbc.krate, crate_name);
if !receipt.conserved() {
return Err(io::Error::new(
Expand Down Expand Up @@ -246,6 +319,36 @@ impl Store {
"COMPLETE"
};
writeln!(out, "CRATE\t{crate_name}\t{completeness}\t{GRADE}\t-\t-\t-")?;
// The same rows, in the same order, for the binary file.
let mut bin_rows = Vec::with_capacity(rows.len() + 1);
for r in &rows {
let fun = r
.fun
.map(|id| u32::try_from(id.index()).map_err(invalid))
.transpose()?;
bin_rows.push(BinRow {
predicate: r.predicate.to_owned(),
subject: r.subject.clone(),
object: r.object.clone(),
grade: GRADE.to_owned(),
site: r.site.as_ref().map(|s| (s.file.clone(), s.start, s.end)),
fun,
});
}
bin_rows.push(BinRow {
predicate: "CRATE".to_owned(),
subject: crate_name.to_owned(),
object: completeness.to_owned(),
grade: GRADE.to_owned(),
site: None,
fun: None,
});
let bin = store_bin::write(
&bin_rows,
llbc.has_errors,
&[Self::prov(llbc, src, charon_commit)],
)
.map_err(invalid)?;
let mut res = Vec::new();
header(&mut res, RESIDUALS_VERSION, RESIDUALS_SCHEMA)?;
for r in &residual {
Expand All @@ -257,12 +360,55 @@ impl Store {
writeln!(files, "{p}\t{d:016x}")?;
}
// Files last: a crate whose digests are present has its rows.
Self::replace(&self.path(crate_name, "rows.tsv"), &out)?;
Self::replace(&self.path(crate_name, "rows.bin"), &bin)?;
if self.tsv_export {
Self::replace(&self.path(crate_name, "rows.tsv"), &out)?;
}
Comment thread
AdaWorldAPI marked this conversation as resolved.
Resolved
Self::replace(&self.path(crate_name, "residuals.tsv"), &res)?;
Self::replace(&self.path(crate_name, "files.tsv"), &files)?;
Ok(receipt)
}

/// The provenance record of one import. `llbc_schema_version` repeats the
/// Charon version: no separate schema version exists today. `target_config`
/// is the sorted target triples, then `;`, then the Charon options as JSON
/// (serde's fixed field order).
fn prov(llbc: &Llbc, src: &SourceProv, charon_commit: Option<String>) -> Prov {
let mut triples: Vec<&str> = llbc
.krate
.target_information
.keys()
.map(String::as_str)
.collect();
triples.sort_unstable();
let target_config = serde_json::to_string(&llbc.krate.options)
.ok()
.map(|opts| format!("{};{opts}", triples.join(",")));
Prov {
charon_version: Some(llbc.charon_version.clone()),
charon_commit,
llbc_schema_version: Some(llbc.charon_version.clone()),
llbc_digest: Some(format!("{:016x}", llbc.llbc_digest)),
rustc_commit: src.rustc_commit.clone(),
target_config,
source_revision: src.source_revision.clone(),
}
}

fn decode_bin(&self, crate_name: &str) -> io::Result<store_bin::Decoded> {
let path = self.path(crate_name, "rows.bin");
let bytes = fs::read(&path)?;
store_bin::read(&bytes).map_err(|e| invalid(format!("{}: {e}", path.display())))
}

/// The provenance records of one crate's `rows.bin`.
///
/// # Errors
/// I/O or format errors.
pub fn provenance(&self, crate_name: &str) -> io::Result<Vec<Prov>> {
Ok(self.decode_bin(crate_name)?.prov)
}

/// The crates in the store, sorted.
///
/// # Errors
Expand All @@ -282,11 +428,38 @@ impl Store {
Ok(out)
}

/// One crate's rows, read by schema names.
/// One crate's rows, read from `rows.bin`, or from `rows.tsv` when the
/// crate was stored before the binary format existed.
///
/// # Errors
/// I/O or format errors.
#[expect(clippy::disallowed_methods, reason = "see `replace`")]
pub fn rows(&self, crate_name: &str) -> io::Result<Vec<Row>> {
// A store written before the binary format has only `rows.tsv`; it
// stays readable until its crate is imported again.
if !self.path(crate_name, "rows.bin").exists() {
return self.rows_tsv(crate_name);
}
Ok(self
.decode_bin(crate_name)?
.rows
.into_iter()
.map(|r| Row {
predicate: r.predicate,
subject: r.subject,
object: r.object,
grade: r.grade,
site: r.site,
})
.collect())
}

/// One crate's rows, read from `rows.tsv` by schema names (debug and test
/// path; the file exists only while the TSV export is on).
///
/// # Errors
/// I/O or format errors.
pub fn rows_tsv(&self, crate_name: &str) -> io::Result<Vec<Row>> {
let table = read_table(
&self.path(crate_name, "rows.tsv"),
ROWS_VERSION,
Expand Down
Loading
Loading