diff options
| -rw-r--r-- | backend/CSE2.v | 54 | ||||
| -rw-r--r-- | 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. |