On 20/07/23 17:54, Julien Grall wrote:
Hi Nicola,
On 20/07/2023 15:29, Nicola Vetrini wrote:
The local variables with type 'struct arm_smccc_res' are initialized
just after the declaration to avoid any possible read usage prior
to any write usage, which would constitute a violation of
MISRA C:2012 Rule 9.1.
This is already prevented by suitable checks in the code,
but the correctness of this approach is difficult to prove and
reason about.
So I looked at the implementation of arm_smccc_smc(). For arm64, it is
(simplified):
if ( cpus_have_const_cap(ARM_SMCCC_1_1) )
arm_smccc_1_1_smc(__VA_ARGS__);
else
arm_smccc_1_0_smc(_VA_ARGS__);
In arm_smccc_1_1_smc(), we will explicitly initialize __res:
if ( ___res )
*___res = (typeof(*___res)) {r0, r1, r2, r3};
Whereas for arm_smccc_1_0_smc(), we would call assembly function. I
assuming this is the problem?
I think this is similar to the discussion we had on set_interrupts() and
dt_set_cells(). If so, couldn't we tell ECLAIR that
__arm_smccc_1_0_smc() will always initialize *res?
This is slightly different because of the chained variadic macro
expansions of arm_smccc_smc. I could have stated that arm_smccc_smc
initializes its args, but because it's variadic I can't narrow it down
to a specific index, therefore the property is not correct, because the
input arguments are instead expected to be read by the macro. The same
reasoning applies for all variadic macros that have some input and
output parameters, not just this one.
In the end, if these were fixed-argument functions or macros we can aim
for that, and that would obsolete this patch.
Regards,
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)