Incorrect semantic computation for MULX when first and second argument are same

[basavesh]

Found through random fuzz-test. this is true for both size variants of 32 and 64.
Bug: When the first and second argument are same, Jasmin semantics and hardware semantics differ.

If the first and second operand are identical, it will contain the high half of the multiplication result.

Size=64
Executing instruction MULX R14 R14 RDI -> mulxq %rdi, %r14, %r14
Before:

RDI: 12585089653095806027
R14: 3958074007382419651

Jasmin After:

R14: 37409020628164682

H/W After:

r14 = 7136978533371468338

Size = 32
Executing instruction MULX_32 R14 R14 RDI -> mulxl %edi, %r14d, %r14d

Before:

RDI: 13977003853042703850
R14: 17852321287948986267

Jasmin After:

R14: 3375765496

H/W After:

r14 = 915477969

CC: @vbgl @bgregoir @gbarthe @cryptojedi

[vbgl]

Thanks for finding and reporting this issue. Might it be that the results are written (in the semantics) in the wrong order, so that the low half overwrites the high half?

I think that the compiler cannot produce code that witnesses this error: the liveness analysis used during register allocation is not precise enough.

[basavesh]

That is possible. However, I don't think I saw a special case when the 1st and 2nd arguments are same.
As you suggested, it might be a better idea to simply write the high half later to deal with this special case.

[bgregoir]

Just to resume, the discussion with Vincent. We are agree that this is a bug in the semantics.
There is a simple way to fix it, say that mulx return (lo, hi) instead of (hi, lo). In that case the pb is solve but
this require to fix the jasmin program, and certainly to do the same kind of change for similar instructions.
like (hi, lo) = x * y --> (lo, hi) = x * y.
The EC model need to be changed to.
So we think it is not reasonable...
The other way to fix it is to ensure that the semantic reject such a program were both destination are equals.
So the semantics will be incomplete compare to the architecture but it is correct.
In any case, the compiler never generate code where both destination are the same register. Both destination are marked to be in conflict.
But maybe this can change in the future

[cryptojedi]

bgregoir ***@***.***> wrote: Hi Benjamin,

Just to resume, the discussion with Vincent. We are agree that this is a bug in the semantics. There is a simple way to fix it, say that mulx return (lo, hi) instead of (hi, lo). In that case the pb is solve but this require to fix the jasmin program, and certainly to do the same kind of change for similar instructions. like (hi, lo) = x * y --> (lo, hi) = x * y. The EC model need to be changed to. So we think it is not reasonable... The other way to fix it is to ensure that the semantic reject such a program were both destination are equals. So the semantics will be incomplete compare to the architecture but it is correct. In any case, the compiler never generate code where both destination are the same register. Both destination are marked to be in conflict.

If you prevent the compiler to ever generating such code, wouldn't it still be possible to write such code using intrinsics? If yes, then wouldn't the EasyCrypt semantics need to change anyway? Cheers, Peter

[vbgl]

It is already the case that the compiler cannot emit code that witness the bug: two outputs of an instruction are considered live after this instruction, hence conflict, i.e., cannot be allocated to the same register.

[basavesh]

So there is a room for improving the live analysis and maybe do better allocation in the future. (Depending on whether this instruction will help in some special case).

So, is it going to be a semantic bug which will not be fixed?

[basavesh]

According to me, a better and probably correct solution to implement in the future would be to track if those two registers are same and then return (hi, hi). I think this will faithfully implement the Intel semantics instead of writing high later hack.

[bgregoir]

I agree that the best solution will be to change the order of elements in the return (i.e. (lo,hi) instead of (hi,lo)).
The question is are we agree to pay the cost of this change.
@peter, I think the compiler will fail to generate code like (hi,hi) = #mulx(x,y) (I have not tested, I think this come from what was explained by Vincent). This does not means that it will still true in the futur.

[cryptojedi]

bgregoir ***@***.***> wrote:

I agree that the best solution will be to change the order of elements in the return (i.e. (lo,hi) instead of (hi,lo)). The question is are we agree to pay the cost of this change. @peter, I think the compiler will fail to generate code like (hi,hi) = #mulx(x,y) (I have not tested, I think this come from what was explained by Vincent). This does not means that it will still true in the futur.

This is probably the biggest risk: if we accept wrong semantics and make sure in other components of the compiler that the special cases are never triggered, there is a risk that at some point in the future those other parts of the compiler change and actually *do* trigger the special case. This wouldn't then be caught by anything really, right?

[bgregoir]

It was the point of rejecting mulx r r, if this has no semantic if the compiler generates a mulx r r at some point
we will not be able to prove its correctness.
Any way, we discussed with Vincent, and we decided to do the following.
Add an instruction MULX_lo_hi (the current MULX return hi, lo), the compiler will emit a mulx
Add an instruction MULX_hi (return a single element) the compiler mulx hi hi ...
Keep the current MULX, the compiler will emit a warning that the instruction is deprecated.
(hi,lo) = #MULX(x,y) will be translated to (lo,hi) = #MULX_lo_hi(x,y) with a check that lo <> hi, else fail.
Once libjade is patched, we can remove MULX with a explicite failure instead of a warning.
A some point we can rename MULX_lo_hi into MULX (in 2 or 3 version of the compiler).

[bgregoir]

Ok, I think the current solution will not require to do any change in libjade.