220 22520 article Path: news.gmane.org!not-for-mail From: Jonas Persson Newsgroups: gmane.comp.lang.c++.isocpp.proposals Subject: Re: Unreachable attribute. Date: Wed, 11 Nov 2015 23:44:06 +0100 Lines: 288 Approved: news@gmane.org Message-ID: References: <2573561.klGZ6ZHjC3@lastique-n550jv> <4611855.M52eYPluZF@lastique-n550jv> <3705e2b3-76ac-4a55-b4d3-9252c6462c50@isocpp.org> Reply-To: std-proposals@isocpp.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=047d7b5d36b26095fb05244b90d3 X-Trace: ger.gmane.org 1447281850 18613 80.91.229.3 (11 Nov 2015 22:44:10 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 11 Nov 2015 22:44:10 +0000 (UTC) To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBDLJBMEUU4NBBN4JR6ZAKGQELKGOS4A@isocpp.org Wed Nov 11 23:44:10 2015 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-wm0-f71.google.com ([74.125.82.71]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Zwe7c-0001Kz-Ri for gclcip-std-proposals@m.gmane.org; Wed, 11 Nov 2015 23:44:08 +0100 Original-Received: by wmeo63 with SMTP id o63sf14663734wme.1 for ; Wed, 11 Nov 2015 14:44:08 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=isocpp_org.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:x-original-sender:x-original-authentication-results :reply-to:precedence:mailing-list:list-id:x-spam-checked-in-group :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=1YKuGuDkaASKzuVgZK+jUA4ARnaV9bKxCJ9wdwQtK5M=; b=LkjE9vaJuprmhT0wPJen1B4HgsNTY7/eS093FGcL/mj3DJvKGcrDMe7uHdgU4Tb5p3 VuQLxLfHJAYXpnqKWuxwWw2HMypysh8YmwQyEodw2GFuYZfYLgSIa3wNA6Dd2xaKEn+D jZMJ1OLR+CvebpQSbxQXa6O4NiPV7UGljMjjAQ6z0d7LHsL0xAc5Ielh800mDOc//sMJ 4eKOOLlwXlAqXIUv4DnWhyglLzEVS6pYabGnLf2mZMEnK3pXfsz2Ea+oKLqYK/qnttmb l8hAWqDWJjbu5NIGAbcIZL7Cu8SB79TF6vs66gY+g5vCZYRSLdp3sAdUVG0kQmmgjPNl wQgQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:content-type:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-spam-checked-in-group:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=1YKuGuDkaASKzuVgZK+jUA4ARnaV9bKxCJ9wdwQtK5M=; b=QZFTDevAv7Uyn+3Lrw5Tkp7KFcH3Ipn76isuzAxOKuwyKJNOmCzSuuhP58qC1zNH3Y mkV8dBCh9MgSpSt+cV4h3gDkY6FfTDVF7KMZ7uzBwRMLNJkuY7e5W7H4VA0LgaXPaHQD ymZyDkss6GlPKMOEwakIMF4S5gI4jSbUuALAYVqNFpwhhdtk3fWCoge6Z4ZMul7mD84m UQpMsTiAB4GGYAVK+JCxkw6ILjme8JhEVLgky7QUeqgiqnwgohe6zOdinQ5wLCCWAgSV E7RY1uYc4zg0DcwnW6DZxB643W+mFVdKK31HKFvR0OelwuisQwY4Wfw+GbWvASgVHGZ7 N7kA== X-Gm-Message-State: ALoCoQn+sesngv5eGVvb2iBK+YwosSaXC+JrH8+eL3qbkDIUEvL+LIioT1LIa96WntgFowztyH1y X-Received: by 10.25.166.143 with SMTP id p137mr1697693lfe.0.1447281848204; Wed, 11 Nov 2015 14:44:08 -0800 (PST) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.28.22.6 with SMTP id 6ls600043wmw.44.canary; Wed, 11 Nov 2015 14:44:07 -0800 (PST) X-Received: by 10.28.146.136 with SMTP id u130mr14285472wmd.91.1447281847088; Wed, 11 Nov 2015 14:44:07 -0800 (PST) Original-Received: from mail-wm0-x230.google.com (mail-wm0-x230.google.com. [2a00:1450:400c:c09::230]) by mx.google.com with ESMTPS id gc9si14519778wjb.57.2015.11.11.14.44.07 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 11 Nov 2015 14:44:07 -0800 (PST) Received-SPF: pass (google.com: domain of l.j.persson@gmail.com designates 2a00:1450:400c:c09::230 as permitted sender) client-ip=2a00:1450:400c:c09::230; Original-Received: by wmec201 with SMTP id c201so67083580wme.1 for ; Wed, 11 Nov 2015 14:44:07 -0800 (PST) X-Received: by 10.194.20.130 with SMTP id n2mr14377348wje.115.1447281846947; Wed, 11 Nov 2015 14:44:06 -0800 (PST) Original-Received: by 10.28.157.148 with HTTP; Wed, 11 Nov 2015 14:44:06 -0800 (PST) In-Reply-To: X-Original-Sender: l.j.persson@gmail.com X-Original-Authentication-Results: mx.google.com; spf=pass (google.com: domain of l.j.persson@gmail.com designates 2a00:1450:400c:c09::230 as permitted sender) smtp.mailfrom=l.j.persson@gmail.com; dkim=pass header.i=@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list std-proposals@isocpp.org; contact std-proposals+owners@isocpp.org List-ID: X-Spam-Checked-In-Group: std-proposals@isocpp.org X-Google-Group-Id: 399137483710 List-Post: , List-Help: , List-Archive: List-Subscribe: , List-Unsubscribe: , Xref: news.gmane.org gmane.comp.lang.c++.isocpp.proposals:22520 Archived-At: --047d7b5d36b26095fb05244b90d3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Wed, Nov 11, 2015 at 11:37 PM, Tony V E wrote: > > > On Wed, Nov 11, 2015 at 5:26 PM, Jonas Persson > wrote: > >> >> >> On Wed, Nov 11, 2015 at 5:28 PM, Giovanni Piero Deretta < >> gpderetta@gmail.com> wrote: >> >>> On Wednesday, November 11, 2015 at 3:36:44 PM UTC, Jonas Persson wrote: >>>> >>>> >>>> >>>> On Wed, Nov 11, 2015 at 4:09 PM, Giovanni Piero Deretta < >>>> gpde...@gmail.com> wrote: >>>> >>>>> >>>>> >>>>> On Wednesday, November 11, 2015 at 1:51:22 PM UTC, David Krauss wrote= : >>>>>> >>>>>> >>>>>> On 2015=E2=80=9311=E2=80=9311, at 8:04 PM, Giovanni Piero Deretta >>>>>> wrote: >>>>>> >>>>>> Interesting. A possible definition of std::unreachable() would be an >>>>>> empty function whose precondition is always false. The problem of de= fining >>>>>> its behavior if is actually invoked would be part of the general han= dling >>>>>> of contracts. >>>>>> >>>>>> >>>>>> The contract is an attribute in Ed=E2=80=99s example because the con= sensus is >>>>>> that UB on precondition failure doesn=E2=80=99t alter semantics, rig= ht? So, a >>>>>> language extension for contracts isn=E2=80=99t needed for [[unreacha= ble]]. >>>>>> >>>>>> >>>>> if that's the consensus for contracts, then yes, there is no need for >>>>> explicit support for unreachable. >>>>> >>>>> >>>>>> It would still be nice to spell unreachable as an >>>>>> attribute-statement as opposed to a function, even if it=E2=80=99s n= ot magic. It >>>>>> acts like a language construct. Inside switch, it=E2=80=99s also an >>>>>> alternative to [[fallthrough]]. >>>>>> >>>>> >>>>> why though? Wouldn't an std::unreachable() work just fine in your >>>>> example? I don't have strong preference either way, but wouldn't a fu= nction >>>>> call be more idiomatic than an attribute attached to an empty stateme= nt? >>>>> >>>>> -- gpd >>>>> >>>>> This can't be how contracts work. That would be very confusing. >>>> If the compiler figure out that a precondition is always false it has >>>> to either fail to compile or invoke the violation handler. >>>> It can use the preconditions to optimize inside the function, but not >>>> silently optimize away the code on the caller side as we would expect >>>> [[unreachable]] to do. >>>> >>>> >>> Assuming that the effect contract violations can be configured as UB, >>> then it is just another source of UB. Compilers already optimize today = by >>> backpropagating UB, std::unreachable wouldn't be any different. >>> >> >> It is a bit strange to reason about precondition UB that way. There is >> usefulness in assuming that the preconditions true and optimize for that= , >> where it beeing false leads to UB. But here the compiler first proves th= e >> program to be incorrect and than uses that information for optimizations= .. >> Why optimize an incorrect program? >> >> >> >>> If you prefer an exception or an handler to be called on precondition >>> violation, you probably want that on a reached std::unreachable as well= .. >>> >> >> If the handler I choose is the compile time check(I dont know if this >> part of the proposal, but is really should be) any use of std::unreachab= le >> would be a compiler error. >> >> >>> >>> Also the compiler (or static analyser) should complain only if it can >>> statically prove that a function with invalid preconditions is actually >>> called. >>> >>> -- gpd >>> >> >> Why would you want that? It would lead to runtime check for a lot >> conditions that are fully known at compile time. >> >> So in the case of std::unreachable it is not allowed to complain since >> it cannot prove it will be called, but is is allowed to optimize as if i= t >> is not, even if that cannot be proved? >> > > I'm not 100% sure I understand what you are saying, but I think my answer > is: > > Yes, exactly. > > The point of facilities like this is for you, the developer, to tell the > compiler things that it can't (with current technology) prove on its own. > It is your way of saying "trust me, even if you can't prove this, I can". > So optimize as if it was proven. > > Then on the flip side, maybe in debug, ie no optimizations, we want to sa= y > "but wait, if it turns out I was wrong, scream and yell at runtime". > > Tony > I agree that is a thing we need. What I am objecting to is using a funtction with a precondition to achive this. A precondition from the callers perspective is something that should be checked, not a thruth. For that it would be better to have something designed for the task, like __assume(expr) / Jonas --=20 ---=20 You received this message because you are subscribed to the Google Groups "= ISO C++ Standard - Future Proposals" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to std-proposals+unsubscribe@isocpp.org. To post to this group, send email to std-proposals@isocpp.org. Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposa= ls/. --047d7b5d36b26095fb05244b90d3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable


On Wed, Nov 11, 2015 at 11:37 PM, Tony V E <tvaneerd@gmail.com>= ; wrote:


On W= ed, Nov 11, 2015 at 5:26 PM, Jonas Persson <l.j.persson@gmail.com&= gt; wrote:


On Wed, Nov 1= 1, 2015 at 5:28 PM, Giovanni Piero Deretta <gpderetta@gmail.com><= /span> wrote:
On Wednesday, November 11, 2015 at 3:36:4= 4 PM UTC, Jonas Persson wrote:

<= div>
On Wed, Nov 11, 2015 at 4:09 PM, Giovann= i Piero Deretta <gpde...@gmail.com= > wrote:


On Wednesday, November 1= 1, 2015 at 1:51:22 PM UTC, David Krauss wrote:

On 20= 15=E2=80=9311=E2=80=9311, at 8:04 PM, Giovanni Piero Deretta <gpde...@gmail.com> wrote:

Interesting. A possible definition of std:= :unreachable() would be an empty function whose precondition is always fals= e. The problem of defining its behavior if is actually invoked would be par= t of the general handling of contracts.

The contract is an attribute in Ed=E2=80=99s example beca= use the consensus is that UB on precondition failure doesn=E2=80=99t alter = semantics, right? So, a language extension for contracts isn=E2=80=99t need= ed for=C2=A0[[unreachable]].


if that's the consensus for cont= racts, then yes, there is no need for explicit support for unreachable.
= =C2=A0
It would still be nice to spell unreacha= ble as an attribute-statement as opposed to a function, even if it= =E2=80=99s not magic. It acts like a language construct. Inside switch, it=E2=80=99s also an alternative to [[fallthrough]].
why though? Wouldn't an std::unreachable() work just fine in your exa= mple? I don't have strong preference either way, but wouldn't a fun= ction call be more idiomatic than an attribute attached to an empty stateme= nt?

-- gpd

This can't be how contracts = work. That would be very confusing.=C2=A0
If the compiler figure = out that a precondition is always false it has to either fail to compile or= invoke the violation handler.=C2=A0
It can use the preconditions= to optimize inside the function, but not silently optimize away the code o= n the caller side as we would expect [[unreachable]] to do.

<= /div>

Assuming that the effect cont= ract violations can be configured as UB, then it is just another source of = UB. Compilers already optimize today by backpropagating UB, std::unreachabl= e wouldn't be any different.
=C2=A0= =C2=A0
It is a bit strange to reason about precondition UB that w= ay. There is usefulness in assuming that the preconditions true and optimiz= e for that, where it beeing false leads to UB. But here the compiler first = proves the program to be incorrect and than uses that information for optim= izations. Why optimize an incorrect program?

=C2=A0
If you prefer an exception or an = handler to be called on precondition violation, you probably want that on a= reached std::unreachable as well.

=C2=A0 If the handler I choose is the compile time check(I dont kn= ow if this part of the proposal, but is really should be) any use of std::u= nreachable would be a compiler error.
=C2=A0

Also the compiler (or static analyser) should complain onl= y if it can statically prove that a function with invalid preconditions is = actually called.

-- gpd
=

=C2=A0 Why would you want that? It would lead to= runtime check for a lot conditions that are fully known at compile time.= =C2=A0

=C2=A0 So in the case of std::unreacha= ble it is not allowed to complain since it cannot prove it will be called, = but is is allowed to optimize as if it is not, even if that cannot be prove= d?

I&#= 39;m not 100% sure I understand what you are saying, but I think my answer = is:

Yes, exactly.

The point of facilities like thi= s is for you, the developer, to tell the compiler things that it can't = (with current technology) prove on its own.
It is your way of= saying "trust me, even if you can't prove this, I can".=C2= =A0 So optimize as if it was proven.

Then on the flip sid= e, maybe in debug, ie no optimizations, we want to say "but wait, if i= t turns out I was wrong, scream and yell at runtime".

Tony

I agree that= is a thing we need. What I am objecting to is using a funtction with a pre= condition to achive this. A precondition from the callers perspective is so= mething that should be checked, not a thruth.
For that it would b= e better to have something designed for the task, like __assume(expr)=C2=A0=

=C2=A0 / Jonas

--

---
You received this message because you are subscribed to the Google Groups &= quot;ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to std-proposa= ls+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposals/<= /a>.
--047d7b5d36b26095fb05244b90d3-- .