aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-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.v17
-rw-r--r--mppa_k1c/Asmblockgenproof.v32
-rw-r--r--mppa_k1c/Asmexpand.ml35
-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/SelectLong.vp1
-rw-r--r--mppa_k1c/SelectLongproof.v1
-rw-r--r--mppa_k1c/SelectOp.vp35
-rw-r--r--mppa_k1c/SelectOpproof.v82
-rw-r--r--mppa_k1c/TargetPrinter.ml16
14 files changed, 220 insertions, 63 deletions
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 6f872188..7f03c66a 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 5b00a64f..1afb627a 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)
@@ -911,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..2a238c7c 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,26 @@ 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.
+ { admit. }
+ discriminate.
+ (* MBreturn *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
inv TBC. inv TIC. inv H0.
@@ -1393,7 +1419,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/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 1c9e4e4c..f1528389 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -124,9 +124,6 @@ let expand_annot_val kind txt targ args res = assert false
(* Handling of memcpy *)
-let offset_in_range ofs =
- let ofs = Z.to_int64 ofs in -2048L <= ofs && ofs < 2048L
-
let emit_move dst r =
if dst <> r
then emit (Paddil(dst, r, Z.zero));;
@@ -175,7 +172,7 @@ let expand_builtin_memcpy sz al args =
| _ -> assert false;;
(* Handling of volatile reads and writes *)
-
+(* FIXME probably need to check for size of displacement *)
let expand_builtin_vload_common chunk base ofs res =
match chunk, res with
| Mint8unsigned, BR(Asmblock.IR res) ->
@@ -211,21 +208,9 @@ let expand_builtin_vload chunk args res =
| [BA(Asmblock.IR addr)] ->
expand_builtin_vload_common chunk addr _0 res
| [BA_addrstack ofs] ->
- if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
- expand_builtin_vload_common chunk stack_pointer ofs res
- else begin
- assert false (* FIXME
- expand_addptrofs Asmblock.GPR32 stack_pointer ofs; (* X31 <- sp + ofs *)
- expand_builtin_vload_common chunk GPR32 _0 res *)
- end
+ expand_builtin_vload_common chunk stack_pointer ofs res
| [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs))] ->
- if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
- expand_builtin_vload_common chunk addr ofs res
- else begin
- assert false (* FIXME
- expand_addptrofs Asmblock.GPR32 addr ofs; (* X31 <- addr + ofs *)
- expand_builtin_vload_common chunk Asmblock.GPR32 _0 res *)
- end
+ expand_builtin_vload_common chunk addr ofs res
| _ ->
assert false
@@ -256,19 +241,9 @@ let expand_builtin_vstore chunk args =
| [BA(Asmblock.IR addr); src] ->
expand_builtin_vstore_common chunk addr _0 src
| [BA_addrstack ofs; src] ->
- if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
- expand_builtin_vstore_common chunk stack_pointer ofs src
- else begin (* FIXME
- expand_addptrofs X31 X2 ofs; (* X31 <- sp + ofs *)
- expand_builtin_vstore_common chunk X31 _0 src *)
- end
+ expand_builtin_vstore_common chunk stack_pointer ofs src
| [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs)); src] ->
- if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
- expand_builtin_vstore_common chunk addr ofs src
- else begin (* FIXME
- expand_addptrofs X31 addr ofs; (* X31 <- addr + ofs *)
- expand_builtin_vstore_common chunk X31 _0 src *)
- end
+ expand_builtin_vstore_common chunk addr ofs src
| _ ->
assert false
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/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 3a17ab17..0c3618d7 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -21,6 +21,7 @@ Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
+Require Import OpHelpers.
Require Import SelectOp SplitLong.
Local Open Scope cminorsel_scope.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 4723278a..79187338 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -21,6 +21,7 @@ Require Import String Coqlib Maps Integers Floats Errors.
Require Archi.
Require Import AST Values Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
Require Import SelectLong.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index e4d65ced..f6605c11 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -15,6 +15,7 @@
(* *)
(* *********************************************************************)
+
(** Instruction selection for operators *)
(** The instruction selection pass recognizes opportunities for using
@@ -49,9 +50,17 @@ Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import CminorSel.
+Require Import OpHelpers.
Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Section SELECT.
+
+Context {hf: helper_functions}.
+
(** ** Constants **)
Definition addrsymbol (id: ident) (ofs: ptrofs) :=
@@ -302,10 +311,17 @@ Nondetfunction notint (e: expr) :=
(** ** Integer division and modulus *)
-Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
-Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
-Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) :=
+ Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil).
+
+Definition mods_base (e1: expr) (e2: expr) :=
+ Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).
+
+Definition divu_base (e1: expr) (e2: expr) :=
+ Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
+
+Definition modu_base (e1: expr) (e2: expr) :=
+ Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).
Definition shrximm (e1: expr) (n2: int) :=
if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
@@ -485,3 +501,14 @@ Nondetfunction builtin_arg (e: expr) :=
if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
| _ => BA e
end.
+
+(* float division *)
+
+Definition divf_base (e1: expr) (e2: expr) :=
+ (* Eop Odivf (e1 ::: e2 ::: Enil). *)
+ Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil).
+
+Definition divfs_base (e1: expr) (e2: expr) :=
+ (* Eop Odivf (e1 ::: e2 ::: Enil). *)
+ Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).
+End SELECT.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 94d162a2..89af39ee 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -29,8 +29,13 @@ Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
+Require Import Events.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
(** * Useful lemmas and tactics *)
@@ -80,12 +85,53 @@ Ltac TrivialExists :=
(** * Correctness of the smart constructors *)
Section CMCONSTR.
-
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
Variable sp: val.
Variable e: env.
Variable m: mem.
+(* Helper lemmas - from SplitLongproof.v *)
+
+Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
+Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
+
+Lemma eval_helper:
+ forall le id name sg args vargs vres,
+ eval_exprlist ge sp e m le args vargs ->
+ helper_declared prog id name sg ->
+ external_implements name sg vargs vres ->
+ eval_expr ge sp e m le (Eexternal id sg args) vres.
+Proof.
+ intros.
+ red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q).
+ rewrite <- Genv.find_funct_ptr_iff in Q.
+ econstructor; eauto.
+Qed.
+
+Corollary eval_helper_1:
+ forall le id name sg arg1 varg1 vres,
+ eval_expr ge sp e m le arg1 varg1 ->
+ helper_declared prog id name sg ->
+ external_implements name sg (varg1::nil) vres ->
+ eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres.
+Proof.
+ intros. eapply eval_helper; eauto. constructor; auto. constructor.
+Qed.
+
+Corollary eval_helper_2:
+ forall le id name sg arg1 arg2 varg1 varg2 vres,
+ eval_expr ge sp e m le arg1 varg1 ->
+ eval_expr ge sp e m le arg2 varg2 ->
+ helper_declared prog id name sg ->
+ external_implements name sg (varg1::varg2::nil) vres ->
+ eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres.
+Proof.
+ intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor.
+Qed.
+
(** We now show that the code generated by "smart constructor" functions
such as [Selection.notint] behaves as expected. Continuing the
[notint] example, we show that if the expression [e]
@@ -557,7 +603,8 @@ Theorem eval_divs_base:
Val.divs x y = Some z ->
exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
Proof.
- intros. unfold divs_base. exists z; split. EvalOp. auto.
+ intros; unfold divs_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
Qed.
Theorem eval_mods_base:
@@ -567,7 +614,8 @@ Theorem eval_mods_base:
Val.mods x y = Some z ->
exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
Proof.
- intros. unfold mods_base. exists z; split. EvalOp. auto.
+ intros; unfold mods_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
Qed.
Theorem eval_divu_base:
@@ -577,7 +625,8 @@ Theorem eval_divu_base:
Val.divu x y = Some z ->
exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
Proof.
- intros. unfold divu_base. exists z; split. EvalOp. auto.
+ intros; unfold divu_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
Qed.
Theorem eval_modu_base:
@@ -587,7 +636,8 @@ Theorem eval_modu_base:
Val.modu x y = Some z ->
exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
Proof.
- intros. unfold modu_base. exists z; split. EvalOp. auto.
+ intros; unfold modu_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
Qed.
Theorem eval_shrximm:
@@ -968,4 +1018,24 @@ Proof.
- constructor; auto.
Qed.
+(* floating-point division *)
+Theorem eval_divf_base:
+ forall le a b x y,
+ eval_expr ge sp e m le a x ->
+ eval_expr ge sp e m le b y ->
+ exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+ intros; unfold divf_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+Theorem eval_divfs_base:
+ forall le a b x y,
+ eval_expr ge sp e m le a x ->
+ eval_expr ge sp e m le b y ->
+ exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+ intros; unfold divfs_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
End CMCONSTR.
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
generated by cgit (git 2.34.1) at 2024-07-14 09:16:53 +0000