blob: 6064e4cda00655a714dafe96e8dd2283ee34f1ac (
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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
Require Import Errors RTL BTL BTLmatchRTL.
(** TODO: adapt stuff RTLpathLivegen *)
Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.
Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
match rl with
| nil => true
| r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
end.
(*
Fixpoint iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option Regset.t :=
match ib with
| Bseq ib1 ib2 =>
SOME alive' <- iblock_checker btl ib1 alive IN
iblock_checker btl ib1 alive' (Some ib2)
| Bnop _ =>
iblock_checker btl alive
| Bop _ args dest _ =>
ASSERT list_mem args alive IN
iblock_checker btl (Regset.add dest alive)
| Bload _ _ _ args dest _ =>
ASSERT list_mem args alive IN
iblock_checker btl (Regset.add dest alive)
| Bstore _ _ args src _ =>
ASSERT Regset.mem src alive IN
ASSERT list_mem args alive IN
iblock_checker btl alive
| Bcond _ args (BF (Bgoto s) _) ib2 _ =>
ASSERT list_mem args alive IN
SOME _ <- iblock_checker btl ib2 alive None IN
SOME next <- btl!s IN
ASSERT Regset.subset next.(input_regs) alive IN
iblock_checker btl next.(entry) next.(input_regs) None
| Bcond _ _ _ _ _ => None
| BF _ _ => Some tt
end.
Definition liveness_checker (f: BTL.function): res unit :=
match f.(fn_code)!(f.(fn_entrypoint)) with
| Some ibf => iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs)
| None => Error (msg "liveness_checker: empty function")
end.
*)
Definition liveness_checker (f: BTL.function): res unit := OK tt.
Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
(** TODO: adapt stuff RTLpathLivegenproof *)
Local Notation ext alive := (fun r => Regset.In r alive).
Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
destruct (Pos.eq_dec r1 r2).
- subst. intuition; eapply Regset.add_1; auto.
- intuition.
* right. eapply Regset.add_3; eauto.
* eapply Regset.add_2; auto.
Qed.
Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
forall r, (alive r) -> rs1#r = rs2#r.
(* continue to adapt stuff RTLpathLivegenproof *)
Section FSEM_SIMULATES_CFGSEM.
Variable prog: BTL.program.
Let ge := Genv.globalenv prog.
Hypothesis liveness_checker_correct: forall b f, Genv.find_funct_ptr ge b = Some (Internal f) -> liveness_ok_function f.
Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
Proof.
exploit liveness_checker_correct.
Admitted.
End FSEM_SIMULATES_CFGSEM.
|
