From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 129663 invoked by alias); 25 Apr 2019 13:13:46 -0000 Mailing-List: contact gcc-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-owner@gcc.gnu.org Received: (qmail 129349 invoked by uid 89); 25 Apr 2019 13:13:46 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-1.8 required=5.0 tests=AWL,BAYES_00,FREEMAIL_FROM,RCVD_IN_DNSWL_NONE,SPF_PASS autolearn=ham version=3.3.1 spammy=H*i:sk:zZBw@ma, H*f:sk:zZBw@ma, H*i:sk:CAHWkzR X-HELO: mail-lj1-f181.google.com Received: from mail-lj1-f181.google.com (HELO mail-lj1-f181.google.com) (209.85.208.181) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Thu, 25 Apr 2019 13:13:44 +0000 Received: by mail-lj1-f181.google.com with SMTP id p14so20208896ljg.5 for ; Thu, 25 Apr 2019 06:13:44 -0700 (PDT) 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=s/QR4lBMY6FqkTnlwVGCNWtvOjIB/vo7Os9515ynHE4=; b=ZAsXDL0bfh6WrT49VoUux2s2OhnsHOMQTT89KUmASE/C5Cfges9er/NrFRH9zxyDww R40182N9kbyn8eFtQefs84Hdt8v6iRpmPy4zrNOJcssVKVKX3dRSs/O1u+BsOhYjBfJa krW51Bajft24odjpChKeDtk5g7JL2zoj6/BZGm3vaeHWrSKwjGOt9JViBMMEmEgLkY0o RBXonlcrlViTWT/laUzKUCpUKE7TVzgL2BddnNg1qlnI0V23Jf3mLvKGQ+YUSjZQa8GX VAtzmgee5prOH4EboThoYmFG8UgtUZuQpDjIclWx5LI2Z3q0lC3EsXMVsx7MxdK/WLij yvNw== MIME-Version: 1.0 References: <1555502021.4884.1.camel@med.uni-goettingen.de> <1555505779.4884.4.camel@med.uni-goettingen.de> <1555510321.4884.7.camel@med.uni-goettingen.de> <1555590011.12545.3.camel@med.uni-goettingen.de> <30c3be07-433d-b945-40de-7b9a02f78789@redhat.com> <917e49da-bc4f-80a8-3399-30fff4a573f0@redhat.com> In-Reply-To: From: Richard Biener Date: Thu, 25 Apr 2019 13:13:00 -0000 Message-ID: Subject: Re: C provenance semantics proposal To: Peter.Sewell@cl.cam.ac.uk Cc: Jeff Law , "Uecker, Martin" , "gcc@gcc.gnu.org" , "cl-c-memory-object-model@lists.cam.ac.uk" Content-Type: text/plain; charset="UTF-8" X-IsSubscribed: yes X-SW-Source: 2019-04/txt/msg00252.txt.bz2 On Thu, Apr 25, 2019 at 3:03 PM Peter Sewell wrote: > > On 25/04/2019, Richard Biener wrote: > > On Wed, Apr 24, 2019 at 11:18 PM Peter Sewell > > wrote: > >> > >> On 24/04/2019, Jeff Law wrote: > >> > On 4/24/19 4:19 AM, Richard Biener wrote: > >> >> On Thu, Apr 18, 2019 at 3:42 PM Jeff Law wrote: > >> >>> > >> >>> On 4/18/19 6:20 AM, Uecker, Martin wrote: > >> >>>> Am Donnerstag, den 18.04.2019, 11:45 +0100 schrieb Peter Sewell: > >> >>>>> On Thu, 18 Apr 2019 at 10:32, Richard Biener > >> >>>>> wrote: > >> >>>> > >> >>>> > >> >>>>> An equality test of two pointers, on the other hand, doesn't > >> >>>>> necessarily > >> >>>>> mean that they are interchangeable. I don't see any good way to > >> >>>>> avoid that in a provenance semantics, where a one-past > >> >>>>> pointer might sometimes compare equal to a pointer to an > >> >>>>> adjacent object but be illegal for accessing it. > >> >>>> > >> >>>> As I see it, there are essentially four options: > >> >>>> > >> >>>> 1.) Compilers do not use conditional equivalences for > >> >>>> optimizations of pointers (or only when additional > >> >>>> conditions apply which make it safe) > >> >>> I know this will hit DOM and CSE. I wouldn't be surprised if it > >> >>> touches > >> >>> VRP as well, maybe PTA. It seems simple enough though :-) > >> >> > >> >> Also touches fundamental PHI-OPT transforms like > >> >> > >> >> if (a == b) > >> >> ... > >> >> > >> >> # c = PHI > >> >> > >> >> where we'd lose eliding such a conditional. IMHO that's bad > >> >> and very undesirable. > >> > But if we only suppress this optimization for pointers is it that > >> > terrible? > >> > >> As far as I can see right now, there isn't a serious alternative. > >> Suppose x and y are adjacent, p=&x+1, and q=&y, so p==q might > >> be true (either in a semantics for the source-language == that just > >> compares the concrete representations or in one that's allowed > >> but not required to be provenance-sensitive). It's not possible > >> to simultaneously have *p UB (which AIUI the compiler has to > >> have in the intermediate language, to make alias analysis sound), > >> *q not UB, and p interchangeable with q. Am I missing something? > > > > No, you are not missing anything. We do have this issue right now, > > independent of standard wordings. But the standard has that, too, > > not allowing *(&x + 1), allowing the compare and allowing *&y. > > Isn't that a defect as well? > > In the source-language semantics, it's ok for p==q to not imply > that p and q are interchangeable, and if compilers are doing > provenance-based alias analysis (so address equality doesn't > imply equally-readable/writable), it's pretty much inescapable. > > Hence why (without knowing much about the optimisations that > actually go on) it's tempting to suggest that for pointer equality > comparison one could just not infer that interchangeability. I'd be > very interested to know the actual cost of that. Since we at the moment track provenance through non-pointers it means we cannot do this for non-pointer equivalences either. So doing this means no longer tracking provenance through non-pointers. > (The standard does also have a defect in its definition of equality - on > the one hand, it says that &x+1==&y comparison must be true > if they are adjacent, but on the other (in DR260) that everything > might be provenance-aware. My preference would be to resolve > that by requiring source-language == to not be provenance aware, > but I think this is a more-or-less independent thing.) I think it's related at least to us using provenance to optimize pointer comparisons. Richard. > Peter