Re: [XEN PATCH] xen/arm: optee: provide an initialization for struct arm_smccc_res

[Julien Grall <julien@xxxxxxx>]

Hi,

On 21/07/2023 08:28, Nicola Vetrini wrote:
> 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.
They are all ending up to call a fixed-argument macro 
(__arm_smccc_1_0_smc_7()) and then function __arm_smccc_1_0_smc().
Are you suggesting that this would still not be enough for Eclair?

Cheers,

--
Julien Grall