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
369
370
371
|
(** Alternate semantics for the Mach intermediate language. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Mem.
Require Import Integers.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Conventions.
Require Import Mach.
(** This file defines an alternate semantics for the Mach intermediate
language, which differ from the standard semantics given in file [Mach]
as follows: the stack access instructions [Mgetstack], [Msetstack]
and [Mgetparam] are interpreted not as memory accesses, but as
accesses in a frame environment, not resident in memory. The evaluation
relations take two such frame environments as parameters and results,
one for the current function and one for its caller.
Not having the frame data in memory facilitates the proof of
the [Stacking] pass, which shows that the generated code executes
correctly with the alternate semantics. In file [Machabstr2mach],
we show an implication from this alternate semantics to
the standard semantics, thus establishing that the [Stacking] pass
generates code that behaves correctly against the standard [Mach]
semantics as well. *)
(** * Structure of abstract stack frames *)
(** A frame has the same structure as the contents of a memory block. *)
Definition frame := block_contents.
Definition empty_frame := empty_block 0 0.
Definition mem_type (ty: typ) :=
match ty with Tint => Size32 | Tfloat => Size64 end.
(** [get_slot fr ty ofs v] holds if the frame [fr] contains value [v]
with type [ty] at word offset [ofs]. *)
Inductive get_slot: frame -> typ -> Z -> val -> Prop :=
| get_slot_intro:
forall fr ty ofs v,
0 <= ofs ->
fr.(low) + ofs + 4 * typesize ty <= 0 ->
v = load_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) ->
get_slot fr ty ofs v.
Remark size_mem_type:
forall ty, size_mem (mem_type ty) = 4 * typesize ty.
Proof.
destruct ty; reflexivity.
Qed.
Remark set_slot_undef_outside:
forall fr ty ofs v,
fr.(high) = 0 ->
0 <= ofs ->
fr.(low) + ofs + 4 * typesize ty <= 0 ->
(forall x, x < fr.(low) \/ x >= fr.(high) -> fr.(contents) x = Undef) ->
(forall x, x < fr.(low) \/ x >= fr.(high) ->
store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v x = Undef).
Proof.
intros. apply store_contents_undef_outside with fr.(low) fr.(high).
rewrite <- size_mem_type in H1. omega. assumption. assumption.
Qed.
(** [set_slot fr ty ofs v fr'] holds if frame [fr'] is obtained from
frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *)
Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop :=
| set_slot_intro:
forall fr ty ofs v
(A: fr.(high) = 0)
(B: 0 <= ofs)
(C: fr.(low) + ofs + 4 * typesize ty <= 0),
set_slot fr ty ofs v
(mkblock fr.(low) fr.(high)
(store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v)
(set_slot_undef_outside fr ty ofs v A B C fr.(undef_outside))).
Definition init_frame (f: function) :=
empty_block (- f.(fn_framesize)) 0.
Section RELSEM.
Variable ge: genv.
(** Execution of one instruction has the form
[exec_instr ge f sp parent c rs fr m c' rs' fr' m'],
where [parent] is the caller's frame (read-only)
and [fr], [fr'] are the current frame, before and after execution
of one instruction. The other parameters are as in the Mach semantics. *)
Inductive exec_instr:
function -> val -> frame ->
code -> regset -> frame -> mem ->
code -> regset -> frame -> mem -> Prop :=
| exec_Mlabel:
forall f sp parent lbl c rs fr m,
exec_instr f sp parent
(Mlabel lbl :: c) rs fr m
c rs fr m
| exec_Mgetstack:
forall f sp parent ofs ty dst c rs fr m v,
get_slot fr ty (Int.signed ofs) v ->
exec_instr f sp parent
(Mgetstack ofs ty dst :: c) rs fr m
c (rs#dst <- v) fr m
| exec_Msetstack:
forall f sp parent src ofs ty c rs fr m fr',
set_slot fr ty (Int.signed ofs) (rs src) fr' ->
exec_instr f sp parent
(Msetstack src ofs ty :: c) rs fr m
c rs fr' m
| exec_Mgetparam:
forall f sp parent ofs ty dst c rs fr m v,
get_slot parent ty (Int.signed ofs) v ->
exec_instr f sp parent
(Mgetparam ofs ty dst :: c) rs fr m
c (rs#dst <- v) fr m
| exec_Mop:
forall f sp parent op args res c rs fr m v,
eval_operation ge sp op rs##args = Some v ->
exec_instr f sp parent
(Mop op args res :: c) rs fr m
c (rs#res <- v) fr m
| exec_Mload:
forall f sp parent chunk addr args dst c rs fr m a v,
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
exec_instr f sp parent
(Mload chunk addr args dst :: c) rs fr m
c (rs#dst <- v) fr m
| exec_Mstore:
forall f sp parent chunk addr args src c rs fr m m' a,
eval_addressing ge sp addr rs##args = Some a ->
Mem.storev chunk m a (rs src) = Some m' ->
exec_instr f sp parent
(Mstore chunk addr args src :: c) rs fr m
c rs fr m'
| exec_Mcall:
forall f sp parent sig ros c rs fr m f' rs' m',
find_function ge ros rs = Some f' ->
exec_function f' fr rs m rs' m' ->
exec_instr f sp parent
(Mcall sig ros :: c) rs fr m
c rs' fr m'
| exec_Mgoto:
forall f sp parent lbl c rs fr m c',
find_label lbl f.(fn_code) = Some c' ->
exec_instr f sp parent
(Mgoto lbl :: c) rs fr m
c' rs fr m
| exec_Mcond_true:
forall f sp parent cond args lbl c rs fr m c',
eval_condition cond rs##args = Some true ->
find_label lbl f.(fn_code) = Some c' ->
exec_instr f sp parent
(Mcond cond args lbl :: c) rs fr m
c' rs fr m
| exec_Mcond_false:
forall f sp parent cond args lbl c rs fr m,
eval_condition cond rs##args = Some false ->
exec_instr f sp parent
(Mcond cond args lbl :: c) rs fr m
c rs fr m
with exec_instrs:
function -> val -> frame ->
code -> regset -> frame -> mem ->
code -> regset -> frame -> mem -> Prop :=
| exec_refl:
forall f sp parent c rs fr m,
exec_instrs f sp parent c rs fr m c rs fr m
| exec_one:
forall f sp parent c rs fr m c' rs' fr' m',
exec_instr f sp parent c rs fr m c' rs' fr' m' ->
exec_instrs f sp parent c rs fr m c' rs' fr' m'
| exec_trans:
forall f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 c3 rs3 fr3 m3,
exec_instrs f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 ->
exec_instrs f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 ->
exec_instrs f sp parent c1 rs1 fr1 m1 c3 rs3 fr3 m3
with exec_function_body:
function -> frame -> val -> val ->
regset -> mem -> regset -> mem -> Prop :=
| exec_funct_body:
forall f parent link ra rs m rs' m1 m2 stk fr1 fr2 fr3 c,
Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
set_slot (init_frame f) Tint 0 link fr1 ->
set_slot fr1 Tint 4 ra fr2 ->
exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent
f.(fn_code) rs fr2 m1
(Mreturn :: c) rs' fr3 m2 ->
exec_function_body f parent link ra rs m rs' (Mem.free m2 stk)
with exec_function:
function -> frame -> regset -> mem -> regset -> mem -> Prop :=
| exec_funct:
forall f parent rs m rs' m',
(forall link ra,
Val.has_type link Tint ->
Val.has_type ra Tint ->
exec_function_body f parent link ra rs m rs' m') ->
exec_function f parent rs m rs' m'.
Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop
with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop
with exec_function_body_ind4 := Minimality for exec_function_body Sort Prop
with exec_function_ind4 := Minimality for exec_function Sort Prop.
(** Ugly mutual induction principle over evaluation derivations.
Coq is not able to generate it directly, even though it is
an immediate consequence of the 4 induction principles generated
by the [Scheme] command above. *)
Lemma exec_mutual_induction:
forall (P
P0 : function ->
val ->
frame ->
code ->
regset ->
frame -> mem -> code -> regset -> frame -> mem -> Prop)
(P1 : function ->
frame -> val -> val -> regset -> mem -> regset -> mem -> Prop)
(P2 : function -> frame -> regset -> mem -> regset -> mem -> Prop),
(forall (f : function) (sp : val) (parent : frame) (lbl : label)
(c : list instruction) (rs : regset) (fr : frame) (m : mem),
P f sp parent (Mlabel lbl :: c) rs fr m c rs fr m) ->
(forall (f : function) (sp : val) (parent : frame) (ofs : int)
(ty : typ) (dst : mreg) (c : list instruction) (rs : regset)
(fr : frame) (m : mem) (v : val),
get_slot fr ty (Int.signed ofs) v ->
P f sp parent (Mgetstack ofs ty dst :: c) rs fr m c rs # dst <- v fr
m) ->
(forall (f : function) (sp : val) (parent : frame) (src : mreg)
(ofs : int) (ty : typ) (c : list instruction) (rs : mreg -> val)
(fr : frame) (m : mem) (fr' : frame),
set_slot fr ty (Int.signed ofs) (rs src) fr' ->
P f sp parent (Msetstack src ofs ty :: c) rs fr m c rs fr' m) ->
(forall (f : function) (sp : val) (parent : frame) (ofs : int)
(ty : typ) (dst : mreg) (c : list instruction) (rs : regset)
(fr : frame) (m : mem) (v : val),
get_slot parent ty (Int.signed ofs) v ->
P f sp parent (Mgetparam ofs ty dst :: c) rs fr m c rs # dst <- v fr
m) ->
(forall (f : function) (sp : val) (parent : frame) (op : operation)
(args : list mreg) (res : mreg) (c : list instruction)
(rs : mreg -> val) (fr : frame) (m : mem) (v : val),
eval_operation ge sp op rs ## args = Some v ->
P f sp parent (Mop op args res :: c) rs fr m c rs # res <- v fr m) ->
(forall (f : function) (sp : val) (parent : frame)
(chunk : memory_chunk) (addr : addressing) (args : list mreg)
(dst : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame)
(m : mem) (a v : val),
eval_addressing ge sp addr rs ## args = Some a ->
loadv chunk m a = Some v ->
P f sp parent (Mload chunk addr args dst :: c) rs fr m c
rs # dst <- v fr m) ->
(forall (f : function) (sp : val) (parent : frame)
(chunk : memory_chunk) (addr : addressing) (args : list mreg)
(src : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame)
(m m' : mem) (a : val),
eval_addressing ge sp addr rs ## args = Some a ->
storev chunk m a (rs src) = Some m' ->
P f sp parent (Mstore chunk addr args src :: c) rs fr m c rs fr m') ->
(forall (f : function) (sp : val) (parent : frame) (sig : signature)
(ros : mreg + ident) (c : list instruction) (rs : regset)
(fr : frame) (m : mem) (f' : function) (rs' : regset) (m' : mem),
find_function ge ros rs = Some f' ->
exec_function f' fr rs m rs' m' ->
P2 f' fr rs m rs' m' ->
P f sp parent (Mcall sig ros :: c) rs fr m c rs' fr m') ->
(forall (f : function) (sp : val) (parent : frame) (lbl : label)
(c : list instruction) (rs : regset) (fr : frame) (m : mem)
(c' : code),
find_label lbl (fn_code f) = Some c' ->
P f sp parent (Mgoto lbl :: c) rs fr m c' rs fr m) ->
(forall (f : function) (sp : val) (parent : frame)
(cond : condition) (args : list mreg) (lbl : label)
(c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem)
(c' : code),
eval_condition cond rs ## args = Some true ->
find_label lbl (fn_code f) = Some c' ->
P f sp parent (Mcond cond args lbl :: c) rs fr m c' rs fr m) ->
(forall (f : function) (sp : val) (parent : frame)
(cond : condition) (args : list mreg) (lbl : label)
(c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem),
eval_condition cond rs ## args = Some false ->
P f sp parent (Mcond cond args lbl :: c) rs fr m c rs fr m) ->
(forall (f : function) (sp : val) (parent : frame) (c : code)
(rs : regset) (fr : frame) (m : mem),
P0 f sp parent c rs fr m c rs fr m) ->
(forall (f : function) (sp : val) (parent : frame) (c : code)
(rs : regset) (fr : frame) (m : mem) (c' : code) (rs' : regset)
(fr' : frame) (m' : mem),
exec_instr f sp parent c rs fr m c' rs' fr' m' ->
P f sp parent c rs fr m c' rs' fr' m' ->
P0 f sp parent c rs fr m c' rs' fr' m') ->
(forall (f : function) (sp : val) (parent : frame) (c1 : code)
(rs1 : regset) (fr1 : frame) (m1 : mem) (c2 : code) (rs2 : regset)
(fr2 : frame) (m2 : mem) (c3 : code) (rs3 : regset) (fr3 : frame)
(m3 : mem),
exec_instrs f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 ->
P0 f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 ->
exec_instrs f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 ->
P0 f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 ->
P0 f sp parent c1 rs1 fr1 m1 c3 rs3 fr3 m3) ->
(forall (f : function) (parent : frame) (link ra : val) (rs : regset)
(m : mem) (rs' : regset) (m1 m2 : mem) (stk : block)
(fr1 fr2 fr3 : frame) (c : list instruction),
alloc m 0 (fn_stacksize f) = (m1, stk) ->
set_slot (init_frame f) Tint 0 link fr1 ->
set_slot fr1 Tint 4 ra fr2 ->
exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3
m2 ->
P0 f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3 m2 ->
P1 f parent link ra rs m rs' (free m2 stk)) ->
(forall (f : function) (parent : frame) (rs : regset) (m : mem)
(rs' : regset) (m' : mem),
(forall link ra : val,
Val.has_type link Tint ->
Val.has_type ra Tint ->
exec_function_body f parent link ra rs m rs' m') ->
(forall link ra : val,
Val.has_type link Tint ->
Val.has_type ra Tint -> P1 f parent link ra rs m rs' m') ->
P2 f parent rs m rs' m') ->
(forall (f15 : function) (sp : val) (f16 : frame) (c : code)
(r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset)
(f18 : frame) (m0 : mem),
exec_instr f15 sp f16 c r f17 m c0 r0 f18 m0 ->
P f15 sp f16 c r f17 m c0 r0 f18 m0)
/\ (forall (f15 : function) (sp : val) (f16 : frame) (c : code)
(r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset)
(f18 : frame) (m0 : mem),
exec_instrs f15 sp f16 c r f17 m c0 r0 f18 m0 ->
P0 f15 sp f16 c r f17 m c0 r0 f18 m0)
/\ (forall (f15 : function) (f16 : frame) (v1 v2 : val) (r : regset) (m : mem)
(r0 : regset) (m0 : mem),
exec_function_body f15 f16 v1 v2 r m r0 m0 -> P1 f15 f16 v1 v2 r m r0 m0)
/\ (forall (f15 : function) (f16 : frame) (r : regset) (m : mem)
(r0 : regset) (m0 : mem),
exec_function f15 f16 r m r0 m0 -> P2 f15 f16 r m r0 m0).
Proof.
intros. split. apply (exec_instr_ind4 P P0 P1 P2); assumption.
split. apply (exec_instrs_ind4 P P0 P1 P2); assumption.
split. apply (exec_function_body_ind4 P P0 P1 P2); assumption.
apply (exec_function_ind4 P P0 P1 P2); assumption.
Qed.
End RELSEM.
Definition exec_program (p: program) (r: val) : Prop :=
let ge := Genv.globalenv p in
let m0 := Genv.init_mem p in
exists b, exists f, exists rs, exists m,
Genv.find_symbol ge p.(prog_main) = Some b /\
Genv.find_funct_ptr ge b = Some f /\
f.(fn_sig) = mksignature nil (Some Tint) /\
exec_function ge f empty_frame (Regmap.init Vundef) m0 rs m /\
rs (Conventions.loc_result f.(fn_sig)) = r.
|
