From 79cec9615b4a28e90b93dbbda93fa998fe70417a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 26 Jun 2026 14:42:20 +0200 Subject: [PATCH] feat(analysis): verify wrpc-binding Actual_Connection_Binding resolves to a bus (REQ-WRPC-BINDING-003) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to REQ-WRPC-BINDING-002 (presence check). When a cross-processor connection HAS an Actual_Connection_Binding, wrpc-binding now resolves the binding's `reference (...)` target and warns ONLY when it resolves UNAMBIGUOUSLY to a non-bus component. A bus / virtual bus, an unresolvable name, a dotted/multi-level path, or a multi-reference list are all accepted (the sound rule from the requirement — avoids new false-positives). - extract_simple_reference_name: split-based parse of `reference (x)` / `(reference (x))`; rejects empty, dotted, and multi-reference values. - unambiguous_non_bus_category: warns only on an exactly-one-match non-bus resolution. Oracle (TEST-WRPC-BINDING-BUS-TARGET): non-bus target warns; real bus and virtual bus do not; unresolvable / dotted / multi-reference do not; parser unit test. 16 wrpc tests pass (10 existing unchanged), 898 spar-analysis lib tests pass, clippy -D clean, nightly fmt clean, mutation --in-diff 8 caught / 3 unviable / 0 missed. Co-Authored-By: Claude Opus 4.8 (1M context) --- .gitignore | 3 + artifacts/requirements.yaml | 2 +- artifacts/verification.yaml | 27 +++ crates/spar-analysis/src/wrpc_binding.rs | 200 ++++++++++++++++++++++- 4 files changed, 222 insertions(+), 10 deletions(-) diff --git a/.gitignore b/.gitignore index bcb1893..96ae595 100644 --- a/.gitignore +++ b/.gitignore @@ -24,3 +24,6 @@ verification.yaml # cargo-mutants output — regenerable mutation-testing scratch. /mutants.out/ /mutants.out.old/ + +# Agent-maintained durable session scratch — never commit. +.pulseengine-session-notes.md diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index a010b72..f7fc6f0 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -2309,7 +2309,7 @@ artifacts: resolves UNAMBIGUOUSLY to a non-bus component, accept otherwise". Oracle: a connection bound to a non-bus component warns; one bound to a bus, or whose reference cannot be resolved, does not. - status: proposed + status: implemented tags: [wrpc, binding, analysis] fields: release: v0.22.0 diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index ec44723..95480ee 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -3337,6 +3337,33 @@ artifacts: - type: satisfies target: REQ-WRPC-BINDING-002 + - id: TEST-WRPC-BINDING-BUS-TARGET + type: feature + title: wrpc-binding verifies Actual_Connection_Binding resolves to a bus + description: > + Unit tests in crates/spar-analysis/src/wrpc_binding.rs verify + REQ-WRPC-BINDING-003: when a cross-processor connection HAS an + Actual_Connection_Binding, the analysis resolves the binding's + `reference (...)` target and warns ONLY when it resolves + UNAMBIGUOUSLY to a non-bus component. (a) binding to a processor + (non-bus) warns "not a bus"; (b) binding to a real bus does NOT warn; + (c) binding to a virtual bus does NOT warn; (d) an unresolvable + reference does NOT warn (the sound rule — no new false-positive); (e) + a dotted / multi-level path or a multi-reference binding list does NOT + warn (ambiguous → accept); (f) extract_simple_reference_name parses + `reference (x)` and `(reference (x))`, rejecting empty, dotted, and + multi-reference values. The presence-only REQ-WRPC-BINDING-002 path + (TEST-WRPC-BINDING) is unchanged and still green. + fields: + method: automated-test + steps: + - run: "cargo test -p spar-analysis --lib -- wrpc_binding" + status: passing + tags: [wrpc, binding, analysis] + links: + - type: satisfies + target: REQ-WRPC-BINDING-003 + # ── CI / Verification gate ────────────────────────────────────────────── - id: TEST-VERIFY-GATE-RUNNER diff --git a/crates/spar-analysis/src/wrpc_binding.rs b/crates/spar-analysis/src/wrpc_binding.rs index 74bd0af..7f19121 100644 --- a/crates/spar-analysis/src/wrpc_binding.rs +++ b/crates/spar-analysis/src/wrpc_binding.rs @@ -98,16 +98,18 @@ impl Analysis for WrpcBindingAnalysis { // `bus` — not mere presence — is a tracked follow-up.) let conn_props = instance.properties_for_connection(conn_idx); let owner_props = instance.properties_for(owner); - let has_conn_binding = conn_props + // Capture the binding VALUE (not just presence) — prefer the + // per-connection property map (the #281 `applies to ` idiom), + // then the owning component's flat map. + let binding_value = conn_props .get("Deployment_Properties", "Actual_Connection_Binding") - .is_some() - || conn_props.get("", "Actual_Connection_Binding").is_some() - || owner_props - .get("Deployment_Properties", "Actual_Connection_Binding") - .is_some() - || owner_props.get("", "Actual_Connection_Binding").is_some(); - - if !has_conn_binding { + .or_else(|| conn_props.get("", "Actual_Connection_Binding")) + .or_else(|| owner_props.get("Deployment_Properties", "Actual_Connection_Binding")) + .or_else(|| owner_props.get("", "Actual_Connection_Binding")); + + let Some(binding_value) = binding_value else { + // REQ-WRPC-BINDING-002: no binding at all on a cross-processor + // connection → warn (missing transport). let path = component_path(instance, owner); diagnostics.push(AnalysisDiagnostic { severity: Severity::Warning, @@ -123,6 +125,29 @@ impl Analysis for WrpcBindingAnalysis { path, analysis: "wrpc-binding".to_string(), }); + continue; + }; + + // REQ-WRPC-BINDING-003: the binding is present — verify its + // `reference (...)` target is a bus / virtual bus. Warn ONLY when + // the reference resolves UNAMBIGUOUSLY to a non-bus component; + // accept a bus, an unresolvable name, a dotted/multi-level path, or + // a multi-reference list (the sound rule that avoids new + // false-positives, per the requirement). + if let Some(target) = extract_simple_reference_name(binding_value) + && let Some(category) = unambiguous_non_bus_category(instance, &target) + { + let path = component_path(instance, owner); + diagnostics.push(AnalysisDiagnostic { + severity: Severity::Warning, + message: format!( + "connection '{}' in '{}' is bound via Actual_Connection_Binding \ + to '{}', which is a {} — not a bus or virtual bus", + conn.name, owner_comp.name, target, category, + ), + path, + analysis: "wrpc-binding".to_string(), + }); } } @@ -165,6 +190,51 @@ fn get_processor_binding(instance: &SystemInstance, idx: ComponentInstanceIdx) - None } +/// Extract the simple referenced component name from an +/// `Actual_Connection_Binding` value of the form `reference (name)` or +/// `(reference (name))`. Returns `None` for empty, dotted/multi-level, or +/// multi-reference values — the sound rule (REQ-WRPC-BINDING-003) accepts +/// those rather than risk a false positive on a path the resolver cannot +/// unambiguously follow. +fn extract_simple_reference_name(value: &str) -> Option { + // Split on the `reference` keyword (no manual index arithmetic). The text + // before the first `reference` is discarded (handles the outer-paren + // `(reference (x))` form); the text after holds the parenthesised target. + let mut parts = value.split("reference"); + let _before = parts.next()?; + let after = parts.next()?; + // A second `reference` means a binding LIST (`reference (a), reference (b)`) + // — ambiguous, accept (do not warn). + if parts.next().is_some() { + return None; + } + let inner = after.split_once('(')?.1; + let name = inner.split_once(')')?.0.trim(); + if name.is_empty() || name.contains('.') || name.contains(',') { + return None; + } + Some(name.to_string()) +} + +/// If `name` resolves to EXACTLY ONE component and that component is not a +/// `bus` / `virtual bus`, return its category (for the diagnostic). A bus, +/// zero matches, or multiple matches all return `None` — accept, no warning. +fn unambiguous_non_bus_category( + instance: &SystemInstance, + name: &str, +) -> Option { + let mut matches = instance + .all_components() + .filter(|(_, c)| c.name.as_str().eq_ignore_ascii_case(name)); + match (matches.next(), matches.next()) { + (Some((_, comp)), None) => match comp.category { + ComponentCategory::Bus | ComponentCategory::VirtualBus => None, + other => Some(other), + }, + _ => None, + } +} + #[cfg(test)] mod tests { use super::*; @@ -649,4 +719,116 @@ mod tests { diags ); } + + // ---- REQ-WRPC-BINDING-003: bus-target verification ---- + + /// Build a 2-processor model with `sender`→`receiver` crossing the + /// boundary, plus any extra children, returning the builder ready for a + /// connection + `Actual_Connection_Binding`. + fn two_proc_base() -> (TestBuilder, ComponentInstanceIdx) { + let mut b = TestBuilder::new(); + let root = b.add_component("top", ComponentCategory::System, None); + let cpu1 = b.add_component("cpu1", ComponentCategory::Processor, Some(root)); + let cpu2 = b.add_component("cpu2", ComponentCategory::Processor, Some(root)); + let can_bus = b.add_component("can_bus", ComponentCategory::Bus, Some(root)); + let vbus = b.add_component("ip_vbus", ComponentCategory::VirtualBus, Some(root)); + let sender = b.add_component("sender", ComponentCategory::Process, Some(root)); + let receiver = b.add_component("receiver", ComponentCategory::Process, Some(root)); + b.set_children(root, vec![cpu1, cpu2, can_bus, vbus, sender, receiver]); + b.set_property( + sender, + "Deployment_Properties", + "Actual_Processor_Binding", + "reference (cpu1)", + ); + b.set_property( + receiver, + "Deployment_Properties", + "Actual_Processor_Binding", + "reference (cpu2)", + ); + b.add_connection("c1", root, "sender", "out_port", "receiver", "in_port"); + (b, root) + } + + fn analyze_with_binding(value: &str) -> Vec { + let (mut b, root) = two_proc_base(); + b.set_property( + root, + "Deployment_Properties", + "Actual_Connection_Binding", + value, + ); + let inst = b.build(root); + WrpcBindingAnalysis.analyze(&inst) + } + + #[test] + fn binding_to_non_bus_component_warns() { + // Bound, but the reference resolves to a PROCESSOR — not a bus. + let diags = analyze_with_binding("reference (cpu1)"); + assert_eq!(diags.len(), 1, "non-bus target must warn: {diags:?}"); + assert!( + diags[0].message.contains("not a bus") && diags[0].message.contains("cpu1"), + "{}", + diags[0].message + ); + } + + #[test] + fn binding_to_real_bus_does_not_warn() { + assert!( + analyze_with_binding("reference (can_bus)").is_empty(), + "a real bus target must not warn", + ); + } + + #[test] + fn binding_to_virtual_bus_does_not_warn() { + assert!( + analyze_with_binding("reference (ip_vbus)").is_empty(), + "a virtual-bus target must not warn", + ); + } + + #[test] + fn binding_to_unresolvable_reference_does_not_warn() { + // The sound rule: an unresolvable name is accepted, not warned. + assert!( + analyze_with_binding("reference (ghost_bus)").is_empty(), + "an unresolvable reference must not warn", + ); + } + + #[test] + fn binding_with_dotted_or_multi_reference_does_not_warn() { + // Dotted/multi-level path the resolver cannot follow → accept. + assert!( + analyze_with_binding("reference (top.cpu1)").is_empty(), + "a dotted reference must not warn", + ); + // A binding LIST is ambiguous → accept (even though cpu1 is non-bus). + assert!( + analyze_with_binding("reference (cpu1), reference (can_bus)").is_empty(), + "a multi-reference binding list must not warn", + ); + } + + #[test] + fn reference_name_extraction_is_conservative() { + assert_eq!( + extract_simple_reference_name("reference (bus1)").as_deref(), + Some("bus1"), + ); + assert_eq!( + extract_simple_reference_name("(reference (bus1))").as_deref(), + Some("bus1"), + ); + assert_eq!(extract_simple_reference_name("reference (sys.bus1)"), None); + assert_eq!( + extract_simple_reference_name("reference (a), reference (b)"), + None, + ); + assert_eq!(extract_simple_reference_name("bus1"), None); + } }