diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-19 09:54:40 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-19 09:54:40 +0000 |
| commit | be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec (patch) | |
| tree | c51b66e9154bc64cf4fd4191251f29d102928841 /ia32/Asm.v | |
| parent | 60e1fd71c7e97b2214daf574e0f41b55a3e0bceb (diff) | |
Merge of the float32 branch:
- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asm.v')
| -rw-r--r-- | ia32/Asm.v | 18 |
1 files changed, 6 insertions, 12 deletions
@@ -115,8 +115,6 @@ Inductive instruction: Type := | Pmov_ra (rd: ireg) (id: ident) | Pmov_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) - | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) - | Pmovd_rf (rd: ireg) (rd: freg) | Pmovsd_ff (rd: freg) (r1: freg) (**r [movsd] (single 64-bit float) *) | Pmovsd_fi (rd: freg) (n: float) (**r (pseudo-instruction) *) | Pmovsd_fm (rd: freg) (a: addrmode) @@ -129,16 +127,16 @@ Inductive instruction: Type := (** Moves with conversion *) | Pmovb_mr (a: addrmode) (rs: ireg) (**r [mov] (8-bit int) *) | Pmovw_mr (a: addrmode) (rs: ireg) (**r [mov] (16-bit int) *) - | Pmovzb_rr (rd: ireg) (rs: ireg) (**r [movzb] (8-bit zero-extension) *) + | Pmovzb_rr (rd: ireg) (rs: ireg) (**r [movzb] (8-bit zero-extension) *) | Pmovzb_rm (rd: ireg) (a: addrmode) - | Pmovsb_rr (rd: ireg) (rs: ireg) (**r [movsb] (8-bit sign-extension) *) + | Pmovsb_rr (rd: ireg) (rs: ireg) (**r [movsb] (8-bit sign-extension) *) | Pmovsb_rm (rd: ireg) (a: addrmode) - | Pmovzw_rr (rd: ireg) (rs: ireg) (**r [movzw] (16-bit zero-extension) *) + | Pmovzw_rr (rd: ireg) (rs: ireg) (**r [movzw] (16-bit zero-extension) *) | Pmovzw_rm (rd: ireg) (a: addrmode) - | Pmovsw_rr (rd: ireg) (rs: ireg) (**r [movsw] (16-bit sign-extension) *) + | Pmovsw_rr (rd: ireg) (rs: ireg) (**r [movsw] (16-bit sign-extension) *) | Pmovsw_rm (rd: ireg) (a: addrmode) | Pcvtss2sd_fm (rd: freg) (a: addrmode) (**r [cvtss2sd] (single float load) *) - | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r pseudo (single conversion) *) + | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r conversion to single (pseudo) *) | Pcvtsd2ss_mf (a: addrmode) (r1: freg) (**r [cvtsd2ss] (single float store *) | Pcvttsd2si_rf (rd: ireg) (r1: freg) (**r double to signed int *) | Pcvtsi2sd_fr (rd: freg) (r1: ireg) (**r signed int to double *) @@ -185,7 +183,7 @@ Inductive instruction: Type := | Pjmp_s (symb: ident) | Pjmp_r (r: ireg) | Pjcc (c: testcond)(l: label) - | Pjcc2 (c1 c2: testcond)(l: label) + | Pjcc2 (c1 c2: testcond)(l: label) (**r pseudo *) | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *) | Pcall_s (symb: ident) | Pcall_r (r: ireg) @@ -481,10 +479,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome exec_load Mint32 m a rs rd | Pmov_mr a r1 => exec_store Mint32 m a rs r1 nil - | Pmovd_fr rd r1 => - Next (nextinstr (rs#rd <- (rs r1))) m - | Pmovd_rf rd r1 => - Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_ff rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_fi rd n => |