From a14b9578ee5297d954103e05d7b2d322816ddd8f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:38:24 +0200 Subject: Support for 64-bit architectures: x86 in 64-bit mode This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing. --- ia32/Asm.v | 543 ++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 362 insertions(+), 181 deletions(-) (limited to 'ia32/Asm.v') diff --git a/ia32/Asm.v b/ia32/Asm.v index b4fc950b..01ecb15a 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -2,7 +2,7 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -12,19 +12,9 @@ (** Abstract syntax and semantics for IA32 assembly language *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Locations. -Require Import Stacklayout. -Require Import Conventions. +Require Import Coqlib Maps. +Require Import AST Integers Floats Values Memory Events Globalenvs Smallstep. +Require Import Locations Stacklayout Conventions. (** * Abstract syntax *) @@ -33,14 +23,14 @@ Require Import Conventions. (** Integer registers. *) Inductive ireg: Type := - | EAX: ireg | EBX: ireg | ECX: ireg | EDX: ireg - | ESI: ireg | EDI: ireg | EBP: ireg | ESP: ireg. + | RAX | RBX | RCX | RDX | RSI | RDI | RBP | RSP + | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15. (** Floating-point registers, i.e. SSE2 registers *) Inductive freg: Type := - | XMM0: freg | XMM1: freg | XMM2: freg | XMM3: freg - | XMM4: freg | XMM5: freg | XMM6: freg | XMM7: freg. + | XMM0 | XMM1 | XMM2 | XMM3 | XMM4 | XMM5 | XMM6 | XMM7 + | XMM8 | XMM9 | XMM10 | XMM11 | XMM12 | XMM13 | XMM14 | XMM15. Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. @@ -69,7 +59,7 @@ Coercion CR: crbit >-> preg. (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) -Notation SP := ESP (only parsing). +Notation SP := RSP (only parsing). (** ** Instruction set. *) @@ -79,8 +69,8 @@ Definition label := positive. Inductive addrmode: Type := | Addrmode (base: option ireg) - (ofs: option (ireg * int)) - (const: int + ident * int). + (ofs: option (ireg * Z)) + (const: Z + ident * ptrofs). (** Testable conditions (for conditional jumps and more). *) @@ -94,7 +84,15 @@ Inductive testcond: Type := registers, memory references and immediate constants as arguments. Here, we list only the combinations that we actually use. - Naming conventions: + Naming conventions for types: +- [b]: 8 bits +- [w]: 16 bits ("word") +- [l]: 32 bits ("longword") +- [q]: 64 bits ("quadword") +- [d] or [sd]: FP double precision (64 bits) +- [s] or [ss]: FP single precision (32 bits) + + Naming conventions for operands: - [r]: integer register operand - [f]: XMM register operand - [m]: memory operand @@ -109,11 +107,14 @@ Inductive testcond: Type := Inductive instruction: Type := (** Moves *) - | Pmov_rr (rd: ireg) (r1: ireg) (**r [mov] (32-bit int) *) - | Pmov_ri (rd: ireg) (n: int) - | Pmov_ra (rd: ireg) (id: ident) - | Pmov_rm (rd: ireg) (a: addrmode) - | Pmov_mr (a: addrmode) (rs: ireg) + | Pmov_rr (rd: ireg) (r1: ireg) (**r [mov] (integer) *) + | Pmovl_ri (rd: ireg) (n: int) + | Pmovq_ri (rd: ireg) (n: int64) + | Pmov_rs (rd: ireg) (id: ident) + | Pmovl_rm (rd: ireg) (a: addrmode) + | Pmovq_rm (rd: ireg) (a: addrmode) + | Pmovl_mr (a: addrmode) (rs: ireg) + | Pmovq_mr (a: addrmode) (rs: ireg) | 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) @@ -125,7 +126,6 @@ Inductive instruction: Type := | Pfstpl_m (a: addrmode) (**r [fstp] double precision *) | Pflds_m (a: addrmode) (**r [fld] simple precision *) | Pfstps_m (a: addrmode) (**r [fstp] simple precision *) - | Pxchg_rr (r1: ireg) (r2: ireg) (**r register-register exchange *) (** 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) *) @@ -137,43 +137,81 @@ Inductive instruction: Type := | Pmovzw_rm (rd: ireg) (a: addrmode) | Pmovsw_rr (rd: ireg) (rs: ireg) (**r [movsw] (16-bit sign-extension) *) | Pmovsw_rm (rd: ireg) (a: addrmode) + | Pmovzl_rr (rd: ireg) (rs: ireg) (**r [movzl] (32-bit zero-extension) *) + | Pmovsl_rr (rd: ireg) (rs: ireg) (**r [movsl] (32-bit sign-extension) *) + | Pmovls_rr (rd: ireg) (** 64 to 32 bit conversion (pseudo) *) | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r conversion to single float *) | Pcvtss2sd_ff (rd: freg) (r1: freg) (**r conversion to double float *) | Pcvttsd2si_rf (rd: ireg) (r1: freg) (**r double to signed int *) | Pcvtsi2sd_fr (rd: freg) (r1: ireg) (**r signed int to double *) | Pcvttss2si_rf (rd: ireg) (r1: freg) (**r single to signed int *) | Pcvtsi2ss_fr (rd: freg) (r1: ireg) (**r signed int to single *) + | Pcvttsd2sl_rf (rd: ireg) (r1: freg) (**r double to signed long *) + | Pcvtsl2sd_fr (rd: freg) (r1: ireg) (**r signed long to double *) + | Pcvttss2sl_rf (rd: ireg) (r1: freg) (**r single to signed long *) + | Pcvtsl2ss_fr (rd: freg) (r1: ireg) (**r signed long to single *) (** Integer arithmetic *) - | Plea (rd: ireg) (a: addrmode) - | Pneg (rd: ireg) - | Psub_rr (rd: ireg) (r1: ireg) - | Pimul_rr (rd: ireg) (r1: ireg) - | Pimul_ri (rd: ireg) (n: int) - | Pimul_r (r1: ireg) - | Pmul_r (r1: ireg) + | Pleal (rd: ireg) (a: addrmode) + | Pleaq (rd: ireg) (a: addrmode) + | Pnegl (rd: ireg) + | Pnegq (rd: ireg) + | Paddl_ri (rd: ireg) (n: int) + | Paddq_ri (rd: ireg) (n: int64) + | Psubl_rr (rd: ireg) (r1: ireg) + | Psubq_rr (rd: ireg) (r1: ireg) + | Pimull_rr (rd: ireg) (r1: ireg) + | Pimulq_rr (rd: ireg) (r1: ireg) + | Pimull_ri (rd: ireg) (n: int) + | Pimulq_ri (rd: ireg) (n: int64) + | Pimull_r (r1: ireg) +(* | Pimulq_r (r1: ireg) *) + | Pmull_r (r1: ireg) +(* | Pmulq_r (r1: ireg) *) | Pcltd - | Pdiv (r1: ireg) - | Pidiv (r1: ireg) - | Pand_rr (rd: ireg) (r1: ireg) - | Pand_ri (rd: ireg) (n: int) - | Por_rr (rd: ireg) (r1: ireg) - | Por_ri (rd: ireg) (n: int) - | Pxor_r (rd: ireg) (**r [xor] with self = set to zero *) - | Pxor_rr (rd: ireg) (r1: ireg) - | Pxor_ri (rd: ireg) (n: int) - | Pnot (rd: ireg) - | Psal_rcl (rd: ireg) - | Psal_ri (rd: ireg) (n: int) - | Pshr_rcl (rd: ireg) - | Pshr_ri (rd: ireg) (n: int) - | Psar_rcl (rd: ireg) - | Psar_ri (rd: ireg) (n: int) + | Pcqto + | Pdivl (r1: ireg) + | Pdivq (r1: ireg) + | Pidivl (r1: ireg) + | Pidivq (r1: ireg) + | Pandl_rr (rd: ireg) (r1: ireg) + | Pandq_rr (rd: ireg) (r1: ireg) + | Pandl_ri (rd: ireg) (n: int) + | Pandq_ri (rd: ireg) (n: int64) + | Porl_rr (rd: ireg) (r1: ireg) + | Porq_rr (rd: ireg) (r1: ireg) + | Porl_ri (rd: ireg) (n: int) + | Porq_ri (rd: ireg) (n: int64) + | Pxorl_r (rd: ireg) (**r [xor] with self = set to zero *) + | Pxorq_r (rd: ireg) + | Pxorl_rr (rd: ireg) (r1: ireg) + | Pxorq_rr (rd: ireg) (r1: ireg) + | Pxorl_ri (rd: ireg) (n: int) + | Pxorq_ri (rd: ireg) (n: int64) + | Pnotl (rd: ireg) + | Pnotq (rd: ireg) + | Psall_rcl (rd: ireg) + | Psalq_rcl (rd: ireg) + | Psall_ri (rd: ireg) (n: int) + | Psalq_ri (rd: ireg) (n: int) + | Pshrl_rcl (rd: ireg) + | Pshrq_rcl (rd: ireg) + | Pshrl_ri (rd: ireg) (n: int) + | Pshrq_ri (rd: ireg) (n: int) + | Psarl_rcl (rd: ireg) + | Psarq_rcl (rd: ireg) + | Psarl_ri (rd: ireg) (n: int) + | Psarq_ri (rd: ireg) (n: int) | Pshld_ri (rd: ireg) (r1: ireg) (n: int) - | Pror_ri (rd: ireg) (n: int) - | Pcmp_rr (r1 r2: ireg) - | Pcmp_ri (r1: ireg) (n: int) - | Ptest_rr (r1 r2: ireg) - | Ptest_ri (r1: ireg) (n: int) + | Prorl_ri (rd: ireg) (n: int) + | Prorq_ri (rd: ireg) (n: int) + | Pcmpl_rr (r1 r2: ireg) + | Pcmpq_rr (r1 r2: ireg) + | Pcmpl_ri (r1: ireg) (n: int) + | Pcmpq_ri (r1: ireg) (n: int64) + | Ptestl_rr (r1 r2: ireg) + | Ptestq_rr (r1 r2: ireg) + | Ptestl_ri (r1: ireg) (n: int) + | Ptestq_ri (r1: ireg) (n: int64) | Pcmov (c: testcond) (rd: ireg) (r1: ireg) | Psetcc (c: testcond) (rd: ireg) (** Floating-point arithmetic *) @@ -204,24 +242,26 @@ Inductive instruction: Type := | Pcall_r (r: ireg) (sg: signature) | Pret (** Saving and restoring registers *) - | Pmov_rm_a (rd: ireg) (a: addrmode) (**r like [Pmov_rm], using [Many32] chunk *) - | Pmov_mr_a (a: addrmode) (rs: ireg) (**r like [Pmov_mr], using [Many32] chunk *) + | Pmov_rm_a (rd: ireg) (a: addrmode) (**r like [Pmov_rm], using [Many64] chunk *) + | Pmov_mr_a (a: addrmode) (rs: ireg) (**r like [Pmov_mr], using [Many64] chunk *) | Pmovsd_fm_a (rd: freg) (a: addrmode) (**r like [Pmovsd_fm], using [Many64] chunk *) | Pmovsd_mf_a (a: addrmode) (r1: freg) (**r like [Pmovsd_mf], using [Many64] chunk *) (** Pseudo-instructions *) | Plabel(l: label) - | Pallocframe(sz: Z)(ofs_ra ofs_link: int) - | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) + | Pallocframe(sz: Z)(ofs_ra ofs_link: ptrofs) + | Pfreeframe(sz: Z)(ofs_ra ofs_link: ptrofs) | Pbuiltin(ef: external_function)(args: list (builtin_arg preg))(res: builtin_res preg) - (** 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) + (** Instructions not generated by [Asmgen] -- TO CHECK *) + | Padcl_ri (rd: ireg) (n: int) + | Padcl_rr (rd: ireg) (r2: ireg) + | Paddl_mi (a: addrmode) (n: int) + | Paddl_rr (rd: ireg) (r2: ireg) + | Pbsfl (rd: ireg) (r1: ireg) + | Pbsfq (rd: ireg) (r1: ireg) + | Pbsrl (rd: ireg) (r1: ireg) + | Pbsrq (rd: ireg) (r1: ireg) + | Pbswap64 (rd: ireg) + | Pbswap32 (rd: ireg) | Pbswap16 (rd: ireg) | Pcfi_adjust (n: int) | Pfmadd132 (rd: freg) (r2: freg) (r3: freg) @@ -239,15 +279,16 @@ Inductive instruction: Type := | 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) + | Pmovsq_mr (a: addrmode) (rs: freg) + | Pmovsq_rm (rd: freg) (a: addrmode) | Pmovsb | Pmovsw | Pmovw_rm (rd: ireg) (ad: addrmode) | Prep_movsl - | Psbb_rr (rd: ireg) (r2: ireg) + | Psbbl_rr (rd: ireg) (r2: ireg) | Psqrtsd (rd: freg) (r1: freg) - | Psub_ri (rd: ireg) (n: int). + | Psubl_ri (rd: ireg) (n: int) + | Psubq_ri (rd: ireg) (n: int64). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -334,22 +375,44 @@ Variable ge: genv. (** Evaluating an addressing mode *) -Definition eval_addrmode (a: addrmode) (rs: regset) : val := - match a with Addrmode base ofs const => - Val.add (match base with - | None => Vzero - | Some r => rs r +Definition eval_addrmode32 (a: addrmode) (rs: regset) : val := + let '(Addrmode base ofs const) := a in + Val.add (match base with + | None => Vint Int.zero + | Some r => rs r + end) + (Val.add (match ofs with + | None => Vint Int.zero + | Some(r, sc) => + if zeq sc 1 + then rs r + else Val.mul (rs r) (Vint (Int.repr sc)) end) - (Val.add (match ofs with - | None => Vzero - | Some(r, sc) => - if Int.eq sc Int.one then rs r else Val.mul (rs r) (Vint sc) - end) - (match const with - | inl ofs => Vint ofs - | inr(id, ofs) => Genv.symbol_address ge id ofs - end)) - end. + (match const with + | inl ofs => Vint (Int.repr ofs) + | inr(id, ofs) => Genv.symbol_address ge id ofs + end)). + +Definition eval_addrmode64 (a: addrmode) (rs: regset) : val := + let '(Addrmode base ofs const) := a in + Val.addl (match base with + | None => Vlong Int64.zero + | Some r => rs r + end) + (Val.addl (match ofs with + | None => Vlong Int64.zero + | Some(r, sc) => + if zeq sc 1 + then rs r + else Val.mull (rs r) (Vlong (Int64.repr sc)) + end) + (match const with + | inl ofs => Vlong (Int64.repr ofs) + | inr(id, ofs) => Genv.symbol_address ge id ofs + end)). + +Definition eval_addrmode (a: addrmode) (rs: regset) : val := + if Archi.ptr64 then eval_addrmode64 a rs else eval_addrmode32 a rs. (** Performing a comparison *) @@ -368,6 +431,13 @@ Definition compare_ints (x y: val) (rs: regset) (m: mem): regset := #OF <- (Val.sub_overflow x y) #PF <- Vundef. +Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := + rs #ZF <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq x y)) + #CF <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt x y)) + #SF <- (Val.negativel (Val.subl x y)) + #OF <- (Val.subl_overflow x y) + #PF <- Vundef. + (** Floating-point comparison between x and y: - ZF = 1 if x=y or unordered, 0 if x<>y - CF = 1 if x=y @@ -481,7 +551,7 @@ Inductive outcome: Type := to [Vundef] in addition to incrementing the [PC]. *) Definition nextinstr (rs: regset) := - rs#PC <- (Val.add rs#PC Vone). + rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one). Definition nextinstr_nf (rs: regset) : regset := nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs). @@ -491,7 +561,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := | None => Stuck | Some pos => match rs#PC with - | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m | _ => Stuck end end. @@ -537,14 +607,20 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** Moves *) | Pmov_rr rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m - | Pmov_ri rd n => + | Pmovl_ri rd n => Next (nextinstr_nf (rs#rd <- (Vint n))) m - | Pmov_ra rd id => - Next (nextinstr_nf (rs#rd <- (Genv.symbol_address ge id Int.zero))) m - | Pmov_rm rd a => + | Pmovq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Vlong n))) m + | Pmov_rs rd id => + Next (nextinstr_nf (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero))) m + | Pmovl_rm rd a => exec_load Mint32 m a rs rd - | Pmov_mr a r1 => + | Pmovq_rm rd a => + exec_load Mint64 m a rs rd + | Pmovl_mr a r1 => exec_store Mint32 m a rs r1 nil + | Pmovq_mr a r1 => + exec_store Mint64 m a rs r1 nil | Pmovsd_ff rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_fi rd n => @@ -567,8 +643,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out exec_load Mfloat32 m a rs ST0 | Pfstps_m a => exec_store Mfloat32 m a rs ST0 (ST0 :: nil) - | Pxchg_rr r1 r2 => - Next (nextinstr (rs#r1 <- (rs r2) #r2 <- (rs r1))) m (** Moves with conversion *) | Pmovb_mr a r1 => exec_store Mint8unsigned m a rs r1 nil @@ -590,6 +664,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m | Pmovsw_rm rd a => exec_load Mint16signed m a rs rd + | Pmovzl_rr rd r1 => + Next (nextinstr (rs#rd <- (Val.longofintu rs#r1))) m + | Pmovsl_rr rd r1 => + Next (nextinstr (rs#rd <- (Val.longofint rs#r1))) m + | Pmovls_rr rd => + Next (nextinstr (rs#rd <- (Val.loword rs#rd))) m | Pcvtsd2ss_ff rd r1 => Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m | Pcvtss2sd_ff rd r1 => @@ -602,85 +682,165 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.maketotal (Val.intofsingle rs#r1)))) m | Pcvtsi2ss_fr rd r1 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofint rs#r1)))) m + | Pcvttsd2sl_rf rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m + | Pcvtsl2sd_fr rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m + | Pcvttss2sl_rf rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.longofsingle rs#r1)))) m + | Pcvtsl2ss_fr rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflong rs#r1)))) m (** Integer arithmetic *) - | Plea rd a => - Next (nextinstr (rs#rd <- (eval_addrmode a rs))) m - | Pneg rd => + | Pleal rd a => + Next (nextinstr (rs#rd <- (eval_addrmode32 a rs))) m + | Pleaq rd a => + Next (nextinstr (rs#rd <- (eval_addrmode64 a rs))) m + | Pnegl rd => Next (nextinstr_nf (rs#rd <- (Val.neg rs#rd))) m - | Psub_rr rd r1 => + | Pnegq rd => + Next (nextinstr_nf (rs#rd <- (Val.negl rs#rd))) m + | Paddl_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.add rs#rd (Vint n)))) m + | Paddq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.addl rs#rd (Vlong n)))) m + | Psubl_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.sub rs#rd rs#r1))) m - | Pimul_rr rd r1 => + | Psubq_rr rd r1 => + Next (nextinstr_nf (rs#rd <- (Val.subl rs#rd rs#r1))) m + | Pimull_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd rs#r1))) m - | Pimul_ri rd n => + | Pimulq_rr rd r1 => + Next (nextinstr_nf (rs#rd <- (Val.mull rs#rd rs#r1))) m + | Pimull_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd (Vint n)))) m - | Pimul_r r1 => - Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) - #EDX <- (Val.mulhs rs#EAX rs#r1))) m - | Pmul_r r1 => - Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) - #EDX <- (Val.mulhu rs#EAX rs#r1))) m + | Pimulq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.mull rs#rd (Vlong n)))) m + | Pimull_r r1 => + Next (nextinstr_nf (rs#RAX <- (Val.mul rs#RAX rs#r1) + #RDX <- (Val.mulhs rs#RAX rs#r1))) m + | Pmull_r r1 => + Next (nextinstr_nf (rs#RAX <- (Val.mul rs#RAX rs#r1) + #RDX <- (Val.mulhu rs#RAX rs#r1))) m | Pcltd => - Next (nextinstr_nf (rs#EDX <- (Val.shr rs#EAX (Vint (Int.repr 31))))) m - | Pdiv r1 => - match rs#EDX, rs#EAX, rs#r1 with + Next (nextinstr_nf (rs#RDX <- (Val.shr rs#RAX (Vint (Int.repr 31))))) m + | Pcqto => + Next (nextinstr_nf (rs#RDX <- (Val.shrl rs#RAX (Vint (Int.repr 63))))) m + | Pdivl r1 => + match rs#RDX, rs#RAX, rs#r1 with | Vint nh, Vint nl, Vint d => match Int.divmodu2 nh nl d with - | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | Some(q, r) => Next (nextinstr_nf (rs#RAX <- (Vint q) #RDX <- (Vint r))) m | None => Stuck end | _, _, _ => Stuck end - | Pidiv r1 => - match rs#EDX, rs#EAX, rs#r1 with + | Pdivq r1 => + match rs#RDX, rs#RAX, rs#r1 with + | Vlong nh, Vlong nl, Vlong d => + match Int64.divmodu2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#RAX <- (Vlong q) #RDX <- (Vlong r))) m + | None => Stuck + end + | _, _, _ => Stuck + end + | Pidivl r1 => + match rs#RDX, rs#RAX, rs#r1 with | Vint nh, Vint nl, Vint d => match Int.divmods2 nh nl d with - | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | Some(q, r) => Next (nextinstr_nf (rs#RAX <- (Vint q) #RDX <- (Vint r))) m + | None => Stuck + end + | _, _, _ => Stuck + end + | Pidivq r1 => + match rs#RDX, rs#RAX, rs#r1 with + | Vlong nh, Vlong nl, Vlong d => + match Int64.divmods2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#RAX <- (Vlong q) #RDX <- (Vlong r))) m | None => Stuck end | _, _, _ => Stuck end - | Pand_rr rd r1 => + | Pandl_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.and rs#rd rs#r1))) m - | Pand_ri rd n => + | Pandq_rr rd r1 => + Next (nextinstr_nf (rs#rd <- (Val.andl rs#rd rs#r1))) m + | Pandl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.and rs#rd (Vint n)))) m - | Por_rr rd r1 => + | Pandq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.andl rs#rd (Vlong n)))) m + | Porl_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.or rs#rd rs#r1))) m - | Por_ri rd n => + | Porq_rr rd r1 => + Next (nextinstr_nf (rs#rd <- (Val.orl rs#rd rs#r1))) m + | Porl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.or rs#rd (Vint n)))) m - | Pxor_r rd => + | Porq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.orl rs#rd (Vlong n)))) m + | Pxorl_r rd => Next (nextinstr_nf (rs#rd <- Vzero)) m - | Pxor_rr rd r1 => + | Pxorq_r rd => + Next (nextinstr_nf (rs#rd <- (Vlong Int64.zero))) m + | Pxorl_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m - | Pxor_ri rd n => + | Pxorq_rr rd r1 => + Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd rs#r1))) m + | Pxorl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd (Vint n)))) m - | Pnot rd => + | Pxorq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd (Vlong n)))) m + | Pnotl rd => Next (nextinstr_nf (rs#rd <- (Val.notint rs#rd))) m - | Psal_rcl rd => - Next (nextinstr_nf (rs#rd <- (Val.shl rs#rd rs#ECX))) m - | Psal_ri rd n => + | Pnotq rd => + Next (nextinstr_nf (rs#rd <- (Val.notl rs#rd))) m + | Psall_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shl rs#rd rs#RCX))) m + | Psalq_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shll rs#rd rs#RCX))) m + | Psall_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.shl rs#rd (Vint n)))) m - | Pshr_rcl rd => - Next (nextinstr_nf (rs#rd <- (Val.shru rs#rd rs#ECX))) m - | Pshr_ri rd n => + | Psalq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.shll rs#rd (Vint n)))) m + | Pshrl_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shru rs#rd rs#RCX))) m + | Pshrq_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shrlu rs#rd rs#RCX))) m + | Pshrl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.shru rs#rd (Vint n)))) m - | Psar_rcl rd => - Next (nextinstr_nf (rs#rd <- (Val.shr rs#rd rs#ECX))) m - | Psar_ri rd n => + | Pshrq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.shrlu rs#rd (Vint n)))) m + | Psarl_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shr rs#rd rs#RCX))) m + | Psarq_rcl rd => + Next (nextinstr_nf (rs#rd <- (Val.shrl rs#rd rs#RCX))) m + | Psarl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.shr rs#rd (Vint n)))) m + | Psarq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.shrl rs#rd (Vint n)))) m | Pshld_ri rd r1 n => Next (nextinstr_nf (rs#rd <- (Val.or (Val.shl rs#rd (Vint n)) (Val.shru rs#r1 (Vint (Int.sub Int.iwordsize n)))))) m - | Pror_ri rd n => + | Prorl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.ror rs#rd (Vint n)))) m - | Pcmp_rr r1 r2 => + | Prorq_ri rd n => + Next (nextinstr_nf (rs#rd <- (Val.rorl rs#rd (Vint n)))) m + | Pcmpl_rr r1 r2 => Next (nextinstr (compare_ints (rs r1) (rs r2) rs m)) m - | Pcmp_ri r1 n => + | Pcmpq_rr r1 r2 => + Next (nextinstr (compare_longs (rs r1) (rs r2) rs m)) m + | Pcmpl_ri r1 n => Next (nextinstr (compare_ints (rs r1) (Vint n) rs m)) m - | Ptest_rr r1 r2 => + | Pcmpq_ri r1 n => + Next (nextinstr (compare_longs (rs r1) (Vlong n) rs m)) m + | Ptestl_rr r1 r2 => Next (nextinstr (compare_ints (Val.and (rs r1) (rs r2)) Vzero rs m)) m - | Ptest_ri r1 n => + | Ptestq_rr r1 r2 => + Next (nextinstr (compare_longs (Val.andl (rs r1) (rs r2)) (Vlong Int64.zero) rs m)) m + | Ptestl_ri r1 n => Next (nextinstr (compare_ints (Val.and (rs r1) (Vint n)) Vzero rs m)) m + | Ptestq_ri r1 n => + Next (nextinstr (compare_longs (Val.andl (rs r1) (Vlong n)) (Vlong Int64.zero) rs m)) m | Pcmov c rd r1 => match eval_testcond c rs with | Some true => Next (nextinstr (rs#rd <- (rs#r1))) m @@ -727,7 +887,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pjmp_l lbl => goto_label f lbl rs m | Pjmp_s id sg => - Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m | Pjmp_r r sg => Next (rs#PC <- (rs r)) m | Pjcc cond lbl => @@ -752,16 +912,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end | Pcall_s id sg => - Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m + Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m | Pcall_r r sg => - Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m + Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (rs r)) m | Pret => Next (rs#PC <- (rs#RA)) m (** Saving and restoring registers *) | Pmov_rm_a rd a => - exec_load Many32 m a rs rd + exec_load (if Archi.ptr64 then Many64 else Many32) m a rs rd | Pmov_mr_a a r1 => - exec_store Many32 m a rs r1 nil + exec_store (if Archi.ptr64 then Many64 else Many32) m a rs r1 nil | Pmovsd_fm_a rd a => exec_load Many64 m a rs rd | Pmovsd_mf_a a r1 => @@ -771,27 +931,27 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr rs) m | Pallocframe sz ofs_ra ofs_link => let (m1, stk) := Mem.alloc m 0 sz in - let sp := Vptr stk Int.zero in - match Mem.storev Mint32 m1 (Val.add sp (Vint ofs_link)) rs#ESP with + let sp := Vptr stk Ptrofs.zero in + match Mem.storev Mptr m1 (Val.offset_ptr sp ofs_link) rs#RSP with | None => Stuck | Some m2 => - match Mem.storev Mint32 m2 (Val.add sp (Vint ofs_ra)) rs#RA with + match Mem.storev Mptr m2 (Val.offset_ptr sp ofs_ra) rs#RA with | None => Stuck - | Some m3 => Next (nextinstr (rs #EDX <- (rs#ESP) #ESP <- sp)) m3 + | Some m3 => Next (nextinstr (rs #RAX <- (rs#RSP) #RSP <- sp)) m3 end end | Pfreeframe sz ofs_ra ofs_link => - match Mem.loadv Mint32 m (Val.add rs#ESP (Vint ofs_ra)) with + match Mem.loadv Mptr m (Val.offset_ptr rs#RSP ofs_ra) with | None => Stuck | Some ra => - match Mem.loadv Mint32 m (Val.add rs#ESP (Vint ofs_link)) with + match Mem.loadv Mptr m (Val.offset_ptr rs#RSP ofs_link) with | None => Stuck | Some sp => - match rs#ESP with + match rs#RSP with | Vptr stk ofs => match Mem.free m stk 0 sz with | None => Stuck - | Some m' => Next (nextinstr (rs#ESP <- sp #RA <- ra)) m' + | Some m' => Next (nextinstr (rs#RSP <- sp #RA <- ra)) m' end | _ => Stuck end @@ -801,14 +961,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Stuck (**r treated specially below *) (** 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 _ + | Padcl_ri _ _ + | Padcl_rr _ _ + | Paddl_mi _ _ + | Paddl_rr _ _ + | Pbsfl _ _ + | Pbsfq _ _ + | Pbsrl _ _ + | Pbsrq _ _ + | Pbswap64 _ + | Pbswap32 _ | Pbswap16 _ | Pcfi_adjust _ | Pfmadd132 _ _ _ @@ -826,15 +988,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmaxsd _ _ | Pminsd _ _ | Pmovb_rm _ _ - | Pmovq_rm _ _ - | Pmovq_mr _ _ + | Pmovsq_rm _ _ + | Pmovsq_mr _ _ | Pmovsb | Pmovsw | Pmovw_rm _ _ | Prep_movsl - | Psbb_rr _ _ + | Psbbl_rr _ _ | Psqrtsd _ _ - | Psub_ri _ _ => Stuck + | Psubl_ri _ _ + | Psubq_ri _ _ => Stuck end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -842,13 +1005,21 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Definition preg_of (r: mreg) : preg := match r with - | AX => IR EAX - | BX => IR EBX - | CX => IR ECX - | DX => IR EDX - | SI => IR ESI - | DI => IR EDI - | BP => IR EBP + | AX => IR RAX + | BX => IR RBX + | CX => IR RCX + | DX => IR RDX + | SI => IR RSI + | DI => IR RDI + | BP => IR RBP + | Machregs.R8 => IR R8 + | Machregs.R9 => IR R9 + | Machregs.R10 => IR R10 + | Machregs.R11 => IR R11 + | Machregs.R12 => IR R12 + | Machregs.R13 => IR R13 + | Machregs.R14 => IR R14 + | Machregs.R15 => IR R15 | X0 => FR XMM0 | X1 => FR XMM1 | X2 => FR XMM2 @@ -857,6 +1028,14 @@ Definition preg_of (r: mreg) : preg := | X5 => FR XMM5 | X6 => FR XMM6 | X7 => FR XMM7 + | X8 => FR XMM8 + | X9 => FR XMM9 + | X10 => FR XMM10 + | X11 => FR XMM11 + | X12 => FR XMM12 + | X13 => FR XMM13 + | X14 => FR XMM14 + | X15 => FR XMM15 | FP0 => ST0 end. @@ -870,7 +1049,7 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := | extcall_arg_stack: forall ofs ty bofs v, bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> Mem.loadv (chunk_of_type ty) m - (Val.add (rs (IR ESP)) (Vint (Int.repr bofs))) = Some v -> + (Val.offset_ptr (rs (IR RSP)) (Ptrofs.repr bofs)) = Some v -> extcall_arg rs m (S Outgoing ofs ty) v. Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := @@ -899,15 +1078,15 @@ Inductive step: state -> trace -> state -> Prop := forall b ofs f i rs m rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some i -> + find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i -> exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> - eval_builtin_args ge rs (rs ESP) m args vargs -> + find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> + eval_builtin_args ge rs (rs RSP) m args vargs -> external_call ef ge vargs m t vres m' -> rs' = nextinstr_nf (set_res res vres @@ -915,7 +1094,7 @@ Inductive step: state -> trace -> state -> Prop := step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', - rs PC = Vptr b Int.zero -> + rs PC = Vptr b Ptrofs.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> extcall_arguments rs m (ef_sig ef) args -> external_call ef ge args m t res m' -> @@ -932,15 +1111,15 @@ Inductive initial_state (p: program): state -> Prop := let ge := Genv.globalenv p in let rs0 := (Pregmap.init Vundef) - # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero) - # RA <- Vzero - # ESP <- Vzero in + # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) + # RA <- Vnullptr + # RSP <- Vnullptr in initial_state p (State rs0 m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs#PC = Vzero -> - rs#EAX = Vint r -> + rs#PC = Vnullptr -> + rs#RAX = Vint r -> final_state (State rs m) r. Definition semantics (p: program) := @@ -998,7 +1177,9 @@ Ltac Equalities := - (* initial states *) inv H; inv H0. f_equal. congruence. - (* final no step *) - inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. + assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs). + { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. } + inv H. red; intros; red; intros. inv H; rewrite H0 in *; eelim NOTNULL; eauto. - (* final states *) inv H; inv H0. congruence. Qed. -- cgit