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

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.

Package: emacs; Reported by: Pip Cet <pipcet@HIDDEN>; dated Mon, 1 Mar 2021 13:08:01 UTC; Maintainer for emacs is bug-gnu-emacs@HIDDEN.

Message received at 46847 <at> debbugs.gnu.org:


Received: (at 46847) by debbugs.gnu.org; 2 Mar 2021 06:58:31 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Mar 02 01:58:31 2021
Received: from localhost ([127.0.0.1]:51509 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1lGyzG-0006zg-RP
	for submit <at> debbugs.gnu.org; Tue, 02 Mar 2021 01:58:31 -0500
Received: from mail-ot1-f49.google.com ([209.85.210.49]:35012)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <pipcet@HIDDEN>) id 1lGyzB-0006zN-6q
 for 46847 <at> debbugs.gnu.org; Tue, 02 Mar 2021 01:58:29 -0500
Received: by mail-ot1-f49.google.com with SMTP id r19so19083933otk.2
 for <46847 <at> debbugs.gnu.org>; Mon, 01 Mar 2021 22:58:25 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
 h=mime-version:references:in-reply-to:from:date:message-id:subject:to
 :cc; bh=Dnj89hy0an6V7Jp+wLTUcNQB7/8wCp+g1c1tQcAIoTA=;
 b=Z2RBaUk+b3rafIjzZYiU56oaK6ApDNRt81hPIQc6isKReDltobKXoTl9ugmzmp6CbX
 RUU0tUPB2QWKouqbroqo9T3ZR/UW9ka6dyNoKe/ALzj1yGaD9/cM007ehpIHpzYDt23A
 sLS2GjYV7Vvv/L3UhXu+0m/qDFM9A1V/Lo65qo0GW4EY+mCf2xXE+9sv7Z5ePeDyC/C7
 IhYsSYwer3uEIZaHXG/xKxOjwpgXRUTzg3FnIjdRhc1stR51ZcmiTTVgOPclQYoDV+hh
 S/zuaJwhczpSO4y4qwdfFsVvHEY+gKW4RVL/Rwh5X6zpW2lbbZRQaFPN5YhHJiYacFeF
 5t3g==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20161025;
 h=x-gm-message-state:mime-version:references:in-reply-to:from:date
 :message-id:subject:to:cc;
 bh=Dnj89hy0an6V7Jp+wLTUcNQB7/8wCp+g1c1tQcAIoTA=;
 b=nKKpX3Rbe9LB3xTILESZ6e81xTS/hg0t4qSe4104ckHHxl+WzkAN4ebeB7nTMnS2tX
 olj7sR5Qd+R3AuRryDYwrvhzKVWL4XaP18nzWDOGF8UTE/5+Qjn+eLSE6hhLQRJkiO4r
 DCRtVbAp8eEnCtDyZIsPE/JPQKzSDYIWCveVzmjRU2HLkivgQaRiQwEMuMntOIn2eWk2
 JzcqEyrnTBBBaWrTbUa2IKt1EfI/mIQSFlxNyq/4ERq9Ay1VRS4VzYG4YoWltvHXtnOV
 dkaa2JniZPPXUKyUc6Ea5+XvR6+LN+DQUlmp2v9llL9BmA+jGZbqQnH5IN8dOnA4gAM9
 XB8A==
X-Gm-Message-State: AOAM531UtCnCO0RciQXupDRp7nNNHceq74FN6cWgv+uRE+p7bBpa0p26
 Jgi3m8ngFG2oW4DPfVuLo5YGxlnSWls0vnraAemLuzDviaP3TQ==
X-Google-Smtp-Source: ABdhPJxefPQMLycG19HhEzkFuRb5+31ezMBuqwxfkJIRwIG1AamK6pjmImLdUi4mt2Sdai6PGfq6gsRBYciKVr4toKw=
X-Received: by 2002:a05:6830:1682:: with SMTP id
 k2mr16922857otr.154.1614668299293; 
 Mon, 01 Mar 2021 22:58:19 -0800 (PST)
