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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.
Require Import Errors Linking BTL_SEtheory BTL_SEimpl.
(** External oracle *)
Axiom scheduler: BTL.function -> BTL.code.
Extract Constant scheduler => "BTLScheduleraux.btl_scheduler".
Definition equiv_input_regs (f1 f2: BTL.function): Prop :=
(forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None)
/\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)).
Lemma equiv_input_regs_union f1 f2:
equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl.
Proof.
intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto.
generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS.
do 2 autodestruct; intuition; try_simplify_someHyps.
intros; exploit EQS; eauto; clear EQS. congruence.
Qed.
Lemma equiv_input_regs_pre f1 f2 tbl or:
equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or.
Proof.
intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto.
Qed.
Lemma equiv_input_regs_tr_inputs f1 f2 l oreg rs:
equiv_input_regs f1 f2 ->
tr_inputs f1 l oreg rs = tr_inputs f2 l oreg rs.
Proof.
intros; unfold tr_inputs; erewrite equiv_input_regs_pre; eauto.
Qed.
(* a specification of the verification to do on each function *)
Record match_function (f1 f2: BTL.function): Prop := {
preserv_fnsig: fn_sig f1 = fn_sig f2;
preserv_fnparams: fn_params f1 = fn_params f2;
preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2;
preserv_inputs: equiv_input_regs f1 f2;
symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 ->
exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
}.
Inductive match_fundef: fundef -> fundef -> Prop :=
| match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
| match_External ef: match_fundef (External ef) (External ef).
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
| match_stackframe_intro
res f sp pc rs rs' f'
(EQREGS: forall r, rs # r = rs' # r)
(TRANSF: match_function f f')
: match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').
Inductive match_states: state -> state -> Prop :=
| match_states_intro
st f sp pc rs rs' m st' f'
(EQREGS: forall r, rs # r = rs' # r)
(STACKS: list_forall2 match_stackframes st st')
(TRANSF: match_function f f')
: match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
| match_states_call
st st' f f' args m
(STACKS: list_forall2 match_stackframes st st')
(TRANSF: match_fundef f f')
: match_states (Callstate st f args m) (Callstate st' f' args m)
| match_states_return
st st' v m
(STACKS: list_forall2 match_stackframes st st')
: match_states (Returnstate st v m) (Returnstate st' v m)
.
Lemma match_stack_equiv stk1 stk2:
list_forall2 match_stackframes stk1 stk2 ->
forall stk3, list_forall2 equiv_stackframe stk2 stk3 ->
list_forall2 match_stackframes stk1 stk3.
Proof.
induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
inv H3; inv H; econstructor; eauto.
intros; rewrite <- EQUIV; auto.
Qed.
Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
Proof.
Local Hint Resolve match_stack_equiv: core.
destruct 1; intros EQ; inv EQ; econstructor; eauto.
intros; rewrite <- EQUIV; auto.
Qed.
Local Open Scope error_monad_scope.
Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=
match lpc with
| nil => OK tt
| pc :: lpc' =>
match (fn_code f1)!pc, (fn_code f2)!pc with
| Some ibf1, Some ibf2 =>
do _ <- simu_check f1 f2 ibf1 ibf2;
check_symbolic_simu_rec f1 f2 lpc'
| _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch")
end
end.
Definition erase_input_regs f1 f2 :=
let code := PTree.map (fun pc ibf =>
let oibf := match (fn_code f2)!pc with
| None => ibf
| Some oibf => oibf
end in
{| entry:= oibf.(entry); input_regs := ibf.(input_regs); binfo := oibf.(binfo) |}) (fn_code f1) in
BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2).
Lemma erase_input_regs_correct f1 f2 f3:
erase_input_regs f1 f2 = f3 ->
equiv_input_regs f1 f3.
Proof.
unfold erase_input_regs; simpl; intros.
unfold equiv_input_regs; intuition auto.
- subst; simpl. rewrite PTree.gmap, H0; simpl; auto.
- subst; simpl in H0. rewrite PTree.gmap in H0.
destruct ((fn_code f1)!pc) eqn:EQF; simpl in H0; inv H0; auto.
- subst; simpl in H1. rewrite PTree.gmap in H1.
rewrite H0 in H1; simpl in H1; inv H1; simpl; auto.
Qed.
Global Opaque erase_input_regs.
Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).
Definition transf_function (f: BTL.function) :=
let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in
let tf' := erase_input_regs f tf in
do _ <- check_symbolic_simu f tf';
OK tf'.
Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
check_symbolic_simu_rec f1 f2 lpc = OK x ->
forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc ->
exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
Proof.
induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction.
destruct HIN; subst.
- rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X.
exists i; split; auto. destruct x0. eapply simu_check_correct; eauto.
- destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X.
eapply IHlpc; eauto.
Qed.
Lemma check_symbolic_simu_correct x f1 f2:
check_symbolic_simu f1 f2 = OK x ->
forall pc ib1, (fn_code f1)!pc = Some ib1 ->
exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
Proof.
unfold check_symbolic_simu; intros X pc ib1 PC.
eapply check_symbolic_simu_rec_correct; intuition eauto.
apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto.
Qed.
Lemma check_symbolic_simu_input_equiv x f1 f2:
transf_function f1 = OK f2 ->
check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
Proof.
unfold transf_function; intros TRANSF X; monadInv TRANSF.
exploit erase_input_regs_correct; eauto.
Qed.
Definition transf_fundef (f: fundef) : res fundef :=
transf_partial_fundef (fun f => transf_function f) f.
Definition transf_program (p: program) : res program :=
transform_partial_program transf_fundef p.
|
