RecordFlux
RecordFlux copied to clipboard
Published
20 hours ago •
AdaCore
AdaCore
Setting a sequence field by referring to a sequence field of a message
When I try to edit a message in a session by assigning it to itself and editing the fields as follows
Response := SPDM::Response'
(Meas_Cap => Response.Meas_Cap,
Hash_Type => Response.Hash_Type,
Hash_Length => Response.Hash_Length,
Signature_Length => Signature_Length,
Exchange_Data_Length => Response.Exchange_Data_Length,
Handshake_In_The_Clear => Response.Handshake_In_The_Clear,
Major_Version => Response.Major_Version,
Minor_Version => Response.Minor_Version,
Code => Response.Code,
Measurements_Response_Number_Of_Indices => Response.Measurements_Response_Number_Of_Indices,
Measurements_Response_Reserved_1 => 0,
Measurements_Response_Slot_ID => Response.Measurements_Response_Slot_ID,
Measurements_Response_Number_Of_Blocks => Response.Measurements_Response_Number_Of_Blocks,
Measurements_Response_Measurement_Record_Length =>
Response.Measurements_Response_Measurement_Record_Length,
Measurements_Response_Measurement_Record => Response.Measurements_Response_Measurement_Record,
Measurements_Response_Nonce_Data => Response.Measurements_Response_Nonce_Data,
Measurements_Response_Opaque_Length => Response.Measurements_Response_Opaque_Length,
Measurements_Response_Opaque_Data => Response.Measurements_Response_Opaque_Data,
Measurements_Response_Signature => Signature.Data);
I get the following error:
------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.10.0
z3-solver 4.8.15.0
pydotplus 2.0.2
ruamel.yaml 0.17.21
attrs 21.4.0
pydantic 1.9.0
icontract 2.6.1
Optimized: False
Command: /tmp/tmp.QgcLtdI4Iq/venv/bin/rflx --no-verification generate specs/spdm.rflx specs/spdm_responder.rflx specs/spdm_emu.rflx specs/spdm_proxy.rflx --debug -d build/debug/generated
Traceback (most recent call last):
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/cli.py", line 201, in main
args.func(args)
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/cli.py", line 259, in generate
generator = Generator(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 175, in __init__
self.__generate(model, integration)
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 250, in __generate
self.__create_session(s, integration)
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 261, in __create_session
session_generator = SessionGenerator(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 219, in __init__
self._create()
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 249, in _create
state_machine = self._create_state_machine()
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 357, in _create_state_machine
unit += self._create_states(self._session, composite_globals, is_global)
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 844, in _create_states
*[
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 847, in <listcomp>
for s in self._state_action(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 1893, in _state_action
result = self._assign(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 2123, in _assign
return self._assign_to_message_aggregate(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 2397, in _assign_to_message_aggregate
*self._set_message_fields(
File "/tmp/tmp.QgcLtdI4Iq/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 3697, in _set_message_fields
assert target_field_type == rty.OPAQUE
AssertionError
----------------------------------------------------------------------------
It is not yet possible to set a sequence field by referring to a sequence field of another message. A workaround could be storing the sequence in a temporary variable.
I can still reproduce the issue with the following spec:
package Test is
type Element is mod 2 ** 8;
type List is sequence of Element;
type Message is
message
Data : List
with Size => 32;
end message;
generic
Channel : Channel with Readable, Writable;
session Session with
Initial => Start,
Final => Terminated
is
Msg_1 : Message;
Msg_2 : Message;
begin
state Start
is
begin
Channel'Read (Msg_1);
transition
goto Process
end Start;
state Process
is
begin
Msg_1.Data := Msg_2.Data;
transition
goto Send
exception
goto Terminated
end Process;
state Send
is
begin
Channel'Write (Msg_2);
transition
goto Terminated
end Send;
state Terminated is null state;
end Session;
end Test;
The spec is checked as valid but I get the following error:
python3 bin/rflx generate test.rflx -d out [55/698]
Parsing test.rflx
Processing Test
Generating Test::Element
Generating Test::List
Generating Test::Message
Generating Test::Session
------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.1.dev6+g69d65226
RecordFlux-parser 0.11.0
attrs 21.4.0
icontract 2.6.2
pydantic 1.9.2
pydotplus 2.0.2
ruamel.yaml 0.17.21
z3-solver 4.10.2.0
Optimized: False
Command: bin/rflx generate test.rflx -d out
Traceback (most recent call last):
File "/.../RecordFlux/rflx/cli.py", line 215, in main
args.func(args)
File "/.../RecordFlux/rflx/cli.py", line 273, in generate
Generator(
File "/.../RecordFlux/rflx/generator/generator.py", line 142, in generate
units = self._generate(model, integration)
File "/.../RecordFlux/rflx/generator/generator.py", line 265, in _generate
units.update(self._create_session(s, integration))
File "/.../RecordFlux/rflx/generator/generator.py", line 282, in _create_session
session_generator = SessionGenerator(
File "/.../RecordFlux/rflx/generator/session.py", line 188, in __init__
self._create()
File "/.../RecordFlux/rflx/generator/session.py", line 218, in _create
state_machine = self._create_state_machine()
File "/.../RecordFlux/rflx/generator/session.py", line 338, in _create_state_machine
unit += self._create_states(self._session, composite_globals, is_global)
File "/.../RecordFlux/rflx/generator/session.py", line 822, in _create_states
*[
File "/.../RecordFlux/rflx/generator/session.py", line 825, in <listcomp>
for s in self._state_action(
File "/.../RecordFlux/rflx/generator/session.py", line 1961, in _state_action
result = self._assign_message_field(
File "/.../RecordFlux/rflx/generator/session.py", line 3421, in _assign_message_field
*self._set_message_field(
File "/.../RecordFlux/rflx/generator/session.py", line 4334, in _set_message_field
assert field_type == rty.OPAQUE
AssertionError