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
|
(** The Mach intermediate language: abstract syntax and semantics.
Mach is the last intermediate language before generation of assembly
code.
*)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
(** * Abstract syntax *)
(** Like Linear, the Mach language is organized as lists of instructions
operating over machine registers, with default fall-through behaviour
and explicit labels and branch instructions.
The main difference with Linear lies in the instructions used to
access the activation record. Mach has three such instructions:
[Mgetstack] and [Msetstack] to read and write within the activation
record for the current function, at a given word offset and with a
given type; and [Mgetparam], to read within the activation record of
the caller.
These instructions implement a more concrete view of the activation
record than the the [Bgetstack] and [Bsetstack] instructions of
Linear: actual offsets are used instead of abstract stack slots; the
distinction between the caller's frame and the callee's frame is
made explicit. *)
Definition label := positive.
Inductive instruction: Set :=
| Mgetstack: int -> typ -> mreg -> instruction
| Msetstack: mreg -> int -> typ -> instruction
| Mgetparam: int -> typ -> mreg -> instruction
| Mop: operation -> list mreg -> mreg -> instruction
| Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction
| Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
| Mcall: signature -> mreg + ident -> instruction
| Mlabel: label -> instruction
| Mgoto: label -> instruction
| Mcond: condition -> list mreg -> label -> instruction
| Mreturn: instruction.
Definition code := list instruction.
Record function: Set := mkfunction
{ fn_sig: signature;
fn_code: code;
fn_stacksize: Z;
fn_framesize: Z }.
Definition program := AST.program function.
Definition genv := Genv.t function.
(** * Dynamic semantics *)
Module RegEq.
Definition t := mreg.
Definition eq := mreg_eq.
End RegEq.
Module Regmap := EMap(RegEq).
Definition regset := Regmap.t val.
Notation "a ## b" := (List.map a b) (at level 1).
Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).
Definition is_label (lbl: label) (instr: instruction) : bool :=
match instr with
| Mlabel lbl' => if peq lbl lbl' then true else false
| _ => false
end.
Lemma is_label_correct:
forall lbl instr,
if is_label lbl instr then instr = Mlabel lbl else instr <> Mlabel lbl.
Proof.
intros. destruct instr; simpl; try discriminate.
case (peq lbl l); intro; congruence.
Qed.
Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
match c with
| nil => None
| i1 :: il => if is_label lbl i1 then Some il else find_label lbl il
end.
(** The three stack-related Mach instructions are interpreted as
memory accesses relative to the stack pointer. More precisely:
- [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative
to the stack pointer.
- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative
to the stack pointer.
- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4]
relative to the pointer found at offset 0 from the stack pointer.
The semantics maintain a linked structure of activation records,
with the current record containing a pointer to the record of the
caller function at offset 0. *)
Definition chunk_of_type (ty: typ) :=
match ty with Tint => Mint32 | Tfloat => Mfloat64 end.
Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).
Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) :=
Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v.
Definition align_16_top (lo hi: Z) :=
Zmax 0 (((hi - lo + 15) / 16) * 16 + lo).
Section RELSEM.
Variable ge: genv.
Definition find_function (ros: mreg + ident) (rs: regset) : option function :=
match ros with
| inl r => Genv.find_funct ge (rs r)
| inr symb =>
match Genv.find_symbol ge symb with
| None => None
| Some b => Genv.find_funct_ptr ge b
end
end.
(** [exec_instr ge f sp c rs m c' rs' m'] reflects the execution of
the first instruction in the current instruction sequence [c].
[c'] is the current instruction sequence after this execution.
[rs] and [rs'] map machine registers to values, respectively
before and after instruction execution. [m] and [m'] are the
memory states before and after. *)
Inductive exec_instr:
function -> val ->
code -> regset -> mem ->
code -> regset -> mem -> Prop :=
| exec_Mlabel:
forall f sp lbl c rs m,
exec_instr f sp
(Mlabel lbl :: c) rs m
c rs m
| exec_Mgetstack:
forall f sp ofs ty dst c rs m v,
load_stack m sp ty ofs = Some v ->
exec_instr f sp
(Mgetstack ofs ty dst :: c) rs m
c (rs#dst <- v) m
| exec_Msetstack:
forall f sp src ofs ty c rs m m',
store_stack m sp ty ofs (rs src) = Some m' ->
exec_instr f sp
(Msetstack src ofs ty :: c) rs m
c rs m'
| exec_Mgetparam:
forall f sp parent ofs ty dst c rs m v,
load_stack m sp Tint (Int.repr 0) = Some parent ->
load_stack m parent ty ofs = Some v ->
exec_instr f sp
(Mgetparam ofs ty dst :: c) rs m
c (rs#dst <- v) m
| exec_Mop:
forall f sp op args res c rs m v,
eval_operation ge sp op rs##args = Some v ->
exec_instr f sp
(Mop op args res :: c) rs m
c (rs#res <- v) m
| exec_Mload:
forall f sp chunk addr args dst c rs m a v,
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
exec_instr f sp
(Mload chunk addr args dst :: c) rs m
c (rs#dst <- v) m
| exec_Mstore:
forall f sp chunk addr args src c rs 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
(Mstore chunk addr args src :: c) rs m
c rs m'
| exec_Mcall:
forall f sp sig ros c rs m f' rs' m',
find_function ros rs = Some f' ->
exec_function f' sp rs m rs' m' ->
exec_instr f sp
(Mcall sig ros :: c) rs m
c rs' m'
| exec_Mgoto:
forall f sp lbl c rs m c',
find_label lbl f.(fn_code) = Some c' ->
exec_instr f sp
(Mgoto lbl :: c) rs m
c' rs m
| exec_Mcond_true:
forall f sp cond args lbl c rs m c',
eval_condition cond rs##args = Some true ->
find_label lbl f.(fn_code) = Some c' ->
exec_instr f sp
(Mcond cond args lbl :: c) rs m
c' rs m
| exec_Mcond_false:
forall f sp cond args lbl c rs m,
eval_condition cond rs##args = Some false ->
exec_instr f sp
(Mcond cond args lbl :: c) rs m
c rs m
with exec_instrs:
function -> val ->
code -> regset -> mem ->
code -> regset -> mem -> Prop :=
| exec_refl:
forall f sp c rs m,
exec_instrs f sp c rs m c rs m
| exec_one:
forall f sp c rs m c' rs' m',
exec_instr f sp c rs m c' rs' m' ->
exec_instrs f sp c rs m c' rs' m'
| exec_trans:
forall f sp c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
exec_instrs f sp c1 rs1 m1 c2 rs2 m2 ->
exec_instrs f sp c2 rs2 m2 c3 rs3 m3 ->
exec_instrs f sp c1 rs1 m1 c3 rs3 m3
(** In addition to reserving the word at offset 0 in the activation
record for maintaining the linking of activation records,
we need to reserve the word at offset 4 to store the return address
into the caller. However, the return address (a pointer within
the code of the caller) is not precisely known at this point:
it will be determined only after the final translation to PowerPC
assembly code. Therefore, we simply reserve that word in the strongest
sense of the word ``reserve'': we make sure that whatever pointer
is stored there at function entry keeps the same value until the
final return instruction, and that the return value and final memory
state are the same regardless of the return address.
This is captured in the evaluation rule [exec_function]
that quantifies universally over all possible values of the return
address, and pass this value to [exec_function_body]. In other
terms, the inference rule [exec_function] has an infinity of
premises, one for each possible return address. Such infinitely
branching inference rules are uncommon in operational semantics,
but cause no difficulties in Coq. *)
with exec_function_body:
function -> val -> val ->
regset -> mem -> regset -> mem -> Prop :=
| exec_funct_body:
forall f parent ra rs m rs' m1 m2 m3 m4 stk c,
Mem.alloc m (- f.(fn_framesize))
(align_16_top (- f.(fn_framesize)) f.(fn_stacksize))
= (m1, stk) ->
let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in
store_stack m1 sp Tint (Int.repr 0) parent = Some m2 ->
store_stack m2 sp Tint (Int.repr 4) ra = Some m3 ->
exec_instrs f sp
f.(fn_code) rs m3
(Mreturn :: c) rs' m4 ->
load_stack m4 sp Tint (Int.repr 0) = Some parent ->
load_stack m4 sp Tint (Int.repr 4) = Some ra ->
exec_function_body f parent ra rs m rs' (Mem.free m4 stk)
with exec_function:
function -> val -> regset -> mem -> regset -> mem -> Prop :=
| exec_funct:
forall f parent rs m rs' m',
(forall ra,
Val.has_type ra Tint ->
exec_function_body f parent 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.
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 /\
exec_function ge f (Vptr Mem.nullptr Int.zero) (Regmap.init Vundef) m0 rs m /\
rs R3 = r.
|