MIME-Version: 1.0
References: <CAOqdjBc+ch3KY0ChrLBR3vWyS4eXQgUQQKHzeQRwMv18aFER9A@HIDDEN>
 <xjf7dmqbpls.fsf@HIDDEN>
In-Reply-To: <xjf7dmqbpls.fsf@HIDDEN>
From: Pip Cet <pipcet@HIDDEN>
Date: Tue, 2 Mar 2021 06:57:42 +0000
Message-ID: <CAOqdjBe8F=NFOvYKYZw0NrK3YCQ5jRfr1_+oQRTQyDPu+MK+3w@HIDDEN>
Subject: Re: bug#46847: 28.0.50;
 [native-comp] assume pseudo-insns should be verified
To: Andrea Corallo <akrl@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 46847
Cc: 46847 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

On Mon, Mar 1, 2021 at 8:12 PM Andrea Corallo <akrl@HIDDEN> wrote:
> Pip Cet <pipcet@HIDDEN> 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




Information forwarded to bug-gnu-emacs@HIDDEN:
bug#46847; Package emacs. Full text available.

Message received at 46847 <at> debbugs.gnu.org:


Received: (at 46847) by debbugs.gnu.org; 1 Mar 2021 20:12:20 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Mar 01 15:12:20 2021
Received: from localhost ([127.0.0.1]:50951 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1lGotv-0003Wa-Vu
	for submit <at> debbugs.gnu.org; Mon, 01 Mar 2021 15:12:20 -0500
Received: from mx.sdf.org ([205.166.94.24]:62819)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <akrl@HIDDEN>) id 1lGots-0003WR-Lz
 for 46847 <at> debbugs.gnu.org; Mon, 01 Mar 2021 15:12:18 -0500
Received: from mab (ma.sdf.org [205.166.94.33])
 by mx.sdf.org (8.15.2/8.14.5) with ESMTPS id 121KCFOh017247
 (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256 bits) verified NO);
 Mon, 1 Mar 2021 20:12:15 GMT
From: Andrea Corallo <akrl@HIDDEN>
To: Pip Cet <pipcet@HIDDEN>
Subject: Re: bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be
 verified
References: <CAOqdjBc+ch3KY0ChrLBR3vWyS4eXQgUQQKHzeQRwMv18aFER9A@HIDDEN>
Date: Mon, 01 Mar 2021 20:12:15 +0000
In-Reply-To: <CAOqdjBc+ch3KY0ChrLBR3vWyS4eXQgUQQKHzeQRwMv18aFER9A@HIDDEN>
 (Pip Cet's message of "Mon, 1 Mar 2021 13:06:31 +0000")
Message-ID: <xjf7dmqbpls.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 46847
Cc: 46847 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Pip Cet <pipcet@HIDDEN> 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




Information forwarded to bug-gnu-emacs@HIDDEN:
bug#46847; Package emacs. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 1 Mar 2021 13:07:13 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Mar 01 08:07:13 2021
Received: from localhost ([127.0.0.1]:48451 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1lGiGX-0007J2-Cc
	for submit <at> debbugs.gnu.org; Mon, 01 Mar 2021 08:07:13 -0500
Received: from lists.gnu.org ([209.51.188.17]:44456)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <pipcet@HIDDEN>) id 1lGiGW-0007Iv-8P
 for submit <at> debbugs.gnu.org; Mon, 01 Mar 2021 08:07:12 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:50964)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <pipcet@HIDDEN>) id 1lGiGW-0008Ez-3L
 for bug-gnu-emacs@HIDDEN; Mon, 01 Mar 2021 08:07:12 -0500
Received: from mail-ot1-x32a.google.com ([2607:f8b0:4864:20::32a]:33741)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
 (Exim 4.90_1) (envelope-from <pipcet@HIDDEN>) id 1lGiGU-0005rF-Fs
 for bug-gnu-emacs@HIDDEN; Mon, 01 Mar 2021 08:07:11 -0500
