Hi Mathias, Thanks for the comments. Unfortunately, changing "r" to "rm" for the out parameter in a systematic way is quite trick. Allowing arguments to be passed independently in a register or in memory is currently out of scope of the Vale model we use for verification. We must decide early on in the verification pipeline if the argument is passed in a register, or if it stored in memory. Doing this in a sound way would require a significant change to our (trusted) model.
Cheers, Aymeric ----- Mail original ----- > De: "Mathias Krause" <[email protected]> > À: "Aymeric Fromherz" <[email protected]>, "Jason A. Donenfeld" > <[email protected]> > Cc: "WireGuard mailing list" <[email protected]> > Envoyé: Lundi 13 Décembre 2021 08:44:51 > Objet: Re: [PATCH 0/2] wireguard-linux-compat: grsecurity compat patches > Hi Aymeric, > > the changes look good to me -- quite what we already had in grsec. Just > one more nit. The constraints for the 'out' parameter in fmul(), > fmul2(), fsqr() and fsqr2() can be further lifted to "rm" as 'out' is > only referenced once. This allows gcc to choose either a register or a > memory operand, as it sees fit. In our experiments the latter lead to > much better code gen. > > Thanks, > Mathias > > Am 11.12.21 um 17:35 schrieb Aymeric Fromherz: >> Thanks for the heads-up. We were being overly conservative during >> verification >> of inline assembly code in Vale, and marked several registers as possibly >> modified while they were only read. >> >> This is now fixed for fmul, fmul2, fsqr and fsqr2, and will be merged into >> the >> master branch of EverCrypt shortly. >> In the meantime, the diff for the resulting inline assembly after Vale >> codegen >> is available here: >> https://github.com/project-everest/hacl-star/pull/501/commits/1a71adb40c3f78da16e16975dbb1d4de5adeab8c#diff-5aabe9f6aa87508c9d81d4c9e89eff0b06b1e2aeaf5b04eba51da71c5bea6940 >> >> Cheers, >> Aymeric >> >> ----- Mail original ----- >>> De: "Jason A. Donenfeld" <[email protected]> >>> À: "Mathias Krause" <[email protected]>, "aymeric fromherz" >>> <[email protected]> >>> Cc: "WireGuard mailing list" <[email protected]> >>> Envoyé: Vendredi 10 Décembre 2021 23:58:01 >>> Objet: Re: [PATCH 0/2] wireguard-linux-compat: grsecurity compat patches >> >>> CC'ing in Aymeric, who's working on Vale's codegen. >>> >>> On Thu, Dec 9, 2021 at 8:59 AM Mathias Krause <[email protected]> >>> wrote: >>>> >>>> Am 08.12.21 um 15:56 schrieb Jason A. Donenfeld: >>>>> On Mon, Dec 6, 2021 at 10:00 PM Mathias Krause <[email protected]> >>>>> wrote: >>>>>> Yes, probably, but you're mixing up the two. >>>>> >>>>> Oh, thanks, right. >>>>> >>>>> I'll talk to EverCrypt upstream and see. >>>> >>>> FWIW, 'out' is also wrongly flagged as output operand in fmul() and >>>> fmul2(). But making it an input operand needs more surgery, as the >>>> operand order changes and this requires some code churn. >>>> > >>> Mathias
