Endianness #104
Comments
|
@KOLANICH Thanks for the pointers! This is quite a lengthy discussion and a lot of information to digest. As our DSL is influenced heavily by Ada (and the SPARK subset of Ada is also our target language), we will probably try to stay syntactically close to what the Ada community is doing. Here is a discussion on how they handle the endianness issue. |
|
Here is a first design. Language designA message type definition can have an aspect
This corresponds to the Ada/GNAT aspect/attribute. Implementation changes
This last part looks quite hard as the code is already intricate. But the change is very local and can be easily unit-tested. |
|
P.S. In our discussion with @senier I was surprised that we wanted to support little endian even if the field is not byte-aligned. But having looked at the code now I understand things better. It's not obvious how we would benefit from such a restriction even if we introduced it. |
I agree, we should not introduce any restriction if there is no benefit.
I think the aspect should be called
I think the parameter should be called
I agree. It would make sense to get some samples from real-world messages to validate the implementation. SPDM would be a sensible option. |
The advantage would be that the Byte_Order is specified by the client at one point only, so we can avoid the mistake where different byte orderings would be used throughout the application. I have updated the design to reflect your comments. |
|
|
I'm OK with a non-generic parameter. I'm updating the design. |
|
Summary from our live discussion. The |
|
Coming back to this point. Is it really worthwhile to have a single |
|
Checking in here before I go any further to avoid losing time working in a wrong direction. I have written a version of function U64_Extract_Little
(Data : Bytes;
Off : Offset;
Value_Size : Positive) return U64 with
Pre =>
(Value_Size in 1 .. U64'Size
and then Long_Integer ((Natural (Off) + Value_Size - 1) / Byte'Size) < Data'Length
and then (Natural (Off) + Value_Size - 1) / Byte'Size <= Natural'Size
and then (Byte'Size - Natural (Off) mod Byte'Size) < Long_Integer'Size - 1),
Post =>
(if Value_Size < U64'Size then U64_Extract_Little'Result < 2**Value_Size)
is
LSE_Index : constant Index := Index (Natural (Data'Last) - Natural (Off) / Byte'Size);
MSE_Index : constant Index := Index (Natural (Data'Last) - (Natural (Off) + Value_Size - 1) / Byte'Size);
LSE_Offset : constant Natural := Natural (Natural (Off) mod Byte'Size);
LSE_Size : constant Natural := Byte'Size - LSE_Offset;
MSE_Size : constant Natural := (LSE_Offset + Value_Size + Byte'Size - 1) mod Byte'Size + 1;
Result : U64 := 0;
Bits : Natural with Ghost;
-- Data is assumed to contain Amount bits of information. We append
-- those bits to the current value of Result. We also update the Bits
-- ghost variable.
procedure Shift_Add (Data : U64; Amount : Natural)
with Pre => Bits < U64'Size and then Amount < U64'Size and then Result < 2 ** Bits and then U64'Size - Amount >= Bits and then Data < 2 ** Amount,
Post => (if Bits < U64'Size then Result < 2 ** Bits) and then Bits = Bits'Old + Amount;
procedure Shift_Add (Data : U64; Amount : Natural) is
begin
Result := Shift_Left (Result, Amount) + Data;
Bits := Bits + Amount;
end Shift_Add;
pragma Warnings (Off, "postcondition does not check the outcome of calling ""Lemma_Bound_And""");
procedure Lemma_Bound_And (X : U64; Bound : Natural)
with Pre => Bound < U64'Size,
Post => (X and (2 ** Bound - 1)) < 2 ** Bound
is
begin
null;
end Lemma_Bound_And;
pragma Warnings (On, "postcondition does not check the outcome of calling ""Lemma_Bound_And""");
begin
-- This function simply iterates over all data bytes that contain
-- relevant data, from most significant to least significant, and adds
-- them up in Result, shifting the Result before the addition as needed
-- (see helper function Shift_Add).
-- The ghost variable Bits stores the number of bits that are contained
-- in Result. This is useful to bound the -- current value of Result by
-- 2 ** Bits. At the end of the function, Bits = Value_Size.
-- We start with the most significant byte, which is LSE_Index in little
-- endian. We need to take into account the case where this is the
-- last/only byte.
declare
Tmp : U64 := Byte'Pos (Data (LSE_Index));
begin
if LSE_Index = MSE_Index then
Tmp := Tmp and (2 ** MSE_Size - 1);
end if;
Tmp := Shift_Right (Tmp, LSE_Offset);
Result := Result + Tmp;
end;
-- If it was the only byte, we are done.
if LSE_Index = MSE_Index then
return Result;
end if;
-- The Bits variable is not needed for the previous early return, so we
-- update it only here. Also, setting it to LSE_Size is only correct if
-- we did not return early, so this is the best place to update it.
Bits := LSE_Size;
-- We now iterate over the "inner bytes" excluding the two extreme bytes.
for I in reverse MSE_Index + 1 .. LSE_Index - 1 loop
pragma Loop_Invariant
(Bits = Natural (LSE_Index - I) * Byte'Size - LSE_Offset
and then Result < 2 ** Bits);
Shift_Add (Byte'Pos (Data (I)), Byte'Size);
end loop;
-- We now add the relevant bits from the last byte (MSE_Index in little
-- endian). Some helper assertions and a lemma are needed.
pragma Assert (MSE_Size < U64'Size);
Lemma_Bound_And (Byte'Pos (Data (MSE_Index)), MSE_Size);
Shift_Add (Byte'Pos (Data (MSE_Index)) and (2 ** MSE_Size - 1), MSE_Size);
pragma Assert (Bits = Value_Size);
pragma Assert (if Bits < U64'Size then Result < 2 ** Bits);
return Result;
end U64_Extract_Little;Some comments:
Going forward, my next steps would be:
Any opinions on this before I go any further? |
I think it is fine to have separate functions for LE and BE. Nevertheless, both functions should not be completely different, but use the same approach.
I suppose that will not be a viable solution at the moment, as our CI pipeline uses Community 2021 which does not include Colibri. I don't think we can easily switch to another version. Not testing it in the CI pipeline is also not an option.
As far as I remember, we did not use the built-in shift functions, because they did not have the necessary contracts to prove anything about their results. Isn't this the case in Community 2021 anymore?
That makes sense. Ideally, all the |
I was using the Community 2021 for my experiments. It contains Colibri, but was not advertised as it was still experimental. But I don't think there were any known unsoundnesses. If not acceptable I can also try to eliminate colibri from the required provers.
The built-in Shift functions have had the relevant contracts for quite a while I think, and definitely in CE 2021. |
I see. If you don't see an increased probability of soundness issues by enabling Colibri, I think it is fine to use it. |
Also, bump version to 0.10.0 For AdaCore/RecordFlux#104
Also, bump version to 0.10.0 For AdaCore/RecordFlux#104
Use the correct Insert/Extract functions depending on the Byte_Order specification of the message. Adding a test. This requires Recordflux-parser 0.10.0
Use the correct Insert/Extract functions depending on the Byte_Order specification of the message. Adding a test. This requires Recordflux-parser 0.10.0
|
Here are some tests for the changes on PyRFLX: diff --git a/tests/data/fixtures/pyrflx.py b/tests/data/fixtures/pyrflx.py
index 840cbee23..b80b68bd0 100644
--- a/tests/data/fixtures/pyrflx.py
+++ b/tests/data/fixtures/pyrflx.py
@@ -27,6 +27,7 @@ def fixture_pyrflx() -> pyrflx.PyRFLX:
f"{SPEC_DIR}/message_type_size_condition.rflx",
f"{SPEC_DIR}/always_valid_aspect.rflx",
f"{SPEC_DIR}/parameterized.rflx",
+ f"{SPEC_DIR}/endianness.rflx",
],
skip_model_verification=True,
)
@@ -225,3 +226,8 @@ def fixture_always_valid_aspect_value(
@pytest.fixture(name="parameterized_package", scope="session")
def fixture_parameterized_package(pyrflx_: pyrflx.PyRFLX) -> pyrflx.Package:
return pyrflx_.package("Parameterized")
+
+
+@pytest.fixture(name="endianness_package", scope="session")
+def fixture_endianness_package(pyrflx_: pyrflx.PyRFLX) -> pyrflx.Package:
+ return pyrflx_.package("Endianness")
diff --git a/tests/data/specs/endianness.rflx b/tests/data/specs/endianness.rflx
new file mode 100644
index 000000000..1ad326d0c
--- /dev/null
+++ b/tests/data/specs/endianness.rflx
@@ -0,0 +1,31 @@
+package Endianness is
+
+ type Tag is (None => 1, Data => 2) with Size => 16;
+ type Length is range 0 .. 2 ** 14 - 1 with Size => 16;
+
+ type Message is
+ message
+ Tag : Tag
+ then null
+ if Tag = None
+ then Length
+ if Tag = Data;
+ Length : Length;
+ Payload : Opaque
+ with Size => Length * 8;
+ end message;
+
+ type Message_LE is
+ message
+ Tag : Tag
+ then null
+ if Tag = None
+ then Length
+ if Tag = Data;
+ Length : Length;
+ Payload : Opaque
+ with Size => Length * 8;
+ end message
+ with Byte_Order => Low_Order_First;
+
+end Endianness;
diff --git a/tests/unit/pyrflx_test.py b/tests/unit/pyrflx_test.py
index 3d6575f8a..efdd12917 100644
--- a/tests/unit/pyrflx_test.py
+++ b/tests/unit/pyrflx_test.py
@@ -1439,3 +1439,67 @@ def test_json_serialization() -> None:
opaque_value = OpaqueValue(Opaque())
opaque_value.assign(b"RecordFlux")
assert opaque_value.as_json() == b"RecordFlux"
+
+
+def test_message_endianness_parse_be(endianness_package: Package) -> None:
+ message = endianness_package.new_message("Message")
+
+ message.parse(b"\x00\x01")
+
+ assert message.valid_message
+ assert message.get("Tag") == "None"
+
+ message.parse(b"\x00\x02\x00\x04\x01\x02\x03\x04")
+
+ assert message.valid_message
+ assert message.get("Tag") == "Data"
+ assert message.get("Length") == 4
+ assert message.get("Payload") == b"\x01\x02\x03\x04"
+
+
+def test_message_endianness_parse_le(endianness_package: Package) -> None:
+ message_le = endianness_package.new_message("Message_LE")
+
+ message_le.parse(b"\x01\x00")
+
+ assert message_le.valid_message
+ assert message_le.get("Tag") == "None"
+
+ message_le.parse(b"\x02\x00\x04\x00\x01\x02\x03\x04")
+
+ assert message_le.valid_message
+ assert message_le.get("Tag") == "Data"
+ assert message_le.get("Length") == 4
+ assert message_le.get("Payload") == b"\x01\x02\x03\x04"
+
+
+def test_message_endianness_set_be(endianness_package: Package) -> None:
+ message = endianness_package.new_message("Message")
+
+ message.set("Tag", "None")
+
+ assert message.valid_message
+ assert message.bytestring == b"\x00\x01"
+
+ message.set("Tag", "Data")
+ message.set("Length", 4)
+ message.set("Payload", b"\x01\x02\x03\x04")
+
+ assert message.valid_message
+ assert message.bytestring == b"\x00\x02\x00\x04\x01\x02\x03\x04"
+
+
+def test_message_endianness_set_le(endianness_package: Package) -> None:
+ message_le = endianness_package.new_message("Message_LE")
+
+ message_le.set("Tag", "None")
+
+ assert message_le.valid_message
+ assert message_le.bytestring == b"\x01\x00"
+
+ message_le.set("Tag", "Data")
+ message_le.set("Length", 4)
+ message_le.set("Payload", b"\x01\x02\x03\x04")
+
+ assert message_le.valid_message
+ assert message_le.bytestring == b"\x02\x00\x04\x00\x01\x02\x03\x04" |
|
Thanks, that helps a lot. I was able to modify pyrflx to pass your tests, though I'm not confident in my patch ... I will put it on review when the other patches are through. |
Use the correct Insert/Extract functions depending on the Byte_Order specification of the message. Adding a test. This requires Recordflux-parser 0.10.0
Also, bump version to 0.10.0 For #104
Currently the parsing is done only in big endian (network byte order). It should also be possible to specify host byte order (or more explicitly little endian).
Work items:
The text was updated successfully, but these errors were encountered: