summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-10-17 08:55:24 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-10-17 08:55:24 +0000
commit8a07279be78b9e504d0ea304bca72c49fdad0b37 (patch)
tree2d70651e4d12aba8a847f55184f37af94ef75ba3
parentc48b9097201dc9a1e326acdbce491fe16cab01e6 (diff)
Utilisation d'une monade avec types dependants pour garder trace des proprietes state_incr
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--backend/RTLgen.v190
-rw-r--r--backend/RTLgenproof.v29
-rw-r--r--backend/RTLgenspec.v798
3 files changed, 461 insertions, 556 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 2fe13e5..52a6c8a 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -40,6 +40,41 @@ Record state: Set := mkstate {
st_wf: forall (pc: positive), Plt pc st_nextnode \/ st_code!pc = None
}.
+(** Operations over the global state satisfy a crucial monotonicity property:
+ nodes are only added to the CFG, but are never removed nor their
+ instructions are changed; similarly, fresh nodes and fresh registers
+ are only consumed, but never reused. This property is captured by
+ the following predicate over states, which we show is a partial
+ order. *)
+
+Inductive state_incr: state -> state -> Prop :=
+ state_incr_intro:
+ forall (s1 s2: state),
+ Ple s1.(st_nextnode) s2.(st_nextnode) ->
+ Ple s1.(st_nextreg) s2.(st_nextreg) ->
+ (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) ->
+ state_incr s1 s2.
+
+Lemma state_incr_refl:
+ forall s, state_incr s s.
+Proof.
+ intros. apply state_incr_intro.
+ apply Ple_refl. apply Ple_refl. intros; auto.
+Qed.
+Hint Resolve state_incr_refl: rtlg.
+
+Lemma state_incr_trans:
+ forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3.
+Proof.
+ intros. inversion H. inversion H0. apply state_incr_intro.
+ apply Ple_trans with (st_nextnode s2); assumption.
+ apply Ple_trans with (st_nextreg s2); assumption.
+ intros. transitivity (s2.(st_code)!pc).
+ apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto.
+ apply H3; auto.
+Qed.
+Hint Resolve state_incr_trans: rtlg.
+
(** ** The state and error monad *)
(** The translation functions can fail to produce RTL code, for instance
@@ -50,36 +85,52 @@ Record state: Set := mkstate {
to modify the global state. These luxuries are not available in Coq,
however. Instead, we use a monadic encoding of the translation:
translation functions take the current global state as argument,
- and return either [Error msg] to denote an error, or [OK r s] to denote
- success. [s] is the modified state, and [r] the result value of the
- translation function. In the error case, [msg] is an error message
- (see modules [Errors]) describing the problem.
+ and return either [Error msg] to denote an error,
+ or [OK r s incr] to denote success. [s] is the modified state, [r]
+ the result value of the translation function. and [incr] a proof
+ that the final state is in the [state_incr] relation with the
+ initial state. In the error case, [msg] is an error message (see
+ modules [Errors]) describing the problem.
We now define this monadic encoding -- the ``state and error'' monad --
as well as convenient syntax to express monadic computations. *)
-Set Implicit Arguments.
+Inductive res (A: Set) (s: state): Set :=
+ | Error: Errors.errmsg -> res A s
+ | OK: A -> forall (s': state), state_incr s s' -> res A s.
+
+Implicit Arguments OK [A s].
+Implicit Arguments Error [A s].
+
+Definition mon (A: Set) : Set := forall (s: state), res A s.
-Inductive res (A: Set) : Set :=
- | Error: Errors.errmsg -> res A
- | OK: A -> state -> res A.
+Definition ret (A: Set) (x: A) : mon A :=
+ fun (s: state) => OK x s (state_incr_refl s).
-Definition mon (A: Set) : Set := state -> res A.
+Implicit Arguments ret [A].
-Definition ret (A: Set) (x: A) : mon A := fun (s: state) => OK x s.
+Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
-Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error A msg.
+Implicit Arguments error [A].
Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
fun (s: state) =>
match f s with
- | Error msg => Error B msg
- | OK a s' => g a s'
+ | Error msg => Error msg
+ | OK a s' i =>
+ match g a s' with
+ | Error msg => Error msg
+ | OK b s'' i' => OK b s'' (state_incr_trans s s' s'' i i')
+ end
end.
+Implicit Arguments bind [A B].
+
Definition bind2 (A B C: Set) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
bind f (fun xy => g (fst xy) (snd xy)).
+Implicit Arguments bind2 [A B C].
+
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
@@ -89,7 +140,7 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
(** The initial state (empty CFG). *)
-Lemma init_state_wf:
+Remark init_state_wf:
forall pc, Plt pc 1%positive \/ (PTree.empty instruction)!pc = None.
Proof. intros; right; apply PTree.gempty. Qed.
@@ -99,7 +150,7 @@ Definition init_state : state :=
(** Adding a node with the given instruction to the CFG. Return the
label of the new node. *)
-Lemma add_instr_wf:
+Remark add_instr_wf:
forall s i pc,
let n := s.(st_nextnode) in
Plt pc (Psucc n) \/ (PTree.set n i s.(st_code))!pc = None.
@@ -112,6 +163,20 @@ Proof.
right; assumption.
Qed.
+Remark add_instr_incr:
+ forall s i,
+ let n := s.(st_nextnode) in
+ state_incr s (mkstate s.(st_nextreg)
+ (Psucc n)
+ (PTree.set n i s.(st_code))
+ (add_instr_wf s i)).
+Proof.
+ constructor; simpl.
+ apply Ple_succ.
+ apply Ple_refl.
+ intros. apply PTree.gso. apply Plt_ne; auto.
+Qed.
+
Definition add_instr (i: instruction) : mon node :=
fun s =>
let n := s.(st_nextnode) in
@@ -119,13 +184,14 @@ Definition add_instr (i: instruction) : mon node :=
(mkstate s.(st_nextreg)
(Psucc n)
(PTree.set n i s.(st_code))
- (add_instr_wf s i)).
+ (add_instr_wf s i))
+ (add_instr_incr s i).
(** [add_instr] can be decomposed in two steps: reserving a fresh
CFG node, and filling it later with an instruction. This is needed
to compile loops. *)
-Lemma reserve_instr_wf:
+Remark reserve_instr_wf:
forall s pc,
Plt pc (Psucc s.(st_nextnode)) \/ s.(st_code)!pc = None.
Proof.
@@ -134,13 +200,14 @@ Proof.
right; auto.
Qed.
-Definition reserve_instr : mon node :=
- fun s =>
- let n := s.(st_nextnode) in
- OK n (mkstate s.(st_nextreg) (Psucc n) s.(st_code)
- (reserve_instr_wf s)).
+Definition reserve_instr (s: state): (node * state)%type :=
+ let n := s.(st_nextnode) in
+ (n, mkstate s.(st_nextreg)
+ (Psucc n)
+ s.(st_code)
+ (reserve_instr_wf s)).
-Lemma update_instr_wf:
+Remark update_instr_wf:
forall s n i,
Plt n s.(st_nextnode) ->
forall pc,
@@ -152,24 +219,62 @@ Proof.
rewrite PTree.gso; auto. exact (st_wf s pc).
Qed.
-Definition update_instr (n: node) (i: instruction) : mon unit :=
- fun s =>
- match plt n s.(st_nextnode) with
- | left PEQ =>
- OK tt (mkstate s.(st_nextreg) s.(st_nextnode)
- (PTree.set n i s.(st_code))
- (@update_instr_wf s n i PEQ))
- | right _ =>
- Error unit (Errors.msg "RTLgen.update_instr")
+Definition update_instr (n: node) (i: instruction) (s: state) : state :=
+ match plt n s.(st_nextnode) with
+ | left PLT =>
+ mkstate s.(st_nextreg)
+ s.(st_nextnode)
+ (PTree.set n i s.(st_code))
+ (update_instr_wf s n i PLT)
+ | right _ => s (* never happens *)
+ end.
+
+Remark add_loop_incr:
+ forall s1 s3 i,
+ let n := fst (reserve_instr s1) in
+ let s2 := snd (reserve_instr s1) in
+ state_incr s2 s3 ->
+ state_incr s1 (update_instr n i s3).
+Proof.
+ intros. inv H. unfold update_instr. destruct (plt n (st_nextnode s3)).
+ constructor; simpl.
+ apply Ple_trans with (st_nextnode s2).
+ unfold s2; simpl. apply Ple_succ. auto.
+ assumption.
+ intros. rewrite PTree.gso. rewrite H2. reflexivity.
+ unfold s2; simpl. apply Plt_trans_succ. auto.
+ apply Plt_ne. assumption.
+ elim n0. apply Plt_Ple_trans with (st_nextnode s2).
+ unfold n, s2; simpl; apply Plt_succ. auto.
+Qed.
+
+Definition add_loop (body: node -> mon node) : mon node :=
+ fun (s1: state) =>
+ let nloop := fst(reserve_instr s1) in
+ let s2 := snd(reserve_instr s1) in
+ match body nloop s2 with
+ | Error msg => Error msg
+ | OK nbody s3 i =>
+ OK nbody (update_instr nloop (Inop nbody) s3)
+ (add_loop_incr s1 s3 (Inop nbody) i)
end.
(** Generate a fresh RTL register. *)
+Remark new_reg_incr:
+ forall s,
+ state_incr s (mkstate (Psucc s.(st_nextreg))
+ s.(st_nextnode) s.(st_code) s.(st_wf)).
+Proof.
+ constructor; simpl. apply Ple_refl. apply Ple_succ. auto.
+Qed.
+
Definition new_reg : mon reg :=
fun s =>
OK s.(st_nextreg)
(mkstate (Psucc s.(st_nextreg))
- s.(st_nextnode) s.(st_code) s.(st_wf)).
+ s.(st_nextnode) s.(st_code) s.(st_wf))
+ (new_reg_incr s).
(** ** Operations on mappings *)
@@ -193,7 +298,7 @@ Fixpoint add_vars (map: mapping) (names: list ident)
Definition find_var (map: mapping) (name: ident) : mon reg :=
match PTree.get name map.(map_vars) with
- | None => error reg (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil)
+ | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil)
| Some r => ret r
end.
@@ -202,7 +307,7 @@ Definition add_letvar (map: mapping) (r: reg) : mapping :=
Definition find_letvar (map: mapping) (idx: nat) : mon reg :=
match List.nth_error map.(map_letvars) idx with
- | None => error reg (Errors.msg "RTLgen: unbound let variable")
+ | None => error (Errors.msg "RTLgen: unbound let variable")
| Some r => ret r
end.
@@ -311,7 +416,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
| Econs b bs, r :: rs =>
do no <- transl_exprlist map bs rs nd; transl_expr map b r no
| _, _ =>
- error node (Errors.msg "RTLgen.transl_exprlist")
+ error (Errors.msg "RTLgen.transl_exprlist")
end.
(** Generation of code for variable assignments. *)
@@ -344,7 +449,7 @@ Parameter compile_switch: nat -> table -> comptree.
Definition transl_exit (nexits: list node) (n: nat) : mon node :=
match nth_error nexits n with
- | None => error node (Errors.msg "RTLgen: wrong exit")
+ | None => error (Errors.msg "RTLgen: wrong exit")
| Some ne => ret ne
end.
@@ -415,10 +520,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
do nfalse <- transl_stmt map sfalse nd nexits nret rret;
transl_condition map a ntrue nfalse
| Sloop sbody =>
- do nloop <- reserve_instr;
- do nbody <- transl_stmt map sbody nloop nexits nret rret;
- do x <- update_instr nloop (Inop nbody);
- ret nbody
+ add_loop (fun nloop => transl_stmt map sbody nloop nexits nret rret)
| Sblock sbody =>
transl_stmt map sbody nd (nd :: nexits) nret rret
| Sexit n =>
@@ -430,12 +532,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
do ns <- transl_switch r nexits t;
transl_expr map a r ns)
else
- error node (Errors.msg "RTLgen: wrong switch")
+ error (Errors.msg "RTLgen: wrong switch")
| Sreturn opt_a =>
match opt_a, rret with
| None, None => ret nret
| Some a, Some r => transl_expr map a r nret
- | _, _ => error node (Errors.msg "RTLgen: type mismatch on return")
+ | _, _ => error (Errors.msg "RTLgen: type mismatch on return")
end
| Stailcall sig b cl =>
do rf <- alloc_reg map b;
@@ -465,7 +567,7 @@ Definition transl_fun (f: CminorSel.function) : mon (node * list reg) :=
Definition transl_function (f: CminorSel.function) : Errors.res RTL.function :=
match transl_fun f init_state with
| Error msg => Errors.Error msg
- | OK (nentry, rparams) s =>
+ | OK (nentry, rparams) s i =>
Errors.OK (RTL.mkfunction
f.(CminorSel.fn_sig)
rparams
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index e9a04fc..dd8728f 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -46,8 +46,8 @@ Proof.
Qed.
Lemma add_var_wf:
- forall s1 s2 map name r map',
- add_var map name s1 = OK (r,map') s2 ->
+ forall s1 s2 map name r map' i,
+ add_var map name s1 = OK (r,map') s2 i ->
map_wf map -> map_valid map s1 -> map_wf map'.
Proof.
intros. monadInv H.
@@ -74,8 +74,8 @@ Proof.
Qed.
Lemma add_vars_wf:
- forall names s1 s2 map map' rl,
- add_vars map names s1 = OK (rl,map') s2 ->
+ forall names s1 s2 map map' rl i,
+ add_vars map names s1 = OK (rl,map') s2 i ->
map_wf map -> map_valid map s1 -> map_wf map'.
Proof.
induction names; simpl; intros; monadInv H.
@@ -218,8 +218,8 @@ Qed.
between environments. *)
Lemma match_set_params_init_regs:
- forall il rl s1 map2 s2 vl,
- add_vars init_mapping il s1 = OK (rl, map2) s2 ->
+ forall il rl s1 map2 s2 vl i,
+ add_vars init_mapping il s1 = OK (rl, map2) s2 i ->
match_env map2 (set_params vl il) nil (init_regs vl rl)
/\ (forall r, reg_fresh r s2 -> (init_regs vl rl)#r = Vundef).
Proof.
@@ -234,7 +234,7 @@ Proof.
monadInv EQ1.
destruct vl as [ | v1 vs].
(* vl = nil *)
- destruct (IHil _ _ _ _ nil EQ) as [ME UNDEF]. inv ME. split.
+ destruct (IHil _ _ _ _ nil _ EQ) as [ME UNDEF]. inv ME. split.
constructor; simpl.
intros id v. repeat rewrite PTree.gsspec. destruct (peq id a); intros.
subst a. inv H. exists x1; split. auto. apply Regmap.gi.
@@ -243,7 +243,7 @@ Proof.
destruct (map_letvars x0). auto. simpl in me_letvars0. congruence.
intros. apply Regmap.gi.
(* vl = v1 :: vs *)
- destruct (IHil _ _ _ _ vs EQ) as [ME UNDEF]. inv ME. split.
+ destruct (IHil _ _ _ _ vs _ EQ) as [ME UNDEF]. inv ME. split.
constructor; simpl.
intros id v. repeat rewrite PTree.gsspec. destruct (peq id a); intros.
subst a. inv H. exists x1; split. auto. apply Regmap.gss.
@@ -261,10 +261,10 @@ Qed.
Lemma match_set_locals:
forall map1 s1,
map_wf map1 ->
- forall il rl map2 s2 e le rs,
+ forall il rl map2 s2 e le rs i,
match_env map1 e le rs ->
(forall r, reg_fresh r s1 -> rs#r = Vundef) ->
- add_vars map1 il s1 = OK (rl, map2) s2 ->
+ add_vars map1 il s1 = OK (rl, map2) s2 i ->
match_env map2 (set_locals il e) le rs.
Proof.
induction il; simpl in *; intros.
@@ -278,17 +278,16 @@ Proof.
intros id v. simpl. repeat rewrite PTree.gsspec.
destruct (peq id a). subst a. intro.
exists x1. split. auto. inv H3.
- apply H1. apply reg_fresh_decr with s.
- eapply add_vars_incr; eauto.
+ apply H1. apply reg_fresh_decr with s. auto.
eauto with rtlg.
intros. eapply me_vars; eauto.
simpl. eapply me_letvars; eauto.
Qed.
Lemma match_init_env_init_reg:
- forall params s0 rparams map1 s1 vars rvars map2 s2 vparams,
- add_vars init_mapping params s0 = OK (rparams, map1) s1 ->
- add_vars map1 vars s1 = OK (rvars, map2) s2 ->
+ forall params s0 rparams map1 s1 i1 vars rvars map2 s2 i2 vparams,
+ add_vars init_mapping params s0 = OK (rparams, map1) s1 i1 ->
+ add_vars map1 vars s1 = OK (rvars, map2) s2 i2 ->
match_env map2 (set_locals vars (set_params vparams params))
nil (init_regs vparams rparams).
Proof.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index a291d32..94afff8 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -26,104 +26,100 @@ Require Import RTLgen.
(** * Reasoning about monadic computations *)
-(** The tactics below simplify hypotheses of the form [f ... = OK x s]
+(** The tactics below simplify hypotheses of the form [f ... = OK x s i]
where [f] is a monadic computation. For instance, the hypothesis
- [(do x <- a; b) s = OK y s'] will generate the additional witnesses
- [x], [s1] and the additional hypotheses
- [a s = OK x s1] and [b x s1 = OK y s'], reflecting the fact that
+ [(do x <- a; b) s = OK y s' i] will generate the additional witnesses
+ [x], [s1], [i1], [i'] and the additional hypotheses
+ [a s = OK x s1 i1] and [b x s1 = OK y s' i'], reflecting the fact that
both monadic computations [a] and [b] succeeded.
*)
Remark bind_inversion:
- forall (A B: Set) (f: mon A) (g: A -> mon B) (y: B) (s1 s3: state),
- bind f g s1 = OK y s3 ->
- exists x, exists s2, f s1 = OK x s2 /\ g x s2 = OK y s3.
+ forall (A B: Set) (f: mon A) (g: A -> mon B)
+ (y: B) (s1 s3: state) (i: state_incr s1 s3),
+ bind f g s1 = OK y s3 i ->
+ exists x, exists s2, exists i1, exists i2,
+ f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.
Proof.
- intros until s3. unfold bind. destruct (f s1); intros.
+ intros until i. unfold bind. destruct (f s1); intros.
discriminate.
- exists a; exists s; auto.
+ exists a; exists s'; exists s.
+ destruct (g a s'); inv H.
+ exists s0; auto.
Qed.
Remark bind2_inversion:
forall (A B C: Set) (f: mon (A*B)) (g: A -> B -> mon C)
- (z: C) (s1 s3: state),
- bind2 f g s1 = OK z s3 ->
- exists x, exists y, exists s2, f s1 = OK (x, y) s2 /\ g x y s2 = OK z s3.
+ (z: C) (s1 s3: state) (i: state_incr s1 s3),
+ bind2 f g s1 = OK z s3 i ->
+ exists x, exists y, exists s2, exists i1, exists i2,
+ f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2.
Proof.
- intros until s3. unfold bind2, bind. destruct (f s1). congruence.
- destruct p as [x y]; simpl; intro.
- exists x; exists y; exists s; auto.
+ unfold bind2; intros.
+ exploit bind_inversion; eauto.
+ intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q.
+ exists x; exists y; exists s2; exists i1; exists i2; auto.
Qed.
Ltac monadInv1 H :=
match type of H with
- | (OK _ _ = OK _ _) =>
+ | (OK _ _ _ = OK _ _ _) =>
inversion H; clear H; try subst
- | (Error _ _ = OK _ _) =>
+ | (Error _ _ = OK _ _ _) =>
discriminate
- | (ret _ _ = OK _ _) =>
+ | (ret _ _ = OK _ _ _) =>
inversion H; clear H; try subst
- | (error _ _ = OK _ _) =>
+ | (error _ _ = OK _ _ _) =>
discriminate
- | (bind ?F ?G ?S = OK ?X ?S') =>
+ | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
let x := fresh "x" in (
let s := fresh "s" in (
+ let i1 := fresh "INCR" in (
+ let i2 := fresh "INCR" in (
let EQ1 := fresh "EQ" in (
let EQ2 := fresh "EQ" in (
- destruct (bind_inversion _ _ F G X S S' H) as [x [s [EQ1 EQ2]]];
+ destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
clear H;
- try (monadInv1 EQ2)))))
- | (bind2 ?F ?G ?S = OK ?X ?S') =>
+ try (monadInv1 EQ2)))))))
+ | (bind2 ?F ?G ?S = OK ?X ?S' ?I) =>
let x1 := fresh "x" in (
let x2 := fresh "x" in (
let s := fresh "s" in (
+ let i1 := fresh "INCR" in (
+ let i2 := fresh "INCR" in (
let EQ1 := fresh "EQ" in (
let EQ2 := fresh "EQ" in (
- destruct (bind2_inversion _ _ _ F G X S S' H) as [x1 [x2 [s [EQ1 EQ2]]]];
+ destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]];
clear H;
- try (monadInv1 EQ2))))))
+ try (monadInv1 EQ2))))))))
end.
Ltac monadInv H :=
match type of H with
- | (ret _ _ = OK _ _) => monadInv1 H
- | (error _ _ = OK _ _) => monadInv1 H
- | (bind ?F ?G ?S = OK ?X ?S') => monadInv1 H
- | (bind2 ?F ?G ?S = OK ?X ?S') => monadInv1 H
- | (?F _ _ _ _ _ _ _ _ = OK _ _) =>
+ | (ret _ _ = OK _ _ _) => monadInv1 H
+ | (error _ _ = OK _ _ _) => monadInv1 H
+ | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+ | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+ | (?F _ _ _ _ _ _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ _ _ _ _ _ = OK _ _) =>
+ | (?F _ _ _ _ _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ _ _ _ _ = OK _ _) =>
+ | (?F _ _ _ _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ _ _ _ = OK _ _) =>
+ | (?F _ _ _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ _ _ = OK _ _) =>
+ | (?F _ _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ _ = OK _ _) =>
+ | (?F _ _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ _ = OK _ _) =>
+ | (?F _ _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
- | (?F _ = OK _ _) =>
+ | (?F _ = OK _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
end.
(** * Monotonicity properties of the state *)
-(** Operations over the global state satisfy a crucial monotonicity property:
- nodes are only added to the CFG, but never removed nor their instructions
- changed; similarly, fresh nodes and fresh registers are only consumed,
- but never reused. This property is captured by the following predicate
- over states, which we show is a partial order. *)
-
-Inductive state_incr: state -> state -> Prop :=
- state_incr_intro:
- forall (s1 s2: state),
- Ple s1.(st_nextnode) s2.(st_nextnode) ->
- Ple s1.(st_nextreg) s2.(st_nextreg) ->
- (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) ->
- state_incr s1 s2.
-
Lemma instr_at_incr:
forall s1 s2 n i,
state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i.
@@ -132,26 +128,7 @@ Proof.
rewrite H3. auto. elim (st_wf s1 n); intro.
assumption. congruence.
Qed.
-
-Lemma state_incr_refl:
- forall s, state_incr s s.
-Proof.
- intros. apply state_incr_intro.
- apply Ple_refl. apply Ple_refl. intros; auto.
-Qed.
-Hint Resolve state_incr_refl: rtlg.
-
-Lemma state_incr_trans:
- forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3.
-Proof.
- intros. inversion H. inversion H0. apply state_incr_intro.
- apply Ple_trans with (st_nextnode s2); assumption.
- apply Ple_trans with (st_nextreg s2); assumption.
- intros. transitivity (s2.(st_code)!pc).
- apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto.
- apply H3; auto.
-Qed.
-Hint Resolve state_incr_trans: rtlg.
+Hint Resolve instr_at_incr: rtlg.
(** The following relation between two states is a weaker version of
[state_incr]. It permits changing the contents at an already reserved
@@ -179,7 +156,7 @@ Proof.
left. elim (s1.(st_wf) pc); intro.
elim (n H5). auto.
Qed.
-Hint Resolve state_incr_extends.
+Hint Resolve state_incr_extends: rtlg.
(** * Validity and freshness of registers *)
@@ -276,91 +253,84 @@ Hint Resolve map_valid_incr: rtlg.
(** Properties of [add_instr]. *)
-Lemma add_instr_incr:
- forall s1 s2 i n,
- add_instr i s1 = OK n s2 -> state_incr s1 s2.
-Proof.
- intros. monadInv H.
- apply state_incr_intro; simpl.
- apply Ple_succ.
- apply Ple_refl.
- intros. apply PTree.gso; apply Plt_ne; auto.
-Qed.
-Hint Resolve add_instr_incr: rtlg.
-
Lemma add_instr_at:
- forall s1 s2 i n,
- add_instr i s1 = OK n s2 -> s2.(st_code)!n = Some i.
+ forall s1 s2 incr i n,
+ add_instr i s1 = OK n s2 incr -> s2.(st_code)!n = Some i.
Proof.
intros. monadInv H. simpl. apply PTree.gss.
Qed.
-Hint Resolve add_instr_at.
-
-(** Properties of [reserve_instr] and [update_instr]. *)
-
-Lemma reserve_instr_incr:
- forall s1 s2 n,
- reserve_instr s1 = OK n s2 -> state_incr s1 s2.
-Proof.
- intros. monadInv H.
- apply state_incr_intro; simpl.
- apply Ple_succ.
- apply Ple_refl.
- auto.
-Qed.
-
-Lemma update_instr_incr:
- forall s1 s2 s3 s4 i n t,
- reserve_instr s1 = OK n s2 ->
- state_incr s2 s3 ->
- update_instr n i s3 = OK t s4 ->
- state_incr s1 s4.
-Proof.
- intros.
- generalize H1; clear H1; unfold update_instr.
- case (plt n (st_nextnode s3)); intros. 2: discriminate.
- inv H1. inv H0. monadInv H; simpl in *.
- apply state_incr_intro; simpl.
- eapply Ple_trans; eauto. apply Plt_Ple. apply Plt_succ.
- auto.
- intros. rewrite PTree.gso.
- apply H3. apply Plt_trans_succ; auto.
- apply Plt_ne. auto.
-Qed.
+Hint Resolve add_instr_at: rtlg.
+
+(** Properties of [update_instr] and [add_loop]. The following diagram
+ shows the evolutions of the code component of the state during [add_loop].
+ The vertical bar materializes the [st_nextnode] pointer.
+<<
+ s1: I1 I2 ... In |None None None None None None None
+reserve_instr
+ s2: I1 I2 ... In None|None None None None None None
+body n
+ s3: I1 I2 ... In None Ip ... Iq |None None None
+update_instr
+ s4: I1 I2 ... In Inop Ip ... Iq |None None None
+>>
+ It is apparent that [state_incr s1 s2] and [state_incr s1 s4] hold.
+ Moreover, [state_extends s3 s4] holds but not [state_incr s3 s4].
+*)
Lemma update_instr_extends:
- forall s1 s2 s3 s4 i n t,
- reserve_instr s1 = OK n s2 ->
+ forall s1 s2 s3 i n,
+ reserve_instr s1 = (n, s2) ->
state_incr s2 s3 ->
- update_instr n i s3 = OK t s4 ->
- state_extends s3 s4.
+ state_extends s3 (update_instr n i s3).
Proof.
- intros. injection H. intros EQ1 EQ2.
- red; intros.
+ intros. injection H. intros EQ1 EQ2.
+ unfold update_instr. destruct (plt n (st_nextnode s3)).
+ red; simpl; intros. rewrite PTree.gsspec.
case (peq pc n); intro.
- subst pc. left. inversion H0. rewrite H4. rewrite <- EQ1; simpl.
- destruct (s1.(st_wf) n). rewrite <- EQ2 in H7. elim (Plt_strict _ H7).
+ subst pc. left. inversion H0. subst s0 s4. rewrite H3.
+ rewrite <- EQ1; simpl.
+ destruct (s1.(st_wf) n).
+ rewrite <- EQ2 in H4. elim (Plt_strict _ H4).
auto.
rewrite <- EQ1; rewrite <- EQ2; simpl. apply Plt_succ.
- generalize H1; unfold update_instr.
- case (plt n s3.(st_nextnode)); intros; inv H2.
- right; simpl. apply PTree.gso; auto.
+ auto.
+ red; intros; auto.
+Qed.
+
+Lemma add_loop_inversion:
+ forall f s1 nbody s4 i,
+ add_loop f s1 = OK nbody s4 i ->
+ exists nloop, exists s2, exists s3, exists i',
+ state_incr s1 s2
+ /\ f nloop s2 = OK nbody s3 i'
+ /\ state_extends s3 s4
+ /\ s4.(st_code)!nloop = Some(Inop nbody).
+Proof.
+ intros until i. unfold add_loop.
+ unfold reserve_instr; simpl.
+ set (s2 := mkstate (st_nextreg s1) (Psucc (st_nextnode s1)) (st_code s1)
+ (reserve_instr_wf s1)).
+ set (nloop := st_nextnode s1).
+ case_eq (f nloop s2). intros; discriminate.
+ intros n s3 i' EQ1 EQ2. inv EQ2.
+ exists nloop; exists s2; exists s3; exists i'.
+ split.
+ unfold s2; constructor; simpl.
+ apply Ple_succ. apply Ple_refl. auto.
+ split. auto.
+ split. apply update_instr_extends with s1 s2; auto.
+ unfold update_instr. destruct (plt nloop (st_nextnode s3)).
+ simpl. apply PTree.gss.
+ elim n. apply Plt_Ple_trans with (st_nextnode s2).
+ unfold nloop, s2; simpl; apply Plt_succ.
+ inversion i'; auto.
Qed.
(** Properties of [new_reg]. *)
-Lemma new_reg_incr:
- forall s1 s2 r, new_reg s1 = OK r s2 -> state_incr s1 s2.
-Proof.
- intros. monadInv H.
- apply state_incr_intro; simpl.
- apply Ple_refl. apply Ple_succ. auto.
-Qed.
-Hint Resolve new_reg_incr: rtlg.
-
Lemma new_reg_valid:
- forall s1 s2 r,
- new_reg s1 = OK r s2 -> reg_valid r s2.
+ forall s1 s2 r i,
+ new_reg s1 = OK r s2 i -> reg_valid r s2.
Proof.
intros. monadInv H.
unfold reg_valid; simpl. apply Plt_succ.
@@ -368,8 +338,8 @@ Qed.
Hint Resolve new_reg_valid: rtlg.
Lemma new_reg_fresh:
- forall s1 s2 r,
- new_reg s1 = OK r s2 -> reg_fresh r s1.
+ forall s1 s2 r i,
+ new_reg s1 = OK r s2 i -> reg_fresh r s1.
Proof.
intros. monadInv H.
unfold reg_fresh; simpl.
@@ -378,8 +348,8 @@ Qed.
Hint Resolve new_reg_fresh: rtlg.
Lemma new_reg_not_in_map:
- forall s1 s2 m r,
- new_reg s1 = OK r s2 -> map_valid m s1 -> ~(reg_in_map m r).
+ forall s1 s2 m r i,
+ new_reg s1 = OK r s2 i -> map_valid m s1 -> ~(reg_in_map m r).
Proof.
unfold not; intros; eauto with rtlg.
Qed.
@@ -398,19 +368,9 @@ Qed.
(** Properties of [find_var]. *)
-Lemma find_var_incr:
- forall s1 s2 map name r,
- find_var map name s1 = OK r s2 -> state_incr s1 s2.
-Proof.
- intros until r. unfold find_var.
- case (map_vars map)!name; intros; monadInv H.
- auto with rtlg.
-Qed.
-Hint Resolve find_var_incr: rtlg.
-
Lemma find_var_in_map:
- forall s1 s2 map name r,
- find_var map name s1 = OK r s2 -> reg_in_map map r.
+ forall s1 s2 map name r i,
+ find_var map name s1 = OK r s2 i -> reg_in_map map r.
Proof.
intros until r. unfold find_var; caseEq (map.(map_vars)!name).
intros. inv H0. left; exists name; auto.
@@ -419,8 +379,8 @@ Qed.
Hint Resolve find_var_in_map: rtlg.
Lemma find_var_valid:
- forall s1 s2 map name r,
- find_var map name s1 = OK r s2 -> map_valid map s1 -> reg_valid r s1.
+ forall s1 s2 map name r i,
+ find_var map name s1 = OK r s2 i -> map_valid map s1 -> reg_valid r s1.
Proof.
eauto with rtlg.
Qed.
@@ -428,19 +388,9 @@ Hint Resolve find_var_valid: rtlg.
(** Properties of [find_letvar]. *)
-Lemma find_letvar_incr:
- forall s1 s2 map idx r,
- find_letvar map idx s1 = OK r s2 -> state_incr s1 s2.
-Proof.
- intros until r. unfold find_letvar.
- case (nth_error (map_letvars map) idx); intros; monadInv H.
- auto with rtlg.
-Qed.
-Hint Resolve find_letvar_incr: rtlg.
-
Lemma find_letvar_in_map:
- forall s1 s2 map idx r,
- find_letvar map idx s1 = OK r s2 -> reg_in_map map r.
+ forall s1 s2 map idx r i,
+ find_letvar map idx s1 = OK r s2 i -> reg_in_map map r.
Proof.
intros until r. unfold find_letvar.
caseEq (nth_error (map_letvars map) idx); intros; monadInv H0.
@@ -449,8 +399,8 @@ Qed.
Hint Resolve find_letvar_in_map: rtlg.
Lemma find_letvar_valid:
- forall s1 s2 map idx r,
- find_letvar map idx s1 = OK r s2 -> map_valid map s1 -> reg_valid r s1.
+ forall s1 s2 map idx r i,
+ find_letvar map idx s1 = OK r s2 i -> map_valid map s1 -> reg_valid r s1.
Proof.
eauto with rtlg.
Qed.
@@ -459,8 +409,8 @@ Hint Resolve find_letvar_valid: rtlg.
(** Properties of [add_var]. *)
Lemma add_var_valid:
- forall s1 s2 map1 map2 name r,
- add_var map1 name s1 = OK (r, map2) s2 ->
+ forall s1 s2 map1 map2 name r i,
+ add_var map1 name s1 = OK (r, map2) s2 i ->
map_valid map1 s1 ->
reg_valid r s2 /\ map_valid map2 s2.
Proof.
@@ -475,33 +425,16 @@ Proof.
apply H0. right; auto.
Qed.
-Lemma add_var_incr:
- forall s1 s2 map name rm,
- add_var map name s1 = OK rm s2 -> state_incr s1 s2.
-Proof.
- intros. monadInv H. eauto with rtlg.
-Qed.
-Hint Resolve add_var_incr: rtlg.
-
Lemma add_var_find:
- forall s1 s2 map name r map',
- add_var map name s1 = OK (r,map') s2 -> map'.(map_vars)!name = Some r.
+ forall s1 s2 map name r map' i,
+ add_var map name s1 = OK (r,map') s2 i -> map'.(map_vars)!name = Some r.
Proof.
intros. monadInv H. simpl. apply PTree.gss.
Qed.
-Lemma add_vars_incr:
- forall names s1 s2 map r,
- add_vars map names s1 = OK r s2 -> state_incr s1 s2.
-Proof.
- induction names; simpl; intros; monadInv H.
- auto with rtlg.
- eauto with rtlg.
-Qed.
-
Lemma add_vars_valid:
- forall namel s1 s2 map1 map2 rl,
- add_vars map1 namel s1 = OK (rl, map2) s2 ->
+ forall namel s1 s2 map1 map2 rl i,
+ add_vars map1 namel s1 = OK (rl, map2) s2 i ->
map_valid map1 s1 ->
regs_valid rl s2 /\ map_valid map2 s2.
Proof.
@@ -509,22 +442,21 @@ Proof.
split. red; simpl; intros; tauto. auto.
exploit IHnamel; eauto. intros [A B].
exploit add_var_valid; eauto. intros [C D].
- exploit add_var_incr; eauto. intros INCR.
split. apply regs_valid_cons; eauto with rtlg.
auto.
Qed.
Lemma add_var_letenv:
- forall map1 i s1 r map2 s2,
- add_var map1 i s1 = OK (r, map2) s2 ->
+ forall map1 id s1 r map2 s2 i,
+ add_var map1 id s1 = OK (r, map2) s2 i ->
map2.(map_letvars) = map1.(map_letvars).
Proof.
intros; monadInv H. reflexivity.
Qed.
Lemma add_vars_letenv:
- forall il map1 s1 rl map2 s2,
- add_vars map1 il s1 = OK (rl, map2) s2 ->
+ forall il map1 s1 rl map2 s2 i,
+ add_vars map1 il s1 = OK (rl, map2) s2 i ->
map2.(map_letvars) = map1.(map_letvars).
Proof.
induction il; simpl; intros; monadInv H.
@@ -551,19 +483,10 @@ Qed.
(** * Properties of [alloc_reg] and [alloc_regs] *)
-Lemma alloc_reg_incr:
- forall a s1 s2 map r,
- alloc_reg map a s1 = OK r s2 -> state_incr s1 s2.
-Proof.
- intros until r. unfold alloc_reg.
- case a; eauto with rtlg.
-Qed.
-Hint Resolve alloc_reg_incr: rtlg.
-
Lemma alloc_reg_valid:
- forall a s1 s2 map r,
+ forall a s1 s2 map r i,
map_valid map s1 ->
- alloc_reg map a s1 = OK r s2 -> reg_valid r s2.
+ alloc_reg map a s1 = OK r s2 i -> reg_valid r s2.
Proof.
intros until r. unfold alloc_reg.
case a; eauto with rtlg.
@@ -571,9 +494,9 @@ Qed.
Hint Resolve alloc_reg_valid: rtlg.
Lemma alloc_reg_fresh_or_in_map:
- forall map a s r s',
+ forall map a s r s' i,
map_valid map s ->
- alloc_reg map a s = OK r s' ->
+ alloc_reg map a s = OK r s' i ->
reg_in_map map r \/ reg_fresh r s.
Proof.
intros until s'. unfold alloc_reg.
@@ -582,18 +505,10 @@ Proof.
left; eauto with rtlg.
Qed.
-Lemma alloc_regs_incr:
- forall al s1 s2 map rl,
- alloc_regs map al s1 = OK rl s2 -> state_incr s1 s2.
-Proof.
- induction al; simpl; intros; monadInv H; eauto with rtlg.
-Qed.
-Hint Resolve alloc_regs_incr: rtlg.
-
Lemma alloc_regs_valid:
- forall al s1 s2 map rl,
+ forall al s1 s2 map rl i,
map_valid map s1 ->
- alloc_regs map al s1 = OK rl s2 ->
+ alloc_regs map al s1 = OK rl s2 i ->
regs_valid rl s2.
Proof.
induction al; simpl; intros; monadInv H0.
@@ -603,9 +518,9 @@ Qed.
Hint Resolve alloc_regs_valid: rtlg.
Lemma alloc_regs_fresh_or_in_map:
- forall map al s rl s',
+ forall map al s rl s' i,
map_valid map s ->
- alloc_regs map al s = OK rl s' ->
+ alloc_regs map al s = OK rl s' i ->
forall r, In r rl -> reg_in_map map r \/ reg_fresh r s.
Proof.
induction al; simpl; intros; monadInv H0.
@@ -613,7 +528,7 @@ Proof.
elim H1; intro.
subst r.
eapply alloc_reg_fresh_or_in_map; eauto.
- exploit IHal. apply map_valid_incr with s0; eauto with rtlg. eauto. eauto.
+ exploit IHal. 2: eauto. apply map_valid_incr with s; eauto with rtlg. eauto.
intros [A|B]. auto. right; eauto with rtlg.
Qed.
@@ -674,10 +589,10 @@ Proof.
Qed.
Lemma new_reg_target_ok:
- forall map pr s1 a r s2,
+ forall map pr s1 a r s2 i,
map_valid map s1 ->
regs_valid pr s1 ->
- new_reg s1 = OK r s2 ->
+ new_reg s1 = OK r s2 i ->
target_reg_ok map pr a r.
Proof.
intros. constructor.
@@ -688,16 +603,16 @@ Proof.
Qed.
Lemma alloc_reg_target_ok:
- forall map pr s1 a r s2,
+ forall map pr s1 a r s2 i,
map_valid map s1 ->
regs_valid pr s1 ->
- alloc_reg map a s1 = OK r s2 ->
+ alloc_reg map a s1 = OK r s2 i ->
target_reg_ok map pr a r.
Proof.
intros. unfold alloc_reg in H1. destruct a;
try (eapply new_reg_target_ok; eauto; fail).
(* Evar *)
- generalize H1; unfold find_var. caseEq (map_vars map)!i; intros.
+ generalize H1; unfold find_var. caseEq (map_vars map)!i0; intros.
inv H3. constructor. auto. inv H3.
(* Elet *)
generalize H1; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros.
@@ -705,17 +620,17 @@ Proof.
Qed.
Lemma alloc_regs_target_ok:
- forall map al pr s1 rl s2,
+ forall map al pr s1 rl s2 i,
map_valid map s1 ->
regs_valid pr s1 ->
- alloc_regs map al s1 = OK rl s2 ->
+ alloc_regs map al s1 = OK rl s2 i ->
target_regs_ok map pr al rl.
Proof.
induction al; intros; monadInv H1.
constructor.
constructor.
eapply alloc_reg_target_ok; eauto.
- apply IHal with s s2; eauto with rtlg.
+ apply IHal with s s2 INCR1; eauto with rtlg.
apply regs_valid_cons; eauto with rtlg.
Qed.
@@ -743,8 +658,8 @@ Qed.
Hint Resolve return_reg_ok_incr: rtlg.
Lemma new_reg_return_ok:
- forall s1 r s2 map sig,
- new_reg s1 = OK r s2 ->
+ forall s1 r s2 map sig i,
+ new_reg s1 = OK r s2 i ->
map_valid map s1 ->
return_reg_ok s2 map (ret_reg sig r).
Proof.
@@ -957,9 +872,9 @@ Inductive tr_stmt (c: code) (map: mapping):
Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
| tr_function_intro:
- forall f code rparams map1 s1 rvars map2 s2 nentry nret rret orret nextnode wfcode,
- add_vars init_mapping f.(CminorSel.fn_params) init_state = OK (rparams, map1) s1 ->
- add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 ->
+ forall f code rparams map1 s1 i1 rvars map2 s2 i2 nentry nret rret orret nextnode wfcode,
+ add_vars init_mapping f.(CminorSel.fn_params) init_state = OK (rparams, map1) s1 i1 ->
+ add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 ->
orret = ret_reg f.(CminorSel.fn_sig) rret ->
tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil nret orret ->
code!nret = Some(Ireturn orret) ->
@@ -1065,161 +980,126 @@ Definition expr_condexpr_exprlist_ind
(exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l)).
Lemma add_move_charact:
- forall s ns rs nd rd s',
- add_move rs rd nd s = OK ns s' ->
- tr_move s'.(st_code) ns rs nd rd /\ state_incr s s'.
+ forall s ns rs nd rd s' i,
+ add_move rs rd nd s = OK ns s' i ->
+ tr_move s'.(st_code) ns rs nd rd.
Proof.
intros. unfold add_move in H. destruct (Reg.eq rs rd).
- inv H. split. constructor. auto with rtlg.
- split. constructor. eauto with rtlg. eauto with rtlg.
+ inv H. constructor.
+ constructor. eauto with rtlg.
Qed.
Lemma transl_expr_condexpr_list_charact:
- (forall a map rd nd s ns s' pr
- (TR: transl_expr map a rd nd s = OK ns s')
+ (forall a map rd nd s ns s' pr INCR
+ (TR: transl_expr map a rd nd s = OK ns s' INCR)
(WF: map_valid map s)
(OK: target_reg_ok map pr a rd)
(VALID: regs_valid pr s)
(VALID2: reg_valid rd s),
- tr_expr s'.(st_code) map pr a ns nd rd
- /\ state_incr s s')
+ tr_expr s'.(st_code) map pr a ns nd rd)
/\
- (forall a map ntrue nfalse s ns s' pr
- (TR: transl_condition map a ntrue nfalse s = OK ns s')
+ (forall a map ntrue nfalse s ns s' pr INCR
+ (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
(WF: map_valid map s)
(VALID: regs_valid pr s),
- tr_condition s'.(st_code) map pr a ns ntrue nfalse
- /\ state_incr s s')
+ tr_condition s'.(st_code) map pr a ns ntrue nfalse)
/\
- (forall al map rl nd s ns s' pr
- (TR: transl_exprlist map al rl nd s = OK ns s')
+ (forall al map rl nd s ns s' pr INCR
+ (TR: transl_exprlist map al rl nd s = OK ns s' INCR)
(WF: map_valid map s)
(OK: target_regs_ok map pr al rl)
(VALID1: regs_valid pr s)
(VALID2: regs_valid rl s),
- tr_exprlist s'.(st_code) map pr al ns nd rl
- /\ state_incr s s').
+ tr_exprlist s'.(st_code) map pr al ns nd rl).
Proof.
apply expr_condexpr_exprlist_ind; intros; try (monadInv TR).
(* Evar *)
generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
- exploit add_move_charact; eauto.
- intros [A B].
- split. econstructor; eauto.
- inv OK. left; congruence. right; eauto.
- auto.
+ econstructor; eauto.
+ inv OK. left; congruence. right; eauto.
+ eapply add_move_charact; eauto.
(* Eop *)
- inv OK.
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg. intros [A B].
- split. econstructor; eauto.
- eapply instr_at_incr; eauto.
- apply state_incr_trans with s1; eauto with rtlg.
+ inv OK.
+ econstructor; eauto with rtlg.
+ eapply H; eauto with rtlg.
(* Eload *)
inv OK.
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg. intros [A B].
- split. econstructor; eauto.
- eapply instr_at_incr; eauto.
- apply state_incr_trans with s1; eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply H; eauto with rtlg.
(* Econdition *)
inv OK.
- exploit (H1 _ _ _ _ _ _ pr EQ); eauto with rtlg.
- constructor; auto.
- intros [A B].
- exploit (H0 _ _ _ _ _ _ pr EQ1); eauto with rtlg.
- constructor; auto.
- intros [C D].
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg.
- intros [E F].
- split. econstructor; eauto.
- apply tr_expr_incr with s1; auto.
- apply tr_expr_incr with s0; eauto with rtlg.
- apply state_incr_trans with s0; auto.
- apply state_incr_trans with s1; auto.
+ econstructor; eauto with rtlg.
+ eapply H; eauto with rtlg.
+ apply tr_expr_incr with s1; auto.
+ eapply H0; eauto with rtlg. constructor; auto.
+ apply tr_expr_incr with s0; auto.
+ eapply H1; eauto with rtlg. constructor; auto.
(* Elet *)
inv OK.
- exploit (H0 _ _ _ _ _ _ pr EQ1).
+ econstructor. eapply new_reg_not_in_map; eauto with rtlg.
+ eapply H; eauto with rtlg.
+ apply tr_expr_incr with s1; auto.
+ eapply H0. eauto.
apply add_letvar_valid; eauto with rtlg.
constructor; auto.
red; unfold reg_in_map. simpl. intros [[id A] | [B | C]].
elim H1. left; exists id; auto.
subst x. apply valid_fresh_absurd with rd s. auto. eauto with rtlg.
elim H1. right; auto.
- eauto with rtlg. eauto with rtlg.
- intros [A B].
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg. intros [C D].
- split. econstructor.
- eapply new_reg_not_in_map; eauto with rtlg. eauto.
- apply tr_expr_incr with s1; auto.
- eauto with rtlg.
+ eauto with rtlg. eauto with rtlg.
(* Eletvar *)
generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0.
monadInv EQ1.
- exploit add_move_charact; eauto.
- intros [A B].
- split. econstructor; eauto.
- inv OK. left; congruence. right; eauto.
- auto.
+ econstructor; eauto with rtlg.
+ inv OK. left; congruence. right; eauto.
+ eapply add_move_charact; eauto.
monadInv EQ1.
(* CEtrue *)
- split. constructor. auto with rtlg.
+ constructor.
(* CEfalse *)
- split. constructor. auto with rtlg.
+ constructor.
(* CEcond *)
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg.
- intros [A B].
- split. econstructor; eauto.
- apply instr_at_incr with s1; eauto with rtlg.
- eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply H; eauto with rtlg.
(* CEcondition *)
- exploit (H1 _ _ _ _ _ _ pr EQ); eauto with rtlg.
- intros [A B].
- exploit (H0 _ _ _ _ _ _ pr EQ1); eauto with rtlg.
- intros [C D].
- exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg.
- intros [E F].
- split. econstructor; eauto.
- apply tr_condition_incr with s1; eauto with rtlg.
- apply tr_condition_incr with s0; eauto with rtlg.
- eauto with rtlg.
+ econstructor.
+ eapply H; eauto with rtlg.
+ apply tr_condition_incr with s1; auto.
+ eapply H0; eauto with rtlg.
+ apply tr_condition_incr with s0; auto.
+ eapply H1; eauto with rtlg.
(* Enil *)
- destruct rl; inv TR. split. constructor. eauto with rtlg.
+ destruct rl; inv TR. constructor.
(* Econs *)
- destruct rl; simpl in TR; monadInv TR. inv OK.
- exploit H0; eauto.
- apply regs_valid_cons. apply VALID2. auto with coqlib. auto.
- red; intros; apply VALID2; auto with coqlib.
- intros [A B].
- exploit H; eauto.
- eauto with rtlg.
- eauto with rtlg.
+ destruct rl; simpl in TR; monadInv TR. inv OK.
+ econstructor.
+ eapply H; eauto with rtlg.
generalize (VALID2 r (in_eq _ _)). eauto with rtlg.
- intros [C D].
- split. econstructor; eauto.
apply tr_exprlist_incr with s0; auto.
- apply state_incr_trans with s0; eauto with rtlg.
+ eapply H0; eauto with rtlg.
+ apply regs_valid_cons. apply VALID2. auto with coqlib. auto.
+ red; intros; apply VALID2; auto with coqlib.
Qed.
Lemma transl_expr_charact:
- forall a map rd nd s ns s'
- (TR: transl_expr map a rd nd s = OK ns s')
+ forall a map rd nd s ns s' INCR
+ (TR: transl_expr map a rd nd s = OK ns s' INCR)
(WF: map_valid map s)
(OK: target_reg_ok map nil a rd)
(VALID2: reg_valid rd s),
- tr_expr s'.(st_code) map nil a ns nd rd
- /\ state_incr s s'.
+ tr_expr s'.(st_code) map nil a ns nd rd.
Proof.
destruct transl_expr_condexpr_list_charact as [A [B C]].
intros. eapply A; eauto with rtlg.
Qed.
Lemma transl_condexpr_charact:
- forall a map ntrue nfalse s ns s'
- (TR: transl_condition map a ntrue nfalse s = OK ns s')
+ forall a map ntrue nfalse s ns s' INCR
+ (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
(WF: map_valid map s),
- tr_condition s'.(st_code) map nil a ns ntrue nfalse
- /\ state_incr s s'.
+ tr_condition s'.(st_code) map nil a ns ntrue nfalse.
Proof.
destruct transl_expr_condexpr_list_charact as [A [B C]].
intros. eapply B; eauto with rtlg.
@@ -1283,225 +1163,151 @@ Qed.
Lemma store_var_charact:
- forall map rs id nd s ns s',
- store_var map rs id nd s = OK ns s' ->
- tr_store_var s'.(st_code) map rs id ns nd /\ state_incr s s'.
+ forall map rs id nd s ns s' incr,
+ store_var map rs id nd s = OK ns s' incr ->
+ tr_store_var s'.(st_code) map rs id ns nd.
Proof.
intros. monadInv H. generalize EQ. unfold find_var.
caseEq ((map_vars map)!id). 2: intros; discriminate. intros. monadInv EQ1.
- exploit add_move_charact; eauto. intros [A B].
- split; auto. exists x; auto.
+ exists x; split. auto. eapply add_move_charact; eauto.
Qed.
Lemma store_optvar_charact:
- forall map rs optid nd s ns s',
- store_optvar map rs optid nd s = OK ns s' ->
- tr_store_optvar s'.(st_code) map rs optid ns nd /\ state_incr s s'.
+ forall map rs optid nd s ns s' incr,
+ store_optvar map rs optid nd s = OK ns s' incr ->
+ tr_store_optvar s'.(st_code) map rs optid ns nd.
Proof.
intros. destruct optid; simpl in H; simpl.
eapply store_var_charact; eauto.
- monadInv H. split. auto. apply state_incr_refl.
+ monadInv H. auto.
Qed.
Lemma transl_exit_charact:
- forall nexits n s ne s',
- transl_exit nexits n s = OK ne s' ->
+ forall nexits n s ne s' incr,
+ transl_exit nexits n s = OK ne s' incr ->
nth_error nexits n = Some ne /\ s' = s.
Proof.
- intros until s'. unfold transl_exit.
+ intros until incr. unfold transl_exit.
destruct (nth_error nexits n); intro; monadInv H. auto.
Qed.
Lemma transl_switch_charact:
- forall r nexits t s ns s',
- transl_switch r nexits t s = OK ns s' ->
- tr_switch s'.(st_code) r nexits t ns /\ state_incr s s'.
+ forall r nexits t s ns s' incr,
+ transl_switch r nexits t s = OK ns s' incr ->
+ tr_switch s'.(st_code) r nexits t ns.
Proof.
induction t; simpl; intros.
exploit transl_exit_charact; eauto. intros [A B].
- split. econstructor; eauto. subst s'; auto with rtlg.
+ econstructor; eauto.
monadInv H.
exploit transl_exit_charact; eauto. intros [A B]. subst s1.
- exploit IHt; eauto. intros [C D].
- split. econstructor; eauto with rtlg.
+ econstructor; eauto with rtlg.
apply tr_switch_extends with s0; eauto with rtlg.
- eauto with rtlg.
monadInv H.
- exploit IHt2; eauto. intros [A B].
- exploit IHt1; eauto. intros [C D].
- split. econstructor.
+ econstructor; eauto with rtlg.
apply tr_switch_extends with s1; eauto with rtlg.
apply tr_switch_extends with s0; eauto with rtlg.
- eauto with rtlg.
- eauto with rtlg.
Qed.
Lemma transl_stmt_charact:
- forall map stmt nd nexits nret rret s ns s'
- (TR: transl_stmt map stmt nd nexits nret rret s = OK ns s')
+ forall map stmt nd nexits nret rret s ns s' INCR
+ (TR: transl_stmt map stmt nd nexits nret rret s = OK ns s' INCR)
(WF: map_valid map s)
(OK: return_reg_ok s map rret),
- tr_stmt s'.(st_code) map stmt ns nd nexits nret rret
- /\ state_incr s s'.
+ tr_stmt s'.(st_code) map stmt ns nd nexits nret rret.
Proof.
induction stmt; intros; simpl in TR; try (monadInv TR).
(* Sskip *)
- split. constructor. auto with rtlg.
+ constructor.
(* Sassign *)
- exploit store_var_charact; eauto. intros [A B].
- exploit transl_expr_charact; eauto with rtlg.
- intros [C D].
- split. econstructor; eauto.
- apply tr_store_var_extends with s1; eauto with rtlg.
- eauto with rtlg.
+ econstructor. eapply transl_expr_charact; eauto with rtlg.
+ apply tr_store_var_extends with s1; auto with rtlg.
+ eapply store_var_charact; eauto.
(* Sstore *)
- assert (state_incr s s1). eauto with rtlg.
- assert (state_incr s s2). eauto with rtlg.
- assert (map_valid map s2). eauto with rtlg.
destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
- exploit (P1 _ _ _ _ _ _ _ x EQ2).
- auto.
- eapply alloc_reg_target_ok with (s1 := s0); eauto with rtlg.
- apply regs_valid_incr with s0; eauto with rtlg.
- apply reg_valid_incr with s1; eauto with rtlg.
- intros [A B].
- exploit (P3 _ _ _ _ _ _ _ nil EQ4).
- apply map_valid_incr with s2; auto.
- eapply alloc_regs_target_ok with (s1 := s); eauto with rtlg.
- auto with rtlg.
- apply regs_valid_incr with s0; eauto with rtlg.
- intros [C D].
- split. econstructor; eauto.
- apply tr_expr_incr with s3; eauto with rtlg.
- apply instr_at_incr with s2; eauto with rtlg.
- eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply P3; eauto with rtlg.
+ apply tr_expr_incr with s3; eauto with rtlg.
+ eapply P1; eauto with rtlg.
(* Scall *)
- assert (state_incr s0 s3).
- apply state_incr_trans with s1. eauto with rtlg.
- apply state_incr_trans with s2; eauto with rtlg.
- exploit store_optvar_charact; eauto. intros [A B].
- assert (state_incr s0 s5) by eauto with rtlg.
destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
- exploit (P3 _ _ _ _ _ _ _ (x :: nil) EQ4).
- apply map_valid_incr with s0; auto.
- eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
- apply regs_valid_cons; eauto with rtlg.
- apply regs_valid_incr with s1.
- apply state_incr_trans with s3; eauto with rtlg.
- apply regs_valid_cons; eauto with rtlg.
- apply regs_valid_incr with s2.
- apply state_incr_trans with s3; eauto with rtlg.
- eauto with rtlg.
- intros [C D].
- exploit (P1 _ _ _ _ _ _ _ nil EQ6).
- apply map_valid_incr with s0; eauto with rtlg.
- eapply alloc_reg_target_ok with (s1 := s0); eauto with rtlg.
- auto with rtlg.
- apply reg_valid_incr with s1.
- apply state_incr_trans with s3; eauto with rtlg.
- eauto with rtlg.
- intros [E F].
- split. econstructor; eauto.
- apply tr_exprlist_incr with s6; eauto.
- apply instr_at_incr with s5; eauto with rtlg.
+ assert (state_incr s0 s3) by eauto with rtlg.
+ assert (state_incr s3 s6) by eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply P1; eauto with rtlg.
+ apply tr_exprlist_incr with s6. auto.
+ eapply P3; eauto with rtlg.
+ eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
+ apply regs_valid_cons; eauto with rtlg.
+ apply regs_valid_incr with s1; eauto with rtlg.
+ apply regs_valid_cons; eauto with rtlg.
+ apply regs_valid_incr with s2; eauto with rtlg.
apply tr_store_optvar_extends with s4; eauto with rtlg.
- red; intro.
- apply valid_fresh_absurd with x1 s2.
- apply reg_valid_incr with s0; eauto with rtlg.
- eauto with rtlg.
- eauto with rtlg.
+ eapply store_optvar_charact; eauto with rtlg.
(* Salloc *)
- exploit store_var_charact; eauto. intros [A B].
- exploit transl_expr_charact; eauto.
- apply map_valid_incr with s; auto.
- apply state_incr_trans with s1; eauto with rtlg.
- eapply alloc_reg_target_ok with (s1 := s); eauto with rtlg.
- apply reg_valid_incr with s0; eauto with rtlg.
- intros [C D].
- split. econstructor; eauto.
- apply instr_at_incr with s3; eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
apply tr_store_var_extends with s2; eauto with rtlg.
- red; intro.
- apply valid_fresh_absurd with x0 s0.
- apply reg_valid_incr with s; eauto with rtlg.
- eauto with rtlg.
- apply state_incr_trans with s2; eauto with rtlg.
+ eapply store_var_charact; eauto with rtlg.
(* Sseq *)
- exploit IHstmt2; eauto with rtlg. intros [A B].
- exploit IHstmt1; eauto with rtlg. intros [C D].
- split. econstructor; eauto. apply tr_stmt_incr with s0; eauto with rtlg.
- eauto with rtlg.
+ econstructor.
+ apply tr_stmt_incr with s0; auto.
+ eapply IHstmt2; eauto with rtlg.
+ eapply IHstmt1; eauto with rtlg.
(* Sifthenelse *)
destruct (more_likely c stmt1 stmt2); monadInv TR.
- exploit IHstmt2; eauto. intros [A B].
- exploit IHstmt1; eauto with rtlg. intros [C D].
- exploit transl_condexpr_charact; eauto with rtlg. intros [E F].
- split. econstructor; eauto.
- apply tr_stmt_incr with s1; eauto with rtlg.
- apply tr_stmt_incr with s0; eauto with rtlg.
- eauto with rtlg.
- exploit IHstmt1; eauto. intros [A B].
- exploit IHstmt2; eauto with rtlg. intros [C D].
- exploit transl_condexpr_charact; eauto with rtlg. intros [E F].
- split. econstructor; eauto.
- apply tr_stmt_incr with s0; eauto with rtlg.
- apply tr_stmt_incr with s1; eauto with rtlg.
- eauto with rtlg.
+ econstructor.
+ apply tr_stmt_incr with s1; auto.
+ eapply IHstmt1; eauto with rtlg.
+ apply tr_stmt_incr with s0; auto.
+ eapply IHstmt2; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
+ econstructor.
+ apply tr_stmt_incr with s0; auto.
+ eapply IHstmt1; eauto with rtlg.
+ apply tr_stmt_incr with s1; auto.
+ eapply IHstmt2; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
(* Sloop *)
- assert (state_incr s s0).
- eapply reserve_instr_incr; eauto.
- exploit IHstmt; eauto with rtlg. intros [A B].
- split. econstructor.
- apply tr_stmt_extends with s1; eauto.
- eapply update_instr_extends; eauto.
- unfold update_instr in EQ0.
- destruct (plt x (st_nextnode s1)); inv EQ0.
- simpl. apply PTree.gss.
- eapply update_instr_incr; eauto.
+ exploit add_loop_inversion; eauto.
+ intros [nloop [s2 [s3 [INCR23 [INCR02 [EQ [EXT CODEAT]]]]]]].
+ econstructor.
+ apply tr_stmt_extends with s3; auto.
+ eapply IHstmt; eauto with rtlg.
+ auto.
(* Sblock *)
- exploit IHstmt; eauto. intros [A B].
- split. econstructor; eauto. auto.
+ econstructor.
+ eapply IHstmt; eauto with rtlg.
(* Sexit *)
- exploit transl_exit_charact; eauto. intros [A B]. subst s'.
- split. econstructor; eauto. auto with rtlg.
+ exploit transl_exit_charact; eauto. intros [A B].
+ econstructor. eauto.
(* Sswitch *)
generalize TR; clear TR.
set (t := compile_switch n l).
caseEq (validate_switch n l t); intro VALID; intros.
- monadInv TR.
- exploit transl_switch_charact; eauto with rtlg. intros [A B].
- exploit transl_expr_charact; eauto with rtlg. intros [C D].
- split. econstructor; eauto with rtlg.
- apply tr_switch_extends with s1; eauto with rtlg.
- eauto with rtlg.
+ monadInv TR.
+ econstructor; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
+ apply tr_switch_extends with s1; auto with rtlg.
+ eapply transl_switch_charact; eauto with rtlg.
monadInv TR.
(* Sreturn *)
destruct o; destruct rret; inv TR.
- inv OK.
- exploit transl_expr_charact; eauto with rtlg.
+ inv OK.
+ econstructor; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
constructor. auto. simpl; tauto.
- intros [A B].
- split. econstructor; eauto. auto.
- split. constructor. auto with rtlg.
+ constructor.
(* Stailcall *)
- assert (state_incr s0 s2) by eauto with rtlg.
destruct transl_expr_condexpr_list_charact as [A [B C]].
- exploit (C _ _ _ _ _ _ _ (x ::nil) EQ2); eauto with rtlg.
- apply alloc_regs_target_ok with s1 s2; eauto with rtlg.
- apply regs_valid_cons. eauto with rtlg. apply regs_valid_nil.
- apply regs_valid_cons. apply reg_valid_incr with s1; eauto with rtlg.
- apply regs_valid_nil.
- apply regs_valid_incr with s2; eauto with rtlg.
- intros [D E].
- exploit (A _ _ _ _ _ _ _ nil EQ4); eauto with rtlg.
- apply reg_valid_incr with s1; eauto with rtlg.
- intros [F G].
- split. econstructor; eauto.
- apply tr_exprlist_incr with s4; eauto.
- apply instr_at_incr with s3; eauto with rtlg.
- eauto with rtlg.
+ assert (RV: regs_valid (x :: nil) s1).
+ apply regs_valid_cons; eauto with rtlg.
+ econstructor; eauto with rtlg.
+ eapply A; eauto with rtlg.
+ apply tr_exprlist_incr with s4; auto.
+ eapply C; eauto with rtlg.
Qed.
Lemma transl_function_charact:
@@ -1511,17 +1317,15 @@ Lemma transl_function_charact:
Proof.
intros until tf. unfold transl_function.
caseEq (transl_fun f init_state). congruence.
- intros [nentry rparams] sfinal TR E. inv E.
+ intros [nentry rparams] sfinal INCR TR E. inv E.
monadInv TR.
exploit add_vars_valid. eexact EQ. apply init_mapping_valid.
intros [A B].
exploit add_vars_valid. eexact EQ1. auto.
intros [C D].
- exploit transl_stmt_charact; eauto with rtlg.
+ eapply tr_function_intro; eauto with rtlg.
+ eapply transl_stmt_charact; eauto with rtlg.
unfold ret_reg. destruct (sig_res (CminorSel.fn_sig f)).
constructor. eauto with rtlg. eauto with rtlg.
constructor.
- intros [E F].
- eapply tr_function_intro; eauto with rtlg.
- apply instr_at_incr with s2; eauto with rtlg.
Qed.