Validate Behavior Annex communication and call signatures 🤖

ba/doc/conformance.md

@@ -59,8 +59,8 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato
 | D.1–D.2: scope and concepts | Embedded `behavior_specification` parser, linker, serializer, and strict-model translation are registered. | Supports the language-tooling role; execution semantics require separate consumer evidence. |
 | 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 (V03) and shared-data resource release (#3189) are now checked, while signature obligations remain incomplete or unverified. |
+| 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; communication target categories/directions and structural call signatures are now checked (#3181). Data-type conformance remains deferred to #3199 and the instance-model pass; 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 (V03) and shared-data resource release (#3189) are now checked, and structural call signatures (#3181) are now checked; property-dependent type conformance remains deferred. |
 | 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. |
 
@@ -164,13 +164,17 @@ The AST precedence error and the strict-model flattening error must be assessed
 
 **Addressed by [#3205](https://github.com/osate/osate2/issues/3205):** D.6 gives the assignment action and the port dequeue action the same `target` production, so the rule reaches the dequeue action too, and the same check now covers it: `p?(i)` and `p?(i.field)` are rejected for the same reason and with the same message as their assignment counterparts. The dequeue shape was invisible for one more reason, that `AadlBaTypeChecker.checkPortDequeue` accepts a dequeue with no target at all, which is what translation leaves behind when the target names an iterator. `Issue3205Test` verifies exact diagnostics and source ranges across both loop forms and nested scopes, and keeps a targetless dequeue, a dequeue into a behavior variable shadowed by an iterator, and a dequeue into a data element of a behavior variable valid.
 
-### G17 — Call signatures and communication categories lack complete enforcement
+### G17 — Communication categories and structural call signatures
 
-**Standard:** D.5–D.6 constrain communication targets and require actual call parameters to match the called subprogram's features/signature.
+**Standard:** D.5–D.6 constrain communication targets and require actual call parameters to match the called subprogram's features/signature, in declaration order.
 
-**Evidence:** The grammar's `CommunicationAction` accepts a generic reference and a list of expressions. Translator `toCommunicationAction` distinguishes an ordinary port send from a subprogram call, but a port send takes only the first expression from that list. `getFormalParameters` selects parameters and data accesses. [AadlBaTypeChecker.checkBasicAction](../../ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaTypeChecker.java) checks assignment, port send, and dequeue actions, then returns true for other basic actions; it does not validate a `SubprogramCallAction` signature. The rules driver does not add that signature check.
+**Implemented for [#3181](https://github.com/osate/osate2/issues/3181):** The declarative validator rejects non-callable targets, sends on incoming ports, dequeues on outgoing or data-only ports, freezes on outgoing ports, and individual lock/unlock actions on elements other than required data accesses. Port sends reject extra values instead of silently accepting only the first; event-port sends and dequeues cannot carry data. Feature-group inversion is included in direction checks.
 
-**Assessment:** Source-confirmed incomplete checking and a source-confirmed extra-argument discard path for port sends. The exact user-visible acceptance/diagnostics of each invalid call needs external-model reproduction. Required cases include missing/extra parameters, wrong parameter type or direction, calls involving supported non-parameter features, sends on input ports, and attempts to call non-callable elements. G10 illustrates why a generic holder fallback must not be treated as proof of a valid communication action.
+Signatures include every feature, including ports, in source declaration order. Inherited features precede added features and refinements retain their inherited positions. Classifier, implementation, subprogram-access, subcomponent, and constrained-prototype calls use the same signature lookup. Unconstrained, unbound prototypes have no signature to check yet. Parameters require readable input expressions and writable output targets; data-access actuals must reference data; port actuals must match the port category and direction. Formal categories that the strict model cannot represent receive an explicit unsupported-feature diagnostic rather than being omitted from the signature. Writable record-field and port actuals remain targets in the strict model.
+
+**Validation:** `Issue3181Test` reproduces the missing diagnostics and lost writable-target representation through external AADL models, and includes valid calls, inverse feature groups, inherited/refined signatures, and prototypes. Call data actuals now reach the existing type checker, including its active expression-operator checks.
+
+**Deferred:** Actual/formal type comparisons use the existing `DataTypeChecker`; the production `AdaLikeDataTypeChecker.conformsTo` is still disabled under [#3199](https://github.com/osate/osate2/issues/3199). Effective `Access_Right` and property-derived representation, array, and range checks require the instance-model pass described in [properties.md](properties.md). Structural signature validation does not establish those properties.
 
 ### G18 — Type conformance is disabled, so no type mismatch is reported
 
@@ -233,7 +237,7 @@ These are proposed follow-up changes, not changes made by this review.
 | 1 | ~~Repair the conformance test oracle and ensure deterministic BA validator registration. Separate legacy characterization from standard expectations.~~ **Done**, branch `repair_conformance_test_oracle` (commit `Repair the Behavior Annex conformance test oracle`). | Exact diagnostics are compared, by `expected/diagnostics` and the new `expected/diagnostics-validated`; registration is proved end to end by requiring at least one BA rule diagnostic in the validated suite and none in the plain baseline; both suites and the conformance class assert nonzero executed cases; the nine skips it left were listed in `TRACKED_SKIPS` against their own issues and enforced by reflection, and that list has shrunk to five as those issues closed; `SelfPropertyReference.aadl` no longer carries an unrelated D.3 error. Each repaired expectation was confirmed to fail for its intended reason by temporarily removing its `@Ignore`. |
 | 2 | Preserve strict-model meaning: numeric literals, array extents, logical grouping, `self`, internal events, and mode bindings (G08, G10–G14). **Done:** G08 and G10–G14 are implemented. | External AADL input produces correct literal values, extents, references, operation kinds, and mode links; no test-only model mutation is needed. Assert attributes and semantic structure directly. |
 | 3 | Implement the missing standard syntax and remove unwanted overacceptance (G01–G07, G09, G13). **Under way:** G01–G07 and G13 are closed; G09 remains. G06 uses a deliberate warned-extension policy rather than strict grammar rejection. | Each standard form parses and translates; nonstandard forms have deliberate rejection/extension policy. Enable corrected standard acceptance tests and add AST/strict-model expression tests. |
-| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16 and V01–V03 are addressed; G15, G17, G18, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. |
+| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16 and V01–V03 are addressed; G17 structural checks are implemented; G15, G18, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. |
 | 5 | Establish behavioral/dataflow coverage and consumer boundaries (V04–V05, V08–V09, D.5 and D.8 runtime semantics). **Under way:** V05 is addressed, except for the subcomponent override rule, which that row assigns to the consumer that walks the instance hierarchy. | State which obligations the front end can prove, which are warnings/approximations, and which belong to a simulator, analyzer, or generator. Validate queue behavior, timeouts, lock lifetimes, initialization, and call synchronization in the responsible consumer. |
 
 There is no basis here for a numerical conformance percentage: the suite is not a clause-complete standard test suite, some assertions are ineffective, and operational semantics were outside the executed scope. A defensible future claim should distinguish syntax acceptance, valid strict-model construction, legality/consistency enforcement, and downstream execution semantics.

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

@@ -1,19 +1,11 @@
 error | semantic | 230 | 17 | 14 | Port status value 'outPortA'count' is defined only for a port that is frozen on input, but 'outPortA' is an outgoing port. AS5506/3 Rev. A states no corresponding legality rule.
 error | semantic | 237 | 23 | 14 | Port status value 'outPortA'fresh' is defined only for a port that is frozen on input, but 'outPortA' is an outgoing port. AS5506/3 Rev. A states no corresponding legality rule.
-error | semantic | 643 | 22 | 13 | There is no applicable operator ">" for type Base_Types::Boolean
-error | semantic | 645 | 22 | 17 | There is no applicable operator ">" for type AadlBaTest::Types::Opaque
-error | semantic | 650 | 21 | 14 | There is no applicable operator "+" for type AadlBaTest::Types::Opaque
-error | semantic | 655 | 21 | 13 | Operator "-" not defined for type Base_Types::Character
-error | semantic | 656 | 24 | 17 | There is no applicable operator "+" for type Base_Types::String
-error | semantic | 665 | 21 | 17 | There is no applicable operator "mod" for type Base_Types::Float
-error | semantic | 666 | 21 | 17 | There is no applicable operator "rem" for type Base_Types::Float
-error | semantic | 669 | 23 | 9 | Operator "abs" not defined for type Base_Types::Character
-error | semantic | 673 | 23 | 5 | Operator "!" not defined for type universal integer
-error | semantic | 679 | 21 | 56 | exponent must be of type natural, found universal integer
-error | semantic | 680 | 21 | 15 | exponent must be of type natural, found DataTypeCheckerTest::NegativeInteger
-error | semantic | 681 | 21 | 14 | exponent must be of type natural, found Base_Types::Float
-error | semantic | 682 | 21 | 12 | exponent must be of type natural, found Base_Types::Integer
-error | semantic | 684 | 23 | 14 | Invalid operand types for operator "**": left operand has type DataTypeCheckerTest::MyFixedPoint, right operand has type Base_Types::Natural
+error | semantic | 609 | 26 | 3 | Actual for out parameter 'y' must be a writable target
+error | semantic | 611 | 13 | 8 | Subprogram call requires 2 actuals but has 0
+error | semantic | 612 | 13 | 23 | Subprogram call requires 0 actuals but has 2
+error | semantic | 614 | 13 | 14 | Subprogram call requires 2 actuals but has 0
+error | semantic | 615 | 13 | 10 | A send or call action requires a port, internal feature, or callable subprogram
+error | semantic | 618 | 30 | 1 | Actual for out parameter 'y' must be a writable target
 warning | semantic | 25 | 33 | 21 | AadlBaTestPropertySet in 'with' clause of public package section is not used.
 warning | semantic | 25 | 75 | 20 | AadlBaTestSubprogram in 'with' clause of public package section is not used.
 warning | semantic | 426 | 21 | 1 | Unary plus is not part of AS5506/3 Rev. A
@@ -32,4 +24,3 @@ warning | semantic | 454 | 23 | 1 | Unary plus is not part of AS5506/3 Rev. A
 warning | semantic | 456 | 23 | 1 | Unary plus is not part of AS5506/3 Rev. A
 warning | semantic | 458 | 23 | 1 | Unary plus is not part of AS5506/3 Rev. A
 warning | semantic | 460 | 23 | 1 | Unary plus is not part of AS5506/3 Rev. A
-warning | semantic | 683 | 21 | 38 | Cannot evaluate if the exponent is a natural

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

@@ -4,6 +4,13 @@ error | semantic | 182 | 5 | 54 | Invalid circular dependency. Subcomponent 'sub
 error | semantic | 183 | 5 | 48 | The type of subcomponent 'recursiveGrp' cannot be the object that contains it
 error | semantic | 231 | 5 | 54 | Invalid circular dependency. Subcomponent 'subprogGrp' directly or indirectly contains 'thread2.impl'.
 error | semantic | 379 | 5 | 45 | Invalid circular dependency. Subcomponent 'threadGrp' directly or indirectly contains 'process1.impl'.
+error | semantic | 476 | 16 | 25 | A port send action requires an outgoing port
+error | semantic | 477 | 16 | 24 | A freeze action requires an incoming port
+error | semantic | 478 | 16 | 24 | A dequeue action requires an incoming event or event data port
+error | semantic | 482 | 16 | 34 | A lock or unlock action requires a required data access
+error | semantic | 483 | 16 | 34 | A lock or unlock action requires a required data access
+error | semantic | 484 | 16 | 47 | A lock or unlock action requires a required data access
+error | semantic | 485 | 16 | 47 | A lock or unlock action requires a required data access
 error | semantic | 96 | 5 | 42 | Feature group directly or indirectly contains itself
 warning | semantic | 29 | 30 | 21 | AadlBaTestPropertySet in 'with' clause of public package section is not used.
 warning | semantic | 29 | 72 | 20 | AadlBaTestSubprogram in 'with' clause of public package section is not used.

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

@@ -0,0 +1,3 @@
+error | semantic | 57 | 20 | 3 | Actual for out parameter 'f3' must be a writable target
+error | semantic | 57 | 25 | 3 | Actual for in out parameter 'f4' must be a writable target
+error | semantic | 59 | 11 | 3 | Actual for in out parameter 'f2' must be a writable target

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

@@ -0,0 +1,2 @@
+error | semantic | 16 | 6 | 4 | A dequeue action requires an incoming event or event data port
+error | semantic | 17 | 6 | 4 | A dequeue action requires an incoming event or event data port

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

@@ -0,0 +1,5 @@
+error | semantic | 44 | 42 | 1 | Actual for out parameter 'result' must be a writable target
+error | semantic | 45 | 42 | 9 | Actual for out parameter 'result' must be a writable target
+error | semantic | 46 | 42 | 5 | Actual for out parameter 'result' must be a writable target
+error | semantic | 47 | 39 | 6 | Actual for in parameter 'argument' must be readable
+error | semantic | 48 | 62 | 1 | Actual for out parameter 'result' must be a writable target

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

@@ -0,0 +1,4 @@
+error | semantic | 50 | 28 | 10 | Subprogram call requires 5 actuals but has 0
+error | semantic | 51 | 28 | 15 | Subprogram call requires 5 actuals but has 1
+error | semantic | 52 | 28 | 22 | Subprogram call requires 5 actuals but has 2
+error | semantic | 53 | 28 | 49 | Subprogram call requires 5 actuals but has 6

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

@@ -0,0 +1 @@
+error | semantic | 40 | 39 | 7 | There is no applicable operator "and" for type universal integer