From cc61b0e400fcb7dea8e32a60995c2060e2afded6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 12:21:59 +0100 Subject: begin proving stuff --- backend/CSE2.v | 436 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 436 insertions(+) create mode 100644 backend/CSE2.v (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v new file mode 100644 index 00000000..cca9fa0f --- /dev/null +++ b/backend/CSE2.v @@ -0,0 +1,436 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. + +(* Static analysis *) + +Inductive sym_val : Type := +| SMove (src : reg) +| SOp (op : operation) (args : list reg). + +Definition eq_args (x y : list reg) : { x = y } + { x <> y } := + list_eq_dec peq x y. + +Definition eq_sym_val : forall x y : sym_val, + {x = y} + { x <> y }. +Proof. + generalize eq_operation. + generalize eq_args. + generalize peq. + decide equality. +Defined. + +Module RELATION. + +Definition t := (PTree.t sym_val). +Definition eq (r1 r2 : t) := + forall x, (PTree.get x r1) = (PTree.get x r2). + +Definition top : t := PTree.empty sym_val. + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq. + intros; reflexivity. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq. + intros; eauto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq. + intros; congruence. +Qed. + +Definition sym_val_beq (x y : sym_val) := + if eq_sym_val x y then true else false. + +Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2. + +Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2. +Proof. + unfold beq, eq. intros r1 r2 EQ x. + pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT. + destruct CORRECT as [CORRECTF CORRECTB]. + pose proof (CORRECTF EQ x) as EQx. + clear CORRECTF CORRECTB EQ. + unfold sym_val_beq in *. + destruct (r1 ! x) as [R1x | ] in *; + destruct (r2 ! x) as [R2x | ] in *; + trivial; try contradiction. + destruct (eq_sym_val R1x R2x) in *; congruence. +Qed. + +Definition ge (r1 r2 : t) := + forall x, + match PTree.get x r1 with + | None => True + | Some v => (PTree.get x r2) = Some v + end. + +Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2. +Proof. + unfold eq, ge. + intros r1 r2 EQ x. + pose proof (EQ x) as EQx. + clear EQ. + destruct (r1 ! x). + - congruence. + - trivial. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge. + intros r1 r2 r3 GE12 GE23 x. + pose proof (GE12 x) as GE12x; clear GE12. + pose proof (GE23 x) as GE23x; clear GE23. + destruct (r1 ! x); trivial. + destruct (r2 ! x); congruence. +Qed. + +Definition lub (r1 r2 : t) := + PTree.combine + (fun ov1 ov2 => + match ov1, ov2 with + | (Some v1), (Some v2) => + if eq_sym_val v1 v2 + then ov1 + else None + | None, _ + | _, None => None + end) + r1 r2. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. + unfold ge, lub. + intros r1 r2 x. + rewrite PTree.gcombine by reflexivity. + destruct (_ ! _); trivial. + destruct (_ ! _); trivial. + destruct (eq_sym_val _ _); trivial. +Qed. + +Lemma ge_lub_right: forall x y, ge (lub x y) y. +Proof. + unfold ge, lub. + intros r1 r2 x. + rewrite PTree.gcombine by reflexivity. + destruct (_ ! _); trivial. + destruct (_ ! _); trivial. + destruct (eq_sym_val _ _); trivial. + congruence. +Qed. + +End RELATION. + +Module Type SEMILATTICE_WITHOUT_BOTTOM. + + Parameter t: Type. + Parameter eq: t -> t -> Prop. + Axiom eq_refl: forall x, eq x x. + Axiom eq_sym: forall x y, eq x y -> eq y x. + Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Parameter beq: t -> t -> bool. + Axiom beq_correct: forall x y, beq x y = true -> eq x y. + Parameter ge: t -> t -> Prop. + Axiom ge_refl: forall x y, eq x y -> ge x y. + Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Parameter lub: t -> t -> t. + Axiom ge_lub_left: forall x y, ge (lub x y) x. + Axiom ge_lub_right: forall x y, ge (lub x y) y. + +End SEMILATTICE_WITHOUT_BOTTOM. + +Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). + Definition t := option L.t. + Definition eq (a b : t) := + match a, b with + | None, None => True + | Some x, Some y => L.eq x y + | Some _, None | None, Some _ => False + end. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq; destruct x; trivial. + apply L.eq_refl. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq; destruct x; destruct y; trivial. + apply L.eq_sym. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq; destruct x; destruct y; destruct z; trivial. + - apply L.eq_trans. + - contradiction. + Qed. + + Definition beq (x y : t) := + match x, y with + | None, None => true + | Some x, Some y => L.beq x y + | Some _, None | None, Some _ => false + end. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq, eq. + destruct x; destruct y; trivial; try congruence. + apply L.beq_correct. + Qed. + + Definition ge (x y : t) := + match x, y with + | None, Some _ => False + | _, None => True + | Some a, Some b => L.ge a b + end. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + destruct x; destruct y; trivial. + apply L.ge_refl. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + destruct x; destruct y; destruct z; trivial; try contradiction. + apply L.ge_trans. + Qed. + + Definition bot: t := None. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot. + destruct x; trivial. + Qed. + + Definition lub (a b : t) := + match a, b with + | None, _ => b + | _, None => a + | (Some x), (Some y) => Some (L.lub x y) + end. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_left. + - apply L.ge_refl. + apply L.eq_refl. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_right. + - apply L.ge_refl. + apply L.eq_refl. + Qed. +End ADD_BOTTOM. + +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Definition kill_sym_val (dst : reg) (sv : sym_val) := + match sv with + | SMove src => if peq dst src then true else false + | SOp op args => List.existsb (peq dst) args + end. + +Definition kill (dst : reg) (rel : RELATION.t) := + PTree.filter1 (fun x => negb (kill_sym_val dst x)) + (PTree.remove dst rel). + +Lemma args_unaffected: + forall rs : regset, + forall dst : reg, + forall v, + forall args : list reg, + existsb (fun y : reg => peq dst y) args = false -> + (rs # dst <- v ## args) = (rs ## args). +Proof. + induction args; simpl; trivial. + destruct (peq dst a) as [EQ | NEQ]; simpl. + { discriminate. + } + intro EXIST. + f_equal. + { + apply Regmap.gso. + congruence. + } + apply IHargs. + assumption. +Qed. + +Section SOUNDNESS. + Parameter F V : Type. + Parameter genv: Genv.t F V. + Parameter sp : val. + Parameter m : mem. + +Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := + match PTree.get x rel with + | None => Some (rs # x) + | Some (SMove src) => Some (rs # src) + | Some (SOp op args) => + eval_operation genv sp op (rs ## args) m + end. + +Definition sem_rel (rel : RELATION.t) (rs : regset) := + forall x : reg, (sem_reg rel x rs) = Some (rs # x). + +Lemma kill_sound : + forall rel : RELATION.t, + forall dst : reg, + forall rs, + forall v, + sem_rel rel rs -> + sem_rel (kill dst rel) (rs # dst <- v). +Proof. + unfold sem_rel, kill, sem_reg. + intros until v. + intros REL x. + rewrite PTree.gfilter1. + destruct (Pos.eq_dec dst x). + { + subst x. + rewrite PTree.grs. + rewrite Regmap.gss. + reflexivity. + } + rewrite PTree.gro by congruence. + rewrite Regmap.gso by congruence. + destruct (rel ! x) as [relx | ] eqn:RELx. + 2: reflexivity. + unfold kill_sym_val. + pose proof (REL x) as RELinstx. + rewrite RELx in RELinstx. + destruct relx eqn:SYMVAL. + { + destruct (peq dst src); simpl. + { reflexivity. } + rewrite Regmap.gso by congruence. + assumption. + } + { destruct existsb eqn:EXISTS; simpl. + { reflexivity. } + rewrite args_unaffected by exact EXISTS. + assumption. + } +Qed. + +Definition move (src dst : reg) (rel : RELATION.t) := + PTree.set dst (match PTree.get src rel with + | Some (SMove src') => SMove src' + | _ => SMove src + end) (kill dst rel). + +Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := + match res with + | BR z => kill z rel + | BR_none => rel + | BR_splitlong hi lo => kill_builtin_res hi (kill_builtin_res lo rel) + end. + +Definition apply_instr instr x := + match instr with + | Inop _ + | Icond _ _ _ _ + | Ijumptable _ _ + | Istore _ _ _ _ _ => Some x + | Iop Omove (src :: nil) dst _ => Some (move src dst x) + | Iop _ _ dst _ + | Iload _ _ _ _ dst _ + | Icall _ _ _ dst _ => Some (kill dst x) + | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) + | Itailcall _ _ _ | Ireturn _ => RB.bot + end. + +Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := + match ro with + | None => None + | Some x => + match code ! pc with + | None => RB.bot + | Some instr => apply_instr instr x + end + end. + +Definition forward_map (f : RTL.function) := DS.fixpoint + (RTL.fn_code f) RTL.successors_instr + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). + +Definition get_r (rel : RELATION.t) (x : reg) := + match PTree.get x rel with + | None => x + | Some src => src + end. + +Definition get_rb (rb : RB.t) (x : reg) := + match rb with + | None => x + | Some rel => get_r rel x + end. + +Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := + match fmap with + | None => x + | Some inv => get_rb (PMap.get pc inv) x + end. + +Definition subst_args fmap pc := List.map (subst_arg fmap pc). + +(* Transform *) +Definition transf_instr (fmap : option (PMap.t RB.t)) + (pc: node) (instr: instruction) := + match instr with + | Iop op args dst s => + Iop op (subst_args fmap pc args) dst s + | Iload trap chunk addr args dst s => + Iload trap chunk addr (subst_args fmap pc args) dst s + | Istore chunk addr args src s => + Istore chunk addr (subst_args fmap pc args) src s + | Icall sig ros args dst s => + Icall sig ros (subst_args fmap pc args) dst s + | Itailcall sig ros args => + Itailcall sig ros (subst_args fmap pc args) + | Icond cond args s1 s2 => + Icond cond (subst_args fmap pc args) s1 s2 + | Ijumptable arg tbl => + Ijumptable (subst_arg fmap pc arg) tbl + | Ireturn (Some arg) => + Ireturn (Some (subst_arg fmap pc arg)) + | _ => instr + end. + +Definition transf_function (f: function) : function := + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. + + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. -- cgit From f5dbc0f7555b511c4200c0ce738f44800088e5d9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 15:17:03 +0100 Subject: move sound --- backend/CSE2.v | 104 ++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 85 insertions(+), 19 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index cca9fa0f..a244d3bb 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -279,19 +279,41 @@ Proof. apply IHargs. assumption. Qed. - + +Inductive sym_cases : option sym_val -> Type := +| Move_case : forall src, (sym_cases (Some (SMove src))) +| Other_case : forall osv, (sym_cases osv). + +Definition move_cases (osv : option sym_val) : (sym_cases osv). +Proof. + destruct osv as [sv |]. + { destruct sv; try apply Move_case; apply Other_case. } + apply Other_case. +Defined. + +Definition move (src dst : reg) (rel : RELATION.t) := + PTree.set dst (match move_cases (PTree.get src rel) with + | Move_case src' => SMove src' + | Other_case _ => SMove src + end) (kill dst rel). + Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. Parameter sp : val. Parameter m : mem. - + +Definition sem_sym_val sym rs := + match sym with + | SMove src => Some (rs # src) + | SOp op args => + eval_operation genv sp op (rs ## args) m + end. + Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := - match PTree.get x rel with + match rel ! x with | None => Some (rs # x) - | Some (SMove src) => Some (rs # src) - | Some (SOp op args) => - eval_operation genv sp op (rs ## args) m + | Some sym => sem_sym_val sym rs end. Definition sem_rel (rel : RELATION.t) (rs : regset) := @@ -305,7 +327,7 @@ Lemma kill_sound : sem_rel rel rs -> sem_rel (kill dst rel) (rs # dst <- v). Proof. - unfold sem_rel, kill, sem_reg. + unfold sem_rel, kill, sem_reg, sem_sym_val. intros until v. intros REL x. rewrite PTree.gfilter1. @@ -336,20 +358,63 @@ Proof. assumption. } Qed. - -Definition move (src dst : reg) (rel : RELATION.t) := - PTree.set dst (match PTree.get src rel with - | Some (SMove src') => SMove src' - | _ => SMove src - end) (kill dst rel). -Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := - match res with - | BR z => kill z rel - | BR_none => rel - | BR_splitlong hi lo => kill_builtin_res hi (kill_builtin_res lo rel) - end. +Lemma write_same: + forall rs : regset, + forall src dst : reg, + (rs # dst <- (rs # src)) # src = rs # src. +Proof. + intros. + destruct (peq src dst). + { + subst dst. + apply Regmap.gss. + } + rewrite Regmap.gso by congruence. + reflexivity. +Qed. +Lemma move_sound : + forall rel : RELATION.t, + forall src dst : reg, + forall rs, + sem_rel rel rs -> + sem_rel (move src dst rel) (rs # dst <- (rs # src)). +Proof. + intros until rs. intros REL x. + pose proof (kill_sound rel dst rs (rs # src) REL x) as KILL. + pose proof (REL src) as RELsrc. + unfold move. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + unfold sem_reg in RELsrc. + destruct move_cases; simpl. + { + simpl in RELsrc. + destruct (peq dst src0). + { + subst src0. + rewrite Regmap.gss. + reflexivity. + } + rewrite Regmap.gso by congruence. + assumption. + } + rewrite write_same. + reflexivity. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +(* Definition apply_instr instr x := match instr with | Inop _ @@ -434,3 +499,4 @@ Definition transf_fundef (fd: fundef) : fundef := Definition transf_program (p: program) : program := transform_program transf_fundef p. +*) \ No newline at end of file -- cgit From d28f8d67bf025ff0beb478672813860793f2b2a8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 17:51:29 +0100 Subject: arg replace --- backend/CSE2.v | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 87 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index a244d3bb..61abbcdf 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -297,6 +297,14 @@ Definition move (src dst : reg) (rel : RELATION.t) := | Other_case _ => SMove src end) (kill dst rel). +Definition oper1 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + let rel' := kill dst rel in + PTree.set dst (SOp op (List.map (fun arg => + match move_cases (rel' ! arg) with + | Move_case arg' => arg' + | Other_case _ => arg + end) args)) rel'. Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. @@ -413,7 +421,85 @@ Proof. rewrite Regmap.gso in KILL by congruence. exact KILL. Qed. - + +Lemma move_cases_neq: + forall dst rel a, + a <> dst -> + (match move_cases (kill dst rel) ! a with + | Move_case a' => a' + | Other_case _ => a + end) <> dst. +Proof. + intros until a. intro NEQ. + unfold kill. + rewrite PTree.gfilter1. + rewrite PTree.gro by congruence. + destruct (rel ! a); simpl. + 2: congruence. + destruct s. + { simpl. + destruct peq; simpl; congruence. + } + { simpl. + destruct negb; simpl; congruence. + } +Qed. + +Lemma args_replace_dst : + forall rel, + forall args : list reg, + forall dst : reg, + forall rs : regset, + forall v, + (sem_rel rel rs) -> + not (In dst args) -> + (rs # dst <- v) + ## (map + (fun arg : positive => + match move_cases (kill dst rel) ! arg with + | Move_case arg' => arg' + | Other_case _ => arg + end) args) = rs ## args. +Proof. + induction args; simpl; trivial. + intros until v. + intros REL NOT_IN. + rewrite IHargs by auto. + f_equal. + pose proof (REL a) as RELa. + rewrite Regmap.gso by (apply move_cases_neq; auto). + unfold kill. + unfold sem_reg in RELa. + rewrite PTree.gfilter1. + rewrite PTree.gro by auto. + destruct (rel ! a); simpl; trivial. + destruct s; simpl in *; destruct negb; simpl; congruence. +Qed. + +Lemma oper1_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + not (In dst args) -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper1 op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL NOT_IN EVAL x. + pose proof (kill_sound rel dst rs v REL x) as KILL. + unfold oper1. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + replace ( (* Definition apply_instr instr x := match instr with -- cgit From 569a32b730608002dbb01088660ecf5bfa19dc02 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 17:55:14 +0100 Subject: oper1_sound --- backend/CSE2.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 61abbcdf..87460f90 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -499,7 +499,16 @@ Proof. rewrite PTree.gss. rewrite Regmap.gss. simpl. - replace ( + rewrite args_replace_dst by auto. + assumption. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + (* Definition apply_instr instr x := match instr with -- cgit From 9ec01ece75310b28c79b57697238b57517eb4392 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 18:01:36 +0100 Subject: oper_sound --- backend/CSE2.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 87460f90..a70c3d9f 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -305,6 +305,12 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg) | Move_case arg' => arg' | Other_case _ => arg end) args)) rel'. +Definition oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + if List.in_dec peq dst args + then kill dst rel + else oper1 op dst args rel. + Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. @@ -509,6 +515,27 @@ Proof. exact KILL. Qed. +Lemma oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold oper. + destruct in_dec. + { + apply kill_sound; auto. + } + apply oper1_sound; auto. +Qed. + (* Definition apply_instr instr x := match instr with -- cgit From fe7d4a81d4999c71f856372716a4a198c46ded8e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 18:14:47 +0100 Subject: gen_oper_sound --- backend/CSE2.v | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index a70c3d9f..1278d729 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -305,12 +305,20 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg) | Move_case arg' => arg' | Other_case _ => arg end) args)) rel'. + Definition oper (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := if List.in_dec peq dst args then kill dst rel else oper1 op dst args rel. +Definition gen_oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match op, args with + | Omove, src::nil => move src dst rel + | _, _ => oper op dst args rel + end. + Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. @@ -536,7 +544,35 @@ Proof. apply oper1_sound; auto. Qed. -(* + +Lemma gen_oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (gen_oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold gen_oper. + destruct op. + { destruct args as [ | h0 t0]. + apply oper_sound; auto. + destruct t0. + { + simpl in *. + replace v with (rs # h0) by congruence. + apply move_sound; auto. + } + apply oper_sound; auto. + } + all: apply oper_sound; auto. +Qed. + (* Definition apply_instr instr x := match instr with | Inop _ -- cgit From e4e8c2d83a03090761c23752831499c0547fa037 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 18:23:13 +0100 Subject: renamed kill_reg into kill_mem --- backend/CSE2.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 1278d729..53fc92bf 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -254,7 +254,7 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) := | SOp op args => List.existsb (peq dst) args end. -Definition kill (dst : reg) (rel : RELATION.t) := +Definition kill_reg (dst : reg) (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val dst x)) (PTree.remove dst rel). @@ -295,11 +295,11 @@ Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (match move_cases (PTree.get src rel) with | Move_case src' => SMove src' | Other_case _ => SMove src - end) (kill dst rel). + end) (kill_reg dst rel). Definition oper1 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := - let rel' := kill dst rel in + let rel' := kill_reg dst rel in PTree.set dst (SOp op (List.map (fun arg => match move_cases (rel' ! arg) with | Move_case arg' => arg' @@ -309,7 +309,7 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg) Definition oper (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := if List.in_dec peq dst args - then kill dst rel + then kill_reg dst rel else oper1 op dst args rel. Definition gen_oper (op: operation) (dst : reg) (args : list reg) @@ -347,9 +347,9 @@ Lemma kill_sound : forall rs, forall v, sem_rel rel rs -> - sem_rel (kill dst rel) (rs # dst <- v). + sem_rel (kill_reg dst rel) (rs # dst <- v). Proof. - unfold sem_rel, kill, sem_reg, sem_sym_val. + unfold sem_rel, kill_reg, sem_reg, sem_sym_val. intros until v. intros REL x. rewrite PTree.gfilter1. @@ -439,13 +439,13 @@ Qed. Lemma move_cases_neq: forall dst rel a, a <> dst -> - (match move_cases (kill dst rel) ! a with + (match move_cases (kill_reg dst rel) ! a with | Move_case a' => a' | Other_case _ => a end) <> dst. Proof. intros until a. intro NEQ. - unfold kill. + unfold kill_reg. rewrite PTree.gfilter1. rewrite PTree.gro by congruence. destruct (rel ! a); simpl. @@ -470,7 +470,7 @@ Lemma args_replace_dst : (rs # dst <- v) ## (map (fun arg : positive => - match move_cases (kill dst rel) ! arg with + match move_cases (kill_reg dst rel) ! arg with | Move_case arg' => arg' | Other_case _ => arg end) args) = rs ## args. @@ -482,7 +482,7 @@ Proof. f_equal. pose proof (REL a) as RELa. rewrite Regmap.gso by (apply move_cases_neq; auto). - unfold kill. + unfold kill_reg. unfold sem_reg in RELa. rewrite PTree.gfilter1. rewrite PTree.gro by auto. @@ -582,7 +582,7 @@ Definition apply_instr instr x := | Iop Omove (src :: nil) dst _ => Some (move src dst x) | Iop _ _ dst _ | Iload _ _ _ _ dst _ - | Icall _ _ _ dst _ => Some (kill dst x) + | Icall _ _ _ dst _ => Some (kill_reg dst x) | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) | Itailcall _ _ _ | Ireturn _ => RB.bot end. -- cgit From 3c5122f71e1b3c2348b653b03bc7bcd6cc75ecbf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 19:27:59 +0100 Subject: kill_mem_sound --- backend/CSE2.v | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 59 insertions(+), 8 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 53fc92bf..b26d6820 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -258,6 +258,15 @@ Definition kill_reg (dst : reg) (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val dst x)) (PTree.remove dst rel). +Definition kill_sym_val_mem (sv: sym_val) := + match sv with + | SMove _ => false + | SOp op _ => op_depends_on_memory op + end. + +Definition kill_mem (rel : RELATION.t) := + PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. + Lemma args_unaffected: forall rs : regset, forall dst : reg, @@ -320,10 +329,12 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg) end. Section SOUNDNESS. - Parameter F V : Type. - Parameter genv: Genv.t F V. - Parameter sp : val. - Parameter m : mem. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section SAME_MEMORY. + Variable m : mem. Definition sem_sym_val sym rs := match sym with @@ -341,7 +352,7 @@ Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := Definition sem_rel (rel : RELATION.t) (rs : regset) := forall x : reg, (sem_reg rel x rs) = Some (rs # x). -Lemma kill_sound : +Lemma kill_reg_sound : forall rel : RELATION.t, forall dst : reg, forall rs, @@ -404,7 +415,7 @@ Lemma move_sound : sem_rel (move src dst rel) (rs # dst <- (rs # src)). Proof. intros until rs. intros REL x. - pose proof (kill_sound rel dst rs (rs # src) REL x) as KILL. + pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL. pose proof (REL src) as RELsrc. unfold move. destruct (peq x dst). @@ -504,7 +515,7 @@ Lemma oper1_sound : Proof. intros until v. intros REL NOT_IN EVAL x. - pose proof (kill_sound rel dst rs v REL x) as KILL. + pose proof (kill_reg_sound rel dst rs v REL x) as KILL. unfold oper1. destruct (peq x dst). { @@ -539,7 +550,7 @@ Proof. unfold oper. destruct in_dec. { - apply kill_sound; auto. + apply kill_reg_sound; auto. } apply oper1_sound; auto. Qed. @@ -572,6 +583,46 @@ Proof. } all: apply oper_sound; auto. Qed. + +End SAME_MEMORY. + +Lemma kill_mem_sound : + forall m m' : mem, + forall rel : RELATION.t, + forall rs, + sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. +Proof. + unfold sem_rel, sem_reg. + intros until rs. + intros SEM x. + pose proof (SEM x) as SEMx. + unfold kill_mem. + rewrite PTree.gfilter1. + unfold kill_sym_val_mem. + destruct (rel ! x) as [ sv | ]. + 2: reflexivity. + destruct sv; simpl in *; trivial. + { + destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. + rewrite <- SEMx. + apply op_depends_on_memory_correct; auto. + } +Qed. + +End SOUNDNESS. + +Lemma gen_oper_sound : + forall m m' : mem, + forall sp, + forall rel : RELATION.t, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (gen_oper op dst args rel) (rs # dst <- v). + + +Lemma kill_mem_sound: + forall m' : mem, + (* Definition apply_instr instr x := match instr with -- cgit From c6755b93351943a86f36904c158a81f6f433862d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 19:34:06 +0100 Subject: static analysis done --- backend/CSE2.v | 27 +++++++-------------------- 1 file changed, 7 insertions(+), 20 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index b26d6820..60f2f8a1 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -610,30 +610,16 @@ Proof. Qed. End SOUNDNESS. - -Lemma gen_oper_sound : - forall m m' : mem, - forall sp, - forall rel : RELATION.t, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (gen_oper op dst args rel) (rs # dst <- v). - - -Lemma kill_mem_sound: - forall m' : mem, - (* -Definition apply_instr instr x := +Definition apply_instr instr (rel : RELATION.t) : RB.t := match instr with | Inop _ | Icond _ _ _ _ - | Ijumptable _ _ - | Istore _ _ _ _ _ => Some x - | Iop Omove (src :: nil) dst _ => Some (move src dst x) - | Iop _ _ dst _ - | Iload _ _ _ _ dst _ - | Icall _ _ _ dst _ => Some (kill_reg dst x) + | Ijumptable _ _ => Some rel + | Istore _ _ _ _ _ => Some (kill_mem rel) + | Iop op args dst _ => Some (gen_oper op dst args rel) + | Iload _ _ _ dst _ + | Icall _ _ _ dst _ => Some (kill_reg dst rel) | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) | Itailcall _ _ _ | Ireturn _ => RB.bot end. @@ -652,6 +638,7 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). +(* Definition get_r (rel : RELATION.t) (x : reg) := match PTree.get x rel with | None => x -- cgit From bec3d3e29881590541130ef3f1116bd41df71a25 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 20:21:17 +0100 Subject: simpler definitions --- backend/CSE2.v | 65 ++++++++++++++++++++++------------------------------------ 1 file changed, 24 insertions(+), 41 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 60f2f8a1..36558033 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -289,31 +289,19 @@ Proof. assumption. Qed. -Inductive sym_cases : option sym_val -> Type := -| Move_case : forall src, (sym_cases (Some (SMove src))) -| Other_case : forall osv, (sym_cases osv). - -Definition move_cases (osv : option sym_val) : (sym_cases osv). -Proof. - destruct osv as [sv |]. - { destruct sv; try apply Move_case; apply Other_case. } - apply Other_case. -Defined. +Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match rel ! x with + | Some (SMove org) => org + | _ => x + end. Definition move (src dst : reg) (rel : RELATION.t) := - PTree.set dst (match move_cases (PTree.get src rel) with - | Move_case src' => SMove src' - | Other_case _ => SMove src - end) (kill_reg dst rel). + PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). Definition oper1 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := let rel' := kill_reg dst rel in - PTree.set dst (SOp op (List.map (fun arg => - match move_cases (rel' ! arg) with - | Move_case arg' => arg' - | Other_case _ => arg - end) args)) rel'. + PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. Definition oper (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := @@ -425,9 +413,11 @@ Proof. rewrite PTree.gss. rewrite Regmap.gss. unfold sem_reg in RELsrc. - destruct move_cases; simpl. + simpl. + unfold forward_move. + destruct (rel ! src) as [ sv |]; simpl. + destruct sv; simpl in *. { - simpl in RELsrc. destruct (peq dst src0). { subst src0. @@ -437,8 +427,7 @@ Proof. rewrite Regmap.gso by congruence. assumption. } - rewrite write_same. - reflexivity. + all: f_equal; apply write_same. } rewrite Regmap.gso by congruence. unfold sem_reg. @@ -450,24 +439,21 @@ Qed. Lemma move_cases_neq: forall dst rel a, a <> dst -> - (match move_cases (kill_reg dst rel) ! a with - | Move_case a' => a' - | Other_case _ => a - end) <> dst. + (forward_move (kill_reg dst rel) a) <> dst. Proof. intros until a. intro NEQ. - unfold kill_reg. + unfold kill_reg, forward_move. rewrite PTree.gfilter1. rewrite PTree.gro by congruence. destruct (rel ! a); simpl. 2: congruence. destruct s. - { simpl. + { + unfold kill_sym_val. destruct peq; simpl; congruence. } - { simpl. + all: simpl; destruct negb; simpl; congruence. - } Qed. Lemma args_replace_dst : @@ -480,13 +466,10 @@ Lemma args_replace_dst : not (In dst args) -> (rs # dst <- v) ## (map - (fun arg : positive => - match move_cases (kill_reg dst rel) ! arg with - | Move_case arg' => arg' - | Other_case _ => arg - end) args) = rs ## args. + (forward_move (kill_reg dst rel)) args) = rs ## args. Proof. - induction args; simpl; trivial. + induction args; simpl. + 1: reflexivity. intros until v. intros REL NOT_IN. rewrite IHargs by auto. @@ -495,6 +478,7 @@ Proof. rewrite Regmap.gso by (apply move_cases_neq; auto). unfold kill_reg. unfold sem_reg in RELa. + unfold forward_move. rewrite PTree.gfilter1. rewrite PTree.gro by auto. destruct (rel ! a); simpl; trivial. @@ -555,7 +539,6 @@ Proof. apply oper1_sound; auto. Qed. - Lemma gen_oper_sound : forall rel : RELATION.t, forall op : operation, @@ -640,9 +623,9 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (* Definition get_r (rel : RELATION.t) (x : reg) := - match PTree.get x rel with - | None => x - | Some src => src + match move_cases (PTree.get x rel) with + | Move_case x' => x' + | Other_case _ => x end. Definition get_rb (rb : RB.t) (x : reg) := -- cgit From 7dd2fce8926e3d9fa30ad2619dd38c5e2d535a5e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 20:27:20 +0100 Subject: goes to the end but does not find available ops --- backend/CSE2.v | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 36558033..d5412d73 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -621,23 +621,16 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). -(* -Definition get_r (rel : RELATION.t) (x : reg) := - match move_cases (PTree.get x rel) with - | Move_case x' => x' - | Other_case _ => x - end. - -Definition get_rb (rb : RB.t) (x : reg) := +Definition forward_move_b (rb : RB.t) (x : reg) := match rb with | None => x - | Some rel => get_r rel x + | Some rel => forward_move rel x end. Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := match fmap with | None => x - | Some inv => get_rb (PMap.get pc inv) x + | Some inv => forward_move_b (PMap.get pc inv) x end. Definition subst_args fmap pc := List.map (subst_arg fmap pc). @@ -648,8 +641,8 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) match instr with | Iop op args dst s => Iop op (subst_args fmap pc args) dst s - | Iload trap chunk addr args dst s => - Iload trap chunk addr (subst_args fmap pc args) dst s + | Iload chunk addr args dst s => + Iload chunk addr (subst_args fmap pc args) dst s | Istore chunk addr args src s => Istore chunk addr (subst_args fmap pc args) src s | Icall sig ros args dst s => @@ -678,4 +671,3 @@ Definition transf_fundef (fd: fundef) : fundef := Definition transf_program (p: program) : program := transform_program transf_fundef p. -*) \ No newline at end of file -- cgit From d6f23a4835a644a4f554fcf75485d5da786b7758 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 22:10:11 +0100 Subject: find_op_sound --- backend/CSE2.v | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 110 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index d5412d73..a042b0a9 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -567,6 +567,115 @@ Proof. all: apply oper_sound; auto. Qed. + +Definition find_op_fold op args (already : option reg) x sv := + match already with + | Some found => already + | None => + match sv with + | (SOp op' args') => + if (eq_operation op op') && (eq_args args args') + then Some x + else None + | _ => None + end + end. + +Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := + PTree.fold (find_op_fold op args) rel None. + +Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := + match l with + | nil => True + | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr + end. + +Lemma elements_represent : + forall { X : Type }, + forall tr : (PTree.t X), + (list_represents (PTree.elements tr) tr). +Proof. + intros. + generalize (PTree.elements_complete tr). + generalize (PTree.elements tr). + induction l; simpl; trivial. + intro COMPLETE. + destruct a as [ r sv ]. + split. + { + apply COMPLETE. + left; reflexivity. + } + apply IHl; auto. +Qed. + +Lemma find_op_sound : + forall rel : RELATION.t, + forall op : operation, + forall src dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + find_op rel op args = Some src -> + (eval_operation genv sp op (rs ## args) m) = Some (rs # src). +Proof. + intros until rs. + unfold find_op. + rewrite PTree.fold_spec. + intro REL. + assert ( + forall start, + match start with + | None => True + | Some src => eval_operation genv sp op rs ## args m = Some rs # src + end -> fold_left + (fun (a : option reg) (p : positive * sym_val) => + find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = + Some src -> + eval_operation genv sp op rs ## args m = Some rs # src) as REC. + { + unfold sem_rel, sem_reg in REL. + generalize (PTree.elements_complete rel). + generalize (PTree.elements rel). + induction l; simpl. + { + intros. + subst start. + assumption. + } + destruct a as [r sv]; simpl. + intros COMPLETE start GEN. + apply IHl. + { + intros. + apply COMPLETE. + right. + assumption. + } + unfold find_op_fold. + destruct start. + assumption. + destruct sv. + { trivial. } + destruct eq_operation; trivial. + subst op0. + destruct eq_args; trivial. + subst args0. + simpl. + assert ((rel ! r) = Some (SOp op args)) as RELatr. + { + apply COMPLETE. + left. + reflexivity. + } + pose proof (REL r) as RELr. + rewrite RELatr in RELr. + simpl in RELr. + assumption. + } + apply REC; auto. +Qed. + End SAME_MEMORY. Lemma kill_mem_sound : @@ -634,7 +743,7 @@ Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg : end. Definition subst_args fmap pc := List.map (subst_arg fmap pc). - + (* Transform *) Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := -- cgit From 441524f4b63d8e9fa7161d640fb7be00a7235f3a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 22:18:08 +0100 Subject: use in transformation --- backend/CSE2.v | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index a042b0a9..79c52973 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -709,7 +709,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Icond _ _ _ _ | Ijumptable _ _ => Some rel | Istore _ _ _ _ _ => Some (kill_mem rel) - | Iop op args dst _ => Some (gen_oper op dst args rel) + | Iop op args dst _ => Some (gen_oper op dst args rel) | Iload _ _ _ dst _ | Icall _ _ _ dst _ => Some (kill_reg dst rel) | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) @@ -743,13 +743,31 @@ Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg : end. Definition subst_args fmap pc := List.map (subst_arg fmap pc). - + +Definition gen_move src dst s := + if peq src dst + then Inop s + else Iop Omove (src::nil) dst s. + (* Transform *) +Definition find_op_in_fmap fmap pc op args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => find_op rel op args + | None => None + end + end. + Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => - Iop op (subst_args fmap pc args) dst s + match find_op_in_fmap fmap pc op args with + | None => Iop op (subst_args fmap pc args) dst s + | Some src => gen_move src dst s + end | Iload chunk addr args dst s => Iload chunk addr (subst_args fmap pc args) dst s | Istore chunk addr args src s => -- cgit From 528935a59259b006ed56c83457b3a018494fc9ec Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 22:36:33 +0100 Subject: progress --- backend/CSE2.v | 467 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 467 insertions(+) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 79c52973..011806cc 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -3,6 +3,8 @@ Require Import AST Linking. Require Import Memory Registers Op RTL Maps. Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. (* Static analysis *) @@ -798,3 +800,468 @@ Definition transf_fundef (fd: fundef) : fundef := Definition transf_program (p: program) : program := transform_program transf_fundef p. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; trivial. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +Lemma transf_function_at: + forall (f : function) (pc : node) (i : instruction), + (fn_code f)!pc = Some i -> + (fn_code (transf_function f))!pc = + Some(transf_instr (forward_map f) pc i). +Proof. + intros until i. intro CODE. + unfold transf_function; simpl. + rewrite PTree.gmap. + unfold option_map. + rewrite CODE. + reflexivity. +Qed. + +Definition sem_rel_b (relb : RB.t) sp m (rs : regset) := + match relb with + | Some rel => sem_rel fundef unit ge sp m rel rs + | None => True + end. + +Definition fmap_sem (fmap : option (PMap.t RB.t)) + sp m (pc : node) (rs : regset) := + match fmap with + | None => True + | Some map => sem_rel_b (PMap.get pc map) sp m rs + end. + +(* +Lemma step_simulation: + forall S1 t S2, RTL.step ge S1 t S2 -> + forall S1', match_states S1 S1' -> + exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. + induction 1; intros S1' MS; inv MS; try TR_AT. +- (* nop *) + econstructor; split. eapply exec_Inop; eauto. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. +- (* op *) + econstructor; split. + eapply exec_Iop with (v := v); eauto. + rewrite <- H0. + rewrite subst_args_ok by assumption. + apply eval_operation_preserved. exact symbols_preserved. + constructor; auto. + + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr' in GE. + rewrite MPC in GE. + rewrite H in GE. + + destruct (op_cases op args res pc' mpc) as [[src [OP [ARGS MOVE]]] | KILL]. + { + subst op. + subst args. + rewrite MOVE in GE. + simpl in H0. + simpl in GE. + apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). + assumption. + replace v with (rs # src) by congruence. + apply move_ok. + assumption. + } + rewrite KILL in GE. + apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). + assumption. + apply kill_ok. + assumption. + +(* load *) +- econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + rewrite subst_args_ok; assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. + +- (* load notrap1 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + rewrite subst_args_ok; assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. + +- (* load notrap2 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap2; eauto. + rewrite subst_args_ok; assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. + +- (* store *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. + rewrite subst_args_ok; assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. + +(* call *) +- econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + rewrite subst_args_ok by assumption. + constructor. constructor; auto. constructor. + + { + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). + { + replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_weaken. + assumption. + } + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr' in GE. + unfold fmap_sem in *. + destruct (map # pc) as [mpc |] in *; try contradiction. + rewrite H in GE. + simpl in GE. + unfold is_killed_in_fmap, is_killed_in_map. + unfold RB.ge in GE. + destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial. + eauto. + +(* tailcall *) +- econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + rewrite subst_args_ok by assumption. + constructor. auto. + +(* builtin *) +- econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + + apply get_rb_sem_ge with (rb2 := Some RELATION.top). + { + replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply top_ok. + +(* cond *) +- econstructor; split. + eapply exec_Icond; eauto. + rewrite subst_args_ok; eassumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + destruct b; tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. + +(* jumptbl *) +- econstructor; split. + eapply exec_Ijumptable; eauto. + rewrite subst_arg_ok; eassumption. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + apply list_nth_z_in with (n := Int.unsigned n). + assumption. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. + +(* return *) +- destruct or as [arg | ]. + { + econstructor; split. + eapply exec_Ireturn; eauto. + unfold regmap_optget. + rewrite subst_arg_ok by eassumption. + constructor; auto. + } + econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. + + +(* internal function *) +- simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := Some RELATION.top). + { + eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. + } + apply top_ok. + +(* external function *) +- econstructor; split. + eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. + +(* return *) +- inv STACKS. inv H1. + econstructor; split. + eapply exec_return; eauto. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + unfold is_killed_in_fmap in H8. + unfold is_killed_in_map in H8. + destruct (map # pc) as [mpc |] in *; try contradiction. + destruct H8 as [rel' RGE]. + eapply get_rb_killed; eauto. +Qed. + + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. +*) \ No newline at end of file -- cgit From 93b1e0034733dcc19dc42c04725439e8bdf3d10d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 06:53:30 +0100 Subject: CSE2 split in two files --- backend/CSE2.v | 829 +-------------------------------------------------------- 1 file changed, 2 insertions(+), 827 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 011806cc..0bd5bf81 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -2,10 +2,6 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. -Require Import Globalenvs Values. -Require Import Linking Values Memory Globalenvs Events Smallstep. -Require Import Registers Op RTL. - (* Static analysis *) Inductive sym_val : Type := @@ -269,27 +265,6 @@ Definition kill_sym_val_mem (sv: sym_val) := Definition kill_mem (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. -Lemma args_unaffected: - forall rs : regset, - forall dst : reg, - forall v, - forall args : list reg, - existsb (fun y : reg => peq dst y) args = false -> - (rs # dst <- v ## args) = (rs ## args). -Proof. - induction args; simpl; trivial. - destruct (peq dst a) as [EQ | NEQ]; simpl. - { discriminate. - } - intro EXIST. - f_equal. - { - apply Regmap.gso. - congruence. - } - apply IHargs. - assumption. -Qed. Definition forward_move (rel : RELATION.t) (x : reg) : reg := match rel ! x with @@ -318,258 +293,6 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg) | _, _ => oper op dst args rel end. -Section SOUNDNESS. - Variable F V : Type. - Variable genv: Genv.t F V. - Variable sp : val. - -Section SAME_MEMORY. - Variable m : mem. - -Definition sem_sym_val sym rs := - match sym with - | SMove src => Some (rs # src) - | SOp op args => - eval_operation genv sp op (rs ## args) m - end. - -Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := - match rel ! x with - | None => Some (rs # x) - | Some sym => sem_sym_val sym rs - end. - -Definition sem_rel (rel : RELATION.t) (rs : regset) := - forall x : reg, (sem_reg rel x rs) = Some (rs # x). - -Lemma kill_reg_sound : - forall rel : RELATION.t, - forall dst : reg, - forall rs, - forall v, - sem_rel rel rs -> - sem_rel (kill_reg dst rel) (rs # dst <- v). -Proof. - unfold sem_rel, kill_reg, sem_reg, sem_sym_val. - intros until v. - intros REL x. - rewrite PTree.gfilter1. - destruct (Pos.eq_dec dst x). - { - subst x. - rewrite PTree.grs. - rewrite Regmap.gss. - reflexivity. - } - rewrite PTree.gro by congruence. - rewrite Regmap.gso by congruence. - destruct (rel ! x) as [relx | ] eqn:RELx. - 2: reflexivity. - unfold kill_sym_val. - pose proof (REL x) as RELinstx. - rewrite RELx in RELinstx. - destruct relx eqn:SYMVAL. - { - destruct (peq dst src); simpl. - { reflexivity. } - rewrite Regmap.gso by congruence. - assumption. - } - { destruct existsb eqn:EXISTS; simpl. - { reflexivity. } - rewrite args_unaffected by exact EXISTS. - assumption. - } -Qed. - -Lemma write_same: - forall rs : regset, - forall src dst : reg, - (rs # dst <- (rs # src)) # src = rs # src. -Proof. - intros. - destruct (peq src dst). - { - subst dst. - apply Regmap.gss. - } - rewrite Regmap.gso by congruence. - reflexivity. -Qed. - -Lemma move_sound : - forall rel : RELATION.t, - forall src dst : reg, - forall rs, - sem_rel rel rs -> - sem_rel (move src dst rel) (rs # dst <- (rs # src)). -Proof. - intros until rs. intros REL x. - pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL. - pose proof (REL src) as RELsrc. - unfold move. - destruct (peq x dst). - { - subst x. - unfold sem_reg. - rewrite PTree.gss. - rewrite Regmap.gss. - unfold sem_reg in RELsrc. - simpl. - unfold forward_move. - destruct (rel ! src) as [ sv |]; simpl. - destruct sv; simpl in *. - { - destruct (peq dst src0). - { - subst src0. - rewrite Regmap.gss. - reflexivity. - } - rewrite Regmap.gso by congruence. - assumption. - } - all: f_equal; apply write_same. - } - rewrite Regmap.gso by congruence. - unfold sem_reg. - rewrite PTree.gso by congruence. - rewrite Regmap.gso in KILL by congruence. - exact KILL. -Qed. - -Lemma move_cases_neq: - forall dst rel a, - a <> dst -> - (forward_move (kill_reg dst rel) a) <> dst. -Proof. - intros until a. intro NEQ. - unfold kill_reg, forward_move. - rewrite PTree.gfilter1. - rewrite PTree.gro by congruence. - destruct (rel ! a); simpl. - 2: congruence. - destruct s. - { - unfold kill_sym_val. - destruct peq; simpl; congruence. - } - all: simpl; - destruct negb; simpl; congruence. -Qed. - -Lemma args_replace_dst : - forall rel, - forall args : list reg, - forall dst : reg, - forall rs : regset, - forall v, - (sem_rel rel rs) -> - not (In dst args) -> - (rs # dst <- v) - ## (map - (forward_move (kill_reg dst rel)) args) = rs ## args. -Proof. - induction args; simpl. - 1: reflexivity. - intros until v. - intros REL NOT_IN. - rewrite IHargs by auto. - f_equal. - pose proof (REL a) as RELa. - rewrite Regmap.gso by (apply move_cases_neq; auto). - unfold kill_reg. - unfold sem_reg in RELa. - unfold forward_move. - rewrite PTree.gfilter1. - rewrite PTree.gro by auto. - destruct (rel ! a); simpl; trivial. - destruct s; simpl in *; destruct negb; simpl; congruence. -Qed. - -Lemma oper1_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - not (In dst args) -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper1 op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL NOT_IN EVAL x. - pose proof (kill_reg_sound rel dst rs v REL x) as KILL. - unfold oper1. - destruct (peq x dst). - { - subst x. - unfold sem_reg. - rewrite PTree.gss. - rewrite Regmap.gss. - simpl. - rewrite args_replace_dst by auto. - assumption. - } - rewrite Regmap.gso by congruence. - unfold sem_reg. - rewrite PTree.gso by congruence. - rewrite Regmap.gso in KILL by congruence. - exact KILL. -Qed. - -Lemma oper_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL EVAL. - unfold oper. - destruct in_dec. - { - apply kill_reg_sound; auto. - } - apply oper1_sound; auto. -Qed. - -Lemma gen_oper_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (gen_oper op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL EVAL. - unfold gen_oper. - destruct op. - { destruct args as [ | h0 t0]. - apply oper_sound; auto. - destruct t0. - { - simpl in *. - replace v with (rs # h0) by congruence. - apply move_sound; auto. - } - apply oper_sound; auto. - } - all: apply oper_sound; auto. -Qed. - - Definition find_op_fold op args (already : option reg) x sv := match already with | Some found => already @@ -586,6 +309,7 @@ Definition find_op_fold op args (already : option reg) x sv := Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := PTree.fold (find_op_fold op args) rel None. +(* NO LONGER NEEDED Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := match l with | nil => True @@ -610,100 +334,7 @@ Proof. } apply IHl; auto. Qed. - -Lemma find_op_sound : - forall rel : RELATION.t, - forall op : operation, - forall src dst : reg, - forall args: list reg, - forall rs : regset, - sem_rel rel rs -> - find_op rel op args = Some src -> - (eval_operation genv sp op (rs ## args) m) = Some (rs # src). -Proof. - intros until rs. - unfold find_op. - rewrite PTree.fold_spec. - intro REL. - assert ( - forall start, - match start with - | None => True - | Some src => eval_operation genv sp op rs ## args m = Some rs # src - end -> fold_left - (fun (a : option reg) (p : positive * sym_val) => - find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = - Some src -> - eval_operation genv sp op rs ## args m = Some rs # src) as REC. - { - unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete rel). - generalize (PTree.elements rel). - induction l; simpl. - { - intros. - subst start. - assumption. - } - destruct a as [r sv]; simpl. - intros COMPLETE start GEN. - apply IHl. - { - intros. - apply COMPLETE. - right. - assumption. - } - unfold find_op_fold. - destruct start. - assumption. - destruct sv. - { trivial. } - destruct eq_operation; trivial. - subst op0. - destruct eq_args; trivial. - subst args0. - simpl. - assert ((rel ! r) = Some (SOp op args)) as RELatr. - { - apply COMPLETE. - left. - reflexivity. - } - pose proof (REL r) as RELr. - rewrite RELatr in RELr. - simpl in RELr. - assumption. - } - apply REC; auto. -Qed. - -End SAME_MEMORY. - -Lemma kill_mem_sound : - forall m m' : mem, - forall rel : RELATION.t, - forall rs, - sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. -Proof. - unfold sem_rel, sem_reg. - intros until rs. - intros SEM x. - pose proof (SEM x) as SEMx. - unfold kill_mem. - rewrite PTree.gfilter1. - unfold kill_sym_val_mem. - destruct (rel ! x) as [ sv | ]. - 2: reflexivity. - destruct sv; simpl in *; trivial. - { - destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. - rewrite <- SEMx. - apply op_depends_on_memory_correct; auto. - } -Qed. - -End SOUNDNESS. +*) Definition apply_instr instr (rel : RELATION.t) : RB.t := match instr with @@ -809,459 +440,3 @@ Lemma transf_program_match: Proof. intros. eapply match_transform_program; eauto. Qed. - -Section PRESERVATION. - -Variables prog tprog: program. -Hypothesis TRANSL: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma functions_translated: - forall v f, - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof (Genv.find_funct_transf TRANSL). - -Lemma function_ptr_translated: - forall v f, - Genv.find_funct_ptr ge v = Some f -> - Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (Genv.find_funct_ptr_transf TRANSL). - -Lemma symbols_preserved: - forall id, - Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (Genv.find_symbol_transf TRANSL). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_transf TRANSL). - -Lemma sig_preserved: - forall f, funsig (transf_fundef f) = funsig f. -Proof. - destruct f; trivial. -Qed. - -Lemma find_function_translated: - forall ros rs fd, - find_function ge ros rs = Some fd -> - find_function tge ros rs = Some (transf_fundef fd). -Proof. - unfold find_function; intros. destruct ros as [r|id]. - eapply functions_translated; eauto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. - eapply function_ptr_translated; eauto. -Qed. - -Lemma transf_function_at: - forall (f : function) (pc : node) (i : instruction), - (fn_code f)!pc = Some i -> - (fn_code (transf_function f))!pc = - Some(transf_instr (forward_map f) pc i). -Proof. - intros until i. intro CODE. - unfold transf_function; simpl. - rewrite PTree.gmap. - unfold option_map. - rewrite CODE. - reflexivity. -Qed. - -Definition sem_rel_b (relb : RB.t) sp m (rs : regset) := - match relb with - | Some rel => sem_rel fundef unit ge sp m rel rs - | None => True - end. - -Definition fmap_sem (fmap : option (PMap.t RB.t)) - sp m (pc : node) (rs : regset) := - match fmap with - | None => True - | Some map => sem_rel_b (PMap.get pc map) sp m rs - end. - -(* -Lemma step_simulation: - forall S1 t S2, RTL.step ge S1 t S2 -> - forall S1', match_states S1 S1' -> - exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. -Proof. - induction 1; intros S1' MS; inv MS; try TR_AT. -- (* nop *) - econstructor; split. eapply exec_Inop; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. -- (* op *) - econstructor; split. - eapply exec_Iop with (v := v); eauto. - rewrite <- H0. - rewrite subst_args_ok by assumption. - apply eval_operation_preserved. exact symbols_preserved. - constructor; auto. - - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr' in GE. - rewrite MPC in GE. - rewrite H in GE. - - destruct (op_cases op args res pc' mpc) as [[src [OP [ARGS MOVE]]] | KILL]. - { - subst op. - subst args. - rewrite MOVE in GE. - simpl in H0. - simpl in GE. - apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). - assumption. - replace v with (rs # src) by congruence. - apply move_ok. - assumption. - } - rewrite KILL in GE. - apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). - assumption. - apply kill_ok. - assumption. - -(* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* store *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Istore; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* call *) -- econstructor; split. - eapply exec_Icall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - rewrite subst_args_ok by assumption. - constructor. constructor; auto. constructor. - - { - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). - { - replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_weaken. - assumption. - } - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr' in GE. - unfold fmap_sem in *. - destruct (map # pc) as [mpc |] in *; try contradiction. - rewrite H in GE. - simpl in GE. - unfold is_killed_in_fmap, is_killed_in_map. - unfold RB.ge in GE. - destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial. - eauto. - -(* tailcall *) -- econstructor; split. - eapply exec_Itailcall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - rewrite subst_args_ok by assumption. - constructor. auto. - -(* builtin *) -- econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - - apply get_rb_sem_ge with (rb2 := Some RELATION.top). - { - replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply top_ok. - -(* cond *) -- econstructor; split. - eapply exec_Icond; eauto. - rewrite subst_args_ok; eassumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. - destruct b; tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* jumptbl *) -- econstructor; split. - eapply exec_Ijumptable; eauto. - rewrite subst_arg_ok; eassumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. - apply list_nth_z_in with (n := Int.unsigned n). - assumption. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* return *) -- destruct or as [arg | ]. - { - econstructor; split. - eapply exec_Ireturn; eauto. - unfold regmap_optget. - rewrite subst_arg_ok by eassumption. - constructor; auto. - } - econstructor; split. - eapply exec_Ireturn; eauto. - constructor; auto. - - -(* internal function *) -- simpl. econstructor; split. - eapply exec_function_internal; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := Some RELATION.top). - { - eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. - } - apply top_ok. - -(* external function *) -- econstructor; split. - eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. - -(* return *) -- inv STACKS. inv H1. - econstructor; split. - eapply exec_return; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - unfold is_killed_in_fmap in H8. - unfold is_killed_in_map in H8. - destruct (map # pc) as [mpc |] in *; try contradiction. - destruct H8 as [rel' RGE]. - eapply get_rb_killed; eauto. -Qed. - - -Lemma transf_initial_states: - forall S1, RTL.initial_state prog S1 -> - exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. -Proof. - intros. inv H. econstructor; split. - econstructor. - eapply (Genv.init_mem_transf TRANSL); eauto. - rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. - eapply function_ptr_translated; eauto. - rewrite <- H3; apply sig_preserved. - constructor. constructor. -Qed. - -Lemma transf_final_states: - forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. -Proof. - intros. inv H0. inv H. inv STACKS. constructor. -Qed. - -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTL.semantics tprog). -Proof. - eapply forward_simulation_step. - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact step_simulation. -Qed. -*) \ No newline at end of file -- cgit From 47bcd22f7e1febf10bd0629c1774b7ab39fac872 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 13:25:12 +0100 Subject: CSE2 now works for expressions --- backend/CSE2.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 0bd5bf81..5b850cbb 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -343,8 +343,8 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Ijumptable _ _ => Some rel | Istore _ _ _ _ _ => Some (kill_mem rel) | Iop op args dst _ => Some (gen_oper op dst args rel) - | Iload _ _ _ dst _ - | Icall _ _ _ dst _ => Some (kill_reg dst rel) + | Iload _ _ _ dst _ => Some (kill_reg dst rel) + | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) | Itailcall _ _ _ | Ireturn _ => RB.bot end. @@ -377,11 +377,6 @@ Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg : Definition subst_args fmap pc := List.map (subst_arg fmap pc). -Definition gen_move src dst s := - if peq src dst - then Inop s - else Iop Omove (src::nil) dst s. - (* Transform *) Definition find_op_in_fmap fmap pc op args := match fmap with @@ -399,7 +394,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) | Iop op args dst s => match find_op_in_fmap fmap pc op args with | None => Iop op (subst_args fmap pc args) dst s - | Some src => gen_move src dst s + | Some src => Iop Omove (src::nil) dst s end | Iload chunk addr args dst s => Iload chunk addr (subst_args fmap pc args) dst s -- cgit From a7df9f6f48aa9282cb66b02bb63ca047b01f09b4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 15:01:39 +0100 Subject: still buggy --- backend/CSE2.v | 48 ++++++++++++++++++++++++++++-------------------- 1 file changed, 28 insertions(+), 20 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 5b850cbb..07bde1ac 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -275,24 +275,6 @@ Definition forward_move (rel : RELATION.t) (x : reg) : reg := Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). -Definition oper1 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - let rel' := kill_reg dst rel in - PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. - -Definition oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - if List.in_dec peq dst args - then kill_reg dst rel - else oper1 op dst args rel. - -Definition gen_oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - match op, args with - | Omove, src::nil => move src dst rel - | _, _ => oper op dst args rel - end. - Definition find_op_fold op args (already : option reg) x sv := match already with | Some found => already @@ -309,6 +291,31 @@ Definition find_op_fold op args (already : option reg) x sv := Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := PTree.fold (find_op_fold op args) rel None. +Definition oper2 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + let rel' := kill_reg dst rel in + PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. + +Definition oper1 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 op dst args rel. + +Definition oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match find_op rel op args with + | Some r => move r dst rel + | None => oper1 op dst args rel + end. + +Definition gen_oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match op, args with + | Omove, src::nil => move src dst rel + | _, _ => oper op dst args rel + end. + (* NO LONGER NEEDED Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := match l with @@ -392,8 +399,9 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => - match find_op_in_fmap fmap pc op args with - | None => Iop op (subst_args fmap pc args) dst s + let args' := subst_args fmap pc args in + match find_op_in_fmap fmap pc op args' with + | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end | Iload chunk addr args dst s => -- cgit From 3e15c72f5a5e34ac2e96e77022b2129125abcdd0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 15:24:11 +0100 Subject: much better - seems to eliminate CSE not containing loads --- backend/CSE2.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 07bde1ac..14c6e042 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -304,7 +304,7 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg) Definition oper (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := - match find_op rel op args with + match find_op rel op (List.map (forward_move rel) args) with | Some r => move r dst rel | None => oper1 op dst args rel end. -- cgit From 727c890d3174ec313961dd1b7e1b8726125450e9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 15:33:13 +0100 Subject: begin adding loads --- backend/CSE2.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 14c6e042..e07e7adc 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -6,8 +6,9 @@ Require Import Memory Registers Op RTL Maps. Inductive sym_val : Type := | SMove (src : reg) -| SOp (op : operation) (args : list reg). - +| SOp (op : operation) (args : list reg) +| SLoad (chunk : memory_chunk) (addr : addressing) (args : list reg). + Definition eq_args (x y : list reg) : { x = y } + { x <> y } := list_eq_dec peq x y. @@ -17,6 +18,8 @@ Proof. generalize eq_operation. generalize eq_args. generalize peq. + generalize eq_addressing. + generalize chunk_eq. decide equality. Defined. @@ -250,6 +253,7 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) := match sv with | SMove src => if peq dst src then true else false | SOp op args => List.existsb (peq dst) args + | SLoad chunk addr args => List.existsb (peq dst) args end. Definition kill_reg (dst : reg) (rel : RELATION.t) := @@ -260,6 +264,7 @@ Definition kill_sym_val_mem (sv: sym_val) := match sv with | SMove _ => false | SOp op _ => op_depends_on_memory op + | SLoad _ _ _ => true end. Definition kill_mem (rel : RELATION.t) := -- cgit From 3bdfc2288714f1c238a5b59586aa1409f4eda056 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 16:38:57 +0100 Subject: with loads too ? --- backend/CSE2.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 52 insertions(+), 2 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index e07e7adc..f1ed877a 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -296,6 +296,24 @@ Definition find_op_fold op args (already : option reg) x sv := Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := PTree.fold (find_op_fold op args) rel None. +Definition find_load_fold chunk addr args (already : option reg) x sv := + match already with + | Some found => already + | None => + match sv with + | (SLoad chunk' addr' args') => + if (chunk_eq chunk chunk') && + (eq_addressing addr addr') && + (eq_args args args') + then Some x + else None + | _ => None + end + end. + +Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) := + PTree.fold (find_load_fold chunk addr args) rel None. + Definition oper2 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := let rel' := kill_reg dst rel in @@ -321,6 +339,24 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg) | _, _ => oper op dst args rel end. +Definition load2 (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + let rel' := kill_reg dst rel in + PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'. + +Definition load1 (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + if List.in_dec peq dst args + then kill_reg dst rel + else load2 chunk addr dst args rel. + +Definition load (chunk: memory_chunk) (addr : addressing) + (dst : reg) (args : list reg) (rel : RELATION.t) := + match find_load rel chunk addr (List.map (forward_move rel) args) with + | Some r => move r dst rel + | None => load1 chunk addr dst args rel + end. + (* NO LONGER NEEDED Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := match l with @@ -355,7 +391,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Ijumptable _ _ => Some rel | Istore _ _ _ _ _ => Some (kill_mem rel) | Iop op args dst _ => Some (gen_oper op dst args rel) - | Iload _ _ _ dst _ => Some (kill_reg dst rel) + | Iload chunk addr args dst _ => Some (load chunk addr dst args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) | Itailcall _ _ _ | Ireturn _ => RB.bot @@ -400,6 +436,16 @@ Definition find_op_in_fmap fmap pc op args := end end. +Definition find_load_in_fmap fmap pc chunk addr args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => find_load rel chunk addr args + | None => None + end + end. + Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := match instr with @@ -410,7 +456,11 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) | Some src => Iop Omove (src::nil) dst s end | Iload chunk addr args dst s => - Iload chunk addr (subst_args fmap pc args) dst s + let args' := subst_args fmap pc args in + match find_load_in_fmap fmap pc chunk addr args' with + | None => Iload chunk addr args' dst s + | Some src => Iop Omove (src::nil) dst s + end | Istore chunk addr args src s => Istore chunk addr (subst_args fmap pc args) src s | Icall sig ros args dst s => -- cgit