From 63738d107404b90a22f1e19ac3801fa3c51335c3 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 29 Aug 2024 14:07:45 +0200 Subject: [PATCH] Fix initialization of SPDM responder Ref. eng/recordflux/RecordFlux!1663 --- .../apps/spdm_responder/src/lib/responder.adb | 13 ++++++----- .../src/lib/rflx-spdm_responder-session.adb | 22 ------------------- ...flx-spdm_responder-session_environment.adb | 16 ++++++++++++++ ...flx-spdm_responder-session_environment.ads | 13 ++++++++++- 4 files changed, 36 insertions(+), 28 deletions(-) create mode 100644 examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.adb diff --git a/examples/apps/spdm_responder/src/lib/responder.adb b/examples/apps/spdm_responder/src/lib/responder.adb index 003a9e2f9..c8180a5de 100644 --- a/examples/apps/spdm_responder/src/lib/responder.adb +++ b/examples/apps/spdm_responder/src/lib/responder.adb @@ -1,4 +1,5 @@ with RFLX.SPDM_Responder.Session.FSM; +with RFLX.SPDM_Responder.Session_Environment; with RFLX.RFLX_Types; with RFLX.RFLX_Types.Operators; @@ -9,8 +10,11 @@ is use RFLX.RFLX_Types; use RFLX.RFLX_Types.Operators; + package SR renames RFLX.SPDM_Responder.Session.FSM; + package Session_Environment renames RFLX.SPDM_Responder.Session_Environment; + Buffer : Bytes (Index'First .. Index'First + 1279) := (others => 0); - Context : RFLX.SPDM_Responder.Session.FSM.Context; + Context : SR.Context; function Uninitialized return Boolean is (RFLX.SPDM_Responder.Session.FSM.Uninitialized (Context)); @@ -29,13 +33,11 @@ is procedure Responder_Main is - package SR renames RFLX.SPDM_Responder.Session.FSM; begin loop - -- Eng/RecordFlux/RecordFlux#1032 - -- Context.Plat_Initialize; pragma Loop_Invariant (SR.Uninitialized (Context)); + Session_Environment.Plat_Initialize (Context.E); SR.Initialize (Context); while SR.Active (Context) loop @@ -70,5 +72,6 @@ is SR.Finalize (Context); end loop; end Responder_Main; - +begin + Session_Environment.Plat_Initialize (Context.E); end Responder; diff --git a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb index bb6f85223..e43933c9a 100644 --- a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb +++ b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb @@ -18,28 +18,6 @@ with RFLX.SPDM_Responder.Session_Environment; package body RFLX.SPDM_Responder.Session with SPARK_Mode is - - -- Ensure initialization of State.Instance. - -- - -- This procedure is both implemented and called by the platform code. It is - -- called before the start of the state machine and ensures that - -- RFLX.SPDM_Responder.Session_Environment.State.Instance is initialized. It - -- is not necessary for the state machine to function. If the platform code - -- has other means of initializing the - -- RFLX.SPDM_Responder.Session_Environment.State this procedure can be - -- removed. - -- - -- @param State RFLX.SPDM_Responder.Session_Environment.State. - procedure Plat_Initialize (State : in out RFLX.SPDM_Responder.Session_Environment.State) - is - procedure C_Interface (Instance : out System.Address) with - Import, - Convention => C, - External_Name => "spdm_platform_initialize"; - begin - C_Interface (State.Instance); - end Plat_Initialize; - -- Return CT exponent (DSP0274_1.1.0 [178]). -- -- @param State RFLX.SPDM_Responder.Session_Environment.State. diff --git a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.adb b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.adb new file mode 100644 index 000000000..080b2b64a --- /dev/null +++ b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.adb @@ -0,0 +1,16 @@ +package body RFLX.SPDM_Responder.Session_Environment with + SPARK_Mode +is + + procedure Plat_Initialize (State : out Session_Environment.State) with + SPARK_Mode => Off + is + procedure C_Interface (Instance : out System.Address) with + Import, + Convention => C, + External_Name => "spdm_platform_initialize"; + begin + C_Interface (State.Instance); + end Plat_Initialize; + +end RFLX.SPDM_Responder.Session_Environment; diff --git a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.ads b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.ads index a04844ec9..f64b52d75 100644 --- a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.ads +++ b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.ads @@ -12,7 +12,18 @@ is -- implementer. type State is record - Instance : System.Address := System.Null_Address; + Instance : System.Address; end record; + -- Initialize State. + -- + -- This procedure is implemented by the platform code. It must be called + -- before the start of the state machine to ensure that State.Instance is + -- initialized. If all components of State are initialized by default, this + -- procedure can be removed. + -- + -- @param State Session_Environment.State. + procedure Plat_Initialize (State : out Session_Environment.State) with + Always_Terminates; + end RFLX.SPDM_Responder.Session_Environment;