blob: 2baba025a74ab85a79208ab6b22de585155b0e3a (
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
|
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 *)
Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *)
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.
|
