From 247460efec0ea52bfb0c96b2958179fe9b81b96b Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Fri, 3 Jul 2026 08:40:29 +0400 Subject: [PATCH] A041 DuplicateLocalName --- CHANGELOG.md | 4 + core/analysis/README.md | 9 + core/analysis/src/errors.rs | 46 +- core/analysis/src/lib.rs | 10 + .../src/rules/duplicate_local_name.rs | 107 ++++ core/analysis/src/rules/mod.rs | 3 + .../docs/local-variables-lowering.md | 4 +- core/wasm-codegen/src/compiler.rs | 22 +- tests/src/analysis/mod.rs | 1 + tests/src/analysis/rules_a041.rs | 531 ++++++++++++++++++ tests/src/codegen/wasm/negative.rs | 25 + 11 files changed, 756 insertions(+), 6 deletions(-) create mode 100644 core/analysis/src/rules/duplicate_local_name.rs create mode 100644 tests/src/analysis/rules_a041.rs diff --git a/CHANGELOG.md b/CHANGELOG.md index ec0669c3..fc242176 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -373,6 +373,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 element has no enclosing variable name and panicked codegen. Distinct from A028 (whole-array `@`), and also covers a nested-array element such as the outer `@` in `[@, [1, 2]]`. The array-element sibling of #225's struct-literal-field fix ([#225]) +- A041 `DuplicateLocalName`: reject duplicate function-local names across disjoint + sibling blocks (if/else arms, sequential ifs, non-det blocks) with a two-location + diagnostic instead of panicking in codegen ([#217]) ### AST @@ -861,3 +864,4 @@ Initial tagged release. [#224]: https://github.com/Inferara/inference/issues/224 [#225]: https://github.com/Inferara/inference/issues/225 [#227]: https://github.com/Inferara/inference/issues/227 +[#217]: https://github.com/Inferara/inference/issues/217 diff --git a/core/analysis/README.md b/core/analysis/README.md index b66e2f74..a0f7bffb 100644 --- a/core/analysis/README.md +++ b/core/analysis/README.md @@ -131,6 +131,14 @@ A037 is the static half of array bounds checking. When the index is a constant i A compound (struct or array) `@` is lowered by writing into a *named* frame slot, which only a `let`/`const` binding supplies, so `@` of such a type is rejected wherever no slot exists. These complement A014 (array `@` as a function argument) and A027/A028 (whole-binding compound `@`). A scalar or enum `@` is unaffected: the type checker threads it its declared field/element type, so it lowers to a single uzumaki opcode. Array-literal arguments are handled separately by A012, so these rules do not extend to that position. +### Duplicate Local Names (errors) + +| ID | Struct | Severity | What it checks | +|----|--------|----------|----------------| +| A041 | `DuplicateLocalName` | error | a function-local name (`let`/`const`) declared more than once per function body; well-typed across disjoint sibling blocks but collides in the flat WebAssembly local namespace — rename or hoist a single declaration | + +A041 rejects a function-local name introduced more than once in a single function body, even when the two declarations sit in disjoint sibling blocks (`if`/`else` arms, sequential `if`s, `loop` bodies, or non-deterministic blocks) and are individually well-typed — the type checker's scope-based shadowing check never flags them, since sibling scopes never coexist. The conflict surfaces one phase later: `core/wasm-codegen` flattens every body local into a single name-keyed WebAssembly local namespace, so two sibling declarations of the same name would otherwise collide. This is a simplicity and auditability rule, not a proof-soundness requirement — the Rocq translation addresses locals by numeric index, so the flat namespace exists only to preserve a 1:1 mapping between source name, WASM local, and proof index for humans reading traces and proofs. The diagnostic cites both declaration sites and suggests renaming one of them or hoisting a single declaration above the blocks. + ## Diagnostic Output Format ``` @@ -231,6 +239,7 @@ Test files are organized by rule group: | `rules_a038.rs` | A038 (uzumaki on compound struct field) | | `rules_a039.rs` | A039 (struct uzumaki passed as function argument) | | `rules_a040.rs` | A040 (uzumaki as compound element of an array literal) | +| `rules_a041.rs` | A041 (duplicate function-local name across sibling blocks) | | `walker_tests.rs` | `walk_function_bodies`, `WalkContext` depth tracking | ## Dependencies diff --git a/core/analysis/src/errors.rs b/core/analysis/src/errors.rs index af4ef9a4..64a3a7a4 100644 --- a/core/analysis/src/errors.rs +++ b/core/analysis/src/errors.rs @@ -209,6 +209,13 @@ pub enum AnalysisDiagnostic { length: u32, location: Location, }, + + #[error("local `{name}` is already declared in this function (first declaration at {first_location}); each local name is introduced once per function body — rename one of them or hoist a single declaration above the blocks")] + DuplicateLocalName { + name: String, + location: Location, + first_location: Location, + }, } impl AnalysisDiagnostic { @@ -252,7 +259,8 @@ impl AnalysisDiagnostic { | AnalysisDiagnostic::VisibilityInsideSpec { location, .. } | AnalysisDiagnostic::RecursionDetected { location, .. } | AnalysisDiagnostic::StackDepthExceeded { location, .. } - | AnalysisDiagnostic::ArrayIndexConstOutOfBounds { location, .. } => location, + | AnalysisDiagnostic::ArrayIndexConstOutOfBounds { location, .. } + | AnalysisDiagnostic::DuplicateLocalName { location, .. } => location, } } @@ -300,6 +308,7 @@ impl AnalysisDiagnostic { AnalysisDiagnostic::UzumakiOnCompoundField { .. } => "A038", AnalysisDiagnostic::StructUzumakiAsArgument { .. } => "A039", AnalysisDiagnostic::UzumakiOnCompoundArrayElement { .. } => "A040", + AnalysisDiagnostic::DuplicateLocalName { .. } => "A041", } } } @@ -1197,6 +1206,41 @@ mod tests { assert_eq!(err.rule_id(), "A040"); } + #[test] + fn display_duplicate_local_name() { + let first_location = Location { + offset_start: 0, + offset_end: 5, + start_line: 2, + start_column: 9, + end_line: 2, + end_column: 14, + }; + let err = AnalysisDiagnostic::DuplicateLocalName { + name: "x".to_string(), + location: test_location(), + first_location, + }; + let text = err.to_string(); + assert!( + text.contains("local `x` is already declared"), + "A041 diagnostic must name the duplicated local, got: {text}" + ); + assert!( + text.contains("first declaration at 2:9"), + "A041 diagnostic must cite the first declaration's location, got: {text}" + ); + assert!( + text.contains("rename one of them or hoist"), + "A041 diagnostic must give the rename-or-hoist guidance, got: {text}" + ); + assert!( + !text.contains("shadow"), + "A041 diagnostic must not use shadowing terminology, got: {text}" + ); + assert_eq!(err.rule_id(), "A041"); + } + #[test] fn partial_eq_for_diagnostic() { let a = AnalysisDiagnostic::BreakOutsideLoop { diff --git a/core/analysis/src/lib.rs b/core/analysis/src/lib.rs index 30dc8800..da7b4100 100644 --- a/core/analysis/src/lib.rs +++ b/core/analysis/src/lib.rs @@ -85,6 +85,15 @@ //! `c < 0` or `c >= length`. This is a compile-time check with zero runtime //! cost; dynamic (non-literal) indices are out of scope for this rule. //! +//! ### Duplicate Local Names (A041) +//! +//! - A041: A function-local name (`let` or `const`) may be declared at most once +//! per function body. Reusing a name across disjoint sibling blocks is well +//! typed but collides in the flat WebAssembly local namespace, so it is +//! rejected with a rename-or-hoist hint. This is a simplicity and auditability +//! rule — it preserves a 1:1 source-name to local to proof-index mapping per +//! function — not a proof-soundness requirement. +//! //! ## Pipeline Position //! //! ```text @@ -198,6 +207,7 @@ mod tests { AnalysisDiagnostic::UzumakiOnCompoundField { field: "i".to_string(), ty: "Inner".to_string(), location: dummy_location() }, AnalysisDiagnostic::StructUzumakiAsArgument { location: dummy_location() }, AnalysisDiagnostic::UzumakiOnCompoundArrayElement { ty: "Point".to_string(), location: dummy_location() }, + AnalysisDiagnostic::DuplicateLocalName { name: "x".to_string(), location: dummy_location(), first_location: dummy_location() }, ]; let rules = rules::all_rules(); diff --git a/core/analysis/src/rules/duplicate_local_name.rs b/core/analysis/src/rules/duplicate_local_name.rs new file mode 100644 index 00000000..c837c5c8 --- /dev/null +++ b/core/analysis/src/rules/duplicate_local_name.rs @@ -0,0 +1,107 @@ +//! A041: A function-local name is declared at most once per function body. +//! +//! Every `let` and `const` binding in a function body shares a single flat +//! namespace. Two declarations of the same name — even in disjoint sibling +//! blocks that never coexist at runtime (the two arms of an `if`, two +//! sequential `if`s, a loop body and a later block, or two non-deterministic +//! blocks) — are rejected here. +//! +//! The type checker treats each lexical block as its own scope, so reusing a +//! name across sibling blocks is *not* shadowing and it is accepted there. Code +//! generation, however, flattens every body local into one name-keyed map (one +//! WebAssembly local per source name), where a repeated name would collide. +//! This rule enforces the flat-namespace contract as a diagnostic instead of a +//! codegen crash. +//! +//! The rationale is simplicity and auditability, **not** proof soundness: the +//! Rocq backend addresses locals by numeric index and is unaffected by names, +//! so either policy yields a sound proof term. What a single flat namespace +//! buys is a 1:1 source-name to WebAssembly-local to proof-index mapping per +//! function, which keeps proofs and traces legible to a human reading them. +//! See issue #217. +//! +//! ## Invariant +//! +//! A041 must flag *exactly* the body-local duplicates that would trip the +//! defense-in-depth collision asserts in wasm-codegen's `pre_scan_locals`. The +//! two walks must agree: if they diverge, either a panic leaks through (A041 +//! misses a duplicate) or legal code is rejected (A041 over-flags). To hold +//! that agreement, the descent here mirrors `pre_scan_locals`' pre-order DFS — +//! it recurses through `Stmt::Block`, both arms of `Stmt::If`, and `Stmt::Loop` +//! bodies, treating `VarDef`/`ConstDef` as leaves. Non-deterministic blocks +//! (`forall`/`exists`/`unique`/`assume`) surface as `Stmt::Block` carrying a +//! kind and are descended unconditionally, exactly as codegen descends them. +//! +//! Parameters are out of scope: a body local that reuses a parameter name is +//! already rejected by the type checker (`VariableShadowed`, since parameters +//! sit in an enclosing scope), and analysis only runs on type-checked programs. +//! The accumulator is therefore a flat per-body map with no scope tree — it +//! makes no ancestor/sibling distinction because the type checker has already +//! removed every ancestor collision. + +use inference_ast::arena::AstArena; +use inference_ast::ids::{IdentId, StmtId}; +use inference_ast::nodes::{Def, Location, Stmt}; +use rustc_hash::FxHashMap; + +use crate::{ + errors::{AnalysisDiagnostic, LabeledDiagnostic}, + walker, +}; + +crate::rule! { + /// A function-local name may be declared at most once per function body. + #[id = "A041"] + #[name = "Duplicate local name"] + #[severity = error] + pub struct DuplicateLocalName; + fn check(ctx: &TypedContext) -> Vec { + let mut errors = Vec::new(); + let arena = ctx.arena(); + for source_file in ctx.source_files() { + let module_path = &source_file.module_path; + walker::for_each_function_body(arena, &source_file.defs, &mut |body_id| { + // Fresh per body: names in different functions never interact. + let mut first_seen: FxHashMap = FxHashMap::default(); + walker::walk_block_stmts(arena, body_id, &mut |stmt_id| { + let Some((name_id, location)) = local_declaration(arena, stmt_id) else { + return; + }; + let name = arena[name_id].name.clone(); + if let Some(&first_location) = first_seen.get(&name) { + errors.push(LabeledDiagnostic::new( + module_path.clone(), + AnalysisDiagnostic::DuplicateLocalName { + name, + location, + first_location, + }, + )); + } else { + first_seen.insert(name, location); + } + }); + }); + } + errors + } +} + +/// The declared name and the statement's own location for a `let` or `const` +/// statement, or `None` for any other statement. +/// +/// Both arms cite `arena[stmt_id].location` so the caret points at the whole +/// statement uniformly — for a `ConstDef` this is the statement's location, not +/// the inner `Def::Constant` node's. +#[must_use = "the extracted declaration drives duplicate detection"] +fn local_declaration(arena: &AstArena, stmt_id: StmtId) -> Option<(IdentId, Location)> { + let location = arena[stmt_id].location; + match &arena[stmt_id].kind { + Stmt::VarDef { name, .. } => Some((*name, location)), + Stmt::ConstDef(def_id) => match &arena[*def_id].kind { + Def::Constant { name, .. } => Some((*name, location)), + _ => None, + }, + _ => None, + } +} diff --git a/core/analysis/src/rules/mod.rs b/core/analysis/src/rules/mod.rs index bbc47fd2..cef47297 100644 --- a/core/analysis/src/rules/mod.rs +++ b/core/analysis/src/rules/mod.rs @@ -10,6 +10,7 @@ pub mod compound_literal_position; pub mod compound_return_call_assignment; pub mod compound_return_call_position; pub mod dead_code; +pub mod duplicate_local_name; pub mod empty_enum_definition; pub mod empty_struct_definition; pub mod extern_function_call; @@ -48,6 +49,7 @@ use compound_literal_position::CompoundLiteralPosition; use compound_return_call_assignment::CompoundReturnCallAssignment; use compound_return_call_position::CompoundReturnCallPosition; use dead_code::DeadCode; +use duplicate_local_name::DuplicateLocalName; use empty_enum_definition::EmptyEnumDefinition; use empty_struct_definition::EmptyStructDefinition; use extern_function_call::ExternFunctionCall; @@ -120,5 +122,6 @@ pub fn all_rules() -> &'static [&'static dyn crate::rule::Rule] { &UzumakiOnCompoundField, &StructUzumakiAsArgument, &UzumakiOnCompoundArrayElement, + &DuplicateLocalName, ] } diff --git a/core/wasm-codegen/docs/local-variables-lowering.md b/core/wasm-codegen/docs/local-variables-lowering.md index d07e32f3..ee5cc36e 100644 --- a/core/wasm-codegen/docs/local-variables-lowering.md +++ b/core/wasm-codegen/docs/local-variables-lowering.md @@ -80,7 +80,9 @@ The pre-scan intentionally flattens all nested scopes into a single WASM local p local declared inside a `forall { }` block, an `if` arm, an `else` arm, or a `loop` body shares the same pool as one declared at the top of the function. This is consistent with how WebAssembly defines locals: they are function-scoped, not block-scoped. The Inference -type-checker is responsible for enforcing lexical scoping rules at the language level. +type-checker enforces lexical scoping for nested (ancestor) shadowing; analysis rule A041 +additionally rejects a name declared more than once across disjoint sibling blocks, since +such names are individually well-typed but would otherwise collide in this flat pool. ## Supported Initializer Expression Kinds diff --git a/core/wasm-codegen/src/compiler.rs b/core/wasm-codegen/src/compiler.rs index 9a03a743..81548b5c 100644 --- a/core/wasm-codegen/src/compiler.rs +++ b/core/wasm-codegen/src/compiler.rs @@ -1366,7 +1366,8 @@ impl Compiler { assert!( prev.is_none(), "local `{const_name}` collides with an existing entry in locals_map; \ - the type-checker should have rejected shadowing", + analysis rule A041 rejects duplicate function-local names before codegen \ + (each name maps to exactly one WebAssembly local)", ); *local_idx += 1; } @@ -1386,7 +1387,8 @@ impl Compiler { assert!( prev.is_none(), "local `{var_name}` collides with an existing entry in locals_map; \ - the type-checker should have rejected shadowing", + analysis rule A041 rejects duplicate function-local names before codegen \ + (each name maps to exactly one WebAssembly local)", ); *local_idx += 1; } @@ -1682,7 +1684,13 @@ impl Compiler { element_layout, }; let binding_name = arena[name_id].name.clone(); - array_offsets.insert(binding_name, slot); + let prev = array_offsets.insert(binding_name.clone(), slot); + assert!( + prev.is_none(), + "array local `{binding_name}` collides with an existing frame slot; \ + analysis rule A041 rejects duplicate function-local names before codegen \ + (each name maps to exactly one frame slot)", + ); *current_offset = aligned_offset.checked_add(byte_count).expect( "Frame offset overflow: total array allocation exceeds u32::MAX", ); @@ -1719,7 +1727,13 @@ impl Compiler { fields: field_slots, }; let binding_name = arena[name_id].name.clone(); - struct_offsets.insert(binding_name, slot); + let prev = struct_offsets.insert(binding_name.clone(), slot); + assert!( + prev.is_none(), + "struct local `{binding_name}` collides with an existing frame slot; \ + analysis rule A041 rejects duplicate function-local names before codegen \ + (each name maps to exactly one frame slot)", + ); *current_offset = aligned_offset.checked_add(total_size).expect( "Frame offset overflow: struct allocation exceeds u32::MAX", ); diff --git a/tests/src/analysis/mod.rs b/tests/src/analysis/mod.rs index fe8b38b7..f3968b3c 100644 --- a/tests/src/analysis/mod.rs +++ b/tests/src/analysis/mod.rs @@ -16,4 +16,5 @@ mod rules_a037; mod rules_a038; mod rules_a039; mod rules_a040; +mod rules_a041; mod walker_tests; diff --git a/tests/src/analysis/rules_a041.rs b/tests/src/analysis/rules_a041.rs new file mode 100644 index 00000000..a4ff06e6 --- /dev/null +++ b/tests/src/analysis/rules_a041.rs @@ -0,0 +1,531 @@ +/// Integration tests for analysis rule A041. +/// +/// - A041: DuplicateLocalName — each function-local name (`let`/`const`) may be +/// introduced at most once per function body. Two declarations of the same +/// name in disjoint sibling blocks — both arms of an `if`, two sequential +/// `if`s, a loop body and a later block, or two non-deterministic blocks — +/// are rejected here, because codegen flattens every body local into one +/// name-keyed map (one WebAssembly local per source name) where a repeat would +/// collide. Ancestor (nested) and parameter collisions are the type checker's +/// `VariableShadowed` territory and never reach analysis, so this file does not +/// exercise those shapes. +/// +/// These tests are the cross-crate guard that the rule fires through a real +/// parse -> type-check -> analyze pipeline on Inference source, complementing the +/// in-crate message/`rule_id` unit tests in `core/analysis`. +#[cfg(test)] +mod analysis_rules_tests { + use crate::utils::{build_ast, try_codegen, try_type_check_multi_file}; + use inference_analysis::errors::{AnalysisDiagnostic, AnalysisErrors, AnalysisResult}; + use inference_type_checker::typed_context::TypedContext; + + fn type_check(source: &str) -> TypedContext { + let arena = build_ast(source.to_string()); + inference_type_checker::TypeCheckerBuilder::build_typed_context(arena) + .expect("type checking should succeed for analysis test input") + .typed_context() + } + + fn analyze(source: &str) -> Result { + let ctx = type_check(source); + inference_analysis::analyze(&ctx) + } + + /// Returns true if any analysis error is a `DuplicateLocalName` (A041). + /// Filters by variant rather than asserting a total error count, since the + /// surface may also trip unrelated rules. + fn has_a041(source: &str) -> bool { + match analyze(source) { + Ok(_) => false, + Err(errors) => errors + .errors() + .iter() + .any(|e| matches!(e, AnalysisDiagnostic::DuplicateLocalName { .. })), + } + } + + fn a041_diag(source: &str) -> AnalysisDiagnostic { + analyze(source) + .expect_err("expected analysis errors but got Ok") + .errors() + .iter() + .find(|e| matches!(e, AnalysisDiagnostic::DuplicateLocalName { .. })) + .expect("expected a DuplicateLocalName diagnostic") + .clone() + } + + /// Counts how many `DuplicateLocalName` (A041) diagnostics the analysis emits + /// for `source`. Used by the triple-duplicate test that asserts an exact A041 + /// count; like the other helpers it filters by variant so unrelated rules + /// tripped by the same surface do not perturb the count. + fn count_a041(source: &str) -> usize { + match analyze(source) { + Ok(_) => 0, + Err(errors) => errors + .errors() + .iter() + .filter(|e| matches!(e, AnalysisDiagnostic::DuplicateLocalName { .. })) + .count(), + } + } + + /// Collects every `DuplicateLocalName` (A041) diagnostic for `source`, so a + /// multi-violation test can inspect each diagnostic's two locations. + fn a041_diags(source: &str) -> Vec { + match analyze(source) { + Ok(_) => Vec::new(), + Err(errors) => errors + .errors() + .iter() + .filter(|e| matches!(e, AnalysisDiagnostic::DuplicateLocalName { .. })) + .cloned() + .collect(), + } + } + + // --------------------------------------------------------------------- + // Fires: duplicates across disjoint sibling blocks + // --------------------------------------------------------------------- + + /// The two arms of one `if`/`else` each declare `x`. The arms are disjoint + /// sibling scopes (no ancestor `x`), so the type checker accepts them, but + /// they collapse to one WebAssembly local — A041 must fire on `x`. + #[test] + fn a041_if_else_arms_same_name_rejected() { + let source = r#" + fn f(c: bool) { + if c { + let x: i32 = 1; + } else { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 to flag the duplicated `x` across the if/else arms, got: {diag}" + ); + } + + /// The issue's exact repro: two sequential `if`s, each declaring `x` in its + /// then-arm, followed by a trailing `let z` so every path returns. The two + /// `x`s live in sibling blocks at the same depth under different parents — + /// the shape codegen panicked on. + #[test] + fn a041_sequential_sibling_ifs_rejected() { + let source = r#"pub fn f(c: bool) -> i32 { if c { let x: i32 = 1; return x; } if !c { let x: i32 = 2; return x; } let z: i32 = 0; return z; }"#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 to flag `x` across the two sequential ifs, got: {diag}" + ); + } + + /// Sibling reuse at the SAME nesting depth under DIFFERENT parents: `x` in the + /// then-arm of one `if` and in the then-arm of a second `if`, isolated with + /// no returns to obscure it. + #[test] + fn a041_two_then_arms_same_depth_rejected() { + let source = r#" + fn f(c: bool) { + if c { + let x: i32 = 1; + } + if c { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for `x` reused in two sibling then-arms, got: {diag}" + ); + } + + /// A `loop` body declares `x` and a later plain `{ }` block declares `x` + /// again. The two are disjoint siblings; A041 descends into both the loop + /// body and the bare block exactly as codegen's `pre_scan_locals` does. + #[test] + fn a041_loop_body_then_block_rejected() { + let source = r#" + fn f() { + loop { + let x: i32 = 1; + break; + } + { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for `x` in a loop body and a later block, got: {diag}" + ); + } + + /// Two sibling non-deterministic blocks — a `forall` then an `exists` — each + /// declare `x`. The descent is BlockKind-agnostic: non-det blocks are walked + /// with the same per-body accumulator as any other block, so the reuse is + /// caught. (Neither block needs an uzumaki to be legal.) + #[test] + fn a041_sibling_nondet_blocks_rejected() { + let source = r#" + fn f() { + forall { + let x: i32 = 1; + } + exists { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for `x` across a forall and an exists block, got: {diag}" + ); + } + + /// A `const x` in one sibling arm and a `let x` in the other collide: the rule + /// treats `ConstDef` and `VarDef` as the same flat namespace, so the + /// cross-kind duplicate is rejected. + #[test] + fn a041_const_then_let_cross_collision_rejected() { + let source = r#" + fn f(c: bool) { + if c { + const x: i32 = 1; + } + if !c { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for a `const x` then `let x` cross-collision, got: {diag}" + ); + } + + /// The reverse direction of the cross-kind collision: a `let x` first, then a + /// `const x`. `local_declaration` must recognise both kinds whether they land + /// first or second in the walk. + #[test] + fn a041_let_then_const_cross_collision_rejected() { + let source = r#" + fn f(c: bool) { + if c { + let x: i32 = 1; + } + if !c { + const x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for a `let x` then `const x` cross-collision, got: {diag}" + ); + } + + /// Three sibling blocks each declare `x`. A041 emits one diagnostic per + /// *repeat*, so three declarations yield exactly two diagnostics, and both + /// cite the SAME first declaration. The source has no leading newline so line + /// numbers are unambiguous: the first `x` is on line 2, the repeats on lines + /// 3 and 4. + #[test] + fn a041_triple_duplicate_emits_two_diagnostics_citing_first() { + let source = r#"fn f(c: bool) { + if c { let x: i32 = 1; } + if c { let x: i32 = 2; } + if c { let x: i32 = 3; } +}"#; + assert_eq!( + count_a041(source), + 2, + "three sibling declarations of `x` must yield exactly two A041 diagnostics" + ); + let diags = a041_diags(source); + assert_eq!(diags.len(), 2, "expected exactly two A041 diagnostics"); + + let mut first_lines = Vec::new(); + let mut first_locations = Vec::new(); + let mut repeat_locations = Vec::new(); + for diag in &diags { + let AnalysisDiagnostic::DuplicateLocalName { + name, + location, + first_location, + } = diag + else { + panic!("filtered diagnostic was not a DuplicateLocalName: {diag}"); + }; + assert_eq!(name, "x", "each diagnostic must name the duplicated local `x`"); + first_lines.push(first_location.start_line); + first_locations.push(*first_location); + repeat_locations.push(*location); + } + + assert_eq!( + first_locations[0], first_locations[1], + "both A041 diagnostics must cite the same first declaration" + ); + assert_eq!( + first_lines[0], 2, + "the cited first declaration must be the line-2 `let x`, got line {}", + first_lines[0] + ); + assert_ne!( + repeat_locations[0], repeat_locations[1], + "the two diagnostics must be anchored at the two distinct repeat sites" + ); + } + + /// Two sibling blocks each declare a compound (`Point`) local `p`. This is the + /// frame-slot hazard shape: two compound `p`s would otherwise map to one + /// name-keyed frame slot. A041 fires on `p` before that can happen. + #[test] + fn a041_compound_struct_duplicate_rejected() { + let source = r#" + struct Point { x: i32; y: i32; } + fn f(c: bool) { + if c { + let p: Point = Point { x: 1, y: 2 }; + } + if !c { + let p: Point = Point { x: 3, y: 4 }; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "p"), + "expected A041 for the duplicated compound local `p`, got: {diag}" + ); + } + + /// A duplicate inside a struct *method* body is caught: the walker's + /// `for_each_function_body` descends into methods, and each method body gets + /// its own fresh accumulator. The method accesses `self` so it trips no + /// unrelated rule. + #[test] + fn a041_duplicate_in_method_body_rejected() { + let source = r#" + struct S { + v: i32; + fn m(self, c: bool) -> i32 { + if c { + let x: i32 = 1; + } + if !c { + let x: i32 = 2; + } + return self.v; + } + } + fn main() -> i32 { return 0; } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for `x` duplicated inside a method body, got: {diag}" + ); + } + + /// A duplicate inside a *spec function* body is caught: `for_each_function_body` + /// recurses into spec definitions, so proof-obligation bodies are walked like + /// any other. + #[test] + fn a041_duplicate_in_spec_function_rejected() { + let source = r#" + fn main() -> i32 { return 0; } + spec S { + fn check(c: bool) -> i32 { + if c { + let x: i32 = 1; + } + if !c { + let x: i32 = 2; + } + return 0; + } + } + "#; + let diag = a041_diag(source); + assert!( + matches!(&diag, AnalysisDiagnostic::DuplicateLocalName { name, .. } if name == "x"), + "expected A041 for `x` duplicated inside a spec function body, got: {diag}" + ); + } + + // --------------------------------------------------------------------- + // Diagnostic quality + // --------------------------------------------------------------------- + + /// The diagnostic names the duplicated local, cites the first declaration, + /// gives the rename-or-hoist guidance, never uses shadowing terminology, and + /// reports rule id A041. + #[test] + fn a041_diagnostic_quality() { + let source = r#" + fn f(c: bool) { + if c { + let x: i32 = 1; + } + if !c { + let x: i32 = 2; + } + } + "#; + let diag = a041_diag(source); + let msg = diag.to_string(); + assert!( + msg.contains("is already declared in this function"), + "A041 message must state the local is already declared, got: {msg}" + ); + assert!( + msg.contains("first declaration at"), + "A041 message must cite the first declaration, got: {msg}" + ); + assert!( + msg.contains("rename one of them or hoist"), + "A041 message must give the rename-or-hoist guidance, got: {msg}" + ); + assert!( + !msg.contains("shadow"), + "A041 message must not use shadowing terminology (nothing is shadowed here), got: {msg}" + ); + assert_eq!(diag.rule_id(), "A041"); + } + + // --------------------------------------------------------------------- + // Does not fire + // --------------------------------------------------------------------- + + /// Distinct names in the two arms (`a` in then, `b` in else) share no local + /// name, so A041 must stay silent — the accepted-code shape. + #[test] + fn a041_unique_names_in_sibling_arms_accepted() { + let source = r#" + fn f(c: bool) { + if c { + let a: i32 = 1; + } else { + let b: i32 = 2; + } + } + "#; + assert!( + !has_a041(source), + "distinct names `a` and `b` in sibling arms must not trip A041" + ); + } + + /// The same local name in two different functions in one file is fine: each + /// function body gets a fresh accumulator, so the names never interact. + #[test] + fn a041_same_name_in_two_functions_accepted() { + let source = r#" + fn f() { + let x: i32 = 1; + } + fn g() { + let x: i32 = 2; + } + "#; + assert!( + !has_a041(source), + "the same local name in two different functions must not trip A041" + ); + } + + /// The hoisted rewrite the diagnostic suggests — a single `let mut x` above + /// the branches, assigned in each and used after — must compile cleanly all + /// the way through parse -> type-check -> analyze -> codegen. `try_codegen` + /// runs that whole pipeline and catches panics, so an `Ok` here pins that the + /// suggested fix genuinely works (and trips no analysis error, since a stray + /// diagnostic would make the pipeline fail rather than return `Ok`). + #[test] + fn a041_hoisted_single_declaration_compiles_end_to_end() { + let source = r#" + fn f(c: bool) -> i32 { + let mut x: i32 = 0; + if c { + x = 1; + } else { + x = 2; + } + return x; + } + "#; + assert!( + !has_a041(source), + "a single hoisted declaration must not trip A041" + ); + assert!( + try_codegen(source).is_ok(), + "the hoisted rewrite must compile end-to-end through the analysis-inclusive pipeline" + ); + } + + // --------------------------------------------------------------------- + // Multi-file: per-function scoping across module boundaries + // --------------------------------------------------------------------- + + /// Type-checks a multi-file program (entry first, empty module path) and runs + /// the analysis pass, returning its result. + fn analyze_multi(files: &[(Vec<&str>, &str)]) -> Result { + let ctx = try_type_check_multi_file(files) + .expect("multi-file type checking should succeed for analysis test input"); + inference_analysis::analyze(&ctx) + } + + fn has_a041_multi(files: &[(Vec<&str>, &str)]) -> bool { + match analyze_multi(files) { + Ok(_) => false, + Err(errors) => errors + .errors() + .iter() + .any(|e| matches!(e, AnalysisDiagnostic::DuplicateLocalName { .. })), + } + } + + /// The same local name declared in functions in two *different files* must not + /// trip A041: the fresh-per-body accumulator makes names in distinct function + /// bodies non-interacting even across module boundaries. Both files must + /// type-check as one project, so the entry `use`s and calls the module fn. + #[test] + fn a041_same_name_in_two_files_accepted() { + let files: &[(Vec<&str>, &str)] = &[ + ( + vec![], + r#" + use lib; + pub fn main() -> i32 { + let x: i32 = lib::helper(); + return x; + } + "#, + ), + ( + vec!["lib"], + r#" + pub fn helper() -> i32 { + let x: i32 = 1; + return x; + } + "#, + ), + ]; + assert!( + !has_a041_multi(files), + "the same local `x` in functions in two different files must not trip A041" + ); + } +} diff --git a/tests/src/codegen/wasm/negative.rs b/tests/src/codegen/wasm/negative.rs index 8c580324..8f0696ba 100644 --- a/tests/src/codegen/wasm/negative.rs +++ b/tests/src/codegen/wasm/negative.rs @@ -344,3 +344,28 @@ mod extern_function_call { ); } } + +mod duplicate_local_name { + use crate::utils::try_codegen_no_analysis; + + /// The issue repro — two sequential sibling `if`s each declaring `x` — is + /// rejected by analysis rule A041, so it only reaches codegen on the + /// no-analysis path. There, `pre_scan_locals`' flat `locals_map` still + /// catches the duplicate as a defense-in-depth backstop. This pins that the + /// backstop survives and that A041 and codegen agree on this shape. + #[test] + fn duplicate_local_backstop_assert_still_fires_without_analysis() { + let result = try_codegen_no_analysis( + r#"pub fn f(c: bool) -> i32 { if c { let x: i32 = 1; return x; } if !c { let x: i32 = 2; return x; } let z: i32 = 0; return z; }"#, + ); + assert!( + result.is_err(), + "duplicate function-local name should panic in codegen without analysis" + ); + let err = result.unwrap_err(); + assert!( + err.contains("collides with an existing entry in locals_map"), + "unexpected error message: {err}" + ); + } +}