From 3fde34d48925db4153c5c288fa37da35725502ce Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 4 Feb 2020 09:14:25 +0100 Subject: stuff information into a record --- backend/CSE2.v | 59 ++++++++++++++++++++++++++++++----------------------- backend/CSE2proof.v | 50 +++++++++++++++++++++++++++------------------ 2 files changed, 63 insertions(+), 46 deletions(-) diff --git a/backend/CSE2.v b/backend/CSE2.v index b7665097..0479dad9 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -29,13 +29,18 @@ Proof. decide equality. Defined. +Record relmap := mkrel { + var_to_sym : (PTree.t sym_val) + }. + Module RELATION. - -Definition t := (PTree.t sym_val). + +Definition t := relmap. + Definition eq (r1 r2 : t) := - forall x, (PTree.get x r1) = (PTree.get x r2). + forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)). -Definition top : t := PTree.empty sym_val. +Definition top : t := mkrel (PTree.empty sym_val). Lemma eq_refl: forall x, eq x x. Proof. @@ -58,27 +63,27 @@ 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. +Definition beq (r1 r2 : t) := PTree.beq sym_val_beq (var_to_sym r1) (var_to_sym 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. + pose proof (PTree.beq_correct sym_val_beq (var_to_sym r1) (var_to_sym 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 *; + destruct ((var_to_sym r1) ! x) as [R1x | ] in *; + destruct ((var_to_sym 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 + match PTree.get x (var_to_sym r1) with | None => True - | Some v => (PTree.get x r2) = Some v + | Some v => (PTree.get x (var_to_sym r2)) = Some v end. Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2. @@ -87,7 +92,7 @@ Proof. intros r1 r2 EQ x. pose proof (EQ x) as EQx. clear EQ. - destruct (r1 ! x). + destruct ((var_to_sym r1) ! x). - congruence. - trivial. Qed. @@ -98,12 +103,13 @@ Proof. 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. + destruct ((var_to_sym r1) ! x); trivial. + destruct ((var_to_sym r2) ! x); congruence. Qed. Definition lub (r1 r2 : t) := - PTree.combine + mkrel + (PTree.combine (fun ov1 ov2 => match ov1, ov2 with | (Some v1), (Some v2) => @@ -113,12 +119,12 @@ Definition lub (r1 r2 : t) := | None, _ | _, None => None end) - r1 r2. + (var_to_sym r1) (var_to_sym r2)). Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold ge, lub. - intros r1 r2 x. + intros r1 r2 x. simpl. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -128,7 +134,7 @@ Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. unfold ge, lub. - intros r1 r2 x. + intros r1 r2 x. simpl. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -263,8 +269,8 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) := end. Definition kill_reg (dst : reg) (rel : RELATION.t) := - PTree.filter1 (fun x => negb (kill_sym_val dst x)) - (PTree.remove dst rel). + mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) + (PTree.remove dst (var_to_sym rel))). Definition kill_sym_val_mem (sv: sym_val) := match sv with @@ -274,17 +280,18 @@ Definition kill_sym_val_mem (sv: sym_val) := end. Definition kill_mem (rel : RELATION.t) := - PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. + mkrel + (PTree.filter1 (fun x => negb (kill_sym_val_mem x)) (var_to_sym rel)). Definition forward_move (rel : RELATION.t) (x : reg) : reg := - match rel ! x with + match (var_to_sym rel) ! x with | Some (SMove org) => org | _ => x end. Definition move (src dst : reg) (rel : RELATION.t) := - PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). + mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym (kill_reg dst rel))). Definition find_op_fold op args (already : option reg) x sv := match already with @@ -300,7 +307,7 @@ Definition find_op_fold op args (already : option reg) x sv := end. Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := - PTree.fold (find_op_fold op args) rel None. + PTree.fold (find_op_fold op args) (var_to_sym rel) None. Definition find_load_fold chunk addr args (already : option reg) x sv := match already with @@ -318,12 +325,12 @@ Definition find_load_fold chunk addr args (already : option reg) x sv := 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. + PTree.fold (find_load_fold chunk addr args) (var_to_sym 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'. + mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')). Definition oper1 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := @@ -348,7 +355,7 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg) 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'. + mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')). Definition load1 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) := diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 82fa8a28..a29bf202 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -58,7 +58,7 @@ Definition sem_sym_val sym rs (v : option val) : Prop := end. Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop := - match rel ! x with + match (var_to_sym rel) ! x with | None => True | Some sym => sem_sym_val sym rs (Some (rs # x)) end. @@ -98,7 +98,7 @@ Proof. pose proof (SEM arg) as SEMarg. simpl. unfold forward_move. unfold sem_sym_val in *. - destruct (t ! arg); trivial. + destruct (_ ! arg); trivial. destruct s; congruence. Qed. @@ -127,7 +127,7 @@ Lemma kill_reg_sound : Proof. unfold sem_rel, kill_reg, sem_reg, sem_sym_val. intros until v. - intros REL x. + intros REL x. simpl. rewrite PTree.gfilter1. destruct (Pos.eq_dec dst x). { @@ -137,7 +137,7 @@ Proof. } rewrite PTree.gro by congruence. rewrite Regmap.gso by congruence. - destruct (rel ! x) as [relx | ] eqn:RELx; trivial. + destruct (_ ! x) as [relx | ] eqn:RELx; trivial. unfold kill_sym_val. pose proof (REL x) as RELinstx. rewrite RELx in RELinstx. @@ -190,12 +190,13 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. unfold sem_reg in *. simpl. unfold forward_move. - destruct (rel ! src) as [ sv |]; simpl. + destruct (_ ! src) as [ sv |]; simpl. destruct sv eqn:SV; simpl in *. { destruct (peq dst src0). @@ -211,6 +212,7 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -223,9 +225,10 @@ Lemma move_cases_neq: Proof. intros until a. intro NEQ. unfold kill_reg, forward_move. + simpl. rewrite PTree.gfilter1. rewrite PTree.gro by congruence. - destruct (rel ! a); simpl. + destruct (_ ! a); simpl. 2: congruence. destruct s. { @@ -259,9 +262,10 @@ Proof. unfold kill_reg. unfold sem_reg in RELa. unfold forward_move. + simpl. rewrite PTree.gfilter1. rewrite PTree.gro by auto. - destruct (rel ! a); simpl; trivial. + destruct (_ ! a); simpl; trivial. destruct s; simpl in *; destruct negb; simpl; congruence. Qed. @@ -285,6 +289,7 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -294,6 +299,7 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -341,13 +347,13 @@ Proof. | 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 = + find_op_fold op args a (fst p) (snd p)) (PTree.elements (var_to_sym 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). + generalize (PTree.elements_complete (var_to_sym rel)). + generalize (PTree.elements (var_to_sym rel)). induction l; simpl. { intros. @@ -372,7 +378,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert ((rel ! r) = Some (SOp op args)) as RELatr. + assert (((var_to_sym rel) ! r) = Some (SOp op args)) as RELatr. { apply COMPLETE. left. @@ -417,7 +423,7 @@ Proof. 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 = + find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start = Some src -> match eval_addressing genv sp addr rs##args with | Some a => (Mem.loadv chunk m a) = Some (rs # src) @@ -426,8 +432,8 @@ Proof. { unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete rel). - generalize (PTree.elements rel). + generalize (PTree.elements_complete (var_to_sym rel)). + generalize (PTree.elements (var_to_sym rel)). induction l; simpl. { intros. @@ -454,7 +460,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr. + assert (((var_to_sym rel) ! r) = Some (SLoad chunk addr args)) as RELatr. { apply COMPLETE. left. @@ -497,7 +503,7 @@ Proof. 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 (_ ! a); trivial. destruct s; congruence. Qed. @@ -580,6 +586,7 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -588,6 +595,7 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -661,6 +669,7 @@ Proof. intros REL x. pose proof (REL x) as RELx. unfold kill_reg, sem_reg in *. + simpl. rewrite PTree.gfilter1. destruct (peq res x). { subst x. @@ -668,7 +677,7 @@ Proof. reflexivity. } rewrite PTree.gro by congruence. - destruct (mpc ! x) as [sv | ]; trivial. + destruct (_ ! x) as [sv | ]; trivial. destruct negb; trivial. Qed. @@ -691,8 +700,8 @@ Proof. 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 *; + destruct ((var_to_sym r1) ! x) as [r1x | ] in *; + destruct ((var_to_sym r2) ! x) as [r2x | ] in *; congruence. Qed. End SAME_MEMORY. @@ -708,9 +717,10 @@ Proof. intros SEM x. pose proof (SEM x) as SEMx. unfold kill_mem. + simpl. rewrite PTree.gfilter1. unfold kill_sym_val_mem. - destruct (rel ! x) as [ sv | ]. + destruct ((var_to_sym rel) ! x) as [ sv | ]. 2: reflexivity. destruct sv; simpl in *; trivial. { -- cgit