-
Notifications
You must be signed in to change notification settings - Fork 2
/
contract_assertions_versus_static_analysis_and_safety.html
907 lines (720 loc) · 40.7 KB
/
contract_assertions_versus_static_analysis_and_safety.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
<!DOCTYPE html>
<html lang="en"><head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<style>
pre {font-family: "Consolas", "Lucida Console", monospace; margin-left:20pt; }
code {font-family: "Consolas", "Lucida Console", monospace; }
pre > i { font-family: "Consolas", "Lucida Console", monospace; font-style:italic; }
code > i { font-family: "Consolas", "Lucida Console", monospace; font-style:italic; }
pre > em { font-family: "Consolas", "Lucida Console", monospace; font-style:italic; }
code > em { font-family: "Consolas", "Lucida Console", monospace; font-style:italic; }
dl > dt { font-style:italic; }
body { font-family: "Calibri" }
h1 { margin-top: 3ex; margin-bottom: 2ex }
/* h2 { margin-top: 9ex; margin-bottom: 3ex }*/
@media (prefers-color-scheme: dark) {
body { background: #111; color: #ccc; }
a { color: #38f; }
a:visited { color: #a4d; }
.sect { color: #ccc; }
del { text-decoration: line-through; color: #EE9999; }
ins { text-decoration: underline; color: #99EE99; }
blockquote.std { color: #ccc; background-color: #2A2A2A; border: 1px solid #3A3A3A; padding-left: 0.5em; padding-right: 0.5em; }
blockquote.stddel { text-decoration: line-through; color: #ccc; background-color: #221820; border: 1px solid #332228; padding-left: 0.5em; padding-right: 0.5em; ; }
blockquote.stdins { text-decoration: underline; color: #ccc; background-color: #182220; border: 1px solid #223328; padding: 0.5em; }
table { border: 1px solid #ccc; border-spacing: 0px; margin-left: auto; margin-right: auto; }
}
@media (prefers-color-scheme: light) {
body { background: white; color: black; }
del { text-decoration: line-through; color: #8B0040; }
ins { text-decoration: underline; color: #005100; }
blockquote.std { color: #000000; background-color: #F1F1F1; border: 1px solid #D1D1D1; padding-left: 0.5em; padding-right: 0.5em; }
blockquote.stddel { text-decoration: line-through; color: #000000; background-color: #FFEBFF; border: 1px solid #ECD7EC; padding-left: 0.5em; padding-right: 0.5em; ; }
blockquote.stdins { text-decoration: underline; color: #000000; background-color: #C8FFC8; border: 1px solid #B3EBB3; padding: 0.5em; }
table { border: 1px solid black; border-spacing: 1px; margin-left: auto; margin-right: auto; }
}
.comment em { font-family: "Calibri"; font-style:italic; }
p.example { margin-left: 2em; }
pre.example { margin-left: 2em; }
div.example { margin-left: 2em; }
div.poll { margin-left: 2em; }
code.extract { background-color: #F5F6A2; }
pre.extract { margin-left: 2em; background-color: #F5F6A2; border: 1px solid #E1E28E; }
p.function { }
.attribute { margin-left: 2em; }
.attribute dt { float: left; font-style: italic; padding-right: 1ex; }
.attribute dd { margin-left: 0em; }
.editor { color: #4444BB; font-style: normal; background-color: #DDDDDD; }
tab { padding-left: 4em; }
tab3 { padding-left: 3em; }
.link { float: right; font-family: "Consolas", "Lucida Console", monospace; font-size:80% }
table.header { border: none; border-spacing: 0; margin-left: 0px; font-style: normal; }
td.header { border: none; border-spacing: 0; margin-left: 0px; font-style: normal; }
.header { border: none; border-spacing: 0; margin-left: 0px; font-style: normal; }
table.poll { border: 1px solid black; border-spacing: 0px; margin-left: 0px; font-style: normal; }
th { text-align: left; vertical-align: top; padding-left: 0.4em; /*padding-right: 0.4em; border-bottom:1px dashed;*/ }
td { text-align: left; padding-left: 0.4em; padding-right: 0.4em; /*border-right:1px dashed; */}
tr { border: solid; border-width: 1px 0; border-bottom:1px solid blue }
.revision { /*color: #005599;*/ }
.grammar { list-style-type:none }
</style>
<title>Contract assertions versus static analysis and 'safety'</title>
</head>
<body>
<table class="header"><tbody>
<tr>
<th>Document number: </th><th> </th><td class="header">P3376R0</td>
</tr>
<tr>
<th>Date: </th><th> </th><td class="header">2024-10-14</td>
</tr>
<tr>
<th>Audience: </th><th> </th><td class="header">SG21, EWG</td>
</tr>
<tr>
<th>Reply-to: </th><th> </th><td class="header">
<address>Andrzej Krzemieński <akrzemi1 at gmail dot com></address>
</td>
</tr>
</tbody></table>
<h1>Contract assertions versus static analysis and ‘safety’</h1>
<p> This paper tries to systematize the discussion regarding how contract annotations
address ‘safety’ and how they interact with
‘static analysis’. We describe two different definitions of
‘safety’, and describe different kinds of ‘static analysis’.
Depending on which definition one adopts, one draws different conclusions as to
what the contract annotations should do.
</p>
<p> We also review, in the context of safety and static analysis, the two visions for
contract annotations:</p>
<ol>
<li>Predicates are just C++ code, modulo the treatment of <em>unqualified-id</em>s as <code>const</code>,
as proposed in <a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”"
>[P2900R9]</a>.</li>
<li>Predicates are UB-free, side-effect-free <em>strict</em> expressions (with an escape
hatch to switch to "just C++ code"), as proposed in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2680r1.pdf"
title="Gabriel Dos Reis, “Contracts for C++: Prioritizing Safety”">[P2680R1]</a>
and
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>,
and argued for in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>.
</li>
</ol>
<h2><a class="sect" id="1">1.</a> The perception of safety</h2>
<p> As a human, a consumer and a user of systems, tools and mechanisms, the question that is important to me is:
<em>is this safe?</em> By which I mean, can this cause harm to me, to other people, to my privacy, my savings, my environment?
In response to this, we have the notion of <em>system safety</em>, which, as
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3297r1.pdf"
title="Christian Eltzschig, Mathias Kraus, Ryan McDougall, Pez Zarifian, “C++26 Needs Contract Checking”">[P3297R1]</a>
reminds us, is a practice of performing all possible tests at all possible integration levels, in order to be able to draw
<em>statistical</em> conclusions as to how likely the system is to cause harm. The key aspects here are:</p>
<ul>
<li>it applies to the system as a whole,</li>
<li>it is a statistical property.</li>
</ul>
<p> This notion is very different from the notions like "UB safety" / "memory safety"
/ "exception safety" / "thread safety". It doesn't talk about "safe language
constructs" or "safe languages". It is about the final product to satisfy certain
properties. In pursuit of this ultimate goal, it is fine to employ a feature
that has the <em>potential</em> to trigger UB (undefined behavior), as long
as the system as a whole becomes less likely to cause harm.
</p>
<p> On the other hand, we have the definition of a "safe operation" in a language,
as formulated by David Abrahams in
<a href="https://youtu.be/QthAU-t3PQ4?si=b6yz24Ps5B5DXG2R"
title="David Abrahams, “Values: Safety, Regularity, Independence, and the Future of Programming”">[ABRAHAMS22]</a>:
</p>
<blockquote>
A safe operation is one that can't cause undefined behavior.
</blockquote>
<p> In this view, accessing any object via a reference of unknown origin is an unsafe
operation:</p>
<pre>
bool has_name(string const& s) <em>// reference may be dangling</em>
{
return !s.empty(); <em>// may be accessing a non-object</em>
}
</pre>
<p> UB- and memory-safe code can also be source of unsafe programs. Consider:</p>
<pre>
bool should_launch_missiles(
bool enemy_launched_missles,
bool system_armed)
{
return enemy_launched_missles
|| system_armed; <em>// bug: should be `&&`</em>
}
</pre>
<p> It can also be shown that naively increasing UB-safety can decrease system safety.
Consider:</p>
<pre>
bool alert()
{
bool alerting_on = check_if_alerting_is_on();
bool alert_user; <em>// #1 uninitialized variable</em>
Alerts all_alerts = get_all_alerts(alert_user); <em>// #2 typo: wrong variable passed</em>
alert_user = filter_by_user(all_alerts);
log_state(alerting_on, alert_user);
return alert_user;
}
</pre>
<p> This function has a bug. The intention was to pass variable
<code>alerting_on</code> to function <code>get_all_alerts</code> in #2.
As a consequence, when this function is invoked, it triggers UB in C++23,
because variable
<code>alert_user</code> is read prior to any value assignment in #2.
If a compiler issues a warning about this, and a programmer naively applies
the advice "always initialize your variables", they will assign any value in #1,
and the warning will be silenced, advice will be followed, UB will be prevented,
but a life-critical program will become incorrect, and therefore unsafe.</p>
<p> In contrast, when the programmer doesn't try to initialize the variable, and runs
a tool like Clang-Tidy, the tool will highlight places #1 and #2 in the code,
and the programmer will be drawn attention to the fact that a typo has occurred
at #2, and will be able to pass the correct variable to the function.
Thus, our goal cannot be "just don't have UB": it should be "have correct code".
Program correctness is an important factor in system safety.
</p>
<p> Undefined behavior is always a consequence of a bug. On the other hand, in
consequence, it can trigger more bugs. Thus, a tool that (1) prevents UB and (2)
does not conceal bugs is required. In this spirit, C++ has now the notion of
<em>erroneous behavior</em>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html"
title="Thomas Köppe, “Erroneous behaviour for uninitialized reads”">[P2795R5]</a>).
</p>
<p> Bottom line: while there is an overlap between UB-safety and system safety,
they are in general different goals. </p>
<h2><a class="sect" id="2">2.</a> Static analysis</h2>
<p> How can a program analysis — static or dynamic — conclude
that a program is correct, or incorrect? You measure the program correctness by
comparing its behavior against the programmer intentions or against the program
specification. One thing that helps here is undefined behavior: it is a safe
assumption that it is never the programmer's intention to cause undefined behavior,
so whenever we can demonstrate that a program hits or would hit UB, it is incorrect.
We do not know which part exactly is incorrect, but we can be <em>sure</em> that at
least one part is.
</p>
<p> Similarly, contract annotations will also be able to help tools performing program
correctness verification. This is because they can encode parts of the program
specification. It is safe
to assume that it is never the programmers intention to have any contract predicate
evaluate to <code>false</code>.
</p>
<p> There are different goals that static analysis tools can have. Here, we will describe
only one, in two variants. This is where a tool, looking at a single translation unit,
tries to answer
the question if a given function <code>f</code> calls all functions in its body
<em>in contract</em>; that is, if all preconditions of the called functions evaluate
to <code>true</code>.
</p>
<pre>
bool pre(X const& x); <em>// not defined in this translation unit</em>
X make() post(r: pred(x));
void use(X const& x) pre(pred(x));
void f(X const& a, X const& b, X const& c)
pre(pred(a))
{
use(x); <em>// #1 OK, matches with f's precond </em>
if (pred(b))
use(b); <em>// #2 OK, matches with condition in `if`-statement </em>
use(make()); <em>// #3 OK, matches with the postcond of `make()` </em>
use(c); <em>// #4 WARNING: nothing to match with</em>
}
</pre>
<p> In this form of analysis, we treat predicates in the preconditions of the called functions
as <em>symbols</em>. That is, we do not try to determine what is evaluated inside them.
Instead, if function <code>use()</code> has symbol <code>pred(x)</code> associated with
its argument, we try to determine, if the same symbol has been produced by the
preceding part of the function body. The call at #1 is ok because this symbol is already
a precondition on <code>f()</code>. The call at #2 is ok, because <code>pred()</code>
is already checked in the <code>if</code>-statement. The call at #3 is ok, because the same
symbol is produced by the postcondition of <code>make()</code>. The call at #4 is not
ok, because we cannot find symbol <code>pred(c)</code> in the scope of function <code>f()</code>,
so a warning is produced.
</p>
<p> In order for thus described analysis to give <em>certainty</em> of correctness,
a number of conditions would have to be satisfied:</p>
<ol>
<li>The code invoked in function <code>f()</code>, for instance the definition of
function <code>use()</code>, does not have UB.</li>
<li>The definitions of contract annotations do not have UB.</li>
<li>The code invoked in function <code>f()</code>, for instance the definition of
function <code>use()</code>, does not alter the state of the program in a way that
changes the results of <code>pred()</code> at different points in the function execution.
</li>
<li>The definition of <code>pred()</code>, doesn't alter the state of the program.
</li>
</ol>
<p> Because contract annotations are a new feature, we are not bound by backwards
compatibility requirement and can afford defining it the way we need. So it is
possible to enforce the assumptions #2 and #4 above. This is advocated for in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>.
</p>
<p> An alternative, is to leave all four points as assumptions. This results in
reduced confidence, but is still valuable. This would render the type of analysis
similar to the one for axiom-kind
predicates described in <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2176r0.html"
title="Andrzej Krzemieński, “A different take on inexpressible conditions”"
>[P2176R0]</a>.</p>
<p> We will call these two form of verification <em>strict precondition matching</em> and
<em>relaxed precondition matching</em>, respectively.</p>
<!--
<p> In this vein, we find the initial example in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>
illustrates something different than what it claims to illustrate. Paraphrasing a bit:
</p>
<pre>
int f(int a) { return a + 100; }
int g(int a) pre(f(a) > a)
{
int r = a - f(a);
return 2 * r;
}
</pre>
<p><a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>
goes to say that after potential inlining the compiler sees expression <code>a + 100 > a</code>,
and it feels free to assume that the expression always either returns <code>true</code>
or has UB. This is correct, but we should also observe another thing. We should assume that
the programmer consciously chooses the predicates, that they understand what expression
<code>f(a)</code> represents, and that they were aware that the underlying full condition is
<code>a + 100 > a</code>. Why would they put such a tautologous condition?
The only plausible explanation is that the programmer
intended to put a different condition, but planted a bug. Which seems to illustrate that
this is bugs that cause UB.
</p>
-->
<h2><a class="sect" id="3">3.</a>
Why is <a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>
useful already</h2>
<p> Contract annotations are a tool for communicating parts of program specification.
They can be used for detecting bugs. Detecting and removing bugs increases system
safety.
</p>
<p> The primary value that
<a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>
brings to the table is:</p>
<ul>
<li> the standardized notation for contract assertions and</li>
<li> the position where you put them.</li>
</ul>
<p> Precondition assertions are visible in the translation unit where the guarantee is
delivered by the caller;
postconditions are visible in the translation unit where the guarantee is consumed.
This means that a static analysis task of verifying if preconditions of the called
functions are satisfied by postconditions of other
called functions can now be narrowed to a single translation unit, and is therefore more affordable
in terms of resources.</p>
<p> The fact that the syntax for expressing contract annotations is standardized,
enables different tools to recognize the syntax, and expect that third party libraries
will use it. The tools can now perform static analysis on a new library code
out of the box, rather than instructing the users to first put the tool-specific
annotations. Library writers can use the standard notation for expressing the contract,
rather than trying to figure out which tool they are going to target.
</p>
<p> Precondition and postcondition assertions
can now be placed in the right sequence between other operations. Currently, with assertion macros
(which work as either expressions or statements), it is difficult to express that a precondition
should hold before the constructor initializer list starts. Similarly, it is difficult to
express a postcondition when a function has multiple return statements or when the expression in the
<code>return</code>-statement produces an rvalue.
</p>
<p> The contract predicates are regular C++ code, so they can be runtime-evaluated if needed.
The value added to the runtime-checking of contract assertions is that, apart from calling them in the right
places, you have a finer-grained control over which assertions are actually called. A library can be compiled
in a no-runtime-checking mode, but the precondition runtime checks can still be added in the caller code.
This is described in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2780r0.html"
title="Ville Voutilainen, “Caller-side precondition checking, and Eval_and_throw”">[P2780R0]</a>.
</p>
<p> Next, the way precondition assertions are expected to help prevent bugs
is not necessarily through runtime evaluation or static analysis,
but because IDEs can simply display them in places where functions
are called. Imagine that a programmer writes the following function
call and gets the following hint from the compiler, where the precondition
is displayed but with function argument names substituted for
parameter names:
</p>
<pre>
int min = config.read("min");
int max = config.read("max");
return is_in_range(val, min, max);
/*-------------------------
| PRE: val <= min |
-------------------------*/
</pre>
<p> The user expected the precondition to say <code>min <= max</code>,
so they are alerted that something is wrong. They are now motivated to go and read
the function declaration, which is:
</p>
<pre>
bool is_in_range(int lo, int hi, int v)
pre (lo <= hi);
</pre>
<p> And now the programmer learns that they put the arguments to the function
in the wrong order. Bug prevented!</p>
<p> Further, because contract assertions are visible on function declarations,
<a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>
enables the form of static analysis that we called the relaxed precondition matching.
This analysis can be contained to a single translation unit. It doesn't give as certain
correctness results as
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>
would expect, but allows the predicates to be normal C++ code, and sufficient to detect bugs in
programs, even if not performing <em>full</em> correctness proofs.
Remember that system safety is a
statistical property.
</p>
<p> Finally, by the anecdotal evidence, a significant portion of the precondition and postcondition predicates are of the form: </p>
<pre>
i > 0 <em>/* int comparisons */</em>
p != nullptr
vec.empty()
vec.size() > i
x.has_value() <em>/* inline fun that only returns the
value of a boolean member data */</em>
</pre>
<p> They are simple enough, using only inline functions, that the assumption of non-UB and no-side-effect often holds.
</p>
<!--
<p> Another form of static analysis is also already enabled, for the case as the one in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>:
</p>
<pre>
bool pred(int x);
int func_a() post(r: pred(r));
void func_b(int x) pre(pred(x));
func_b(func_a());
</pre>
<p> the static analyzer can compare the structures of two predicates,
modulo the parameters referenced, and if they are equal, perform a symbolic
analysis, where the predicates are the symbols compared. While it may give
false positives and false negatives, and the analyzed code may be different than runtime code
(in the case of nasty things in predicates), the results of such analysis may still
be useful, and do not require solving the halting problem.</p>
<p> Second, when one uses primarily predicates as simple as the ones above, one doesn't
appreciate that much a tool that helps detect side effects in precondition predicates.</p>
<p> Next, while contract predicates are also (potentially buggy) code, the whole idea works,
because programmers put way simpler code in contract predicates that in function bodies.
So while the predicates have potential for bugs, this potential is smaller.</p>
-->
<h2><a class="sect" id="4">4.</a> <em>Strict</em> assertions</h2>
<p> <em>Strict</em> assertions, as described in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2680r1.pdf"
title="Gabriel Dos Reis, “Contracts for C++: Prioritizing Safety”">[P2680R1]</a>
and
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>,
would guarantee zero modifications to the program state (outside the predicate), and zero UB.
That is, if they were implementable. C++ is so saturated with <em>narrow-contract</em>
constructs that trying to reject code with the UB potential effectively means
preventing practically any code.
</p>
<p> <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>
from the outset gives up on preventing UB caused by data races. This is just too difficult.
As the next thing, it will also need to give up on memory-safety-related UB, or alternatively
narrow the applicability of strict predicates only to functions taking non-view parameters by value.
More often than not, functions parameters are references. When such a function is
invoked, the reference may already refer to a non-object: that is, be a dangling reference. However "safe"
the internals of a strict predicate are, it already starts with a corrupt input. We could say
that <code>std::object_address</code> has special powers where upon the function call, in the caller
it tries to prove that the reference points to a valid object, and when this cannot be proven
we get a compiler error. Let's picture a common case:
</p>
<pre>
void foo(int const& i)
pre(std::object_address(&i) && i > 0);
void bar(int const& i)
{
if (i > 0)
foo(i);
}
</pre>
<p> Inside function <code>bar</code> we cannot validate if the reference is non-dangling,
because <code>bar</code> already receives a reference. This is a common case, and it would
fail to compile. We would get a feature that is UB-safe but not applicable to the real
code.
</p>
<p> True, there are languages, that can guarantee zero memory issues, but this is because
they are memory-safe all across. But here we are talking about a small 'safe' execution
of a predicate after a long 'unsafe' execution of the program. This boundary between
the 'unsafe' and the 'safe', corrupts the safety guarantee of the 'safe' part.
</p>
<p> Next, given that <em>conveyor</em> functions do not affect overload resolution,
strict predicates will behave uncomfortably in cases where
a class offers a <code>const</code> and a non-<code>const</code> overload of a member
function: a case very common in STL containers. The following small example illustrate this.
</p>
<pre>
template <typename T>
class Wrapper
{
public:
T& get() & conveyor;
const T& get() const& conveyor;
};
</pre>
<p> And now we want to write a function with a strict precondition:</p>
<pre>
void modify(Wrapper<int> & w)
pre(w.get() > 0);
</pre>
<p> This fails to compile because <code>w</code> is function argument and it would be
passed to a function (<code>Wrapper::get</code>) taking the argument by a
non-<code>const</code> reference, which is banned by
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>.
The author would have to change the predicate to:
</p>
<pre>
void modify(Wrapper<int> & w)
pre(std::as_const(w.get()) > 0);
</pre>
<p> This works, but forces us to type a different predicate than we intended, and this
is likely to impede some forms of static analysis:
</p>
<pre>
void work(Wrapper<int> & w)
{
if (w.get() > 0) <em>// <-- same predicate as</em>
modify(w); <em>// in the precondition?</em>
}
</pre>
<p> Next, is it possible to implement function <code>std::vector::operator[]</code>
as a conveyor? The implementation would probably look like this.
</p>
<pre>
T const& vector::operator[](index_type i) const
{
return _array[i];
}
</pre>
<p> In the return statement we have a postfix expression dealing with two runtime
values, one of which is an address of a dynamically allocated array.
This cannot pass as a conveyor, because it is impossible to prove
that this access is valid without a difficult flow analysis. There would have
to be a "disable conveyor safety" block that allows doing "unsafe" things
inside the conveyor functions. But that would compromise the initial
goals of guaranteeing no UB.
</p>
<p> Next, while the idea of preventing UB in constrained environments (such as conveyor functions)
is fine in general, some ways of achieving it, proposed in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>,
are not acceptable, and could be themselves source of bugs, and therefore negatively
contribute to system safety. For instance, the idea that the
arithmetic overflow should produce an implementation-defined value,
resulting in wrap-around arithmetic. The effect would be that programmers would
start relying on the new semantics, and one could no longer detect whether some
situations in code are intentional or not. Also, the same expressions would now render
different values in precondition assertions and in function bodies:
</p>
<pre>
int f (int i, int j)
pre (i > 0)
pre (j > 0)
pre (j + i < 0) <em>// clever way to check if the combined values are big enough</em>
{ <em>// under a wrap-around arithmetic</em>
if (i > 0)
if (j > 0)
if (j + i < 0) <em>// skipped as either false or UB. </em>
return 0;
_Undefined_behavior(); // UB is hit.
}
f(INT_MAX, 2); <em>// precondition passes, but in-body check fails</em>
</pre>
<p> This particular aspect could be fixed by saying that
arithmetic overflow is an erroneous behavior
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html"
title="Thomas Köppe, “Erroneous behaviour for uninitialized reads”">[P2795R5]</a>)
and results in unspecified value. Alternatively, we could only allow
addition provided that there is code in the close vicinity that
proves that the addition will not overflow:
</p>
<pre>
int f1 (int i, int j)
pre (j + i > 0) <em>// Error: could overflow</em>
int f2 (int i, int j)
pre (std::add_sat(j, i) > 0) <em>// OK, cannot overflow</em>
int f3 (int i, int j)
pre (-100 < i && i < 100)
pre (-100 < j && j < 100)
pre (j + i > 0) <em>// OK, we know max ranges</em>
</pre>
<p> In summary, the design for strict contract assertions is not just buggy,
it doesn't address fundamental issues. The advertised approach "let's
start with something small and then expand" doesn't work here. The proposed
small initial state is too small, and there is not even a sketch of the plan
on how (if at all) it can be expanded. The present design for strict contract
assertions doesn't give confidence that even if we postpone the adoption of contacts
by additional three or six years, we would get something that fulfills
the promise of usable UB-free and side-effect-free predicates.
</p>
<p> The author's requirement on the viability of the "strict assertions" solutions are two.
First, not substituting a seemingly well behavior for UB when a programmer plants
a bug in the predicate; instead, substitute it for a diagnosable error.
Second, the solution should allow the expression of the following types of predicates.
</p>
<pre>
i > 0 <em>/* int comparisons */</em>
p != nullptr
vec.empty()
vec.size() > i
x.has_value() <em>/* only returns the value of
a boolean member data */</em>
</pre>
<!--
<p> Because in general assigning arbitrary behavior in the place of
unintended UB can be a way of concealing bugs. C++ constructs have
the potential to cause UB, but UB is only triggered when the construct
is used incorrectly. The same potential for UB combined with a bug can
give good warnings (no false positives or false negatives) during program analysis:
it is always safe to assume that the programmer never intends to plant a UB.
This has been described in
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html"
title="Thomas Köppe, “Erroneous behaviour for uninitialized reads”">[P2795R5]</a>.
</p>
-->
<h2><a class="sect" id="5">5.</a> Discussion</h2>
<p> <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>,
much like <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>,
argues that even when the strict contract assertions are present in C++,
there would still be a need for <em>relaxed</em> contract assertions,
which behave practically like assertions in
<a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>.
One could imagine the adoption order where relaxed predicates are included in C++26,
and strict predicates are included in one of the next revisions of C++.
However, <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>
argues that releasing relaxed predicates before strict predicates would be a failure.
This claim is made without providing sufficient rationale.
How is "adding relaxed in C++26 and strict in C++29" worse from "adding both in C++29"?
On the other hand, <a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3297r1.pdf"
title="Christian Eltzschig, Mathias Kraus, Ryan McDougall, Pez Zarifian, “C++26 Needs Contract Checking”">[P3297R1]</a>
argues that delaying the addition of contracts (even in <a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a> form)
will damage the C++ community. We seem to have two conflicting future predictions.
</p>
<p> One incompatibility of the "relaxed first, strict second" approach with the
"strict and relaxed together" approach
is about which of the two types of contract assertions is the default.
The strict one would be a better default as this would encourage users to choose this
type, and therewith offer additional benefits of correctness checking.
Would the change to <a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>
that requires the addition of contextual keyword <code>relaxed</code> after <code>pre</code>,
<code>post</code> and <code>contract_assert</code> address the concerns?
</p>
<h2><a class="sect" id="6">6.</a> Acknowledgments</h2>
<p> Ville Voutilainen helped me understand the strict predicates better,
and offered a critique of the paper which significantly improved
its quality.
</p>
<h2><a class="sect" id="7">7.</a>References</h2>
<ul>
<li>[ABRAHAMS22] — David Abrahams,
"Values: Safety, Regularity, Independence, and the Future of Programming", <br>
(<a href="https://youtu.be/QthAU-t3PQ4?si=b6yz24Ps5B5DXG2R">"https://youtu.be/QthAU-t3PQ4?si=b6yz24Ps5B5DXG2R"</a>).
</li>
<!--
<a href="https://youtu.be/QthAU-t3PQ4?si=b6yz24Ps5B5DXG2R"
title="David Abrahams, “Values: Safety, Regularity, Independence, and the Future of Programming”">[ABRAHAMS22]</a>
-->
<li>[P0542R5] — G. Dos Reis, J. D. Garcia, J. Lakos, A. Meredith, N. Myers, B. Stroustrup,
"Support for contract based programming in C++" <br>
(<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0542r5.html">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0542r5.html</a>).
</li>
<!--
<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0542r5.html"
title="G. Dos Reis, J. D. Garcia, J. Lakos, A. Meredith, N. Myers, B. Stroustrup, “Support for contract based programming in C++”"
>[P0542R5]</a>
-->
<li>[P2176R0] — Andrzej Krzemieński,
"A different take on inexpressible conditions" <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2176r0.html">https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2176r0.html</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2176r0.html"
title="Andrzej Krzemieński, “A different take on inexpressible conditions”"
>[P2176R0]</a>
-->
<li>[P2680R1] — Gabriel Dos Reis,
"Contracts for C++: Prioritizing Safety", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2680r1.pdf">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2680r1.pdf"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2680r1.pdf"
title="Gabriel Dos Reis, “Contracts for C++: Prioritizing Safety”">[P2680R1]</a>
-->
<li>[P2780R0] — Ville Voutilainen,
"Caller-side precondition checking, and Eval_and_throw", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2780r0.html">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2780r0.html"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2780r0.html"
title="Ville Voutilainen, “Caller-side precondition checking, and Eval_and_throw”">[P2780R0]</a>
-->
<li>[P2795R5] — Thomas Köppe,
"Erroneous behaviour for uninitialized reads", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2795r5.html"
title="Thomas Köppe, “Erroneous behaviour for uninitialized reads”">[P2795R5]</a>
-->
<li>[P2900R9] — Joshua Berne, Timur Doumler, Andrzej Krzemieński et al.,
"Contracts for C++", <br>
(<a href="https://isocpp.org/files/papers/P2900R9.pdf">"https://isocpp.org/files/papers/P2900R9.pdf"</a>).
</li>
<!--
<a href="https://isocpp.org/files/papers/P2900R9.pdf"
title="Joshua Berne, Timur Doumler, Andrzej Krzemieński et al., “Contracts for C++”">[P2900R9]</a>
-->
<li>[P3023R1] — David Sankel,
"C++ Should Be C++", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p3023r1.html">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p3023r1.html"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p3023r1.html"
title="David Sankel, “C++ Should Be C++”">[P3023R1]</a>
-->
<li>[P3285R0] — Gabriel Dos Reis,
"Contracts: Protecting The Protector", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3285r0.pdf"
title="Gabriel Dos Reis, “Contracts: Protecting The Protector”">[P3285R0]</a>
-->
<li>[P3297R1] — Christian Eltzschig, Mathias Kraus, Ryan McDougall, Pez Zarifian,,
"C++26 Needs Contract Checking", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3297r1.pdf">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3297r1.pdf"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3297r1.pdf"
title="Christian Eltzschig, Mathias Kraus, Ryan McDougall, Pez Zarifian, “C++26 Needs Contract Checking”">[P3297R1]</a>
-->
<li>[P3362R0] — Ville Voutilainen, Richard Corden,
"Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285", <br>
(<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html">"https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"</a>).
</li>
<!--
<a href="https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3362r0.html"
title="Ville Voutilainen, Richard Corden, “Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285”">[P3362R0]</a>
-->
</ul>
</body></html>