blob: 465b1538ff70be4b67e9d551d13ef3255133f354 (
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
139
140
141
142
143
144
145
146
147
148
149
150
|
(** RTL node duplication using external oracle. Used to form superblock
structures *)
Require Import AST RTL Maps Globalenvs.
Require Import Coqlib Errors Op.
Local Open Scope error_monad_scope.
Local Open Scope positive_scope.
(** External oracle returning the new RTL code (entry point unchanged),
along with the new entrypoint, and a mapping of new nodes to old nodes *)
Axiom duplicate_aux: function -> code * node * (PTree.t node).
Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
Record xfunction : Type :=
{ fn_RTL: function;
fn_revmap: PTree.t node;
}.
Definition xfundef := AST.fundef xfunction.
Definition xprogram := AST.program xfundef unit.
Definition xgenv := Genv.t xfundef unit.
Definition fundef_RTL (fu: xfundef) : fundef :=
match fu with
| Internal f => Internal (fn_RTL f)
| External ef => External ef
end.
(** * Verification of node duplications *)
Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit :=
match ((fn_revmap xf)!(fn_entrypoint (fn_RTL xf))) with
| None => Error (msg "verify_mapping: No node in xf revmap for entrypoint")
| Some n => match (Pos.compare n (fn_entrypoint f)) with
| Eq => OK tt
| _ => Error (msg "verify_mapping_entrypoint: xf revmap for entrypoint does not correspond to the entrypoint of f")
end
end.
Definition verify_is_copy revmap n n' :=
match revmap!n' with
| None => Error(msg "verify_is_copy None")
| Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
end.
Definition verify_match_inst revmap inst tinst :=
match inst with
| Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
| Iop op lr r n => match tinst with
Iop op' lr' r' n' =>
do u <- verify_is_copy revmap n n';
if (eq_operation op op') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then
OK tt
else Error (msg "Different r in Iop")
else Error (msg "Different lr in Iop")
else Error(msg "Different operations in Iop")
| _ => Error(msg "verify_match_inst Inop") end
| Iload m a lr r n => match tinst with
| Iload m' a' lr' r' n' =>
do u <- verify_is_copy revmap n n';
if (chunk_eq m m') then
if (eq_addressing a a') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r in Iload")
else Error (msg "Different lr in Iload")
else Error (msg "Different addressing in Iload")
else Error (msg "Different mchunk in Iload")
| _ => Error (msg "verify_match_inst Iload") end
| Istore m a lr r n => match tinst with
| Istore m' a' lr' r' n' =>
do u <- verify_is_copy revmap n n';
if (chunk_eq m m') then
if (eq_addressing a a') then
if (list_eq_dec Pos.eq_dec lr lr') then
if (Pos.eq_dec r r') then OK tt
else Error (msg "Different r in Istore")
else Error (msg "Different lr in Istore")
else Error (msg "Different addressing in Istore")
else Error (msg "Different mchunk in Istore")
| _ => Error (msg "verify_match_inst Istore") end
| _ => Error(msg "not implemented")
end.
Definition verify_mapping_mn f xf (m: positive*positive) :=
let (tn, n) := m in
match (fn_code f)!n with
| None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n")
| Some inst => match (fn_code (fn_RTL xf))!tn with
| None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn")
| Some tinst => verify_match_inst (fn_revmap xf) inst tinst
end
end.
Fixpoint verify_mapping_mn_rec f xf lm :=
match lm with
| nil => OK tt
| m :: lm => do u <- verify_mapping_mn f xf m;
do u2 <- verify_mapping_mn_rec f xf lm;
OK tt
end.
Definition verify_mapping_match_nodes (f: function) (xf: xfunction) : res unit :=
verify_mapping_mn_rec f xf (PTree.elements (fn_revmap xf)).
(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *)
Definition verify_mapping (f: function) (xf: xfunction) : res unit :=
do u <- verify_mapping_entrypoint f xf;
do v <- verify_mapping_match_nodes f xf; OK tt.
(* TODO - verify the other axiom *)
(** * Entry points *)
Definition transf_function_aux (f: function) : res xfunction :=
let (tcte, mp) := duplicate_aux f in
let (tc, te) := tcte in
let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in
do u <- verify_mapping f xf;
OK xf.
Theorem transf_function_aux_preserves:
forall f xf,
transf_function_aux f = OK xf ->
fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf).
Proof.
intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H.
repeat (split; try reflexivity).
Qed.
Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf).
Proof. apply transf_function_aux_preserves. Qed.
Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf).
Proof. apply transf_function_aux_preserves. Qed.
Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf).
Proof. apply transf_function_aux_preserves. Qed.
Definition transf_function (f: function) : res function :=
do xf <- transf_function_aux f;
OK (fn_RTL xf).
Definition transf_fundef (f: fundef) : res fundef :=
transf_partial_fundef transf_function f.
Definition transf_program (p: program) : res program :=
transform_partial_program transf_fundef p.
|
