bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Pip Cet]

This is a wishlist item for the native-comp branch, though I consider
the feature in question to be so essential that its absence also
qualifies as a bug.

The native-comp branch is emitting assume pseudo-insns. Those come in
various forms, but their interpretation is clear: they express
conditions which are meant to hold at runtime, and which the compiler
may use to optimize code.

I would like to add an optional compiler pass which asserts that the
conditions are actually true at runtime. This is a basic safeguard
that any assume() mechanism should have, and it's perfectly equivalent
to the way eassume() becomes eassert() in debug builds of Emacs.

Unfortunately, it turns out that while adding the compiler pass is
easy, there are many failures because the assume pseudo-insns emitted
at present are inconsistent or plain wrong. Some of these wrong
assumes result in reproducible Lisp-to-native-code bugs today; others
will not; for still others, we're not sure.

For example, the four following bugs became a problem only because of
a lack of this safeguard: bug#46843 (both bugs), bug#46812, bug#46670.

Merging native-comp without such a safeguard would, I am convinced,
introduce preventable, tricky, unnecessary bugs into the Emacs master
branch.  We shouldn't do that.

Pip

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors]

Pip Cet <pipcet@gmail.com> writes:

> This is a wishlist item for the native-comp branch, though I consider
> the feature in question to be so essential that its absence also
> qualifies as a bug.
>
> The native-comp branch is emitting assume pseudo-insns. Those come in
> various forms, but their interpretation is clear: they express
> conditions which are meant to hold at runtime, and which the compiler
> may use to optimize code.
>
> I would like to add an optional compiler pass which asserts that the
> conditions are actually true at runtime. This is a basic safeguard
> that any assume() mechanism should have, and it's perfectly equivalent
> to the way eassume() becomes eassert() in debug builds of Emacs.
>
> Unfortunately, it turns out that while adding the compiler pass is
> easy, there are many failures because the assume pseudo-insns emitted
> at present are inconsistent or plain wrong. Some of these wrong
> assumes result in reproducible Lisp-to-native-code bugs today; others
> will not; for still others, we're not sure.

I think the issue might be that how assumes works has been
miss-understood here.

Assumes are working after SSA rename in the world of mvar ids, in
contrast we render code based on slot numbers.  Rendering assertions
based on assumes using the slot numbers (IIUC that's what your patch
did) certainly leads to inconsistencies, but that's a fundamental
miss-interpretation of how assumes are working.  This is probably also
why you often suggests assumes are inconsistent.

Anyway, for the reasons above rendering 1:1 assumes into run-time checks
is not easily possible.

OTOH a possible way, and that's what I want to do, would be to verify
just before each (non pseudo) insn actually rendered that the slots in
use there are consistent with the prediction.

One could even control that with a parameter and have a mode where we
just inject asserts on return insns not to bloat excessively the code.

Note: I'm not aware of any compiler emitting run-time checks to verify
its compile time predictions by why not.

I'll take this task as sounds like good verification/development cost
trade-off to me.  Will follow-up on this!

Thanks

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Pip Cet]

On Mon, Mar 1, 2021 at 8:12 PM Andrea Corallo <akrl@sdf.org> wrote:
> Pip Cet <pipcet@gmail.com> writes:
> > This is a wishlist item for the native-comp branch, though I consider
> > the feature in question to be so essential that its absence also
> > qualifies as a bug.
> >
> > The native-comp branch is emitting assume pseudo-insns. Those come in
> > various forms, but their interpretation is clear: they express
> > conditions which are meant to hold at runtime, and which the compiler
> > may use to optimize code.
> >
> > I would like to add an optional compiler pass which asserts that the
> > conditions are actually true at runtime. This is a basic safeguard
> > that any assume() mechanism should have, and it's perfectly equivalent
> > to the way eassume() becomes eassert() in debug builds of Emacs.
> >
> > Unfortunately, it turns out that while adding the compiler pass is
> > easy, there are many failures because the assume pseudo-insns emitted
> > at present are inconsistent or plain wrong. Some of these wrong
> > assumes result in reproducible Lisp-to-native-code bugs today; others
> > will not; for still others, we're not sure.
>
> I think the issue might be that how assumes works has been
> miss-understood here.

> Assumes are working after SSA rename in the world of mvar ids, in
> contrast we render code based on slot numbers.

If mvars introduced in assumes don't have valid slot numbers, they
shouldn't have a valid slot number in the :slot slot.

But in the case of the assumes emitted so far, they do have valid slot
numbers, they're just not the ones that are used.

>  Rendering assertions
> based on assumes using the slot numbers (IIUC that's what your patch
> did)

I merely converted the assumes into assertions. I did not use the slot
numbers there.

> certainly leads to inconsistencies, but that's a fundamental
> miss-interpretation of how assumes are working.

If there is a consistent slot number to assign to an assume-d
variable, we should use it. If there isn't, we shouldn't use a slot
number at all. What we do right now is to simply use a slot number
that we know to be incorrect, even though a correct one is available.

Again, what we emit is

(assume (mvar X :slot 1) (not (mvar Y :slot 1)))
(assume (mvar Z :slot 2) (and ... (mvar X :slot 1)))

