blob: 276e95d1b7ed08fca47c3d47ff2d16648d367e16 (
plain)
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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Justus Fasse UGA, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock.
Require Machblockgenproof Asmblockgenproof.
Require Import Asmgen.
Module Asmblock_PRESERVATION.
Import Asmblock_TRANSF.
Definition match_prog (p: Asmblock.program) (tp: Asm.program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
intros. eapply match_transform_partial_program; eauto.
Qed.
Section PRESERVATION.
Variable prog: Asmblock.program.
Variable tprog: Asm.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs),
Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
Proof.
unfold lk; simpl. intros; rewrite Asm.symbol_high_low.
Admitted.
Lemma transf_program_correct:
forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog).
Admitted. (* TODO *)
End PRESERVATION.
End Asmblock_PRESERVATION.
Local Open Scope linking_scope.
Definition block_passes :=
mkpass Machblockgenproof.match_prog
::: mkpass PseudoAsmblockproof.match_prog
::: mkpass Asmblockgenproof.match_prog
::: mkpass Asmblock_PRESERVATION.match_prog
::: pass_nil _.
Definition match_prog := pass_match (compose_passes block_passes).
Lemma transf_program_match:
forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
Proof.
intros p tp H.
unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
inversion_clear H. apply bind_inversion in H1. destruct H1.
inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
unfold match_prog; simpl.
exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
Qed.
(** Return Address Offset *)
Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
Lemma return_address_exists:
forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
exists ra, return_address_offset f c ra.
Proof.
intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
Admitted.
Section PRESERVATION.
Variable prog: Mach.program.
Variable tprog: Asm.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
Proof.
unfold match_prog in TRANSF. simpl in TRANSF.
inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
eapply compose_forward_simulations.
{ exploit Machblockgenproof.transf_program_correct; eauto. }
eapply compose_forward_simulations.
+ apply PseudoAsmblockproof.transf_program_correct; eauto.
- intros; apply Asmblockgenproof.next_progress.
- intros; eapply Asmblockgenproof.functions_bound_max_pos; eauto.
{ intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
+ eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
{ intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
apply Asmblock_PRESERVATION.transf_program_correct. eauto.
Qed.
End PRESERVATION.
Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
(*******************************************)
(* Stub actually needed by driver/Compiler *)
Module Asmgenproof0.
Definition return_address_offset := return_address_offset.
End Asmgenproof0.
|
