Detect unreleased Behavior Annex shared-data locks 🤖

ba/doc/conformance.md

@@ -60,7 +60,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato
 | D.3: behavior specification | Variables, grouped states, state kinds, named/prioritized and multiple-source transitions, execute conditions, and dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions (G01), complete external-condition expressions (G02), naming and otherwise-transition rules (V01 and V02), complete-state mode binding (G14), and multiple subprogram final states (G15) were absent and are now implemented; several consistency obligations lack demonstrated enforcement. |
 | D.4: thread dispatch | Dispatch conjunction/disjunction, `stop`, bare timeout, timeout with a duration, and an unparenthesized frozen-port list. Selected timeout/stop checks exist. | Partial. Required frozen-list parentheses were missing (G03) and timeout reset ports absent (G04), both since fixed. Full protocol/trigger compatibility and core-property consistency are not demonstrated. |
 | D.5: component interactions | Port send/dequeue/freeze, count/fresh/updated, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` was absent (G07), internal events were represented incorrectly (G10), and outgoing ports were accepted for the three input-freeze status values, all since fixed; call-signature and remaining communication direction/category checks need additional coverage. Input/output timing consistency is not established. |
-| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, loops with a written or an omitted iterator classifier, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers were missing (G09) and are now implemented; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. |
+| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, loops with a written or an omitted iterator classifier, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers were missing (G09) and are now implemented; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules (V03) and shared-data resource release (#3189) are now checked, while signature obligations remain incomplete or unverified. |
 | D.7: expressions | Boolean/numeric/string syntax, arithmetic/relational/logical operators, property references, indexing, and operator applicability checks per operand data representation. | Partial, with semantic preservation defects. Operand consistency between the two operands is not checked, only applicability of the operator to the first one (G18). Short-circuit logical operators, including in external conditions, and `updated` are now supported (#3166, #3169, and G07, since fixed), and value-expression precedence, association, admissible forms, and grouping now follow the document (G13, since fixed); numeric translation differs from the document, unary plus remains accepted as an extension but now produces a compatibility warning (G06), and declarative initializer typing and definite initialization are now checked (#3190). Instance-dependent initialization from prefixed property values remains #3230. |
 | D.8: synchronization | `Behavior_Properties::Subprogram_Call_Protocol` declares HSER/LSER/ASER and defaults to HSER, matching the supplied document. A client/server example exists. | Property definition conforms. Enforcement of the two LSER/ASER legality rules and execution of the protocols are not established. |
 
@@ -199,7 +199,7 @@ These are bounded findings from the inspected grammar/translator/checker path. E
 | V05 | D.3 component-category/mode restrictions on external/internal conditions; behavior inheritance and replacement. | Conditions can be parsed generically, while type checking dispatches only execute conditions and the rules driver primarily dispatch conditions. Same-named complete states are now bound for no-`in modes` refinements (G14), but the builder does not copy an in-modes context into the strict annex. Core AADL may retain mode applicability on the enclosing annex. Verify the complete consumer path before declaring inheritance or mode-specific selection unsupported. Cover thread/subprogram external-condition rejection and device condition mixing. **Addressed by [#3186](https://github.com/osate/osate2/issues/3186):** the consistency checker rejects an external condition in a thread or a subprogram and rejects a mixture of external and dispatch conditions out of one complete state of a device; the validator rejects an external condition in a subclause with an `in modes` statement, which is where in-modes rules already live because core AADL keeps that statement on the enclosing subclause rather than in the strict annex. D.3 states no per-category restriction on internal conditions beyond the execution-state rule closed with [#3165](https://github.com/osate/osate2/issues/3165). C4 now reads the triggers of an external condition as well, so the mode-transition comparison covers the way a component of any other category than thread and subprogram describes a mode transition; that made `issue2147` report the missing-mode-transition finding its dispatch equivalent already produced. Mode applicability is not duplicated into the strict annex: core AADL keeps it on the `DefaultAnnexSubclause` that every consumer of `BehaviorAnnexUtil.getStrictModel` already holds. `BehaviorAnnexUtil.getBehaviorAnnexSubclauses` implements the ancestor/descendant rule on that access path, with a mode-selecting overload. `Issue3186Test` covers each rejection, a positive control for each, and the inheritance, replacement, type-fallback, and mode-selection cases. The subcomponent override rule is not enforced: it selects which subclause a consumer interprets for an instance rather than constraining a declaration, so it belongs to the consumer that walks the instance hierarchy. |
 | V06 | D.4 protocol/trigger compatibility, legal trigger/frozen-port categories, and consistency with core dispatch/freeze properties. | The checker has dedicated timeout branches and a stop check, but no complete implementation of the document's protocol/trigger table was found. Dispatch references use generic `Reference` syntax. A rule implementing one timeout form is not evidence for all rows of the table. Test the matrix and invalid trigger direction/category through embedded source. |
 | V07 | D.5 C1/C2: BA freeze/send operations agree with `Input_Time`/`Output_Time`, or are absent where required. | No BA check referring to these properties was found in the active BA checker/translator/validator code. Core property validation alone does not establish agreement with BA actions. Use models that are individually legal on each side but inconsistent together. |
-| V08 | D.6: a complete state cannot be reached while shared data remains locked. | Lock/unlock syntax and holders exist; `Issue2372Test` checks resolved lock references. No path-sensitive lock-balance check was found. Cover a balanced path, an unreleased resource, alternative branches, loops, and wildcard lock/unlock. Parsing a lock operation does not establish this rule. |
+| V08 | D.6: a complete state cannot be reached while shared data remains locked. | **Implemented for [#3189](https://github.com/osate/osate2/issues/3189):** `AadlBaLockChecker` tracks each required data-access path, including inherited, nested, and inverted feature-group accesses, from initial states through transition joins and cycles. It reports each transition/resource pair that can enter a complete state with a held lock. A path established without assumptions about runtime values produces an error; a finding that depends on conservative runtime assumptions is informational, so potential false positives do not invalidate a balanced model. Action summaries handle sequences, unordered sets (including interleaved nested sequences), conditional alternatives, zero-or-more versus one-or-more loop iterations, and wildcard lock/unlock. Statically false branches/transitions, disabled `otherwise` transitions, empty literal ranges, and loops with no possible exit do not introduce spurious complete-state paths. `Issue3189Test` covers balanced controls and unreleased-resource paths through the embedded validator. Runtime-dependent guards and collection/range sizes are approximated conservatively; the checker does not correlate data values across separate conditions or resolve instance-level aliases between accesses. |
 | V09 | D.7: right-hand-side variables/data must be initialized; declaration initialization overrides the Data Modeling `Initial_Value` property. | Declaration initializer types and declarative definite initialization are checked by #3190. Explicit declaration initializers and unprefixed `Data_Model::Initial_Value` associations seed the analysis, with declaration initialization taking precedence. Instance-dependent initialization from prefixed property values is tracked by #3230 and blocked by #3229. |
 | V10 | D.7 property references are restricted to unitless properties or properties with time units. | **Addressed by [#3191](https://github.com/osate/osate2/issues/3191):** the validator checks the declared units type of referenced properties, constants, and selected record fields, accepting unitless values and `AADL_Project::Time_Units`. Other units types are reported at the property reference. `Issue3191Test` covers integer and real values, defaults, symbolic element prefixes, record fields, and a custom units type whose literal is named `ms`. Translation retains default values and their written units, and prefixed references retain their owners and property definitions. Effective instance-value selection remains part of #3229. |
 | V11 | D.8 LSER/ASER prohibits synchronous called-subprogram type and out/in-out parameters. | The [property set](../../ba/org.osate.ba.contrib/resources/properties/behavior_properties.aadl) matches the standard. Searches of BA and the core AADL validator found no checks consuming `Subprogram_Call_Protocol`; [ba_example_007.aadl](../../ba/org.osate.ba/examples/standard_examples/ba_example_007.aadl) describes the rules in comments but is not negative legality coverage. Add both prohibited combinations for both protocols. |

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_ActionSets.txt

@@ -0,0 +1,3 @@
+error | semantic | 38 | 13 | 79 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 49 | 13 | 122 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 60 | 13 | 113 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_Branches.txt

@@ -0,0 +1,3 @@
+info | semantic | 39 | 13 | 110 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 50 | 13 | 130 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 61 | 13 | 158 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_GroupedResources.txt

@@ -0,0 +1,2 @@
+error | semantic | 55 | 13 | 66 | Complete state 'ready' may be reached while shared data 'left.d' remains locked: Behavior Annex D.6.
+error | semantic | 64 | 13 | 84 | Complete state 'ready' may be reached while shared data 'nested.inner.d' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_Issue3189.txt

@@ -0,0 +1 @@
+error | semantic | 38 | 13 | 78 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_Loops.txt

@@ -0,0 +1,6 @@
+error | semantic | 72 | 13 | 97 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 83 | 13 | 103 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 94 | 13 | 107 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 39 | 13 | 99 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 50 | 13 | 107 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 61 | 13 | 99 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_PotentialFalsePositives.txt

@@ -0,0 +1,3 @@
+error | semantic | 55 | 13 | 111 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 40 | 13 | 143 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 72 | 13 | 48 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_Transitions.txt

@@ -0,0 +1,2 @@
+info | semantic | 41 | 13 | 35 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+info | semantic | 59 | 13 | 39 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3189_Wildcards.txt

@@ -0,0 +1,4 @@
+error | semantic | 43 | 13 | 63 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 52 | 13 | 77 | Complete state 'ready' may be reached while shared data 'd' remains locked: Behavior Annex D.6.
+error | semantic | 52 | 13 | 77 | Complete state 'ready' may be reached while shared data 'e' remains locked: Behavior Annex D.6.
+error | semantic | 63 | 13 | 87 | Complete state 'ready' may be reached while shared data 'e' remains locked: Behavior Annex D.6.

ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3189_ActionSets.txt

@@ -0,0 +1,63 @@
+annex[0] owner=ActionSets::subject.order
+  (BehaviorActionBlock, <null>, 2158, 41)
+  (BehaviorActionSet, <null>, 2176, 9)
+  (BehaviorAnnex, behavior_specification, 2032, 168)
+  (BehaviorCondition, <null>, 2137, 11)
+  (BehaviorState, ready, 2051, 5)
+  (BehaviorStateGroup, <null>, 2051, 37)
+  (BehaviorTransition, order, 2121, 79)
+  (CommunicationAction, <null>, 2176, 3)
+  (CommunicationAction, <null>, 2182, 3)
+  (DispatchCondition, <null>, 2140, 8)
+  (Reference, <null>, 2176, 1)
+  (Reference, <null>, 2182, 1)
+  (ReferenceSegment, d, 2176, 1)
+  (ReferenceSegment, d, 2182, 1)
+annex[1] owner=ActionSets::subject.nestedOrder
+  (BehaviorActionBlock, <null>, 2457, 78)
+  (BehaviorActionBlock, <null>, 2475, 17)
+  (BehaviorActionBlock, <null>, 2495, 26)
+  (BehaviorActionSequence, <null>, 2477, 13)
+  (BehaviorActionSequence, <null>, 2497, 22)
+  (BehaviorActionSet, <null>, 2475, 46)
+  (BehaviorAnnex, behavior_specification, 2325, 211)
+  (BehaviorCondition, <null>, 2436, 11)
+  (BehaviorIntegerLiteral, <null>, 2509, 1)
+  (BehaviorState, ready, 2344, 5)
+  (BehaviorStateGroup, <null>, 2344, 37)
+  (BehaviorTime, <null>, 2509, 4)
+  (BehaviorTransition, nestedOrder, 2414, 122)
+  (CommunicationAction, <null>, 2477, 3)
+  (CommunicationAction, <null>, 2482, 3)
+  (CommunicationAction, <null>, 2487, 3)
+  (CommunicationAction, <null>, 2516, 3)
+  (DispatchCondition, <null>, 2439, 8)
+  (Reference, <null>, 2477, 1)
+  (Reference, <null>, 2482, 1)
+  (Reference, <null>, 2487, 1)
+  (Reference, <null>, 2516, 1)
+  (ReferenceSegment, d, 2477, 1)
+  (ReferenceSegment, d, 2516, 1)
+  (ReferenceSegment, e, 2482, 1)
+  (ReferenceSegment, e, 2487, 1)
+  (TimedAction, <null>, 2497, 17)
+annex[2] owner=ActionSets::subject.unrelatedRelease
+  (BehaviorActionBlock, <null>, 2809, 64)
+  (BehaviorActionBlock, <null>, 2832, 27)
+  (BehaviorActionSequence, <null>, 2827, 32)
+  (BehaviorActionSet, <null>, 2834, 23)
+  (BehaviorAnnex, behavior_specification, 2672, 202)
+  (BehaviorCondition, <null>, 2788, 11)
+  (BehaviorIntegerLiteral, <null>, 2852, 1)
+  (BehaviorState, ready, 2691, 5)
+  (BehaviorStateGroup, <null>, 2691, 37)
+  (BehaviorTime, <null>, 2852, 4)
+  (BehaviorTransition, unrelatedRelease, 2761, 113)
+  (CommunicationAction, <null>, 2827, 3)
+  (CommunicationAction, <null>, 2834, 3)
+  (DispatchCondition, <null>, 2791, 8)
+  (Reference, <null>, 2827, 1)
+  (Reference, <null>, 2834, 1)
+  (ReferenceSegment, d, 2827, 1)
+  (ReferenceSegment, e, 2834, 1)
+  (TimedAction, <null>, 2840, 17)