diff --git a/Cargo.lock b/Cargo.lock index 81b7f4a7..4b74a498 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1483,6 +1483,7 @@ dependencies = [ "salsa", "serde", "smol_str", + "spar-annex", "spar-base-db", "spar-syntax", ] diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 1b5846c2..6381c7af 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -2266,10 +2266,12 @@ artifacts: LAYER STATUS (4-PR foundation, user-directed v0.23.0 headline 2026-07-01): L1 (semantic EMV2 model in spar-annex — Emv2Model lifting the CST into typed propagations/flows) LANDED, verified by - TEST-EMV2-SEMANTIC-MODEL; L2 (item-tree attach), L3 (instance - projection), L4 (overlay populate + analyze-path wiring + end-to-end - > 0-chains oracle) remain. Requirement flips proposed → implemented when - L4 closes the end-to-end oracle. + TEST-EMV2-SEMANTIC-MODEL; L2 (item-tree attach — the component's EMV2 + subclause is retained in an emv2_subclauses arena, referenced from + ComponentType/ImplItem.emv2) LANDED, verified by + TEST-EMV2-ITEMTREE-ATTACH; L3 (instance projection), L4 (overlay populate + + analyze-path wiring + end-to-end > 0-chains oracle) remain. Requirement + flips proposed → implemented when L4 closes the end-to-end oracle. status: proposed tags: [emv2, analysis, safety, hir-def, capability] fields: diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index cb070283..7c058089 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -3468,6 +3468,36 @@ artifacts: - type: verifies target: REQ-EMV2-PROPAGATION-002 + - id: TEST-EMV2-ITEMTREE-ATTACH + type: feature + title: EMV2 subclause retained in the item-tree, attached to its component + description: > + Layer 2 of REQ-EMV2-PROPAGATION-002 (GitHub #294): a component's + `annex EMV2 {** … **}` subclause is no longer dropped at item-tree + lowering (previously the empty ANNEX_SUBCLAUSE arm) — it is lifted via the + L1 Emv2Model and stored in a new `emv2_subclauses` arena, referenced from + `ComponentTypeItem.emv2` / `ComponentImplItem.emv2` + (crates/spar-hir-def/src/item_tree). Oracle tests in spar-hir-def + (parse real AADL → item-tree → assert, NON-CIRCULAR by comparing the + lowered model against L1 parsing the same snippet directly): (a) a system + TYPE with an EMV2 annex retains exactly one subclause whose model EQUALS + the L1 oracle (2 propagations, 3 flows — non-vacuous); (b) a system + IMPLEMENTATION with an EMV2 annex retains it on its own `emv2` list; + (c) a component with an EMV2 annex AND a non-EMV2 annex + (behavior_specification) retains EXACTLY the EMV2 one (guards the + case-insensitive name filter; annex subclauses repeat, so lowering + filters rather than finds). Stops at the item-tree/type level — does NOT + touch instantiation (that is layer 3). + fields: + method: automated-test + steps: + - run: cargo test -p spar-hir-def --lib emv2 + status: passing + tags: [emv2, analysis, safety, v0.23.0, hir-def] + links: + - type: verifies + target: REQ-EMV2-PROPAGATION-002 + - id: TEST-WRPC-BINDING type: feature title: wrpc-binding honors per-connection Actual_Connection_Binding diff --git a/crates/spar-analysis/src/category_check.rs b/crates/spar-analysis/src/category_check.rs index 7bad50fe..33a60ab7 100644 --- a/crates/spar-analysis/src/category_check.rs +++ b/crates/spar-analysis/src/category_check.rs @@ -86,6 +86,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree } @@ -120,6 +121,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree } diff --git a/crates/spar-analysis/src/extends_rules.rs b/crates/spar-analysis/src/extends_rules.rs index 65f47d94..7860ff36 100644 --- a/crates/spar-analysis/src/extends_rules.rs +++ b/crates/spar-analysis/src/extends_rules.rs @@ -302,6 +302,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ext_ct = tree.component_types.alloc(ComponentTypeItem { @@ -316,6 +317,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -433,6 +435,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ext_ct = tree.component_types.alloc(ComponentTypeItem { @@ -447,6 +450,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -510,6 +514,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ext_ct = tree.component_types.alloc(ComponentTypeItem { @@ -524,6 +529,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -588,6 +594,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ext_ct = tree.component_types.alloc(ComponentTypeItem { @@ -602,6 +609,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -645,6 +653,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -692,6 +701,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -734,6 +744,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -774,6 +785,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ci_idx = tree.component_impls.alloc(ComponentImplItem { @@ -792,6 +804,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -833,6 +846,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ci_idx = tree.component_impls.alloc(ComponentImplItem { @@ -851,6 +865,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -893,6 +908,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -933,6 +949,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -977,6 +994,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -1039,6 +1057,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ext_ct = tree.component_types.alloc(ComponentTypeItem { @@ -1053,6 +1072,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -1096,6 +1116,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-analysis/src/legality.rs b/crates/spar-analysis/src/legality.rs index b096dc90..c3326a0c 100644 --- a/crates/spar-analysis/src/legality.rs +++ b/crates/spar-analysis/src/legality.rs @@ -587,6 +587,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ci_idx = tree.component_impls.alloc(ComponentImplItem { @@ -605,6 +606,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -736,6 +738,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -843,6 +846,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -990,6 +994,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("Pkg"), @@ -1461,6 +1466,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -1545,6 +1551,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); let ci_idx = tree.component_impls.alloc(ComponentImplItem { @@ -1563,6 +1570,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -1612,6 +1620,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-analysis/src/naming_rules.rs b/crates/spar-analysis/src/naming_rules.rs index d6b71463..84c65338 100644 --- a/crates/spar-analysis/src/naming_rules.rs +++ b/crates/spar-analysis/src/naming_rules.rs @@ -325,6 +325,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -379,6 +380,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -504,6 +506,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -552,6 +555,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -598,6 +602,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -832,6 +837,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); // Subcomponents @@ -882,6 +888,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); // Property set with unique names @@ -1004,6 +1011,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-hir-def/Cargo.toml b/crates/spar-hir-def/Cargo.toml index 632fe05a..5cd851ae 100644 --- a/crates/spar-hir-def/Cargo.toml +++ b/crates/spar-hir-def/Cargo.toml @@ -9,6 +9,7 @@ description = "HIR definitions and name resolution for AADL analysis" [dependencies] spar-syntax.workspace = true spar-base-db.workspace = true +spar-annex.workspace = true salsa.workspace = true rowan.workspace = true la-arena = "0.3" diff --git a/crates/spar-hir-def/src/instance.rs b/crates/spar-hir-def/src/instance.rs index 23c2626e..79ce51e7 100644 --- a/crates/spar-hir-def/src/instance.rs +++ b/crates/spar-hir-def/src/instance.rs @@ -3180,6 +3180,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Type B @@ -3195,6 +3196,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Subcomponent in A.Impl: b : system B.Impl @@ -3244,6 +3246,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Impl B.Impl @@ -3263,6 +3266,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Package @@ -3320,6 +3324,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let b_type_idx = tree.component_types.alloc(ComponentTypeItem { @@ -3334,6 +3339,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let _c_type_idx = tree.component_types.alloc(ComponentTypeItem { @@ -3348,6 +3354,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // B.Impl has subcomponent c: process C (type-only, no impl -> no recursion) @@ -3377,6 +3384,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // A.Impl has subcomponent b: system B.Impl @@ -3410,6 +3418,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -3460,6 +3469,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let b_type_idx = tree.component_types.alloc(ComponentTypeItem { @@ -3474,6 +3484,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let sub_b = tree.subcomponents.alloc(SubcomponentItem { @@ -3520,6 +3531,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let b_impl_idx = tree.component_impls.alloc(ComponentImplItem { @@ -3538,6 +3550,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -3607,6 +3620,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let _b_type_idx = tree.component_types.alloc(ComponentTypeItem { @@ -3621,6 +3635,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let sub_b = tree.subcomponents.alloc(SubcomponentItem { @@ -3649,6 +3664,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -3703,6 +3719,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let a_impl_idx = tree.component_impls.alloc(ComponentImplItem { @@ -3721,6 +3738,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-hir-def/src/item_tree/lower.rs b/crates/spar-hir-def/src/item_tree/lower.rs index 608b030a..9d7d39fd 100644 --- a/crates/spar-hir-def/src/item_tree/lower.rs +++ b/crates/spar-hir-def/src/item_tree/lower.rs @@ -6,9 +6,40 @@ use spar_syntax::ast::{self, AstNode}; use spar_syntax::{SyntaxKind, SyntaxNode, SyntaxToken}; +use spar_annex::emv2::Emv2Model; + use crate::item_tree::*; use crate::name::{ClassifierRef, Name, PropertyRef}; +/// Lift EMV2 annex subclauses that are direct children of a component +/// type/impl node into the item tree, returning their arena indices. +/// +/// Non-EMV2 annex languages remain dropped (only their diagnostics apply +/// elsewhere). REQ-EMV2-PROPAGATION-002, layer 2, GitHub #294. +fn lower_emv2_subclauses(node: &SyntaxNode, tree: &mut ItemTree) -> Vec { + let mut out = Vec::new(); + for sub in node + .children() + .filter(|c| c.kind() == SyntaxKind::ANNEX_SUBCLAUSE) + { + let Some((name, text)) = spar_annex::extract_annex_content(&sub) else { + continue; + }; + // Other annex languages stay dropped. + if !name.eq_ignore_ascii_case("EMV2") { + continue; + } + let parsed = spar_annex::emv2::parse(&text); + let model = Emv2Model::from_syntax(&parsed.syntax_node()); + let idx = tree.emv2_subclauses.alloc(Emv2Subclause { + name: Name::new(&name), + model, + }); + out.push(idx); + } + out +} + /// Lower a parsed source file into an item tree. pub fn lower_file(root: &SyntaxNode) -> ItemTree { let mut tree = ItemTree::default(); @@ -237,6 +268,8 @@ fn lower_component_type_with_visibility( .find(|c| c.kind() == SyntaxKind::MODE_SECTION) .is_some_and(|ms| has_requires_modes_prefix(&ms)); + let emv2 = lower_emv2_subclauses(node, tree); + let idx = tree.component_types.alloc(ComponentTypeItem { name, category, @@ -249,6 +282,7 @@ fn lower_component_type_with_visibility( prototypes, property_associations, requires_modes, + emv2, }); Some(ItemRef::ComponentType(idx)) } @@ -337,6 +371,8 @@ fn lower_component_impl_with_visibility( .find(|c| c.kind() == SyntaxKind::MODE_SECTION) .is_some_and(|ms| has_requires_modes_prefix(&ms)); + let emv2 = lower_emv2_subclauses(node, tree); + let idx = tree.component_impls.alloc(ComponentImplItem { type_name, impl_name, @@ -353,6 +389,7 @@ fn lower_component_impl_with_visibility( call_sequences, property_associations, requires_modes, + emv2, }); Some(ItemRef::ComponentImpl(idx)) } diff --git a/crates/spar-hir-def/src/item_tree/mod.rs b/crates/spar-hir-def/src/item_tree/mod.rs index 4d5e6f37..e0c6ac13 100644 --- a/crates/spar-hir-def/src/item_tree/mod.rs +++ b/crates/spar-hir-def/src/item_tree/mod.rs @@ -12,6 +12,7 @@ pub mod lower; use la_arena::{Arena, Idx}; use serde::{Deserialize, Serialize}; +use spar_annex::emv2::Emv2Model; use crate::name::{ClassifierRef, Name, PropertyRef}; @@ -36,6 +37,7 @@ pub type FlowImplIdx = Idx; pub type CallSequenceIdx = Idx; pub type SubprogramCallIdx = Idx; pub type RenamesIdx = Idx; +pub type Emv2SubclauseIdx = Idx; // ── Lowering diagnostics ────────────────────────────────────────── @@ -80,10 +82,21 @@ pub struct ItemTree { pub call_sequences: Arena, pub subprogram_calls: Arena, pub renames: Arena, + pub emv2_subclauses: Arena, /// Diagnostics produced during lowering (STPA-REQ-002, STPA-REQ-004). pub diagnostics: Vec, } +/// An `annex EMV2 {** … **}` subclause attached to a component type or +/// implementation (REQ-EMV2-PROPAGATION-002, layer 2, GitHub #294). +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Emv2Subclause { + /// Annex name as written (provenance). + pub name: Name, + /// The L1 semantic model lifted from the subclause body. + pub model: Emv2Model, +} + // ── Top-level items ──────────────────────────────────────────────── /// AADL component category. @@ -175,6 +188,8 @@ pub struct ComponentTypeItem { /// Whether the modes section uses `requires modes` (derived modes) /// rather than declaring its own modes. pub requires_modes: bool, + /// EMV2 annex subclauses attached to this component type. + pub emv2: Vec, } /// A component implementation declaration. @@ -207,6 +222,8 @@ pub struct ComponentImplItem { /// Whether the modes section uses `requires modes` (derived modes) /// rather than declaring its own modes. pub requires_modes: bool, + /// EMV2 annex subclauses attached to this component implementation. + pub emv2: Vec, } /// A feature group type declaration. diff --git a/crates/spar-hir-def/src/lib.rs b/crates/spar-hir-def/src/lib.rs index 275de66f..314092c0 100644 --- a/crates/spar-hir-def/src/lib.rs +++ b/crates/spar-hir-def/src/lib.rs @@ -199,6 +199,92 @@ end P; assert_eq!(fgt.features.len(), 2); } + // ── EMV2 subclause retention (REQ-EMV2-PROPAGATION-002, layer 2) ────── + // + // Verbatim `error propagations` body from the bundled OSATE corpus + // (test-data/interop/osate-examples/LargeExamplesforEMV2TR/ + // network_protocol_pkg.aadl) — the same block L1's spar-annex tests pin. + const EMV2_SNIPPET: &str = r#"error propagations + bindings: out propagation {LateDelivery, ValueCorruption}; + connection: in propagation {LostMessage, ValueCorruption}; +flows + RetryTiming: error source bindings {LateDelivery}; + MaskLoss: error sink connection {LostMessage}; + PassCorruption: error path connection {ValueCorruption} -> bindings; +end propagations;"#; + + /// Independent oracle: L1 parsing the bare snippet directly. If L2's + /// lowering drops/mangles the subclause, the item-tree model diverges. + fn emv2_oracle_model() -> spar_annex::emv2::Emv2Model { + let parsed = spar_annex::emv2::parse(EMV2_SNIPPET); + spar_annex::emv2::Emv2Model::from_syntax(&parsed.syntax_node()) + } + + #[test] + fn item_tree_retains_component_emv2_subclause() { + let db = make_db(); + let src = format!( + "package P\npublic\n system S\n annex EMV2 {{**\n{EMV2_SNIPPET}\n **}};\n end S;\nend P;\n" + ); + let file = spar_base_db::SourceFile::new(&db, "emv2.aadl".to_string(), src); + let tree = file_item_tree(&db, file); + + assert_eq!(tree.component_types.len(), 1); + let ct = &tree.component_types[tree.component_types.iter().next().unwrap().0]; + assert_eq!( + ct.emv2.len(), + 1, + "the component's EMV2 subclause must be retained" + ); + let sub = &tree.emv2_subclauses[ct.emv2[0]]; + assert!(sub.name.as_str().eq_ignore_ascii_case("EMV2")); + // The lowered model must EQUAL the independently-parsed L1 oracle. + assert_eq!(sub.model, emv2_oracle_model()); + // Spot-check it is non-empty (2 propagations, 3 flows) so an empty + // model can't vacuously pass. + assert_eq!(sub.model.propagations.len(), 2); + assert_eq!(sub.model.flows.len(), 3); + } + + #[test] + fn item_tree_retains_impl_emv2_subclause() { + let db = make_db(); + let src = format!( + "package P\npublic\n system S\n end S;\n system implementation S.i\n annex EMV2 {{**\n{EMV2_SNIPPET}\n **}};\n end S.i;\nend P;\n" + ); + let file = spar_base_db::SourceFile::new(&db, "emv2impl.aadl".to_string(), src); + let tree = file_item_tree(&db, file); + + assert_eq!(tree.component_impls.len(), 1); + let ci = &tree.component_impls[tree.component_impls.iter().next().unwrap().0]; + assert_eq!( + ci.emv2.len(), + 1, + "the implementation's EMV2 subclause must be retained" + ); + assert_eq!(tree.emv2_subclauses[ci.emv2[0]].model, emv2_oracle_model()); + } + + #[test] + fn item_tree_emv2_filter_drops_non_emv2_annex() { + // A component with an EMV2 annex AND a non-EMV2 annex retains exactly + // the EMV2 one (guards the case-insensitive name filter). + let db = make_db(); + let src = format!( + "package P\npublic\n system S\n annex EMV2 {{**\n{EMV2_SNIPPET}\n **}};\n annex behavior_specification {{** **}};\n end S;\nend P;\n" + ); + let file = spar_base_db::SourceFile::new(&db, "mixed.aadl".to_string(), src); + let tree = file_item_tree(&db, file); + + let ct = &tree.component_types[tree.component_types.iter().next().unwrap().0]; + assert_eq!( + ct.emv2.len(), + 1, + "only the EMV2 annex is retained, not behavior_specification" + ); + assert_eq!(tree.emv2_subclauses.len(), 1); + } + #[test] fn item_tree_connections() { let db = make_db(); diff --git a/crates/spar-hir-def/src/resolver.rs b/crates/spar-hir-def/src/resolver.rs index de1cd3a5..127e0205 100644 --- a/crates/spar-hir-def/src/resolver.rs +++ b/crates/spar-hir-def/src/resolver.rs @@ -692,6 +692,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -713,6 +714,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("B"), @@ -762,6 +764,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -783,6 +786,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("B"), @@ -830,6 +834,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("C"), @@ -851,6 +856,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -893,6 +899,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree1.packages.alloc(Package { name: Name::new("Foo"), @@ -915,6 +922,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree2.packages.alloc(Package { name: Name::new("Foo"), @@ -986,6 +994,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Public type in the same package to verify selective visibility let ct_public = tree.component_types.alloc(ComponentTypeItem { @@ -1000,6 +1009,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -1066,6 +1076,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("Pkg1"), @@ -1125,6 +1136,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -1185,6 +1197,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); let ci = tree.component_impls.alloc(ComponentImplItem { type_name: Name::new("OriginalSensor"), @@ -1202,6 +1215,7 @@ mod tests { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("A"), @@ -1311,6 +1325,7 @@ mod tests { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { name: Name::new("Lib"), diff --git a/crates/spar-sysml2/src/lower.rs b/crates/spar-sysml2/src/lower.rs index 641afc86..05f3def1 100644 --- a/crates/spar-sysml2/src/lower.rs +++ b/crates/spar-sysml2/src/lower.rs @@ -368,6 +368,7 @@ fn lower_part_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: property_associations.clone(), requires_modes: false, + emv2: Vec::new(), }); if !subcomponents.is_empty() || !connections.is_empty() { @@ -387,6 +388,7 @@ fn lower_part_def(node: &SyntaxNode, ctx: &mut LowerCtx) { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -446,6 +448,7 @@ fn lower_port_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -468,6 +471,7 @@ fn lower_connection_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -493,6 +497,7 @@ fn lower_action_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -519,6 +524,7 @@ fn lower_state_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -544,6 +550,7 @@ fn lower_attribute_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -569,6 +576,7 @@ fn lower_item_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -633,6 +641,7 @@ fn lower_enum_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations, requires_modes: false, + emv2: Vec::new(), }); } @@ -739,6 +748,7 @@ fn lower_requirement_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations, requires_modes: false, + emv2: Vec::new(), }); } @@ -777,6 +787,7 @@ fn lower_constraint_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations, requires_modes: false, + emv2: Vec::new(), }); } @@ -802,6 +813,7 @@ fn lower_calc_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } @@ -827,6 +839,7 @@ fn lower_allocation_def(node: &SyntaxNode, ctx: &mut LowerCtx) { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); } diff --git a/crates/spar-transform/src/protocol_library.rs b/crates/spar-transform/src/protocol_library.rs index 052d7027..258c831b 100644 --- a/crates/spar-transform/src/protocol_library.rs +++ b/crates/spar-transform/src/protocol_library.rs @@ -196,6 +196,7 @@ pub fn protocol_library() -> ItemTree { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); public_items.push(ItemRef::ComponentType(ct_idx)); } diff --git a/crates/spar-transform/src/rust_crate.rs b/crates/spar-transform/src/rust_crate.rs index bee29e99..92f9fe15 100644 --- a/crates/spar-transform/src/rust_crate.rs +++ b/crates/spar-transform/src/rust_crate.rs @@ -150,6 +150,7 @@ fn lower_metadata(metadata: &CargoMetadata) -> ItemTree { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); public_items.push(ItemRef::ComponentType(ct_idx)); } @@ -201,6 +202,7 @@ fn lower_metadata(metadata: &CargoMetadata) -> ItemTree { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); // Create subcomponents for each crate in the implementation @@ -257,6 +259,7 @@ fn lower_metadata(metadata: &CargoMetadata) -> ItemTree { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-transform/src/wac.rs b/crates/spar-transform/src/wac.rs index 3f59ee75..e12b7f08 100644 --- a/crates/spar-transform/src/wac.rs +++ b/crates/spar-transform/src/wac.rs @@ -145,6 +145,7 @@ fn lower_wac(doc: &WacDocument) -> ItemTree { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); public_items.push(ItemRef::ComponentType(sys_type_idx)); @@ -230,6 +231,7 @@ fn lower_wac(doc: &WacDocument) -> ItemTree { call_sequences: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); public_items.push(ItemRef::ComponentImpl(impl_idx)); diff --git a/crates/spar-transform/src/wit.rs b/crates/spar-transform/src/wit.rs index 809918d6..3ba74cc3 100644 --- a/crates/spar-transform/src/wit.rs +++ b/crates/spar-transform/src/wit.rs @@ -273,6 +273,7 @@ fn lower_interface(iface: &WitInterface, tree: &mut ItemTree) -> Vec { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); items.push(ItemRef::ComponentType(sg_idx)); @@ -329,6 +330,7 @@ fn lower_function( property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }) } @@ -398,6 +400,7 @@ fn lower_async_function( property_associations: vec![dispatch_prop_idx], is_public: true, requires_modes: false, + emv2: Vec::new(), }) } @@ -546,6 +549,7 @@ fn lower_world(world: &WitWorld, tree: &mut ItemTree) -> ItemRef { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); ItemRef::ComponentType(ct_idx) } @@ -582,6 +586,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -635,6 +640,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: vec![prop_idx, enum_prop_idx], is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -668,6 +674,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -721,6 +728,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: vec![prop_idx, flags_prop_idx], is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -740,6 +748,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -758,6 +767,7 @@ fn lower_type_def(typedef: &WitTypeDef, tree: &mut ItemTree) -> Option property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); Some(ItemRef::ComponentType(ct_idx)) } @@ -1359,6 +1369,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { @@ -1410,6 +1421,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); // Create a subprogram group type with a feature referencing the subprogram @@ -1436,6 +1448,7 @@ mod tests { property_associations: Vec::new(), is_public: true, requires_modes: false, + emv2: Vec::new(), }); tree.packages.alloc(Package { diff --git a/crates/spar-transform/src/wrpc.rs b/crates/spar-transform/src/wrpc.rs index 648f639e..611b62dd 100644 --- a/crates/spar-transform/src/wrpc.rs +++ b/crates/spar-transform/src/wrpc.rs @@ -48,6 +48,7 @@ pub fn wrpc_standard_library() -> ItemTree { prototypes: Vec::new(), property_associations: Vec::new(), requires_modes: false, + emv2: Vec::new(), }); public_items.push(ItemRef::ComponentType(ct_idx)); }