ruff_charon: no '?' dispatch targets; record witnessed effects with exact assert kind

crates/ruff_charon/src/lib.rs

@@ -99,6 +99,20 @@ pub fn path_name(name: &Name) -> String {
         .join("::")
 }
 
+/// The object of a `MAY_DISPATCH` row (`Trait::method via kind`) and its
+/// Kythe target (the trait). `None` when the trait or the method has no
+/// name: a placeholder would be one symbol shared by every unresolved
+/// target, so the caller records the call as a `CALLEE_NOT_NAMED` residual
+/// instead of guessing an identity.
+fn may_dispatch_object(
+    trait_name: Option<String>,
+    method_name: Option<String>,
+    kind: &str,
+) -> Option<(String, String)> {
+    let (tr, name) = (trait_name?, method_name?);
+    Some((format!("{tr}::{name} via {kind}"), tr))
+}
+
 /// Charon's own rendering of a name, which spells impl blocks out
 /// (`{impl Shape for Square}`), so distinct items print distinctly.
 pub fn qualified_name(krate: &TranslatedCrate, name: &Name) -> String {
@@ -167,6 +181,57 @@ pub struct FunFacts {
     pub deref_write_local: usize,
     /// `Assert` statements: overflow, division and bounds checks that can panic.
     pub asserts: usize,
+    /// Every effect the body witnesses, one per occurrence, in body order.
+    /// An observation list: a function with none is NOT proven pure.
+    pub effects: Vec<Effect>,
+}
+
+/// One effect a function body witnesses, at its site.
+///
+/// Only what the LLBC shows is recorded. The absence of an effect is never a
+/// purity verdict: Charon's own passes may fold checks into fallible
+/// operations, callees' effects are not included, and an unstructured body
+/// records nothing.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Effect {
+    pub kind: EffectKind,
+    pub site: Option<Site>,
+}
+
+/// The kind of a witnessed effect.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum EffectKind {
+    /// An `Assert` that can panic. The text is Charon's `BuiltinAssertKind`
+    /// tag (`BoundsCheck`, `DivisionByZero`, ...), `Overflow:<BinOp>` for an
+    /// overflow check (`Overflow:Mul`), and `User` for a source `assert!`.
+    Assert(String),
+    /// A write through a dereference rooted in an argument.
+    DerefWriteArg,
+    /// A write through a dereference rooted in a local.
+    DerefWriteLocal,
+}
+
+impl EffectKind {
+    /// The `effect` and `kind` columns of `<crate>.effects.tsv`.
+    pub fn columns(&self) -> (&'static str, &str) {
+        match self {
+            EffectKind::Assert(k) => ("ASSERT", k),
+            EffectKind::DerefWriteArg => ("DEREF_WRITE", "Arg"),
+            EffectKind::DerefWriteLocal => ("DEREF_WRITE", "Local"),
+        }
+    }
+}
+
+/// The exact kind of an assert: Charon's tag, with the operator for an
+/// overflow check; `User` when Charon records no built-in kind.
+fn assert_kind(assert: &Assert) -> String {
+    match &assert.check_kind {
+        None => "User".to_owned(),
+        Some(BuiltinAssertKind::Overflow(op, ..)) => {
+            format!("Overflow:{}", variant(format!("{op:?}")))
+        }
+        Some(k) => variant(format!("{k:?}")),
+    }
 }
 
 fn file_name(krate: &TranslatedCrate, id: FileId) -> String {
@@ -277,6 +342,7 @@ pub fn fun_facts(krate: &TranslatedCrate, crate_name: &str) -> Vec<FunFacts> {
             deref_write_arg: 0,
             deref_write_local: 0,
             asserts: 0,
+            effects: Vec::new(),
         };
         if let Body::Structured(body) = &f.body {
             let args = body.locals.arg_count;
@@ -305,12 +371,28 @@ pub fn fun_facts(krate: &TranslatedCrate, crate_name: &str) -> Vec<FunFacts> {
                         callee: callee(krate, call),
                         site: site(krate, st.span),
                     }),
-                    StatementKind::Assert { .. } => facts.asserts += 1,
+                    StatementKind::Assert { assert, .. } => {
+                        facts.asserts += 1;
+                        facts.effects.push(Effect {
+                            kind: EffectKind::Assert(assert_kind(assert)),
+                            site: site(krate, st.span),
+                        });
+                    }
                     StatementKind::Assign(place, _) if has_deref(place) => {
-                        match root_local(place) {
-                            Some(l) if l.index() <= args => facts.deref_write_arg += 1,
-                            _ => facts.deref_write_local += 1,
-                        }
+                        let kind = match root_local(place) {
+                            Some(l) if l.index() <= args => {
+                                facts.deref_write_arg += 1;
+                                EffectKind::DerefWriteArg
+                            }
+                            _ => {
+                                facts.deref_write_local += 1;
+                                EffectKind::DerefWriteLocal
+                            }
+                        };
+                        facts.effects.push(Effect {
+                            kind,
+                            site: site(krate, st.span),
+                        });
                     }
                     _ => {}
                 }
