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
|
(* *********************************************************************)
(* *)
(* 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 INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Compile-time evaluation of initializers for global C variables. *)
Require Import Coqlib Maps Errors.
Require Import Integers Floats Values AST Memory Globalenvs.
Require Import Ctypes Cop Csyntax.
Open Scope error_monad_scope.
(** * Evaluation of compile-time constant expressions *)
(** To evaluate constant expressions at compile-time, we use the same [value]
type and the same [sem_*] functions that are used in CompCert C's semantics
(module [Csem]). However, we interpret pointer values symbolically:
[Vptr id ofs] represents the address of global variable [id]
plus byte offset [ofs]. *)
(** [constval a] evaluates the constant expression [a].
If [a] is a r-value, the returned value denotes:
- [Vint n], [Vlong n], [Vfloat f], [Vsingle f]: the corresponding number
- [Vptr id ofs]: address of global variable [id] plus byte offset [ofs]
- [Vundef]: erroneous expression
If [a] is a l-value, the returned value denotes:
- [Vptr id ofs]: global variable [id] plus byte offset [ofs]
*)
Definition do_cast (v: val) (t1 t2: type) : res val :=
match sem_cast v t1 t2 Mem.empty with
| Some v' => OK v'
| None => Error(msg "undefined cast")
end.
Definition lookup_composite (ce: composite_env) (id: ident) : res composite :=
match ce!id with
| Some co => OK co
| None => Error (MSG "Undefined struct or union " :: CTX id :: nil)
end.
Fixpoint constval (ce: composite_env) (a: expr) : res val :=
match a with
| Eval v ty =>
match v with
| Vint _ | Vfloat _ | Vsingle _ | Vlong _ => OK v
| Vptr _ _ | Vundef => Error(msg "illegal constant")
end
| Evalof l ty =>
match access_mode ty with
| By_reference | By_copy => constval ce l
| _ => Error(msg "dereferencing of an l-value")
end
| Eaddrof l ty =>
constval ce l
| Eunop op r1 ty =>
do v1 <- constval ce r1;
match sem_unary_operation op v1 (typeof r1) Mem.empty with
| Some v => OK v
| None => Error(msg "undefined unary operation")
end
| Ebinop op r1 r2 ty =>
do v1 <- constval ce r1;
do v2 <- constval ce r2;
match sem_binary_operation ce op v1 (typeof r1) v2 (typeof r2) Mem.empty with
| Some v => OK v
| None => Error(msg "undefined binary operation")
end
| Ecast r ty =>
do v1 <- constval ce r; do_cast v1 (typeof r) ty
| Esizeof ty1 ty =>
OK (Vptrofs (Ptrofs.repr (sizeof ce ty1)))
| Ealignof ty1 ty =>
OK (Vptrofs (Ptrofs.repr (alignof ce ty1)))
| Eseqand r1 r2 ty =>
do v1 <- constval ce r1;
do v2 <- constval ce r2;
match bool_val v1 (typeof r1) Mem.empty with
| Some true => do_cast v2 (typeof r2) type_bool
| Some false => OK (Vint Int.zero)
| None => Error(msg "undefined && operation")
end
| Eseqor r1 r2 ty =>
do v1 <- constval ce r1;
do v2 <- constval ce r2;
match bool_val v1 (typeof r1) Mem.empty with
| Some false => do_cast v2 (typeof r2) type_bool
| Some true => OK (Vint Int.one)
| None => Error(msg "undefined || operation")
end
| Econdition r1 r2 r3 ty =>
do v1 <- constval ce r1;
do v2 <- constval ce r2;
do v3 <- constval ce r3;
match bool_val v1 (typeof r1) Mem.empty with
| Some true => do_cast v2 (typeof r2) ty
| Some false => do_cast v3 (typeof r3) ty
| None => Error(msg "condition is undefined")
end
| Ecomma r1 r2 ty =>
do v1 <- constval ce r1; constval ce r2
| Evar x ty =>
OK(Vptr x Ptrofs.zero)
| Ederef r ty =>
constval ce r
| Efield l f ty =>
match typeof l with
| Tstruct id _ =>
do co <- lookup_composite ce id;
do delta <- field_offset ce f (co_members co);
do v <- constval ce l;
OK (if Archi.ptr64
then Val.addl v (Vlong (Int64.repr delta))
else Val.add v (Vint (Int.repr delta)))
| Tunion id _ =>
constval ce l
| _ =>
Error(msg "ill-typed field access")
end
| Eparen r tycast ty =>
do v <- constval ce r; do_cast v (typeof r) tycast
| _ =>
Error(msg "not a compile-time constant")
end.
(** [constval_cast ce a ty] evaluates [a] then converts its value to type [ty]. *)
Definition constval_cast (ce: composite_env) (a: expr) (ty: type): res val :=
do v <- constval ce a; do_cast v (typeof a) ty.
(** * Translation of initializers *)
Inductive initializer :=
| Init_single (a: expr)
| Init_array (il: initializer_list)
| Init_struct (il: initializer_list)
| Init_union (f: ident) (i: initializer)
with initializer_list :=
| Init_nil
| Init_cons (i: initializer) (il: initializer_list).
(** Translate an initializing expression [a] for a scalar variable
of type [ty]. Return the corresponding initialization datum. *)
Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data :=
do v <- constval_cast ce a ty;
match v, ty with
| Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n)
| Vint n, Tint I16 sg _ => OK(Init_int16 n)
| Vint n, Tint I32 sg _ => OK(Init_int32 n)
| Vint n, Tpointer _ _ => assertion (negb Archi.ptr64); OK(Init_int32 n)
| Vlong n, Tlong _ _ => OK(Init_int64 n)
| Vlong n, Tpointer _ _ => assertion (Archi.ptr64); OK(Init_int64 n)
| Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
| Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
| Vptr id ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); OK(Init_addrof id ofs)
| Vptr id ofs, Tlong _ _ => assertion (Archi.ptr64); OK(Init_addrof id ofs)
| Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
| Vundef, _ => Error(msg "undefined operation in initializer")
| _, _ => Error (msg "type mismatch in initializer")
end.
(** Translate an initializer [i] for a variable of type [ty].
[transl_init ce ty i] returns the appropriate list of initialization data.
The intermediate functions [transl_init_rec], [transl_init_array]
and [transl_init_struct] append initialization data to the given
list [k], and build the list of initialization data in reverse order,
so as to remain tail-recursive. *)
Definition padding (frm to: Z) (k: list init_data) : list init_data :=
if zlt frm to then Init_space (to - frm) :: k else k.
Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer)
(k: list init_data) {struct i} : res (list init_data) :=
match i, ty with
| Init_single a, _ =>
do d <- transl_init_single ce ty a; OK (d :: k)
| Init_array il, Tarray tyelt nelt _ =>
transl_init_array ce tyelt il (Z.max 0 nelt) k
| Init_struct il, Tstruct id _ =>
do co <- lookup_composite ce id;
match co_su co with
| Struct => transl_init_struct ce ty (co_members co) il 0 k
| Union => Error (MSG "struct/union mismatch on " :: CTX id :: nil)
end
| Init_union f i1, Tunion id _ =>
do co <- lookup_composite ce id;
match co_su co with
| Struct => Error (MSG "union/struct mismatch on " :: CTX id :: nil)
| Union =>
do ty1 <- field_type f (co_members co);
do k1 <- transl_init_rec ce ty1 i1 k;
OK (padding (sizeof ce ty1) (sizeof ce ty) k1)
end
| _, _ =>
Error (msg "wrong type for compound initializer")
end
with transl_init_array (ce: composite_env) (ty: type) (il: initializer_list) (sz: Z)
(k: list init_data) {struct il} : res (list init_data) :=
match il with
| Init_nil =>
if zeq sz 0 then OK k
else if zle 0 sz then OK (Init_space (sz * sizeof ce ty) :: k)
else Error (msg "wrong number of elements in array initializer")
| Init_cons i1 il' =>
do k1 <- transl_init_rec ce ty i1 k;
transl_init_array ce ty il' (sz - 1) k1
end
with transl_init_struct (ce: composite_env) (ty: type)
(fl: members) (il: initializer_list) (pos: Z)
(k: list init_data)
{struct il} : res (list init_data) :=
match il, fl with
| Init_nil, nil =>
OK (padding pos (sizeof ce ty) k)
| Init_cons i1 il', (_, ty1) :: fl' =>
let pos1 := align pos (alignof ce ty1) in
do k1 <- transl_init_rec ce ty1 i1 (padding pos pos1 k);
transl_init_struct ce ty fl' il' (pos1 + sizeof ce ty1) k1
| _, _ =>
Error (msg "wrong number of elements in struct initializer")
end.
Definition transl_init (ce: composite_env) (ty: type) (i: initializer)
: res (list init_data) :=
do k <- transl_init_rec ce ty i nil; OK (List.rev' k).
|
