aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v5
-rw-r--r--mppa_k1c/Asmblock.v22
-rw-r--r--mppa_k1c/Asmblockdeps.v49
-rw-r--r--mppa_k1c/Asmblockgen.v6
-rw-r--r--mppa_k1c/Asmblockgenproof.v7
-rw-r--r--mppa_k1c/Asmexpand.ml15
-rw-r--r--mppa_k1c/Machregs.v12
-rw-r--r--mppa_k1c/PostpassScheduling.v25
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml3
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v6
-rw-r--r--mppa_k1c/TargetPrinter.ml4
11 files changed, 109 insertions, 45 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 0ca554ab..493f4a05 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)
@@ -215,6 +218,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 386106d6..d335801e 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -85,7 +85,8 @@ Module Pregmap := EMap(PregEq).
(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
Notation "'SP'" := GPR12 (only parsing) : asm.
-Notation "'FP'" := GPR14 (only parsing) : asm.
+Notation "'FP'" := GPR17 (only parsing) : asm.
+Notation "'MFP'" := R17 (only parsing) : asm.
Notation "'GPRA'" := GPR16 (only parsing) : asm.
Notation "'RTMP'" := GPR32 (only parsing) : asm.
@@ -178,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 !
@@ -543,9 +546,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.
@@ -1481,10 +1483,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.
@@ -1506,7 +1518,7 @@ Definition preg_of (r: mreg) : preg :=
match r with
| R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
| R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9
- | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | *) | R14 => GPR14
+ | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *)
| R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19 => GPR19
| R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
| R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index f50b7d4a..501ec212 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)
.
@@ -191,6 +193,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
@@ -344,6 +356,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
@@ -526,6 +540,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.
@@ -796,7 +812,7 @@ Proof.
rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity.
* Simpl.
* intros rr; destruct rr; Simpl.
- destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl.
+ destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
(* Freeframe *)
- simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate.
destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0.
@@ -804,7 +820,7 @@ Proof.
* simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE.
Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity.
* Simpl.
- * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl.
+ * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
(* Pget *)
- simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0.
eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
@@ -847,6 +863,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.
@@ -1038,6 +1070,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.
@@ -1149,6 +1187,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.
@@ -1488,6 +1531,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 80b712e3..312d2386 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -25,8 +25,6 @@ Require Import Op Locations Machblock Asmblock.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
-Notation "'MFP'" := R14 (only parsing).
-
(** The code generation functions take advantage of several
characteristics of the [Mach] code generated by earlier passes of the
compiler, mostly that argument and result registers are of the correct
@@ -992,7 +990,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.
@@ -1002,7 +1000,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 84877488..ea4d1918 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -758,9 +758,9 @@ Qed. *)
the unwanted behaviour. *)
-Remark preg_of_not_FP: forall r, negb (mreg_eq r R14) = true -> IR FP <> preg_of r.
+Remark preg_of_not_FP: forall r, negb (mreg_eq r MFP) = true -> IR FP <> preg_of r.
Proof.
- intros. change (IR FP) with (preg_of R14). red; intros.
+ intros. change (IR FP) with (preg_of MFP). red; intros.
exploit preg_of_injective; eauto. intros; subst r; discriminate.
Qed.
@@ -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/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index cd6cf1ec..1c9e4e4c 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -401,15 +401,14 @@ let expand_instruction instr =
match instr with
| Pallocframe (sz, ofs) ->
let sg = get_current_function_sig() in
+ emit (Pmv (Asmblock.GPR17, stack_pointer));
if sg.sig_cc.cc_vararg then begin
let n = arguments_size sg in
let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
- let full_sz = Z.add sz (Z.of_uint extra_sz) in begin
- expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz));
- emit Psemi;
- expand_storeind_ptr Asmblock.GPR14 stack_pointer ofs;
- expand_addptrofs Asmblock.GPR14 stack_pointer (Ptrofs.repr full_sz)
- end;
+ let full_sz = Z.add sz (Z.of_uint extra_sz) in
+ expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz));
+ emit Psemi;
+ expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
emit Psemi;
let va_ofs =
sz in
@@ -419,8 +418,7 @@ let expand_instruction instr =
end else begin
expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg sz));
emit Psemi;
- expand_storeind_ptr Asmblock.GPR14 stack_pointer ofs;
- expand_addptrofs Asmblock.GPR14 stack_pointer (Ptrofs.repr sz);
+ expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
emit Psemi;
vararg_start_ofs := None
end
@@ -431,7 +429,6 @@ let expand_instruction instr =
let n = arguments_size sg in
if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize)
end else 0 in
- expand_loadind_ptr Asmblock.GPR14 stack_pointer ofs;
expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
(*| Pseqw(rd, rs1, rs2) ->
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 9f0f6a4d..ef0f97a9 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -41,7 +41,7 @@ Require Import Op.
Inductive mreg: Type :=
(* Allocatable General Purpose regs. *)
| R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9
- | R10 | R11 | (* R12 | R13 | *) R14 | R15 (* | R16 *) | R17 | R18 | R19
+ | R10 | R11 (* | R12 | R13 | R14 *) | R15 (* | R16 *) | R17 | R18 | R19
| R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29
| R30 | R31 (* | R32 *) | R33 | R34 | R35 | R36 | R37 | R38 | R39
| R40 | R41 | R42 | R43 | R44 | R45 | R46 | R47 | R48 | R49
@@ -54,7 +54,7 @@ Global Opaque mreg_eq.
Definition all_mregs :=
R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9
- :: R10 :: R11 (* :: R12 :: R13 *) :: R14 :: R15 (* :: R16 *) :: R17 :: R18 :: R19
+ :: R10 :: R11 (* :: R12 :: R13 :: R14 *) :: R15 (* :: R16 *) :: R17 :: R18 :: R19
:: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29
:: R30 :: R31 (* :: R32 *) :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39
:: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49
@@ -86,7 +86,7 @@ Module IndexedMreg <: INDEXED_TYPE.
match r with
| R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5
| R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10
- | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 *) | R14 => 15
+ | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 | R14 => 15 *)
| R15 => 16 (* | R16 => 17 *) | R17 => 18 | R18 => 19 | R19 => 20
| R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25
| R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30
@@ -115,7 +115,7 @@ Local Open Scope string_scope.
Definition register_names :=
("R0" , R0) :: ("R1" , R1) :: ("R2" , R2) :: ("R3" , R3) :: ("R4" , R4)
:: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R8" , R8) :: ("R9" , R9)
- :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) *) :: ("R14", R14)
+ :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) :: ("R14", R14) *)
:: ("R15", R15) (* :: ("R16", R16) *) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19)
:: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24)
:: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29)
@@ -174,9 +174,9 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
Definition destroyed_by_setstack (ty: typ): list mreg := nil.
-Definition destroyed_at_function_entry: list mreg := R14 :: nil.
+Definition destroyed_at_function_entry: list mreg := R17 :: nil.
-Definition temp_for_parent_frame: mreg := R14. (* FIXME - ?? *)
+Definition temp_for_parent_frame: mreg := R17. (* Temporary used to store the parent frame, where the arguments are *)
Definition destroyed_at_indirect_call: list mreg := nil.
(* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *)
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 f4732ee4..2c39e342 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -222,6 +222,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
@@ -496,7 +497,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/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 2de49faa..33912203 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -67,8 +67,8 @@ Proof.
erewrite exec_basic_instr_pc; eauto.
Qed.
-Lemma next_eq {A: Type}:
- forall (rs rs':A) m m',
+Lemma next_eq:
+ forall (rs rs': regset) m m',
rs = rs' -> m = m' -> Next rs m = Next rs' m'.
Proof.
intros. congruence.
@@ -136,7 +136,7 @@ Proof.
inv H. apply next_eq; auto. apply functional_extensionality. intros.
rewrite (regset_double_set GPR32 PC); try discriminate.
rewrite (regset_double_set GPR12 PC); try discriminate.
- rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
+ rewrite (regset_double_set FP PC); try discriminate. reflexivity.
- repeat (rewrite Pregmap.gso; try discriminate).
destruct (Mem.loadv _ _ _); try discriminate.
destruct (rs GPR12); try discriminate.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 69824852..d4e2afc9 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-14 02:42:51 +0000