diff options
Diffstat (limited to 'ia32/Asm.v')
-rw-r--r-- | ia32/Asm.v | 85 |
1 files changed, 42 insertions, 43 deletions
@@ -212,41 +212,41 @@ Inductive instruction: Type := | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list (builtin_arg preg))(res: builtin_res preg) - | Padcl_ir (n: int) (r: ireg) - | Padcl_rr (r1: ireg) (r2: ireg) - | Paddl (r1: ireg) (r2: ireg) - | Paddl_mi (a: addrmode) (n: int) - | Paddl_ri (r1: ireg) (n: int) - | Pbsfl (r1: ireg) (r2: ireg) - | Pbslr (r1: ireg) (r2: ireg) - | Pbswap (r: ireg) + (** Instructions not generated by [Asmgen] *) + | Padc_ri (rd: ireg) (n: int) + | Padc_rr (rd: ireg) (r2: ireg) + | Padd_mi (a: addrmode) (n: int) + | Padd_ri (rd: ireg) (n: int) + | Padd_rr (rd: ireg) (r2: ireg) + | Pbsf (rd: ireg) (r1: ireg) + | Pbsr (rd: ireg) (r1: ireg) + | Pbswap (rd: ireg) + | Pbswap16 (rd: ireg) | Pcfi_adjust (n: int) - | Pfmadd132 (r1: freg) (r2: freg) (r3: freg) - | Pfmadd213 (r1: freg) (r2: freg) (r3: freg) - | Pfmadd231 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub132 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub213 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub231 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg) - | Pmaxsd (r1: freg) (r2: freg) - | Pminsd (r1: freg) (r2: freg) - | Pmovb_rm (rs: ireg) (a: addrmode) - | Pmovq_rm (rs: freg) (a: addrmode) + | Pfmadd132 (rd: freg) (r2: freg) (r3: freg) + | Pfmadd213 (rd: freg) (r2: freg) (r3: freg) + | Pfmadd231 (rd: freg) (r2: freg) (r3: freg) + | Pfmsub132 (rd: freg) (r2: freg) (r3: freg) + | Pfmsub213 (rd: freg) (r2: freg) (r3: freg) + | Pfmsub231 (rd: freg) (r2: freg) (r3: freg) + | Pfnmadd132 (rd: freg) (r2: freg) (r3: freg) + | Pfnmadd213 (rd: freg) (r2: freg) (r3: freg) + | Pfnmadd231 (rd: freg) (r2: freg) (r3: freg) + | Pfnmsub132 (rd: freg) (r2: freg) (r3: freg) + | Pfnmsub213 (rd: freg) (r2: freg) (r3: freg) + | Pfnmsub231 (rd: freg) (r2: freg) (r3: freg) + | Pmaxsd (rd: freg) (r2: freg) + | Pminsd (rd: freg) (r2: freg) + | Pmovb_rm (rd: ireg) (a: addrmode) | Pmovq_mr (a: addrmode) (rs: freg) + | Pmovq_rm (rd: freg) (a: addrmode) | Pmovsb | Pmovsw - | Pmovw_rm (rs: ireg) (ad: addrmode) + | Pmovw_rm (rd: ireg) (ad: addrmode) | Prep_movsl - | Prolw_8 (r: ireg) - | Psbbl (r1: ireg) (r2: ireg) - | Psqrtsd (r1: freg) (r2: freg) - | Psubl_ri (r1: ireg) (n: int) - | Pxchg (r1: ireg) (r2: ireg). + | Psbb_rr (rd: ireg) (r2: ireg) + | Psqrtsd (rd: freg) (r1: freg) + | Psub_ri (rd: ireg) (n: int). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -790,16 +790,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pbuiltin ef args res => Stuck (**r treated specially below *) - (** The following instructions and directives are not generated directly by Asmgen, - so we do not model them. *) - | Padcl_ir _ _ - | Padcl_rr _ _ - | Paddl _ _ - | Paddl_mi _ _ - | Paddl_ri _ _ + (** The following instructions and directives are not generated + directly by [Asmgen], so we do not model them. *) + | Padc_ri _ _ + | Padc_rr _ _ + | Padd_mi _ _ + | Padd_ri _ _ + | Padd_rr _ _ + | Pbsf _ _ + | Pbsr _ _ | Pbswap _ - | Pbsfl _ _ - | Pbslr _ _ + | Pbswap16 _ | Pcfi_adjust _ | Pfmadd132 _ _ _ | Pfmadd213 _ _ _ @@ -822,11 +823,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmovsw | Pmovw_rm _ _ | Prep_movsl - | Prolw_8 _ - | Psbbl _ _ + | Psbb_rr _ _ | Psqrtsd _ _ - | Psubl_ri _ _ - | Pxchg _ _ => Stuck + | Psub_ri _ _ => Stuck end. (** Translation of the LTL/Linear/Mach view of machine registers |