Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bug when comparing opaque values #1294

Open
NickFoubert opened this issue Dec 5, 2023 · 2 comments
Open

Bug when comparing opaque values #1294

NickFoubert opened this issue Dec 5, 2023 · 2 comments
Labels

Comments

@NickFoubert
Copy link

I've been trying to figure out how to compare opaque values, and while trying out one iteration I've bumped into a bug.

Reproducer:

package Bug is

   type Message is
      message
         Key : Opaque with Size => 3 * 8;
      end message;

   type Messages is sequence of Message;

   generic
   session Session is
   begin
      state S is
        Ms_1     : Messages;
        Ms_2     : Messages;
        Test_Key : Opaque := [0, 1, 0];
      begin
        Ms_1'Reset;
        Ms_2'Reset;
        Ms_2 :=
            [for M in Ms_1
             if M.Key = Test_Key =>
             M];
      transition
         goto null
      exception
         goto null
      end S;

   end Session;
end Bug;

generating results in the following output:

Parsing specs/bug.rflx
Processing Bug
Verifying __BUILTINS__::Boolean
Verifying __INTERNAL__::Opaque
Verifying Bug::Message
Verifying Bug::Messages
Verifying Bug::Session
Generating Bug::Message
Generating Bug::Messages
Generating Bug::Session

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.15.0
attrs 23.1.0
icontract 2.6.5
importlib-resources 6.1.1
pydantic 1.10.13
pydotplus 2.0.2
pygls 1.0.2
ruamel.yaml 0.17.40
z3-solver 4.12.2.0

Optimized: False

Command: /usr/local/bin/rflx --workers 20 generate -d generated/ specs/bug.rflx

Traceback (most recent call last):
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 413, in main
    args.func(args)
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 507, in generate
    ).generate(
      ^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 143, in generate
    units = self._generate(model, integration)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 322, in _generate
    units.update(self._create_session(s, integration))
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 339, in _create_session
    session_generator = SessionGenerator(
                        ^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 181, in __init__
    self._create()
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 214, in _create
    state_machine = self._create_state_machine()
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 379, in _create_state_machine
    unit += self._create_states(self._session, composite_globals, is_global)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 843, in _create_states
    Variable("Ctx.P.Slots" * self._allocator.get_slot_ptr(d.location)),
                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/allocator.py", line 121, in get_slot_ptr
    slot_id: int = self._allocation_slots[location]
                   ~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^
KeyError: 
    Location(
        _source=PosixPath('specs/bug.rflx'),
        _start=(22, 17),
        _end=(22, 22),
        _verbose=False)

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

A bug was detected. Please report this issue on GitHub:
@NickFoubert NickFoubert added the bug label Dec 5, 2023
@treiher
Copy link
Collaborator

treiher commented Dec 6, 2023

Thank you for your report! We will look into it and get back to you.

@treiher treiher self-assigned this Dec 6, 2023
@treiher
Copy link
Collaborator

treiher commented Dec 14, 2023

We fixed the fatal error. Unfortunately, comparing opaque message fields requires some additional work and is not yet supported. For now, an error message will be displayed in this case.

@treiher treiher removed their assignment Dec 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants