Bug box due to dangling field when merging messages

[treiher]

package Test is

   type T is range 0 .. 3 with Size => 8;

   type I is
      message
         A : T;
      end message;

   type O is
      message
         C : I
            then null
               if C_A /= 4
            then D
               if C_A = 4;
         D : T;
      end message;

end Test;

Checking this specification with assertion leads to a bug box:

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.10.0
attrs 21.4.0
icontract 2.6.0
pydantic 1.9.0
pydotplus 2.0.2
ruamel.yaml 0.17.20
z3-solver 4.8.14.0

Optimized: False

Command: /home/devel/Componolit/RecordFlux/venv/bin/rflx check reproduce.rflx

Traceback (most recent call last):
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 201, in main
    args.func(args)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 242, in check
    parse(args.files, args.no_verification, args.workers)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 300, in parse
    model = parser.create_model()
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1595, in create_model
    self.__evaluate_specification(error, spec_node.spec, spec_node.filename)
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1653, in __evaluate_specification
    new_type = handlers[t.f_definition.kind_name](
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 829, in create_message
    ).merged(message_arguments),
  File "/home/devel/Componolit/RecordFlux/venv/lib/python3.10/site-packages/icontract/_checkers.py", line 641, in wrapper
    result = func(*args, **kwargs)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 1953, in merged
    message = self._merge_inner_message(message, *inner_message, message_arguments)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 2071, in _merge_inner_message
    return message.copy(structure=structure, types=types, byte_order=byte_order)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 1913, in copy
    return UnprovenMessage(
  File "/home/devel/Componolit/RecordFlux/venv/lib/python3.10/site-packages/icontract/_checkers.py", line 810, in wrapper
    result = func(*args, **kwargs)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 165, in __init__
    assert all(f in self.fields for f in byte_order)
AssertionError

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

Without assertions, D is detected as unreachable field:

test.rflx:17:10: model: error: unreachable field "D" in "Test::O"

[treiher]

If I remember correctly, the removal of dangling fields when merging messages (cf. https://github.com/Componolit/RecordFlux/blob/main/rflx/model/message.py#L2178-L2197) was mainly added for the fuzzer. @jklmnn @senier Should D be detected as dangling field in this specific case? If not, for which cases was the removal of dangling fields intended? (We should document that.) I don't think it would be a good idea to silently remove field D in this specific case.

[jklmnn]

Tbh I can't remember when and why we introduced that particular feature. Just looking at the example I think the field should not be removed and the warning about the unreachable field should be generated.

[senier]

Apparently I added that functionality in 39e3109 as part of #410. Tbh, I have no recollection. @treiher Maybe your concerns we're justified...
I think removing false conditions from merged message will be necessary in some situations. However, when this leads to dangling fields we should detect it and create a proper error message.

[treiher]

In a separate discussion, we decided to just fix the assertion error for the time being. The pruning of dangling fields may be changed in the future (cf. #1034).