diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-29 19:29:34 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-29 19:29:34 +0100 |
commit | a7def1212eff65221d2528a27e567235420d7f15 (patch) | |
tree | b191ed1f9fbe541d6b4eae10f58135b2676e3974 | |
parent | 4c35899ac3f057d66784e658be5d21582b2d7e9c (diff) | |
parent | c0558ea2fd66679eeca136b41c4378ebebb9b3a0 (diff) | |
download | compcert-kvx-a7def1212eff65221d2528a27e567235420d7f15.tar.gz compcert-kvx-a7def1212eff65221d2528a27e567235420d7f15.zip |
Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mul
-rw-r--r-- | common/Switchaux.ml | 5 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 11 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 218 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 5 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 33 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 10 | ||||
-rw-r--r-- | mppa_k1c/Machregs.v | 3 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 1 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 1 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 16 | ||||
-rw-r--r-- | test/monniaux/mod_int_mat/Makefile | 2 |
12 files changed, 235 insertions, 72 deletions
diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 06337e7d..69300feb 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -80,10 +80,6 @@ let compile_switch_as_jumptable default cases minkey maxkey = CTaction default) let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = - (* FIXME DMonniaux disable jump tables until we can prove them through *) - false - -(* let span = Z.sub maxkey minkey in assert (Z.ge span Z.zero); let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases) @@ -91,7 +87,6 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = numcases >= 7 (* small jump tables are always less efficient *) && Z.le table_size tree_size && Z.lt span (Z.of_uint Sys.max_array_length) - *) let compile_switch modulus default table = let (tbl, keys) = normalize_table table in diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 7afed212..2d708b79 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -66,6 +66,7 @@ Inductive instruction : Type := | Pj_l (l: label) (**r jump to label *)
| Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *)
| Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *)
+ | Pjumptable (r: ireg) (labels: list label)
| Ploopdo (count: ireg) (loopend: label)
(** Loads **)
@@ -223,6 +224,7 @@ Definition control_to_instruction (c: control) := | PCtlFlow (Asmblock.Pj_l l) => Pj_l l
| PCtlFlow (Asmblock.Pcb bt r l) => Pcb bt r l
| PCtlFlow (Asmblock.Pcbu bt r l) => Pcbu bt r l
+ | PCtlFlow (Asmblock.Pjumptable r label) => Pjumptable r label
end.
Definition basic_to_instruction (b: basic) :=
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b341388c..b4cf57ae 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -231,6 +231,7 @@ Inductive cf_instruction : Type := | Pret (**r return *) | Pcall (l: label) (**r function call *) | Picall (r: ireg) (**r function call on register value *) + | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *) (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *) | Pgoto (l: label) (**r goto *) @@ -1468,6 +1469,16 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) Next (rs#PC <- (rs#r)) m | Pj_l l => goto_label f l rs m + | Pjumptable r tbl => + match rs#r with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label f lbl (rs #GPR62 <- Vundef #GPR63 <- Vundef) m + end + | _ => Stuck + end + | Pcb bt r l => match cmp_for_btest bt with | (Some c, Int) => eval_branch f l rs m (Val.cmp_bool c rs#r (Vint (Int.repr 0))) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 500fc504..dd876485 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -42,6 +42,7 @@ Inductive control_op := | Odivu | OError | OIncremPC (sz: Z) + | Ojumptable (l: list label) . Inductive arith_op := @@ -180,6 +181,15 @@ Definition eval_branch_deps (f: function) (l: label) (vpc: val) (res: option boo Definition control_eval (o: control_op) (l: list value) := let (ge, fn) := Ge in match o, l with + | (Ojumptable tbl), [Val index; Val vpc] => + match index with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => None + | Some lbl => goto_label_deps fn lbl vpc + end + | _ => None + end | Oj_l l, [Val vpc] => goto_label_deps fn l vpc | Ocb bt l, [Val v; Val vpc] => match cmp_for_btest bt with @@ -356,6 +366,7 @@ Definition control_op_eq (c1 c2: control_op): ?? bool := | Oj_l l1, Oj_l l2 => phys_eq l1 l2 | Ocb bt1 l1, Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | Ocbu bt1 l1, Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) + | Ojumptable tbl1, Ojumptable tbl2 => phys_eq tbl1 tbl2 | Odiv, Odiv => RET true | Odivu, Odivu => RET true | OIncremPC sz1, OIncremPC sz2 => RET (Z.eqb sz1 sz2) @@ -371,6 +382,7 @@ Proof. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - rewrite Z.eqb_eq in * |-. congruence. + - congruence. Qed. @@ -540,6 +552,9 @@ Definition trans_control (ctl: control) : macro := | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))] | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))] | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))] + | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (Name (#r) @ Name (#PC) @ Enil)); + (#GPR62, Op (Constant Vundef) Enil); + (#GPR63, Op (Constant Vundef) Enil) ] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] end. @@ -861,8 +876,27 @@ Proof. intros. destruct ex. - simpl in *. inv H1. destruct c; destruct i; try discriminate. all: try (inv H0; eexists; split; try split; [ simpl control_eval; pose (H3 PC); simpl in e; rewrite e; reflexivity | Simpl | intros rr; destruct rr; Simpl]). + (* Pjumptable *) + + unfold goto_label in *. + repeat (rewrite Pregmap.gso in H0; try discriminate). + destruct (nextblock _ _ _) eqn:NB; try discriminate. + destruct (list_nth_z _ _) eqn:LI; try discriminate. + destruct (label_pos _ _ _) eqn:LPOS; try discriminate. + destruct (nextblock b rs PC) eqn:MB2; try discriminate. inv H0. + eexists; split; try split. + * simpl control_eval. rewrite (H3 PC). simpl. Simpl. + rewrite H3. unfold nextblock in NB. rewrite Pregmap.gso in NB; try discriminate. rewrite NB. + rewrite LI. unfold goto_label_deps. rewrite LPOS. + unfold nextblock in MB2. rewrite Pregmap.gss in MB2. rewrite MB2. + reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (preg_eq GPR62 g); Simpl. rewrite e. Simpl. + destruct (preg_eq GPR63 g); Simpl. rewrite e. Simpl. (* Pj_l *) - + unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. + + unfold goto_label in H0. + destruct (label_pos _ _ _) eqn:LPOS; try discriminate. + destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity. @@ -1052,6 +1086,11 @@ Lemma exec_exit_none: Proof. intros. inv H0. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try reflexivity; try discriminate. +(* Pjumptable *) + - simpl in *. repeat (rewrite H3 in H1). + destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto. + unfold goto_label_deps in H1. unfold goto_label. Simpl. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e. unfold goto_label_deps in H1. unfold goto_label. @@ -1163,6 +1202,10 @@ Lemma forward_simu_exit_stuck: Proof. intros. inv H1. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). + (* Pjumptable *) + - simpl in *. repeat (rewrite H3). destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto. + unfold goto_label_deps. unfold goto_label in H0. + destruct (label_pos _ _ _); auto. repeat (rewrite Pregmap.gso in H0; try discriminate). destruct (rs PC); auto. discriminate. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0. destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate. @@ -1504,6 +1547,7 @@ Definition string_of_control (op: control_op) : pstring := | Ocbu _ _ => "Ocbu" | Odiv => "Odiv" | Odivu => "Odivu" + | Ojumptable _ => "Ojumptable" | OError => "OError" | OIncremPC _ => "OIncremPC" end. @@ -1731,6 +1775,37 @@ Proof. - simpl in H. inv H. inv MSR. inv MSW. eexists. split; try split. assumption. assumption. Qed. +Theorem forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_basic_instr ge bi rsr rsw mr mw = Stuck -> + macro_prun Ge (trans_basic bi) sw sr sr = None. +Proof. + intros GENV MSR MSW H0. inv MSR; inv MSW. + unfold parexec_basic_instr in H0. destruct bi; try discriminate. +(* PLoad *) + - destruct i; destruct i. + all: simpl; rewrite H; rewrite (H1 ra); unfold parexec_load in H0; + destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate. +(* PStore *) + - destruct i; destruct i; + simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); + unfold parexec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate. +(* Pallocframe *) + - simpl. Simpl. rewrite (H1 SP). rewrite H. destruct (Mem.alloc _ _ _). simpl in H0. + destruct (Mem.store _ _ _ _); try discriminate. reflexivity. +(* Pfreeframe *) + - simpl. Simpl. rewrite (H1 SP). rewrite H. + destruct (Mem.loadv _ _ _); auto. destruct (rsr GPR12); auto. destruct (Mem.free _ _ _ _); auto. + discriminate. +(* Pget *) + - simpl. destruct rs; subst; try discriminate. + all: simpl; auto. + - simpl. destruct rd; subst; try discriminate. + all: simpl; auto. +Qed. + Theorem forward_simu_par_body: forall bdy ge fn rsr mr sr rsw mw sw rs' m', Ge = Genv ge fn -> @@ -1770,6 +1845,17 @@ Proof. - destruct c; destruct i; try discriminate. all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [simpl; rewrite (H0 PC); reflexivity | Simpl | intros rr; destruct rr; unfold par_nextblock; Simpl]). + (* Pjumptable *) + + simpl in H0. destruct (par_nextblock _ _ _) eqn:PNEXT; try discriminate. + destruct (list_nth_z _ _) eqn:LISTS; try discriminate. unfold par_goto_label in H0. + destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ rsr PC) eqn:NB; try discriminate. inv H0. + inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock in PNEXT. rewrite Pregmap.gso in PNEXT; try discriminate. rewrite PNEXT. + rewrite LISTS. unfold goto_label_deps. rewrite LPOS. unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. + destruct (preg_eq g GPR62). rewrite e. Simpl. + destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. (* Pj_l *) + simpl in H0. unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. inv H0. inv MSR; inv MSW. @@ -1856,20 +1942,56 @@ Proof. intros rr. destruct rr; unfold par_nextblock; Simpl. Qed. -Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). - -(* Lemma put in Parallelizability. -Lemma prun_iw_app_some: - forall c c' sr sw s' s'', - prun_iw Ge c sw sr = Some s' -> - prun_iw Ge c' s' sr = Some s'' -> - prun_iw Ge (c ++ c') sw sr = Some s''. +Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck -> + macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. Proof. - induction c. - - simpl. intros. congruence. - - intros. simpl in *. destruct (macro_prun _ _ _ _); auto. eapply IHc; eauto. discriminate. + intros GENV MSR MSW H0. inv MSR; inv MSW. destruct ex as [ctl|]; try discriminate. + destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). +(* Pbuiltin *) + - simpl in *. rewrite (H1 PC). reflexivity. +(* Pjumptable *) + - simpl in *. rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (rsr r); auto. destruct (list_nth_z _ _); auto. unfold par_goto_label in H0. unfold goto_label_deps. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); try discriminate; auto. +(* Pj_l *) + - simpl in *. rewrite (H1 PC). unfold goto_label_deps. unfold par_goto_label in H0. + destruct (label_pos _ _ _); auto. simpl in *. unfold par_nextblock in H0. rewrite Pregmap.gss in H0. + destruct (Val.offset_ptr _ _); try discriminate; auto. +(* Pcb *) + - simpl in *. destruct (cmp_for_btest bt). destruct i. + -- destruct o. + + unfold par_eval_branch in H0; unfold eval_branch_deps. + rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate. + + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity. + -- destruct o. + + unfold par_eval_branch in H0; unfold eval_branch_deps. + rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate. + + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity. +(* Pcbu *) + - simpl in *. destruct (cmpu_for_btest bt). destruct i. + -- destruct o. + + unfold par_eval_branch in H0; unfold eval_branch_deps. + rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate. + + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity. + -- destruct o. + + unfold par_eval_branch in H0; unfold eval_branch_deps. + rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (Val_cmplu_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); auto. discriminate. + + rewrite (H1 PC). Simpl. rewrite (H1 r). reflexivity. Qed. -*) + +Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m': Ge = Genv ge fn -> @@ -1908,41 +2030,6 @@ Proof. erewrite prun_iw_app_Some; eauto. eassumption. Qed. -Lemma trans_body_perserves_permutation bdy1 bdy2: - Permutation bdy1 bdy2 -> - Permutation (trans_body bdy1) (trans_body bdy2). -Proof. - induction 1; simpl; econstructor; eauto. -Qed. - -Lemma trans_body_app bdy1: forall bdy2, - trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2). -Proof. - induction bdy1; simpl; congruence. -Qed. - -Theorem trans_block_perserves_permutation bdy1 bdy2 b: - Permutation (bdy1 ++ bdy2) (body b) -> - Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). -Proof. - intro H; unfold trans_block, trans_block_aux. - eapply perm_trans. - - eapply Permutation_app_tail. - apply trans_body_perserves_permutation. - apply Permutation_sym; eapply H. - - rewrite trans_body_app. rewrite <-! app_assoc. - apply Permutation_app_head. - apply Permutation_app_comm. -Qed. - -Lemma forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - parexec_basic_instr ge bi rsr rsw mr mw = Stuck -> - macro_prun Ge (trans_basic bi) sw sr sr = None. -Admitted. - Lemma forward_simu_par_body_Stuck bdy: forall ge fn rsr mr sr rsw mw sw, Ge = Genv ge fn -> match_states (State rsr mr) sr -> @@ -1962,14 +2049,6 @@ Proof. intros X; simpl; rewrite X; auto. Qed. -Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex: - Ge = Genv ge fn -> - match_states (State rsr mr) sr -> - match_states (State rsw mw) sw -> - parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck -> - macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. -Admitted. - Lemma forward_simu_par_wio_stuck_bdy1 ge fn rs m s1' bdy1 sz ex: Ge = Genv ge fn -> match_states (State rs m) s1' -> @@ -1999,6 +2078,33 @@ Proof. eapply forward_simu_par_body_Stuck. 4: eauto. all: eauto. Qed. +Lemma trans_body_perserves_permutation bdy1 bdy2: + Permutation bdy1 bdy2 -> + Permutation (trans_body bdy1) (trans_body bdy2). +Proof. + induction 1; simpl; econstructor; eauto. +Qed. + +Lemma trans_body_app bdy1: forall bdy2, + trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2). +Proof. + induction bdy1; simpl; congruence. +Qed. + +Theorem trans_block_perserves_permutation bdy1 bdy2 b: + Permutation (bdy1 ++ bdy2) (body b) -> + Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). +Proof. + intro H; unfold trans_block, trans_block_aux. + eapply perm_trans. + - eapply Permutation_app_tail. + apply trans_body_perserves_permutation. + apply Permutation_sym; eapply H. + - rewrite trans_body_app. rewrite <-! app_assoc. + apply Permutation_app_head. + apply Permutation_app_comm. +Qed. + Theorem forward_simu_par: forall rs1 m1 s1' b ge fn rs2 m2, Ge = Genv ge fn -> diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index c03e319c..1afb627a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -899,8 +899,9 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co | MBreturn => OK (make_epilogue f (Pret ::g nil)) (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) - | MBjumptable _ _ => - Error (msg "Asmblockgen.transl_instr_control MBjumptable") + | MBjumptable arg tbl => + do r <- ireg_of arg; + OK (Pjumptable r tbl ::g nil) end end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index ea4d1918..63f4c136 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -883,11 +883,16 @@ Proof. intros until x2. intros Hbuiltin TIC.
destruct ex.
- destruct c.
+ (* MBcall *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBtailcall *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBbuiltin *)
+ assert (H: Some (MBbuiltin e l b) <> Some (MBbuiltin e l b)).
apply Hbuiltin. contradict H; auto.
+ (* MBgoto *)
+ simpl in TIC. exploreInst; simpl; eauto.
+ (* MBcond *)
+ simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto.
* unfold transl_opt_compuimm. exploreInst; simpl; eauto.
* unfold transl_opt_compluimm. exploreInst; simpl; eauto.
@@ -895,7 +900,9 @@ Proof. * unfold transl_comp_notfloat64. exploreInst; simpl; eauto.
* unfold transl_comp_float32. exploreInst; simpl; eauto.
* unfold transl_comp_notfloat32. exploreInst; simpl; eauto.
- + simpl in TIC. inv TIC.
+ (* MBjumptable *)
+ + simpl in TIC. exploreInst; simpl; eauto.
+ (* MBreturn *)
+ simpl in TIC. monadInv TIC. simpl. eauto.
- monadInv TIC. simpl; auto.
Qed.
@@ -1358,7 +1365,29 @@ Proof. intros. discriminate.
+ (* MBjumptable *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
- inv TBC. inv TIC.
+ inv TBC. inv TIC. inv H0.
+
+ assert (f0 = f) by congruence. subst f0.
+ monadInv H1.
+ generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
+ assert (f1 = f) by congruence. subst f1.
+ exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).
+ unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
+ exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
+
+ intros [tc' [rs' [A [B C]]]].
+ exploit ireg_val; eauto. rewrite H13. intros LD; inv LD.
+
+ repeat eexists.
+ rewrite H6. simpl extract_basic. simpl. eauto.
+ rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.
+ econstructor; eauto.
+ eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
+ { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.
+ destruct (preg_eq r' GPR63). subst. contradiction.
+ destruct (preg_eq r' GPR62). subst. contradiction.
+ destruct r'; Simpl. }
+ discriminate.
+ (* MBreturn *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
inv TBC. inv TIC. inv H0.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index a6e9f04b..d553c612 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -211,6 +211,15 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw | Picall r => Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw + | Pjumptable r tbl => + match rsr#r with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw + end + | _ => Stuck + end | Pgoto s => Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw | Pigoto r => @@ -230,7 +239,6 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) | (None, _) => Stuck end - (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 4de37af4..60142797 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -152,8 +152,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre Definition destroyed_by_cond (cond: condition): list mreg := nil. -(* Definition destroyed_by_jumptable: list mreg := R5 :: nil. *) -Definition destroyed_by_jumptable: list mreg := nil. +Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil. Fixpoint destroyed_by_clobber (cl: list string): list mreg := match cl with diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 56b00c7e..62df124a 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -233,6 +233,7 @@ let ctl_flow_rec = function | Pj_l lbl -> { inst = "Pj_l"; write_locs = []; read_locs = []; imm = None ; is_control = true} | Pcb (bt, rs, lbl) -> { inst = "Pcb"; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true} | Pcbu (bt, rs, lbl) -> { inst = "Pcbu"; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true} + | Pjumptable (r, _) -> { inst = "Pjumptable"; write_locs = [Reg (IR GPR62); Reg (IR GPR63)]; read_locs = [Reg (IR r)]; imm = None ; is_control = true} let control_rec i = match i with diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index dd485ea4..4e33fc90 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -550,6 +550,7 @@ Proof. - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. Qed. Lemma eval_offset_preserved: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 41a6622a..29e0fef4 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -264,7 +264,17 @@ module Target (*: TARGET*) = fprintf oc " cb.%a %a? %a\n" bcond bt ireg r print_label lbl | Ploopdo (r, lbl) -> fprintf oc " loopdo %a, %a\n" ireg r print_label lbl - + | Pjumptable (idx_reg, tbl) -> + let lbl = new_label() in + jumptables := (lbl, tbl) :: !jumptables; + let base_reg = if idx_reg=Asmblock.GPR63 then Asmblock.GPR62 else Asmblock.GPR63 in + fprintf oc "%s jumptable [ " comment; + List.iter (fun l -> fprintf oc "%a " print_label l) tbl; + fprintf oc "]\n"; + fprintf oc " make %a = %a\n ;;\n" ireg base_reg label lbl; + fprintf oc " lwz.xs %a = %a[%a]\n ;;\n" ireg base_reg ireg idx_reg ireg base_reg; + fprintf oc " igoto %a\n ;;\n" ireg base_reg + (* Load/Store instructions *) | Plb(rd, ra, ofs) -> fprintf oc " lbs %a = %a[%a]\n" ireg rd offset ofs ireg ra @@ -518,8 +528,8 @@ module Target (*: TARGET*) = let print_tbl oc (lbl, tbl) = fprintf oc "%a:\n" label lbl; List.iter - (fun l -> fprintf oc " .long %a - %a\n" - print_label l label lbl) + (fun l -> fprintf oc " .4byte %a\n" + print_label l) tbl in if !jumptables <> [] then begin diff --git a/test/monniaux/mod_int_mat/Makefile b/test/monniaux/mod_int_mat/Makefile index f904c1e4..d1365b34 100644 --- a/test/monniaux/mod_int_mat/Makefile +++ b/test/monniaux/mod_int_mat/Makefile @@ -1,4 +1,4 @@ -CFLAGS=-Wall -O3 +CFLAGS=-Wall -O3 -std=c99 K1C_CC=k1-mbr-gcc K1C_CFLAGS=-Wall -O3 -std=c99 K1C_CCOMP=../../../ccomp |