Topic: C++ contracts for compiler optimizations
Author: Alexander Zaitsev <zamazan4ik@gmail.com>
Date: Wed, 1 Aug 2018 16:35:41 -0700 (PDT)
Raw View
------=_Part_15_2055052985.1533166541634
Content-Type: multipart/alternative;
boundary="----=_Part_16_1586036264.1533166541635"
------=_Part_16_1586036264.1533166541635
Content-Type: text/plain; charset="UTF-8"
Hello,
As I know the main goal of contracts is program verification. It's very
important, but also I am interested in using C++ contracts as additional
help for compilers in optimizations.
E.g. we have this code:
int foo()
{
std::vector<int> vec = {5,4,3,2,1};
boost::sort(vec.begin(), vec.end());
std::sort(vec.begin(), vec.end());
int result = 0;
for(int i = 0; i < 5; ++i)
{
if(i % 2 == 0) result += vec[i];
else result -= vec[i];
}
return result;
}
What should be done here with very clever compiler?
- At first compiler should try to precalculate it at compile-time. But it's
impossible for some large vectors. Let's imagine that we can't precalculate
result at compile-time.
- At second we have here two sort functions, which goes one by one
sequentially without any intermediate operations with 'vec' between them.
Compiler can't detect without contracts that result after first call
boost::sort will be enough and call std::sort isn't required here. Compiler
can't detect that functions are semantically identical. But with contracts
we can try to do next hint: let's define that boost::sort and std::sort
both have equal post-condition - [[axiom: is_sorted(vec.begin(),
vec.end)]]. Compiler see two sequential call of sort functions, call
boost::sort, because compiler can't prove that is_sorted is satisfied for
boost::sort call. After boost::sort call we exactly know that is_sorted
condition is true, and what we see - std::sort also has post-condition
is_sorted... And if we already satisfied is_sorted post-condition before
std::sort call, we can simply skip this function! Here I see at least one
problem: function can has some side-effects which are not presented in
post-condition - it's probably work for library writers
I am not a compiler writer and haven't any strong knowledge in this kind of
compiler optimizations. So I am interested - with C++ contracts is it
possible to implement more optimizations? Which additional optimizations
can be implemented with contracts?
P.S. If you want to play with contracts, you can try this Clang fork with
C++ contracts support: https://github.com/arcosuc3m/clang-contracts
--
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 email to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/083fe6dd-52b6-4b58-bcfc-8aa89606433e%40isocpp.org.
------=_Part_16_1586036264.1533166541635
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">Hello,<div><br><div>As I know the main goal of contracts i=
s program verification. It's very important, but also I am interested i=
n using C++ contracts as additional help for compilers in optimizations.</d=
iv><div><br></div><div>E.g. we have this code:</div></div><div><br></div><d=
iv><div class=3D"prettyprint" style=3D"background-color: rgb(250, 250, 250)=
; border-color: rgb(187, 187, 187); border-style: solid; border-width: 1px;=
word-wrap: break-word;"><code class=3D"prettyprint"><div class=3D"subprett=
yprint"><span style=3D"color: #008;" class=3D"styled-by-prettify">int</span=
><span style=3D"color: #000;" class=3D"styled-by-prettify"> foo</span><span=
style=3D"color: #660;" class=3D"styled-by-prettify">()</span><span style=
=3D"color: #000;" class=3D"styled-by-prettify"> <br></span><span style=3D"c=
olor: #660;" class=3D"styled-by-prettify">{</span><span style=3D"color: #00=
0;" class=3D"styled-by-prettify"> <br>=C2=A0 =C2=A0 std</span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">::</span><span style=3D"colo=
r: #000;" class=3D"styled-by-prettify">vector</span><span style=3D"color: #=
080;" class=3D"styled-by-prettify"><int></span><span style=3D"color: =
#000;" class=3D"styled-by-prettify"> vec </span><span style=3D"color: #660;=
" class=3D"styled-by-prettify">=3D</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify"> </span><span style=3D"color: #660;" class=3D"style=
d-by-prettify">{</span><span style=3D"color: #066;" class=3D"styled-by-pret=
tify">5</span><span style=3D"color: #660;" class=3D"styled-by-prettify">,</=
span><span style=3D"color: #066;" class=3D"styled-by-prettify">4</span><spa=
n style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span style=
=3D"color: #066;" class=3D"styled-by-prettify">3</span><span style=3D"color=
: #660;" class=3D"styled-by-prettify">,</span><span style=3D"color: #066;" =
class=3D"styled-by-prettify">2</span><span style=3D"color: #660;" class=3D"=
styled-by-prettify">,</span><span style=3D"color: #066;" class=3D"styled-by=
-prettify">1</span><span style=3D"color: #660;" class=3D"styled-by-prettify=
">};</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> <br>=
=C2=A0<br>=C2=A0 =C2=A0 boost</span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">::</span><span style=3D"color: #000;" class=3D"styled-by=
-prettify">sort</span><span style=3D"color: #660;" class=3D"styled-by-prett=
ify">(</span><span style=3D"color: #000;" class=3D"styled-by-prettify">vec<=
/span><span style=3D"color: #660;" class=3D"styled-by-prettify">.</span><sp=
an style=3D"color: #008;" class=3D"styled-by-prettify">begin</span><span st=
yle=3D"color: #660;" class=3D"styled-by-prettify">(),</span><span style=3D"=
color: #000;" class=3D"styled-by-prettify"> vec</span><span style=3D"color:=
#660;" class=3D"styled-by-prettify">.</span><span style=3D"color: #008;" c=
lass=3D"styled-by-prettify">end</span><span style=3D"color: #660;" class=3D=
"styled-by-prettify">());</span><span style=3D"color: #000;" class=3D"style=
d-by-prettify"> <br>=C2=A0 =C2=A0 std</span><span style=3D"color: #660;" cl=
ass=3D"styled-by-prettify">::</span><span style=3D"color: #000;" class=3D"s=
tyled-by-prettify">sort</span><span style=3D"color: #660;" class=3D"styled-=
by-prettify">(</span><span style=3D"color: #000;" class=3D"styled-by-pretti=
fy">vec</span><span style=3D"color: #660;" class=3D"styled-by-prettify">.</=
span><span style=3D"color: #008;" class=3D"styled-by-prettify">begin</span>=
<span style=3D"color: #660;" class=3D"styled-by-prettify">(),</span><span s=
tyle=3D"color: #000;" class=3D"styled-by-prettify"> vec</span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">.</span><span style=3D"color=
: #008;" class=3D"styled-by-prettify">end</span><span style=3D"color: #660;=
" class=3D"styled-by-prettify">());</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"> <br>=C2=A0<br>=C2=A0 =C2=A0 </span><span style=3D=
"color: #008;" class=3D"styled-by-prettify">int</span><span style=3D"color:=
#000;" class=3D"styled-by-prettify"> result </span><span style=3D"color: #=
660;" class=3D"styled-by-prettify">=3D</span><span style=3D"color: #000;" c=
lass=3D"styled-by-prettify"> </span><span style=3D"color: #066;" class=3D"s=
tyled-by-prettify">0</span><span style=3D"color: #660;" class=3D"styled-by-=
prettify">;</span><span style=3D"color: #000;" class=3D"styled-by-prettify"=
> <br>=C2=A0 =C2=A0 </span><span style=3D"color: #008;" class=3D"styled-by-=
prettify">for</span><span style=3D"color: #660;" class=3D"styled-by-prettif=
y">(</span><span style=3D"color: #008;" class=3D"styled-by-prettify">int</s=
pan><span style=3D"color: #000;" class=3D"styled-by-prettify"> i </span><sp=
an style=3D"color: #660;" class=3D"styled-by-prettify">=3D</span><span styl=
e=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"colo=
r: #066;" class=3D"styled-by-prettify">0</span><span style=3D"color: #660;"=
class=3D"styled-by-prettify">;</span><span style=3D"color: #000;" class=3D=
"styled-by-prettify"> i </span><span style=3D"color: #660;" class=3D"styled=
-by-prettify"><</span><span style=3D"color: #000;" class=3D"styled-by-pr=
ettify"> </span><span style=3D"color: #066;" class=3D"styled-by-prettify">5=
</span><span style=3D"color: #660;" class=3D"styled-by-prettify">;</span><s=
pan style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">++</span><span style=3D"colo=
r: #000;" class=3D"styled-by-prettify">i</span><span style=3D"color: #660;"=
class=3D"styled-by-prettify">)</span><span style=3D"color: #000;" class=3D=
"styled-by-prettify"> <br>=C2=A0 =C2=A0 </span><span style=3D"color: #660;"=
class=3D"styled-by-prettify">{</span><span style=3D"color: #000;" class=3D=
"styled-by-prettify"> <br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 </span><span style=3D=
"color: #008;" class=3D"styled-by-prettify">if</span><span style=3D"color: =
#660;" class=3D"styled-by-prettify">(</span><span style=3D"color: #000;" cl=
ass=3D"styled-by-prettify">i </span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">%</span><span style=3D"color: #000;" class=3D"styled-by-=
prettify"> </span><span style=3D"color: #066;" class=3D"styled-by-prettify"=
>2</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span>=
<span style=3D"color: #660;" class=3D"styled-by-prettify">=3D=3D</span><spa=
n style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=
=3D"color: #066;" class=3D"styled-by-prettify">0</span><span style=3D"color=
: #660;" class=3D"styled-by-prettify">)</span><span style=3D"color: #000;" =
class=3D"styled-by-prettify"> =C2=A0 =C2=A0result </span><span style=3D"col=
or: #660;" class=3D"styled-by-prettify">+=3D</span><span style=3D"color: #0=
00;" class=3D"styled-by-prettify"> vec</span><span style=3D"color: #660;" c=
lass=3D"styled-by-prettify">[</span><span style=3D"color: #000;" class=3D"s=
tyled-by-prettify">i</span><span style=3D"color: #660;" class=3D"styled-by-=
prettify">];</span><span style=3D"color: #000;" class=3D"styled-by-prettify=
"> <br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 </span><span style=3D"color: #008;" clas=
s=3D"styled-by-prettify">else</span><span style=3D"color: #000;" class=3D"s=
tyled-by-prettify"> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0result =
</span><span style=3D"color: #660;" class=3D"styled-by-prettify">-=3D</span=
><span style=3D"color: #000;" class=3D"styled-by-prettify"> vec</span><span=
style=3D"color: #660;" class=3D"styled-by-prettify">[</span><span style=3D=
"color: #000;" class=3D"styled-by-prettify">i</span><span style=3D"color: #=
660;" class=3D"styled-by-prettify">];</span><span style=3D"color: #000;" cl=
ass=3D"styled-by-prettify"> <br>=C2=A0 =C2=A0 </span><span style=3D"color: =
#660;" class=3D"styled-by-prettify">}</span><span style=3D"color: #000;" cl=
ass=3D"styled-by-prettify"> <br>=C2=A0 =C2=A0 </span><span style=3D"color: =
#008;" class=3D"styled-by-prettify">return</span><span style=3D"color: #000=
;" class=3D"styled-by-prettify"> result</span><span style=3D"color: #660;" =
class=3D"styled-by-prettify">;</span><span style=3D"color: #000;" class=3D"=
styled-by-prettify"> <br></span><span style=3D"color: #660;" class=3D"style=
d-by-prettify">}</span><span style=3D"color: #000;" class=3D"styled-by-pret=
tify"> </span></div></code></div><br>What should be done here with very cle=
ver compiler?
<br>- At first compiler should try to precalculate it at compile-time. But=
=20
it's impossible for some large vectors. Let's imagine that we can&#=
39;t=20
precalculate result at compile-time.<br>- At second we have here two sort f=
unctions, which goes one by one=20
sequentially without any intermediate operations with 'vec' between=
=20
them. Compiler can't detect without contracts that result after first=
=20
call boost::sort will be enough and call std::sort isn't required here.=
=20
Compiler can't detect that functions are semantically identical. But wi=
th contracts we can try to do next hint: let's=20
define that boost::sort and std::sort both have equal post-condition -=20
[[axiom: is_sorted(vec.begin(), vec.end)]]. Compiler see two sequential=20
call of sort functions, call boost::sort, because compiler can't prove=
=20
that is_sorted is satisfied for boost::sort call. After boost::sort call=20
we exactly know that is_sorted condition is true, and what we see -=20
std::sort also has post-condition is_sorted... And if we already=20
satisfied is_sorted post-condition before std::sort call, we can simply=20
skip this function! Here I see at least one problem: function can has=20
some side-effects which are not presented in post-condition - it's=20
probably work for library writers<br></div><div><br></div><div>I am not a c=
ompiler writer and haven't any strong knowledge in this kind of compile=
r optimizations. So I am interested - with C++ contracts is it possible to =
implement more optimizations? Which additional optimizations can be impleme=
nted with contracts?</div><div><br></div><div>P.S. If you want to play with=
contracts, you can try this Clang fork with C++ contracts support:=C2=A0ht=
tps://github.com/arcosuc3m/clang-contracts</div></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/083fe6dd-52b6-4b58-bcfc-8aa89606433e%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/083fe6dd-52b6-4b58-bcfc-8aa89606433e=
%40isocpp.org</a>.<br />
------=_Part_16_1586036264.1533166541635--
------=_Part_15_2055052985.1533166541634--
.
Author: Henry Miller <hank@millerfarm.com>
Date: Thu, 02 Aug 2018 08:04:06 -0500
Raw View
This is a multi-part message in MIME format.
--_----------=_153321504620482400
Content-Type: text/plain; charset="UTF-8"
--
Henry Miller
hank@millerfarm.com
On Wed, Aug 1, 2018, at 6:35 PM, Alexander Zaitsev wrote:
> Hello,
>
> As I know the main goal of contracts is program verification. It's
> very important, but also I am interested in using C++ contracts as
> additional help for compilers in optimizations.>
> E.g. we have this code:
>
>
> int foo() { std::vector<int> vec = {5,4,3,2,1};
>
> boost::sort(vec.begin(), vec.end()); std::sort(vec.begin(),
> vec.end());
>
> int result = ; for(int i = ; i < 5; ++i) { if(i % 2 == )
> result += vec[i]; else result -= vec[i]; } return
> result; }>
>
> What should be done here with very clever compiler?
> - At first compiler should try to precalculate it at compile-time. But
> it's impossible for some large vectors. Let's imagine that we can't
> precalculate result at compile-time.> - At second we have here two sort functions, which goes one by one
> sequentially without any intermediate operations with 'vec' between
> them. Compiler can't detect without contracts that result after
> first call boost::sort will be enough and call std::sort isn't
> required here. Compiler can't detect that functions are semantically
> identical. But with contracts we can try to do next hint: let's
> define that boost::sort and std::sort both have equal post-condition
> - [[axiom: is_sorted(vec.begin(), vec.end)]]. Compiler see two
> sequential call of sort functions, call boost::sort, because
> compiler can't prove that is_sorted is satisfied for boost::sort
> call. After boost::sort call we exactly know that is_sorted
> condition is true, and what we see - std::sort also has post-
> condition is_sorted... And if we already satisfied is_sorted post-
> condition before std::sort call, we can simply skip this function!Here is where you go start to go wrong. The compiler cannot know that
is_sorted checks all properties. Boost and the standard library
generally do reasonable things, so sort actually sorts. In the real
world sort might randomize, and is_sorted verifies the maximum value is
less than 10 - I've seen humans do stupid things like that. (indeed it
is often argued that using the shift operators for io is a stupid thing
in c++) thus in the generic sense what you proposed isn't enough either.
The good news is that you are not wrong, just that your reasoning
doesn't account for the stupid things that people do. If the compiler
can understand is_sorted well enough and the lack of side effects in
either sort the compiler can eliminate one. Contracts do allow for
additional optimization that isn't possible without them. It isn't a
free lunch for the compiler though, the compiler needs to understand the
contract to optimize with it.
One other factor. In the real world of contracts it is often recommended
that you don't check is_sorted, that is too expensive. You more likely
check first < last, or two random elements. This contract is much more
efficient to check at runtime, but doesn't give the compiler as much
information.
>
> Here I see at least one problem: function can has some side-effects
> which are not presented in post-condition - it's probably work for
> library writers>
> I am not a compiler writer and haven't any strong knowledge in this
> kind of compiler optimizations. So I am interested - with C++
> contracts is it possible to implement more optimizations? Which
> additional optimizations can be implemented with contracts?>
> P.S. If you want to play with contracts, you can try this Clang fork
> with C++ contracts support:
> https://github.com/arcosuc3m/clang-contracts>
> --
> 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 email to std-proposals+unsubscribe@isocpp.org.> To post to this group, send email to std-proposals@isocpp.org.
> To view this discussion on the web visit
> https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/083fe6dd-52b6-4b58-bcfc-8aa89606433e%40isocpp.org[1].
Links:
1. https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/083fe6dd-52b6-4b58-bcfc-8aa89606433e%40isocpp.org?utm_medium=email&utm_source=footer
--
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 email to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/1533215046.2048240.1461141104.01BC6D5B%40webmail.messagingengine.com.
--_----------=_153321504620482400
Content-Transfer-Encoding: quoted-printable
Content-Type: text/html; charset="UTF-8"
<!DOCTYPE html>
<html>
<head>
<title></title>
<style type=3D"text/css">p.MsoNormal,p.MsoNoSpacing{margin:0}</style>
</head>
<body><div style=3D"font-family:Arial;"><br></div>
<div style=3D"font-family:Arial;"><br></div>
<div id=3D"sig11221025"><div class=3D"signature">--<br></div>
<div class=3D"signature"> Henry Miller<br></div>
<div class=3D"signature"> hank@millerfarm.com<br></div>
<div class=3D"signature"><br></div>
</div>
<div><br></div>
<div><br></div>
<div>On Wed, Aug 1, 2018, at 6:35 PM, Alexander Zaitsev wrote:<br></div>
<blockquote type=3D"cite"><div dir=3D"ltr"><div style=3D"font-family:Arial;=
">Hello,<br></div>
<div><div style=3D"font-family:Arial;"><br></div>
<div>As I know the main goal of contracts is program verification. It's ver=
y important, but also I am interested in using C++ contracts as additional =
help for compilers in optimizations.<br></div>
<div><br></div>
<div>E.g. we have this code:<br></div>
</div>
<div><br></div>
<div><div style=3D"background-color:rgb(250, 250, 250);border-top-color:rgb=
(187, 187, 187);border-right-color:rgb(187, 187, 187);border-bottom-color:r=
gb(187, 187, 187);border-left-color:rgb(187, 187, 187);border-top-style:sol=
id;border-right-style:solid;border-bottom-style:solid;border-left-style:sol=
id;border-top-width:1px;border-right-width:1px;border-bottom-width:1px;bord=
er-left-width:1px;word-wrap:break-word;"><div style=3D"font-family:Arial;">=
<code></code><br></div>
<div><code><span class=3D"colour" style=3D"color:rgb(0, 0, 136)">int</span>=
<span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> foo</span><span class=
=3D"colour" style=3D"color:rgb(102, 102, 0)">()</span><span class=3D"colour=
" style=3D"color:rgb(0, 0, 0)"> <br></span><span class=3D"colour" style=3D"=
color:rgb(102, 102, 0)">{</span><span class=3D"colour" style=3D"color:rgb(0=
, 0, 0)"> <br> std</span><span class=3D"colour" style=3D"color=
:rgb(102, 102, 0)">::</span><span class=3D"colour" style=3D"color:rgb(0, 0,=
0)">vector</span><span class=3D"colour" style=3D"color:rgb(0, 136, 0)"><=
;int></span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> vec </s=
pan><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">=3D</span><span=
class=3D"colour" style=3D"color:rgb(0, 0, 0)"> </span><span class=3D"colou=
r" style=3D"color:rgb(102, 102, 0)">{</span><span class=3D"colour" style=3D=
"color:rgb(0, 102, 102)">5</span><span class=3D"colour" style=3D"color:rgb(=
102, 102, 0)">,</span><span class=3D"colour" style=3D"color:rgb(0, 102, 102=
)">4</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">,</span>=
<span class=3D"colour" style=3D"color:rgb(0, 102, 102)">3</span><span class=
=3D"colour" style=3D"color:rgb(102, 102, 0)">,</span><span class=3D"colour"=
style=3D"color:rgb(0, 102, 102)">2</span><span class=3D"colour" style=3D"c=
olor:rgb(102, 102, 0)">,</span><span class=3D"colour" style=3D"color:rgb(0,=
102, 102)">1</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)"=
>};</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> <br> <b=
r> boost</span><span class=3D"colour" style=3D"color:rgb(102, =
102, 0)">::</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)">sort<=
/span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">(</span><span=
class=3D"colour" style=3D"color:rgb(0, 0, 0)">vec</span><span class=3D"col=
our" style=3D"color:rgb(102, 102, 0)">.</span><span class=3D"colour" style=
=3D"color:rgb(0, 0, 136)">begin</span><span class=3D"colour" style=3D"color=
:rgb(102, 102, 0)">(),</span><span class=3D"colour" style=3D"color:rgb(0, 0=
, 0)"> vec</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">.<=
/span><span class=3D"colour" style=3D"color:rgb(0, 0, 136)">end</span><span=
class=3D"colour" style=3D"color:rgb(102, 102, 0)">());</span><span class=
=3D"colour" style=3D"color:rgb(0, 0, 0)"> <br> std</span><span=
class=3D"colour" style=3D"color:rgb(102, 102, 0)">::</span><span class=3D"=
colour" style=3D"color:rgb(0, 0, 0)">sort</span><span class=3D"colour" styl=
e=3D"color:rgb(102, 102, 0)">(</span><span class=3D"colour" style=3D"color:=
rgb(0, 0, 0)">vec</span><span class=3D"colour" style=3D"color:rgb(102, 102,=
0)">.</span><span class=3D"colour" style=3D"color:rgb(0, 0, 136)">begin</s=
pan><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">(),</span><span=
class=3D"colour" style=3D"color:rgb(0, 0, 0)"> vec</span><span class=3D"co=
lour" style=3D"color:rgb(102, 102, 0)">.</span><span class=3D"colour" style=
=3D"color:rgb(0, 0, 136)">end</span><span class=3D"colour" style=3D"color:r=
gb(102, 102, 0)">());</span><span class=3D"colour" style=3D"color:rgb(0, 0,=
0)"> <br> <br> </span><span class=3D"colour" style=3D"co=
lor:rgb(0, 0, 136)">int</span><span class=3D"colour" style=3D"color:rgb(0, =
0, 0)"> result </span><span class=3D"colour" style=3D"color:rgb(102, 102, 0=
)">=3D</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> </span><s=
pan class=3D"colour" style=3D"color:rgb(0, 102, 102)">0</span><span class=
=3D"colour" style=3D"color:rgb(102, 102, 0)">;</span><span class=3D"colour"=
style=3D"color:rgb(0, 0, 0)"> <br> </span><span class=3D"colo=
ur" style=3D"color:rgb(0, 0, 136)">for</span><span class=3D"colour" style=
=3D"color:rgb(102, 102, 0)">(</span><span class=3D"colour" style=3D"color:r=
gb(0, 0, 136)">int</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)=
"> i </span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">=3D</sp=
an><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> </span><span class=
=3D"colour" style=3D"color:rgb(0, 102, 102)">0</span><span class=3D"colour"=
style=3D"color:rgb(102, 102, 0)">;</span><span class=3D"colour" style=3D"c=
olor:rgb(0, 0, 0)"> i </span><span class=3D"colour" style=3D"color:rgb(102,=
102, 0)"><</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> <=
/span><span class=3D"colour" style=3D"color:rgb(0, 102, 102)">5</span><span=
class=3D"colour" style=3D"color:rgb(102, 102, 0)">;</span><span class=3D"c=
olour" style=3D"color:rgb(0, 0, 0)"> </span><span class=3D"colour" style=3D=
"color:rgb(102, 102, 0)">++</span><span class=3D"colour" style=3D"color:rgb=
(0, 0, 0)">i</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">=
)</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> <br> &nb=
sp; </span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">{</span>=
<span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> <br> &nbs=
p; </span><span class=3D"colour" style=3D"color:rgb(0, 0, 136)">if</=
span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">(</span><span =
class=3D"colour" style=3D"color:rgb(0, 0, 0)">i </span><span class=3D"colou=
r" style=3D"color:rgb(102, 102, 0)">%</span><span class=3D"colour" style=3D=
"color:rgb(0, 0, 0)"> </span><span class=3D"colour" style=3D"color:rgb(0, 1=
02, 102)">2</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> </sp=
an><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">=3D=3D</span><sp=
an class=3D"colour" style=3D"color:rgb(0, 0, 0)"> </span><span class=3D"col=
our" style=3D"color:rgb(0, 102, 102)">0</span><span class=3D"colour" style=
=3D"color:rgb(102, 102, 0)">)</span><span class=3D"colour" style=3D"color:r=
gb(0, 0, 0)"> result </span><span class=3D"colour" style=3D"co=
lor:rgb(102, 102, 0)">+=3D</span><span class=3D"colour" style=3D"color:rgb(=
0, 0, 0)"> vec</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)=
">[</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)">i</span><span=
class=3D"colour" style=3D"color:rgb(102, 102, 0)">];</span><span class=3D"=
colour" style=3D"color:rgb(0, 0, 0)"> <br> </spa=
n><span class=3D"colour" style=3D"color:rgb(0, 0, 136)">else</span><span cl=
ass=3D"colour" style=3D"color:rgb(0, 0, 0)"> &n=
bsp; result </span><span class=3D"colour" style=3D"color:rgb(1=
02, 102, 0)">-=3D</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"=
> vec</span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">[</span=
><span class=3D"colour" style=3D"color:rgb(0, 0, 0)">i</span><span class=3D=
"colour" style=3D"color:rgb(102, 102, 0)">];</span><span class=3D"colour" s=
tyle=3D"color:rgb(0, 0, 0)"> <br> </span><span class=3D"colour=
" style=3D"color:rgb(102, 102, 0)">}</span><span class=3D"colour" style=3D"=
color:rgb(0, 0, 0)"> <br> </span><span class=3D"colour" style=
=3D"color:rgb(0, 0, 136)">return</span><span class=3D"colour" style=3D"colo=
r:rgb(0, 0, 0)"> result</span><span class=3D"colour" style=3D"color:rgb(102=
, 102, 0)">;</span><span class=3D"colour" style=3D"color:rgb(0, 0, 0)"> <br=
></span><span class=3D"colour" style=3D"color:rgb(102, 102, 0)">}</span><sp=
an class=3D"colour" style=3D"color:rgb(0, 0, 0)"></span></code></div>
<div style=3D"font-family:Arial;"><code></code><br></div>
</div>
<div style=3D"font-family:Arial;"><br></div>
<div style=3D"font-family:Arial;">What should be done here with very clever=
compiler? <br></div>
<div style=3D"font-family:Arial;">- At first compiler should try to precalc=
ulate it at compile-time. But=20
it's impossible for some large vectors. Let's imagine that we can't=20
precalculate result at compile-time.<br></div>
<div style=3D"font-family:Arial;">- At second we have here two sort functio=
ns, which goes one by one=20
sequentially without any intermediate operations with 'vec' between=20
them. Compiler can't detect without contracts that result after first=20
call boost::sort will be enough and call std::sort isn't required here.=20
Compiler can't detect that functions are semantically identical. But with c=
ontracts we can try to do next hint: let's=20
define that boost::sort and std::sort both have equal post-condition -=20
[[axiom: is_sorted(vec.begin(), vec.end)]]. Compiler see two sequential=20
call of sort functions, call boost::sort, because compiler can't prove=20
that is_sorted is satisfied for boost::sort call. After boost::sort call=20
we exactly know that is_sorted condition is true, and what we see -=20
std::sort also has post-condition is_sorted... And if we already=20
satisfied is_sorted post-condition before std::sort call, we can simply=20
skip this function! <br></div>
</div>
</div>
</blockquote><div style=3D"font-family:Arial;">Here is where you go start t=
o go wrong. The compiler cannot know that is_sorted checks all properties. =
Boost and the standard library generally do reasonable things, so sort actu=
ally sorts. In the real world sort might randomize, and is_sorted verifies =
the maximum value is less than 10 - I've seen humans do stupid things like =
that. (indeed it is often argued that using the shift operators for io is a=
stupid thing in c++) thus in the generic sense what you proposed isn't eno=
ugh either. <br></div>
<div style=3D"font-family:Arial;"><br></div>
<div style=3D"font-family:Arial;">The good news is that you are not wrong, =
just that your reasoning doesn't account for the stupid things that people =
do. If the compiler can understand is_sorted well enough and the lack of si=
de effects in either sort the compiler can eliminate one. Contracts do allo=
w for additional optimization that isn't possible without them. It isn't a =
free lunch for the compiler though, the compiler needs to understand the co=
ntract to optimize with it. <br></div>
<div style=3D"font-family:Arial;"><br></div>
<div style=3D"font-family:Arial;">One other factor. In the real world of co=
ntracts it is often recommended that you don't check is_sorted, that is too=
expensive. You more likely check first < last, or two random elements. =
This contract is much more efficient to check at runtime, but doesn't give =
the compiler as much information. </div>
<div style=3D"font-family:Arial;"><br></div>
<div style=3D"font-family:Arial;"><br></div>
<blockquote type=3D"cite"><div dir=3D"ltr"><div><div style=3D"font-family:A=
rial;"><br></div>
<div style=3D"font-family:Arial;">Here I see at least one problem: function=
can has=20
some side-effects which are not presented in post-condition - it's=20
probably work for library writers<br></div>
</div>
<div><br></div>
<div>I am not a compiler writer and haven't any strong knowledge in this ki=
nd of compiler optimizations. So I am interested - with C++ contracts is it=
possible to implement more optimizations? Which additional optimizations c=
an be implemented with contracts?<br></div>
<div><br></div>
<div>P.S. If you want to play with contracts, you can try this Clang fork w=
ith C++ contracts support: https://github.com/arcosuc3m/clang-contract=
s<br></div>
</div>
<p><br></p><div style=3D"font-family:Arial;">--<br></div>
<div style=3D"font-family:Arial;"> You received this message because you ar=
e subscribed to the Google Groups "ISO C++ Standard - Future Proposals" gro=
up.<br></div>
<div style=3D"font-family:Arial;"> To unsubscribe from this group and stop =
receiving emails from it, send an email to <a href=3D"mailto:std-proposals+=
unsubscribe@isocpp.org">std-proposals+unsubscribe@isocpp.org</a>.<br></div>
<div style=3D"font-family:Arial;"> To post to this group, send email to <a =
href=3D"mailto:std-proposals@isocpp.org">std-proposals@isocpp.org</a>.<br><=
/div>
<div style=3D"font-family:Arial;"> To view this discussion on the web visit=
<a href=3D"https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/08=
3fe6dd-52b6-4b58-bcfc-8aa89606433e%40isocpp.org?utm_medium=3Demail&utm_=
source=3Dfooter">https://groups.google.com/a/isocpp.org/d/msgid/std-proposa=
ls/083fe6dd-52b6-4b58-bcfc-8aa89606433e%40isocpp.org</a>.<br></div>
</blockquote></body>
</html>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/1533215046.2048240.1461141104.01BC6D5=
B%40webmail.messagingengine.com?utm_medium=3Demail&utm_source=3Dfooter">htt=
ps://groups.google.com/a/isocpp.org/d/msgid/std-proposals/1533215046.204824=
0.1461141104.01BC6D5B%40webmail.messagingengine.com</a>.<br />
--_----------=_153321504620482400--
.
Author: florian.csdt@gmail.com
Date: Thu, 2 Aug 2018 06:19:57 -0700 (PDT)
Raw View
------=_Part_226_745093237.1533215997825
Content-Type: multipart/alternative;
boundary="----=_Part_227_514125175.1533215997826"
------=_Part_227_514125175.1533215997826
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Le jeudi 2 ao=C3=BBt 2018 15:04:09 UTC+2, Henry Miller a =C3=A9crit :
>
>
>
> --
> Henry Miller
> ha...@millerfarm.com <javascript:>
>
>
>
> On Wed, Aug 1, 2018, at 6:35 PM, Alexander Zaitsev wrote:
>
> Hello,
>
> As I know the main goal of contracts is program verification. It's very=
=20
> important, but also I am interested in using C++ contracts as additional=
=20
> help for compilers in optimizations.
>
> E.g. we have this code:
>
>
> int foo()=20
> {=20
> std::vector<int> vec =3D {5,4,3,2,1};=20
> =20
> boost::sort(vec.begin(), vec.end());=20
> std::sort(vec.begin(), vec.end());=20
> =20
> int result =3D 0;=20
> for(int i =3D 0; i < 5; ++i)=20
> {=20
> if(i % 2 =3D=3D 0) result +=3D vec[i];=20
> else result -=3D vec[i];=20
> }=20
> return result;=20
> }
>
>
> What should be done here with very clever compiler?=20
> - At first compiler should try to precalculate it at compile-time. But=20
> it's impossible for some large vectors. Let's imagine that we can't=20
> precalculate result at compile-time.
> - At second we have here two sort functions, which goes one by one=20
> sequentially without any intermediate operations with 'vec' between them.=
=20
> Compiler can't detect without contracts that result after first call=20
> boost::sort will be enough and call std::sort isn't required here. Compil=
er=20
> can't detect that functions are semantically identical. But with contract=
s=20
> we can try to do next hint: let's define that boost::sort and std::sort=
=20
> both have equal post-condition - [[axiom: is_sorted(vec.begin(),=20
> vec.end)]]. Compiler see two sequential call of sort functions, call=20
> boost::sort, because compiler can't prove that is_sorted is satisfied for=
=20
> boost::sort call. After boost::sort call we exactly know that is_sorted=
=20
> condition is true, and what we see - std::sort also has post-condition=20
> is_sorted... And if we already satisfied is_sorted post-condition before=
=20
> std::sort call, we can simply skip this function!=20
>
> Here is where you go start to go wrong. The compiler cannot know that=20
> is_sorted checks all properties. Boost and the standard library generally=
=20
> do reasonable things, so sort actually sorts. In the real world sort migh=
t=20
> randomize, and is_sorted verifies the maximum value is less than 10 - I'v=
e=20
> seen humans do stupid things like that. (indeed it is often argued that=
=20
> using the shift operators for io is a stupid thing in c++) thus in the=20
> generic sense what you proposed isn't enough either.=20
>
> The good news is that you are not wrong, just that your reasoning doesn't=
=20
> account for the stupid things that people do. If the compiler can=20
> understand is_sorted well enough and the lack of side effects in either=
=20
> sort the compiler can eliminate one. Contracts do allow for additional=20
> optimization that isn't possible without them. It isn't a free lunch for=
=20
> the compiler though, the compiler needs to understand the contract to=20
> optimize with it.=20
>
=20
It could be enough if there were a notion a fixed point with contracts.
template <class RandomIt>
void sort(RandomIt first, RandomIt last)
[[ensures axiom: is_sorted(first, last)]]
[[fixed_point: is_sorted(first, last)]]
;
This would mean if std::is_sorted(first, last) before the call, then the=20
call has no observable effect (and returns the same value).
Like that, a compiler would be able to optimize one sort away without even=
=20
needing to understand is_sorted because after a call to sort, the compiler=
=20
knows that is_sorted(first, last) is true.
--=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.
To view this discussion on the web visit https://groups.google.com/a/isocpp=
..org/d/msgid/std-proposals/662b003b-3b7d-4d54-a674-5d5bb40487da%40isocpp.or=
g.
------=_Part_227_514125175.1533215997826
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr"><br>Le jeudi 2 ao=C3=BBt 2018 15:04:09 UTC+2, Henry Miller=
a =C3=A9crit=C2=A0:<blockquote class=3D"gmail_quote" style=3D"margin: 0;ma=
rgin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">
<div><div style=3D"font-family:Arial"><br></div>
<div style=3D"font-family:Arial"><br></div>
<div><div>--<br></div>
<div>=C2=A0 Henry Miller<br></div>
<div>=C2=A0 <a href=3D"javascript:" target=3D"_blank" gdf-obfuscated-mailto=
=3D"RBtfhJUZDQAJ" rel=3D"nofollow" onmousedown=3D"this.href=3D'javascri=
pt:';return true;" onclick=3D"this.href=3D'javascript:';return =
true;">ha...@millerfarm.com</a><br></div>
<div><br></div>
</div>
<div><br></div>
<div><br></div>
<div>On Wed, Aug 1, 2018, at 6:35 PM, Alexander Zaitsev wrote:<br></div>
<blockquote type=3D"cite"><div dir=3D"ltr"><div style=3D"font-family:Arial"=
>Hello,<br></div>
<div><div style=3D"font-family:Arial"><br></div>
<div>As I know the main goal of contracts is program verification. It's=
very important, but also I am interested in using C++ contracts as additio=
nal help for compilers in optimizations.<br></div>
<div><br></div>
<div>E.g. we have this code:<br></div>
</div>
<div><br></div>
<div><div style=3D"background-color:rgb(250,250,250);border-top-color:rgb(1=
87,187,187);border-right-color:rgb(187,187,187);border-bottom-color:rgb(187=
,187,187);border-left-color:rgb(187,187,187);border-top-style:solid;border-=
right-style:solid;border-bottom-style:solid;border-left-style:solid;border-=
top-width:1px;border-right-width:1px;border-bottom-width:1px;border-left-wi=
dth:1px;word-wrap:break-word"><div style=3D"font-family:Arial"><code></code=
><br></div>
<div><code><span style=3D"color:rgb(0,0,136)">int</span><span style=3D"colo=
r:rgb(0,0,0)"> foo</span><span style=3D"color:rgb(102,102,0)">()</span><spa=
n style=3D"color:rgb(0,0,0)"> <br></span><span style=3D"color:rgb(102,102,0=
)">{</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 std</span><s=
pan style=3D"color:rgb(102,102,0)">::</span><span style=3D"color:rgb(0,0,0)=
">vector</span><span style=3D"color:rgb(0,136,0)"><int></span><span s=
tyle=3D"color:rgb(0,0,0)"> vec </span><span style=3D"color:rgb(102,102,0)">=
=3D</span><span style=3D"color:rgb(0,0,0)"> </span><span style=3D"color:rgb=
(102,102,0)">{</span><span style=3D"color:rgb(0,102,102)">5</span><span sty=
le=3D"color:rgb(102,102,0)">,</span><span style=3D"color:rgb(0,102,102)">4<=
/span><span style=3D"color:rgb(102,102,0)">,</span><span style=3D"color:rgb=
(0,102,102)">3</span><span style=3D"color:rgb(102,102,0)">,</span><span sty=
le=3D"color:rgb(0,102,102)">2</span><span style=3D"color:rgb(102,102,0)">,<=
/span><span style=3D"color:rgb(0,102,102)">1</span><span style=3D"color:rgb=
(102,102,0)">};</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=A0<br>=C2=
=A0 =C2=A0 boost</span><span style=3D"color:rgb(102,102,0)">::</span><span =
style=3D"color:rgb(0,0,0)">sort</span><span style=3D"color:rgb(102,102,0)">=
(</span><span style=3D"color:rgb(0,0,0)">vec</span><span style=3D"color:rgb=
(102,102,0)">.</span><span style=3D"color:rgb(0,0,136)">begin</span><span s=
tyle=3D"color:rgb(102,102,0)">(),</span><span style=3D"color:rgb(0,0,0)"> v=
ec</span><span style=3D"color:rgb(102,102,0)">.</span><span style=3D"color:=
rgb(0,0,136)">end</span><span style=3D"color:rgb(102,102,0)">());</span><sp=
an style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 std</span><span style=3D"c=
olor:rgb(102,102,0)">::</span><span style=3D"color:rgb(0,0,0)">sort</span><=
span style=3D"color:rgb(102,102,0)">(</span><span style=3D"color:rgb(0,0,0)=
">vec</span><span style=3D"color:rgb(102,102,0)">.</span><span style=3D"col=
or:rgb(0,0,136)">begin</span><span style=3D"color:rgb(102,102,0)">(),</span=
><span style=3D"color:rgb(0,0,0)"> vec</span><span style=3D"color:rgb(102,1=
02,0)">.</span><span style=3D"color:rgb(0,0,136)">end</span><span style=3D"=
color:rgb(102,102,0)">());</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=
=A0<br>=C2=A0 =C2=A0 </span><span style=3D"color:rgb(0,0,136)">int</span><s=
pan style=3D"color:rgb(0,0,0)"> result </span><span style=3D"color:rgb(102,=
102,0)">=3D</span><span style=3D"color:rgb(0,0,0)"> </span><span style=3D"c=
olor:rgb(0,102,102)">0</span><span style=3D"color:rgb(102,102,0)">;</span><=
span style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 </span><span style=3D"co=
lor:rgb(0,0,136)">for</span><span style=3D"color:rgb(102,102,0)">(</span><s=
pan style=3D"color:rgb(0,0,136)">int</span><span style=3D"color:rgb(0,0,0)"=
> i </span><span style=3D"color:rgb(102,102,0)">=3D</span><span style=3D"co=
lor:rgb(0,0,0)"> </span><span style=3D"color:rgb(0,102,102)">0</span><span =
style=3D"color:rgb(102,102,0)">;</span><span style=3D"color:rgb(0,0,0)"> i =
</span><span style=3D"color:rgb(102,102,0)"><</span><span style=3D"color=
:rgb(0,0,0)"> </span><span style=3D"color:rgb(0,102,102)">5</span><span sty=
le=3D"color:rgb(102,102,0)">;</span><span style=3D"color:rgb(0,0,0)"> </spa=
n><span style=3D"color:rgb(102,102,0)">++</span><span style=3D"color:rgb(0,=
0,0)">i</span><span style=3D"color:rgb(102,102,0)">)</span><span style=3D"c=
olor:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 </span><span style=3D"color:rgb(102,102=
,0)">{</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 =C2=A0 =C2=
=A0 </span><span style=3D"color:rgb(0,0,136)">if</span><span style=3D"color=
:rgb(102,102,0)">(</span><span style=3D"color:rgb(0,0,0)">i </span><span st=
yle=3D"color:rgb(102,102,0)">%</span><span style=3D"color:rgb(0,0,0)"> </sp=
an><span style=3D"color:rgb(0,102,102)">2</span><span style=3D"color:rgb(0,=
0,0)"> </span><span style=3D"color:rgb(102,102,0)">=3D=3D</span><span style=
=3D"color:rgb(0,0,0)"> </span><span style=3D"color:rgb(0,102,102)">0</span>=
<span style=3D"color:rgb(102,102,0)">)</span><span style=3D"color:rgb(0,0,0=
)"> =C2=A0 =C2=A0result </span><span style=3D"color:rgb(102,102,0)">+=3D</s=
pan><span style=3D"color:rgb(0,0,0)"> vec</span><span style=3D"color:rgb(10=
2,102,0)">[</span><span style=3D"color:rgb(0,0,0)">i</span><span style=3D"c=
olor:rgb(102,102,0)">];</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 </span><span style=3D"color:rgb(0,0,136)">else</span><=
span style=3D"color:rgb(0,0,0)"> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0result </span><span style=3D"color:rgb(102,102,0)">-=3D</span><span s=
tyle=3D"color:rgb(0,0,0)"> vec</span><span style=3D"color:rgb(102,102,0)">[=
</span><span style=3D"color:rgb(0,0,0)">i</span><span style=3D"color:rgb(10=
2,102,0)">];</span><span style=3D"color:rgb(0,0,0)"> <br>=C2=A0 =C2=A0 </sp=
an><span style=3D"color:rgb(102,102,0)">}</span><span style=3D"color:rgb(0,=
0,0)"> <br>=C2=A0 =C2=A0 </span><span style=3D"color:rgb(0,0,136)">return</=
span><span style=3D"color:rgb(0,0,0)"> result</span><span style=3D"color:rg=
b(102,102,0)">;</span><span style=3D"color:rgb(0,0,0)"> <br></span><span st=
yle=3D"color:rgb(102,102,0)">}</span><span style=3D"color:rgb(0,0,0)"></spa=
n></code></div>
<div style=3D"font-family:Arial"><code></code><br></div>
</div>
<div style=3D"font-family:Arial"><br></div>
<div style=3D"font-family:Arial">What should be done here with very clever =
compiler? <br></div>
<div style=3D"font-family:Arial">- At first compiler should try to precalcu=
late it at compile-time. But=20
it's impossible for some large vectors. Let's imagine that we can&#=
39;t=20
precalculate result at compile-time.<br></div>
<div style=3D"font-family:Arial">- At second we have here two sort function=
s, which goes one by one=20
sequentially without any intermediate operations with 'vec' between=
=20
them. Compiler can't detect without contracts that result after first=
=20
call boost::sort will be enough and call std::sort isn't required here.=
=20
Compiler can't detect that functions are semantically identical. But wi=
th contracts we can try to do next hint: let's=20
define that boost::sort and std::sort both have equal post-condition -=20
[[axiom: is_sorted(vec.begin(), vec.end)]]. Compiler see two sequential=20
call of sort functions, call boost::sort, because compiler can't prove=
=20
that is_sorted is satisfied for boost::sort call. After boost::sort call=20
we exactly know that is_sorted condition is true, and what we see -=20
std::sort also has post-condition is_sorted... And if we already=20
satisfied is_sorted post-condition before std::sort call, we can simply=20
skip this function!=C2=A0<br></div>
</div>
</div>
</blockquote><div style=3D"font-family:Arial">Here is where you go start to=
go wrong. The compiler cannot know that is_sorted checks all properties. B=
oost and the standard library generally do reasonable things, so sort actua=
lly sorts. In the real world sort might randomize, and is_sorted verifies t=
he maximum value is less than 10 - I've seen humans do stupid things li=
ke that. (indeed it is often argued that using the shift operators for io i=
s a stupid thing in c++) thus in the generic sense what you proposed isn=
9;t enough either.=C2=A0<br></div>
<div style=3D"font-family:Arial"><br></div>
<div style=3D"font-family:Arial">The good news is that you are not wrong, j=
ust that your reasoning doesn't account for the stupid things that peop=
le do. If the compiler can understand is_sorted well enough and the lack of=
side effects in either sort the compiler can eliminate one. Contracts do a=
llow for additional optimization that isn't possible without them. It i=
sn't a free lunch for the compiler though, the compiler needs to unders=
tand the contract to optimize with it.=C2=A0<br></div>
</div></blockquote><div>=C2=A0</div><div>It could be enough if there were a=
notion a fixed point with contracts.</div><div><br></div><div><div style=
=3D"background-color: rgb(250, 250, 250); border-color: rgb(187, 187, 187);=
border-style: solid; border-width: 1px; overflow-wrap: break-word;" class=
=3D"prettyprint"><code class=3D"prettyprint"><div class=3D"subprettyprint">=
<span style=3D"color: #008;" class=3D"styled-by-prettify">template</span><s=
pan style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=
=3D"color: #660;" class=3D"styled-by-prettify"><</span><span style=3D"co=
lor: #008;" class=3D"styled-by-prettify">class</span><span style=3D"color: =
#000;" class=3D"styled-by-prettify"> </span><span style=3D"color: #606;" cl=
ass=3D"styled-by-prettify">RandomIt</span><span style=3D"color: #660;" clas=
s=3D"styled-by-prettify">></span><span style=3D"color: #000;" class=3D"s=
tyled-by-prettify"><br></span><span style=3D"color: #008;" class=3D"styled-=
by-prettify">void</span><span style=3D"color: #000;" class=3D"styled-by-pre=
ttify"> sort</span><span style=3D"color: #660;" class=3D"styled-by-prettify=
">(</span><span style=3D"color: #606;" class=3D"styled-by-prettify">RandomI=
t</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> first</s=
pan><span style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span=
style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D=
"color: #606;" class=3D"styled-by-prettify">RandomIt</span><span style=3D"c=
olor: #000;" class=3D"styled-by-prettify"> </span><span style=3D"color: #00=
8;" class=3D"styled-by-prettify">last</span><span style=3D"color: #660;" cl=
ass=3D"styled-by-prettify">)</span><span style=3D"color: #000;" class=3D"st=
yled-by-prettify"><br>=C2=A0 </span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">[[</span><span style=3D"color: #000;" class=3D"styled-by=
-prettify">ensures </span><span style=3D"color: #008;" class=3D"styled-by-p=
rettify">axiom</span><span style=3D"color: #660;" class=3D"styled-by-pretti=
fy">:</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> is_s=
orted</span><span style=3D"color: #660;" class=3D"styled-by-prettify">(</sp=
an><span style=3D"color: #000;" class=3D"styled-by-prettify">first</span><s=
pan style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span style=
=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"color=
: #008;" class=3D"styled-by-prettify">last</span><span style=3D"color: #660=
;" class=3D"styled-by-prettify">)]]</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"><br>=C2=A0 </span><span style=3D"color: #660;" cla=
ss=3D"styled-by-prettify">[[</span><span style=3D"color: #000;" class=3D"st=
yled-by-prettify">fixed_point</span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">:</span><span style=3D"color: #000;" class=3D"styled-by-=
prettify"> is_sorted</span><span style=3D"color: #660;" class=3D"styled-by-=
prettify">(</span><span style=3D"color: #000;" class=3D"styled-by-prettify"=
>first</span><span style=3D"color: #660;" class=3D"styled-by-prettify">,</s=
pan><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span=
style=3D"color: #008;" class=3D"styled-by-prettify">last</span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">)]]</span><span style=3D"col=
or: #000;" class=3D"styled-by-prettify"><br></span><span style=3D"color: #6=
60;" class=3D"styled-by-prettify">;</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"><br></span></div></code></div><br></div><div>This =
would mean if <span style=3D"font-family: courier new, monospace;">std::is_=
sorted(first, last)</span> before the call, then the call has no observable=
effect (and returns the same value).</div><div>Like that, a compiler would=
be able to optimize one sort away without even needing to understand <span=
style=3D"font-family: courier new, monospace;">is_sorted</span> because af=
ter a call to <span style=3D"font-family: courier new, monospace;">sort</sp=
an>, the compiler knows that <span style=3D"font-family: courier new, monos=
pace;">is_sorted(first, last)</span> is true.<br></div></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/662b003b-3b7d-4d54-a674-5d5bb40487da%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/662b003b-3b7d-4d54-a674-5d5bb40487da=
%40isocpp.org</a>.<br />
------=_Part_227_514125175.1533215997826--
------=_Part_226_745093237.1533215997825--
.