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
|
Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Machregs Locations Stacklayout Conventions.
Require Import Mach Machblock OptionMonad.
(** Registers and States *)
Inductive preg: Type :=
| PC: preg (* program counter *)
| RA: preg (* return-address *)
| SP: preg (* stack-pointer *)
| preg_of: mreg -> preg.
Coercion preg_of: mreg >-> preg.
Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
Proof.
decide equality.
apply mreg_eq.
Defined.
Module PregEq.
Definition t := preg.
Definition eq := preg_eq.
End PregEq.
Module Pregmap := EMap(PregEq).
Definition regset := Pregmap.t val.
Module AsmNotations.
(* Declare Scope asm. *)
Notation "a # b" := (a b) (at level 1, only parsing) : asm.
Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
Open Scope asm.
End AsmNotations.
Import AsmNotations.
Definition to_Machrs (rs: regset): Mach.regset :=
fun (r:mreg) => rs r.
Coercion to_Machrs: regset >-> Mach.regset.
Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset :=
fun (r:preg) =>
match r with
| preg_of mr => mrs mr
| _ => rs r
end.
Local Open Scope option_monad_scope.
Record state: Type := State { _rs: regset; _m: mem }.
Definition outcome := option state.
Definition Next rs m: outcome := Some (State rs m).
Definition Stuck: outcome := None.
(* Asm semantic on Mach *)
Section RELSEM.
(** "oracle" stating the successive position (ie offset) of each block in the final assembly function *)
Variable next: function -> Z -> Z.
Inductive is_pos (f: function): Z -> code -> Prop :=
| First_pos: is_pos f 0 (fn_code f)
| Next_pos pos b c: is_pos f pos (b::c) -> is_pos f (next f pos) c.
Fixpoint label_pos (f: function) (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
match c with
| nil => None
| b :: c' =>
if is_label lbl b then Some pos else label_pos f lbl (next f pos) c'
end.
Definition goto_label (f: function) (lbl: label) (rs: regset) : option val :=
SOME pos <- label_pos f lbl 0 (fn_code f) IN
match rs#PC with
| Vptr b _ => Some (Vptr b (Ptrofs.repr pos))
| _ => None
end.
Definition next_addr (f: function) (rs: regset): option val :=
match rs#PC with
| Vptr b ofs => Some (Vptr b (Ptrofs.repr (next f (Ptrofs.unsigned ofs))))
| _ => None
end.
Variable ge:genv.
Inductive basic_step (f: function) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop :=
| exec_MBgetstack:
forall ofs ty dst v,
load_stack m (rs#SP) ty ofs = Some v ->
basic_step f rs m (MBgetstack ofs ty dst) (rs#dst <- v) m
| exec_MBsetstack:
forall (src: mreg) ofs ty m' rs',
store_stack m (rs#SP) ty ofs (rs src) = Some m' ->
rs' = set_from_Machrs (undef_regs (destroyed_by_setstack ty) rs) rs ->
basic_step f rs m (MBsetstack src ofs ty) rs' m'
| exec_MBgetparam:
forall ofs ty (dst: mreg) v rs' psp,
load_stack m (rs#SP) Tptr f.(fn_link_ofs) = Some psp ->
load_stack m psp ty ofs = Some v ->
rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) ->
basic_step f rs m (MBgetparam ofs ty dst) rs' m
| exec_MBop:
forall op args v rs' (res: mreg),
eval_operation ge (rs#SP) op (to_Machrs rs)##args m = Some v ->
rs' = (set_from_Machrs (undef_regs (destroyed_by_op op) rs) rs)#res <- v ->
basic_step f rs m (MBop op args res) rs' m
| exec_MBload:
forall addr args a v rs' trap chunk (dst: mreg),
eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
Mem.loadv chunk m a = Some v ->
rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- v ->
basic_step f rs m (MBload trap chunk addr args dst) rs' m
| exec_MBload_notrap1:
forall addr args rs' chunk (dst: mreg),
eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = None ->
rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
| exec_MBload_notrap2:
forall addr args a rs' chunk (dst: mreg),
eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
Mem.loadv chunk m a = None ->
rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
| exec_MBstore:
forall chunk addr args (src: mreg) m' a rs',
eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
Mem.storev chunk m a (rs src) = Some m' ->
rs' = set_from_Machrs (undef_regs (destroyed_by_store chunk addr) rs) rs ->
basic_step f rs m (MBstore chunk addr args src) rs' m'
.
Inductive body_step (f: function) : bblock_body -> regset -> mem -> regset -> mem -> Prop :=
| exec_nil_body rs m:
body_step f nil rs m rs m
| exec_cons_body rs m bi p rs' m' rs'' m'':
basic_step f rs m bi rs' m' ->
body_step f p rs' m' rs'' m'' ->
body_step f (bi::p) rs m rs'' m''
.
Definition find_function_ptr (ros: mreg + ident) (rs: regset) : option val :=
match ros with
| inl r => Some (rs#r)
| inr symb =>
SOME b <- Genv.find_symbol ge symb IN
Some (Vptr b Ptrofs.zero)
end.
Definition exec_epilogue (f: function) (rs: regset) (m: mem) : outcome :=
SOME sp <- load_stack m rs#SP Tptr f.(fn_link_ofs) IN
SOME ra <- load_stack m rs#SP Tptr f.(fn_retaddr_ofs) IN
match rs#SP with
| Vptr stk ofs =>
SOME m' <- Mem.free m stk 0 f.(fn_stacksize) IN
Next (rs#SP <- sp #RA <- ra) m'
| _ => Stuck
end.
Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
| exec_MBcall sig ros rs m pc:
find_function_ptr ros rs = Some pc ->
cfi_step f (MBcall sig ros) rs m E0 ((rs#RA <- (rs#PC))#PC <- pc) m
| exec_MBtailcall sig ros rs m rs' m' pc:
find_function_ptr ros rs = Some pc ->
exec_epilogue f rs m = Next rs' m' ->
cfi_step f (MBtailcall sig ros) rs m E0 (rs'#PC <- pc) m'
| exec_MBreturn rs m rs' m':
exec_epilogue f rs m = Next rs' m' ->
cfi_step f MBreturn rs m E0 (rs'#PC <- (rs'#RA)) m'
| exec_MBgoto lbl rs m pc:
goto_label f lbl rs = Some pc ->
cfi_step f (MBgoto lbl) rs m E0 (rs#PC <- pc) m
| exec_MBcond_true cond args lbl rs m pc rs':
eval_condition cond (to_Machrs rs)##args m = Some true ->
goto_label f lbl rs = Some pc ->
rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
cfi_step f (MBcond cond args lbl) rs m E0 (rs'#PC <- pc) m
| exec_MBcond_false cond args lbl rs m rs':
eval_condition cond (to_Machrs rs)##args m = Some false ->
rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
cfi_step f (MBcond cond args lbl) rs m E0 rs' m
| exec_MBjumptable arg tbl rs m index lbl pc rs':
to_Machrs rs arg = Vint index ->
list_nth_z tbl (Int.unsigned index) = Some lbl ->
goto_label f lbl rs = Some pc ->
rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs ->
cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m
| exec_MBbuiltin rs m ef args res vargs t vres rs' m':
eval_builtin_args ge (to_Machrs rs) (rs#SP) m args vargs ->
external_call ef ge vargs m t vres m' ->
rs' = set_from_Machrs (set_res res vres (undef_regs (destroyed_by_builtin ef) rs)) rs ->
cfi_step f (MBbuiltin ef args res) rs m t rs' m'
.
Inductive exit_step f : option control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
| exec_Some_exit ctl rs m t rs' m':
cfi_step f ctl rs m t rs' m' ->
exit_step f (Some ctl) rs m t rs' m'
| exec_None_exit rs m:
exit_step f None rs m E0 rs m
.
Inductive exec_bblock f: bblock -> regset -> mem -> trace -> regset -> mem -> Prop :=
| exec_bblock_all (bb: bblock) rs0 m0 rs1 m1 pc t rs2 m2:
body_step f (body bb) rs0 m0 rs1 m1 ->
next_addr f rs1 = Some pc ->
exit_step f (exit bb) (rs1#PC <- pc) m1 t rs2 m2 ->
exec_bblock f bb rs0 m0 t rs2 m2.
Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state :=
if Z.eq_dec pos 0 then
let (m1, stk) := Mem.alloc m 0 f.(fn_stacksize) in
let sp := Vptr stk Ptrofs.zero in
SOME m2 <- store_stack m1 sp Tptr f.(fn_link_ofs) rs#SP IN
SOME m3 <- store_stack m2 sp Tptr f.(fn_retaddr_ofs) rs#RA IN
Next ((set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs)#SP <- sp) m3
else
Next rs m.
Inductive step: state -> trace -> state -> Prop :=
| exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2:
rs0 PC = Vptr b ofs ->
Genv.find_funct_ptr ge b = Some (Internal f) ->
is_pos f (Ptrofs.unsigned ofs) (bb::c) ->
exec_prologue f (Ptrofs.unsigned ofs) rs0 m0 = Next rs1 m1 ->
exec_bblock f bb rs1 m1 t rs2 m2 ->
step (State rs0 m0) t (State rs2 m2)
| exec_step_external:
forall b ef args res rs m t rs' m',
rs PC = Vptr b Ptrofs.zero ->
Genv.find_funct_ptr ge b = Some (External ef) ->
extcall_arguments (to_Machrs rs) m (rs#SP) (ef_sig ef) args ->
external_call ef ge args m t res m' ->
rs' = (set_from_Machrs (set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs)) rs) #PC <- (rs RA) ->
step (State rs m) t (State rs' m').
End RELSEM.
Inductive initial_state (p: program): state -> Prop :=
| initial_state_intro: forall m0,
let ge := Genv.globalenv p in
Genv.init_mem p = Some m0 ->
let rs0 :=
(Pregmap.init Vundef)
# PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
# SP <- Vnullptr
# RA <- Vnullptr in
initial_state p (State rs0 m0).
Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall rs m r retcode,
loc_result signature_main = One r ->
rs PC = Vnullptr ->
rs r = Vint retcode ->
final_state (State rs m) retcode.
Definition semantics (next: function -> Z -> Z) (p: program) :=
Semantics (step next) (initial_state p) final_state (Genv.globalenv p).
|
