From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Andrea Corallo via "Bug reports for GNU Emacs, the Swiss army knife of text editors" Newsgroups: gmane.emacs.bugs Subject: bug#46670: 28.0.50; [feature/native-comp] possible miscompilation affecting lsp-mode Date: Tue, 23 Feb 2021 09:04:46 +0000 Message-ID: References: <87a6ry46uc.fsf@collares.org> Reply-To: Andrea Corallo Mime-Version: 1.0 Content-Type: text/plain Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="6409"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux) Cc: 46670@debbugs.gnu.org, Mauricio Collares To: Pip Cet Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Tue Feb 23 10:06:16 2021 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1lETe4-0001XY-HO for geb-bug-gnu-emacs@m.gmane-mx.org; Tue, 23 Feb 2021 10:06:16 +0100 Original-Received: from localhost ([::1]:49990 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lETe3-0005pO-It for geb-bug-gnu-emacs@m.gmane-mx.org; Tue, 23 Feb 2021 04:06:15 -0500 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:43994) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lETcs-0004uW-Lh for bug-gnu-emacs@gnu.org; Tue, 23 Feb 2021 04:05:02 -0500 Original-Received: from debbugs.gnu.org ([209.51.188.43]:46752) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lETcs-0008LI-Ed for bug-gnu-emacs@gnu.org; Tue, 23 Feb 2021 04:05:02 -0500 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lETcs-0003Ab-92 for bug-gnu-emacs@gnu.org; Tue, 23 Feb 2021 04:05:02 -0500 X-Loop: help-debbugs@gnu.org Resent-From: Andrea Corallo Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Tue, 23 Feb 2021 09:05:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 46670 X-GNU-PR-Package: emacs Original-Received: via spool by 46670-submit@debbugs.gnu.org id=B46670.161407109612169 (code B ref 46670); Tue, 23 Feb 2021 09:05:02 +0000 Original-Received: (at 46670) by debbugs.gnu.org; 23 Feb 2021 09:04:56 +0000 Original-Received: from localhost ([127.0.0.1]:58298 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lETcm-0003AD-3J for submit@debbugs.gnu.org; Tue, 23 Feb 2021 04:04:56 -0500 Original-Received: from mx.sdf.org ([205.166.94.24]:59078) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lETck-0003A5-Ec for 46670@debbugs.gnu.org; Tue, 23 Feb 2021 04:04:55 -0500 Original-Received: from mab (ma.sdf.org [205.166.94.33]) by mx.sdf.org (8.15.2/8.14.5) with ESMTPS id 11N94lfD019899 (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256 bits) verified NO); Tue, 23 Feb 2021 09:04:48 GMT In-Reply-To: (Pip Cet's message of "Tue, 23 Feb 2021 07:59:32 +0000") X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.io gmane.emacs.bugs:200646 Archived-At: Pip Cet writes: > On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo wrote: >> Good catch thanks! :) Should be fixed by d6227f6edc. > > I'm also confused by the use of NEGATED in comp-emit-assume: if RHS is > a constraint, it emits the complementary constraint. > > However, the code in comp-add-cond-cstrs uses NEGATED to express a > much weaker constraint: that two mvars aren't strictly equal. > > If x /= y and y in SET, we can't conclude that x not in SET (unless > SET is a singleton, an important special case). > > So it all works right now because emit-assume NEGATED=t RHS=mvar means > "LHS isn't equal to RHS" but NEGATED=t RHS=cstr means "LHS can't > satisfy RHS". > > My code changed the call to pass a constraint instead of the mvar, and > then things broke :-) > > We should be consistent about what NEGATED means, I think. > > But apart from such problems, my code appears to be working. I'm > attaching it for the sake of completeness, not because I expect you to > read it all before it's cleaned up. Hi Pip thanks for the patch, the approach of adding a cstr directly in the assume works for this case but is not generic as referencing there an mvar. The reason is that a later run of fw-prop after add-cstrs might be able to prove more precisely what the mvar is if the code was morphed in the meanwhile by some other pass. This in contrast with adding a cstr that being "written into the stone" will stay as such no matter what. Admittedly ATM the only pass rewriting some code after assumes are placed and before the last fw-prop is run is 'tco' so this might be a real case only for functions affected by this, but in the future we may (and most likely want to) have more passes in that position of the compiler pipeline. So yeah I still prefer to general approach of keeping an mvar live till there and referencing it in the assume so that any future propagation within the SSA lattice can update this. Yesterday evening I did some work in that direction, doesn't look too invasive or complex. I'll finish it this week as soon as I've some more time to put into. Thanks Andrea