papers/contracts-cannot-be-used-for-stdlib-hardening.html at master · villevoutilainen/papers · GitHub

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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
        "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
	<title>Standard library hardening should not use the 'observe' semantic</title>

	<style>
	p {text-align:justify}
	li {text-align:justify}
	blockquote.note
	{
		background-color:#E0E0E0;
		padding-left: 15px;
		padding-right: 15px;
		padding-top: 1px;
		padding-bottom: 1px;
	}
	ins {color:#00A000}
	del {color:#A00000}
	</style>
</head>
<body>

<address align=right>
Document number: P3878R1<br/>
Audience: LEWG, LWG<br/>
<br/>
<br/>
<a href="mailto:ville.voutilainen@gmail.com">Ville Voutilainen</a><br/>
<a href="mailto:cxx@kayari.org">Jonathan Wakely</a><br/>
<a href="mailto:jhs@edg.com">John Spicer</a><br/>
<a href="mailto:stl@exchange.microsoft.com">Stephan T. Lavavej</a><br/>
2025-11-06<br/>
</address>
<hr/>
<h1 align=center>Standard library hardening should not use the 'observe' semantic</h1>

<h2>Revision history</h2>

<p>The first revision of this paper presented information on some problems
  of using C++26 Contracts for standard library hardening. The second revision
  no longer includes most of that, we now just propose a change to ensure that
  undefined behaviour is not allowed after a hardened precondition is violated.
  </p>

<h2>Abstract</h2>

<p>
  The C++26 IS draft specifies that hardened preconditions may be,
  in a hardened implementation, evaluated with a non-terminating
  semantic. This can result in violations of hardened preconditions being undefined behaviour, rather than guaranteed to be diagnosed, which defeats the purpose of using a hardened implementation.
</p>

<h2>A hardened implementation that uses 'observe' is not hardened</h2>

<p>The specification says, in [structure.specifications]/3.5.1, with the problematic part bolded,</p>
<p><pre><blockquote>When invoking the function in a hardened implementation, prior to any other observable side
effects of the function, one or more contract assertions whose predicates are as described in the
hardened precondition are evaluated with a checking semantic (6.11.2). <b>If any of these assertions
is evaluated with a non-terminating semantic and the contract-violation handler returns, the
program has undefined behavior</b>.</blockquote></pre></p>

<p>That is completely unacceptable for a hardened implementation. A
  hardened implementation is a memory safety mechanism, and it's not
  memory-safe to run into the UB that results in calling a library
  function violating its preconditions.</p>

<p>While there are use cases for having observed hardened
  preconditions, for code that's common in the wild, doesn't actually
  run into abstract machine UB, and works fine, it doesn't make sense
  for that to be allowed by a "hardened implementation".
  Nothing prevents vendors from offering a "checked but not hardened" mode
  where the hardened preconditions are evaluated using the 'observe' semantic
  and invoking a custom violation handler. Users who want that can certainly
  still get that, if their implementation provides it. But we should not allow
  anybody to claim that such a mode is a conforming "hardened implementation".
</p>

<p>If a piece of software has requirements that it be built using a hardened
  implementation (e.g. due to contractual obligations for a customer,
  or hypothetical laws that might be applied to some regulated industries)
  then presumably there is a desire and expectation that undefined behaviour
  resulting from violating hardened preconditions will be <b>prevented</b>,
  not just observed and logged.</p>

<h2>Proposed change</h2>

<p>We propose that in a hardened implementation, the assertions should be
  evaluated using a terminating semantic. This would no longer allow the
  'observe' semantic in a hardened implementation (but checking those
  preconditions using 'observe' would still be allowed as a vendor extension
  in modes which are not called a "hardened implementation".</p>

<p>The proposed change does not guarantee that violating a hardened
  precondition in a program built with a hardened implementation will result
  in the program being be contract-terminated. If a hardened implementation
  supports replacing the contract violation handler, the program can use a
  handler that throws, which will mean the program is not terminated.
  However, this still avoids the concerns presented above, because throwing
  will prevent the rest of the standard library function from being executed
  after the precondition violation was detected. There will be no undefined
  behaviour in the body of that function.</p>

<h2>Allowing 'observe' for hardened preconditions was a mistake</h2>

<p>
  The authors of the standard library hardening proposal consider the change
  proposed in this paper to be a bug fix. They agree with the position here
  that a hardened implementation should not allow undefined behaviour after
  a violation is detected.</p>

<p>The submitters of NB comments about standard library hardening confirmed
  that this change resolves their concerns.</p>


<h2>Wording</h2>

<p>In [structure.specifications]/3.1.5, edit as follows:</p>

<p><pre><blockquote>When invoking the function in a hardened implementation, prior to any other observable side
effects of the function, <del>one or more</del> contract assertions whose predicates are as described in the
hardened precondition are evaluated with a <del>checking</del><ins>terminating</ins> semantic (6.11.2). <del>If any of these assertions
is evaluated with a non-terminating semantic and the contract-violation handler returns, the
program has undefined behavior.</del></blockquote></pre></p>

</body>

</html>