diff options
Diffstat (limited to 'mppa_k1c/Asmgen.v')
-rw-r--r-- | mppa_k1c/Asmgen.v | 173 |
1 files changed, 88 insertions, 85 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index a704ed74..72822f70 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -37,8 +37,9 @@ Definition ireg_of (r: mreg) : res ireg := match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. Definition freg_of (r: mreg) : res freg := - match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. +(* (** Decomposition of 32-bit integer constants. They are split into either small signed immediates that fit in 12-bits, or, if they do not fit, into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *) @@ -61,7 +62,7 @@ Definition make_immed32 (val: int) := *) (** Likewise, for 64-bit integer constants. *) - +*) Inductive immed64 : Type := | Imm64_single (imm: int64) | Imm64_pair (hi: int64) (lo: int64) @@ -74,7 +75,7 @@ Definition make_immed64 (val: int64) := if Int64.eq val (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo) then Imm64_pair hi lo else Imm64_large val. - +(* (** Smart constructors for arithmetic operations involving a 32-bit or 64-bit integer constant. Depending on whether the constant fits in 12 bits or not, one or several instructions @@ -87,7 +88,7 @@ Definition load_hilo32 (r: ireg) (hi lo: int) k := Definition loadimm32 (r: ireg) (n: int) (k: code) := match make_immed32 n with - | Imm32_single imm => Paddiw r X0 imm :: k + | Imm32_single imm => Paddiw r GPR0 imm :: k | Imm32_pair hi lo => load_hilo32 r hi lo k end. @@ -96,7 +97,7 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction) (rd rs: ireg) (n: int) (k: code) := match make_immed32 n with | Imm32_single imm => opimm rd rs imm :: k - | Imm32_pair hi lo => load_hilo32 X31 hi lo (op rd rs X31 :: k) + | Imm32_pair hi lo => load_hilo32 GPR31 hi lo (op rd rs GPR31 :: k) end. Definition addimm32 := opimm32 Paddw Paddiw. @@ -109,24 +110,26 @@ Definition sltuimm32 := opimm32 Psltuw Psltiuw. Definition load_hilo64 (r: ireg) (hi lo: int64) k := if Int64.eq lo Int64.zero then Pluil r hi :: k else Pluil r hi :: Paddil r r lo :: k. - + Definition loadimm64 (r: ireg) (n: int64) (k: code) := match make_immed64 n with - | Imm64_single imm => Paddil r X0 imm :: k + | Imm64_single imm => Paddil r GPR0 imm :: k | Imm64_pair hi lo => load_hilo64 r hi lo k | Imm64_large imm => Ploadli r imm :: k end. - +*) Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction) (opimm: ireg -> ireg0 -> int64 -> instruction) (rd rs: ireg) (n: int64) (k: code) := match make_immed64 n with | Imm64_single imm => opimm rd rs imm :: k - | Imm64_pair hi lo => load_hilo64 X31 hi lo (op rd rs X31 :: k) - | Imm64_large imm => Ploadli X31 imm :: op rd rs X31 :: k +(*| Imm64_pair hi lo => load_hilo64 GPR31 hi lo (op rd rs GPR31 :: k) + | Imm64_large imm => Ploadli GPR31 imm :: op rd rs GPR31 :: k +*)| _ => nil end. Definition addimm64 := opimm64 Paddl Paddil. +(* Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. @@ -215,15 +218,15 @@ Definition transl_cbranch | Ccompimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq n Int.zero then - transl_cbranch_int32s c r1 X0 lbl :: k + transl_cbranch_int32s c r1 GPR0 lbl :: k else - loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k)) + loadimm32 GPR31 n (transl_cbranch_int32s c r1 GPR31 lbl :: k)) | Ccompuimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq n Int.zero then - transl_cbranch_int32u c r1 X0 lbl :: k + transl_cbranch_int32u c r1 GPR0 lbl :: k else - loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k)) + loadimm32 GPR31 n (transl_cbranch_int32u c r1 GPR31 lbl :: k)) | Ccompl c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cbranch_int64s c r1 r2 lbl :: k) @@ -233,31 +236,31 @@ Definition transl_cbranch | Ccomplimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int64.eq n Int64.zero then - transl_cbranch_int64s c r1 X0 lbl :: k + transl_cbranch_int64s c r1 GPR0 lbl :: k else - loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k)) + loadimm64 GPR31 n (transl_cbranch_int64s c r1 GPR31 lbl :: k)) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int64.eq n Int64.zero then - transl_cbranch_int64u c r1 X0 lbl :: k + transl_cbranch_int64u c r1 GPR0 lbl :: k else - loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k)) + loadimm64 GPR31 n (transl_cbranch_int64u c r1 GPR31 lbl :: k)) | Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_float c GPR31 r1 r2 in + OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) | Cnotcompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_float c GPR31 r1 r2 in + OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) | Ccompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_single c GPR31 r1 r2 in + OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_single c GPR31 r1 r2 in + OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) | _, _ => Error(msg "Asmgen.transl_cond_branch") end. @@ -307,45 +310,46 @@ Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: co end. Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else + if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 GPR0 k else match cmp with - | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k) + | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd GPR0 k) | Clt => sltimm32 rd r1 n k | Cle => if Int.eq n (Int.repr Int.max_signed) then loadimm32 rd Int.one k else sltimm32 rd r1 (Int.add n Int.one) k - | _ => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k) + | _ => loadimm32 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 k) end. Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else + if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 GPR0 k else match cmp with | Clt => sltuimm32 rd r1 n k - | _ => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k) + | _ => loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 k) end. Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else + if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 GPR0 k else match cmp with - | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k) + | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd GPR0 k) | Clt => sltimm64 rd r1 n k | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then loadimm32 rd Int.one k else sltimm64 rd r1 (Int64.add n Int64.one) k - | _ => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k) + | _ => loadimm64 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 k) end. Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else + if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 GPR0 k else match cmp with | Clt => sltuimm64 rd r1 n k - | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) + | _ => loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k) end. +*) Definition transl_cond_op - (cond: condition) (rd: ireg) (args: list mreg) (k: code) := + (cond: condition) (rd: ireg) (args: list mreg) (k: code) : res (list instruction) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => +(*| Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cond_int32s c rd r1 r2 k) | Ccompu c, a1 :: a2 :: nil => @@ -385,7 +389,7 @@ Definition transl_cond_op do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c rd r1 r2 in OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | _, _ => +*)| _, _ => Error(msg "Asmgen.transl_cond_op") end. @@ -395,10 +399,9 @@ Definition transl_cond_op Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with - | Omove, a1 :: nil => +(*| Omove, a1 :: nil => match preg_of res, preg_of a1 with | IR r, IR a => OK (Pmv r a :: k) - | FR r, FR a => OK (Pfmv r a :: k) | _ , _ => Error(msg "Asmgen.Omove") end | Ointconst n, nil => @@ -410,12 +413,12 @@ Definition transl_op | Ofloatconst f, nil => do rd <- freg_of res; OK (if Float.eq_dec f Float.zero - then Pfcvtdw rd X0 :: k + then Pfcvtdw rd GPR0 :: k else Ploadfi rd f :: k) | Osingleconst f, nil => do rd <- freg_of res; OK (if Float32.eq_dec f Float32.zero - then Pfcvtsw rd X0 :: k + then Pfcvtsw rd GPR0 :: k else Ploadsi rd f :: k) | Oaddrsymbol s ofs, nil => do rd <- ireg_of res; @@ -440,7 +443,7 @@ Definition transl_op OK (addimm32 rd rs n k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (Psubw rd X0 rs :: k) + OK (Psubw rd GPR0 rs :: k) | Osub, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubw rd rs1 rs2 :: k) @@ -504,10 +507,10 @@ Definition transl_op | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + Psraiw GPR31 rs (Int.repr 31) :: + Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) :: + Paddw GPR31 rs GPR31 :: + Psraiw rd GPR31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -521,15 +524,15 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; assertion (ireg_eq rd rs); OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k) - | Oaddl, a1 :: a2 :: nil => +*)| Oaddl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddl rd rs1 rs2 :: k) | Oaddlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (addimm64 rd rs n k) - | Onegl, a1 :: nil => +(*| Onegl, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (Psubl rd X0 rs :: k) + OK (Psubl rd GPR0 rs :: k) | Osubl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubl rd rs1 rs2 :: k) @@ -593,10 +596,10 @@ Definition transl_op | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + Psrail GPR31 rs (Int.repr 63) :: + Psrlil GPR31 GPR31 (Int.sub Int64.iwordsize' n) :: + Paddl GPR31 rs GPR31 :: + Psrail rd GPR31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; @@ -696,13 +699,13 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k - +*) | _, _ => Error(msg "Asmgen.transl_op") end. (** Accessing data in the stack frame. *) - +(* Definition indexed_memory_access (mk_instr: ireg -> offset -> instruction) (base: ireg) (ofs: ptrofs) (k: code) := @@ -711,27 +714,26 @@ Definition indexed_memory_access | Imm64_single imm => mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k | Imm64_pair hi lo => - Pluil X31 hi :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int64 lo)) :: k + Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k | Imm64_large imm => - Ploadli X31 imm :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm Ptrofs.zero) :: k + Ploadli GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k end else match make_immed32 (Ptrofs.to_int ofs) with | Imm32_single imm => mk_instr base (Ofsimm (Ptrofs.of_int imm)) :: k | Imm32_pair hi lo => - Pluiw X31 hi :: Paddw X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int lo)) :: k + Pluiw GPR31 hi :: Paddw GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int lo)) :: k end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := match ty, preg_of dst with | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs k) | Tlong, IR rd => OK (indexed_memory_access (Pld rd) base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pfls rd) base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pfld rd) base ofs k) + | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs k) + | Tfloat, IR rd => OK (indexed_memory_access (Pfld rd) base ofs k) | Tany32, IR rd => OK (indexed_memory_access (Plw_a rd) base ofs k) | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pfld_a rd) base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. @@ -739,11 +741,10 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : match ty, preg_of src with | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs k) | Tlong, IR rd => OK (indexed_memory_access (Psd rd) base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pfss rd) base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pfsd rd) base ofs k) + | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs k) + | Tfloat, IR rd => OK (indexed_memory_access (Pfsd rd) base ofs k) | Tany32, IR rd => OK (indexed_memory_access (Psw_a rd) base ofs k) | Tany64, IR rd => OK (indexed_memory_access (Psd_a rd) base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pfsd_a rd) base ofs k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -752,28 +753,28 @@ Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) := Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) (k: code) := indexed_memory_access (if Archi.ptr64 then Psd src else Psw src) base ofs k. - +*) (** Translation of memory accesses: loads, and stores. *) Definition transl_memory_access (mk_instr: ireg -> offset -> instruction) - (addr: addressing) (args: list mreg) (k: code) := + (addr: addressing) (args: list mreg) (k: code) : res (list instruction) := match addr, args with - | Aindexed ofs, a1 :: nil => +(*| Aindexed ofs, a1 :: nil => do rs <- ireg_of a1; OK (indexed_memory_access mk_instr rs ofs k) | Aglobal id ofs, nil => - OK (Ploadsymbol_high X31 id ofs :: mk_instr X31 (Ofslow id ofs) :: k) + OK (Ploadsymbol_high GPR31 id ofs :: mk_instr GPR31 (Ofslow id ofs) :: k) | Ainstack ofs, nil => OK (indexed_memory_access mk_instr SP ofs k) - | _, _ => +*)| _, _ => Error(msg "Asmgen.transl_memory_access") end. Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := + (args: list mreg) (dst: mreg) (k: code) : res (list instruction) := match chunk with - | Mint8signed => +(*| Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k | Mint8unsigned => @@ -797,14 +798,14 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of dst; transl_memory_access (Pfld r) addr args k - | _ => +*)| _ => Error (msg "Asmgen.transl_load") end. Definition transl_store (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (src: mreg) (k: code) := + (args: list mreg) (src: mreg) (k: code) : res (list instruction) := match chunk with - | Mint8signed | Mint8unsigned => +(*| Mint8signed | Mint8unsigned => do r <- ireg_of src; transl_memory_access (Psb r) addr args k | Mint16signed | Mint16unsigned => @@ -822,7 +823,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of src; transl_memory_access (Pfsd r) addr args k - | _ => +*)| _ => Error (msg "Asmgen.transl_store") end. @@ -837,18 +838,18 @@ Definition make_epilogue (f: Mach.function) (k: code) := Definition transl_instr (f: Mach.function) (i: Mach.instruction) (ep: bool) (k: code) := match i with - | Mgetstack ofs ty dst => +(*| Mgetstack ofs ty dst => loadind SP ofs ty dst k | Msetstack src ofs ty => storeind src SP ofs ty k | Mgetparam ofs ty dst => (* load via the frame pointer if it is valid *) - do c <- loadind X30 ofs ty dst k; + do c <- loadind GPR30 ofs ty dst k; OK (if ep then c - else loadind_ptr SP f.(fn_link_ofs) X30 c) - | Mop op args res => + else loadind_ptr SP f.(fn_link_ofs) GPR30 c) +*)| Mop op args res => transl_op op args res k - | Mload chunk addr args dst => +(*| Mload chunk addr args dst => transl_load chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k @@ -861,19 +862,21 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (make_epilogue f (Pj_r r1 sig :: k)) | Mtailcall sig (inr symb) => OK (make_epilogue f (Pj_s symb sig :: k)) - | Mbuiltin ef args res => +*)| Mbuiltin ef args res => OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) | Mlabel lbl => OK (Plabel lbl :: k) - | Mgoto lbl => +(*| Mgoto lbl => OK (Pj_l lbl :: k) | Mcond cond args lbl => transl_cbranch cond args lbl k | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) - | Mreturn => +*)| Mreturn => OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k)) + | _ => + Error (msg "Asmgen.transl_instr") end. (** Translation of a code sequence *) |