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

[Pip Cet <pipcet@gmail.com>]

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