Re: [Qemu-devel] [PULL 08/10] target/arm: Conditionalize some asserts on aarch32 support

[Laszlo Ersek <lersek@redhat.com>]

On 07/17/19 10:36, Laszlo Ersek wrote:
> On 07/16/19 22:10, Philippe Mathieu-Daudé wrote:
>> On 7/16/19 8:42 PM, Laszlo Ersek wrote:
>>> On 07/16/19 18:59, Peter Maydell wrote:
>>>> On Tue, 16 Jul 2019 at 17:51, Laszlo Ersek <lersek@redhat.com>
>>>> wrote:
>>>>> The issue still reproduces, so it makes sense for me to look at
>>>>> the host kernel version... Well, I'm afraid it won't help much,
>>>>> for an upstream investigation:
>>>>>
>>>>>   4.14.0-115.8.2.el7a.aarch64
>>>>>
>>>>> This is the latest released kernel from "Red Hat Enterprise Linux
>>>>> for ARM 64 7".
>>>>
>>>> OK. (I'm using 4.15.0-51-generic from ubuntu).
>>>>
>>>> Could you run with QEMU under gdb, and when it hits the
>>>> assertion go back up a stack frame to the arm_cpu_realizefn()
>>>> frame, and then "print /x cpu->isar" ? That should show us
>>>> what we think we've got as ID registers from the kernel.
>>>> (You might need to build QEMU with --enable-debug to get
>>>> useful enough debug info to do that, not sure.)
>>>
>>> (My qemu build script always builds QEMU in two configs, the
>>> difference being --prefix and --enable-debug.)
>>>
>>> This is what I got:
>>>
>>> (gdb) frame 4
>>> #4  0x00000000006a063c in arm_cpu_realizefn (dev=0x1761140,
>>>     errp=0xffffffffe540)
>>>     at .../qemu/target/arm/cpu.c:1159
>>> 1159            assert(no_aa32 || cpu_isar_feature(arm_div, cpu));
>>> (gdb) print /x cpu->isar
>>> $1 = {id_isar0 = 0x0, id_isar1 = 0x0, id_isar2 = 0x0, id_isar3 = 0x0,
>>>   id_isar4 = 0x0, id_isar5 = 0x0, id_isar6 = 0x0, mvfr0 = 0x0,
>>>   mvfr1 = 0x0, mvfr2 = 0x0, id_aa64isar0 = 0x0, id_aa64isar1 = 0x0,
>>>   id_aa64pfr0 = 0x11, id_aa64pfr1 = 0x0, id_aa64mmfr0 = 0x0,
>>>   id_aa64mmfr1 = 0x0}
>>
>> For ISAR0, DIVIDE=0
>>
>> so cpu_isar_feature(arm_div, cpu)=false
>>
>> For AA64PFR0, EL0=1, EL1=1.
>>
>> EL0 = 1: EL0 can be executed in AArch64 state only.
>> EL1 = 1: EL1 can be executed in AArch64 state only.
>>
>> so cpu_isar_feature(aa64_aa32, cpu)=false
>> then no_aa32=true
>>
>> The commit description is "on a host that doesn't support aarch32
>> mode at all, neither arm_div nor jazelle will be supported either."
>>
>> Shouldn't we use a slighly different logic? Such:
>>
>> -    assert(no_aa32 || cpu_isar_feature(arm_div, cpu));
>> +    assert(no_aa32 && !cpu_isar_feature(arm_div, cpu));
>>
>
> I'm unsure. The current formula seems to match the commit description.
> Implication -- that is, "A implies B", (A-->B) -- is equivalent to (!A
> || B).
>
> We have "no_aa32 || arm_div", which corresponds to "aa32 implies
> arm_div" (aa32-->arm_div). And that seems to match exactly what Peter
> said.
>
> The assert you suggest would fire on a host that supports at least one
> of aa32 and arm_div (= the assertion would fail if (aa32 || arm_div)).
> That would break on my host (hw+kernel) just the same, in the end. To
> substitute the boolean values:
>
> -    assert(false || false)
> +    assert(false && true)

Hmmm wait a second. The ARMv8 ARM says, about ID_ISAR0_EL1:

> Divide, bits [27:24]
>
>     Indicates the implemented Divide instructions. Permitted values
>     are:
>     0000 None implemented.
>     0001 Adds SDIV and UDIV in the T32 instruction set.
>     0010 As for 0b0001, and adds SDIV and UDIV in the A32 instruction
>          set.
>     All other values are reserved.

So this means that (aa32 && !arm_div) *does* conform to the architecture
manual! And then, I understand where the bug is.

As I wrote above, the current C expression stands for:

  aa32 --> arm_div

which -- we see from the ARMv8 ARM -- is wrong.

Upon re-reading the commit message more carefully:

    on a host that doesn't support aarch32 mode at all, neither arm_div
    nor jazelle will be supported either

it's clear that the intent was *not* the implication encoded in the
source. Instead, the intent was the *reverse* implication, namely:

  !aa32 --> !arm_div    [1]

Or, equivalently (because, (A --> B) === (!A --> !B)):

  arm_div --> aa32      [2]

Now, if you encode any one of these (equivalent) formulae in C, with the
logical OR operator, you get:

- Starting from [1]:

  (A     --> B)        === (!A   || B)
  (!aa32 --> !arm_div) === (aa32 || !arm_div) === (!no_aa32 || !arm_div)

- Starting from [2]:

  (A       --> B)    === (!A       || B)
  (arm_div --> aa32) === (!arm_div || aa32) === (!arm_div || !no_aa32)

You can see that, regardless of whether we start with [1], or
equivalently, [2], we end up with the exact same predicate, logically
speaking. The final expressions only differ in C with regard to the
order of evaluation / shortcut behavior. We can pick whichever we prefer
(for whatever other reason).

FWIW, the language of the original commit message corresponds to [1].
So, if we want to stick with that, then the patch we need is:

> diff --git a/target/arm/cpu.c b/target/arm/cpu.c
> index e75a64a25a4b..ea84a3e11abb 100644
> --- a/target/arm/cpu.c
> +++ b/target/arm/cpu.c
> @@ -1382,8 +1382,13 @@ static void arm_cpu_realizefn(DeviceState *dev, Error **errp)
>           * include the various other features that V7VE implies.
>           * Presence of EL2 itself is ARM_FEATURE_EL2, and of the
>           * Security Extensions is ARM_FEATURE_EL3.
> +         *
> +         * Lack of aa32 support excludes arm_div support:
> +         *   no_aa32 --> !arm_div
> +         * Using the logical OR operator, the same is expressed as:
> +         *   !no_aa32 || !arm_div
>           */
> -        assert(no_aa32 || cpu_isar_feature(arm_div, cpu));
> +        assert(!no_aa32 || !cpu_isar_feature(arm_div, cpu));
>          set_feature(env, ARM_FEATURE_LPAE);
>          set_feature(env, ARM_FEATURE_V7);
>      }

If you guys agree, I can formally submit this patch.

Thanks
Laszlo