@@ -534,14 +616,20 @@ pub fn relations(
                     } else {
                         let tr = trait_id
                             .and_then(|t| krate.item_names.get(&ItemId::TraitDecl(t)))
-                            .map(|n| qualified_name(krate, n))
-                            .unwrap_or_else(|| "?".to_owned());
+                            .map(|n| qualified_name(krate, n));
                         let name = trait_id
                             .and_then(|t| krate.trait_decls.get(t))
                             .and_then(|t| t.methods.get(*method))
-                            .map_or_else(|| "?".to_owned(), |m| m.skip_binder.name.to_string());
-                        kythe_target = Some(tr.clone());
-                        ("MAY_DISPATCH", format!("{tr}::{name} via {kind}"))
+                            .map(|m| m.skip_binder.name.to_string());
+                        let Some((object, target)) = may_dispatch_object(tr, name, kind) else {
+                            residual.push(Residual {
+                                reason: "CALLEE_NOT_NAMED",
+                                subject: f.qualified.clone(),
+                            });
+                            continue;
+                        };
+                        kythe_target = Some(target);
+                        ("MAY_DISPATCH", object)
                     }
                 }
                 Callee::Dynamic => ("UNRESOLVED_CALL", "dynamic".to_owned()),
@@ -723,6 +811,27 @@ mod tests {
         assert_eq!(b64(b"function"), "ZnVuY3Rpb24=");
     }
 
