diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 6381c7af..8d38f4e6 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -2269,9 +2269,13 @@ artifacts: 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. + TEST-EMV2-ITEMTREE-ATTACH; L3 (instance projection — the classifier's + EMV2 model is projected onto each ComponentInstance at instantiation, + stored as a SystemInstance emv2_models side-table with an emv2_for + accessor) LANDED, verified by TEST-EMV2-INSTANCE-PROJECT; L4 (overlay + populate + analyze-path wiring + end-to-end > 0-chains oracle) remains. + 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 7c058089..c8a66497 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -3498,6 +3498,40 @@ artifacts: - type: verifies target: REQ-EMV2-PROPAGATION-002 + - id: TEST-EMV2-INSTANCE-PROJECT + type: feature + title: EMV2 model projected onto ComponentInstances during instantiation + description: > + Layer 3 of REQ-EMV2-PROPAGATION-002 (GitHub #294): during + instantiation the retained EMV2 model (L2) is projected from each + component's classifier (type ∪ impl, direct only) onto the + ComponentInstance, stored as a SystemInstance side-table + `emv2_models: FxHashMap>` (keyed by + instance so L4 can build the Emv2Overlay without re-reading the item-tree, + which is unreachable post-instantiation) with an `emv2_for(idx)` + accessor. Deliberate side-table (not a ComponentInstance field) to avoid + breaking ~103 constructors; extends-chain EMV2 inheritance deferred. + Oracle tests in spar-hir-def (full pipeline: hand-authored AADL → + item-tree → instantiate → assert, NON-VACUOUS exact counts, since a bare + `== item-tree model` would only prove the copy ran): (a) EMV2 on the TYPE, + root instance is the IMPLEMENTATION — root carries it (2 propagations + + 1 flow), exercising the main alloc path's type∪impl union; (b) a type-only + leaf subcomponent (`sub : device Sensor` with an EMV2 annex) carries the + device type's model (1 propagation + 1 flow) while the EMV2-less root is + empty — exercising the distinct leaf alloc site a main-path-only + projection would miss; (c) no annex ⇒ empty projection. Stops at + instance projection — does NOT build the Emv2Overlay or wire analysis + passes (that is layer 4). + 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/ai_ml/tests.rs b/crates/spar-analysis/src/ai_ml/tests.rs index d51664ad..2c0b8de8 100644 --- a/crates/spar-analysis/src/ai_ml/tests.rs +++ b/crates/spar-analysis/src/ai_ml/tests.rs @@ -91,6 +91,7 @@ fn single_component_instance(category: ComponentCategory, props: PropertyMap) -> property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/arinc653.rs b/crates/spar-analysis/src/arinc653.rs index b21b3558..c78f6765 100644 --- a/crates/spar-analysis/src/arinc653.rs +++ b/crates/spar-analysis/src/arinc653.rs @@ -549,6 +549,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/binding_check.rs b/crates/spar-analysis/src/binding_check.rs index e61fb32d..3d668e6c 100644 --- a/crates/spar-analysis/src/binding_check.rs +++ b/crates/spar-analysis/src/binding_check.rs @@ -304,6 +304,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/binding_rules.rs b/crates/spar-analysis/src/binding_rules.rs index 6a003c21..4e4bcb01 100644 --- a/crates/spar-analysis/src/binding_rules.rs +++ b/crates/spar-analysis/src/binding_rules.rs @@ -277,6 +277,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/bus_bandwidth.rs b/crates/spar-analysis/src/bus_bandwidth.rs index 0142cfb7..7749d225 100644 --- a/crates/spar-analysis/src/bus_bandwidth.rs +++ b/crates/spar-analysis/src/bus_bandwidth.rs @@ -577,6 +577,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -1328,6 +1329,7 @@ mod tests { property_maps: b.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: vec![som], } @@ -1380,6 +1382,7 @@ mod tests { property_maps: b.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: vec![som], } diff --git a/crates/spar-analysis/src/classifier_match.rs b/crates/spar-analysis/src/classifier_match.rs index cac89c9c..540bf82b 100644 --- a/crates/spar-analysis/src/classifier_match.rs +++ b/crates/spar-analysis/src/classifier_match.rs @@ -445,6 +445,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/completeness.rs b/crates/spar-analysis/src/completeness.rs index 353b9d6b..a1454055 100644 --- a/crates/spar-analysis/src/completeness.rs +++ b/crates/spar-analysis/src/completeness.rs @@ -226,6 +226,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/connection_rules.rs b/crates/spar-analysis/src/connection_rules.rs index 86dc34d7..e5c1c71b 100644 --- a/crates/spar-analysis/src/connection_rules.rs +++ b/crates/spar-analysis/src/connection_rules.rs @@ -279,6 +279,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/connectivity.rs b/crates/spar-analysis/src/connectivity.rs index f00b2408..d45c20ff 100644 --- a/crates/spar-analysis/src/connectivity.rs +++ b/crates/spar-analysis/src/connectivity.rs @@ -524,6 +524,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/direction_rules.rs b/crates/spar-analysis/src/direction_rules.rs index e6bdf639..47a97acd 100644 --- a/crates/spar-analysis/src/direction_rules.rs +++ b/crates/spar-analysis/src/direction_rules.rs @@ -413,6 +413,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/emv2_analysis.rs b/crates/spar-analysis/src/emv2_analysis.rs index 46ccabbf..67492d5b 100644 --- a/crates/spar-analysis/src/emv2_analysis.rs +++ b/crates/spar-analysis/src/emv2_analysis.rs @@ -376,6 +376,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/emv2_propagation.rs b/crates/spar-analysis/src/emv2_propagation.rs index 81207f76..e55ba50b 100644 --- a/crates/spar-analysis/src/emv2_propagation.rs +++ b/crates/spar-analysis/src/emv2_propagation.rs @@ -538,6 +538,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: self.semantic_connections, system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/emv2_stpa_bridge.rs b/crates/spar-analysis/src/emv2_stpa_bridge.rs index 3c595ac4..a5ed2af9 100644 --- a/crates/spar-analysis/src/emv2_stpa_bridge.rs +++ b/crates/spar-analysis/src/emv2_stpa_bridge.rs @@ -531,6 +531,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/feature_group_check.rs b/crates/spar-analysis/src/feature_group_check.rs index e40e549b..7b4237cf 100644 --- a/crates/spar-analysis/src/feature_group_check.rs +++ b/crates/spar-analysis/src/feature_group_check.rs @@ -486,6 +486,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/flow_check.rs b/crates/spar-analysis/src/flow_check.rs index 956c1faf..303bcaf3 100644 --- a/crates/spar-analysis/src/flow_check.rs +++ b/crates/spar-analysis/src/flow_check.rs @@ -309,6 +309,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/flow_rules.rs b/crates/spar-analysis/src/flow_rules.rs index 89275479..8f018cac 100644 --- a/crates/spar-analysis/src/flow_rules.rs +++ b/crates/spar-analysis/src/flow_rules.rs @@ -510,6 +510,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/hierarchy.rs b/crates/spar-analysis/src/hierarchy.rs index ea11ef5d..d2e95dae 100644 --- a/crates/spar-analysis/src/hierarchy.rs +++ b/crates/spar-analysis/src/hierarchy.rs @@ -230,6 +230,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/latency.rs b/crates/spar-analysis/src/latency.rs index a458532e..a4f7197c 100644 --- a/crates/spar-analysis/src/latency.rs +++ b/crates/spar-analysis/src/latency.rs @@ -616,6 +616,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/legality.rs b/crates/spar-analysis/src/legality.rs index c3326a0c..54eb7466 100644 --- a/crates/spar-analysis/src/legality.rs +++ b/crates/spar-analysis/src/legality.rs @@ -547,6 +547,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/memory_budget.rs b/crates/spar-analysis/src/memory_budget.rs index 27298a38..cf642aba 100644 --- a/crates/spar-analysis/src/memory_budget.rs +++ b/crates/spar-analysis/src/memory_budget.rs @@ -250,6 +250,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/modal.rs b/crates/spar-analysis/src/modal.rs index 2aeb2501..face8095 100644 --- a/crates/spar-analysis/src/modal.rs +++ b/crates/spar-analysis/src/modal.rs @@ -159,6 +159,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: soms, } diff --git a/crates/spar-analysis/src/modal_rules.rs b/crates/spar-analysis/src/modal_rules.rs index 9eaba7cb..dbb90d68 100644 --- a/crates/spar-analysis/src/modal_rules.rs +++ b/crates/spar-analysis/src/modal_rules.rs @@ -335,6 +335,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/mode_check.rs b/crates/spar-analysis/src/mode_check.rs index a8589215..7df3b79c 100644 --- a/crates/spar-analysis/src/mode_check.rs +++ b/crates/spar-analysis/src/mode_check.rs @@ -291,6 +291,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/mode_reachability.rs b/crates/spar-analysis/src/mode_reachability.rs index 546f4691..1d5b463a 100644 --- a/crates/spar-analysis/src/mode_reachability.rs +++ b/crates/spar-analysis/src/mode_reachability.rs @@ -703,6 +703,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/mode_rules.rs b/crates/spar-analysis/src/mode_rules.rs index 8dd15869..67cb8f09 100644 --- a/crates/spar-analysis/src/mode_rules.rs +++ b/crates/spar-analysis/src/mode_rules.rs @@ -248,6 +248,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/property_rules.rs b/crates/spar-analysis/src/property_rules.rs index 00f20e00..b72bfe60 100644 --- a/crates/spar-analysis/src/property_rules.rs +++ b/crates/spar-analysis/src/property_rules.rs @@ -446,6 +446,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/regression_tests.rs b/crates/spar-analysis/src/regression_tests.rs index fc80c775..7627c592 100644 --- a/crates/spar-analysis/src/regression_tests.rs +++ b/crates/spar-analysis/src/regression_tests.rs @@ -121,6 +121,7 @@ impl TestInstanceBuilder { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/resource_budget.rs b/crates/spar-analysis/src/resource_budget.rs index 0f9a5825..c3f89b4d 100644 --- a/crates/spar-analysis/src/resource_budget.rs +++ b/crates/spar-analysis/src/resource_budget.rs @@ -372,6 +372,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/rta.rs b/crates/spar-analysis/src/rta.rs index a773ab73..bb09f3ff 100644 --- a/crates/spar-analysis/src/rta.rs +++ b/crates/spar-analysis/src/rta.rs @@ -738,6 +738,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/scheduling.rs b/crates/spar-analysis/src/scheduling.rs index aa6146fd..163eb138 100644 --- a/crates/spar-analysis/src/scheduling.rs +++ b/crates/spar-analysis/src/scheduling.rs @@ -626,6 +626,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/subcomponent_rules.rs b/crates/spar-analysis/src/subcomponent_rules.rs index 7aec5af9..fa5fee9a 100644 --- a/crates/spar-analysis/src/subcomponent_rules.rs +++ b/crates/spar-analysis/src/subcomponent_rules.rs @@ -240,6 +240,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/tests.rs b/crates/spar-analysis/src/tests.rs index 07309a41..2d44904a 100644 --- a/crates/spar-analysis/src/tests.rs +++ b/crates/spar-analysis/src/tests.rs @@ -174,6 +174,7 @@ impl TestInstanceBuilder { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-analysis/src/weight_power.rs b/crates/spar-analysis/src/weight_power.rs index 2449aa18..f147178d 100644 --- a/crates/spar-analysis/src/weight_power.rs +++ b/crates/spar-analysis/src/weight_power.rs @@ -544,6 +544,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -1244,6 +1245,7 @@ mod tests { property_maps: b.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: vec![som], } @@ -1323,6 +1325,7 @@ mod tests { property_maps: b.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: vec![som], } diff --git a/crates/spar-analysis/src/wrpc_binding.rs b/crates/spar-analysis/src/wrpc_binding.rs index 7f191218..a0996abb 100644 --- a/crates/spar-analysis/src/wrpc_binding.rs +++ b/crates/spar-analysis/src/wrpc_binding.rs @@ -381,6 +381,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: self.connection_property_maps, + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-cli/src/assertion/mod.rs b/crates/spar-cli/src/assertion/mod.rs index b03384e7..ae2ca67c 100644 --- a/crates/spar-cli/src/assertion/mod.rs +++ b/crates/spar-cli/src/assertion/mod.rs @@ -550,6 +550,7 @@ mod tests { property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -838,6 +839,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; diff --git a/crates/spar-cli/src/diff.rs b/crates/spar-cli/src/diff.rs index 77f50e32..21b2d92d 100644 --- a/crates/spar-cli/src/diff.rs +++ b/crates/spar-cli/src/diff.rs @@ -935,6 +935,7 @@ mod tests { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-hir-def/src/instance.rs b/crates/spar-hir-def/src/instance.rs index 79ce51e7..67741080 100644 --- a/crates/spar-hir-def/src/instance.rs +++ b/crates/spar-hir-def/src/instance.rs @@ -64,6 +64,11 @@ pub struct SystemInstance { /// Property maps for connection instances — values attached via /// `applies to .` (issue #237). pub connection_property_maps: FxHashMap, + /// EMV2 error-propagation models projected from each component's classifier + /// (type ∪ impl, DIRECT only — extends-chain EMV2 inheritance is deferred) + /// at instantiation time (REQ-EMV2-PROPAGATION-002 L3). Keyed by component + /// instance so L4 can build the Emv2Overlay without re-reading the item-tree. + pub emv2_models: FxHashMap>, /// Semantic (end-to-end) connection instances traced through the hierarchy. pub semantic_connections: Vec, /// System Operation Modes — the cartesian product of modes across all modal components. @@ -222,6 +227,7 @@ impl SystemInstance { property_maps: FxHashMap::default(), feature_property_maps: FxHashMap::default(), connection_property_maps: FxHashMap::default(), + emv2_models: FxHashMap::default(), pending_applies_to: Vec::new(), depth: 0, max_depth: 100, @@ -265,6 +271,7 @@ impl SystemInstance { property_maps: builder.property_maps, feature_property_maps: builder.feature_property_maps, connection_property_maps: builder.connection_property_maps, + emv2_models: builder.emv2_models, semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; @@ -319,6 +326,11 @@ impl SystemInstance { self.property_maps.get(&idx).unwrap_or(&EMPTY) } + /// Projected EMV2 models for a component instance (empty slice if none). + pub fn emv2_for(&self, idx: ComponentInstanceIdx) -> &[spar_annex::emv2::Emv2Model] { + self.emv2_models.get(&idx).map(Vec::as_slice).unwrap_or(&[]) + } + /// Resolved properties attached to a feature instance via /// `applies to .` (issue #237). Empty if none. pub fn properties_for_feature(&self, idx: FeatureInstanceIdx) -> &PropertyMap { @@ -1415,6 +1427,7 @@ struct Builder<'a> { property_maps: FxHashMap, feature_property_maps: FxHashMap, connection_property_maps: FxHashMap, + emv2_models: FxHashMap>, /// Property associations with a non-empty `applies to ` clause. /// /// These are collected during instantiation and eagerly attached to @@ -1504,6 +1517,9 @@ impl<'a> Builder<'a> { // Instantiate features, flows, modes, and mode transitions from the type. self.populate_from_type(idx, type_loc, &resolved_package); + // Project retained EMV2 subclause models (type ∪ impl) onto this instance. + self.project_emv2(idx, type_loc, impl_loc); + // Instantiate subcomponents (recursive) #[allow(clippy::collapsible_if)] if let Some(loc) = impl_loc { @@ -1604,6 +1620,9 @@ impl<'a> Builder<'a> { // from the resolved type. self.populate_from_type(child_idx, leaf_type_loc, &leaf_pkg); + // Project the leaf type's EMV2 models (type only). + self.project_emv2(child_idx, leaf_type_loc, None); + // Build property map for leaf subcomponent (type only) self.build_leaf_property_map( child_idx, @@ -1616,6 +1635,7 @@ impl<'a> Builder<'a> { } } else { // No classifier — anonymous subcomponent + // no classifier → no EMV2 to project let child_idx = self.components.alloc(ComponentInstance { name: instance_name, category: _sub_cat, @@ -2022,6 +2042,40 @@ impl<'a> Builder<'a> { None } + /// Project the classifier's EMV2 subclause models (type ∪ impl, direct only) + /// onto a component instance. No-op when neither loc has EMV2. + fn project_emv2( + &mut self, + idx: ComponentInstanceIdx, + type_loc: Option, + impl_loc: Option, + ) { + let mut models = Vec::new(); + if let Some(loc) = type_loc + && let (Some(ct), Some(tree)) = ( + self.scope.get_component_type(loc), + self.scope.tree(loc.tree), + ) + { + for &sub in &ct.emv2 { + models.push(tree.emv2_subclauses[sub].model.clone()); + } + } + if let Some(loc) = impl_loc + && let (Some(ci), Some(tree)) = ( + self.scope.get_component_impl(loc), + self.scope.tree(loc.tree), + ) + { + for &sub in &ci.emv2 { + models.push(tree.emv2_subclauses[sub].model.clone()); + } + } + if !models.is_empty() { + self.emv2_models.insert(idx, models); + } + } + fn populate_from_type( &mut self, idx: ComponentInstanceIdx, @@ -2605,6 +2659,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: FxHashMap::default(), connection_property_maps: FxHashMap::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -4465,4 +4520,113 @@ end p; "feature property must be stored per-feature, not on the component (#237)" ); } + + // ── EMV2 instance projection (REQ-EMV2-PROPAGATION-002, layer 3) ────── + // + // Full pipeline: hand-authored AADL (with an EMV2 annex) → item-tree + // (L2 retains the subclause) → instantiate → assert the ComponentInstance + // carries the projected model. NON-VACUOUS: exact propagation/flow counts + // from the fixture (a bare `== item-tree model` would only prove the copy + // ran; a wrong/empty/double-counted projection must fail loudly). + + fn instantiate_aadl(src: &str, pkg: &str, ty: &str, imp: &str) -> SystemInstance { + let db = crate::HirDefDatabase::default(); + let file = spar_base_db::SourceFile::new(&db, "emv2_l3.aadl".to_string(), src.to_string()); + let tree = crate::file_item_tree(&db, file); + let scope = GlobalScope::from_trees(vec![tree]); + SystemInstance::instantiate(&scope, &Name::new(pkg), &Name::new(ty), &Name::new(imp)) + } + + #[test] + #[cfg_attr(miri, ignore = "parses via rowan — upstream rowan#192 UB under Miri")] + fn emv2_projected_onto_impl_root_from_type() { + // EMV2 on the TYPE; root instance is the IMPLEMENTATION (main alloc + // path unions type ∪ impl). Fixture: 2 propagations + 1 source flow. + let src = r#"package P +public + system S + annex EMV2 {** +error propagations + p1: out propagation {ServiceError}; + p2: in propagation {LateDelivery}; +flows + f1: error source p1 {ServiceError}; +end propagations; + **}; + end S; + system implementation S.i + end S.i; +end P; +"#; + let inst = instantiate_aadl(src, "P", "S", "i"); + let models = inst.emv2_for(inst.root); + assert_eq!( + models.len(), + 1, + "root instance must carry the type's EMV2 subclause" + ); + assert_eq!(models[0].propagations.len(), 2); + assert_eq!(models[0].flows.len(), 1); + } + + #[test] + #[cfg_attr(miri, ignore = "parses via rowan — upstream rowan#192 UB under Miri")] + fn emv2_projected_onto_type_only_leaf_subcomponent() { + // A type-only leaf subcomponent (`sub : device Sensor;`) hits a + // DIFFERENT alloc site than the root; a main-path-only projection would + // silently miss it. Sensor's EMV2: 1 propagation + 1 source flow. + let src = r#"package P +public + device Sensor + annex EMV2 {** +error propagations + s1: out propagation {BadValue}; +flows + fs: error source s1 {BadValue}; +end propagations; + **}; + end Sensor; + system S + end S; + system implementation S.i + subcomponents + sub : device Sensor; + end S.i; +end P; +"#; + let inst = instantiate_aadl(src, "P", "S", "i"); + // Root (S.i) has no EMV2. + assert!( + inst.emv2_for(inst.root).is_empty(), + "S itself declares no EMV2" + ); + // Its leaf subcomponent carries Sensor's projected model. + let sub = inst.component(inst.root).children[0]; + let models = inst.emv2_for(sub); + assert_eq!( + models.len(), + 1, + "type-only leaf must carry its device type's EMV2" + ); + assert_eq!(models[0].propagations.len(), 1); + assert_eq!(models[0].flows.len(), 1); + } + + #[test] + #[cfg_attr(miri, ignore = "parses via rowan — upstream rowan#192 UB under Miri")] + fn emv2_absent_yields_empty_projection() { + // No EMV2 annex anywhere ⇒ empty projection (guards against a bug that + // attaches empty/duplicate models to every instance). + let src = r#"package P +public + system S + end S; + system implementation S.i + end S.i; +end P; +"#; + let inst = instantiate_aadl(src, "P", "S", "i"); + assert!(inst.emv2_for(inst.root).is_empty()); + assert!(inst.emv2_models.is_empty()); + } } diff --git a/crates/spar-hir-def/src/overlay.rs b/crates/spar-hir-def/src/overlay.rs index f9c59b2a..6b728b3a 100644 --- a/crates/spar-hir-def/src/overlay.rs +++ b/crates/spar-hir-def/src/overlay.rs @@ -449,6 +449,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; @@ -940,6 +941,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; @@ -1107,6 +1109,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; diff --git a/crates/spar-mermaid/src/lib.rs b/crates/spar-mermaid/src/lib.rs index 17afae3a..290b87ac 100644 --- a/crates/spar-mermaid/src/lib.rs +++ b/crates/spar-mermaid/src/lib.rs @@ -717,6 +717,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -878,6 +879,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-render/src/lib.rs b/crates/spar-render/src/lib.rs index 2ee41a50..09a1b091 100644 --- a/crates/spar-render/src/lib.rs +++ b/crates/spar-render/src/lib.rs @@ -1063,6 +1063,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; diff --git a/crates/spar-solver/src/enumerate.rs b/crates/spar-solver/src/enumerate.rs index 2fd9b9d7..88650dbc 100644 --- a/crates/spar-solver/src/enumerate.rs +++ b/crates/spar-solver/src/enumerate.rs @@ -682,6 +682,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; diff --git a/crates/spar-solver/src/tests.rs b/crates/spar-solver/src/tests.rs index 9bb09236..746dd1ab 100644 --- a/crates/spar-solver/src/tests.rs +++ b/crates/spar-solver/src/tests.rs @@ -130,6 +130,7 @@ impl TestBuilder { property_maps: self.property_maps, feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } diff --git a/crates/spar-wasm/src/graph.rs b/crates/spar-wasm/src/graph.rs index b2dc7c1a..7e1397fc 100644 --- a/crates/spar-wasm/src/graph.rs +++ b/crates/spar-wasm/src/graph.rs @@ -247,6 +247,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), } @@ -366,6 +367,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; @@ -471,6 +473,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), }; @@ -551,6 +554,7 @@ mod tests { property_maps: FxHashMap::default(), feature_property_maps: Default::default(), connection_property_maps: Default::default(), + emv2_models: Default::default(), semantic_connections: Vec::new(), system_operation_modes: Vec::new(), };