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 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(-) 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(-) 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(-) 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(+) 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(+) 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 --- Makefile | 1 + backend/CSE2.v | 829 +-------------------------------------------------- backend/CSE2proof.v | 835 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 838 insertions(+), 827 deletions(-) create mode 100644 backend/CSE2proof.v diff --git a/Makefile b/Makefile index 80eca80d..b8bde940 100644 --- a/Makefile +++ b/Makefile @@ -83,6 +83,7 @@ BACKEND=\ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ + CSE2.v CSE2proof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.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 diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v new file mode 100644 index 00000000..a14988a0 --- /dev/null +++ b/backend/CSE2proof.v @@ -0,0 +1,835 @@ +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. +Require Import CSE2. + +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. + 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. + + +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. + + +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. + *) + +End PRESERVATION. \ No newline at end of file -- cgit From a200d33d3751fad37620a22a9e4d33e0b88176c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 09:39:08 +0100 Subject: sem_rel_b_ge --- backend/CSE2proof.v | 95 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 77 insertions(+), 18 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index a14988a0..d9150658 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -438,7 +438,7 @@ 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 + | None => False end. Definition fmap_sem (fmap : option (PMap.t RB.t)) @@ -448,7 +448,66 @@ Definition fmap_sem (fmap : option (PMap.t RB.t)) | Some map => sem_rel_b (PMap.get pc map) sp m rs end. -(* +Definition is_killed_in_map (map : PMap.t RB.t) pc res := + match PMap.get pc map with + | None => True + | Some rel => exists rel', RELATION.ge rel (kill_reg res rel') + end. + +Definition is_killed_in_fmap fmap pc res := + match fmap with + | None => True + | Some map => is_killed_in_map map pc res + end. + + +Lemma sem_rel_b_ge: + forall rb1 rb2 : RB.t, + (RB.ge rb1 rb2) -> + forall sp m, + forall rs : regset, + (sem_rel_b rb2 sp m rs) -> (sem_rel_b rb1 sp m rs). +Proof. + unfold sem_rel_b, sem_rel, sem_reg. + destruct rb1 as [r1 | ]; + destruct rb2 as [r2 | ]; simpl; + intros GE sp m rs RE; try contradiction. + intro x. + pose proof (RE x) as REx. + pose proof (GE x) as GEx. + destruct (r1 ! x) as [r1x | ] in *; + destruct (r2 ! x) as [r2x | ] in *; + congruence. +Qed. + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + (forall m : mem, (fmap_sem (forward_map f) sp m pc rs)) -> + (is_killed_in_fmap (forward_map f) pc res) -> + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + (fmap_sem (forward_map f) sp m pc rs) -> + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + +Ltac TR_AT := + match goal with + | [ A: (fn_code _)!_ = Some _ |- _ ] => + generalize (transf_function_at _ _ _ A); intros + end. + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -462,7 +521,7 @@ Proof. 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. + apply sem_rel_b_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. @@ -470,7 +529,7 @@ Proof. simpl. tauto. } unfold apply_instr'. - unfold get_rb_sem in *. + unfold sem_rel_b in *. destruct (map # pc) in *; try contradiction. rewrite H. reflexivity. @@ -502,14 +561,14 @@ Proof. rewrite MOVE in GE. simpl in H0. simpl in GE. - apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). + apply sem_rel_b_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)). + apply sem_rel_b_ge with (rb2 := Some (kill res mpc)). assumption. apply kill_ok. assumption. @@ -527,7 +586,7 @@ Proof. 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)). + apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)). { replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -555,7 +614,7 @@ Proof. 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)). + apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)). { replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -583,7 +642,7 @@ Proof. 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)). + apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)). { replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -610,7 +669,7 @@ Proof. 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. + apply sem_rel_b_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. @@ -618,7 +677,7 @@ Proof. simpl. tauto. } unfold apply_instr'. - unfold get_rb_sem in *. + unfold sem_rel_b in *. destruct (map # pc) in *; try contradiction. rewrite H. reflexivity. @@ -636,7 +695,7 @@ Proof. 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)). + apply sem_rel_b_ge with (rb2 := Some (kill res mpc)). { replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -689,7 +748,7 @@ Proof. 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). + apply sem_rel_b_ge with (rb2 := Some RELATION.top). { replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). { @@ -713,7 +772,7 @@ Proof. 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. + apply sem_rel_b_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. @@ -722,7 +781,7 @@ Proof. destruct b; tauto. } unfold apply_instr'. - unfold get_rb_sem in *. + unfold sem_rel_b in *. destruct (map # pc) in *; try contradiction. rewrite H. reflexivity. @@ -736,7 +795,7 @@ Proof. 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. + apply sem_rel_b_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. @@ -746,7 +805,7 @@ Proof. assumption. } unfold apply_instr'. - unfold get_rb_sem in *. + unfold sem_rel_b in *. destruct (map # pc) in *; try contradiction. rewrite H. reflexivity. @@ -773,7 +832,7 @@ Proof. 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). + apply sem_rel_b_ge with (rb2 := Some RELATION.top). { eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. } -- cgit From 427fc1fb431b4200ac5e60981a4d570863e2539f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 11:16:38 +0100 Subject: sem_rel_b_ge progress --- backend/CSE2proof.v | 213 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 152 insertions(+), 61 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index d9150658..f2306d21 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -53,6 +53,57 @@ 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). +Definition sem_rel_b (relb : RB.t) (rs : regset) := + match relb with + | Some rel => sem_rel rel rs + | None => False + end. + +Definition fmap_sem (fmap : option (PMap.t RB.t)) + (pc : node) (rs : regset) := + match fmap with + | None => True + | Some m => sem_rel_b (PMap.get pc m) rs + end. + +Lemma subst_arg_ok: + forall f, + forall pc, + forall rs, + forall arg, + fmap_sem (forward_map f) pc rs -> + rs # (subst_arg (forward_map f) pc arg) = rs # arg. +Proof. + intros until arg. + intro SEM. + unfold fmap_sem in SEM. + destruct (forward_map f) as [map |]in *; trivial. + simpl. + unfold sem_rel_b, sem_rel, sem_reg in *. + destruct (map # pc). + 2: contradiction. + pose proof (SEM arg) as SEMarg. + simpl. unfold forward_move. + unfold sem_sym_val in *. + destruct (t ! arg); trivial. + destruct s; congruence. +Qed. + +Lemma subst_args_ok: + forall f, + forall pc, + forall rs, + fmap_sem (forward_map f) pc rs -> + forall args, + rs ## (subst_args (forward_map f) pc args) = rs ## args. +Proof. + induction args; trivial. + simpl. + f_equal. + apply subst_arg_ok; assumption. + assumption. +Qed. + Lemma kill_reg_sound : forall rel : RELATION.t, forall dst : reg, @@ -348,6 +399,27 @@ Proof. apply REC; auto. Qed. + +Lemma kill_reg_weaken: + forall res mpc rs, + sem_rel mpc rs -> + sem_rel (kill_reg res mpc) rs. +Proof. + Check kill_reg_sound. + intros until rs. + intros REL x. + pose proof (REL x) as RELx. + unfold kill_reg, sem_reg in *. + rewrite PTree.gfilter1. + destruct (peq res x). + { subst x. + rewrite PTree.grs. + reflexivity. + } + rewrite PTree.gro by congruence. + destruct (mpc ! x) as [sv | ]; trivial. + destruct negb; trivial. +Qed. End SAME_MEMORY. Lemma kill_mem_sound : @@ -435,19 +507,6 @@ Proof. 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 => False - 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. - Definition is_killed_in_map (map : PMap.t RB.t) pc res := match PMap.get pc map with | None => True @@ -460,15 +519,19 @@ Definition is_killed_in_fmap fmap pc res := | Some map => is_killed_in_map map pc res end. +Definition sem_rel_b' := sem_rel_b fundef unit ge. +Definition fmap_sem' := fmap_sem fundef unit ge. +Definition subst_args_ok' := subst_args_ok fundef unit ge. +Definition kill_mem_sound' := kill_mem_sound fundef unit ge. Lemma sem_rel_b_ge: forall rb1 rb2 : RB.t, (RB.ge rb1 rb2) -> forall sp m, forall rs : regset, - (sem_rel_b rb2 sp m rs) -> (sem_rel_b rb1 sp m rs). + (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs). Proof. - unfold sem_rel_b, sem_rel, sem_reg. + unfold sem_rel_b', sem_rel_b, sem_rel, sem_reg. destruct rb1 as [r1 | ]; destruct rb2 as [r2 | ]; simpl; intros GE sp m rs RE; try contradiction. @@ -480,9 +543,17 @@ Proof. congruence. Qed. +Lemma apply_instr'_bot : + forall code, + forall pc, + RB.eq (apply_instr' code pc RB.bot) RB.bot. +Proof. + reflexivity. +Qed. + Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := | match_frames_intro: forall res f sp pc rs, - (forall m : mem, (fmap_sem (forward_map f) sp m pc rs)) -> + (forall m : mem, (fmap_sem' sp m (forward_map f) pc rs)) -> (is_killed_in_fmap (forward_map f) pc res) -> match_frames (Stackframe res f sp pc rs) (Stackframe res (transf_function f) sp pc rs). @@ -490,7 +561,7 @@ Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := Inductive match_states: RTL.state -> RTL.state -> Prop := | match_regular_states: forall stk f sp pc rs m stk' (STACKS: list_forall2 match_frames stk stk'), - (fmap_sem (forward_map f) sp m pc rs) -> + (fmap_sem' sp m (forward_map f) pc rs) -> match_states (State stk f sp pc rs m) (State stk' (transf_function f) sp pc rs m) | match_callstates: forall stk f args m stk' @@ -519,7 +590,7 @@ Proof. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. apply sem_rel_b_ge with (rb2 := map # pc); trivial. replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). @@ -534,6 +605,7 @@ Proof. rewrite H. reflexivity. - (* op *) + (* econstructor; split. eapply exec_Iop with (v := v); eauto. rewrite <- H0. @@ -572,23 +644,24 @@ Proof. assumption. apply kill_ok. assumption. - + *) + admit. (* 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. + rewrite (subst_args_ok' sp m); assumption. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)). + apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)). { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_reg 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. @@ -599,9 +672,10 @@ Proof. rewrite MPC. reflexivity. } - apply kill_ok. + apply kill_reg_sound. assumption. - + + (* NOT IN THIS VERSION - (* load notrap1 *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = None). @@ -657,20 +731,25 @@ Proof. } 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. + 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' sp m); assumption. + } + constructor; auto. - simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply sem_rel_b_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial. + { + replace (Some (kill_mem 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. @@ -678,39 +757,47 @@ Proof. } unfold apply_instr'. unfold sem_rel_b in *. - destruct (map # pc) in *; try contradiction. + rewrite MPC. rewrite H. reflexivity. + } + apply (kill_mem_sound' sp m). + assumption. (* 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. + rewrite (subst_args_ok' sp m) 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 sem_rel_b_ge with (rb2 := Some (kill res mpc)). - { - replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + intro m'. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (kill_reg res (kill_mem mpc))). { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + replace (Some (kill_reg res (kill_mem 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. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_weaken. - assumption. + apply kill_reg_weaken. + apply (kill_mem_sound' sp m). + assumption. } + { + simpl in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. { @@ -719,23 +806,27 @@ Proof. 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. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. unfold is_killed_in_fmap, is_killed_in_map. - unfold RB.ge in GE. - destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial. - eauto. + destruct (map # pc') as [mpc' |] eqn:MPC' ; try contradiction. + + exists (kill_mem mpc). + assumption. + } (* 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. + Check subst_args_ok. + rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. constructor. auto. - + + (* TODO *) + (* builtin *) - econstructor; split. eapply exec_Ibuiltin; eauto. -- cgit From e974c5a24dcc80ecb4e61725bb5131570bc447fc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 12:11:42 +0100 Subject: rework --- backend/CSE2proof.v | 69 +++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 49 insertions(+), 20 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index f2306d21..ad11a8e9 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -420,6 +420,30 @@ Proof. destruct (mpc ! x) as [sv | ]; trivial. destruct negb; trivial. Qed. + +Lemma top_ok: + forall rs, sem_rel RELATION.top rs. +Proof. + unfold sem_rel, sem_reg, RELATION.top. + intros. + rewrite PTree.gempty. + reflexivity. +Qed. + +Lemma sem_rel_ge: + forall r1 r2 : RELATION.t, + (RELATION.ge r1 r2) -> + forall rs : regset, + (sem_rel r2 rs) -> (sem_rel r1 rs). +Proof. + intros r1 r2 GE rs RE x. + pose proof (RE x) as REx. + pose proof (GE x) as GEx. + unfold sem_reg in *. + destruct (r1 ! x) as [r1x | ] in *; + destruct (r2 ! x) as [r2x | ] in *; + congruence. +Qed. End SAME_MEMORY. Lemma kill_mem_sound : @@ -444,7 +468,7 @@ Proof. apply op_depends_on_memory_correct; auto. } Qed. - + End SOUNDNESS. @@ -521,6 +545,7 @@ Definition is_killed_in_fmap fmap pc res := Definition sem_rel_b' := sem_rel_b fundef unit ge. Definition fmap_sem' := fmap_sem fundef unit ge. +Definition subst_arg_ok' := subst_arg_ok fundef unit ge. Definition subst_args_ok' := subst_args_ok fundef unit ge. Definition kill_mem_sound' := kill_mem_sound fundef unit ge. @@ -531,16 +556,11 @@ Lemma sem_rel_b_ge: forall rs : regset, (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs). Proof. - unfold sem_rel_b', sem_rel_b, sem_rel, sem_reg. + unfold sem_rel_b', sem_rel_b. destruct rb1 as [r1 | ]; destruct rb2 as [r2 | ]; simpl; intros GE sp m rs RE; try contradiction. - intro x. - pose proof (RE x) as REx. - pose proof (GE x) as GEx. - destruct (r1 ! x) as [r1x | ] in *; - destruct (r2 ! x) as [r2x | ] in *; - congruence. + apply sem_rel_ge with (r2 := r2); assumption. Qed. Lemma apply_instr'_bot : @@ -825,8 +845,6 @@ Proof. rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. constructor. auto. - (* TODO *) - (* builtin *) - econstructor; split. eapply exec_Ibuiltin; eauto. @@ -835,7 +853,7 @@ Proof. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. @@ -854,14 +872,15 @@ Proof. } apply top_ok. + (* cond *) - econstructor; split. eapply exec_Icond; eauto. - rewrite subst_args_ok; eassumption. + rewrite (subst_args_ok' sp m); eassumption. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. apply sem_rel_b_ge with (rb2 := map # pc); trivial. replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). @@ -876,15 +895,15 @@ Proof. destruct (map # pc) in *; try contradiction. rewrite H. reflexivity. - + (* jumptbl *) - econstructor; split. eapply exec_Ijumptable; eauto. - rewrite subst_arg_ok; eassumption. + rewrite (subst_arg_ok' sp m); eassumption. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. apply sem_rel_b_ge with (rb2 := map # pc); trivial. replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). @@ -907,7 +926,7 @@ Proof. econstructor; split. eapply exec_Ireturn; eauto. unfold regmap_optget. - rewrite subst_arg_ok by eassumption. + rewrite (subst_arg_ok' (Vptr stk Ptrofs.zero) m) by eassumption. constructor; auto. } econstructor; split. @@ -921,7 +940,7 @@ Proof. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. apply sem_rel_b_ge with (rb2 := Some RELATION.top). { @@ -942,12 +961,22 @@ Proof. constructor; auto. simpl in *. - unfold fmap_sem in *. + unfold fmap_sem', 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 (map # pc) as [mpc |] in *; simpl in *; auto. destruct H8 as [rel' RGE]. + + (* WRONG *) + eapply sem_rel_ge. exact RGE. + apply kill_reg_sound. + assert (sem_rel fundef unit ge sp m (kill_reg res rel') rs # res <- vres). + { + + eapply sem_rel_ge. eassumption. + } + eapply kill_reg_sound. eapply get_rb_killed; eauto. Qed. -- cgit From 76049f12161c0eeeeec8841d2cc07d6601f39b4f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 12:14:55 +0100 Subject: now going back to op --- backend/CSE2proof.v | 51 ++++++--------------------------------------------- 1 file changed, 6 insertions(+), 45 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index ad11a8e9..8e7d7b3b 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -573,9 +573,9 @@ Qed. Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := | match_frames_intro: forall res f sp pc rs, - (forall m : mem, (fmap_sem' sp m (forward_map f) pc rs)) -> - (is_killed_in_fmap (forward_map f) pc res) -> - match_frames (Stackframe res f sp pc rs) + (forall m : mem, + forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) -> + match_frames (Stackframe res f sp pc rs) (Stackframe res (transf_function f) sp pc rs). Inductive match_states: RTL.state -> RTL.state -> Prop := @@ -794,7 +794,7 @@ Proof. constructor. { - intro m'. + intros m' vres. unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. @@ -811,30 +811,10 @@ Proof. rewrite MPC. reflexivity. } - apply kill_reg_weaken. + apply kill_reg_sound. apply (kill_mem_sound' sp m). assumption. } - { - simpl in *. - unfold fmap_sem', fmap_sem in *. - 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. - rewrite H in GE. - simpl in GE. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - unfold is_killed_in_fmap, is_killed_in_map. - destruct (map # pc') as [mpc' |] eqn:MPC' ; try contradiction. - - exists (kill_mem mpc). - assumption. - } (* tailcall *) - econstructor; split. @@ -959,26 +939,7 @@ Proof. econstructor; split. eapply exec_return; eauto. constructor; auto. - - simpl in *. - unfold fmap_sem', 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 *; simpl in *; auto. - destruct H8 as [rel' RGE]. - - (* WRONG *) - eapply sem_rel_ge. exact RGE. - apply kill_reg_sound. - assert (sem_rel fundef unit ge sp m (kill_reg res rel') rs # res <- vres). - { - - eapply sem_rel_ge. eassumption. - } - eapply kill_reg_sound. - eapply get_rb_killed; eauto. -Qed. +Admitted. Lemma transf_initial_states: -- 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 ++---- backend/CSE2proof.v | 105 +++++++++++++++++++++++++++++++++------------------- 2 files changed, 69 insertions(+), 47 deletions(-) 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 diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 8e7d7b3b..558490ba 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -335,7 +335,7 @@ Qed. Lemma find_op_sound : forall rel : RELATION.t, forall op : operation, - forall src dst : reg, + forall src : reg, forall args: list reg, forall rs : regset, sem_rel rel rs -> @@ -625,47 +625,75 @@ Proof. 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. + unfold transf_instr in *. + destruct find_op_in_fmap eqn:FIND_OP. { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + unfold find_op_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + simpl. + rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. + assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)). + { + replace (Some (gen_oper op res args 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. + } + unfold sem_rel_b', sem_rel_b. + apply gen_oper_sound; auto. } - 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 sem_rel_b_ge with (rb2 := Some (move src res mpc)). - assumption. - replace v with (rs # src) by congruence. - apply move_ok. - assumption. + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + rewrite (subst_args_ok' sp m) by assumption. + rewrite <- H0. + apply eval_operation_preserved. exact symbols_preserved. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + unfold find_op_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: constructor. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: contradiction. + + apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)). + { + replace (Some (gen_oper op res args 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. + } + unfold sem_rel_b', sem_rel_b. + apply gen_oper_sound; auto. } - rewrite KILL in GE. - apply sem_rel_b_ge with (rb2 := Some (kill res mpc)). - assumption. - apply kill_ok. - assumption. - *) - admit. + (* load *) - econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). @@ -970,6 +998,5 @@ Proof. eexact transf_final_states. exact step_simulation. Qed. - *) End PRESERVATION. \ No newline at end of file -- cgit From 5412aea57eafe2868244a514471d480b83fc51bd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 13:59:55 +0100 Subject: connected (just a silly problem) --- backend/CSE2proof.v | 10 ++++++++-- driver/Clflags.ml | 1 + driver/Compiler.v | 36 ++++++++++++++++++++++++++++++++---- driver/Compopts.v | 3 +++ driver/Driver.ml | 7 +++++-- extraction/extraction.v | 2 ++ 6 files changed, 51 insertions(+), 8 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 558490ba..1d0a617a 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -405,7 +405,6 @@ Lemma kill_reg_weaken: sem_rel mpc rs -> sem_rel (kill_reg res mpc) rs. Proof. - Check kill_reg_sound. intros until rs. intros REL x. pose proof (REL x) as RELx. @@ -471,6 +470,14 @@ Qed. End SOUNDNESS. +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +Qed. Section PRESERVATION. @@ -849,7 +856,6 @@ Proof. eapply exec_Itailcall with (fd := transf_fundef fd); eauto. eapply find_function_translated; eauto. apply sig_preserved. - Check subst_args_ok. rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. constructor. auto. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..b4ab51e7 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true +let option_fcse2 = ref true let option_fredundancy = ref true let option_fifconversion = ref true let option_Obranchless = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..33e31057 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -40,6 +40,7 @@ Require Inlining. Require Renumber. Require Constprop. Require CSE. +Require CSE2. Require Deadcode. Require Unusedglob. Require Allocation. @@ -61,6 +62,7 @@ Require Inliningproof. Require Renumberproof. Require Constpropproof. Require CSEproof. +Require CSE2proof. Require Deadcodeproof. Require Unusedglobproof. Require Allocproof. @@ -132,10 +134,12 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -241,6 +245,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog @@ -284,7 +289,27 @@ Proof. set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12). + change (@eq (res Asm.program) + (apply_partial Mach.program Asm.program + (apply_partial Linear.program Mach.program + (apply_partial Linear.program Linear.program + (apply_total Linear.program Linear.program + (apply_partial LTL.program Linear.program + (apply_total LTL.program LTL.program + (apply_partial RTL.program LTL.program + (apply_partial RTL.program RTL.program + (@partial_if RTL.program optim_redundancy + Deadcode.transf_program + p12bis) + Unusedglob.transform_program) + Allocation.transf_program) + Tunneling.tunnel_program) Linearize.transf_program) + CleanupLabels.transf_program) + (@partial_if Linear.program debug Debugvar.transf_program)) + Stacking.transf_program) Asmgen.transf_program) + (@OK Asm.program tp)) in T. + destruct (partial_if optim_redundancy Deadcode.transf_program p12bis) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. @@ -305,6 +330,7 @@ Proof. exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p12bis; split. apply total_if_match. apply CSE2proof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. exists p15; split. apply Allocproof.transf_program_match; auto. @@ -364,7 +390,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -389,6 +415,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 2a213350..594b74f1 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -36,6 +36,9 @@ Parameter optim_constprop: unit -> bool. (** Flag -fcse. For common subexpression elimination. *) Parameter optim_CSE: unit -> bool. +(** Flag -fcse2. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE2: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index be1252f9..bdf72250 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) -fcse Perform common subexpression elimination [on] + -fcse2 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -253,8 +254,9 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; - option_fredundancy; option_finline; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; + option_fcse; option_fcse2; + option_fredundancy; option_finline; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -372,6 +374,7 @@ let cmdline_actions = @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse + @ f_opt "cse2" option_fcse2 @ f_opt "redundancy" option_fredundancy @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once diff --git a/extraction/extraction.v b/extraction/extraction.v index 521c0cdd..4635f5a2 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -108,6 +108,8 @@ Extract Constant Compopts.optim_constprop => "fun _ -> !Clflags.option_fconstprop". Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". +Extract Constant Compopts.optim_CSE2 => + "fun _ -> !Clflags.option_fcse2". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.thumb => -- 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 ++++++++++++++---------- backend/CSE2proof.v | 103 ++++++++++++++++++++++++++++++++++------------------ 2 files changed, 95 insertions(+), 56 deletions(-) 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 => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 1d0a617a..47b60902 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -249,7 +249,7 @@ Proof. destruct s; simpl in *; destruct negb; simpl; congruence. Qed. -Lemma oper1_sound : +Lemma oper2_sound : forall rel : RELATION.t, forall op : operation, forall dst : reg, @@ -259,12 +259,12 @@ Lemma oper1_sound : 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). + sem_rel (oper2 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. + unfold oper2. destruct (peq x dst). { subst x. @@ -282,7 +282,7 @@ Proof. exact KILL. Qed. -Lemma oper_sound : +Lemma oper1_sound : forall rel : RELATION.t, forall op : operation, forall dst : reg, @@ -291,45 +291,18 @@ Lemma oper_sound : 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). + sem_rel (oper1 op dst args rel) (rs # dst <- v). Proof. intros until v. intros REL EVAL. - unfold oper. + unfold oper1. destruct in_dec. { apply kill_reg_sound; auto. } - apply oper1_sound; auto. + apply oper2_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. Lemma find_op_sound : @@ -399,6 +372,59 @@ Proof. apply REC; auto. 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 find_op eqn:FIND. + { + assert (eval_operation genv sp op rs ## args m = Some rs # r). + { + apply (find_op_sound rel); trivial. + } + replace v with (rs # r) by congruence. + apply move_sound; auto. + } + apply oper1_sound; trivial. +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. Lemma kill_reg_weaken: forall res mpc rs, @@ -645,8 +671,13 @@ Proof. { eapply exec_Iop with (v := v); eauto. simpl. - rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. - assumption. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + rewrite MAP in H0. + rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } constructor; eauto. unfold fmap_sem', fmap_sem in *. -- 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 +- backend/CSE2proof.v | 18 +++++++++++++++++- 2 files changed, 18 insertions(+), 2 deletions(-) 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. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 47b60902..049423b0 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -372,6 +372,21 @@ Proof. apply REC; auto. Qed. +Lemma forward_move_map: + forall rel args rs, + sem_rel rel rs -> + rs ## (map (forward_move rel) args) = rs ## args. +Proof. + induction args; simpl; trivial. + intros rs REL. + f_equal. + 2: (apply IHargs; assumption). + unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. + pose proof (REL a) as RELa. + destruct (rel ! a); trivial. + destruct s; congruence. +Qed. + Lemma oper_sound : forall rel : RELATION.t, forall op : operation, @@ -388,10 +403,11 @@ Proof. unfold oper. destruct find_op eqn:FIND. { - assert (eval_operation genv sp op rs ## args m = Some rs # r). + assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP. { apply (find_op_sound rel); trivial. } + rewrite forward_move_map in FIND_OP by assumption. replace v with (rs # r) by congruence. apply move_sound; auto. } -- 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(-) 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 4414da3d406685a05ae20ba8994c1a9247137874 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 15:58:25 +0100 Subject: find_load_sound --- backend/CSE2proof.v | 96 ++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 92 insertions(+), 4 deletions(-) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 049423b0..796f3054 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -42,6 +42,11 @@ Definition sem_sym_val sym rs := | SMove src => Some (rs # src) | SOp op args => eval_operation genv sp op (rs ## args) m + | SLoad chunk addr args => + match eval_addressing genv sp addr rs##args with + | Some a => Mem.loadv chunk m a + | None => None + end end. Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := @@ -142,6 +147,11 @@ Proof. rewrite args_unaffected by exact EXISTS. assumption. } + { destruct existsb eqn:EXISTS; simpl. + { reflexivity. } + rewrite args_unaffected by exact EXISTS. + assumption. + } Qed. Lemma write_same: @@ -303,8 +313,6 @@ Proof. apply oper2_sound; auto. Qed. - - Lemma find_op_sound : forall rel : RELATION.t, forall op : operation, @@ -351,8 +359,7 @@ Proof. unfold find_op_fold. destruct start. assumption. - destruct sv. - { trivial. } + destruct sv; trivial. destruct eq_operation; trivial. subst op0. destruct eq_args; trivial. @@ -372,6 +379,87 @@ Proof. apply REC; auto. Qed. +Lemma find_load_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + match eval_addressing genv sp addr rs##args with + | Some a => (Mem.loadv chunk m a) = Some (rs # src) + | None => True + end. +Proof. + intros until rs. + unfold find_load. + rewrite PTree.fold_spec. + intro REL. + assert ( + forall start, + match start with + | None => True + | Some src => + match eval_addressing genv sp addr rs##args with + | Some a => (Mem.loadv chunk m a) = Some (rs # src) + | None => True + end + end -> + fold_left + (fun (a : option reg) (p : positive * sym_val) => + find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start = + Some src -> + match eval_addressing genv sp addr rs##args with + | Some a => (Mem.loadv chunk m a) = Some (rs # src) + | None => True + end ) 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_load_fold. + destruct start. + assumption. + destruct sv; trivial. + destruct chunk_eq; trivial. + subst chunk0. + destruct eq_addressing; trivial. + subst addr0. + destruct eq_args; trivial. + subst args0. + simpl. + assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr. + { + apply COMPLETE. + left. + reflexivity. + } + pose proof (REL r) as RELr. + rewrite RELatr in RELr. + simpl in RELr. + destruct eval_addressing; trivial. + } + apply REC; auto. +Qed. + Lemma forward_move_map: forall rel args rs, sem_rel rel rs -> -- cgit From 2bcac2e8c00493555fb0fb1acd730bab53eb7369 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 16:12:52 +0100 Subject: load_sound --- backend/CSE2proof.v | 96 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 796f3054..5cb85fc2 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -530,6 +530,102 @@ Proof. all: apply oper_sound; auto. Qed. + +Lemma load2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL NOT_IN ADDR LOAD x. + pose proof (kill_reg_sound rel dst rs v REL x) as KILL. + unfold load2. + destruct (peq x dst). + { + subst x. + unfold sem_reg. + rewrite PTree.gss. + rewrite Regmap.gss. + simpl. + rewrite args_replace_dst by auto. + destruct eval_addressing; congruence. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_sound with (a := a); auto. +Qed. + +Lemma load_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + forall v, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rel (load chunk addr dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL ADDR LOAD. + unfold load. + destruct find_load eqn:FIND. + { + assert (match eval_addressing genv sp addr rs##(map (forward_move rel) args) with + | Some a => (Mem.loadv chunk m a) = Some (rs # r) + | None => True + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + destruct eval_addressing in *. + 2: discriminate. + replace v with (rs # r) by congruence. + apply move_sound; auto. + } + apply load1_sound with (a := a); trivial. +Qed. + Lemma kill_reg_weaken: forall res mpc rs, sem_rel mpc rs -> -- 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 +++++++++++++++++++++++++++++++++++++-- backend/CSE2proof.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 119 insertions(+), 8 deletions(-) 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 => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 5cb85fc2..fe2ade4b 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -460,6 +460,24 @@ Proof. apply REC; auto. Qed. +Lemma find_load_sound' : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall src : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + find_load rel chunk addr args = Some src -> + eval_addressing genv sp addr rs##args = Some a -> + (Mem.loadv chunk m a) = Some (rs # src). +Proof. + intros until a. intros REL LOAD ADDR. + pose proof (find_load_sound rel chunk addr src args rs REL LOAD) as Z. + destruct eval_addressing in *; congruence. +Qed. + Lemma forward_move_map: forall rel args rs, sem_rel rel rs -> @@ -933,7 +951,49 @@ Proof. } (* load *) -- econstructor; split. +- unfold transf_instr in *. + destruct find_load_in_fmap eqn:FIND_LOAD. + { + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := v); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + rewrite find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs) in H1; trivial. + rewrite MAP in H0. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args 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. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_sound with (a := a); auto. + } + { + econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. @@ -945,9 +1005,9 @@ Proof. unfold fmap_sem', fmap_sem in *. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)). + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). { - replace (Some (kill_reg dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (load chunk addr dst args 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. @@ -956,11 +1016,12 @@ Proof. unfold apply_instr'. rewrite H. rewrite MPC. + simpl. reflexivity. } - apply kill_reg_sound. - assumption. - + apply load_sound with (a := a); assumption. + } + (* NOT IN THIS VERSION - (* load notrap1 *) econstructor; split. -- cgit