what we should emit is

(assume (mvar X :slot 2) (not (mvar Y :slot 1)))
(assume (mvar Z :slot 2) (and ... (mvar X :slot 2)))

or even

(assume (mvar X :slot -1) (not (mvar Y :slot 1)))
(assume (mvar Z :slot 2) (and ... (mvar X :slot -1)))

or whatever mechanism you're proposing to name mvars which do not
refer to variables (respectfully, but that's what a metavariable is
defined to be).

> This is probably also why you often suggests assumes are inconsistent.

No, the seven bugs we ran into so far which were caused by
inconsistent assumes are why I often suggest assumes are inconsistent.

> Anyway, for the reasons above rendering 1:1 assumes into run-time checks
> is not easily possible.

Then we should call them something else, because that's what an "assume" is.

> OTOH a possible way, and that's what I want to do, would be to verify
> just before each (non pseudo) insn actually rendered that the slots in
> use there are consistent with the prediction.

That would catch fewer bugs, and it would catch them much later, when
code which uses them has been written.

> One could even control that with a parameter and have a mode where we
> just inject asserts on return insns not to bloat excessively the code.

That seems like an entirely arbitrary place to check our assumes, to me.

> Note: I'm not aware of any compiler emitting run-time checks to verify
> its compile time predictions by why not.

I don't know why you're unaware Emacs (pre-native-comp) and GCC both
do that, but they do.

Pip

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors]

Pip Cet <pipcet@gmail.com> writes:

[...]

> (assume (mvar X :slot -1) (not (mvar Y :slot 1)))
> (assume (mvar Z :slot 2) (and ... (mvar X :slot -1)))

Now that we can generate temporaries this might be an option.  But I
think would be helpful if you could show what exactly are the 1:1
assertions you'd like to synthesize for the above assumes, otherwise
this discussion will stay just too high level.

[...]

>> Note: I'm not aware of any compiler emitting run-time checks to verify
>> its compile time predictions by why not.
>
> I don't know why you're unaware Emacs (pre-native-comp) and GCC both
> do that, but they do.

I wasn't even aware that the byte compiler is doing any value prediction
and that is emitting code for to verify these, could give pointers to
boths cases?

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Pip Cet]

On Mon, Mar 1, 2021 at 1:08 PM Pip Cet <pipcet@gmail.com> wrote:
> I would like to add an optional compiler pass which asserts that the
> conditions are actually true at runtime. This is a basic safeguard
> that any assume() mechanism should have, and it's perfectly equivalent
> to the way eassume() becomes eassert() in debug builds of Emacs.

I've proceeded to change things so I can assert assumes, and here's an
incomplete list of the bugs I've found so far:

Function types:
1. append has type (function (&rest t) t), not (function (&rest list) list)
2. aref has type (function (t fixnum) t), not (function (array fixnum) t)
3. bool-vector-count-consecutive has type (function (bool-vector
boolean integer) fixnum), not (function (bool-vector bool-vector
integer) fixnum))
4. at least some of the frame-* functions accept nil parameters
5. intern-soft has type (function ((or string symbol) &optional
vector) symbol), not (function (string &optional vector) symbol)
6. length has type (function (t) integer), not (function (sequence) integer)
7. at least some of the minibuffer functions can return nil as well as a window.
8. nthcdr has type (function (integer t) t), not (function (integer list) list)
9. radians-to-degrees is a macro and probably shouldn't have a function type
10. string has type (function (&rest fixnum) string), not (function
(&rest fixnum) strng)
11. user-full-name has type (function (&optional integer) (or string
null)), not (function (&optional integer) string)

Predicate types:
1. functionp isn't equivalent to (or function symbol)

Other:
1. comp-lambda-list-gen has to allow optional arguments to be nil even
if explicitly specified.

Furthermore, I've already reported some other bugs.

So I think this is worth pursuing further.

Pip

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors]

Pip Cet <pipcet@gmail.com> writes:

> On Mon, Mar 1, 2021 at 1:08 PM Pip Cet <pipcet@gmail.com> wrote:
>> I would like to add an optional compiler pass which asserts that the
>> conditions are actually true at runtime. This is a basic safeguard
>> that any assume() mechanism should have, and it's perfectly equivalent
>> to the way eassume() becomes eassert() in debug builds of Emacs.
>
> I've proceeded to change things so I can assert assumes, and here's an
> incomplete list of the bugs I've found so far:
>
> Function types:
> 1. append has type (function (&rest t) t), not (function (&rest list) list)
> 2. aref has type (function (t fixnum) t), not (function (array fixnum) t)
> 3. bool-vector-count-consecutive has type (function (bool-vector
> boolean integer) fixnum), not (function (bool-vector bool-vector
> integer) fixnum))
> 4. at least some of the frame-* functions accept nil parameters
> 5. intern-soft has type (function ((or string symbol) &optional
> vector) symbol), not (function (string &optional vector) symbol)
> 6. length has type (function (t) integer), not (function (sequence) integer)
> 7. at least some of the minibuffer functions can return nil as well as a window.
> 8. nthcdr has type (function (integer t) t), not (function (integer list) list)
> 9. radians-to-degrees is a macro and probably shouldn't have a function type
> 10. string has type (function (&rest fixnum) string), not (function
> (&rest fixnum) strng)
> 11. user-full-name has type (function (&optional integer) (or string
> null)), not (function (&optional integer) string)

