NotImplementedError raised when using function call as argument of message aggregate

[jklmnn]

With my current SPDM spec I get the following bugbox:

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.10.0
ruamel.yaml 0.17.21
attrs 21.4.0
pydotplus 2.0.2
z3-solver 4.8.17.0
pydantic 1.9.0
icontract 2.6.1

Optimized: False

Command: /tmp/tmp.9hdAmOjNM5/venv/bin/rflx generate build/specs/CHALLENGE_AUTH=True,KEY_EXCHANGE=True,RESPOND_IF_READY=True/spdm_emu.rflx build/specs/CHALLENGE_AUTH=True,KEY_EXCHANGE=True,RESPOND_IF_READY=True/spdm_proxy.rflx build/specs/CHALLENGE_AUTH=True,KEY_EXCHANGE=True,RESPOND_IF_READY=True/spdm_requester.rflx build/specs/CHALLENGE_AUTH=True,KEY_EXCHANGE=True,RESPOND_IF_READY=True/spdm_responder.rflx build/specs/CHALLENGE_AUTH=True,KEY_EXCHANGE=True,RESPOND_IF_READY=True/spdm.rflx --debug -d build/debug/generated

Traceback (most recent call last):
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/cli.py", line 201, in main
    args.func(args)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/cli.py", line 259, in generate
    generator = Generator(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 141, in __init__
    self.__generate(model, integration)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 220, in __generate
    self.__create_session(s, integration)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 231, in __create_session
    session_generator = SessionGenerator(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 219, in __init__
    self._create()
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 249, in _create
    state_machine = self._create_state_machine()
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 357, in _create_state_machine
    unit += self._create_states(self._session, composite_globals, is_global)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 844, in _create_states
    *[
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 847, in <listcomp>
    for s in self._state_action(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 1893, in _state_action
    result = self._assign(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 2123, in _assign
    return self._assign_to_message_aggregate(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 2352, in _assign_to_message_aggregate
    size = self._message_size(message_aggregate)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 3190, in _message_size
    return message.size({model.Field(f): v for f, v in message_aggregate.field_values.items()})
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/model/message.py", line 986, in size
    proof = expr.Equal(expr.Size("Message"), message_size).check(
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/expression.py", line 263, in check
    return Proof(self, facts)
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/expression.py", line 60, in __init__
    solver.add(f.z3expr())
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/expression.py", line 1800, in z3expr
    right = self.right.z3expr()
  File "/tmp/tmp.9hdAmOjNM5/venv/lib/python3.9/site-packages/rflx/expression.py", line 1488, in z3expr
    raise NotImplementedError
NotImplementedError

----------------------------------------------------------------------------

Unfortunately I wasn't able to come up with a good reproducer yet. I already created this ticket to track further findings.

[treiher]

It looks like you tried to use a message aggregate with a function call as an argument. When a message aggregate is used, the generator determines the size of the resulting message to check if the serialized message fits into the available buffer. For the size determination, all arguments of the message aggregate are converted to an Z3 expression. This conversion failed for the Call argument. This issue is related to #1019, but it could make sense to improve the error message until #1019 is implemented.

[senier]

@jklmnn Can you please add a small reproducer for this issue?

[jklmnn]

I tried to reproduce the issue with the following spec:

package Test is

   type Element is mod 2 ** 8;

   type Message is
      message
         E : Element;
      end message;

   generic
      Channel : Channel with Readable, Writable;
      with function Get_Element return Element;
   session Session with
      Initial => Start,
      Final => Terminated
   is
      Msg : Message;
   begin
      state Start
      is
      begin
         Msg := Message'(E => Get_Element);
      transition
         goto Send
      exception
         goto Terminated
      end Start;

      state Send
      is
      begin
         Channel'Write (Msg);
      transition
         goto Terminated
      end Send;

      state Terminated is null state;
   end Session;

end Test;

Running the generator produces the following error:

Parsing test.rflx
Processing Test
Generating Test::Element
Generating Test::Message
Generating Test::Session
test.rflx:22:31: generator: error: Call with integer type "Test::Element" (0 .. 255) as value of message field not yet supported

As the issue is also handled in #1019 and the error message has been improved I'll close this issue.