diff options
34 files changed, 797 insertions, 1659 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9128e188..f0ae4367 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1214,8 +1214,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i64_" -let re_runtime32 = Str.regexp "__compcert_i32_" +let re_runtime = Str.regexp "__compcert_i" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1228,8 +1227,9 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else - if Str.string_match re_runtime32 id.name 0 then AST.EF_runtime(id'', sg) else + if Str.string_match re_runtime id.name 0 + then AST.EF_runtime(id'', sg) + else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.Builtins.functions then AST.EF_builtin(id'', sg) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 8486e25d..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)
@@ -148,6 +151,7 @@ Inductive instruction : Type := | Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
+ | Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
| Psubl (rd rs1 rs2: ireg) (**r sub long *)
@@ -163,6 +167,7 @@ Inductive instruction : Type := | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
| Pfaddw (rd rs1 rs2: ireg) (**r Float addition word *)
@@ -175,6 +180,7 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *)
| Paddiw (rd rs: ireg) (imm: int) (**r add imm word *)
+ | Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *)
| Pandiw (rd rs: ireg) (imm: int) (**r and imm word *)
| Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
| Poriw (rd rs: ireg) (imm: int) (**r or imm word *)
@@ -187,6 +193,7 @@ Inductive instruction : Type := | Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
| Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
+ | Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -194,6 +201,7 @@ Inductive instruction : Type := (** Arith RRI64 *)
| Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *)
| Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *)
+ | Pmulil (rd rs: ireg) (imm: int64) (**r add immediate long *)
| Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Poril (rd rs: ireg) (imm: int64) (**r or immediate long *)
@@ -202,13 +210,16 @@ Inductive instruction : Type := | Pnxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
| Pandnil (rd rs: ireg) (imm: int64) (**r andn long *)
| Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
- .
+ | Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
+.
(** Correspondance between Asmblock and Asm *)
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
@@ -315,6 +326,7 @@ Definition basic_to_instruction (b: basic) := (* RRI32 *)
| PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
| PArithRRI32 Asmblock.Paddiw rd rs imm => Paddiw rd rs imm
+ | PArithRRI32 Asmblock.Pmuliw rd rs imm => Pmuliw rd rs imm
| PArithRRI32 Asmblock.Pandiw rd rs imm => Pandiw rd rs imm
| PArithRRI32 Asmblock.Pnandiw rd rs imm => Pnandiw rd rs imm
| PArithRRI32 Asmblock.Poriw rd rs imm => Poriw rd rs imm
@@ -334,6 +346,7 @@ Definition basic_to_instruction (b: basic) := (* RRI64 *)
| PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm
| PArithRRI64 Asmblock.Paddil rd rs imm => Paddil rd rs imm
+ | PArithRRI64 Asmblock.Pmulil rd rs imm => Pmulil rd rs imm
| PArithRRI64 Asmblock.Pandil rd rs imm => Pandil rd rs imm
| PArithRRI64 Asmblock.Pnandil rd rs imm => Pnandil rd rs imm
| PArithRRI64 Asmblock.Poril rd rs imm => Poril rd rs imm
@@ -343,6 +356,16 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmblock.Pandnil rd rs imm => Pandnil rd rs imm
| PArithRRI64 Asmblock.Pornil rd rs imm => Pornil rd rs imm
+ (** ARRR *)
+ | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
+ | PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+
+ (** ARRI32 *)
+ | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
+
+ (** ARRI64 *)
+ | PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
+
(** Load *)
| PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs
| PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra ofs
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index cdbe4eb3..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 ! @@ -376,6 +379,7 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) + | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) | Pnandiw (**r nand imm word *) | Poriw (**r or imm word *) @@ -396,6 +400,7 @@ Inductive arith_name_rri32 : Type := Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) + | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) | Poril (**r or immediate long *) @@ -406,6 +411,19 @@ Inductive arith_name_rri64 : Type := | Pornil (**r orn immediate long *) . +Inductive arith_name_arrr : Type := + | Pmaddw (**r multiply add word *) + | Pmaddl (**r multiply add long *) +. + +Inductive arith_name_arri32 : Type := + | Pmaddiw (**r multiply add word *) +. + +Inductive arith_name_arri64 : Type := + | Pmaddil (**r multiply add long *) +. + Inductive ar_instruction : Type := | PArithR (i: arith_name_r) (rd: ireg) | PArithRR (i: arith_name_rr) (rd rs: ireg) @@ -416,6 +434,9 @@ Inductive ar_instruction : Type := | PArithRRR (i: arith_name_rrr) (rd rs1 rs2: ireg) | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int) | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64) + | PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg) + | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int) + | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . Coercion PArithR: arith_name_r >-> Funclass. @@ -427,6 +448,9 @@ Coercion PArithRF64: arith_name_rf64 >-> Funclass. Coercion PArithRRR: arith_name_rrr >-> Funclass. Coercion PArithRRI32: arith_name_rri32 >-> Funclass. Coercion PArithRRI64: arith_name_rri64 >-> Funclass. +Coercion PArithARRR: arith_name_arrr >-> Funclass. +Coercion PArithARRI32: arith_name_arri32 >-> Funclass. +Coercion PArithARRI64: arith_name_arri64 >-> Funclass. Inductive basic : Type := | PArith (i: ar_instruction) @@ -522,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. @@ -1149,6 +1172,7 @@ Definition arith_eval_rri32 n v i := match n with | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) + | Pmuliw => Val.mul v (Vint i) | Pandiw => Val.and v (Vint i) | Pnandiw => Val.notint (Val.and v (Vint i)) | Poriw => Val.or v (Vint i) @@ -1170,6 +1194,7 @@ Definition arith_eval_rri64 n v i := match n with | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) + | Pmulil => Val.mull v (Vlong i) | Pandil => Val.andl v (Vlong i) | Pnandil => Val.notl (Val.andl v (Vlong i)) | Poril => Val.orl v (Vlong i) @@ -1180,6 +1205,22 @@ Definition arith_eval_rri64 n v i := | Pornil => Val.orl (Val.notl v) (Vlong i) end. +Definition arith_eval_arrr n v1 v2 v3 := + match n with + | Pmaddw => Val.add v1 (Val.mul v2 v3) + | Pmaddl => Val.addl v1 (Val.mull v2 v3) + end. + +Definition arith_eval_arri32 n v1 v2 v3 := + match n with + | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3)) + end. + +Definition arith_eval_arri64 n v1 v2 v3 := + match n with + | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3)) + end. + Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithR n d => rs#d <- (arith_eval_r n) @@ -1196,6 +1237,12 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i) | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i) + + | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2) + + | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i) + + | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i) end. (** * load/store *) @@ -1436,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. @@ -1461,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 d69903b4..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) . @@ -52,6 +54,9 @@ Inductive arith_op := | OArithRRR (n: arith_name_rrr) | OArithRRI32 (n: arith_name_rri32) (imm: int) | OArithRRI64 (n: arith_name_rri64) (imm: int64) + | OArithARRR (n: arith_name_arrr) + | OArithARRI32 (n: arith_name_arri32) (imm: int) + | OArithARRI64 (n: arith_name_arri64) (imm: int64) . Coercion OArithR: arith_name_r >-> arith_op. @@ -109,10 +114,13 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i)) | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2)) - | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i)) | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i)) + | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3)) + | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i)) + | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i)) + | _, _ => None end. @@ -185,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 @@ -270,17 +288,31 @@ Definition iandb (ib1 ib2: ?? bool): ?? bool := RET (andb b1 b2). Definition arith_op_eq (o1 o2: arith_op): ?? bool := - match o1, o2 with - | OArithR n1, OArithR n2 => struct_eq n1 n2 - | OArithRR n1, OArithRR n2 => phys_eq n1 n2 - | OArithRI32 n1 i1, OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRI64 n1 i1, OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRF32 n1 i1, OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRF64 n1 i1, OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRRR n1, OArithRRR n2 => phys_eq n1 n2 - | OArithRRI32 n1 i1, OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRRI64 n1 i1, OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | _, _ => RET false + match o1 with + | OArithR n1 => + match o2 with OArithR n2 => struct_eq n1 n2 | _ => RET false end + | OArithRR n1 => + match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRI32 n1 i1 => + match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRI64 n1 i1 => + match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF32 n1 i1 => + match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF64 n1 i1 => + match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRR n1 => + match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRRI32 n1 i1 => + match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRI64 n1 i1 => + match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRR n1 => + match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithARRI32 n1 i1 => + match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRI64 n1 i1 => + match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end end. Lemma arith_op_eq_correct o1 o2: @@ -317,12 +349,15 @@ Proof. apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. Qed. - +(* TODO: rewrite control_op_eq in a robust style against the miss of a case + cf. arith_op_eq above *) Definition control_op_eq (c1 c2: control_op): ?? bool := match c1, c2 with | 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 @@ -339,6 +374,8 @@ Proof. Qed. +(* TODO: rewrite op_eq in a robust style against the miss of a case + cf. arith_op_eq above *) Definition op_eq (o1 o2: op): ?? bool := match o1, o2 with | Arith i1, Arith i2 => arith_op_eq i1 i2 @@ -375,13 +412,12 @@ Qed. (* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. - Theorem op_eq_correct o1 o2: WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. Proof. wlp_simplify. Qed. - *) +*) End IMPPARAM. @@ -504,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. @@ -525,6 +563,9 @@ Definition trans_arith (ai: ar_instruction) : macro := | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))] | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))] | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))] + | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (Name(#d) @ Name (#s1) @ Name (#s2) @ Enil))] + | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (Name(#d) @ Name (#s) @ Enil))] + | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (Name(#d) @ Name (#s) @ Enil))] end. @@ -711,6 +752,27 @@ Proof. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRR *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs1); rewrite e0. pose (H1 rs2); rewrite e1. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI32 *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI64 *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. Qed. Lemma forward_simu_basic: @@ -750,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. @@ -758,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. @@ -801,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. @@ -992,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. @@ -1103,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. @@ -1336,6 +1425,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" + | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" | Poriw => "Poriw" @@ -1357,6 +1447,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" + | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" | Poril => "Poril" @@ -1367,6 +1458,22 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pornil => "Pornil" end. +Definition string_of_name_arrr (n: arith_name_arrr): pstring := + match n with + | Pmaddw => "Pmaddw" + | Pmaddl => "Pmaddl" + end. + +Definition string_of_name_arri32 (n: arith_name_arri32): pstring := + match n with + | Pmaddiw => "Pmaddw" + end. + +Definition string_of_name_arri64 (n: arith_name_arri64): pstring := + match n with + | Pmaddil => "Pmaddl" + end. + Definition string_of_arith (op: arith_op): pstring := match op with | OArithR n => string_of_name_r n @@ -1378,6 +1485,9 @@ Definition string_of_arith (op: arith_op): pstring := | OArithRRR n => string_of_name_rrr n | OArithRRI32 n _ => string_of_name_rri32 n | OArithRRI64 n _ => string_of_name_rri64 n + | OArithARRR n => string_of_name_arrr n + | OArithARRI32 n _ => string_of_name_arri32 n + | OArithARRI64 n _ => string_of_name_arri64 n end. Definition string_of_name_lrro (n: load_name_rro) : pstring := @@ -1421,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 87df237c..5b00a64f 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 @@ -85,6 +83,7 @@ Definition opimm32 (op: arith_name_rrr) end. Definition addimm32 := opimm32 Paddw Paddiw. +Definition mulimm32 := opimm32 Pmulw Pmuliw. Definition andimm32 := opimm32 Pandw Pandiw. Definition nandimm32 := opimm32 Pnandw Pnandiw. Definition orimm32 := opimm32 Porw Poriw. @@ -109,6 +108,7 @@ Definition opimm64 (op: arith_name_rrr) end. Definition addimm64 := opimm64 Paddl Paddil. +Definition mulimm64 := opimm64 Pmull Pmulil. Definition orimm64 := opimm64 Porl Poril. Definition andimm64 := opimm64 Pandl Pandil. Definition xorimm64 := opimm64 Pxorl Pxoril. @@ -420,6 +420,9 @@ Definition transl_op | Omul, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulw rd rs1 rs2 ::i k) + | Omulimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + 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.") @@ -513,7 +516,17 @@ Definition transl_op | Ororimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Proriw rd rs n ::i k) - + | Omadd, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmaddw r1 r2 r3 ::i k) + | Omaddimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + OK (Pmaddiw r1 r2 n ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -541,6 +554,9 @@ Definition transl_op | Omull, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmull rd rs1 rs2 ::i k) + | Omullimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + OK (mulimm64 rd rs1 n ::i k) | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *) | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *) | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *) @@ -623,7 +639,17 @@ Definition transl_op Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i Paddl RTMP rs RTMP ::i Psrail rd RTMP n ::i k) - + | Omaddl, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmaddl r1 r2 r3 ::i k) + | Omaddlimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + OK (Pmaddil r1 r2 n ::i k) | Oabsf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfabsd rd rs ::i k) @@ -962,7 +988,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. @@ -972,7 +998,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 1c1930da..4de37af4 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. *) @@ -210,7 +210,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 12d7a4f7..2577370c 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -25,6 +25,7 @@ Require Import NeedDomain. Definition op1 (nv: nval) := nv :: nil. Definition op2 (nv: nval) := nv :: nv :: nil. +Definition op3 (nv: nval) := nv :: nv :: nv :: nil. Definition needs_of_condition (cond: condition): list nval := nil. @@ -44,6 +45,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oneg => op1 (modarith nv) | Osub => op2 (default nv) | Omul => op2 (modarith nv) + | Omulimm _ => op1 (modarith nv) | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) | Oand => op2 (bitwise nv) | Oandimm n => op1 (andimm nv n) @@ -68,6 +70,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ororimm n => op1 (ror nv n) | Oshruimm n => op1 (shruimm nv n) | Oshrximm n => op1 (default nv) + | Omadd => op3 (modarith nv) + | Omaddimm n => op2 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) @@ -77,6 +81,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegl => op1 (default nv) | Osubl => op2 (default nv) | Omull => op2 (default nv) + | Omullimm _ => op1 (default nv) | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv) | Oandl => op2 (default nv) | Oandlimm n => op1 (default nv) @@ -100,6 +105,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrlimm n => op1 (default nv) | Oshrluimm n => op1 (default nv) | Oshrxlimm n => op1 (default nv) + | Omaddl => op3 (default nv) + | Omaddlimm n => op2 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -151,6 +158,39 @@ Proof. eapply default_needs_of_condition_sound; eauto. Qed. +Lemma addl_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.addl v1 v2) (Val.addl w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.addl. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial. + - apply Val.addl_lessdef; trivial. +Qed. + + +Lemma mull_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.mull v1 v2) (Val.mull w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.mull. + destruct v1; destruct v2; trivial. + - unfold Val.mull. + destruct v1; destruct v2; trivial. + inv H. inv H0. + trivial. +Qed. + +Remark default_idem: forall nv, default (default nv) = default nv. +Proof. + destruct nv; simpl; trivial. +Qed. + Lemma needs_of_operation_sound: forall op args v nv args', eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> @@ -168,6 +208,7 @@ Proof. - apply add_sound; auto with na. - apply neg_sound; auto. - apply mul_sound; auto. +- apply mul_sound; auto with na. - apply and_sound; auto. - apply andimm_sound; auto. - apply notint_sound; apply and_sound; auto. @@ -189,6 +230,14 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply ror_sound; auto. + (* madd *) +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. + (* maddl *) +- apply addl_sound; trivial. + apply mull_sound; trivial. + rewrite default_idem; trivial. + rewrite default_idem; trivial. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 04ea8945..c4338857 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -70,6 +70,7 @@ Inductive operation : Type := | Oneg (**r [rd = - r1] *) | Osub (**r [rd = r1 - r2] *) | Omul (**r [rd = r1 * r2] *) + | Omulimm (n: int) (**r [rd = r1 * n] *) | Omulhs (**r [rd = high part of r1 * r2, signed] *) | Omulhu (**r [rd = high part of r1 * r2, unsigned] *) | Odiv (**r [rd = r1 / r2] (signed) *) @@ -101,6 +102,8 @@ Inductive operation : Type := | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Ororimm (n: int) (**r rotate right immediate *) + | Omadd (**r [rd = rd + r1 * r2] *) + | Omaddimm (n: int) (**r [rd = rd + r1 * imm] *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -112,6 +115,7 @@ Inductive operation : Type := | Onegl (**r [rd = - r1] *) | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) + | Omullimm (n: int64) (**r [rd = r1 * n] *) | Omullhs (**r [rd = high part of r1 * r2, signed] *) | Omullhu (**r [rd = high part of r1 * r2, unsigned] *) | Odivl (**r [rd = r1 / r2] (signed) *) @@ -142,6 +146,8 @@ Inductive operation : Type := | Oshrlu (**r [rd = r1 >> r2] (unsigned) *) | Oshrluimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) + | Omaddl (**r [rd = rd + r1 * r2] *) + | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -262,6 +268,7 @@ Definition eval_operation | Oneg, v1 :: nil => Some (Val.neg v1) | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) + | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n)) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 @@ -293,6 +300,9 @@ Definition eval_operation | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2) | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n)) | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) + | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) + | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) | Ohighlong, v1::nil => Some (Val.hiword v1) @@ -303,6 +313,7 @@ Definition eval_operation | Onegl, v1::nil => Some (Val.negl v1) | Osubl, v1::v2::nil => Some (Val.subl v1 v2) | Omull, v1::v2::nil => Some (Val.mull v1 v2) + | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) | Odivl, v1::v2::nil => Val.divls v1 v2 @@ -333,6 +344,9 @@ Definition eval_operation | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) + | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) + | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) + | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) | Oaddf, v1::v2::nil => Some (Val.addf v1 v2) @@ -441,6 +455,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oneg => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) + | Omulimm _ => (Tint :: nil, Tint) | Omulhs => (Tint :: Tint :: nil, Tint) | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) @@ -472,6 +487,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshruimm _ => (Tint :: nil, Tint) | Oshrximm _ => (Tint :: nil, Tint) | Ororimm _ => (Tint :: nil, Tint) + | Omadd => (Tint :: Tint :: Tint :: nil, Tint) + | Omaddimm _ => (Tint :: Tint :: nil, Tint) + | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) @@ -482,6 +500,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Onegl => (Tlong :: nil, Tlong) | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) + | Omullimm _ => (Tlong :: nil, Tlong) | Omullhs => (Tlong :: Tlong :: nil, Tlong) | Omullhu => (Tlong :: Tlong :: nil, Tlong) | Odivl => (Tlong :: Tlong :: nil, Tlong) @@ -512,6 +531,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrlu => (Tlong :: Tint :: nil, Tlong) | Oshrluimm _ => (Tlong :: nil, Tlong) | Oshrxlimm _ => (Tlong :: nil, Tlong) + | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) + | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) + | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -601,8 +623,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) @@ -654,6 +677,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... (* shrimm *) - destruct v0; simpl... + (* madd *) + - destruct v0; destruct v1; destruct v2... + - destruct v0; destruct v1... (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -671,6 +697,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) @@ -720,6 +747,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... + (* maddl, maddlim *) + - destruct v0; destruct v1; destruct v2; simpl; trivial. + destruct Archi.ptr64; simpl; trivial. + - destruct v0; destruct v1; simpl; trivial. + destruct Archi.ptr64; simpl; trivial. (* negf, absf *) - destruct v0... - destruct v0... @@ -1095,8 +1127,9 @@ Proof. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* div, divu *) @@ -1153,6 +1186,9 @@ Proof. destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. (* rorimm *) - inv H4; simpl; auto. + (* madd, maddim *) + - inv H2; inv H3; inv H4; simpl; auto. + - inv H2; inv H4; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1168,6 +1204,7 @@ Proof. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* divl, divlu *) @@ -1222,6 +1259,13 @@ Proof. (* shrx *) - inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. + + (* maddl, maddlimm *) + - apply Val.addl_inject; auto. + inv H2; inv H3; inv H4; simpl; auto. + - apply Val.addl_inject; auto. + inv H4; inv H2; simpl; auto. + (* negf, absf *) - inv H4; simpl; auto. - inv H4; simpl; auto. diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index b5d55ad3..6700e684 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -118,7 +118,7 @@ Proof. destruct hdb. - destruct exb. + destruct c. - * destruct i. monadInv H. + * destruct i; monadInv H; split; auto. * monadInv H. split; auto. + monadInv H. split; auto. - monadInv H. @@ -131,7 +131,8 @@ Proof. destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *. destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2). - destruct c. - + destruct i; try (monadInv EQ2). + + destruct i; monadInv EQ2; + unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity. + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity. - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity. Qed. @@ -144,7 +145,7 @@ Proof. unfold concat2 in H. simpl in H. monadInv H. destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'. - destruct c. - + destruct i; discriminate. + + destruct i; try discriminate; congruence. + congruence. - congruence. Qed. @@ -259,7 +260,7 @@ Proof. destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *. destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'. - destruct c. - + destruct i. discriminate. + + destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity. + inv EQ2. unfold stick_header; simpl. reflexivity. - inv EQ2. unfold stick_header; simpl. reflexivity. Qed. @@ -393,9 +394,9 @@ Definition verified_schedule (bb : bblock) : res (list bblock) := Lemma verified_schedule_size: forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb. Proof. - intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (apply verified_schedule_nob_size; auto; fail). - destruct i. inv H. simpl. omega. + inv H. simpl. omega. Qed. Lemma verified_schedule_no_header_in_middle: @@ -403,9 +404,9 @@ Lemma verified_schedule_no_header_in_middle: verified_schedule bb = OK lbb -> Forall (fun b => header b = nil) (tail lbb). Proof. - intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail). - destruct i. inv H. simpl. auto. + inv H. simpl. auto. Qed. Lemma verified_schedule_header: @@ -414,9 +415,9 @@ Lemma verified_schedule_header: header bb = header tbb /\ Forall (fun b => header b = nil) lbb. Proof. - intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (eapply verified_schedule_nob_header; eauto; fail). - destruct i. inv H. split; simpl; auto. + inv H. split; simpl; auto. Qed. @@ -443,9 +444,9 @@ Theorem verified_schedule_correct: concat_all lbb = OK tbb /\ bblock_equiv ge f bb tbb. Proof. - intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (eapply verified_schedule_nob_correct; eauto; fail). - destruct i. inv H. eexists. split; simpl; auto. constructor; auto. + inv H. eexists. split; simpl; auto. constructor; auto. Qed. Lemma verified_schedule_builtin_idem: diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index ce2fb2ae..2c39e342 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -95,6 +95,7 @@ let arith_rrr_str = function let arith_rri32_str = function | Pcompiw it -> "Pcompiw" | Paddiw -> "Paddiw" + | Pmuliw -> "Pmuliw" | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" | Poriw -> "Poriw" @@ -114,6 +115,7 @@ let arith_rri32_str = function let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" + | Pmulil -> "Pmulil" | Pandil -> "Pandil" | Pnandil -> "Pnandil" | Poril -> "Poril" @@ -123,6 +125,10 @@ let arith_rri64_str = function | Pandnil -> "Pandnil" | Pornil -> "Pornil" +let arith_arrr_str = function + | Pmaddw -> "Pmaddw" + | Pmaddl -> "Pmaddl" + let arith_ri32_str = "Pmake" let arith_ri64_str = "Pmakel" @@ -162,6 +168,12 @@ let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_str i; write_locs = [Re let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false} +let arith_arri32_rec i rd rs imm32 = { inst = "Pmaddiw"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm32; is_control = false } + +let arith_arri64_rec i rd rs imm64 = { inst = "Pmaddil"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false } + +let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false} + let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false} let arith_r_rec i rd = match i with @@ -173,6 +185,10 @@ let arith_rec i = | PArithRRI32 (i, rd, rs, imm32) -> arith_rri32_rec i (IR rd) (IR rs) (Some (I32 imm32)) | PArithRRI64 (i, rd, rs, imm64) -> arith_rri64_rec i (IR rd) (IR rs) (Some (I64 imm64)) | PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2) + (* Seems like single constant constructor types are elided *) + | PArithARRI32 ((* i,*) rd, rs, imm32) -> arith_arri32_rec () (IR rd) (IR rs) (Some (I32 imm32)) + | PArithARRI64 ((* i,*) rd, rs, imm64) -> arith_arri64_rec () (IR rd) (IR rs) (Some (I64 imm64)) + | PArithARRR (i, rd, rs1, rs2) -> arith_arrr_rec i (IR rd) (IR rs1) (IR rs2) | PArithRI32 (rd, imm32) -> { inst = arith_ri32_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false} | PArithRI64 (rd, imm64) -> { inst = arith_ri64_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false} | PArithRF32 (rd, f) -> { inst = arith_rf32_str; write_locs = [Reg (IR rd)]; read_locs = []; @@ -206,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 @@ -399,6 +416,7 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd + | Maddw | Maddd | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -422,8 +440,8 @@ let ab_inst_to_real = function | "Pcompl" | "Pcompil" -> Compd | "Pfcompw" -> Fcompw | "Pfcompl" -> Fcompd - | "Pmulw" -> Mulw - | "Pmull" -> Muld + | "Pmulw" | "Pmuliw" -> Mulw + | "Pmull" | "Pmulil" -> Muld | "Porw" | "Poriw" -> Orw | "Pnorw" | "Pnoriw" -> Norw | "Porl" | "Poril" -> Ord @@ -436,6 +454,7 @@ let ab_inst_to_real = function | "Psrll" | "Psrlil" -> Srld | "Psllw" | "Pslliw" -> Sllw | "Proriw" -> Rorw + | "Pmaddw" | "Pmaddiw" -> Maddw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw @@ -445,6 +464,7 @@ let ab_inst_to_real = function | "Pnxorl" | "Pnxoril" -> Nxord | "Pandnl" | "Pandnil" -> Andnd | "Pornl" | "Pornil" -> Ornd + | "Pmaddl" -> Maddd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Psxwd" -> Sxwd @@ -477,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 @@ -506,11 +526,13 @@ let rec_to_usage r = (* I do not know yet in which context Ofslow can be used by CompCert *) and real_inst = ab_inst_to_real r.inst in match real_inst with - | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> + | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw + | Nxorw | Andnw | Ornw -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) - | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> + | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord + | Nxord | Andnd | Ornd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) @@ -530,10 +552,10 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y | _ -> raise InvalidEncoding) - | Mulw -> (match encoding with None -> mau + | Mulw| Maddw -> (match encoding with None -> mau | Some U6 | Some S10 | Some U27L5 -> mau_x | _ -> raise InvalidEncoding) - | Muld -> (match encoding with None | Some U6 | Some S10 -> mau + | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop @@ -566,7 +588,7 @@ let real_inst_to_latency = function | Sxwd | Zxwd | Fcompw | Fcompd -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 - | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) + | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 3 | Sb | Sh | Sw | Sd -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 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/SelectLong.vp b/mppa_k1c/SelectLong.vp index 07ebf1a2..3a17ab17 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -88,6 +88,14 @@ Nondetfunction addl (e1: expr) (e2: expr) := addlimm n1 (Eop Oaddl (t1:::t2:::Enil)) | t1, Eop (Oaddlimm n2) (t2:::Enil) => addlimm n2 (Eop Oaddl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omaddl (t1:::t2:::t3:::Enil) + | (Eop Omull (t2:::t3:::Enil)), t1 => + Eop Omaddl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Omullimm n) (t2:::Enil)), t1 => + Eop (Omaddlimm n) (t1:::t2:::Enil) | _, _ => Eop Oaddl (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 27681875..4723278a 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -185,6 +185,10 @@ Proof. with (Val.addl (Val.addl x v1) (Vlong n2)). apply eval_addlimm. EvalOp. repeat rewrite Val.addl_assoc. reflexivity. + - subst. TrivialExists. + - subst. rewrite Val.addl_commut. TrivialExists. + - subst. TrivialExists. + - subst. rewrite Val.addl_commut. TrivialExists. - TrivialExists. Qed. diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v deleted file mode 100644 index cab3259b..00000000 --- a/mppa_k1c/SelectOp.v +++ /dev/null @@ -1,1370 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* The contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) - - -(** Instruction selection for operators *) - -(** The instruction selection pass recognizes opportunities for using - combined arithmetic and logical operations and addressing modes - offered by the target processor. For instance, the expression [x + 1] - can take advantage of the "immediate add" instruction of the processor, - and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned - into a "rotate and mask" instruction. - - This file defines functions for building CminorSel expressions and - statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. - - On top of the "smart constructor" functions defined below, - module [Selection] implements the actual instruction selection pass. -*) - -Require Archi. -Require Import Coqlib. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. - -Local Open Scope cminorsel_scope. - -Local Open Scope string_scope. -Local Open Scope error_monad_scope. - -Section SELECT. -(** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following type class collects - the names of these functions. *) - -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. - -Class helper_functions := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_umulh: ident; (**r unsigned multiply high *) - i64_smulh: ident; (**r signed multiply high *) - i32_sdiv: ident; (**r signed division *) - i32_udiv: ident; (**r unsigned division *) - i32_smod: ident; (**r signed remainder *) - i32_umod: ident; (**r unsigned remainder *) -}. - -Context {hf: helper_functions}. - -Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. - -(** ** Constants **) - -Definition addrsymbol (id: ident) (ofs: ptrofs) := - Eop (Oaddrsymbol id ofs) Enil. - -Definition addrstack (ofs: ptrofs) := - Eop (Oaddrstack ofs) Enil. - -(** ** Integer addition and pointer addition *) - -(** Original definition: -<< -Nondetfunction addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match e with - | Eop (Ointconst m) Enil => Eop (Ointconst (Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | _ => Eop (Oaddimm n) (e ::: Enil) - end. ->> -*) - -Inductive addimm_cases: forall (e: expr), Type := - | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil) - | addimm_case2: forall s m, addimm_cases (Eop (Oaddrsymbol s m) Enil) - | addimm_case3: forall m, addimm_cases (Eop (Oaddrstack m) Enil) - | addimm_case4: forall m t, addimm_cases (Eop (Oaddimm m) (t ::: Enil)) - | addimm_default: forall (e: expr), addimm_cases e. - -Definition addimm_match (e: expr) := - match e as zz1 return addimm_cases zz1 with - | Eop (Ointconst m) Enil => addimm_case1 m - | Eop (Oaddrsymbol s m) Enil => addimm_case2 s m - | Eop (Oaddrstack m) Enil => addimm_case3 m - | Eop (Oaddimm m) (t ::: Enil) => addimm_case4 m t - | e => addimm_default e - end. - -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else match addimm_match e with - | addimm_case1 m => (* Eop (Ointconst m) Enil *) - Eop (Ointconst (Int.add n m)) Enil - | addimm_case2 s m => (* Eop (Oaddrsymbol s m) Enil *) - Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | addimm_case3 m => (* Eop (Oaddrstack m) Enil *) - Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | addimm_case4 m t => (* Eop (Oaddimm m) (t ::: Enil) *) - Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | addimm_default e => - Eop (Oaddimm n) (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction add (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => - Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil) - | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => - Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) - | Eop (Oaddimm n1) (t1:::Enil), t2 => - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | _, _ => Eop Oadd (e1:::e2:::Enil) - end. ->> -*) - -Inductive add_cases: forall (e1: expr) (e2: expr), Type := - | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2) - | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil) - | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case4: forall n1 t1 n2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddrstack n2) Enil) - | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2. - -Definition add_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case3 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => add_case4 n1 t1 n2 - | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2 - | e1, e2 => add_default e1 e2 - end. - -Definition add (e1: expr) (e2: expr) := - match add_match e1 e2 with - | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - addimm n1 t2 - | add_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm n2 t1 - | add_case3 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | add_case4 n1 t1 n2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil *) - Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil) - | add_case5 n1 n2 t2 => (* Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) *) - Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) - | add_case6 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | add_default e1 e2 => - Eop Oadd (e1:::e2:::Enil) - end. - - -(** ** Integer and pointer subtraction *) - -(** Original definition: -<< -Nondetfunction sub (e1: expr) (e2: expr) := - match e1, e2 with - | t1, Eop (Ointconst n2) Enil => - addimm (Int.neg n2) t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), t2 => - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | _, _ => Eop Osub (e1:::e2:::Enil) - end. ->> -*) - -Inductive sub_cases: forall (e1: expr) (e2: expr), Type := - | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil) - | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case3: forall n1 t1 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2. - -Definition sub_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with - | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => sub_case2 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => sub_case3 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => sub_case4 t1 n2 t2 - | e1, e2 => sub_default e1 e2 - end. - -Definition sub (e1: expr) (e2: expr) := - match sub_match e1 e2 with - | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm (Int.neg n2) t1 - | sub_case2 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case3 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | sub_case4 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | sub_default e1 e2 => - Eop Osub (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction negint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil - | _ => Eop Oneg (e ::: Enil) - end. ->> -*) - -Inductive negint_cases: forall (e: expr), Type := - | negint_case1: forall n, negint_cases (Eop (Ointconst n) Enil) - | negint_default: forall (e: expr), negint_cases e. - -Definition negint_match (e: expr) := - match e as zz1 return negint_cases zz1 with - | Eop (Ointconst n) Enil => negint_case1 n - | e => negint_default e - end. - -Definition negint (e: expr) := - match negint_match e with - | negint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.neg n)) Enil - | negint_default e => - Eop Oneg (e ::: Enil) - end. - - -(** ** Immediate shifts *) - -(** Original definition: -<< -Nondetfunction shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shl n1 n)) Enil - | Eop (Oshlimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshlimm n) (e1:::Enil) - | _ => - Eop (Oshlimm n) (e1:::Enil) - end. ->> -*) - -Inductive shlimm_cases: forall (e1: expr) , Type := - | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil) - | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil)) - | shlimm_default: forall (e1: expr) , shlimm_cases e1. - -Definition shlimm_match (e1: expr) := - match e1 as zz1 return shlimm_cases zz1 with - | Eop (Ointconst n1) Enil => shlimm_case1 n1 - | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1 - | e1 => shlimm_default e1 - end. - -Definition shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shlimm_match e1 with - | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shl n1 n)) Enil - | shlimm_case2 n1 t1 => (* Eop (Oshlimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil) - | shlimm_default e1 => - Eop (Oshlimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shru n1 n)) Enil - | Eop (Oshruimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshruimm n) (e1:::Enil) - | _ => - Eop (Oshruimm n) (e1:::Enil) - end. ->> -*) - -Inductive shruimm_cases: forall (e1: expr) , Type := - | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil) - | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil)) - | shruimm_default: forall (e1: expr) , shruimm_cases e1. - -Definition shruimm_match (e1: expr) := - match e1 as zz1 return shruimm_cases zz1 with - | Eop (Ointconst n1) Enil => shruimm_case1 n1 - | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1 - | e1 => shruimm_default e1 - end. - -Definition shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shruimm_match e1 with - | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shru n1 n)) Enil - | shruimm_case2 n1 t1 => (* Eop (Oshruimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil) - | shruimm_default e1 => - Eop (Oshruimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shr n1 n)) Enil - | Eop (Oshrimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshrimm n) (e1:::Enil) - | _ => - Eop (Oshrimm n) (e1:::Enil) - end. ->> -*) - -Inductive shrimm_cases: forall (e1: expr) , Type := - | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil) - | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil)) - | shrimm_default: forall (e1: expr) , shrimm_cases e1. - -Definition shrimm_match (e1: expr) := - match e1 as zz1 return shrimm_cases zz1 with - | Eop (Ointconst n1) Enil => shrimm_case1 n1 - | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1 - | e1 => shrimm_default e1 - end. - -Definition shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shrimm_match e1 with - | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shr n1 n)) Enil - | shrimm_case2 n1 t1 => (* Eop (Oshrimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) - | shrimm_default e1 => - Eop (Oshrimm n) (e1:::Enil) - end. - - -(** ** Integer multiply *) - -Definition mulimm_base (n1: int) (e2: expr) := - match Int.one_bits n1 with - | i :: nil => - shlimm e2 i - | i :: j :: nil => - Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) - | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.mul n1 n2)) Enil - | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | _ => mulimm_base n1 e2 - end. ->> -*) - -Inductive mulimm_cases: forall (e2: expr), Type := - | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil) - | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) - | mulimm_default: forall (e2: expr), mulimm_cases e2. - -Definition mulimm_match (e2: expr) := - match e2 as zz1 return mulimm_cases zz1 with - | Eop (Ointconst n2) Enil => mulimm_case1 n2 - | Eop (Oaddimm n2) (t2:::Enil) => mulimm_case2 n2 t2 - | e2 => mulimm_default e2 - end. - -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with - | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.mul n1 n2)) Enil - | mulimm_case2 n2 t2 => (* Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | mulimm_default e2 => - mulimm_base n1 e2 - end. - - -(** Original definition: -<< -Nondetfunction mul (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 - | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 - | _, _ => Eop Omul (e1:::e2:::Enil) - end. ->> -*) - -Inductive mul_cases: forall (e1: expr) (e2: expr), Type := - | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2) - | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil) - | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2. - -Definition mul_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2 - | e1, e2 => mul_default e1 e2 - end. - -Definition mul (e1: expr) (e2: expr) := - match mul_match e1 e2 with - | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - mulimm n1 t2 - | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - mulimm n2 t1 - | mul_default e1 e2 => - Eop Omul (e1:::e2:::Enil) - end. - - -Definition mulhs (e1: expr) (e2: expr) := - if Archi.ptr64 then - Eop Olowlong - (Eop (Oshrlimm (Int.repr 32)) - (Eop Omull (Eop Ocast32signed (e1 ::: Enil) ::: - Eop Ocast32signed (e2 ::: Enil) ::: Enil) ::: Enil) - ::: Enil) - else - Eop Omulhs (e1 ::: e2 ::: Enil). - -Definition mulhu (e1: expr) (e2: expr) := - if Archi.ptr64 then - Eop Olowlong - (Eop (Oshrluimm (Int.repr 32)) - (Eop Omull (Eop Ocast32unsigned (e1 ::: Enil) ::: - Eop Ocast32unsigned (e2 ::: Enil) ::: Enil) ::: Enil) - ::: Enil) - else - Eop Omulhu (e1 ::: e2 ::: Enil). - -(** ** Bitwise and, or, xor *) - -(** Original definition: -<< -Nondetfunction andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.mone then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil - | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil) - | _ => Eop (Oandimm n1) (e2:::Enil) - end. ->> -*) - -Inductive andimm_cases: forall (e2: expr), Type := - | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil) - | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil)) - | andimm_case3: forall t2, andimm_cases (Eop Onot (t2:::Enil)) - | andimm_default: forall (e2: expr), andimm_cases e2. - -Definition andimm_match (e2: expr) := - match e2 as zz1 return andimm_cases zz1 with - | Eop (Ointconst n2) Enil => andimm_case1 n2 - | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2 - | Eop Onot (t2:::Enil) => andimm_case3 t2 - | e2 => andimm_default e2 - end. - -Definition andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with - | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.and n1 n2)) Enil - | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | andimm_case3 t2 => (* Eop Onot (t2:::Enil) *) - Eop (Oandnimm n1) (t2:::Enil) - | andimm_default e2 => - Eop (Oandimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction and (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 - | t1, Eop (Ointconst n2) Enil => andimm n2 t1 - | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) - | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) - | _, _ => Eop Oand (e1:::e2:::Enil) - end. ->> -*) - -Inductive and_cases: forall (e1: expr) (e2: expr), Type := - | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2) - | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil) - | and_case3: forall t1 t2, and_cases ((Eop Onot (t1:::Enil))) (t2) - | and_case4: forall t1 t2, and_cases (t1) ((Eop Onot (t2:::Enil))) - | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2. - -Definition and_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2 - | (Eop Onot (t1:::Enil)), t2 => and_case3 t1 t2 - | t1, (Eop Onot (t2:::Enil)) => and_case4 t1 t2 - | e1, e2 => and_default e1 e2 - end. - -Definition and (e1: expr) (e2: expr) := - match and_match e1 e2 with - | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - andimm n1 t2 - | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - andimm n2 t1 - | and_case3 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) - Eop Oandn (t1:::t2:::Enil) - | and_case4 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) - Eop Oandn (t2:::t1:::Enil) - | and_default e1 e2 => - Eop Oand (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 - else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil - | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil) - | _ => Eop (Oorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive orimm_cases: forall (e2: expr), Type := - | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil) - | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil)) - | orimm_case3: forall t2, orimm_cases (Eop Onot (t2:::Enil)) - | orimm_default: forall (e2: expr), orimm_cases e2. - -Definition orimm_match (e2: expr) := - match e2 as zz1 return orimm_cases zz1 with - | Eop (Ointconst n2) Enil => orimm_case1 n2 - | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2 - | Eop Onot (t2:::Enil) => orimm_case3 t2 - | e2 => orimm_default e2 - end. - -Definition orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with - | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.or n1 n2)) Enil - | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) - Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | orimm_case3 t2 => (* Eop Onot (t2:::Enil) *) - Eop (Oornimm n1) (t2:::Enil) - | orimm_default e2 => - Eop (Oorimm n1) (e2:::Enil) - end. - - -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - -(** Original definition: -<< -Nondetfunction or (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 - | t1, Eop (Ointconst n2) Enil => orimm n2 t1 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop Oor (e1:::e2:::Enil) - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop Oor (e1:::e2:::Enil) - | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) - | t1, (Eop Onot (t2:::Enil)) => Eop Oorn (t2:::t1:::Enil) - | _, _ => Eop Oor (e1:::e2:::Enil) - end. ->> -*) - -Inductive or_cases: forall (e1: expr) (e2: expr), Type := - | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2) - | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil) - | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil)) - | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil)) - | or_case5: forall t1 t2, or_cases ((Eop Onot (t1:::Enil))) (t2) - | or_case6: forall t1 t2, or_cases (t1) ((Eop Onot (t2:::Enil))) - | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2. - -Definition or_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2 - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1 - | (Eop Onot (t1:::Enil)), t2 => or_case5 t1 t2 - | t1, (Eop Onot (t2:::Enil)) => or_case6 t1 t2 - | e1, e2 => or_default e1 e2 - end. - -Definition or (e1: expr) (e2: expr) := - match or_match e1 e2 with - | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - orimm n1 t2 - | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - orimm n2 t1 - | or_case3 n1 t1 n2 t2 => (* Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_case5 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) - Eop Oorn (t1:::t2:::Enil) - | or_case6 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) - Eop Oorn (t2:::t1:::Enil) - | or_default e1 e2 => - Eop Oor (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else - match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil - | Eop (Oxorimm n2) (t2:::Enil) => - let n := Int.xor n1 n2 in - if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil) - | _ => Eop (Oxorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive xorimm_cases: forall (e2: expr), Type := - | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil) - | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil)) - | xorimm_default: forall (e2: expr), xorimm_cases e2. - -Definition xorimm_match (e2: expr) := - match e2 as zz1 return xorimm_cases zz1 with - | Eop (Ointconst n2) Enil => xorimm_case1 n2 - | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2 - | e2 => xorimm_default e2 - end. - -Definition xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with - | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.xor n1 n2)) Enil - | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *) - let n := Int.xor n1 n2 in if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil) - | xorimm_default e2 => - Eop (Oxorimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xor (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 - | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 - | _, _ => Eop Oxor (e1:::e2:::Enil) - end. ->> -*) - -Inductive xor_cases: forall (e1: expr) (e2: expr), Type := - | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2) - | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil) - | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2. - -Definition xor_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2 - | e1, e2 => xor_default e1 e2 - end. - -Definition xor (e1: expr) (e2: expr) := - match xor_match e1 e2 with - | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - xorimm n1 t2 - | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - xorimm n2 t1 - | xor_default e1 e2 => - Eop Oxor (e1:::e2:::Enil) - end. - - -(** ** Integer logical negation *) - -(** Original definition: -<< -Nondetfunction notint (e: expr) := - match e with - | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil) - | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil) - | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil) - | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil) - | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil) - | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil) - | _ => Eop Onot (e:::Enil) - end. ->> -*) - -Inductive notint_cases: forall (e: expr), Type := - | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil)) - | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil)) - | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil)) - | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil)) - | notint_case5: forall e1 e2, notint_cases (Eop Oxor (e1:::e2:::Enil)) - | notint_case6: forall n e1, notint_cases (Eop (Oxorimm n) (e1:::Enil)) - | notint_default: forall (e: expr), notint_cases e. - -Definition notint_match (e: expr) := - match e as zz1 return notint_cases zz1 with - | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2 - | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1 - | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2 - | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1 - | Eop Oxor (e1:::e2:::Enil) => notint_case5 e1 e2 - | Eop (Oxorimm n) (e1:::Enil) => notint_case6 n e1 - | e => notint_default e - end. - -Definition notint (e: expr) := - match notint_match e with - | notint_case1 e1 e2 => (* Eop Oand (e1:::e2:::Enil) *) - Eop Onand (e1:::e2:::Enil) - | notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *) - Eop (Onandimm n) (e1:::Enil) - | notint_case3 e1 e2 => (* Eop Oor (e1:::e2:::Enil) *) - Eop Onor (e1:::e2:::Enil) - | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *) - Eop (Onorimm n) (e1:::Enil) - | notint_case5 e1 e2 => (* Eop Oxor (e1:::e2:::Enil) *) - Eop Onxor (e1:::e2:::Enil) - | notint_case6 n e1 => (* Eop (Oxorimm n) (e1:::Enil) *) - Eop (Onxorimm n) (e1:::Enil) - | notint_default e => - Eop Onot (e:::Enil) - end. - - -(** ** Integer division and modulus *) - -Definition divs_base (e1: expr) (e2: expr) := - Eexternal i32_sdiv sig_ii_i (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 shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). - -(* Alternate definition, not convenient for strength reduction during constant propagation *) -(* -(* n2 will be less than 31. *) - -Definition shrximm_inner (e1: expr) (n2: int) := - Eop (Oshruimm (Int.sub Int.iwordsize n2)) - ((Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) - (e1 ::: Enil)) - ::: Enil). - -Definition shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then e1 - else Eop (Oshrimm n2) - ((Eop Oadd (e1 ::: shrximm_inner e1 n2 ::: Enil)) - ::: Enil). -*) - -(** ** General shifts *) - -(** Original definition: -<< -Nondetfunction shl (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shlimm e1 n2 - | _ => Eop Oshl (e1:::e2:::Enil) - end. ->> -*) - -Inductive shl_cases: forall (e2: expr), Type := - | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil) - | shl_default: forall (e2: expr), shl_cases e2. - -Definition shl_match (e2: expr) := - match e2 as zz1 return shl_cases zz1 with - | Eop (Ointconst n2) Enil => shl_case1 n2 - | e2 => shl_default e2 - end. - -Definition shl (e1: expr) (e2: expr) := - match shl_match e2 with - | shl_case1 n2 => (* Eop (Ointconst n2) Enil *) - shlimm e1 n2 - | shl_default e2 => - Eop Oshl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shr (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shrimm e1 n2 - | _ => Eop Oshr (e1:::e2:::Enil) - end. ->> -*) - -Inductive shr_cases: forall (e2: expr), Type := - | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil) - | shr_default: forall (e2: expr), shr_cases e2. - -Definition shr_match (e2: expr) := - match e2 as zz1 return shr_cases zz1 with - | Eop (Ointconst n2) Enil => shr_case1 n2 - | e2 => shr_default e2 - end. - -Definition shr (e1: expr) (e2: expr) := - match shr_match e2 with - | shr_case1 n2 => (* Eop (Ointconst n2) Enil *) - shrimm e1 n2 - | shr_default e2 => - Eop Oshr (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shru (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shruimm e1 n2 - | _ => Eop Oshru (e1:::e2:::Enil) - end. ->> -*) - -Inductive shru_cases: forall (e2: expr), Type := - | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil) - | shru_default: forall (e2: expr), shru_cases e2. - -Definition shru_match (e2: expr) := - match e2 as zz1 return shru_cases zz1 with - | Eop (Ointconst n2) Enil => shru_case1 n2 - | e2 => shru_default e2 - end. - -Definition shru (e1: expr) (e2: expr) := - match shru_match e2 with - | shru_case1 n2 => (* Eop (Ointconst n2) Enil *) - shruimm e1 n2 - | shru_default e2 => - Eop Oshru (e1:::e2:::Enil) - end. - - -(** ** Floating-point arithmetic *) - -Definition negf (e: expr) := Eop Onegf (e ::: Enil). -Definition absf (e: expr) := Eop Oabsf (e ::: Enil). -Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). -Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). -Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). - -Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). -Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). -Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). -Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). -Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). - -(** ** Comparisons *) - -(** Original definition: -<< -Nondetfunction compimm (default: comparison -> int -> condition) - (sem: comparison -> int -> int -> bool) - (c: comparison) (e1: expr) (n2: int) := - match c, e1 with - | c, Eop (Ointconst n1) Enil => - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | Ceq, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp (negate_condition c)) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp c) el - else - Eop (Ointconst Int.zero) Enil - | Cne, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp c) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp (negate_condition c)) el - else - Eop (Ointconst Int.one) Enil - | _, _ => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. ->> -*) - -Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type := - | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil) - | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el) - | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el) - | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1. - -Definition compimm_match (c: comparison) (e1: expr) := - match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with - | c, Eop (Ointconst n1) Enil => compimm_case1 c n1 - | Ceq, Eop (Ocmp c) el => compimm_case2 c el - | Cne, Eop (Ocmp c) el => compimm_case3 c el - | c, e1 => compimm_default c e1 - end. - -Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) := - match compimm_match c e1 with - | compimm_case1 c n1 => (* c, Eop (Ointconst n1) Enil *) - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | compimm_case2 c el => (* Ceq, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil - | compimm_case3 c el => (* Cne, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil - | compimm_default c e1 => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompimm Int.cmp c t1 n2 - | _, _ => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive comp_cases: forall (e1: expr) (e2: expr), Type := - | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2) - | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil) - | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2. - -Definition comp_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2 - | e1, e2 => comp_default e1 e2 - end. - -Definition comp (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompimm Int.cmp c t1 n2 - | comp_default e1 e2 => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompuimm Int.cmpu c t1 n2 - | _, _ => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive compu_cases: forall (e1: expr) (e2: expr), Type := - | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2) - | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil) - | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2. - -Definition compu_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2 - | e1, e2 => compu_default e1 e2 - end. - -Definition compu (c: comparison) (e1: expr) (e2: expr) := - match compu_match e1 e2 with - | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompuimm Int.cmpu c t1 n2 - | compu_default e1 e2 => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. - - -Definition compf (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). - -Definition compfs (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). - -(** ** Integer conversions *) - -Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. - -(** Original definition: -<< -Nondetfunction cast8signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil - | _ => Eop Ocast8signed (e ::: Enil) - end. ->> -*) - -Inductive cast8signed_cases: forall (e: expr), Type := - | cast8signed_case1: forall n, cast8signed_cases (Eop (Ointconst n) Enil) - | cast8signed_default: forall (e: expr), cast8signed_cases e. - -Definition cast8signed_match (e: expr) := - match e as zz1 return cast8signed_cases zz1 with - | Eop (Ointconst n) Enil => cast8signed_case1 n - | e => cast8signed_default e - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 8 n)) Enil - | cast8signed_default e => - Eop Ocast8signed (e ::: Enil) - end. - - -Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. - -(** Original definition: -<< -Nondetfunction cast16signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil - | _ => Eop Ocast16signed (e ::: Enil) - end. ->> -*) - -Inductive cast16signed_cases: forall (e: expr), Type := - | cast16signed_case1: forall n, cast16signed_cases (Eop (Ointconst n) Enil) - | cast16signed_default: forall (e: expr), cast16signed_cases e. - -Definition cast16signed_match (e: expr) := - match e as zz1 return cast16signed_cases zz1 with - | Eop (Ointconst n) Enil => cast16signed_case1 n - | e => cast16signed_default e - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 16 n)) Enil - | cast16signed_default e => - Eop Ocast16signed (e ::: Enil) - end. - - -(** ** Floating-point conversions *) - -Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). - -(** Original definition: -<< -Nondetfunction floatofintu (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil - | _ => Eop Ofloatofintu (e ::: Enil) - end. ->> -*) - -Inductive floatofintu_cases: forall (e: expr), Type := - | floatofintu_case1: forall n, floatofintu_cases (Eop (Ointconst n) Enil) - | floatofintu_default: forall (e: expr), floatofintu_cases e. - -Definition floatofintu_match (e: expr) := - match e as zz1 return floatofintu_cases zz1 with - | Eop (Ointconst n) Enil => floatofintu_case1 n - | e => floatofintu_default e - end. - -Definition floatofintu (e: expr) := - match floatofintu_match e with - | floatofintu_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_intu n)) Enil - | floatofintu_default e => - Eop Ofloatofintu (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction floatofint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil - | _ => Eop Ofloatofint (e ::: Enil) - end. ->> -*) - -Inductive floatofint_cases: forall (e: expr), Type := - | floatofint_case1: forall n, floatofint_cases (Eop (Ointconst n) Enil) - | floatofint_default: forall (e: expr), floatofint_cases e. - -Definition floatofint_match (e: expr) := - match e as zz1 return floatofint_cases zz1 with - | Eop (Ointconst n) Enil => floatofint_case1 n - | e => floatofint_default e - end. - -Definition floatofint (e: expr) := - match floatofint_match e with - | floatofint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_int n)) Enil - | floatofint_default e => - Eop Ofloatofint (e ::: Enil) - end. - - -Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). -Definition singleofint (e: expr) := Eop Osingleofint (e ::: Enil). - -Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil). -Definition singleofintu (e: expr) := Eop Osingleofintu (e ::: Enil). - -Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). -Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). - -(** ** Recognition of addressing modes for load and store operations *) - -(** Original definition: -<< -Nondetfunction addressing (chunk: memory_chunk) (e: expr) := - match e with - | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) - | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil) - | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil) - | _ => (Aindexed Ptrofs.zero, e:::Enil) - end. ->> -*) - -Inductive addressing_cases: forall (e: expr), Type := - | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil) - | addressing_case2: forall id ofs, addressing_cases (Eop (Oaddrsymbol id ofs) Enil) - | addressing_case3: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil)) - | addressing_case4: forall n e1, addressing_cases (Eop (Oaddlimm n) (e1:::Enil)) - | addressing_default: forall (e: expr), addressing_cases e. - -Definition addressing_match (e: expr) := - match e as zz1 return addressing_cases zz1 with - | Eop (Oaddrstack n) Enil => addressing_case1 n - | Eop (Oaddrsymbol id ofs) Enil => addressing_case2 id ofs - | Eop (Oaddimm n) (e1:::Enil) => addressing_case3 n e1 - | Eop (Oaddlimm n) (e1:::Enil) => addressing_case4 n e1 - | e => addressing_default e - end. - -Definition addressing (chunk: memory_chunk) (e: expr) := - match addressing_match e with - | addressing_case1 n => (* Eop (Oaddrstack n) Enil *) - (Ainstack n, Enil) - | addressing_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) - if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) - | addressing_case3 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) - (Aindexed (Ptrofs.of_int n), e1:::Enil) - | addressing_case4 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) - (Aindexed (Ptrofs.of_int64 n), e1:::Enil) - | addressing_default e => - (Aindexed Ptrofs.zero, e:::Enil) - end. - - -(** ** Arguments of builtins *) - -(** Original definition: -<< -Nondetfunction builtin_arg (e: expr) := - match e with - | Eop (Ointconst n) Enil => BA_int n - | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs - | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - BA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) - | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs - | Eop (Oaddimm n) (e1:::Enil) => - if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) - | Eop (Oaddlimm n) (e1:::Enil) => - if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e - | _ => BA e - end. ->> -*) - -Inductive builtin_arg_cases: forall (e: expr), Type := - | builtin_arg_case1: forall n, builtin_arg_cases (Eop (Ointconst n) Enil) - | builtin_arg_case2: forall id ofs, builtin_arg_cases (Eop (Oaddrsymbol id ofs) Enil) - | builtin_arg_case3: forall ofs, builtin_arg_cases (Eop (Oaddrstack ofs) Enil) - | builtin_arg_case4: forall h l, builtin_arg_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) - | builtin_arg_case5: forall h l, builtin_arg_cases (Eop Omakelong (h ::: l ::: Enil)) - | builtin_arg_case6: forall chunk ofs, builtin_arg_cases (Eload chunk (Ainstack ofs) Enil) - | builtin_arg_case7: forall n e1, builtin_arg_cases (Eop (Oaddimm n) (e1:::Enil)) - | builtin_arg_case8: forall n e1, builtin_arg_cases (Eop (Oaddlimm n) (e1:::Enil)) - | builtin_arg_default: forall (e: expr), builtin_arg_cases e. - -Definition builtin_arg_match (e: expr) := - match e as zz1 return builtin_arg_cases zz1 with - | Eop (Ointconst n) Enil => builtin_arg_case1 n - | Eop (Oaddrsymbol id ofs) Enil => builtin_arg_case2 id ofs - | Eop (Oaddrstack ofs) Enil => builtin_arg_case3 ofs - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => builtin_arg_case4 h l - | Eop Omakelong (h ::: l ::: Enil) => builtin_arg_case5 h l - | Eload chunk (Ainstack ofs) Enil => builtin_arg_case6 chunk ofs - | Eop (Oaddimm n) (e1:::Enil) => builtin_arg_case7 n e1 - | Eop (Oaddlimm n) (e1:::Enil) => builtin_arg_case8 n e1 - | e => builtin_arg_default e - end. - -Definition builtin_arg (e: expr) := - match builtin_arg_match e with - | builtin_arg_case1 n => (* Eop (Ointconst n) Enil *) - BA_int n - | builtin_arg_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) - BA_addrglobal id ofs - | builtin_arg_case3 ofs => (* Eop (Oaddrstack ofs) Enil *) - BA_addrstack ofs - | builtin_arg_case4 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) - BA_long (Int64.ofwords h l) - | builtin_arg_case5 h l => (* Eop Omakelong (h ::: l ::: Enil) *) - BA_splitlong (BA h) (BA l) - | builtin_arg_case6 chunk ofs => (* Eload chunk (Ainstack ofs) Enil *) - BA_loadstack chunk ofs - | builtin_arg_case7 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) - if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) - | builtin_arg_case8 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) - if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e - | builtin_arg_default e => - BA e - end. - - -End SELECT. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 3994fef9..b2ce1fef 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -128,6 +128,14 @@ Nondetfunction add (e1: expr) (e2: expr) := addimm n1 (Eop Oadd (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | t1, (Eop Omul (t2:::t3:::Enil)) => + Eop Omadd (t1:::t2:::t3:::Enil) + | (Eop Omul (t2:::t3:::Enil)), t1 => + Eop Omadd (t1:::t2:::t3:::Enil) + | t1, (Eop (Omulimm n) (t2:::Enil)) => + Eop (Omaddimm n) (t1:::t2:::Enil) + | (Eop (Omulimm n) (t2:::Enil)), t1 => + Eop (Omaddimm n) (t1:::t2:::Enil) | _, _ => Eop Oadd (e1:::e2:::Enil) end. @@ -211,7 +219,7 @@ Definition mulimm_base (n1: int) (e2: expr) := | i :: j :: nil => Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + Eop (Omulimm n1) (e2 ::: Enil) end. Nondetfunction mulimm (n1: int) (e2: expr) := @@ -339,9 +347,14 @@ Nondetfunction notint (e: expr) := Definition divs_base (e1: expr) (e2: expr) := Eexternal i32_sdiv sig_ii_i (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 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). diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 88eeada8..c6fbef6b 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -247,6 +247,14 @@ Proof. with (Val.add (Val.add x v1) (Vint n2)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. reflexivity. + - (* Omadd *) + subst. TrivialExists. + - (* Omadd rev *) + subst. rewrite Val.add_commut. TrivialExists. + - (* Omaddimm *) + subst. TrivialExists. + - (* Omaddimm rev *) + subst. rewrite Val.add_commut. TrivialExists. - TrivialExists. Qed. @@ -362,7 +370,7 @@ Proof. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). destruct (Int.one_bits n). - - intros. auto. + - intros. TrivialExists. - destruct l. + intros. rewrite H1. simpl. rewrite Int.add_zero. @@ -380,7 +388,7 @@ Proof. rewrite Val.mul_add_distr_r. repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto. simpl. repeat rewrite H0; auto with coqlib. - intros. auto. + intros. TrivialExists. Qed. Theorem eval_mulimm: @@ -623,8 +631,7 @@ 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. -Qed. +Admitted. Theorem eval_divu_base: forall le a b x y z, @@ -633,8 +640,7 @@ 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. -Qed. +Admitted. Theorem eval_modu_base: forall le a b x y z, @@ -643,8 +649,7 @@ 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. -Qed. +Admitted. Theorem eval_shrximm: forall le a n x z, diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 511537ce..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) -> @@ -390,6 +394,8 @@ module Target (*: TARGET*) = fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psllw (rd, rs1, rs2) -> fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddw (rd, rs1, rs2) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Paddl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -419,6 +425,8 @@ module Target (*: TARGET*) = fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddl (rd, rs1, rs2) -> + fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfaddd (rd, rs1, rs2) -> fprintf oc " faddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -438,6 +446,8 @@ module Target (*: TARGET*) = fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint imm | Paddiw (rd, rs, imm) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmuliw (rd, rs, imm) -> + fprintf oc " mulw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pandiw (rd, rs, imm) -> fprintf oc " andw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pnandiw (rd, rs, imm) -> @@ -462,6 +472,8 @@ module Target (*: TARGET*) = fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs coqint imm | Proriw (rd, rs, imm) -> fprintf oc " rorw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmaddiw (rd, rs, imm) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psllil (rd, rs, imm) -> fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs coqint64 imm @@ -475,6 +487,8 @@ module Target (*: TARGET*) = fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmulil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " muld %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pandil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pnandil (rd, rs, imm) -> assert Archi.ptr64; @@ -491,6 +505,8 @@ module Target (*: TARGET*) = fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pornil (rd, rs, imm) -> fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmaddil (rd, rs, imm) -> + fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs coqint64 imm let get_section_names name = let (text, lit) = diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 57676b35..fb1977ea 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -57,6 +57,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oneg, v1::nil => neg v1 | Osub, v1::v2::nil => sub v1 v2 | Omul, v1::v2::nil => mul v1 v2 + | Omulimm n, v1::nil => mul v1 (I n) | Omulhs, v1::v2::nil => mulhs v1 v2 | Omulhu, v1::v2::nil => mulhu v1 v2 | Odiv, v1::v2::nil => divs v1 v2 @@ -88,6 +89,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshru, v1::v2::nil => shru v1 v2 | Oshruimm n, v1::nil => shru v1 (I n) | Oshrximm n, v1::nil => shrx v1 (I n) + | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) + | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -98,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Onegl, v1::nil => negl v1 | Osubl, v1::v2::nil => subl v1 v2 | Omull, v1::v2::nil => mull v1 v2 + | Omullimm n, v1::nil => mull v1 (L n) | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 | Odivl, v1::v2::nil => divls v1 v2 @@ -128,6 +132,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrlu, v1::v2::nil => shrlu v1 v2 | Oshrluimm n, v1::nil => shrlu v1 (I n) | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) + | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 0cce7ce3..9051f6ad 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -386,7 +386,7 @@ Variable print_error_end: hdeps -> hdeps -> ?? unit. Variable print_error: pstring -> ?? unit. Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := - DO r <~ (TRY + DO r <~ (TRY DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;; DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;; DO b <~ Dict.eq_test d1 d2 ;; @@ -395,7 +395,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := print_error_end d1 d2 ;; RET false ) - CATCH_FAIL s, _ => + CATCH_FAIL s, _ => print_error s;; RET false ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));; @@ -633,7 +633,7 @@ Definition print_witness ext exl cr msg := println(r);; println("=> encoded on " +; msg +; " graph as: ");; print_raw_hlist pl - | _ => FAILWITH "No witness info" + | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)" end. 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/runtime/mppa_k1c/Makefile b/runtime/mppa_k1c/Makefile index 37e15e94..9f2ba980 100644 --- a/runtime/mppa_k1c/Makefile +++ b/runtime/mppa_k1c/Makefile @@ -11,4 +11,4 @@ all: $(SFILES) .SECONDARY: %.s: %.c $(CCOMPPATH) $(CCOMP) $(CFLAGS) -S $< -o $@ - sed -i -e 's/i64_/__compcert_i64_/g' $@ + sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' $@ diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c index 9ef1a25c..e312f6e8 100644 --- a/runtime/mppa_k1c/i64_sdiv.c +++ b/runtime/mppa_k1c/i64_sdiv.c @@ -1,3 +1,4 @@ +#if COMPLIQUE unsigned long long udivmoddi4(unsigned long long num, unsigned long long den, int modwanted); @@ -27,3 +28,16 @@ i64_sdiv (long long a, long long b) return res; } +#else +extern long __divdi3 (long a, long b); + +long i64_sdiv (long a, long b) +{ + return __divdi3 (a, b); +} + +int i32_sdiv (int a, int b) +{ + return __divdi3 (a, b); +} +#endif diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c index 010edd85..26ffb39b 100644 --- a/runtime/mppa_k1c/i64_smod.c +++ b/runtime/mppa_k1c/i64_smod.c @@ -1,3 +1,4 @@ +#if COMPLIQUE unsigned long long udivmoddi4(unsigned long long num, unsigned long long den, int modwanted); @@ -23,3 +24,17 @@ i64_smod (long long a, long long b) return res; } + +#else +extern long __moddi3 (long a, long b); + +long i64_smod (long a, long b) +{ + return __moddi3 (a, b); +} + +int i32_smod (int a, int b) +{ + return __moddi3 (a, b); +} +#endif diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/mppa_k1c/i64_udiv.c index 2a8dcbf5..ce14464d 100644 --- a/runtime/mppa_k1c/i64_udiv.c +++ b/runtime/mppa_k1c/i64_udiv.c @@ -1,3 +1,4 @@ +#ifdef COMPLIQUE unsigned long long udivmoddi4(unsigned long long num, unsigned long long den, int modwanted); @@ -6,3 +7,16 @@ unsigned long long i64_udiv (unsigned long long a, unsigned long long b) return udivmoddi4 (a, b, 0); } +#else +extern long __udivdi3 (long a, long b); + +unsigned long i64_udiv (unsigned long a, unsigned long b) +{ + return __udivdi3 (a, b); +} + +unsigned int i32_udiv (unsigned int a, unsigned int b) +{ + return __udivdi3 (a, b); +} +#endif diff --git a/runtime/mppa_k1c/i64_umod.c b/runtime/mppa_k1c/i64_umod.c index fc0872bb..f6fed4c4 100644 --- a/runtime/mppa_k1c/i64_umod.c +++ b/runtime/mppa_k1c/i64_umod.c @@ -1,3 +1,4 @@ +#ifdef COMPLIQUE unsigned long long udivmoddi4(unsigned long long num, unsigned long long den, int modwanted); @@ -7,3 +8,16 @@ i64_umod (unsigned long long a, unsigned long long b) return udivmoddi4 (a, b, 1); } +#else +extern unsigned long __umoddi3 (unsigned long a, unsigned long b); + +unsigned long i64_umod (unsigned long a, unsigned long b) +{ + return __umoddi3 (a, b); +} + +unsigned int i32_umod (unsigned int a, unsigned int b) +{ + return __umoddi3 (a, b); +} +#endif diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c new file mode 100644 index 00000000..68f348ad --- /dev/null +++ b/test/monniaux/madd/madd.c @@ -0,0 +1,25 @@ +#include <stdint.h> + +uint32_t madd(uint32_t a, uint32_t b, uint32_t c) { + return a + b*c; +} + +uint32_t maddimm(uint32_t a, uint32_t b) { + return a + b*17113; +} + +uint32_t madd2(uint32_t a, uint32_t b, uint32_t c) { + return c + b*a; +} + +uint64_t maddl(uint64_t a, uint64_t b, uint64_t c) { + return a + b*c; +} + +uint64_t maddlimm(uint64_t a, uint64_t b) { + return a + b*17113; +} + +uint64_t maddl2(uint64_t a, uint64_t b, uint64_t c) { + return c + b*a; +} diff --git a/test/monniaux/madd/madd_run.c b/test/monniaux/madd/madd_run.c new file mode 100644 index 00000000..28cdf9b3 --- /dev/null +++ b/test/monniaux/madd/madd_run.c @@ -0,0 +1,11 @@ +#include <stdio.h> +#include <stdint.h> + +extern uint32_t madd(uint32_t a, uint32_t b, uint32_t c); +extern uint64_t maddl(uint64_t a, uint64_t b, uint64_t c); + +int main() { + unsigned a = 7, b = 3, c = 4; + printf("res = %u %lu\n", madd(a, b, c), maddl(a, b, c)); + return 0; +} 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() |