Bug when including a condition on a field that is a message type

[NickFoubert]

When trying to generate the following:

package Test is

   type Spare_7_Bits is range 0 .. 0 with Size => 7;

   type Some_Record is
      message
         F : Opaque with Size => 8;
      end message;

   type Some_Message is
      message
         Flag         : Boolean;
         Spare_7_Bits : Spare_7_Bits;
         First_Record : Some_Record
            then null
               if Flag = True;
      end message;

end Test;

RecordFlux crashes:

Parsing specs/test.rflx
Processing Test
Verifying __BUILTINS__::Boolean
Verifying __INTERNAL__::Opaque
Verifying Test::Spare_7_Bits
Verifying Test::Some_Record
Verifying Test::Some_Message

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.14.0
attrs 23.1.0
icontract 2.6.4
importlib-resources 6.1.0
pydantic 1.10.13
pydotplus 2.0.2
pygls 1.1.1
ruamel.yaml 0.17.35
z3-solver 4.12.2.0

Optimized: False

Command: /usr/local/bin/rflx generate -d generated/ specs/test.rflx

Traceback (most recent call last):
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 415, in main
    args.func(args)
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 492, in generate
    model, integration = parse(
                         ^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 546, in parse
    model = parser.create_model()
            ^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/specification/parser.py", line 1719, in create_model
    checked_model = unchecked_model.checked(self._cache, self.skip_verification, self._workers)
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/model/model.py", line 39, in checked
    unverified = d.checked(declarations, skip_verification=True)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/model/message.py", line 2518, in checked
    result = self.merged(declarations, arguments)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/model/message.py", line 2552, in merged
    message = self._merge_inner_message(message, *inner_message, message_arguments)
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/model/message.py", line 2660, in _merge_inner_message
    proof = merged_condition.check(
            ^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/expression.py", line 292, in check
    return Proof(self, facts)
           ^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/expression.py", line 59, in __init__
    solver.add(self._expr.z3expr())
               ^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/expression.py", line 708, in z3expr
    z3exprs = [t.z3expr() for t in self.terms]
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/expression.py", line 708, in <listcomp>
    z3exprs = [t.z3expr() for t in self.terms]
               ^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/expression.py", line 2352, in z3expr
    raise Z3TypeError(
rflx.expression.Z3TypeError: invalid relation between "ArithRef" and "BoolRef" in Flag = True

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

This seems to be the case anytime I try to add conditional transitions after a field that is a message type.

The code generates successfully if I omit the conditional transition to null on the First_Record field.

The code also generates successfully if Some_Record is changed to a scalar type and I keep the condition.

[treiher]

Thank you for the report! We will take care of this issue. A workaround could be to check the condition at an earlier point:

   type Some_Message is
      message
         Flag         : Boolean
            then Spare_7_Bits
               if Flag = True;
         Spare_7_Bits : Spare_7_Bits;
         First_Record : Some_Record;
      end message;

[NickFoubert]

Thanks for the quick response! My reproducer example wasn't quite the use case I need, in my case the Flag would be to indicate whether another field was present, e.g.:

First_Record : Some_Record
   then Second_Record
      if Flag = True
   then null
     if Flag = False;
Second_Record : Some_Record;

for which I see there is issue #106 which would help if implemented (I don't think #95 quite gives me what I need). At the moment I'm trying to implement it the standard way, but even that isn't working at the moment due to this bug.

[treiher]

I don't have a good workaround for your use case in the current version (0.14.0). It appears that this bug was recently introduced. For the time being, you could try using the previous version (0.13.0).

[treiher]

This bug will be fixed in the next release (0.15.0).