diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 10:49:09 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 10:49:09 +0100 |
commit | 1bc0ce716ff90a5384a70b5f9426108bb6380549 (patch) | |
tree | b6ca35c578f4b3016ba2507e0f308aa38009fea9 /mppa_k1c | |
parent | 98fe0a6c690c2f273e453048fc7f39bd0248bd0c (diff) | |
download | compcert-kvx-1bc0ce716ff90a5384a70b5f9426108bb6380549.tar.gz compcert-kvx-1bc0ce716ff90a5384a70b5f9426108bb6380549.zip |
rm Pdiv / Pdivu
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 16 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 29 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 1 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 |
6 files changed, 1 insertions, 66 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 493f4a05..0ca554ab 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -50,9 +50,6 @@ Inductive instruction : Type := | Psemi (**r semi colon separating bundles *)
| Pnop (**r instruction that does nothing *)
- | Pdiv (**r 32 bits integer division *)
- | Pdivu (**r 32 bits integer division *)
-
(** builtins *)
| Pclzll (rd rs: ireg)
| Pstsud (rd rs1 rs2: ireg)
@@ -218,8 +215,6 @@ Inductive instruction : Type := Definition control_to_instruction (c: control) :=
match c with
| PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res
- | PExpand (Asmblock.Pdiv) => Pdiv
- | PExpand (Asmblock.Pdivu) => Pdivu
| PCtlFlow Asmblock.Pret => Pret
| PCtlFlow (Asmblock.Pcall l) => Pcall l
| PCtlFlow (Asmblock.Picall r) => Picall r
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d335801e..fdec8ed2 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -178,10 +178,7 @@ Inductive ex_instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) - | Pdiv (**r 32 bits integer division, call to __divdi3 *) - | Pdivu (**r 32 bits integer division, call to __udivdi3 *) -. + -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *). (** FIXME: comment not up to date ! @@ -1486,17 +1483,6 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pdiv => - match Val.divs (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end - - | Pdivu => - match Val.divu (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end end | None => Next rs m end. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 501ec212..ad96ae87 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -540,8 +540,6 @@ 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))] - | Pdiv => [(#GPR0, Op (Control Odiv) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] - | Pdivu => [(#GPR0, Op (Control Odivu) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] end. @@ -863,22 +861,6 @@ 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]). - (* Pdiv *) - + destruct (Val.divs _ _) eqn:DIVS; try discriminate. inv H0. unfold nextblock in DIVS. repeat (rewrite Pregmap.gso in DIVS; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVS. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. - (* Pdivu *) - + destruct (Val.divu _ _) eqn:DIVU; try discriminate. inv H0. unfold nextblock in DIVU. repeat (rewrite Pregmap.gso in DIVU; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVU. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 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. eexists; split; try split. @@ -1070,12 +1052,6 @@ Lemma exec_exit_none: Proof. intros. inv H0. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try reflexivity; try discriminate. -(* Pdiv *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divs _ _); try discriminate; auto. -(* Pdivu *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* 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. @@ -1187,11 +1163,6 @@ Lemma forward_simu_exit_stuck: Proof. intros. inv H1. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). -(* Pdiv *) - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divs _ _); try discriminate; auto. - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* 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. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 5b00a64f..c03e319c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -425,18 +425,6 @@ Definition transl_op OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) - | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivw rd rs1 rs2 :: k) *) - | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivuw rd rs1 rs2 :: k) *) - | Omod, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omod: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premw rd rs1 rs2 :: k) *) - | Omodu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omodu: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premuw rd rs1 rs2 :: k) *) | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 ::i k) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2c39e342..56b00c7e 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -222,7 +222,6 @@ let basic_rec i = | Pnop -> { inst = "nop"; write_locs = []; read_locs = []; imm = None ; is_control = false} let expand_rec = function - | Pdiv | Pdivu -> { inst = "Pdiv"; write_locs = [Reg (IR GPR0)]; read_locs = [Reg (IR GPR0); Reg (IR GPR1)]; imm = None; is_control = true } | Pbuiltin _ -> raise OpaqueInstruction let ctl_flow_rec = function diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index d4e2afc9..69824852 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -258,10 +258,6 @@ module Target (*: TARGET*) = fprintf oc " goto %a\n" symbol s | Pigoto(rs) -> fprintf oc " igoto %a\n" ireg rs - | Pdiv -> - fprintf oc " call __divdi3\n" - | Pdivu -> - fprintf oc " call __udivdi3\n" | Pj_l(s) -> fprintf oc " goto %a\n" print_label s | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) -> |