Hi Aymeric, yeah, don't worry. We can keep this change downstream in grsec. Dunno if Jason wants to take it as well, his call. It was just a side observation which came out of our need to read and understand the code to provide a workaround for the gcc bug we were hitting.
Thanks, Mathias Am 13.12.21 um 15:20 schrieb Aymeric Fromherz: > 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
