PyRFLX cannot handle sequence in comparison

[rssen]

Trying to parse a message using PyRFLX and the following specificaton fails with this error:

AssertionError: unresolved field conditions in Test.Fld_A: Fld_A = [16#1#, 16#2#], Fld_A /= [16#1#, 16#2#]

package Test is

   type B is mod 2 ** 8;

   type Test is
      message
         Fld_A : Opaque
            with Size => 16
            then Fld_B
               if Fld_A /= [16#01#, 16#02#]
            then null
               if Fld_A = [16#01#, 16#02#];
         Fld_B : B;
      end message;

end Test;

This occurs because the __simplified function of typevalue.py cannot handle the list in the comparison.

This could also be observed with the TLS handshake specification, see Componolit/RecordFlux-specifications#105.

Test data: test_data.zip

[senier]

@rssen Thanks for the reproducer. Do you think you can fix that?

[rssen]

When checking the below variation of the specification from above the following errors are raised:

test.rflx:10:28: model: error: expected sequence type "__INTERNAL__::Opaque" with element integer type "Byte" (0 .. 255)
test.rflx:10:28: model: info: found type universal integer (2)
test.rflx:10:19: model: info: on path Fld_A -> Fld_B
test.rflx:12:27: model: error: expected sequence type "__INTERNAL__::Opaque" with element integer type "Byte" (0 .. 255)
test.rflx:12:27: model: info: found type universal integer (2)
test.rflx:12:19: model: info: on path Fld_A -> Final

package Test is

   type B is mod 2 ** 8;

   type Test is
      message
         Fld_A : Opaque
            with Size => 16
            then Fld_B
               if Fld_A /= 16#02#
            then null
               if Fld_A = 16#02#;
         Fld_B : B;
      end message;

end Test;

Is this expected? I am not really sure what the error message is trying to tell me either.

When trying to parse a message using this specification (checks disabled) a similar error as decribed above is raised: AssertionError: unresolved field conditions in Test.Fld_A: Fld_A = 16#2#, Fld_A /= 16#2#.
This error is raised because Fld_A is not correctly simplified in the _simplified method of Relation(BinExpr) in expression.py. This is also the case for the original reproducer and seems to be part of the problem in addition to the sequences not beeing correctly handled.
When checking the original reproducer with rflx check no error is raised.

[treiher]

Is this expected? I am not really sure what the error message is trying to tell me either.

Yes, the error message describes type errors in the two link conditions. Field Fld_A is of type Opaque, which represents an arbitrary sequence of bytes. #16#02 is a numeric literal, which is interpreted as universal integer during type checking. An opaque type cannot be compared to a universal integer, which is done in Fld_A /= 16#02#. In the original reproducer, [16#01#, 16#02#] is used, which is an aggregate that represents a sequence of two bytes. Opaque fields can only be compared to aggregates (or other opaque fields).

This error is raised because Fld_A is not correctly simplified in the _simplified method of Relation(BinExpr) in expression.py. This is also the case for the original reproducer and seems to be part of the problem in addition to the sequences not beeing correctly handled.

That is probably the root cause. Fld_A in Fld_A = [16#1#, 16#2#] would need to be replaced by its bytes representation, so that the relation can be resolved to TRUE or FALSE.

When checking the original reproducer with rflx check no error is raised.

That seems correct to me.

[rssen]

Thank you for the explanation.

[rssen]

I implemented a solution that fixes the problem, but it is very specific to this single usecase where we have a BinExpr with a Variable on the left and an Aggregate on the right side of the expression.
@treiher Should the solution be more generic? Can you think of any other expression (other than a single Variable) that could be on the left side of the BinExpr?
I already checked the following, but these make the specification invalid:

• Fld_A + Fld_0 = [16#01#, 16#02#] where Fld_0 is an opaque field of static size 8 before Fld_A, and Fld_A is of size 8.
• Fld_A + 1 = [16#01#, 16#02#]

[treiher]

In the code generator, we support the following variants:

https://github.com/Componolit/RecordFlux/blob/f81d80fb965e88964346e115991def9d70de177a/tests/integration/specification_model_generator_test.py#L73-L102

Note that concatenations are just syntactic sugar and are converted to an aggregate during parsing, and strings are also (a special form of) aggregates.

The same variants should be supported by PyRFLX. So supporting BinExpr consisting of an Aggregate and a Variable on either side should be sufficient.

[rssen]

@treiher the coverage test is failing because of apparently untested lines that are completely unrelated to this issue and that I did not modify. Should I make a PR anyway or attempt to fix it in this issue? I have had a quick look at it and it seems to be not "easily testable". The uncovered lines are 1157-1164 in typevalue.py.

[treiher]

Are you sure the uncovered code is completely unrelated? As it was covered before, there must be a relation to your changes. Could it be that the uncovered code is now obsolete?