+    /// Fails if a dispatch whose trait or method has no name gets a target:
+    /// a `?` placeholder is shared by every unresolved target, so two
+    /// distinct calls would merge onto one symbol.
+    #[test]
+    fn an_unnamed_dispatch_target_is_not_emitted() {
+        let n = |s: &str| Some(s.to_owned());
+        assert_eq!(may_dispatch_object(None, n("m"), "Clause"), None);
+        assert_eq!(may_dispatch_object(n("a::T"), None, "Dyn"), None);
+        assert_eq!(may_dispatch_object(None, None, "Clause"), None);
+    }
+
+    /// The silence twin: a fully named dispatch keeps its object and target.
+    #[test]
+    fn a_named_dispatch_target_is_emitted() {
+        let n = |s: &str| Some(s.to_owned());
+        assert_eq!(
+            may_dispatch_object(n("a::T"), n("m"), "Clause"),
+            Some(("a::T::m via Clause".to_owned(), "a::T".to_owned()))
+        );
+    }
+
     #[test]
     fn receipt_conservation_is_exact() {
         let ok = Receipt {

crates/ruff_charon/src/store.rs

@@ -42,6 +42,8 @@ const ROWS_SCHEMA: &[&str] = &[
 const FILES_VERSION: u32 = 1;
 const FILES_SCHEMA: &[&str] = &["path", "fnv64"];
 const RESIDUALS_VERSION: u32 = 1;
+const EFFECTS_VERSION: u32 = 1;
+const EFFECTS_SCHEMA: &[&str] = &["subject", "effect", "kind", "file", "start", "end"];
 const RESIDUALS_SCHEMA: &[&str] = &["reason", "subject"];
 
 /// One stored relation row.
@@ -354,6 +356,26 @@ impl Store {
         for r in &residual {
             writeln!(res, "{}\t{}", r.reason, r.subject)?;
         }
+        // Witnessed effects, one row per occurrence. An observation list only:
+        // a function with no row is not proven pure.
+        let mut effects = Vec::new();
+        header(&mut effects, EFFECTS_VERSION, EFFECTS_SCHEMA)?;
+        for f in crate::fun_facts(&llbc.krate, crate_name) {
+            for fx in &f.effects {
+                let (effect, kind) = fx.kind.columns();
+                let (file, start, end) = fx
+                    .site
+                    .as_ref()
+                    .map_or(("-".to_owned(), "-".to_owned(), "-".to_owned()), |s| {
+                        (s.file.clone(), s.start.to_string(), s.end.to_string())
+                    });
+                writeln!(
+                    effects,
+                    "{}\t{effect}\t{kind}\t{file}\t{start}\t{end}",
+                    f.qualified
+                )?;
+            }
+        }
         let mut files = Vec::new();
         header(&mut files, FILES_VERSION, FILES_SCHEMA)?;
         for (p, d) in crate_files(llbc, crate_name) {
@@ -372,6 +394,7 @@ impl Store {
             }
         }
         Self::replace(&self.path(crate_name, "residuals.tsv"), &res)?;
+        Self::replace(&self.path(crate_name, "effects.tsv"), &effects)?;
         Self::replace(&self.path(crate_name, "files.tsv"), &files)?;
         Ok(receipt)
     }

crates/ruff_charon/tests/data/README.md

@@ -13,5 +13,6 @@ cd cg_app && charon cargo --no-dedup-serialized-ast --dest-file cg_app.llbc
 ```
 
 - `fnref.llbc`: Charon LLBC of `fnref.rs` (a function used only as a function pointer, an unused private function, and a call through a pointer argument), produced with `charon rustc --no-dedup-serialized-ast --dest-file fnref.llbc -- --crate-type=lib fnref.rs`. rustc reports `dead_code` for `unused_private` only.
+- `derefw.llbc`: Charon LLBC of `derefw.rs` (writes through argument-rooted and local-rooted dereferences, and a function that assigns only locals), produced the same way as `fnref.llbc`: `charon rustc --no-dedup-serialized-ast --dest-file derefw.llbc -- --crate-type=lib derefw.rs`.
 - `cg_lib.kythe.golden`, `cg_app.kythe.golden`: `ruff_charon kythe <file> <crate>` on rows v1 (before the v2 predicates); the v2 Kythe output must equal them.
 - `cg_broken` (rev1) produces no LLBC: rustc stops on E0425 and E0432 before Charon translates, so a `CRATE … PARTIAL` row cannot come from a crate that does not compile.

crates/ruff_charon/tests/data/derefw.rs

@@ -0,0 +1,24 @@
+//! Writes through dereferenced places, for `tests/effects.rs`.
+//! `through_arg` writes twice through argument-rooted derefs, `through_local`
+//! writes once through a local reference, and `plain` assigns only to locals.
+
+pub struct S {
+    pub f: i32,
+}
+
+pub fn through_arg(p: &mut i32, s: &mut S) {
+    *p = 1;
+    s.f = 2;
+}
+
+pub fn through_local(v: i32) -> i32 {
+    let mut x = v;
+    let r = &mut x;
+    *r = 3;
+    x
+}
+
+pub fn plain(a: i32) -> i32 {
+    let y = a;
+    y
+}

crates/ruff_charon/tests/effects.rs

@@ -0,0 +1,143 @@
+//! Witnessed effects: `<crate>.effects.tsv` records each effect the compiler's
+//! LLBC shows in a function body (a built-in or user assert, with its exact
+//! kind; a write through a dereferenced place). It is a list of observations
+//! only: a function with no row is NOT proven pure (asserts removed by
+//! Charon's own passes, callees' effects and unharvested bodies are not
+//! here), so nothing may read the absence of a row as purity.
+#![expect(
+    clippy::disallowed_methods,
+    reason = "tests write and read their own temp files; there is no ty System here"
+)]
+
+use std::path::PathBuf;
+
+use ruff_charon::load;
+use ruff_charon::store::Store;
+
+fn data(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("tests/data")
+        .join(name)
+}
+
+fn import(name: &str) -> (PathBuf, String) {
+    import_crate(name, "cg_lib")
+}
+
+fn import_crate(name: &str, krate: &str) -> (PathBuf, String) {
+    let dir = std::env::temp_dir().join(format!("ruff_charon_fx_{name}_{}", std::process::id()));
+    let _ = std::fs::remove_dir_all(&dir);
+    let llbc = load(&data(&format!("{krate}.llbc"))).expect("llbc");
+    Store::new(&dir).import(&llbc, krate).expect("import");
+    let text =
+        std::fs::read_to_string(dir.join(format!("{krate}.effects.tsv"))).expect("effects file");
+    (dir, text)
+}
+
+/// `(effect, kind)` of every row of `subject`, in file order.
+fn effects_of<'a>(text: &'a str, subject: &str) -> Vec<(&'a str, &'a str)> {
+    text.lines()
+        .filter(|l| !l.starts_with('#'))
+        .filter_map(|l| {
+            let f: Vec<&str> = l.split('\t').collect();
+            (f[0] == subject).then(|| (f[1], f[2]))
+        })
+        .collect()
+}
+
+/// Fails if the file is missing or its header changes without a version bump.
+#[test]
+fn the_effects_file_has_a_versioned_header() {
+    let (dir, text) = import("header");
+    let mut lines = text.lines();
+    assert_eq!(lines.next(), Some("#version 1"));
+    assert_eq!(
+        lines.next(),
+        Some("#schema subject\teffect\tkind\tfile\tstart\tend")
+    );
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// The N7 witness pair. Today the relation rows of `double` (`x * 2`) and
+/// `unit` are indistinguishable although Charon saw an overflow check in
+/// `double`. The check must be recorded with its exact kind.
+#[test]
+fn a_witnessed_overflow_check_is_recorded_with_its_kind() {
+    let (dir, text) = import("witness");
+    assert_eq!(
+        effects_of(&text, "cg_lib::util::double"),
+        [("ASSERT", "Overflow:Mul")]
+    );
+    assert_eq!(
+        effects_of(&text, "cg_lib::util::triple"),
+        [("ASSERT", "Overflow:Mul")]
+    );
+    // `double(self.0) / 2 * self.0`: two different kinds, in body order.
+    assert_eq!(
+        effects_of(&text, "cg_lib::shapes::impl_Shape_for_Square::area"),
+        [("ASSERT", "DivisionByZero"), ("ASSERT", "Overflow:Mul")]
+    );
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// The silence twin: a function with no witnessed effect has no row. This is
+/// the absence of an observation, never a purity verdict.
+#[test]
+fn a_function_without_a_witnessed_effect_has_no_row() {
+    let (dir, text) = import("silent");
+    assert!(effects_of(&text, "cg_lib::util::unit").is_empty());
+    assert!(effects_of(&text, "cg_lib::util::private_unused").is_empty());
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// Fails if repeated effects of one kind are collapsed: one row per
+/// occurrence, so a count survives. `cg_app::run` has three additions, each
+/// with its own overflow check; a kind-level dedup would leave one.
+#[test]
+fn every_occurrence_is_its_own_row() {
+    let (dir, text) = import_crate("multi", "cg_app");
+    assert_eq!(
+        effects_of(&text, "cg_app::run"),
+        [("ASSERT", "Overflow:Add"); 3]
+    );
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// Fails if the effect rows disagree with the independent reference output
+/// (`cg_lib.llbc_calls.txt`, written by another tool), which counts the
+/// asserts per function.
+#[test]
+fn the_assert_count_matches_the_reference() {
+    let (dir, text) = import("reference");
+    let total_asserts = text
+        .lines()
+        .filter(|l| !l.starts_with('#'))
+        .filter(|l| l.split('\t').nth(1) == Some("ASSERT"))
+        .count();
+    let reference: usize = std::fs::read_to_string(data("cg_lib.llbc_calls.txt"))
+        .expect("reference")
+        .lines()
+        .filter_map(|l| l.rsplit("assert=").next()?.parse::<usize>().ok())
+        .sum();
+    assert_eq!(total_asserts, reference);
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// Fails if writes through a dereferenced place are dropped or their root is
+/// misclassified: `through_arg` writes twice through argument-rooted derefs
+/// (`*p` and `s.f`, which is `(*s).f`), `through_local` once through a local
+/// reference, and `plain` only assigns locals, so it has no row (the twin).
+#[test]
+fn deref_writes_are_classified_by_their_root() {
+    let (dir, text) = import_crate("deref", "derefw");
+    assert_eq!(
+        effects_of(&text, "derefw::through_arg"),
+        vec![("DEREF_WRITE", "Arg"), ("DEREF_WRITE", "Arg")]
+    );
+    assert_eq!(
+        effects_of(&text, "derefw::through_local"),
+        vec![("DEREF_WRITE", "Local")]
+    );
+    assert!(effects_of(&text, "derefw::plain").is_empty(), "{text}");
+    let _ = std::fs::remove_dir_all(&dir);
+}