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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Abstract syntax for the Compcert C language *)
Require Import Coqlib Maps Integers Floats Errors.
Require Import AST Linking Values.
Require Import Ctypes Cop.
(** ** Expressions *)
(** Compcert C expressions are almost identical to those of C.
The only omission is string literals. Some operators are treated
as derived forms: array indexing, pre-increment, pre-decrement, and
the [&&] and [||] operators. All expressions are annotated with
their types. *)
Inductive expr : Type :=
| Eval (v: val) (ty: type) (**r constant *)
| Evar (x: ident) (ty: type) (**r variable *)
| Efield (l: expr) (f: ident) (ty: type)
(**r access to a member of a struct or union *)
| Evalof (l: expr) (ty: type) (**r l-value used as a r-value *)
| Ederef (r: expr) (ty: type) (**r pointer dereference (unary [*]) *)
| Eaddrof (l: expr) (ty: type) (**r address-of operators ([&]) *)
| Eunop (op: unary_operation) (r: expr) (ty: type)
(**r unary arithmetic operation *)
| Ebinop (op: binary_operation) (r1 r2: expr) (ty: type)
(**r binary arithmetic operation *)
| Ecast (r: expr) (ty: type) (**r type cast [(ty)r] *)
| Eseqand (r1 r2: expr) (ty: type) (**r sequential "and" [r1 && r2] *)
| Eseqor (r1 r2: expr) (ty: type) (**r sequential "or" [r1 || r2] *)
| Econdition (r1 r2 r3: expr) (ty: type) (**r conditional [r1 ? r2 : r3] *)
| Esizeof (ty': type) (ty: type) (**r size of a type *)
| Ealignof (ty': type) (ty: type) (**r natural alignment of a type *)
| Eassign (l: expr) (r: expr) (ty: type) (**r assignment [l = r] *)
| Eassignop (op: binary_operation) (l: expr) (r: expr) (tyres ty: type)
(**r assignment with arithmetic [l op= r] *)
| Epostincr (id: incr_or_decr) (l: expr) (ty: type)
(**r post-increment [l++] and post-decrement [l--] *)
| Ecomma (r1 r2: expr) (ty: type) (**r sequence expression [r1, r2] *)
| Ecall (r1: expr) (rargs: exprlist) (ty: type)
(**r function call [r1(rargs)] *)
| Ebuiltin (ef: external_function) (tyargs: typelist) (rargs: exprlist) (ty: type)
(**r builtin function call *)
| Eloc (b: block) (ofs: ptrofs) (bf: bitfield) (ty: type)
(**r memory location, result of evaluating a l-value *)
| Eparen (r: expr) (tycast: type) (ty: type) (**r marked subexpression *)
with exprlist : Type :=
| Enil
| Econs (r1: expr) (rl: exprlist).
(** Expressions are implicitly classified into l-values and r-values,
ranged over by [l] and [r], respectively, in the grammar above.
L-values are those expressions that can occur to the left of an assignment.
They denote memory locations. (Indeed, the reduction semantics for
expression reduces them to [Eloc b ofs] expressions.) L-values are
variables ([Evar]), pointer dereferences ([Ederef]), field accesses ([Efield]).
R-values are all other expressions. They denote values, and the reduction
semantics reduces them to [Eval v] expressions.
A l-value can be used in a r-value context, but this use must be marked
explicitly with the [Evalof] operator, which is not materialized in the
concrete syntax of C but denotes a read from the location corresponding to
the l-value [l] argument of [Evalof l].
The grammar above contains some forms that cannot appear in source terms
but appear during reduction. These forms are:
- [Eval v] where [v] is a pointer or [Vundef]. ([Eval] of an integer or
float value can occur in a source term and represents a numeric literal.)
- [Eloc b ofs], which appears during reduction of l-values.
- [Eparen r tycast ty], which appears during reduction of conditionals
[r1 ? r2 : r3] as well as sequential `and' / `or'.
Some C expressions are derived forms. Array access [r1[r2]] is expressed
as [*(r1 + r2)].
*)
Definition Eindex (r1 r2: expr) (ty: type) :=
Ederef (Ebinop Oadd r1 r2 (Tpointer ty noattr)) ty.
(** Pre-increment [++l] and pre-decrement [--l] are expressed as
[l += 1] and [l -= 1], respectively. *)
Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
Eassignop (match id with Incr => Oadd | Decr => Osub end)
l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty.
(** Selection is a conditional expression that always evaluates both arms
and can be implemented by "conditional move" instructions.
It is expressed as an invocation of a builtin function. *)
Definition Eselection (r1 r2 r3: expr) (ty: type) :=
let t := typ_of_type ty in
let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
Ebuiltin (EF_builtin "__builtin_sel"%string sg)
(Tcons type_bool (Tcons ty (Tcons ty Tnil)))
(Econs r1 (Econs r2 (Econs r3 Enil)))
ty.
(** Extract the type part of a type-annotated expression. *)
Definition typeof (a: expr) : type :=
match a with
| Eloc _ _ _ ty => ty
| Evar _ ty => ty
| Ederef _ ty => ty
| Efield _ _ ty => ty
| Eval _ ty => ty
| Evalof _ ty => ty
| Eaddrof _ ty => ty
| Eunop _ _ ty => ty
| Ebinop _ _ _ ty => ty
| Ecast _ ty => ty
| Econdition _ _ _ ty => ty
| Eseqand _ _ ty => ty
| Eseqor _ _ ty => ty
| Esizeof _ ty => ty
| Ealignof _ ty => ty
| Eassign _ _ ty => ty
| Eassignop _ _ _ _ ty => ty
| Epostincr _ _ ty => ty
| Ecomma _ _ ty => ty
| Ecall _ _ ty => ty
| Ebuiltin _ _ _ ty => ty
| Eparen _ _ ty => ty
end.
(** ** Statements *)
(** Compcert C statements are very much like those of C and include:
- empty statement [Sskip]
- evaluation of an expression for its side-effects [Sdo r]
- conditional [if (...) { ... } else { ... }]
- the three loops [while(...) { ... }] and [do { ... } while (...)]
and [for(..., ..., ...) { ... }]
- the [switch] construct
- [break], [continue], [return] (with and without argument)
- [goto] and labeled statements.
Only structured forms of [switch] are supported; moreover,
the [default] case must occur last. Blocks and block-scoped declarations
are not supported. *)
Definition label := ident.
Inductive statement : Type :=
| Sskip : statement (**r do nothing *)
| Sdo : expr -> statement (**r evaluate expression for side effects *)
| Ssequence : statement -> statement -> statement (**r sequence *)
| Sifthenelse : expr -> statement -> statement -> statement (**r conditional *)
| Swhile : expr -> statement -> statement (**r [while] loop *)
| Sdowhile : expr -> statement -> statement (**r [do] loop *)
| Sfor: statement -> expr -> statement -> statement -> statement (**r [for] loop *)
| Sbreak : statement (**r [break] statement *)
| Scontinue : statement (**r [continue] statement *)
| Sreturn : option expr -> statement (**r [return] statement *)
| Sswitch : expr -> labeled_statements -> statement (**r [switch] statement *)
| Slabel : label -> statement -> statement
| Sgoto : label -> statement
with labeled_statements : Type := (**r cases of a [switch] *)
| LSnil: labeled_statements
| LScons: option Z -> statement -> labeled_statements -> labeled_statements.
(**r [None] is [default], [Some x] is [case x] *)
(** ** Functions *)
(** A function definition is composed of its return type ([fn_return]),
the names and types of its parameters ([fn_params]), the names
and types of its local variables ([fn_vars]), and the body of the
function (a statement, [fn_body]). *)
Record function : Type := mkfunction {
fn_return: type;
fn_callconv: calling_convention;
fn_params: list (ident * type);
fn_vars: list (ident * type);
fn_body: statement
}.
Definition var_names (vars: list(ident * type)) : list ident :=
List.map (@fst ident type) vars.
(** Functions can either be defined ([Internal]) or declared as
external functions ([External]). *)
Definition fundef := Ctypes.fundef function.
(** The type of a function definition. *)
Definition type_of_function (f: function) : type :=
Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
Definition type_of_fundef (f: fundef) : type :=
match f with
| Internal fd => type_of_function fd
| External id args res cc => Tfunction args res cc
end.
(** ** Programs and compilation units *)
(** As defined in module [Ctypes], a program, or compilation unit, is
composed of:
- a list of definitions of functions and global variables;
- the names of functions and global variables that are public (not static);
- the name of the function that acts as entry point ("main" function).
- a list of definitions for structure and union names
- the corresponding composite environment
- a proof that this environment is consistent with the definitions. *)
Definition program := Ctypes.program function.
|
