summaryrefslogtreecommitdiffstats
path: root/site/posts/ClightIntroduction.v
blob: 4bd9a522635381bde8fac15fdbbeb8d69565df22 (plain) (blame)
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
(** * 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 had been interested in CompCert for quite some times, and ultimately
    challenged myself to study Clight and its semantics. This write-up is the
    result of this challenge, written as I was progressing.

    #<div id="generate-toc"></div>#

    #<div id="history">site/posts/ClightIntroduction.v</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 high-level AST of CompCert), and to benefit
    from CompCert proofs after that.

    Installing CompCert is as easy as

<<
opam install coq-compcert
>>

    More precisely, this article uses #<code>coq-compcert.3.8</code>#.

    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 write-up 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 self-explanatory (as it is
    often the case in CompCerts 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
    state-transformation, 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 clean-up 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 lets 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 short-term, 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. Lets 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.

    We can simplify [add_op] and [res_equ], and this allows us to
    conclude. *)

  smart_inv add_op.
  smart_inv res_equ.
  reflexivity.
Qed.

(** ** Conclusion *)

(** 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. *)