diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/Asmblock.v | 22 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 49 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 7 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 15 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 25 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 3 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | runtime/Makefile | 3 | ||||
| -rw-r--r-- | test/mppa/interop/Makefile | 2 | ||||
| -rw-r--r-- | test/mppa/interop/common.c | 370 | ||||
| -rw-r--r-- | test/mppa/interop/common.h | 2 | ||||
| -rw-r--r-- | test/mppa/interop/framework.h | 35 | ||||
| -rw-r--r-- | test/mppa/interop/stackhell.c | 11 |
17 files changed, 336 insertions, 241 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) -> diff --git a/runtime/Makefile b/runtime/Makefile index f58d4b6a..6be85728 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -24,7 +24,8 @@ else ifeq ($(ARCH),powerpc64) OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),mppa_k1c) OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\ - i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o + i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o\ + i64_shl.o i64_shr.o # Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o DOMAKE:=$(shell (cd mppa_k1c && make)) else diff --git a/test/mppa/interop/Makefile b/test/mppa/interop/Makefile index 5818cbcb..a405ebd6 100644 --- a/test/mppa/interop/Makefile +++ b/test/mppa/interop/Makefile @@ -28,7 +28,7 @@ CCPATH=$(shell which $(CC)) CCOMPPATH=$(shell which $(CCOMP)) SIMUPATH=$(shell which $(SIMU)) -TESTNAMES=$(filter-out $(VAARG_COMMON),$(filter-out $(COMMON),$(notdir $(subst .c,,$(wildcard $(DIR)/*.c))))) +TESTNAMES ?= $(filter-out $(VAARG_COMMON),$(filter-out $(COMMON),$(notdir $(subst .c,,$(wildcard $(DIR)/*.c))))) X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.out,$(TESTNAMES))) GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.out,$(TESTNAMES))) diff --git a/test/mppa/interop/common.c b/test/mppa/interop/common.c index 2b5f5b5e..e939e0d1 100644 --- a/test/mppa/interop/common.c +++ b/test/mppa/interop/common.c @@ -8,9 +8,9 @@ #define MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9,\ a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,\ a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)\ - (a0 + a1 * a2 + a3 * a4 + a5 + a6 + a7 - a8 + a9 +\ - a10 + a11 - a12 ^ a13 + a14 - a15 + a16 ^ a17 + a18 + a19 +\ - a20 + a21 + a22 * a23 + a24 + a25 << a26 & a27 + a28 + a29) + (a0 * a1 * a2 * a3 * a4 * a5 * a6 * a7 * a8 * a9 *\ + a10 * a11 * a12 * a13 * a14 * a15 * a16 * a17 * a18 * a19 *\ + a20 * a21 * a22 * a23 * a24 * a25 * a26 * a27 * a28 * a29) void void_void(){ STACK; @@ -61,193 +61,193 @@ long long ll_manyllargs(char a0, int a1, char a2, long long a3, char a4, char a5 a20, a21, a22, a23, a24, a25, a26, a27, a28, a29); } -long long stackhell(char a0, int a1, char a2, long long a3, char a4, char a5, long long a6, long long a7, char a8, long long a9, - char a10, long long a11, char a12, int a13, char a14, char a15, long long a16, long long a17, char a18, long long a19, - char a20, int a21, char a22, long long a23, char a24, char a25, long long a26, int a27, char a28, long long a29) +double stackhell(char a0, int a1, float a2, long long a3, double a4, char a5, long long a6, long long a7, float a8, long long a9, + double a10, long long a11, char a12, int a13, float a14, double a15, long long a16, long long a17, float a18, long long a19, + char a20, int a21, char a22, long long a23, float a24, char a25, long long a26, int a27, double a28, long long a29) { long long b0 = a0; - long long b1 = a1 + b0; - long long b2 = a2 + b1; - int b3 = a3 + b2; - int b4 = a4 + b3; - int b5 = a5 + b4; - int b6 = a6 + b5; - int b7 = a7 + b6; - char b8 = a8 + b7; - char b9 = a9 + b8; - char b10 = a10 + b9; - char b11 = a11 + b10; - char b12 = a12 + b11; - int b13 = a13 + b12; - long long b14 = a14 + b13; - long long b15 = a15 + b14; - long long b16 = a16 + b15; - long long b17 = a17 + b16; - long long b18 = a18 + b17; - long long b19 = a19 + b18; - long long b20 = a20 + b19; - long long b21 = a21 + b20; - long long b22 = a22 + b21; - long long b23 = a23 + b22; - long long b24 = a24 + b23; - long long b25 = a25 + b24; - long long b26 = a26 + b25; - long long b27 = a27 + b26; - int b28 = a28 + b27; - int b29 = a29 + b28; - int b30 = b0 + b29; - int b31 = b1 + b30; - int b32 = b2 + b31; - char b33 = b3 + b32; - char b34 = b4 + b33; - char b35 = b5 + b34; - char b36 = b6 + b35; - char b37 = b7 + b36; - int b38 = b8 + b37; - int b39 = b9 + b38; - int b40 = b0 + b39; - int b41 = b1 + b40; - int b42 = b2 + b41; - int b43 = b3 + b42; - int b44 = b4 + b43; - int b45 = b5 + b44; - int b46 = b6 + b45; - int b47 = b7 + b46; - int b48 = b8 + b47; - long long b49 = b9 + b48; - long long b50 = b0 + b49; - long long b51 = b1 + b50; - long long b52 = b2 + b51; - long long b53 = b3 + b52; - long long b54 = b4 + b53; - long long b55 = b5 + b54; - long long b56 = b6 + b55; - long long b57 = b7 + b56; - int b58 = b8 + b57; - int b59 = b9 + b58; - int b60 = b0 + b59; - int b61 = b1 + b60; - int b62 = b2 + b61; - int b63 = b3 + b62; - int b64 = b4 + b63; - int b65 = b5 + b64; - int b66 = b6 + b65; - int b67 = b7 + b66; - int b68 = b8 + b67; - int b69 = b9 + b68; - char b70 = b0 + b69; - char b71 = b1 + b70; - char b72 = b2 + b71; - char b73 = b3 + b72; - char b74 = b4 + b73; - char b75 = b5 + b74; - char b76 = b6 + b75; - char b77 = b7 + b76; - char b78 = b8 + b77; - char b79 = b9 + b78; - char b80 = b0 + b79; - char b81 = b1 + b80; - char b82 = b2 + b81; - char b83 = b3 + b82; - char b84 = b4 + b83; - int b85 = b5 + b84; - int b86 = b6 + b85; - int b87 = b7 + b86; - int b88 = b8 + b87; - int b89 = b9 + b88; - int b90 = b0 + b89; - int b91 = b1 + b90; - int b92 = b2 + b91; - int b93 = b3 + b92; - int b94 = b4 + b93; - long long b95 = b5 + b94; - long long b96 = b6 + b95; - long long b97 = b7 + b96; - long long b98 = b8 + b97; - long long b99 = b9 + b98; - long long b100 = b0 + b99; - long long b101 = b1 + b100; - long long b102 = b2 + b101; - long long b103 = b3 + b102; - long long b104 = b4 + b103; - long long b105 = b5 + b104; - long long b106 = b6 + b105; - long long b107 = b7 + b106; - long long b108 = b8 + b107; - long long b109 = b9 + b108; - long long b110 = b0 + b109; - long long b111 = b1 + b110; - long long b112 = b2 + b111; - long long b113 = b3 + b112; - long long b114 = b4 + b113; - int b115 = b5 + b114; - int b116 = b6 + b115; - int b117 = b7 + b116; - int b118 = b8 + b117; - int b119 = b9 + b118; - int b120 = b0 + b119; - int b121 = b1 + b120; - int b122 = b2 + b121; - int b123 = b3 + b122; - int b124 = b4 + b123; - int b125 = b5 + b124; - char b126 = b6 + b125; - char b127 = b7 + b126; - char b128 = b8 + b127; - char b129 = b9 + b128; - char b130 = b0 + b129; - char b131 = b1 + b130; - char b132 = b2 + b131; - char b133 = b3 + b132; - char b134 = b4 + b133; - char b135 = b5 + b134; - char b136 = b6 + b135; - char b137 = b7 + b136; - char b138 = b8 + b137; - char b139 = b9 + b138; - char b140 = b0 + b139; - char b141 = b1 + b140; - char b142 = b2 + b141; - char b143 = b3 + b142; - char b144 = b4 + b143; - char b145 = b5 + b144; - char b146 = b6 + b145; - char b147 = b7 + b146; - int b148 = b8 + b147; - int b149 = b9 + b148; - int b150 = b0 + b149; - int b151 = b1 + b150; - int b152 = b2 + b151; - int b153 = b3 + b152; - int b154 = b4 + b153; - int b155 = b5 + b154; - int b156 = b6 + b155; - int b157 = b7 + b156; - int b158 = b8 + b157; - int b159 = b9 + b158; - int b160 = b0 + b159; - int b161 = b1 + b160; - int b162 = b2 + b161; + long long b1 = a1 * b0; + long long b2 = a2 * b1; + float b3 = a3 * b2; + int b4 = a4 * b3; + double b5 = a5 * b4; + int b6 = a6 * b5; + float b7 = a7 * b6; + char b8 = a8 * b7; + double b9 = a9 * b8; + char b10 = a10 * b9; + float b11 = a11 * b10; + char b12 = a12 * b11; + int b13 = a13 * b12; + long long b14 = a14 * b13; + long long b15 = a15 * b14; + long long b16 = a16 * b15; + long long b17 = a17 * b16; + long long b18 = a18 * b17; + long long b19 = a19 * b18; + long long b20 = a20 * b19; + long long b21 = a21 * b20; + long long b22 = a22 * b21; + long long b23 = a23 * b22; + long long b24 = a24 * b23; + long long b25 = a25 * b24; + long long b26 = a26 * b25; + long long b27 = a27 * b26; + int b28 = a28 * b27; + double b29 = a29 * b28; + float b30 = b0 * b29; + double b31 = b1 * b30; + int b32 = b2 * b31; + char b33 = b3 * b32; + float b34 = b4 * b33; + char b35 = b5 * b34; + double b36 = b6 * b35; + float b37 = b7 * b36; + int b38 = b8 * b37; + double b39 = b9 * b38; + float b40 = b0 * b39; + int b41 = b1 * b40; + double b42 = b2 * b41; + float b43 = b3 * b42; + int b44 = b4 * b43; + double b45 = b5 * b44; + int b46 = b6 * b45; + double b47 = b7 * b46; + int b48 = b8 * b47; + long long b49 = b9 * b48; + long long b50 = b0 * b49; + long long b51 = b1 * b50; + long long b52 = b2 * b51; + long long b53 = b3 * b52; + long long b54 = b4 * b53; + long long b55 = b5 * b54; + long long b56 = b6 * b55; + long long b57 = b7 * b56; + int b58 = b8 * b57; + float b59 = b9 * b58; + int b60 = b0 * b59; + float b61 = b1 * b60; + float b62 = b2 * b61; + int b63 = b3 * b62; + double b64 = b4 * b63; + int b65 = b5 * b64; + int b66 = b6 * b65; + double b67 = b7 * b66; + double b68 = b8 * b67; + int b69 = b9 * b68; + char b70 = b0 * b69; + char b71 = b1 * b70; + double b72 = b2 * b71; + double b73 = b3 * b72; + char b74 = b4 * b73; + float b75 = b5 * b74; + float b76 = b6 * b75; + double b77 = b7 * b76; + char b78 = b8 * b77; + float b79 = b9 * b78; + float b80 = b0 * b79; + char b81 = b1 * b80; + char b82 = b2 * b81; + float b83 = b3 * b82; + char b84 = b4 * b83; + int b85 = b5 * b84; + int b86 = b6 * b85; + double b87 = b7 * b86; + float b88 = b8 * b87; + double b89 = b9 * b88; + int b90 = b0 * b89; + float b91 = b1 * b90; + double b92 = b2 * b91; + int b93 = b3 * b92; + int b94 = b4 * b93; + long long b95 = b5 * b94; + long long b96 = b6 * b95; + long long b97 = b7 * b96; + long long b98 = b8 * b97; + long long b99 = b9 * b98; + long long b100 = b0 * b99; + long long b101 = b1 * b100; + long long b102 = b2 * b101; + long long b103 = b3 * b102; + long long b104 = b4 * b103; + long long b105 = b5 * b104; + long long b106 = b6 * b105; + long long b107 = b7 * b106; + long long b108 = b8 * b107; + long long b109 = b9 * b108; + long long b110 = b0 * b109; + long long b111 = b1 * b110; + long long b112 = b2 * b111; + long long b113 = b3 * b112; + long long b114 = b4 * b113; + int b115 = b5 * b114; + int b116 = b6 * b115; + int b117 = b7 * b116; + float b118 = b8 * b117; + float b119 = b9 * b118; + int b120 = b0 * b119; + double b121 = b1 * b120; + float b122 = b2 * b121; + int b123 = b3 * b122; + double b124 = b4 * b123; + int b125 = b5 * b124; + char b126 = b6 * b125; + double b127 = b7 * b126; + char b128 = b8 * b127; + float b129 = b9 * b128; + char b130 = b0 * b129; + double b131 = b1 * b130; + char b132 = b2 * b131; + float b133 = b3 * b132; + char b134 = b4 * b133; + double b135 = b5 * b134; + char b136 = b6 * b135; + float b137 = b7 * b136; + char b138 = b8 * b137; + double b139 = b9 * b138; + char b140 = b0 * b139; + float b141 = b1 * b140; + char b142 = b2 * b141; + double b143 = b3 * b142; + char b144 = b4 * b143; + float b145 = b5 * b144; + char b146 = b6 * b145; + double b147 = b7 * b146; + int b148 = b8 * b147; + float b149 = b9 * b148; + int b150 = b0 * b149; + double b151 = b1 * b150; + int b152 = b2 * b151; + float b153 = b3 * b152; + int b154 = b4 * b153; + double b155 = b5 * b154; + int b156 = b6 * b155; + float b157 = b7 * b156; + int b158 = b8 * b157; + double b159 = b9 * b158; + int b160 = b0 * b159; + float b161 = b1 * b160; + int b162 = b2 * b161; return MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29) - + b0 + b1 + b2 + b3 + b4 + b5 + b6 + b7 + b8 + b9 - + b10 + b11 + b12 + b13 + b14 + b15 + b16 + b17 + b18 + b19 - + b20 + b21 + b22 + b23 + b24 + b25 + b26 + b27 + b28 + b29 - + b30 + b31 + b32 + b33 + b34 + b35 + b36 + b37 + b38 + b39 - + b40 + b41 + b42 + b43 + b44 + b45 + b46 + b47 + b48 + b49 - + b50 + b51 + b52 + b53 + b54 + b55 + b56 + b57 + b58 + b59 - + b60 + b61 + b62 + b63 + b64 + b65 + b66 + b67 + b68 + b69 - + b70 + b71 + b72 + b73 + b74 + b75 + b76 + b77 + b78 + b79 - + b80 + b81 + b82 + b83 + b84 + b85 + b86 + b87 + b88 + b89 - + b90 + b91 + b92 + b93 + b94 + b95 + b96 + b97 + b98 + b99 - + b100 + b101 + b102 + b103 + b104 + b105 + b106 + b107 + b108 + b109 - + b110 + b111 + b112 + b113 + b114 + b115 + b116 + b117 + b118 + b119 - + b120 + b121 + b122 + b123 + b124 + b125 + b126 + b127 + b128 + b129 - + b130 + b131 + b132 + b133 + b134 + b135 + b136 + b137 + b138 + b139 - + b140 + b141 + b142 + b143 + b144 + b145 + b146 + b147 + b148 + b149 - + b150 + b151 + b152 + b153 + b154 + b155 + b156 + b157 + b158 + b159 - + b160 + b161 + b162 + * b0 * b1 * b2 * b3 * b4 * b5 * b6 * b7 * b8 * b9 + * b10 * b11 * b12 * b13 * b14 * b15 * b16 * b17 * b18 * b19 + * b20 * b21 * b22 * b23 * b24 * b25 * b26 * b27 * b28 * b29 + * b30 * b31 * b32 * b33 * b34 * b35 * b36 * b37 * b38 * b39 + * b40 * b41 * b42 * b43 * b44 * b45 * b46 * b47 * b48 * b49 + * b50 * b51 * b52 * b53 * b54 * b55 * b56 * b57 * b58 * b59 + * b60 * b61 * b62 * b63 * b64 * b65 * b66 * b67 * b68 * b69 + * b70 * b71 * b72 * b73 * b74 * b75 * b76 * b77 * b78 * b79 + * b80 * b81 * b82 * b83 * b84 * b85 * b86 * b87 * b88 * b89 + * b90 * b91 * b92 * b93 * b94 * b95 * b96 * b97 * b98 * b99 + * b100 * b101 * b102 * b103 * b104 * b105 * b106 * b107 * b108 * b109 + * b110 * b111 * b112 * b113 * b114 * b115 * b116 * b117 * b118 * b119 + * b120 * b121 * b122 * b123 * b124 * b125 * b126 * b127 * b128 * b129 + * b130 * b131 * b132 * b133 * b134 * b135 * b136 * b137 * b138 * b139 + * b140 * b141 * b142 * b143 * b144 * b145 * b146 * b147 * b148 * b149 + * b150 * b151 * b152 * b153 * b154 * b155 * b156 * b157 * b158 * b159 + * b160 * b161 * b162 ; } diff --git a/test/mppa/interop/common.h b/test/mppa/interop/common.h index 4e4a692a..055ce7ea 100644 --- a/test/mppa/interop/common.h +++ b/test/mppa/interop/common.h @@ -21,7 +21,7 @@ long long ll_manyllargs(char a0, long long a1, char a2, long long a3, char a4, c char a10, long long a11, char a12, long long a13, char a14, char a15, long long a16, long long a17, char a18, long long a19, char a20, long long a21, char a22, long long a23, char a24, char a25, long long a26, long long a27, char a28, long long a29); -long long stackhell(char a0, long long a1, char a2, long long a3, char a4, char a5, long long a6, long long a7, char a8, long long a9, +double stackhell(char a0, long long a1, char a2, long long a3, char a4, char a5, long long a6, long long a7, char a8, long long a9, char a10, long long a11, char a12, long long a13, char a14, char a15, long long a16, long long a17, char a18, long long a19, char a20, long long a21, char a22, long long a23, char a24, char a25, long long a26, long long a27, char a28, long long a29); diff --git a/test/mppa/interop/framework.h b/test/mppa/interop/framework.h index 52ba97bc..3bbfa271 100644 --- a/test/mppa/interop/framework.h +++ b/test/mppa/interop/framework.h @@ -1,6 +1,7 @@ #ifndef __FRAMEWORK_H__ #define __FRAMEWORK_H__ +#include <stdio.h> #include "../prng/prng.c" #define BEGIN_TEST_N(type, N)\ @@ -16,7 +17,8 @@ #define BEGIN_TEST(type)\ int main(void){\ - type a, b, c, i, S;\ + type a, b, c, S;\ + int i;\ srand(0);\ S = 0;\ for (i = 0 ; i < 100 ; i++){\ @@ -27,11 +29,38 @@ /* In between BEGIN_TEST and END_TEST : definition of c */ -#define END_TEST()\ +#define END_TEST64()\ + printf("%llu\t%llu\t%llu\n", a, b, c);\ S += c;\ }\ return S;\ } - /* END END_TEST */ + /* END END_TEST64 */ + +#define END_TEST32()\ + printf("%u\t%u\t%u\n", a, b, c);\ + S += c;\ + }\ + return S;\ + } + /* END END_TEST32 */ + +#define END_TESTF32()\ + printf("%e\t%e\t%e\n", a, b, c);\ + S += c;\ + }\ + return 0;\ + } + /* END END_TESTF32 */ + +#define END_TESTF64()\ + printf("%e\t%e\t%e\n", a, b, c);\ + S += c;\ + }\ + return 0;\ + } + /* END END_TESTF64 */ #endif + + diff --git a/test/mppa/interop/stackhell.c b/test/mppa/interop/stackhell.c index fbe7d56b..5abaa71d 100644 --- a/test/mppa/interop/stackhell.c +++ b/test/mppa/interop/stackhell.c @@ -1,8 +1,9 @@ #include "framework.h" #include "common.h" -BEGIN_TEST(long long) - c = stackhell(a, b, a-b, a+b, a*2, b*2, a*2-b, a+b*2, (a-b)*2, (a+b)*2, - -2*a, -2*b, a-b, a+b, a*3, b*3, a*3-b, a+b*3, (a-b)*3, (a+b)*3, - -3*a, -3*b, a-b, a+b, a*4, b*4, a*4-b, a+b*4, (a-b)*4, (a+b)*4); -END_TEST() +BEGIN_TEST(double) + c = stackhell(a, b, a*b, a*b, a*2, b*2, a*2*b, a*b*2, (a*b)*2, (a*b)*2, + 2*a, 2*b, a*b, a*b, a*3, b*3, a*3*b, a*b*3, (a*b)*3, (a*b)*3, + 3*a, 3*b, a*b, a*b, a*4, b*4, a*4*b, a*b*4, (a*b)*4, (a*b)*4); + +END_TESTF64() |