[bug] AssertionError in "expr_conv.py", line 645 (assert isinstance)

[mgrojo]

I've found a bug while generating code for a state machine.

info: Parsing specs/coap_client.rflx
info: Parsing specs/coap.rflx
info: Processing CoAP
info: Processing CoAP_Client
info: Verifying __BUILTINS__::Boolean
info: Verifying __INTERNAL__::Opaque
info: Verifying CoAP::Code_Class
info: Verifying CoAP::Method_Code
info: Verifying CoAP::Success_Response
info: Verifying CoAP::Client_Error_Response
info: Verifying CoAP::Server_Error_Response
info: Verifying CoAP::Version_Type
info: Verifying CoAP::Message_Type
info: Verifying CoAP::Token_Length
info: Verifying CoAP::Message_ID_Type
info: Skipping verification of CoAP::CoAP_Message (cached)
info: Verifying CoAP::Option_Base_Type
info: Verifying CoAP::Option_Extended8_Type
info: Verifying CoAP::Option_Extended16_Type
info: Skipping verification of CoAP::Option_Type (cached)
info: Verifying CoAP::Option_Sequence
info: Verifying CoAP::Marker_Type
info: Verifying CoAP::Option_Numbers

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.24.0
attrs 23.2.0
defusedxml 0.7.1
importlib-resources 6.4.4
pydantic 2.8.2
pydotplus 2.0.2
pygls 1.3.1
ruamel.yaml 0.18.6
z3-solver 4.12.2.0

Optimized: False

Command: tools/RecordFlux//.venv/bin/rflx generate -d generated/specs/ specs/coap_client.rflx

Traceback (most recent call last):
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/cli.py", line 459, in main
    args.func(args)
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/cli.py", line 484, in generate
    model, integration = parse(
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/cli.py", line 546, in parse
    model = parser.create_model()
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/specification/parser.py", line 1853, in create_model
    checked_model = unchecked_model.checked(
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/model.py", line 35, in checked
    unverified = d.checked(declarations, skip_verification=True)
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 1045, in checked
    return StateMachine(
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 392, in __init__
    self.to_ir()
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 429, in to_ir
    [state.to_ir(variable_id) for state in self.states],
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 429, in <listcomp>
    [state.to_ir(variable_id) for state in self.states],
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 171, in to_ir
    actions = [s for a in self._actions for s in a.to_ir(variable_id)]
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/state_machine.py", line 171, in <listcomp>
    actions = [s for a in self._actions for s in a.to_ir(variable_id)]
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/model/statement.py", line 80, in to_ir
    expression = expr_conv.to_ir(self.expression, variable_id)
  File "/usr/lib/python3.10/functools.py", line 889, in wrapper
    return dispatch(args[0].__class__)(*args, **kw)
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/expr_conv.py", line 831, in _
    e_ir = to_ir(e, variable_id)
  File "/usr/lib/python3.10/functools.py", line 889, in wrapper
    return dispatch(args[0].__class__)(*args, **kw)
  File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/expr_conv.py", line 645, in _
    assert isinstance(expression.type_, (rty.Enumeration, rty.Structure, rty.Message))
AssertionError

The input files are: bug_input_files.zip

[mgrojo]

It seems to be related with the two functions returning Opaque. Removing them and initializing the corresponding fields to [], the exception disappears. bug_avoided.zip

[mgrojo]

I've learned that state-machine functions can only return scalars and definite messages, so what should have happened is the raising of an error telling that indefinite types cannot be returned.

I've followed this example to advance with the state machine: https://github.com/AdaCore/RecordFlux/blob/4981cd565d62c68cd9024c452c237b799ea68bcb/examples/apps/spdm_responder/specs/spdm_responder.rflx#L55-L60

[treiher]

I'm sorry for the inconvenience. This bug has been fixed in the meantime (see 49f8edf1f929d1a52748d6f2813ba9f21646a1e3). The specification in bug_input_files.zip is now correctly rejected:

error: invalid return type
 --> coap_client.rflx:8:60
  |
8 |       with function Get_Request_Options_And_Payload return Opaque;
  |                                                            ------ help: only scalars and definite messages are allowed
  |
error: invalid return type
 --> coap_client.rflx:9:45
  |
9 |       with function Get_Random_Token return Opaque;
  |                                             ------ help: only scalars and definite messages are allowed
  |
error: invalid variable type
  --> coap_client.rflx:19:18
   |
19 |          Token : Opaque := Get_Random_Token;
   |                  ------ help: use a message with an opaque field instead
   |

Opaque cannot be used as a return type or as a variable. Using a definite message with an Opaque field instead is the right approach.

A new version, which also contains a fix for this bug, will be released very soon (probably tomorrow).