diff options
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 328 |
1 files changed, 205 insertions, 123 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a4364051..36269954 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -15,7 +15,8 @@ (* *) (* *********************************************************************) -(** Translation from Machblock to K1c assembly language (Asmblock) *) +(** * Translation from Machblock to K1c assembly language (Asmblock) + Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *) Require Archi. Require Import Coqlib Errors. @@ -27,6 +28,8 @@ Require Import Chunks. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Import PArithCoercions. + (** 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 @@ -41,23 +44,15 @@ Definition ireg_of (r: mreg) : res ireg := Definition freg_of (r: mreg) : res freg := match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.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. *) - -*) Inductive immed32 : Type := | Imm32_single (imm: int). Definition make_immed32 (val: int) := Imm32_single val. -(** Likewise, for 64-bit integer constants. *) Inductive immed64 : Type := | Imm64_single (imm: int64) . -(* For now, let's suppose all instructions of K1c can handle 64-bits immediate *) Definition make_immed64 (val: int64) := Imm64_single val. Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity). @@ -66,12 +61,6 @@ Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associ Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity). Notation "a @@ b" := (app a b) (at level 49, right associativity). -(** 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 - are generated as required to perform the operation - and prepended to the given instruction sequence [k]. *) - Definition loadimm32 (r: ireg) (n: int) := match make_immed32 n with | Imm32_single imm => Pmake r imm @@ -92,10 +81,6 @@ Definition orimm32 := opimm32 Porw Poriw. Definition norimm32 := opimm32 Pnorw Pnoriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. Definition nxorimm32 := opimm32 Pnxorw Pnxoriw. -(* -Definition sltimm32 := opimm32 Psltw Psltiw. -Definition sltuimm32 := opimm32 Psltuw Psltiuw. -*) Definition loadimm64 (r: ireg) (n: int64) := match make_immed64 n with @@ -118,11 +103,6 @@ Definition norimm64 := opimm64 Pnorl Pnoril. Definition nandimm64 := opimm64 Pnandl Pnandil. Definition nxorimm64 := opimm64 Pnxorl Pnxoril. -(* -Definition sltimm64 := opimm64 Psltl Psltil. -Definition sltuimm64 := opimm64 Psltul Psltiul. -*) - Definition addptrofs (rd rs: ireg) (n: ptrofs) := if Ptrofs.eq_dec n Ptrofs.zero then Pmv rd rs @@ -170,19 +150,6 @@ Definition transl_opt_compuimm transl_compi c Unsigned r1 n lbl k . -(* Definition transl_opt_compuimm - (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := - loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k). *) - -(* match select_comp n c with - | Some Ceq => Pcbu BTweqz r1 lbl ::g k - | Some Cne => Pcbu BTwnez r1 lbl ::g k - | Some _ => nil (* Never happens *) - | None => loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k) - end - . - *) - Definition select_compl (n: int64) (c: comparison) : option comparison := if Int64.eq n Int64.zero then match c with @@ -334,6 +301,75 @@ Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) | Reversed ft => Pfcompl ft rd r2 r1 ::i k end. + +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpuwz (c: comparison) := + match c with + | Cne => OK BTwnez + | Ceq => OK BTweqz + | Clt => Error (msg "btest_for_compuwz: Clt") + | Cge => Error (msg "btest_for_compuwz: Cge") + | Cle => OK BTweqz + | Cgt => OK BTwnez + end. + +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpudz (c: comparison) := + match c with + | Cne => OK BTdnez + | Ceq => OK BTdeqz + | Clt => Error (msg "btest_for_compudz: Clt") + | Cge => Error (msg "btest_for_compudz: Cge") + | Cle => OK BTdeqz + | Cgt => OK BTdnez + end. + +Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) : + res basic := + if ireg_eq rd rs + then OK Pnop + else + (match cond0 with + | Ccomp0 cmp => + OK (PArith (Pcmove (btest_for_cmpswz cmp) rd rc rs)) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (PArith (Pcmoveu bt rd rc rs)) + | Ccompl0 cmp => + OK (PArith (Pcmove (btest_for_cmpsdz cmp) rd rc rs)) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (PArith (Pcmoveu bt rd rc rs)) + end). + +Definition conditional_move_imm32 (cond0 : condition0) (rc rd : ireg) (imm : int) : res basic := + match cond0 with + | Ccomp0 cmp => + OK (PArith (Pcmoveiw (btest_for_cmpswz cmp) rd rc imm)) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (PArith (Pcmoveuiw bt rd rc imm)) + | Ccompl0 cmp => + OK (PArith (Pcmoveiw (btest_for_cmpsdz cmp) rd rc imm)) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (PArith (Pcmoveuiw bt rd rc imm)) + end. + +Definition conditional_move_imm64 (cond0 : condition0) (rc rd : ireg) (imm : int64) : res basic := + match cond0 with + | Ccomp0 cmp => + OK (PArith (Pcmoveil (btest_for_cmpswz cmp) rd rc imm)) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (PArith (Pcmoveuil bt rd rc imm)) + | Ccompl0 cmp => + OK (PArith (Pcmoveil (btest_for_cmpsdz cmp) rd rc imm)) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (PArith (Pcmoveuil bt rd rc imm)) + end. + Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) := match cond, args with @@ -377,28 +413,6 @@ Definition transl_cond_op Error(msg "Asmblockgen.transl_cond_op") end. -(* CoMPare Unsigned Words to Zero *) -Definition btest_for_cmpuwz (c: comparison) := - match c with - | Cne => OK BTwnez - | Ceq => OK BTweqz - | Clt => Error (msg "btest_for_compuwz: Clt") - | Cge => Error (msg "btest_for_compuwz: Cge") - | Cle => Error (msg "btest_for_compuwz: Cle") - | Cgt => Error (msg "btest_for_compuwz: Cgt") - end. - -(* CoMPare Unsigned Words to Zero *) -Definition btest_for_cmpudz (c: comparison) := - match c with - | Cne => OK BTdnez - | Ceq => OK BTdeqz - | Clt => Error (msg "btest_for_compudz: Clt") - | Cge => Error (msg "btest_for_compudz: Cge") - | Cle => Error (msg "btest_for_compudz: Cle") - | Cgt => Error (msg "btest_for_compudz: Cgt") - end. - (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -443,12 +457,33 @@ Definition transl_op | Oaddimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (addimm32 rd rs n ::i k) + | Oaddx shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddxw shift rd rs1 rs2 ::i k) + | Oaddximm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Paddxiw shift rd rs n ::i k) + | Oaddxl shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddxl shift rd rs1 rs2 ::i k) + | Oaddxlimm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Paddxil shift rd rs n ::i k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pnegw rd rs ::i 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 ::i k) + | Orevsubimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubiw rd rs n ::i k) + | Orevsubx shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Prevsubxw shift rd rs1 rs2 ::i k) + | Orevsubximm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubxiw shift rd rs n ::i k) | 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) @@ -543,6 +578,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddiw r1 r2 n ::i k) + | Omsub, 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 (Pmsubw r1 r2 r3 ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -567,6 +608,15 @@ Definition transl_op | Osubl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubl rd rs1 rs2 ::i k) + | Orevsubxl shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Prevsubxl shift rd rs1 rs2 ::i k) + | Orevsublimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubil rd rs n ::i k) + | Orevsubxlimm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubxil shift rd rs n ::i k) | 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) @@ -662,6 +712,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddil r1 r2 n ::i k) + | Omsubl, 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 (Pmsubl r1 r2 r3 ::i k) | Oabsf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfabsd rd rs ::i k) @@ -686,12 +742,52 @@ Definition transl_op | Omulfs, a1 :: a2 :: nil => do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; OK (Pfmulw rd rs1 rs2 ::i k) + | Ominf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmind rd rs1 rs2 ::i k) + | Ominfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfminw rd rs1 rs2 ::i k) + | Omaxf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmaxd rd rs1 rs2 ::i k) + | Omaxfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmaxw rd rs1 rs2 ::i k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfnegd rd rs ::i k) | Onegfs, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfnegw rd rs ::i k) + | Oinvfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfinvw rd rs ::i k) + + | Ofmaddf, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do rs1 <- freg_of a1; + do rs2 <- freg_of a2; + do rs3 <- freg_of a3; + OK (Pfmaddfl rs1 rs2 rs3 ::i k) + | Ofmaddfs, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do rs1 <- freg_of a1; + do rs2 <- freg_of a2; + do rs3 <- freg_of a3; + OK (Pfmaddfw rs1 rs2 rs3 ::i k) + | Ofmsubf, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do rs1 <- freg_of a1; + do rs2 <- freg_of a2; + do rs3 <- freg_of a3; + OK (Pfmsubfl rs1 rs2 rs3 ::i k) + | Ofmsubfs, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do rs1 <- freg_of a1; + do rs2 <- freg_of a2; + do rs3 <- freg_of a3; + OK (Pfmsubfw rs1 rs2 rs3 ::i k) | Osingleofint, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; @@ -742,31 +838,10 @@ Definition transl_op | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle") - | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k - | Oselect cond, a0 :: a1 :: aS :: nil - | Oselectl cond, a0 :: a1 :: aS :: nil - | Oselectf cond, a0 :: a1 :: aS :: nil - | Oselectfs cond, a0 :: a1 :: aS :: nil => - assertion (mreg_eq a0 res); - do r0 <- ireg_of a0; - do r1 <- ireg_of a1; - do rS <- ireg_of aS; - (match cond with - | Ccomp0 cmp => - OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k) - | Ccompu0 cmp => - do bt <- btest_for_cmpuwz cmp; - OK (Pcmoveu bt r0 rS r1 ::i k) - | Ccompl0 cmp => - OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k) - | Ccomplu0 cmp => - do bt <- btest_for_cmpudz cmp; - OK (Pcmoveu bt r0 rS r1 ::i k) - end) | Oextfz stop start, a1 :: nil => assertion (ExtValues.is_bitfield stop start); @@ -800,6 +875,29 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pinsfl stop start rd rs ::i k) + | Osel cond0 ty, aT :: aF :: aC :: nil => + assertion (mreg_eq aT res); + do rT <- ireg_of aT; + do rF <- ireg_of aF; + do rC <- ireg_of aC; + do op <- conditional_move (negate_condition0 cond0) rC rT rF; + OK (op ::i k) + + | Oselimm cond0 imm, aT :: aC :: nil => + assertion (mreg_eq aT res); + do rT <- ireg_of aT; + do rC <- ireg_of aC; + do op <- conditional_move_imm32 (negate_condition0 cond0) rC rT imm; + OK (op ::i k) + + + | Osellimm cond0 imm, aT :: aC :: nil => + assertion (mreg_eq aT res); + do rT <- ireg_of aT; + do rC <- ireg_of aC; + do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm; + OK (op ::i k) + | _, _ => Error(msg "Asmgenblock.transl_op") end. @@ -816,12 +914,12 @@ end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. @@ -837,7 +935,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (PLoadRRO Pld dst) base ofs. + indexed_memory_access (PLoadRRO TRAP Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := indexed_memory_access (PStoreRRO Psd src) base ofs. @@ -897,27 +995,28 @@ Definition chunk2load (chunk: memory_chunk) := | Many64 => Pld_a end. -Definition transl_load_rro (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rro (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access (PLoadRRO (chunk2load chunk) r) addr args k. + transl_memory_access (PLoadRRO trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rrr (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. + transl_memory_access2 (PLoadRRR trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) +Definition transl_load_rrrXS (trap: trapping_mode) (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. + transl_memory_access2XS chunk (PLoadRRRXS trap (chunk2load chunk) r) scale args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with - | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k - | Aindexed2 => transl_load_rrr chunk addr args dst k - | _ => transl_load_rro chunk addr args dst k + | Aindexed2XS scale => transl_load_rrrXS trap chunk scale args dst k + | Aindexed2 => transl_load_rrr trap chunk addr args dst k + | _ => transl_load_rro trap chunk addr args dst k end. Definition chunk2store (chunk: memory_chunk) := @@ -961,7 +1060,7 @@ Definition make_epilogue (f: Machblock.function) (k: code) := (loadind_ptr SP f.(fn_retaddr_ofs) GPRA) ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k. -(** Translation of a Mach instruction. *) +(** Translation of a Machblock instruction. *) Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) (ep: bool) (k: bcode) := @@ -977,8 +1076,8 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c) | MBop op args res => transl_op op args res k - | MBload chunk addr args dst => - transl_load chunk addr args dst k + | MBload trap chunk addr args dst => + transl_load trap chunk addr args dst k | MBstore chunk addr args src => transl_store chunk addr args src k end. @@ -1005,32 +1104,25 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co transl_cbranch cond args lbl nil | MBreturn => OK (make_epilogue f (Pret ::g nil)) - (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) | MBjumptable arg tbl => do r <- ireg_of arg; OK (Pjumptable r tbl ::g nil) end end. -(* TODO - dans l'idée, transl_instr_control renvoie une liste d'instructions sous la forme : - * transl_instr_control _ _ _ = lb ++ (ctl :: nil), où lb est une liste de basics, ctl est un control_inst - - Il faut arriver à exprimer cet aspect là ; extraire le lb, le rajouter dans le body ; et extraire le ctl - qu'on met dans le exit -*) - (** Translation of a code sequence *) Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with + | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP) | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | _ => false + | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBstore chunk addr args res => before end. -(** This is the naive definition that we no longer use because it - is not tail-recursive. It is kept as specification. *) +(** This is the naive definition, which is not tail-recursive unlike the other backends *) Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := match il with @@ -1056,20 +1148,11 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_ transl_basic_rec f il it1p (fun c => OK c). *) (** Translation of a whole function. Note that we must check - that the generated code contains less than [2^32] instructions, + that the generated code contains less than [2^64] instructions, otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -(* Local Obligation Tactic := bblock_auto_correct. *) - -(* Program Definition gen_bblock_noctl (hd: list label) (c: list basic) := - match c with - | nil => {| header := hd; body := Pnop::nil; exit := None |} - | i::c => {| header := hd; body := i::c; exit := None |} - end. - *) - -(** Can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) +(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instruction) := match (extract_ctl ctl) with | None => @@ -1077,7 +1160,6 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil end -(* gen_bblock_noctl hd (c ++ (extract_basic ctl)) :: nil *) | Some (PExpand (Pbuiltin ef args res)) => match c with | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil |