aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v5
-rw-r--r--mppa_k1c/Asmblock.v17
-rw-r--r--mppa_k1c/Asmblockdeps.v45
-rw-r--r--mppa_k1c/Asmblockgen.v4
-rw-r--r--mppa_k1c/Asmblockgenproof.v3
-rw-r--r--mppa_k1c/PostpassScheduling.v25
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml3
-rw-r--r--mppa_k1c/TargetPrinter.ml4
8 files changed, 87 insertions, 19 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 8486e25d..029ac995 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -50,6 +50,9 @@ 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)
@@ -209,6 +212,8 @@ 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 4f9fc34d..03c7e6d5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -179,6 +179,8 @@ Inductive ex_instruction : Type :=
| 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 *)
.
(** FIXME: comment not up to date !
@@ -523,9 +525,8 @@ Proof.
assert (b :: body = nil). eapply H; eauto. discriminate.
- destruct body; destruct exit.
all: simpl; auto; try constructor.
- + exploreInst.
+ + exploreInst; try discriminate.
simpl. contradiction.
- discriminate.
+ intros. discriminate.
Qed.
@@ -1437,10 +1438,20 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
| (None, _) => Stuck
end
-
(** 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 a2d75b27..7e9fb8f1 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -38,6 +38,8 @@ Inductive control_op :=
| Oj_l (l: label)
| Ocb (bt: btest) (l: label)
| Ocbu (bt: btest) (l: label)
+ | Odiv
+ | Odivu
| OError
| OIncremPC (sz: Z)
.
@@ -185,6 +187,16 @@ Definition control_eval (o: control_op) (l: list value) :=
| (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0)))
| (None, _) => None
end
+ | Odiv, [Val v1; Val v2] =>
+ match Val.divs v1 v2 with
+ | Some v => Some (Val v)
+ | None => None
+ end
+ | Odivu, [Val v1; Val v2] =>
+ match Val.divu v1 v2 with
+ | Some v => Some (Val v)
+ | None => None
+ end
| OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
| OError, _ => None
| _, _ => None
@@ -323,6 +335,8 @@ 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)
+ | Odiv, Odiv => RET true
+ | Odivu, Odivu => RET true
| OIncremPC sz1, OIncremPC sz2 => RET (Z.eqb sz1 sz2)
| OError, OError => RET true
| _, _ => RET false
@@ -504,6 +518,8 @@ 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.
@@ -801,6 +817,22 @@ 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.
@@ -992,6 +1024,12 @@ 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.
@@ -1103,6 +1141,11 @@ 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.
@@ -1421,6 +1464,8 @@ Definition string_of_control (op: control_op) : pstring :=
| Oj_l _ => "Oj_l"
| Ocb _ _ => "Ocb"
| Ocbu _ _ => "Ocbu"
+ | Odiv => "Odiv"
+ | Odivu => "Odivu"
| OError => "OError"
| OIncremPC _ => "OIncremPC"
end.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 4b168eec..c54394eb 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -960,7 +960,7 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr
| _ => {| header := hd; body := c; exit := None |}
:: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
end
- | Some (PCtlFlow i) => {| header := hd; body := (c ++ extract_basic ctl); exit := Some (PCtlFlow i) |} :: nil
+ | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil
end
.
Next Obligation.
@@ -970,7 +970,7 @@ Next Obligation.
Qed. Next Obligation.
apply wf_bblock_refl. constructor.
right. discriminate.
- discriminate.
+ unfold builtin_alone. intros. pose (H ef args res). rewrite H0 in n. contradiction.
Qed.
Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index ddc96f6c..ea4d1918 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -935,7 +935,8 @@ Proof.
intros until tbb. intros Hnonil Hnobuiltin GENB. unfold gen_bblocks in GENB.
destruct (extract_ctl tex) eqn:ECTL.
- destruct c.
- + destruct i. assert False. eapply Hnobuiltin. eauto. destruct H.
+ + destruct i; try (inv GENB; simpl; auto; fail).
+ assert False. eapply Hnobuiltin. eauto. destruct H.
+ inv GENB. simpl. auto.
- inversion Hnonil.
+ destruct tbdy as [|bi tbdy]; try (contradict H; simpl; auto; fail). inv GENB. auto.
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index b5d55ad3..6700e684 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -118,7 +118,7 @@ Proof.
destruct hdb.
- destruct exb.
+ destruct c.
- * destruct i. monadInv H.
+ * destruct i; monadInv H; split; auto.
* monadInv H. split; auto.
+ monadInv H. split; auto.
- monadInv H.
@@ -131,7 +131,8 @@ Proof.
destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.
destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).
- destruct c.
- + destruct i; try (monadInv EQ2).
+ + destruct i; monadInv EQ2;
+ unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity.
+ monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.
- unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.
Qed.
@@ -144,7 +145,7 @@ Proof.
unfold concat2 in H. simpl in H. monadInv H.
destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'.
- destruct c.
- + destruct i; discriminate.
+ + destruct i; try discriminate; congruence.
+ congruence.
- congruence.
Qed.
@@ -259,7 +260,7 @@ Proof.
destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.
destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.
- destruct c.
- + destruct i. discriminate.
+ + destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity.
+ inv EQ2. unfold stick_header; simpl. reflexivity.
- inv EQ2. unfold stick_header; simpl. reflexivity.
Qed.
@@ -393,9 +394,9 @@ Definition verified_schedule (bb : bblock) : res (list bblock) :=
Lemma verified_schedule_size:
forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.
Proof.
- intros. unfold verified_schedule in H. destruct (exit bb). destruct c.
+ intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
all: try (apply verified_schedule_nob_size; auto; fail).
- destruct i. inv H. simpl. omega.
+ inv H. simpl. omega.
Qed.
Lemma verified_schedule_no_header_in_middle:
@@ -403,9 +404,9 @@ Lemma verified_schedule_no_header_in_middle:
verified_schedule bb = OK lbb ->
Forall (fun b => header b = nil) (tail lbb).
Proof.
- intros. unfold verified_schedule in H. destruct (exit bb). destruct c.
+ intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail).
- destruct i. inv H. simpl. auto.
+ inv H. simpl. auto.
Qed.
Lemma verified_schedule_header:
@@ -414,9 +415,9 @@ Lemma verified_schedule_header:
header bb = header tbb
/\ Forall (fun b => header b = nil) lbb.
Proof.
- intros. unfold verified_schedule in H. destruct (exit bb). destruct c.
+ intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
all: try (eapply verified_schedule_nob_header; eauto; fail).
- destruct i. inv H. split; simpl; auto.
+ inv H. split; simpl; auto.
Qed.
@@ -443,9 +444,9 @@ Theorem verified_schedule_correct:
concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
Proof.
- intros. unfold verified_schedule in H. destruct (exit bb). destruct c.
+ intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
all: try (eapply verified_schedule_nob_correct; eauto; fail).
- destruct i. inv H. eexists. split; simpl; auto. constructor; auto.
+ inv H. eexists. split; simpl; auto. constructor; auto.
Qed.
Lemma verified_schedule_builtin_idem:
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index ce2fb2ae..ac257af3 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -206,6 +206,7 @@ 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
@@ -477,7 +478,7 @@ let ab_inst_to_real = function
| "Psd" | "Psd_a" | "Pfsd" -> Sd
| "Pcb" | "Pcbu" -> Cb
- | "Pcall" -> Call
+ | "Pcall" | "Pdiv" | "Pdivu" -> Call
| "Picall" -> Icall
| "Pgoto" | "Pj_l" -> Goto
| "Pigoto" -> Igoto
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 511537ce..d79a2be8 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -258,6 +258,10 @@ 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) ->
generated by cgit (git 2.34.1) at 2024-07-07 02:58:36 +0000