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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Prashanth Mundkur, SRI International *)
(* *)
(* 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. *)
(* *)
(* The contributions by Prashanth Mundkur are reused and adapted *)
(* under the terms of a Contributor License Agreement between *)
(* SRI International and INRIA. *)
(* *)
(* *********************************************************************)
(** Abstract syntax and semantics for K1c assembly language. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Locations.
Require Stacklayout.
Require Import Conventions.
Require Import Errors.
Require Export Asmvliw.
Section RELSEM.
(** Execution of arith instructions *)
Variable ge: genv.
Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec_arith_instr ge ai rs rs.
(** Auxiliaries for memory accesses *)
Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset ge chunk rs rs m m d a ofs.
Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro.
Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs.
Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro.
(** * basic instructions *)
Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m.
Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
match body with
| nil => Next rs m
| bi::body' =>
match exec_basic_instr bi rs m with
| Next rs' m' => exec_body body' rs' m'
| Stuck => Stuck
end
end.
(** Position corresponding to a label *)
Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
(** Evaluating a branch
Warning: in m PC is assumed to be already pointing on the next instruction !
*)
Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := par_eval_branch f l rs rs m res.
(** Execution of a single control-flow instruction [i] in initial state [rs] and
[m]. Return updated state.
As above: PC is assumed to be incremented on the next block before the control-flow instruction
For instructions that correspond tobuiltin
actual RISC-V instructions, the cases are straightforward
transliterations of the informal descriptions given in the RISC-V
user-mode specification. For pseudo-instructions, refer to the
informal descriptions given above.
Note that we set to [Vundef] the registers used as temporaries by
the expansions of the pseudo-instructions, so that the RISC-V code
we generate cannot use those registers to hold values that must
survive the execution of the pseudo-instruction. *)
Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := parexec_control ge f oc rs rs m.
Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
match exec_body (body b) rs0 m with
| Next rs' m' =>
let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'
| Stuck => Stuck
end.
(** TODO
* For now, we consider a builtin is alone in a basic block.
* Perhaps there is a way to avoid that ?
*)
Inductive step: state -> trace -> state -> Prop :=
| exec_step_internal:
forall b ofs f bi rs m rs' m',
rs PC = Vptr b ofs ->
Genv.find_funct_ptr ge b = Some (Internal f) ->
find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi ->
exec_bblock f bi rs m = Next rs' m' ->
step (State rs m) E0 (State rs' m')
| exec_step_builtin:
forall b ofs f ef args res rs m vargs t vres rs' m' bi,
rs PC = Vptr b ofs ->
Genv.find_funct_ptr ge b = Some (Internal f) ->
find_bblock (Ptrofs.unsigned ofs) f.(fn_blocks) = Some bi ->
exit bi = Some (PExpand (Pbuiltin ef args res)) ->
eval_builtin_args ge rs (rs SP) m args vargs ->
external_call ef ge vargs m t vres m' ->
rs' = nextblock bi
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef))
(rs#RTMP <- Vundef))) ->
step (State rs m) t (State rs' m')
| 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) ->
external_call ef ge args m t res m' ->
extcall_arguments rs m (ef_sig ef) args ->
rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) ->
step (State rs m) t (State rs' m')
.
End RELSEM.
Definition semantics (p: program) :=
Semantics step (initial_state p) final_state (Genv.globalenv p).
(* Useless
Remark extcall_arguments_determ:
forall rs m sg args1 args2,
extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
intros until m.
assert (A: forall l v1 v2,
extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
{ intros. inv H; inv H0; congruence. }
assert (B: forall p v1 v2,
extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
{ intros. inv H; inv H0.
eapply A; eauto.
f_equal; eapply A; eauto. }
assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
{
induction 1; intros vl2 EA; inv EA.
auto.
f_equal; eauto. }
intros. eapply C; eauto.
Qed.
Lemma semantics_determinate: forall p, determinate (semantics p).
Proof.
Ltac Equalities :=
match goal with
| [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
rewrite H1 in H2; inv H2; Equalities
| _ => idtac
end.
intros; constructor; simpl; intros.
- (* determ *)
inv H; inv H0; Equalities.
+ split. constructor. auto.
+ unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate.
rewrite H9 in H4. discriminate.
+ unfold exec_bblock in H13. destruct (exec_body _ _ _ _); try discriminate.
rewrite H4 in H13. discriminate.
+ assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
exploit external_call_determ. eexact H6. eexact H13. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
+ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
exploit external_call_determ. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros. inv H; simpl.
omega.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)
inv H; inv H0. f_equal. congruence.
- (* final no step *)
assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
{ intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
inv H. unfold Vzero in H0. red; intros; red; intros.
inv H; rewrite H0 in *; eelim NOTNULL; eauto.
- (* final states *)
inv H; inv H0. congruence.
Qed.
*)
Definition data_preg (r: preg) : bool :=
match r with
| RA => false
| IR GPRA => false
| IR RTMP => false
| IR _ => true
| PC => false
end.
(** Determinacy of the [Asm] semantics. *)
(* Useless.
Remark extcall_arguments_determ:
forall rs m sg args1 args2,
extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
intros until m.
assert (A: forall l v1 v2,
extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
{ intros. inv H; inv H0; congruence. }
assert (B: forall p v1 v2,
extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
{ intros. inv H; inv H0.
eapply A; eauto.
f_equal; eapply A; eauto. }
assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
{
induction 1; intros vl2 EA; inv EA.
auto.
f_equal; eauto. }
intros. eapply C; eauto.
Qed.
Lemma semantics_determinate: forall p, determinate (semantics p).
Proof.
Ltac Equalities :=
match goal with
| [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
rewrite H1 in H2; inv H2; Equalities
| _ => idtac
end.
intros; constructor; simpl; intros.
- (* determ *)
inv H; inv H0; Equalities.
split. constructor. auto.
discriminate.
discriminate.
assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
exploit external_call_determ. eexact H5. eexact H11. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
exploit external_call_determ. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros. inv H; simpl.
omega.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)
inv H; inv H0. f_equal. congruence.
- (* final no step *)
assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
{ intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
inv H. unfold Vzero in H0. red; intros; red; intros.
inv H; rewrite H0 in *; eelim NOTNULL; eauto.
- (* final states *)
inv H; inv H0. congruence.
Qed.
*)
|
