diff options
Diffstat (limited to 'backend/CSE2proof.v')
-rw-r--r-- | backend/CSE2proof.v | 453 |
1 files changed, 404 insertions, 49 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 09490c4d..7e1dd430 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -53,8 +53,11 @@ Definition sem_sym_val sym rs (v : option val) : Prop := v = (eval_operation genv sp op (rs ## args) m) | SLoad chunk addr args => match eval_addressing genv sp addr rs##args with - | Some a => v = (Mem.loadv chunk m a) - | None => v = None \/ v = Some Vundef + | Some a => match Mem.loadv chunk m a with + | Some dat => v = Some dat + | None => v = None \/ v = Some (default_notrap_load_value chunk) + end + | None => v = None \/ v = Some (default_notrap_load_value chunk) end end. @@ -388,6 +391,7 @@ Proof. apply REC; auto. Qed. + Lemma find_load_sound : forall rel : RELATION.t, forall chunk : memory_chunk, @@ -398,8 +402,11 @@ Lemma find_load_sound : 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 + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk end. Proof. intros until rs. @@ -412,18 +419,24 @@ Proof. | 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 + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + 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. + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as REC. { unfold sem_rel, sem_reg in REL. @@ -464,11 +477,17 @@ Proof. pose proof (REL r) as RELr. rewrite RELatr in RELr. simpl in RELr. - destruct eval_addressing; congruence. + destruct eval_addressing. + { destruct Mem.loadv. + congruence. + destruct RELr; congruence. + } + destruct RELr; congruence. } apply REC; auto. Qed. + Lemma find_load_sound' : forall rel : RELATION.t, forall chunk : memory_chunk, @@ -477,14 +496,61 @@ Lemma find_load_sound' : forall args: list reg, forall rs : regset, forall a, + forall v, + 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 v -> + v = rs # src. +Proof. + intros until v. intros REL FINDLOAD ADDR LOAD. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + destruct eval_addressing in *. + { + replace a with v0 in * by congruence. + destruct Mem.loadv in * ; congruence. + } + discriminate. +Qed. + +Lemma find_load_notrap1_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 -> + eval_addressing genv sp addr rs##args = None -> + rs # src = (default_notrap_load_value chunk). +Proof. + intros until rs. intros REL FINDLOAD ADDR. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + rewrite ADDR in Z. + assumption. +Qed. + +Lemma find_load_notrap2_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). + Mem.loadv chunk m a = None -> + rs # src = (default_notrap_load_value chunk). 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. + intros until a. intros REL FINDLOAD ADDR LOAD. + pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z. + rewrite ADDR in Z. + destruct Mem.loadv. + discriminate. + assumption. Qed. Lemma forward_move_map: @@ -599,7 +665,84 @@ Proof. rewrite Regmap.gss. simpl. rewrite args_replace_dst by auto. - destruct eval_addressing; congruence. + destruct eval_addressing. + { + replace a with v0 in * by congruence. + destruct Mem.loadv; congruence. + } + discriminate. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load2_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL NOT_IN ADDR x. + pose proof (kill_reg_sound rel dst rs (default_notrap_load_value chunk) 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. + rewrite ADDR. + right. + trivial. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + +Lemma load2_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + not (In dst args) -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load2 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL NOT_IN ADDR LOAD x. + pose proof (kill_reg_sound rel dst rs (default_notrap_load_value chunk) 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. + rewrite ADDR. + rewrite LOAD. + right; trivial. } rewrite Regmap.gso by congruence. unfold sem_reg. @@ -632,6 +775,50 @@ Proof. apply load2_sound with (a := a); auto. Qed. +Lemma load1_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_notrap1_sound; auto. +Qed. + +Lemma load1_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load1 chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL ADDR LOAD. + unfold load1. + destruct in_dec. + { + apply kill_reg_sound; auto. + } + apply load2_notrap2_sound with (a := a); auto. +Qed. + Lemma load_sound : forall rel : RELATION.t, forall chunk : memory_chunk, @@ -649,11 +836,14 @@ Proof. intros until v. intros REL ADDR LOAD. unfold load. - destruct find_load eqn:FIND. + destruct find_load as [src | ] 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 + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk end) as FIND_LOAD. { apply (find_load_sound rel); trivial. @@ -661,12 +851,88 @@ Proof. rewrite forward_move_map in FIND_LOAD by assumption. destruct eval_addressing in *. 2: discriminate. - replace v with (rs # r) by congruence. + replace v0 with a in * by congruence. + destruct Mem.loadv in *. + 2: discriminate. + replace v with (rs # src) by congruence. apply move_sound; auto. } apply load1_sound with (a := a); trivial. Qed. +Lemma load_notrap1_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = None -> + sem_rel (load chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until rs. + intros REL ADDR. + unfold load. + destruct find_load as [src | ] eqn:FIND. + { + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + destruct eval_addressing in *. + discriminate. + rewrite <- FIND_LOAD. + apply move_sound; auto. + } + apply load1_notrap1_sound; trivial. +Qed. + +Lemma load_notrap2_sound : + forall rel : RELATION.t, + forall chunk : memory_chunk, + forall addr : addressing, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall a, + sem_rel rel rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.loadv chunk m a = None -> + sem_rel (load chunk addr dst args rel) (rs # dst <- (default_notrap_load_value chunk)). +Proof. + intros until a. + intros REL ADDR. + unfold load. + destruct find_load as [src | ] eqn:FIND. + { + assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with + | Some a => match Mem.loadv chunk m a with + | Some dat => rs#src = dat + | None => rs#src = default_notrap_load_value chunk + end + | None => rs#src = default_notrap_load_value chunk + end) as FIND_LOAD. + { + apply (find_load_sound rel); trivial. + } + rewrite forward_move_map in FIND_LOAD by assumption. + rewrite ADDR in FIND_LOAD. + destruct Mem.loadv; intro. + discriminate. + rewrite <- FIND_LOAD. + apply move_sound; auto. + } + apply load1_notrap2_sound; trivial. +Qed. + Lemma kill_reg_weaken: forall res mpc rs, sem_rel mpc rs -> @@ -759,15 +1025,14 @@ Proof. } destruct may_overlap eqn:OVERLAP; simpl; trivial. destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0. - symmetry. - eapply may_overlap_sound with (args := (map (forward_move rel) args)). - erewrite forward_move_map by eassumption. - exact ADDR. - exact ADDR0. - exact OVERLAP. - exact STORE. - symmetry; assumption. - assumption. + { + erewrite may_overlap_sound with (args := (map (forward_move rel) args)). + all: try eassumption. + + erewrite forward_move_map by eassumption. + assumption. + } + intuition congruence. Qed. End SOUNDNESS. @@ -1024,9 +1289,11 @@ Proof. 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. + f_equal. + symmetry. rewrite MAP in H0. - assumption. + eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. } unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } @@ -1080,22 +1347,65 @@ Proof. apply load_sound with (a := a); assumption. } - (* NOT IN THIS VERSION - (* load notrap1 *) + 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 := (default_notrap_load_value chunk)); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + f_equal. + rewrite MAP in H0. + eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. + } + 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_notrap1_sound; auto. + } + { econstructor; split. assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload_notrap1; 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 (load chunk addr dst args mpc)). { - replace (Some (kill 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. @@ -1104,26 +1414,71 @@ Proof. unfold apply_instr'. rewrite H. rewrite MPC. + simpl. reflexivity. } - apply kill_ok. - assumption. + apply load_notrap1_sound; assumption. + } -- (* load notrap2 *) +(* load notrap2 *) +- 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 := (default_notrap_load_value chunk)); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + f_equal. + rewrite MAP in H0. + eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: try eassumption. + } + 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_notrap2_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. + rewrite <- H0. + apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload_notrap2; 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 (load chunk addr dst args mpc)). { - replace (Some (kill 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. @@ -1132,11 +1487,11 @@ Proof. unfold apply_instr'. rewrite H. rewrite MPC. + simpl. reflexivity. } - apply kill_ok. - assumption. - *) + apply load_notrap2_sound with (a := a); assumption. + } - (* store *) econstructor. split. |