Re: [Eclair false positive] Re: [PATCH] x86/msr: Rework wrmsr_safe() using asm goto()

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

On 21/05/2025 8:48 pm, Nicola Vetrini wrote:
> On 2025-05-21 21:43, Andrew Cooper wrote:
>> On 21/05/2025 8:21 pm, Nicola Vetrini wrote:
>>> On 2025-05-21 20:00, Andrew Cooper wrote:
>>>> On 21/05/2025 3:36 pm, Andrew Cooper wrote:
>>>>> diff --git a/xen/arch/x86/include/asm/msr.h
>>>>> b/xen/arch/x86/include/asm/msr.h
>>>>> index 0d3b1d637488..4c4f18b3a54d 100644
>>>>> --- a/xen/arch/x86/include/asm/msr.h
>>>>> +++ b/xen/arch/x86/include/asm/msr.h
>>>>> @@ -69,20 +69,20 @@ static inline void wrmsr_ns(uint32_t msr,
>>>>> uint32_t lo, uint32_t hi)
>>>>>  /* wrmsr with exception handling */
>>>>>  static inline int wrmsr_safe(unsigned int msr, uint64_t val)
>>>>>  {
>>>>> -    int rc;
>>>>> -    uint32_t lo, hi;
>>>>> -    lo = (uint32_t)val;
>>>>> -    hi = (uint32_t)(val >> 32);
>>>>> -
>>>>> -    __asm__ __volatile__(
>>>>> -        "1: wrmsr\n2:\n"
>>>>> -        ".section .fixup,\"ax\"\n"
>>>>> -        "3: movl %5,%0\n; jmp 2b\n"
>>>>> -        ".previous\n"
>>>>> -        _ASM_EXTABLE(1b, 3b)
>>>>> -        : "=&r" (rc)
>>>>> -        : "c" (msr), "a" (lo), "d" (hi), "0" (0), "i" (-EFAULT));
>>>>> -    return rc;
>>>>> +    uint32_t lo = val, hi = val >> 32;
>>>>> +
>>>>> +    asm_inline goto (
>>>>> +        "1: wrmsr\n\t"
>>>>> +        _ASM_EXTABLE(1b, %l[fault])
>>>>> +        :
>>>>> +        : "a" (lo), "c" (msr), "d" (hi)
>>>>> +        :
>>>>> +        : fault );
>>>>> +
>>>>> +    return 0;
>>>>> +
>>>>> + fault:
>>>>> +    return -EFAULT;
>>>>>  }
>>>>
>>>> It turns out this is the first piece of Eclair-scanned code using asm
>>>> goto.
>>>>
>>>> https://gitlab.com/xen-project/hardware/xen-staging/-/jobs/10108558677
>>>> (The run also contained an equivalent change to xsetbv())
>>>>
>>>> We're getting R1.1 and R2.6 violations.
>>>>
>>>> R1.1 complains about [STD.adrslabl] "label address" not being valid
>>>> C99.
>>>>
>>>> R2.6 complains about unused labels.
>>>>
>>>> I expect this means that Eclair doesn't know how to interpret asm
>>>> goto()
>>>> yet.  The labels listed are reachable from inside the asm block.
>>>>
>>>> From a qualification point of view, this allows for some extensive
>>>> optimisations dropping emitted code.
>>>>
>>>
>>> Hi Andrew,
>>>
>>> R1.1 is easy to fix, I'll send a patch myself. On R2.6 you are
>>> probably right. I suggest marking the rule not clean to unblock while
>>> we investigate. It should not be hard to fix this FP.
>>
>> I've not committed the patch yet, so staging is still green.
>>
>> But, it occurs to me that this is not the first asm goto() to be scanned
>> by Eclair.  There's wrmsr_amd_safe() in amd.c (c/s b3d8b3e3f3aa from ~6w
>> ago) using exactly the same pattern, which has been passing just fine.
>>
>> Clearly something else is relevant in terms of triggering violations.
>>
>> ~Andrew
>
> I think the reason it's simply that file being out of scope due to
> being imported from Linux (whether that is still true I don't know),
> which is unfortunate. We ought to revise that list
> (docs/misra/exclude-list.json).
>

Oh, that.  Anyone who takes a cursory look at amd.c will find it has
diverged entirely from Linux.

If I were an examiner, I wouldn't accept such a claim for being out of
scope...

~Andrew