From 4c9f9b60ac3b117bd0d61913475a399eb23a9fa5 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 19:56:47 +0000 Subject: [PATCH 1/6] ruff_charon: extract may_dispatch_object; register red test for unnamed dispatch targets Behaviour-preserving extraction (missing names still render as '?'), plus a test that fails on it: a dispatch whose trait or method has no name must get no target, since a shared '?' placeholder merges distinct calls. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/src/lib.rs | 50 +++++++++++++++++++++++++++++++---- 1 file changed, 45 insertions(+), 5 deletions(-) diff --git a/crates/ruff_charon/src/lib.rs b/crates/ruff_charon/src/lib.rs index aaebf8bb9b17a..f233494da6ab6 100644 --- a/crates/ruff_charon/src/lib.rs +++ b/crates/ruff_charon/src/lib.rs @@ -99,6 +99,19 @@ 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). Behaviour-preserving extraction: a missing +/// name still renders as the `?` placeholder. +fn may_dispatch_object( + trait_name: Option, + method_name: Option, + kind: &str, +) -> Option<(String, String)> { + let tr = trait_name.unwrap_or_else(|| "?".to_owned()); + let name = method_name.unwrap_or_else(|| "?".to_owned()); + 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 { @@ -534,14 +547,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 +742,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 { From 46ab97b95c45750213d6cefbfb4ef12f1460c236 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 19:57:02 +0000 Subject: [PATCH 2/6] ruff_charon: never emit a '?' placeholder as a MAY_DISPATCH target (B7 producer side) A dispatch whose trait or method has no name is recorded as a CALLEE_NOT_NAMED residual (the existing convention for an unnamed callee) instead of a MAY_DISPATCH row to '?::?'. One harvested call is still one row or one residual, so the receipt stays conserved. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/src/lib.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/crates/ruff_charon/src/lib.rs b/crates/ruff_charon/src/lib.rs index f233494da6ab6..5cd51131510ab 100644 --- a/crates/ruff_charon/src/lib.rs +++ b/crates/ruff_charon/src/lib.rs @@ -100,15 +100,16 @@ pub fn path_name(name: &Name) -> String { } /// The object of a `MAY_DISPATCH` row (`Trait::method via kind`) and its -/// Kythe target (the trait). Behaviour-preserving extraction: a missing -/// name still renders as the `?` placeholder. +/// 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, method_name: Option, kind: &str, ) -> Option<(String, String)> { - let tr = trait_name.unwrap_or_else(|| "?".to_owned()); - let name = method_name.unwrap_or_else(|| "?".to_owned()); + let (tr, name) = (trait_name?, method_name?); Some((format!("{tr}::{name} via {kind}"), tr)) } From 5e53b37719e679e782e92767b82ec7cc6adb8695 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 20:04:58 +0000 Subject: [PATCH 3/6] ruff_charon: register red witnessed-effects fixture (B1) The committed cg_lib LLBC has an overflow check in util::double (x * 2) that no output records; util::unit has none. Expect .effects.tsv with one row per witnessed effect and its exact kind. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/tests/effects.rs | 98 +++++++++++++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 crates/ruff_charon/tests/effects.rs diff --git a/crates/ruff_charon/tests/effects.rs b/crates/ruff_charon/tests/effects.rs new file mode 100644 index 0000000000000..05791d08cc80e --- /dev/null +++ b/crates/ruff_charon/tests/effects.rs @@ -0,0 +1,98 @@ +//! Witnessed effects: `.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. + +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) { + 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("cg_lib.llbc")).expect("llbc"); + Store::new(&dir).import(&llbc, "cg_lib").expect("import"); + let text = std::fs::read_to_string(dir.join("cg_lib.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")] + ); + 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 are collapsed: one row per occurrence, so a +/// count survives. +#[test] +fn every_occurrence_is_its_own_row() { + let (dir, text) = import("multi"); + let total_asserts = text + .lines() + .filter(|l| !l.starts_with('#')) + .filter(|l| l.split('\t').nth(1) == Some("ASSERT")) + .count(); + // The reference output (`cg_lib.llbc_calls.txt`, written by an + // independent tool) counts the asserts per function; the sum must match. + 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::().ok()) + .sum(); + assert_eq!(total_asserts, reference); + let _ = std::fs::remove_dir_all(&dir); +} From bcf1cabf01ee04130fae5077cc0375449f9e84c0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 20:06:23 +0000 Subject: [PATCH 4/6] ruff_charon: record witnessed effects with their exact kind (B1 producer side) Each import now writes .effects.tsv (version 1: subject, effect, kind, file, start, end), one row per occurrence: - ASSERT with Charon's BuiltinAssertKind tag (Overflow:, BoundsCheck, DivisionByZero, ...; User for a source assert!); - DEREF_WRITE Arg / Local. The counters printed by calls_text are unchanged. It is an observation list: a function with no row is not proven pure (Charon passes may fold checks into fallible operations, callees' effects and unstructured bodies are not recorded). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/src/lib.rs | 78 +++++++++++++++++++++++++++-- crates/ruff_charon/src/store.rs | 23 +++++++++ crates/ruff_charon/tests/effects.rs | 4 ++ 3 files changed, 100 insertions(+), 5 deletions(-) diff --git a/crates/ruff_charon/src/lib.rs b/crates/ruff_charon/src/lib.rs index 5cd51131510ab..42a22fc538fb5 100644 --- a/crates/ruff_charon/src/lib.rs +++ b/crates/ruff_charon/src/lib.rs @@ -181,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, +} + +/// 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, +} + +/// 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:` 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 `.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 { @@ -291,6 +342,7 @@ pub fn fun_facts(krate: &TranslatedCrate, crate_name: &str) -> Vec { 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; @@ -319,12 +371,28 @@ pub fn fun_facts(krate: &TranslatedCrate, crate_name: &str) -> Vec { 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), + }); } _ => {} } diff --git a/crates/ruff_charon/src/store.rs b/crates/ruff_charon/src/store.rs index 757c1ea1b2f92..938d49da3b326 100644 --- a/crates/ruff_charon/src/store.rs +++ b/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) } diff --git a/crates/ruff_charon/tests/effects.rs b/crates/ruff_charon/tests/effects.rs index 05791d08cc80e..bd8305ac69cd4 100644 --- a/crates/ruff_charon/tests/effects.rs +++ b/crates/ruff_charon/tests/effects.rs @@ -4,6 +4,10 @@ //! 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; From a36cdb9703823f8574a7754063a22f64944cf7b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 20:07:14 +0000 Subject: [PATCH 5/6] ruff_charon: effects test discriminates per-occurrence rows (cg_app::run: 3 x Overflow:Add) The first occurrence test could not fail when same-kind effects were collapsed (no cg_lib function repeats a kind). It now uses cg_app::run; the reference-count check is kept as its own test. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/tests/effects.rs | 38 +++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 8 deletions(-) diff --git a/crates/ruff_charon/tests/effects.rs b/crates/ruff_charon/tests/effects.rs index bd8305ac69cd4..82dbf08eda81b 100644 --- a/crates/ruff_charon/tests/effects.rs +++ b/crates/ruff_charon/tests/effects.rs @@ -21,11 +21,16 @@ fn data(name: &str) -> PathBuf { } 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("cg_lib.llbc")).expect("llbc"); - Store::new(&dir).import(&llbc, "cg_lib").expect("import"); - let text = std::fs::read_to_string(dir.join("cg_lib.effects.tsv")).expect("effects file"); + 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) } @@ -67,6 +72,11 @@ fn a_witnessed_overflow_check_is_recorded_with_its_kind() { 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); } @@ -80,18 +90,30 @@ fn a_function_without_a_witnessed_effect_has_no_row() { let _ = std::fs::remove_dir_all(&dir); } -/// Fails if repeated effects are collapsed: one row per occurrence, so a -/// count survives. +/// 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("multi"); + 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(); - // The reference output (`cg_lib.llbc_calls.txt`, written by an - // independent tool) counts the asserts per function; the sum must match. let reference: usize = std::fs::read_to_string(data("cg_lib.llbc_calls.txt")) .expect("reference") .lines() From 482a3ddf34b968e2b7e9fe0f34d384cb6def62f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 21:45:38 +0000 Subject: [PATCH 6/6] ruff_charon: cover DEREF_WRITE effects with an argument/local/plain fixture derefw.rs writes twice through argument-rooted derefs, once through a local reference, and has a function that assigns only locals. The new test pins the emitted kinds and counts, so dropping the rows or swapping Arg/Local fails. Codex P1 on #135. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/ruff_charon/tests/data/README.md | 1 + crates/ruff_charon/tests/data/derefw.llbc | 1 + crates/ruff_charon/tests/data/derefw.rs | 24 +++++++++++++++++++++++ crates/ruff_charon/tests/effects.rs | 19 ++++++++++++++++++ 4 files changed, 45 insertions(+) create mode 100644 crates/ruff_charon/tests/data/derefw.llbc create mode 100644 crates/ruff_charon/tests/data/derefw.rs diff --git a/crates/ruff_charon/tests/data/README.md b/crates/ruff_charon/tests/data/README.md index 61754ede1d4f3..9eb6f1eb78a04 100644 --- a/crates/ruff_charon/tests/data/README.md +++ b/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 ` 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. diff --git a/crates/ruff_charon/tests/data/derefw.llbc b/crates/ruff_charon/tests/data/derefw.llbc new file mode 100644 index 0000000000000..65e409c054489 --- /dev/null +++ b/crates/ruff_charon/tests/data/derefw.llbc @@ -0,0 +1 @@ +{"charon_version":"0.1.297","translated":{"crate_name":"derefw","options":{"ullbc":false,"no_code_duplication":false,"precise_drops":false,"mir":null,"rustc_args":[],"targets":[],"sysroot":null,"monomorphize":false,"monomorphize_mut":null,"start_from":[],"start_from_if_exists":[],"start_from_attribute":[],"start_from_pub":false,"include":[],"opaque":[],"exclude":[],"extract_opaque_bodies":false,"translate_all_methods":false,"eager_vtables":false,"duplicate_defaulted_methods":false,"lift_associated_types":[],"hide_marker_traits":false,"hide_allocator":false,"no_doc_comments":false,"remove_unused_clauses":false,"remove_unused_self_clauses":false,"remove_adt_clauses":false,"desugar_drops":false,"resugar_drops":false,"detect_drop_flags":false,"ops_to_function_calls":false,"index_to_function_calls":false,"treat_box_as_builtin":false,"no_gen_tuple_structs":false,"raw_consts":false,"inline_anon_consts":false,"consts":null,"unsized_strings":false,"reconstruct_fallible_operations":false,"reconstruct_panic_calls":false,"reconstruct_asserts":false,"reconstruct_matches":false,"deallocate_all_locals":false,"unbind_item_vars":false,"print_original_ullbc":false,"print_ullbc":false,"print_built_llbc":false,"print_llbc":false,"print_layouts":false,"print_safety":false,"dest_dir":null,"dest_file":"derefw.llbc","no_dedup_serialized_ast":true,"format":null,"run_with_minirust":false,"no_serialize":false,"skip_borrowck":false,"erase_body_lifetimes":false,"no_typecheck":false,"no_normalize":false,"no_reorder_decls":false,"no_compute_layout_guarantees":false,"abort_on_error":false,"error_on_warnings":false,"preset":null},"target_information":[{"key":"x86_64-unknown-linux-gnu","value":{"arch":"X86_64","vendor":"unknown","os":"Linux","env":"Gnu","cfg_abi":"Unspecified","target_pointer_size":8,"is_little_endian":true,"c_enum_smallest_repr_ty":"I32","primitive_alignments":[{"key":"Bool","value":1},{"key":{"Integer":{"Signed":"I8"}},"value":1},{"key":{"Integer":{"Signed":"I16"}},"value":2},{"key":{"Integer":{"Signed":"I32"}},"value":4},{"key":{"Integer":{"Signed":"I64"}},"value":8},{"key":{"Integer":{"Signed":"I128"}},"value":16},{"key":{"Integer":{"Signed":"Isize"}},"value":8},{"key":{"Integer":{"Unsigned":"U8"}},"value":1},{"key":{"Integer":{"Unsigned":"U16"}},"value":2},{"key":{"Integer":{"Unsigned":"U32"}},"value":4},{"key":{"Integer":{"Unsigned":"U64"}},"value":8},{"key":{"Integer":{"Unsigned":"U128"}},"value":16},{"key":{"Integer":{"Unsigned":"Usize"}},"value":8},{"key":{"Float":"F16"},"value":2},{"key":{"Float":"F32"},"value":4},{"key":{"Float":"F64"},"value":8},{"key":{"Float":"F128"},"value":16},{"key":"Char","value":4}]}}],"runtime_checks":{"ub_checks":true,"overflow_checks":true,"contract_checks":false},"files":[{"id":0,"name":{"Local":"derefw.rs"},"crate_name":"derefw","contents":"//! Writes through dereferenced places, for `tests/effects.rs`.\n//! `through_arg` writes twice through argument-rooted derefs, `through_local`\n//! writes once through a local reference, and `plain` assigns only to locals.\n\npub struct S {\n pub f: i32,\n}\n\npub fn through_arg(p: &mut i32, s: &mut S) {\n *p = 1;\n s.f = 2;\n}\n\npub fn through_local(v: i32) -> i32 {\n let mut x = v;\n let r = &mut x;\n *r = 3;\n x\n}\n\npub fn plain(a: i32) -> i32 {\n let y = a;\n y\n}\n"}],"item_names":[{"key":{"Type":0},"value":[{"Builtin":[{"Tuple":0},0]}]},{"key":{"Type":1},"value":[{"Ident":["derefw",0]},{"Ident":["S",0]}]},{"key":{"Fun":0},"value":[{"Ident":["derefw",0]},{"Ident":["through_arg",0]}]},{"key":{"Fun":1},"value":[{"Ident":["derefw",0]},{"Ident":["through_local",0]}]},{"key":{"Fun":2},"value":[{"Ident":["derefw",0]},{"Ident":["plain",0]}]}],"assoc_item_names":[],"short_names":[{"key":{"Type":1},"value":[{"Ident":["S",0]}]},{"key":{"Fun":1},"value":[{"Ident":["through_local",0]}]},{"key":{"Fun":0},"value":[{"Ident":["through_arg",0]}]},{"key":{"Fun":2},"value":[{"Ident":["plain",0]}]}],"type_decls":[{"def_id":0,"item_meta":{"name":[{"Builtin":[{"Tuple":0},0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null}},"source_text":null,"attr_info":{"attributes":[],"inline":null,"rename":null,"public":false},"is_local":false,"started_from":false,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"src":{"Builtin":"Tuple"},"kind":{"Struct":[]},"layout":[{"key":"x86_64-unknown-linux-gnu","value":{"size":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","0"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":{"Untagged":{"AtLeast":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","0"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}}}},"align":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","1"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":{"Untagged":{"AtLeast":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","1"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}}}},"discriminator":{"Known":0},"inhabited":{"Untagged":"True"},"variant_layouts":[{"field_offsets":[],"inhabited":{"Untagged":"True"},"tagger":[]}],"repr":{"repr_algo":"Rust","align_modif":null,"transparent":false,"explicit_discr_type":null}}}],"ptr_metadata":"None","marker_traits":{"is_sized":true,"is_send":true,"is_sync":true,"is_freeze":true,"is_unpin":true}},{"def_id":1,"item_meta":{"name":[{"Ident":["derefw",0]},{"Ident":["S",0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":5,"col":0},"end":{"line":7,"col":1}},"generated_from_span":null}},"source_text":"pub struct S {\n pub f: i32,\n}","attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"is_local":true,"started_from":true,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"src":"Normal","kind":{"Struct":[{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":6,"col":4},"end":{"line":6,"col":14}},"generated_from_span":null}},"attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"name":"f","is_positional":false,"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}]},"layout":[{"key":"x86_64-unknown-linux-gnu","value":{"size":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","4"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":{"Untagged":{"AtLeast":{"Untagged":{"AlignTo":{"base":{"Untagged":{"Plus":[{"Untagged":{"Constant":{"Untagged":[{"OffsetOf":[{"id":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":null},null,0]},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},{"Untagged":{"Constant":{"Untagged":[{"SizeOf":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}]}},"target_align":{"Untagged":{"Constant":{"Untagged":[{"AlignOf":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}}}}}}},"align":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","4"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":{"Untagged":{"AtLeast":{"Untagged":{"Constant":{"Untagged":[{"AlignOf":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}}}},"discriminator":{"Known":0},"inhabited":{"Untagged":"True"},"variant_layouts":[{"field_offsets":[{"guarantee":{"GuaranteedAlignment":{"Untagged":{"Constant":{"Untagged":[{"AlignOf":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}}},"chosen":0}],"inhabited":{"Untagged":"True"},"tagger":[]}],"repr":{"repr_algo":"Rust","align_modif":null,"transparent":false,"explicit_discr_type":null}}}],"ptr_metadata":"None","marker_traits":{"is_sized":true,"is_send":true,"is_sync":true,"is_freeze":true,"is_unpin":true}}],"fun_decls":[{"def_id":0,"item_meta":{"name":[{"Ident":["derefw",0]},{"Ident":["through_arg",0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":0},"end":{"line":12,"col":1}},"generated_from_span":null}},"source_text":"pub fn through_arg(p: &mut i32, s: &mut S) {\n *p = 1;\n s.f = 2;\n}","attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"is_local":true,"started_from":true,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[{"index":0,"name":null,"variance":"Covariant","mutability":"Unknown","late_bound":true},{"index":1,"name":null,"variance":"Covariant","mutability":"Unknown","late_bound":true}],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"signature":{"is_unsafe":false,"abi":"Rust","is_variadic":false,"inputs":[{"Untagged":{"Ref":[{"Var":{"Bound":[0,0]}},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}},{"Untagged":{"Ref":[{"Var":{"Bound":[0,1]}},{"Untagged":{"Adt":{"id":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":null}}},"Mut"]}}],"output":{"Untagged":{"Adt":{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"}}}},"src":"Normal","body":{"Structured":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":0},"end":{"line":12,"col":1}},"generated_from_span":null}},"bound_body_regions":4,"locals":{"arg_count":2,"locals":[{"index":0,"name":null,"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":42},"end":{"line":9,"col":42}},"generated_from_span":null}},"ty":{"Untagged":{"Adt":{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"}}},"drop_flag_for":null},{"index":1,"name":"p","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":19},"end":{"line":9,"col":20}},"generated_from_span":null}},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}},"drop_flag_for":null},{"index":2,"name":"s","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":32},"end":{"line":9,"col":33}},"generated_from_span":null}},"ty":{"Untagged":{"Ref":[{"Body":3},{"Untagged":{"Adt":{"id":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":null}}},"Mut"]}},"drop_flag_for":null}]},"body":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":0,"col":0},"end":{"line":12,"col":1}},"generated_from_span":null}},"id":1,"statements":[{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":0,"col":0},"end":{"line":0,"col":0}},"generated_from_span":null}},"id":0,"kind":{"StorageLive":0},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":0,"col":0},"end":{"line":0,"col":0}},"generated_from_span":null}},"id":1,"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Adt":{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"}}}},{"Aggregate":[{"Adt":[{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"},null,null]},[]]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":10,"col":4},"end":{"line":10,"col":10}},"generated_from_span":null}},"id":2,"kind":{"Assign":[{"kind":{"Projection":[{"kind":{"Local":1},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}}},"Deref"]},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Const":{"Untagged":[{"Integer":{"Signed":["I32","1"]}},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}]}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":11,"col":4},"end":{"line":11,"col":11}},"generated_from_span":null}},"id":3,"kind":{"Assign":[{"kind":{"Projection":[{"kind":{"Projection":[{"kind":{"Local":2},"ty":{"Untagged":{"Ref":[{"Body":3},{"Untagged":{"Adt":{"id":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":null}}},"Mut"]}}},"Deref"]},"ty":{"Untagged":{"Adt":{"id":1,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":null}}}},{"Field":[null,0]}]},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Const":{"Untagged":[{"Integer":{"Signed":["I32","2"]}},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}]}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":9,"col":43},"end":{"line":12,"col":1}},"generated_from_span":null}},"id":4,"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Adt":{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"}}}},{"Aggregate":[{"Adt":[{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"},null,null]},[]]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":12,"col":1},"end":{"line":12,"col":1}},"generated_from_span":null}},"id":5,"kind":"Return","comments_before":[]}]},"comments":[]}}},{"def_id":1,"item_meta":{"name":[{"Ident":["derefw",0]},{"Ident":["through_local",0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":14,"col":0},"end":{"line":19,"col":1}},"generated_from_span":null}},"source_text":"pub fn through_local(v: i32) -> i32 {\n let mut x = v;\n let r = &mut x;\n *r = 3;\n x\n}","attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"is_local":true,"started_from":true,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"signature":{"is_unsafe":false,"abi":"Rust","is_variadic":false,"inputs":[{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}],"output":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},"src":"Normal","body":{"Structured":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":14,"col":0},"end":{"line":19,"col":1}},"generated_from_span":null}},"bound_body_regions":2,"locals":{"arg_count":1,"locals":[{"index":0,"name":null,"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":14,"col":32},"end":{"line":14,"col":35}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null},{"index":1,"name":"v","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":14,"col":21},"end":{"line":14,"col":22}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null},{"index":2,"name":"x","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":8},"end":{"line":15,"col":13}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null},{"index":3,"name":"r","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":16,"col":8},"end":{"line":16,"col":9}},"generated_from_span":null}},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}},"drop_flag_for":null}]},"body":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":8},"end":{"line":19,"col":1}},"generated_from_span":null}},"id":3,"statements":[{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":8},"end":{"line":15,"col":13}},"generated_from_span":null}},"id":6,"kind":{"StorageLive":0},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":8},"end":{"line":15,"col":13}},"generated_from_span":null}},"id":7,"kind":{"StorageLive":2},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":16},"end":{"line":15,"col":17}},"generated_from_span":null}},"id":8,"kind":{"Assign":[{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Copy":{"kind":{"Local":1},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":15,"col":8},"end":{"line":15,"col":13}},"generated_from_span":null}},"id":9,"kind":{"Borrowck":{"FakeRead":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}}},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":16,"col":8},"end":{"line":16,"col":9}},"generated_from_span":null}},"id":10,"kind":{"StorageLive":3},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":16,"col":12},"end":{"line":16,"col":18}},"generated_from_span":null}},"id":11,"kind":{"Assign":[{"kind":{"Local":3},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}}},{"Ref":{"place":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},"kind":"Mut","ptr_metadata":{"Const":{"Untagged":[{"Adt":[null,[]]},{"Untagged":{"Adt":{"id":0,"generics":{"regions":[],"types":[],"const_generics":[],"trait_refs":[]},"builtin":"Tuple"}}}]}}}}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":16,"col":8},"end":{"line":16,"col":9}},"generated_from_span":null}},"id":12,"kind":{"Borrowck":{"FakeRead":{"kind":{"Local":3},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}}}}},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":17,"col":4},"end":{"line":17,"col":10}},"generated_from_span":null}},"id":13,"kind":{"Assign":[{"kind":{"Projection":[{"kind":{"Local":3},"ty":{"Untagged":{"Ref":[{"Body":1},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"Mut"]}}},"Deref"]},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Const":{"Untagged":[{"Integer":{"Signed":["I32","3"]}},{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}]}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":18,"col":4},"end":{"line":18,"col":5}},"generated_from_span":null}},"id":14,"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Copy":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":19,"col":0},"end":{"line":19,"col":1}},"generated_from_span":null}},"id":15,"kind":{"StorageDead":3},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":19,"col":0},"end":{"line":19,"col":1}},"generated_from_span":null}},"id":16,"kind":{"StorageDead":2},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":19,"col":1},"end":{"line":19,"col":1}},"generated_from_span":null}},"id":17,"kind":"Return","comments_before":[]}]},"comments":[]}}},{"def_id":2,"item_meta":{"name":[{"Ident":["derefw",0]},{"Ident":["plain",0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":21,"col":0},"end":{"line":24,"col":1}},"generated_from_span":null}},"source_text":"pub fn plain(a: i32) -> i32 {\n let y = a;\n y\n}","attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"is_local":true,"started_from":true,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"signature":{"is_unsafe":false,"abi":"Rust","is_variadic":false,"inputs":[{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}],"output":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},"src":"Normal","body":{"Structured":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":21,"col":0},"end":{"line":24,"col":1}},"generated_from_span":null}},"bound_body_regions":0,"locals":{"arg_count":1,"locals":[{"index":0,"name":null,"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":21,"col":24},"end":{"line":21,"col":27}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null},{"index":1,"name":"a","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":21,"col":13},"end":{"line":21,"col":14}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null},{"index":2,"name":"y","span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":8},"end":{"line":22,"col":9}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}},"drop_flag_for":null}]},"body":{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":8},"end":{"line":24,"col":1}},"generated_from_span":null}},"id":5,"statements":[{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":8},"end":{"line":22,"col":9}},"generated_from_span":null}},"id":18,"kind":{"StorageLive":0},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":8},"end":{"line":22,"col":9}},"generated_from_span":null}},"id":19,"kind":{"StorageLive":2},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":12},"end":{"line":22,"col":13}},"generated_from_span":null}},"id":20,"kind":{"Assign":[{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Copy":{"kind":{"Local":1},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":22,"col":8},"end":{"line":22,"col":9}},"generated_from_span":null}},"id":21,"kind":{"Borrowck":{"FakeRead":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}}},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":23,"col":4},"end":{"line":23,"col":5}},"generated_from_span":null}},"id":22,"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}},{"Use":[{"Copy":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":{"Integer":{"Signed":"I32"}}}}}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":24,"col":0},"end":{"line":24,"col":1}},"generated_from_span":null}},"id":23,"kind":{"StorageDead":2},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":24,"col":1},"end":{"line":24,"col":1}},"generated_from_span":null}},"id":24,"kind":"Return","comments_before":[]}]},"comments":[]}}}],"global_decls":[],"trait_decls":[],"trait_impls":[],"ordered_decls":[{"Type":{"NonRec":0}},{"Type":{"NonRec":1}},{"Fun":{"NonRec":0}},{"Fun":{"NonRec":1}},{"Fun":{"NonRec":2}}]},"has_errors":false} \ No newline at end of file diff --git a/crates/ruff_charon/tests/data/derefw.rs b/crates/ruff_charon/tests/data/derefw.rs new file mode 100644 index 0000000000000..62052a2f7266f --- /dev/null +++ b/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 +} diff --git a/crates/ruff_charon/tests/effects.rs b/crates/ruff_charon/tests/effects.rs index 82dbf08eda81b..00192b4c51412 100644 --- a/crates/ruff_charon/tests/effects.rs +++ b/crates/ruff_charon/tests/effects.rs @@ -122,3 +122,22 @@ fn the_assert_count_matches_the_reference() { 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); +}