> Predicate types:
> 1. functionp isn't equivalent to (or function symbol)

Thanks, patches are welcome.

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors]

Pip Cet <pipcet@gmail.com> writes:

[...]

> Function types:
> 1. append has type (function (&rest t) t), not (function (&rest list) list)
> 2. aref has type (function (t fixnum) t), not (function (array fixnum) t)
> 3. bool-vector-count-consecutive has type (function (bool-vector
> boolean integer) fixnum), not (function (bool-vector bool-vector
> integer) fixnum))
> 4. at least some of the frame-* functions accept nil parameters
> 5. intern-soft has type (function ((or string symbol) &optional
> vector) symbol), not (function (string &optional vector) symbol)
> 6. length has type (function (t) integer), not (function (sequence) integer)
> 7. at least some of the minibuffer functions can return nil as well as a window.
> 8. nthcdr has type (function (integer t) t), not (function (integer
> list) list)
> 9. radians-to-degrees is a macro and probably shouldn't have a function type
> 10. string has type (function (&rest fixnum) string), not (function
> (&rest fixnum) strng)
> 11. user-full-name has type (function (&optional integer) (or string
> null)), not (function (&optional integer) string)

I've fixed most of these, please given you have already investigated
this issue be more precise on points 4 and 7.

> Predicate types:
> 1. functionp isn't equivalent to (or function symbol)

Would you suggest what's the right type specifier or the counter example
that violated this so we can fix it?

> Other:
> 1. comp-lambda-list-gen has to allow optional arguments to be nil even
> if explicitly specified.

Not sure I understand, please be more precise in describing the issue so
we can fix it.

Thanks

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo]

I'm closing this old bug as with 0b0c7da8c80 I've installed a sanitizer
that instruments the code in order to check that compile time value
predictions of mvars are respected at runtime.  Mvars verified are all
mvars being tested by conditional branches, this to verify the correct
CFG/execution of the program.

Enabling sanitizer instrumentation and runtime verification I'm able to
bootstrap the compiler and run all the compiler testsuite.

We might extend this further in the future but I think for now is okay.

Thanks

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Eli Zaretskii]

> Resent-To: bug-gnu-emacs@gnu.org
> Cc: 46847-done@debbugs.gnu.org, Pip Cet <pipcet@gmail.com>
> From: Andrea Corallo <acorallo@gnu.org>
> Date: Wed, 20 Mar 2024 05:30:04 -0400
> 
> I'm closing this old bug as with 0b0c7da8c80 I've installed a sanitizer
> that instruments the code in order to check that compile time value
> predictions of mvars are respected at runtime.  Mvars verified are all
> mvars being tested by conditional branches, this to verify the correct
> CFG/execution of the program.
> 
> Enabling sanitizer instrumentation and runtime verification I'm able to
> bootstrap the compiler and run all the compiler testsuite.
> 
> We might extend this further in the future but I think for now is okay.

Thanks, but would it be possible to document the suggested use of this
sanitizer in the comments somewhere?

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Andrea Corallo]

Eli Zaretskii <eliz@gnu.org> writes:

>> Resent-To: bug-gnu-emacs@gnu.org
>> Cc: 46847-done@debbugs.gnu.org, Pip Cet <pipcet@gmail.com>
>> From: Andrea Corallo <acorallo@gnu.org>
>> Date: Wed, 20 Mar 2024 05:30:04 -0400
>> 
>> I'm closing this old bug as with 0b0c7da8c80 I've installed a sanitizer
>> that instruments the code in order to check that compile time value
>> predictions of mvars are respected at runtime.  Mvars verified are all
>> mvars being tested by conditional branches, this to verify the correct
>> CFG/execution of the program.
>> 
>> Enabling sanitizer instrumentation and runtime verification I'm able to
>> bootstrap the compiler and run all the compiler testsuite.
>> 
>> We might extend this further in the future but I think for now is okay.
>
> Thanks, but would it be possible to document the suggested use of this
> sanitizer in the comments somewhere?

Hi Eli,

that's a good point.

There are many usage scenarios, I just added a simple example at the
beginning of the 'Sanitizer pass specific code' section.

Thanks

  Andrea

bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified

[Eli Zaretskii]

> From: Andrea Corallo <acorallo@gnu.org>
> Cc: 46847@debbugs.gnu.org,  pipcet@gmail.com
> Date: Wed, 20 Mar 2024 09:58:53 -0400
> 
> Eli Zaretskii <eliz@gnu.org> writes:
> 
> > Thanks, but would it be possible to document the suggested use of this
> > sanitizer in the comments somewhere?
> 
> Hi Eli,
> 
> that's a good point.
> 
> There are many usage scenarios, I just added a simple example at the
> beginning of the 'Sanitizer pass specific code' section.

Thanks!