dsp: firmware_update: Run-time state machine for package parsing
Encoding the necessary sequence of calls with an approximation of linear
types is hampered by DSP0267's introduction of entirely new sections
into the package format across revisions. The existing design enforced a
sequence that precluded _not_ calling the decoder for downstream device
records in the case of pinning to format revision 1. The choice had the
further effect of stunting the API to future expansion of the spec.
Switch from linear types to tracking parse state at runtime based on the
provided pin and the extracted package header.
The state machine implementation is modeled on the TLA+ specification
below, with NR_FORMATS set to 4 in the model:
```tla
---- MODULE pldm_package_parser ----
EXTENDS Integers, Sequences
\* pin and format have non-deterministic init, but are then constant
VARIABLE state, pin, format
vars == << state, pin, format >>
States == {
"Init",
"Header",
"FirmwareDevices",
"DownstreamDevices",
"ComponentImageInfos",
"Complete",
"Unsupported",
"Error"
}
Formats == 1..4
DecodeHeader ==
/\ state = "Init"
/\ state' = IF format <= pin THEN "Header" ELSE "Unsupported"
/\ UNCHANGED << pin, format >>
DecodeFirmwareDevices ==
/\ state = "Header"
/\ state' = "FirmwareDevices"
/\ UNCHANGED << pin, format >>
DecodeDownstreamDevices ==
/\ state = "FirmwareDevices"
/\ state' = IF pin = 1 THEN "Error" ELSE "DownstreamDevices"
/\ UNCHANGED << pin, format >>
DecodeComponentImageInfos ==
/\ \/ /\ state = "FirmwareDevices"
/\ pin = 1
\/ /\ state = "DownstreamDevices"
/\ pin \in ( Formats \ { 1 } )
/\ state' = "Complete"
/\ UNCHANGED << pin, format >>
Done == state \in { "Complete", "Unsupported", "Error" } /\ UNCHANGED vars
Init ==
/\ state = "Init"
/\ pin \in Formats
/\ format \in Formats
Next ==
\/ DecodeHeader
\/ DecodeFirmwareDevices
\/ DecodeDownstreamDevices
\/ DecodeComponentImageInfos
\/ Done
Spec == Init /\ [][Next]_vars /\ WF_state(Next)
TypeInvariant ==
/\ state \in States
/\ pin \in Formats
/\ format \in Formats
Safety ==
/\ TypeInvariant
/\ state \in States \ { "Init", "Unsupported" } => format <= pin
Liveness ==
/\ [][(state \in { "Complete", "Unsupported", "Error" } => UNCHANGED state)]_vars
/\ [][UNCHANGED <<pin, format>>]_vars
====
```
For an introduction to TLA+ see https://www.learntla.com/
Note that the implemented state machine does not exactly replicate that
specified in the model. Specifically:
- No "Unsupported" state is defined. Instead, the APIs return -ENOTSUP
- No "Error" state is defined. Instead, the APIs return -EPROTO
It is expected that callers perform appropriate error handling.
Change-Id: Id8780c1f5f130b77e6eea2519b5d5734aa79040e
Signed-off-by: Andrew Jeffery <andrew@codeconstruct.com.au>
diff --git a/tools/pd.c b/tools/pd.c
index fe63a70..d88cea2 100644
--- a/tools/pd.c
+++ b/tools/pd.c
@@ -103,7 +103,7 @@
struct pldm_package_firmware_device_id_record fdrec;
DEFINE_PLDM_PACKAGE_FORMAT_PIN_FR02H(pin);
pldm_package_header_information_pad hdr;
- struct pldm_package_iter iter;
+ struct pldm_package pkg = { 0 };
size_t nr_fdrecs = 0;
size_t nr_ddrecs = 0;
size_t nr_infos = 0;
@@ -119,8 +119,7 @@
}
in = fread(package, 1, PD_PACKAGE_BUFFER, stdin);
- rc = decode_pldm_firmware_update_package(package, in, &pin, &hdr,
- &iter);
+ rc = decode_pldm_firmware_update_package(package, in, &pin, &hdr, &pkg);
if (rc < 0) {
warnx("Failed to parse PLDM package: %s\n",
strerrorname_np(-rc));
@@ -135,7 +134,7 @@
hdr.package_header_format_revision);
fwrite("\n", 1, 1, stdout);
- foreach_pldm_package_firmware_device_id_record(iter, fdrec, rc)
+ foreach_pldm_package_firmware_device_id_record(pkg, fdrec, rc)
{
struct pldm_descriptor desc;
@@ -153,7 +152,7 @@
printf("\tDescriptors:\n");
foreach_pldm_package_firmware_device_id_record_descriptor(
- iter, fdrec, desc, rc)
+ pkg, fdrec, desc, rc)
{
pd_print_descriptor("\t\t", &desc, "\n");
}
@@ -172,7 +171,7 @@
goto cleanup_package;
}
- foreach_pldm_package_downstream_device_id_record(iter, ddrec, rc)
+ foreach_pldm_package_downstream_device_id_record(pkg, ddrec, rc)
{
struct pldm_descriptor desc;
@@ -190,7 +189,7 @@
" ]\n");
printf("\tDescriptors:\n");
foreach_pldm_package_downstream_device_id_record_descriptor(
- iter, ddrec, desc, rc)
+ pkg, ddrec, desc, rc)
{
pd_print_descriptor("\t\t", &desc, "\n");
}
@@ -209,7 +208,7 @@
goto cleanup_package;
}
- foreach_pldm_package_component_image_information(iter, info, rc)
+ foreach_pldm_package_component_image_information(pkg, info, rc)
{
printf("Component image info: %zu\n", nr_infos++);
printf("\tComponent classification: %" PRIu16 "\n",