aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--common/Switchaux.ml5
-rw-r--r--mppa_k1c/Asm.v2
-rw-r--r--mppa_k1c/Asmblock.v11
-rw-r--r--mppa_k1c/Asmblockdeps.v46
-rw-r--r--mppa_k1c/Asmblockgen.v5
-rw-r--r--mppa_k1c/Asmblockgenproof.v14
-rw-r--r--mppa_k1c/Machregs.v3
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml1
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v1
-rw-r--r--mppa_k1c/TargetPrinter.ml16
10 files changed, 87 insertions, 17 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 0ca554ab..421f3d2c 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 fdec8ed2..d630e767 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -230,6 +230,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 *)
@@ -1467,6 +1468,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 ad96ae87..845a26ed 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.
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..5d952d02 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.
@@ -1357,8 +1364,7 @@ Proof.
all: rewrite <- C; try discriminate; unfold nextblock; Simpl. }
intros. discriminate.
+ (* MBjumptable *)
- destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
- inv TBC. inv TIC.
+ admit.
+ (* MBreturn *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
inv TBC. inv TIC. inv H0.
@@ -1393,7 +1399,7 @@ Proof.
generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto.
eapply agree_exten; eauto. intros. Simpl.
discriminate.
-Qed.
+Admitted.
Definition mb_remove_first (bb: MB.bblock) :=
{| MB.header := MB.header bb; MB.body := tail (MB.body bb); MB.exit := MB.exit bb |}.
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 33912203..b59c381c 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 69824852..233dffec 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
generated by cgit (git 2.34.1) at 2024-07-14 00:57:42 +0000