diff --git a/crates/ruff_charon/src/lib.rs b/crates/ruff_charon/src/lib.rs index aaebf8bb9b17a..42a22fc538fb5 100644 --- a/crates/ruff_charon/src/lib.rs +++ b/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, + method_name: Option, + 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, +} + +/// 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 { @@ -277,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; @@ -305,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), + }); } _ => {} } @@ -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 { 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/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 new file mode 100644 index 0000000000000..00192b4c51412 --- /dev/null +++ b/crates/ruff_charon/tests/effects.rs @@ -0,0 +1,143 @@ +//! 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. +#![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::().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); +}