diff options
Diffstat (limited to 'kvx/Asmblockgen.v')
| -rw-r--r-- | kvx/Asmblockgen.v | 1217 |
1 files changed, 1217 insertions, 0 deletions
diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v new file mode 100644 index 00000000..7167cebe --- /dev/null +++ b/kvx/Asmblockgen.v @@ -0,0 +1,1217 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Translation from Machblock to KVX assembly language (Asmblock) + Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *) + +Require Archi. +Require Import Coqlib Errors. +Require Import AST Integers Floats Memdata. +Require Import Op Locations Machblock Asmblock. +Require ExtValues. +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 + types. These properties are true by construction, but it's easier to + recheck them during code generation and fail if they do not hold. *) + +(** Extracting integer or float registers. *) + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.ireg_of") end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. + +Inductive immed32 : Type := + | Imm32_single (imm: int). + +Definition make_immed32 (val: int) := Imm32_single val. + +Inductive immed64 : Type := + | Imm64_single (imm: int64) +. + +Definition make_immed64 (val: int64) := Imm64_single val. + +Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity). +Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity). +Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity). +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). + +Definition loadimm32 (r: ireg) (n: int) := + match make_immed32 n with + | Imm32_single imm => Pmake r imm + end. + +Definition opimm32 (op: arith_name_rrr) + (opimm: arith_name_rri32) + (rd rs: ireg) (n: int) := + match make_immed32 n with + | Imm32_single imm => opimm rd rs imm + 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. +Definition norimm32 := opimm32 Pnorw Pnoriw. +Definition xorimm32 := opimm32 Pxorw Pxoriw. +Definition nxorimm32 := opimm32 Pnxorw Pnxoriw. + +Definition loadimm64 (r: ireg) (n: int64) := + match make_immed64 n with + | Imm64_single imm => Pmakel r imm + end. + +Definition opimm64 (op: arith_name_rrr) + (opimm: arith_name_rri64) + (rd rs: ireg) (n: int64) := + match make_immed64 n with + | Imm64_single imm => opimm rd rs imm +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. +Definition norimm64 := opimm64 Pnorl Pnoril. +Definition nandimm64 := opimm64 Pnandl Pnandil. +Definition nxorimm64 := opimm64 Pnxorl Pnxoril. + +Definition addptrofs (rd rs: ireg) (n: ptrofs) := + if Ptrofs.eq_dec n Ptrofs.zero then + Pmv rd rs + else + addimm64 rd rs (Ptrofs.to_int64 n). + +(** Translation of conditional branches. *) + +Definition transl_comp + (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := + Pcompw (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k. + +Definition transl_compi + (c: comparison) (s: signedness) (r: ireg) (imm: int) (lbl: label) (k: code) : list instruction := + Pcompiw (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k. + +Definition transl_compl + (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := + Pcompl (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k. + +Definition transl_compil + (c: comparison) (s: signedness) (r: ireg) (imm: int64) (lbl: label) (k: code) : list instruction := + Pcompil (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k. + +Definition select_comp (n: int) (c: comparison) : option comparison := + if Int.eq n Int.zero then + match c with + | Ceq => Some Ceq + | Cne => Some Cne + | _ => None + end + else + None + . + +Definition transl_opt_compuimm + (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := + if Int.eq n Int.zero then + match c with + | Ceq => Pcbu BTweqz r1 lbl ::g k + | Cne => Pcbu BTwnez r1 lbl ::g k + | _ => transl_compi c Unsigned r1 n lbl k + end + else + transl_compi c Unsigned r1 n lbl k + . + +Definition select_compl (n: int64) (c: comparison) : option comparison := + if Int64.eq n Int64.zero then + match c with + | Ceq => Some Ceq + | Cne => Some Cne + | _ => None + end + else + None + . + +Definition transl_opt_compluimm + (n: int64) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := + if Int64.eq n Int64.zero then + match c with + | Ceq => Pcbu BTdeqz r1 lbl ::g k + | Cne => Pcbu BTdnez r1 lbl ::g k + | _ => transl_compil c Unsigned r1 n lbl k + end + else + transl_compil c Unsigned r1 n lbl k + . + +Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_float64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_cbranch + (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := + match cond, args with + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_opt_compuimm n c r1 lbl k) + | Ccomp c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp c Signed r1 r2 lbl k) + | Ccompu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp c Unsigned r1 r2 lbl k) + | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (if Int.eq n Int.zero then + Pcb (btest_for_cmpswz c) r1 lbl ::g k + else + transl_compi c Signed r1 n lbl k + ) + | Ccompluimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_opt_compluimm n c r1 lbl k) + | Ccompl c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_compl c Signed r1 r2 lbl k) + | Ccomplu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_compl c Unsigned r1 r2 lbl k) + | Ccomplimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (if Int64.eq n Int64.zero then + Pcb (btest_for_cmpsdz c) r1 lbl ::g k + else + transl_compil c Signed r1 n lbl k + ) + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float64 c r1 r2 lbl k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat64 c r1 r2 lbl k) + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float32 c r1 r2 lbl k) + | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat32 c r1 r2 lbl k) + | _, _ => + Error(msg "Asmgenblock.transl_cbranch") + end. + +(** Translation of a condition operator. The generated code sets the + [rd] target register to 0 or 1 depending on the truth value of the + condition. *) + +Definition transl_cond_int32s (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + Pcompw (itest_for_cmp cmp Signed) rd r1 r2 ::i k. + +Definition transl_cond_int32u (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k. + +Definition transl_cond_int64s (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + Pcompl (itest_for_cmp cmp Signed) rd r1 r2 ::i k. + +Definition transl_cond_int64u (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + Pcompl (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k. + +Definition transl_condimm_int32s (cmp: comparison) (rd r1: ireg) (n: int) (k: bcode) := + Pcompiw (itest_for_cmp cmp Signed) rd r1 n ::i k. + +Definition transl_condimm_int32u (cmp: comparison) (rd r1: ireg) (n: int) (k: bcode) := + Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n ::i k. + +Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := + Pcompil (itest_for_cmp cmp Signed) rd r1 n ::i k. + +Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := + Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k. + + +Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + +Definition transl_cond_float64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | Reversed ft => Pfcompl ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | 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 + | 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 => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_int32u c rd r1 r2 k) + | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_condimm_int32s c rd r1 n k) + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_condimm_int32u c rd r1 n k) + | Ccompl c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_int64s c rd r1 r2 k) + | Ccomplu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_int64u c rd r1 r2 k) + | Ccomplimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_condimm_int64s c rd r1 n k) + | Ccompluimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (transl_condimm_int64u c rd r1 n k) + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float32 c rd r1 r2 k) + | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat32 c rd r1 r2 k) + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float64 c rd r1 r2 k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat64 c rd r1 r2 k) + | _, _ => + Error(msg "Asmblockgen.transl_cond_op") +end. + +(** Translation of the arithmetic operation [r <- op(args)]. + The corresponding instructions are prepended to [k]. *) + +Definition transl_op + (op: operation) (args: list mreg) (res: mreg) (k: bcode) := + match op, args with + | Omove, a1 :: nil => + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmv r a ::i k) + | _ , _ => Error(msg "Asmgenblock.transl_op: Omove") + end + | Ointconst n, nil => + do rd <- ireg_of res; + OK (loadimm32 rd n ::i k) + | Olongconst n, nil => + do rd <- ireg_of res; + OK (loadimm64 rd n ::i k) + | Ofloatconst f, nil => + do rd <- freg_of res; + OK (Pmakef rd f ::i k) + | Osingleconst f, nil => + do rd <- freg_of res; + OK (Pmakefs rd f ::i k) + | Oaddrsymbol s ofs, nil => + do rd <- ireg_of res; + OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero) + then Ploadsymbol s Ptrofs.zero rd ::i addptrofs rd rd ofs ::i k + else Ploadsymbol s ofs rd ::i k) + | Oaddrstack n, nil => + do rd <- ireg_of res; + OK (addptrofs rd SP n ::i k) + + | Ocast8signed, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pslliw rd rs (Int.repr 24) ::i Psraiw rd rd (Int.repr 24) ::i k) + | Ocast16signed, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pslliw rd rs (Int.repr 16) ::i Psraiw rd rd (Int.repr 16) ::i k) + | Oadd, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddw rd rs1 rs2 ::i k) + | 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) + | 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 *) + | Oand, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pandw rd rs1 rs2 ::i k) + | Oandimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (andimm32 rd rs n ::i k) + | Onand, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnandw rd rs1 rs2 ::i k) + | Onandimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nandimm32 rd rs n ::i k) + | Oor, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Porw rd rs1 rs2 ::i k) + | Onor, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnorw rd rs1 rs2 ::i k) + | Oorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (orimm32 rd rs n ::i k) + | Onorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (norimm32 rd rs n ::i k) + | Oxor, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pxorw rd rs1 rs2 ::i k) + | Oxorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm32 rd rs n ::i k) + | Onxor, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnxorw rd rs1 rs2 ::i k) + | Onxorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nxorimm32 rd rs n ::i k) + | Onot, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm32 rd rs Int.mone ::i k) + | Oandn, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pandnw rd rs1 rs2 ::i k) + | Oandnimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pandniw rd rs n ::i k) + | Oorn, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pornw rd rs1 rs2 ::i k) + | Oornimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Porniw rd rs n ::i k) + | Oshl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Psllw rd rs1 rs2 ::i k) + | Oshlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pslliw rd rs n ::i k) + | Oshr, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Psraw rd rs1 rs2 ::i k) + | Oshrimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psraiw rd rs n ::i k) + | Oshru, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Psrlw rd rs1 rs2 ::i k) + | Oshruimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psrliw rd rs n ::i k) + | Oshrximm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psrxiw rd rs n ::i k) + | 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) + | 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; + OK (Pcvtl2w rd rs ::i k) + | Ocast32signed, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psxwd rd rs ::i k) + | Ocast32unsigned, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pzxwd rd rs ::i k) +(* assertion (ireg_eq rd rs); + OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k) *) + | Oaddl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddl rd rs1 rs2 ::i k) + | Oaddlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (addimm64 rd rs n ::i k) + | Onegl, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pnegl rd rs ::i 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 ::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) + | 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 *) + | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu") (* Géré par fonction externe *) + | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl") (* Géré par fonction externe *) + | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu") (* Géré par fonction externe *) + | Onotl, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm64 rd rs Int64.mone ::i k) + | Oandl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pandl rd rs1 rs2 ::i k) + | Oandlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (andimm64 rd rs n ::i k) + | Onandl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnandl rd rs1 rs2 ::i k) + | Onandlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nandimm64 rd rs n ::i k) + | Oorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Porl rd rs1 rs2 ::i k) + | Oorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (orimm64 rd rs n ::i k) + | Onorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnorl rd rs1 rs2 ::i k) + | Onorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (norimm64 rd rs n ::i k) + | Oxorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pxorl rd rs1 rs2 ::i k) + | Oxorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm64 rd rs n ::i k) + | Onxorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnxorl rd rs1 rs2 ::i k) + | Onxorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nxorimm64 rd rs n ::i k) + | Oandnl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pandnl rd rs1 rs2 ::i k) + | Oandnlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pandnil rd rs n ::i k) + | Oornl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pornl rd rs1 rs2 ::i k) + | Oornlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pornil rd rs n ::i k) + | Oshll, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pslll rd rs1 rs2 ::i k) + | Oshllimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psllil rd rs n ::i k) + | Oshrl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Psral rd rs1 rs2 ::i k) + | Oshrlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psrail rd rs n ::i k) + | Oshrlu, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Psrll rd rs1 rs2 ::i k) + | Oshrluimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psrlil rd rs n ::i k) + | Oshrxlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Psrxil rd rs 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) + | 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) + | Oabsfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfabsw rd rs ::i k) + | Oaddf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfaddd rd rs1 rs2 ::i k) + | Oaddfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfaddw rd rs1 rs2 ::i k) + | Osubf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsbfd rd rs1 rs2 ::i k) + | Osubfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsbfw rd rs1 rs2 ::i k) + | Omulf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmuld rd rs1 rs2 ::i k) + | 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; + OK (Pfloatwrnsz rd rs ::i k) + | Osingleofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatuwrnsz rd rs ::i k) + | Ofloatoflong, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatdrnsz rd rs ::i k) + | Ofloatoflongu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatudrnsz rd rs ::i k) + | Ointofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedwrzz rd rs ::i k) + | Ointuofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeduwrzz rd rs ::i k) + | Olongoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeddrzz rd rs ::i k) + | Ointoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeddrzz_i32 rd rs ::i k) + | Ointuoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrzz_i32 rd rs ::i k) + | Olonguoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrzz rd rs ::i k) + + | Ofloatofsingle, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfwidenlwd rd rs ::i k) + | Osingleoffloat, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfnarrowdw rd rs ::i k) + + + | Odivf , _ => Error (msg "Asmblockgen.transl_op: Odivf") + | Odivfs, _ => Error (msg "Asmblockgen.transl_op: Odivfs") + + (* We use the Splitlong instead for these four conversions *) + | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") + | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu") + | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle") + | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle") + + + | Ocmp cmp, _ => + do rd <- ireg_of res; + transl_cond_op cmp rd args k + + + | Oextfz stop start, a1 :: nil => + assertion (ExtValues.is_bitfield stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfz stop start rd rs ::i k) + + | Oextfs stop start, a1 :: nil => + assertion (ExtValues.is_bitfield stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfs stop start rd rs ::i k) + + | Oextfzl stop start, a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfzl stop start rd rs ::i k) + + | Oextfsl stop start, a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfsl stop start rd rs ::i k) + + | Oinsf stop start, a0 :: a1 :: nil => + assertion (ExtValues.is_bitfield stop start); + assertion (mreg_eq a0 res); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pinsf stop start rd rs ::i k) + + | Oinsfl stop start, a0 :: a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + assertion (mreg_eq a0 res); + 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. + +(** Accessing data in the stack frame. *) + +Definition indexed_memory_access + (mk_instr: ireg -> offset -> basic) + (base: ireg) (ofs: ptrofs) := + match make_immed64 (Ptrofs.to_int64 ofs) with + | Imm64_single imm => + mk_instr base (Ptrofs.of_int64 imm) +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 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. + +Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) := + match ty, preg_of src with + | Tint, IR rd => OK (indexed_memory_access (PStoreRRO Psw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PStoreRRO Psd rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PStoreRRO Pfss rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PStoreRRO Pfsd rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PStoreRRO Psw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PStoreRRO Psd_a rd) base ofs ::i k) + | _, _ => Error (msg "Asmblockgen.storeind") + end. + +Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := + 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. + +(** Translation of memory accesses: loads, and stores. *) + +Definition transl_memory_access2 + (mk_instr: ireg -> ireg -> basic) + (addr: addressing) (args: list mreg) (k: bcode) : res bcode := + match addr, args with + | Aindexed2, a1 :: a2 :: nil => + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (mk_instr rs1 rs2 ::i k) + | _, _ => Error (msg "Asmblockgen.transl_memory_access2") + end. + +Definition transl_memory_access2XS + (chunk: memory_chunk) + (mk_instr: ireg -> ireg -> basic) + scale (args: list mreg) (k: bcode) : res bcode := + match args with + | (a1 :: a2 :: nil) => + assertion (Z.eqb (zscale_of_chunk chunk) scale); + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (mk_instr rs1 rs2 ::i k) + | _ => Error (msg "Asmblockgen.transl_memory_access2XS") + end. + +Definition transl_memory_access + (mk_instr: ireg -> offset -> basic) + (addr: addressing) (args: list mreg) (k: bcode) : res bcode := + match addr, args with + | Aindexed ofs, a1 :: nil => + do rs <- ireg_of a1; + OK (indexed_memory_access mk_instr rs ofs ::i k) + | Aglobal id ofs, nil => + OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP Ptrofs.zero ::i k)) + | Ainstack ofs, nil => + OK (indexed_memory_access mk_instr SP ofs ::i k) + | _, _ => + Error(msg "Asmblockgen.transl_memory_access") + end. + +Definition chunk2load (chunk: memory_chunk) := + match chunk with + | Mint8signed => Plb + | Mint8unsigned => Plbu + | Mint16signed => Plh + | Mint16unsigned => Plhu + | Mint32 => Plw + | Mint64 => Pld + | Mfloat32 => Pfls + | Mfloat64 => Pfld + | Many32 => Plw_a + | Many64 => Pld_a + end. + +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 trap (chunk2load chunk) r) addr args k. + +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 trap (chunk2load chunk) r) addr args k. + +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 trap (chunk2load chunk) r) scale args k. + +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 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) := + match chunk with + | Mint8signed | Mint8unsigned => Psb + | Mint16signed | Mint16unsigned => Psh + | Mint32 => Psw + | Mint64 => Psd + | Mfloat32 => Pfss + | Mfloat64 => Pfsd + | Many32 => Psw_a + | Many64 => Psd_a + end. + +Definition transl_store_rro (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access (PStoreRRO (chunk2store chunk) r) addr args k. + +Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k. + +Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k. + +Definition transl_store (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + match addr with + | Aindexed2 => transl_store_rrr chunk addr args src k + | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k + | _ => transl_store_rro chunk addr args src k + end. + +(** Function epilogue *) + +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 Machblock instruction. *) + +Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) + (ep: bool) (k: bcode) := + match i with + | MBgetstack ofs ty dst => + loadind SP ofs ty dst k + | MBsetstack src ofs ty => + storeind src SP ofs ty k + | MBgetparam ofs ty dst => + (* load via the frame pointer if it is valid *) + do c <- loadind FP ofs ty dst k; + OK (if ep then c + else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c) + | MBop op args res => + transl_op op args res 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. + +Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.control_flow_inst) + : res code := + match oi with + | None => OK nil + | Some i => + match i with + | MBcall sig (inl r) => + do r1 <- ireg_of r; OK ((Picall r1) ::g nil) + | MBcall sig (inr symb) => + OK ((Pcall symb) ::g nil) + | MBtailcall sig (inr symb) => + OK (make_epilogue f ((Pgoto symb) ::g nil)) + | MBtailcall sig (inl r) => + do r1 <- ireg_of r; OK (make_epilogue f ((Pigoto r1) ::g nil)) + | MBbuiltin ef args res => + OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) ::g nil) + | MBgoto lbl => + OK (Pj_l lbl ::g nil) + | MBcond cond args lbl => + transl_cbranch cond args lbl nil + | MBreturn => + OK (make_epilogue f (Pret ::g nil)) + | MBjumptable arg tbl => + do r <- ireg_of arg; + OK (Pjumptable r tbl ::g nil) + end + end. + +(** 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) + | 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, 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 + | nil => OK nil + | i1 :: il' => + do k <- transl_basic_code f il' (fp_is_parent it1p i1); + transl_instr_basic f i1 it1p k + end. + +(* (** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_basic_rec (f: Machblock.function) (il: list Machblock.basic_inst) + (it1p: bool) (k: bcode -> res bcode) := + match il with + | nil => k nil + | i1 :: il' => + transl_basic_rec f il' (fp_is_parent it1p i1) + (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2) + end. + +Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := + 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^64] instructions, + otherwise the offset part of the [PC] code pointer could wrap + around, leading to incorrect executions. *) + +(* 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 => + match c with + | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil + | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil + end + | Some (PExpand (Pbuiltin ef args res)) => + match c with + | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil + | _ => {| header := hd; body := c; exit := None |} + :: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil + end + | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil + end +. +Next Obligation. + apply wf_bblock_refl. constructor. + left. auto. + discriminate. +Qed. Next Obligation. + apply wf_bblock_refl. constructor. + right. 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) := + do c <- transl_basic_code f fb.(Machblock.body) ep; + do ctl <- transl_instr_control f fb.(Machblock.exit); + OK (gen_bblocks fb.(Machblock.header) c ctl) +. + +Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) := + match lmb with + | nil => OK nil + | mb :: lmb => + do lb <- transl_block f mb (if Machblock.header mb then ep else false); + do lb' <- transl_blocks f lmb false; + OK (lb @@ lb') + end +. + +Program Definition make_prologue (f: Machblock.function) lb := + ({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::i + Pget GPRA RA ::i + storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::i nil; + exit := None |} :: lb). + +Definition transl_function (f: Machblock.function) := + do lb <- transl_blocks f f.(Machblock.fn_code) true; + OK (mkfunction f.(Machblock.fn_sig) + (make_prologue f lb)). + +Definition transf_function (f: Machblock.function) : res Asmvliw.function := + do tf <- transl_function f; + if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks)) + then Error (msg "code size exceeded") + else OK tf. + +Definition transf_fundef (f: Machblock.fundef) : res Asmvliw.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Machblock.program) : res Asmvliw.program := + transform_partial_program transf_fundef p. |