Received: by mail-ot1-x32a.google.com with SMTP id 40so7973482otu.0
 for <bug-gnu-emacs@HIDDEN>; Mon, 01 Mar 2021 05:07:08 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
 h=mime-version:from:date:message-id:subject:to;
 bh=/3yMdq7YDKbEPgRymuQifvjpO6lt/7a6fpavKIMk51A=;
 b=kPQX+wVtorODPSr2bhMYa1sIfXGyCLqK/TO7cIFtDqatoAEU8SfwMvy94zAvQoH/1o
 sls6lKFraAiRBSlx5ueZ0+/Hj3cBlLYj2P3QWT+ratQ4gE1lP6Q3He1LYbh9h6m1k+Uu
 u0do9DVtXeCnzPh4au0jSjJ37UHEYTEu0XQpnyOYJCECXIW+MM1D6YmLOv3F89/wxOkh
 8O6D45FIRdGbmEgnYyZ2XFcxQZviHHPn6CMhn1jyfr7T+mWRSwUPTbwKl0GuDR8CNR+3
 HYGfjselOUwI+asJReGURh4Bbw4gJ7KWPkZPpLVH1MMKUjvNYOIdOd5Mb6Sbh7bhAEgK
 Hf+A==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20161025;
 h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
 bh=/3yMdq7YDKbEPgRymuQifvjpO6lt/7a6fpavKIMk51A=;
 b=XZhMVRkRCxhY9SO4yBGY90djSvTEeRSJe8UcltcSVYgYD3yHg4Z5WW2kh4b5cDMiXM
 ycuRV+79ZBcIEr62hgtV6ojXweOa3fIFiB18JFvl6kVvtnTdoQilwN/17LttOG7PVq5G
 H8hxgTLJTxcLtplW2RbWn4Zx1/1CqyCprHVRRKfjWQMisyMHux3y9wd98J8Q82xuUNt1
 qQvNrrwVfwFWFRlr7eASvbk/YFA2a09RpkCqXLzD3wBxVh51XP256+7pcXN7JyXSQTFv
 GihjPKMs18B0PiuQytrERE82d2a2j3V0fI0mC+51z0zSyGXzw/EWeX4zlKkxbvL0fS7s
 1LIA==
X-Gm-Message-State: AOAM532NqSeMGnWKe0Mwx+WSu0sqVMjZBPBNcMl7hmBzTwfBYSOymygO
 FCjcnurEEoyhwSkv5tfzW7CSro9ScPGscVsP/J4BQscYwukCXg==
X-Google-Smtp-Source: ABdhPJzZDrF7JNGanVsvvUcBqvACbS1qt2XIQNjZ9B/SX8WZX/raNRY5WkFE5IqByDq75viQEtBl2oNyScO/9hmxW6w=
X-Received: by 2002:a05:6830:1682:: with SMTP id
 k2mr13489910otr.154.1614604027918; 
 Mon, 01 Mar 2021 05:07:07 -0800 (PST)
MIME-Version: 1.0
From: Pip Cet <pipcet@HIDDEN>
Date: Mon, 1 Mar 2021 13:06:31 +0000
Message-ID: <CAOqdjBc+ch3KY0ChrLBR3vWyS4eXQgUQQKHzeQRwMv18aFER9A@HIDDEN>
Subject: 28.0.50; [native-comp] assume pseudo-insns should be verified
To: bug-gnu-emacs@HIDDEN
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::32a;
 envelope-from=pipcet@HIDDEN; helo=mail-ot1-x32a.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
 RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-Debbugs-Envelope-To: submit
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.3 (--)

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




Acknowledgement sent to Pip Cet <pipcet@HIDDEN>:
New bug report received and forwarded. Copy sent to bug-gnu-emacs@HIDDEN. Full text available.
Report forwarded to bug-gnu-emacs@HIDDEN:
bug#46847; Package emacs. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Tue, 2 Mar 2021 07:00:01 UTC

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997 nCipher Corporation Ltd, 1994-97 Ian Jackson.