blob: 0956471883210f61971271db76878ddf853644d4 (
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Correctness proof for RISC-V generation: main proof. *)
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
Require Import Machblockgenproof Asmblockgenproof.
Local Open Scope linking_scope.
Definition block_passes :=
mkpass Machblockgenproof.match_prog
::: mkpass Asmblockgenproof.match_prog
::: mkpass Asm.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. inversion H1. remember (Machblockgen.transf_program p) as mbp.
unfold match_prog; simpl.
exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
exists x; split. apply Asmblockgenproof.transf_program_match; auto.
exists tp; split. apply Asm.transf_program_match; auto. auto.
Qed.
Section PRESERVATION.
Variable prog: Mach.program.
Variable tprog: 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 (inv_trans_rao 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.
eapply compose_forward_simulations. apply Machblockgenproof.transf_program_correct; eauto.
eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
apply Asm.transf_program_correct. eauto.
Qed.
End PRESERVATION.
Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
|
