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

(** * A Study of Clight and its Semantics *)
(* begin hide *)
From Coq Require Import List.
Import ListNotations.
(* end hide *)
(** CompCert is a certified C compiler which comes with a proof of semantics
preservation. What this means is the following: the semantics of the C code
you write is preserved by CompCert compilation passes up to the generated
machine code.
I have been interested in CompCert for quite some times now. Today (#<span
id="time">#March 18, 2020#</span>#), I have challenged myself to study
Clight and its semantics. This writeup is the result of this challenge,
written as I was progressing.
#<div id="generatetoc"></div># *)
(** ** Installing CompCert *)
(** CompCert has been added to <<opam>>, and as a consequence can be very easily
used as a library for other Coq developments. A typical use case is for a
project to produce Clight (the highlevel AST of CompCert), and to benefit
from CompCert proofs after that.
Installing CompCert is as easy as
<<
opam install compcert
>>
Once <<opam>> terminates, the <<compcert>> namespace becomes available. In
addition, several binaries are now available if you have correctly set your
<<PATH>> environment variable. For instance, <<clightgen>> takes a C file as
an argument, and generates a Coq file which contains the Clight generated by
CompCert. *)
(** ** Problem Statement *)
(** Our goal for this first writeup is to prove that the C function
<<
int add (int x, int y) {
return x + y;
}
>>
returns the expected result, that is <<x + y>>. The <<clightgen>> tool
generates (among other things) the following AST (note: I have modified it
in order to improve its readability). *)
From compcert Require Import Clight Ctypes Clightdefs AST
Coqlib Cop.
Definition _x : ident := 1%positive.
Definition _y : ident := 2%positive.
Definition f_add : function :=
{ fn_return := tint
; fn_callconv := cc_default
; fn_params := [(_x, tint); (_y, tint)]
; fn_vars := []
; fn_temps := []
; fn_body := Sreturn
(Some (Ebinop Oadd
(Etempvar _x tint)
(Etempvar _y tint)
tint))
}.
(** The fields of the [function] type are pretty selfexplanatory (as it is
often the case in CompCert’s ASTs as far as I can tell for now).
Identifiers in Clight are ([positive]) indices. The [fn_body] field is of
type [statement], with the particular constructor [Sreturn] whose argument
is of type [option expr], and [statement] and [expr] look like the two main
types to study. The predicates [step1] and [step2] allow for reasoning
about the execution of a [function], step by step (hence the name). It
appears that <<clightgen>> generates Clight terms using the function call
convention encoded by [step2]. To reason about a complete execution, it
appears that we can use [star] (from the [Smallstep] module) which is
basically a trace of [step]. These semantics are defined as predicates (that
is, they live in [Prop]). They allow for reasoning about
statetransformation, where a state is either
 A function call, with a given list of arguments and a continuation
 A function return, with a result and a continuation
 A [statement] execution within a [function]
We import several CompCert modules to manipulate _values_ (in our case,
bounded integers). *)
From compcert Require Import Values Integers.
Import Int.
(** Putting everything together, the lemma we want to prove about [f_add] is
the following. *)
Lemma f_add_spec (env : genv)
(t : Events.trace)
(m m' : Memory.Mem.mem)
(v : val) (x y z : int)
(trace : Smallstep.star step2 env
(Callstate (Ctypes.Internal f_add)
[Vint x; Vint y]
Kstop
m)
t
(Returnstate (Vint z) Kstop m'))
: z = add x y.
(** ** Proof Walkthrough *)
(** We introduce a custom [inversion] tactic which does some cleanup in
addition to just perform the inversion. *)
Ltac smart_inv H :=
inversion H; subst; cbn in *; clear H.
(** We can now try to prove our lemma. *)
Proof.
(** We first destruct [trace], and we rename the generated hypothesis in order
to improve the readability of these notes. *)
smart_inv trace.
rename H into Hstep.
rename H0 into Hstar.
(** This generates two hypotheses.
<<
Hstep : step1
env
(Callstate (Ctypes.Internal f_add)
[Vint x; Vint y]
Kstop
m)
t1
s2
Hstar : Smallstep.star
step2
env
s2
t2
(Returnstate (Vint z) Kstop m')
>>
In other words, to “go” from a [Callstate] of [f_add] to a [Returnstate],
there is a first step from a [Callstate] to a state [s2], then a succession
of steps to go from [s2] to a [Returnstate].
We consider the single [step], in order to determine the actual value of
[s2] (among other things). To do that, we use [smart_inv] on [Hstep], and
again perform some renaming. *)
smart_inv Hstep.
rename le into tmp_env.
rename e into c_env.
rename H5 into f_entry.
(** This produces two effects. First, a new hypothesis is added to the context.
<<
f_entry : function_entry1
env
f_add
[Vint x; Vint y]
m
c_env
tmp_env
m1
>>
Then, the [Hstar] hypothesis has been updated, because we now have a more
precise value of [s2]. More precisely, [s2] has become
<<
State
f_add
(Sreturn
(Some (Ebinop Oadd
(Etempvar _x tint)
(Etempvar _y tint)
tint)))
Kstop
c_env
tmp_env
m1
>>
Using the same approach as before, we can uncover the next step. *)
smart_inv Hstar.
rename H into Hstep.
rename H0 into Hstar.
(** The resulting hypotheses are
<<
Hstep : step2 env
(State
f_add
(Sreturn
(Some
(Ebinop Oadd
(Etempvar _x tint)
(Etempvar _y tint)
tint)))
Kstop c_env tmp_env m1) t1 s2
Hstar : Smallstep.star
step2
env
s2
t0
(Returnstate (Vint z) Kstop m')
>>
An inversion of [Hstep] can be used to learn more about its resulting
state… So let’s do just that. *)
smart_inv Hstep.
rename H7 into ev.
rename v0 into res.
rename H8 into res_equ.
rename H9 into mem_equ.
(** The generated hypotheses have become
<<
res : val
ev : eval_expr env c_env tmp_env m1
(Ebinop Oadd
(Etempvar _x tint)
(Etempvar _y tint)
tint)
res
res_equ : sem_cast res tint tint m1 = Some v'
mem_equ : Memory.Mem.free_list m1
(blocks_of_env env c_env)
= Some m'0
>>
Our understanding of these hypotheses is the following
 The expression [_x + _y] is evaluated using the [c_env] environment (and
we know thanks to [binding] the value of [_x] and [_y]), and its result
is stored in [res]
 [res] is cast into a [tint] value, and acts as the result of [f_add]
The [Hstar] hypothesis is now interesting
<<
Hstar : Smallstep.star
step2 env
(Returnstate v' Kstop m'0) t0
(Returnstate (Vint z) Kstop m')
>>
It is clear that we are at the end of the execution of [f_add] (even if Coq
generates two subgoals, the second one is not relevant and easy to
discard). *)
smart_inv Hstar; [ smart_inv H ].
(** We are making good progress here, and we can focus our attention on the [ev]
hypothesis, which concerns the evaluation of the [_x + _y] expression. We
can simplify it a bit further. *)
smart_inv ev; [ smart_inv H].
rename H4 into fetch_x.
rename H5 into fetch_y.
rename H6 into add_op.
(** In a shortterm, the hypotheses [fetch_x] and [fetch_y] are the most
important.
<<
fetch_x : eval_expr env c_env tmp_env m1 (Etempvar _x tint) v1
fetch_y : eval_expr env c_env tmp_env m1 (Etempvar _y tint) v2
>>
The current challenge we face is to prove that we know their value. At this
point, we can have a look at [f_entry]. This is starting to look familiar:
[smart_inv], then renaming, etc. *)
smart_inv f_entry.
clear H.
clear H0.
clear H1.
smart_inv H3; subst.
rename H2 into allocs.
(** We are almost done. Let’s simplify as much as possible [fetch_x] and
[fetch_y]. Each time, the [smart_inv] tactic generates two suboals, but only
the first one is relevant. The second one is not, and can be discarded. *)
smart_inv fetch_x; [ inversion H].
smart_inv H2.
smart_inv fetch_y; [ inversion H].
smart_inv H2.
(** We now know the values of the operands of [add]. The two relevant hypotheses
that we need to consider next are [add_op] and [res_equ]. They are easy to
read.
<<
add_op : sem_binarith
(fun (_ : signedness) (n1 n2 : Integers.int)
=> Some (Vint (add n1 n2)))
(fun (_ : signedness) (n1 n2 : int64)
=> Some (Vlong (Int64.add n1 n2)))
(fun n1 n2 : Floats.float
=> Some (Vfloat (Floats.Float.add n1 n2)))
(fun n1 n2 : Floats.float32
=> Some (Vsingle (Floats.Float32.add n1 n2)))
v1 tint v2 tint m1 = Some res
>>
 [add_op] is the addition of [Vint x] and [Vint y], and its result is
[res].
<<
res_equ : sem_cast res tint tint m1 = Some (Vint z)
>>
 [res_equ] is the equation which says that the result of [f_add] is
[res], after it has been cast as a [tint] value
Surprisingly, neither [add_op] nor [res_equ] can be reduced easily… After
some digging, I have found that this is because both rely on [Archi.ptr64],
which is basically opaque as far as reduction strategies are concerned.
Now, there are probably more elegant (idiomatic) way to deal with this
issue, but a working approach is to unfold until [Archi.ptr64] appears, then
use the [Archi.splitlong_ptr32] lemma to replace it with its value
([false]). *)
unfold sem_binarith in *.
cbn in *.
unfold sem_cast in *.
cbn in *.
rewrite Archi.splitlong_ptr32 in *; auto.
(** We can now simplify [add_op] and [res_equ], and this allows us to
conclude. *)
smart_inv add_op.
smart_inv res_equ.
reflexivity.
Qed.
(** ** Conclusion *)
(** The main difficulty of this exercise was the opaqueness of [Archi.ptr64];
this is surprising, since it means my struggle was technical, not
conceptual. On the contrary, the definitions of Clight are easy to
understand, and the #<a
href="http://compcert.inria.fr/doc/index.html">#CompCert documentation#</a>#
is very pleasant to read.
Understanding Clight and its semantics can be very interesting if you are
working on a language that you want to translate into machine code. However,
proving functional properties of a given C snippet using only CompCert can
quickly become cumbersome. From this perspective, the #<a
href="https://github.com/PrincetonUniversity/VST">#VST#</a># project is very
interesting, as its main purpose is to provide tools to reason about Clight
programs more easily. *)
