diff options
Diffstat (limited to 'ia32/Asm.v')
| -rw-r--r-- | ia32/Asm.v | 1204 |
1 files changed, 0 insertions, 1204 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v deleted file mode 100644 index 304cb8e4..00000000 --- a/ia32/Asm.v +++ /dev/null @@ -1,1204 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Abstract syntax and semantics for IA32 assembly language *) - -Require Import Coqlib Maps. -Require Import AST Integers Floats Values Memory Events Globalenvs Smallstep. -Require Import Locations Stacklayout Conventions. - -(** * Abstract syntax *) - -(** ** Registers. *) - -(** Integer registers. *) - -Inductive ireg: Type := - | 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 | 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. - -Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. -Proof. decide equality. Defined. - -(** Bits of the flags register. *) - -Inductive crbit: Type := - | ZF | CF | PF | SF | OF. - -(** All registers modeled here. *) - -Inductive preg: Type := - | PC: preg (**r program counter *) - | IR: ireg -> preg (**r integer register *) - | FR: freg -> preg (**r XMM register *) - | ST0: preg (**r top of FP stack *) - | CR: crbit -> preg (**r bit of the flags register *) - | RA: preg. (**r pseudo-reg representing return address *) - -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. -Coercion CR: crbit >-> preg. - -(** Conventional names for stack pointer ([SP]) and return address ([RA]) *) - -Notation SP := RSP (only parsing). - -(** ** Instruction set. *) - -Definition label := positive. - -(** General form of an addressing mode. *) - -Inductive addrmode: Type := - | Addrmode (base: option ireg) - (ofs: option (ireg * Z)) - (const: Z + ident * ptrofs). - -(** Testable conditions (for conditional jumps and more). *) - -Inductive testcond: Type := - | Cond_e | Cond_ne - | Cond_b | Cond_be | Cond_ae | Cond_a - | Cond_l | Cond_le | Cond_ge | Cond_g - | Cond_p | Cond_np. - -(** Instructions. IA32 instructions accept many combinations of - registers, memory references and immediate constants as arguments. - Here, we list only the combinations that we actually use. - - 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 -- [i]: immediate integer operand -- [s]: immediate symbol operand -- [l]: immediate label operand -- [cl]: the [CL] register - - For two-operand instructions, the first suffix describes the result - (and first argument), the second suffix describes the second argument. -*) - -Inductive instruction: Type := - (** Moves *) - | 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) - | Pmovsd_mf (a: addrmode) (r1: freg) - | Pmovss_fi (rd: freg) (n: float32) (**r [movss] (single 32-bit float) *) - | Pmovss_fm (rd: freg) (a: addrmode) - | Pmovss_mf (a: addrmode) (r1: freg) - | Pfldl_m (a: addrmode) (**r [fld] double precision *) - | Pfstpl_m (a: addrmode) (**r [fstp] double precision *) - | Pflds_m (a: addrmode) (**r [fld] simple precision *) - | Pfstps_m (a: addrmode) (**r [fstp] simple precision *) - (** 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_rm (rd: ireg) (a: addrmode) - | 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_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 *) - | 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 - | 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) - | 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 *) - | Paddd_ff (rd: freg) (r1: freg) - | Psubd_ff (rd: freg) (r1: freg) - | Pmuld_ff (rd: freg) (r1: freg) - | Pdivd_ff (rd: freg) (r1: freg) - | Pnegd (rd: freg) - | Pabsd (rd: freg) - | Pcomisd_ff (r1 r2: freg) - | Pxorpd_f (rd: freg) (**r [xor] with self = set to zero *) - | Padds_ff (rd: freg) (r1: freg) - | Psubs_ff (rd: freg) (r1: freg) - | Pmuls_ff (rd: freg) (r1: freg) - | Pdivs_ff (rd: freg) (r1: freg) - | Pnegs (rd: freg) - | Pabss (rd: freg) - | Pcomiss_ff (r1 r2: freg) - | Pxorps_f (rd: freg) (**r [xor] with self = set to zero *) - (** Branches and calls *) - | Pjmp_l (l: label) - | Pjmp_s (symb: ident) (sg: signature) - | Pjmp_r (r: ireg) (sg: signature) - | Pjcc (c: testcond)(l: label) - | Pjcc2 (c1 c2: testcond)(l: label) (**r pseudo *) - | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *) - | Pcall_s (symb: ident) (sg: signature) - | Pcall_r (r: ireg) (sg: signature) - | Pret - (** Saving and restoring registers *) - | 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: 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] -- 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) - | 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) - | Pmovsq_mr (a: addrmode) (rs: freg) - | Pmovsq_rm (rd: freg) (a: addrmode) - | Pmovsb - | Pmovsw - | Pmovw_rm (rd: ireg) (ad: addrmode) - | Prep_movsl - | Psbbl_rr (rd: ireg) (r2: ireg) - | Psqrtsd (rd: freg) (r1: freg) - | 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 }. -Definition fundef := AST.fundef function. -Definition program := AST.program fundef unit. - -(** * Operational semantics *) - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. decide equality. Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - -Definition regset := Pregmap.t val. -Definition genv := Genv.t fundef unit. - -Notation "a # b" := (a b) (at level 1, only parsing). -Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level). - -(** Undefining some registers *) - -Fixpoint undef_regs (l: list preg) (rs: regset) : regset := - match l with - | nil => rs - | r :: l' => undef_regs l' (rs#r <- Vundef) - end. - -(** Assigning a register pair *) - -Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := - match p with - | One r => rs#r <- v - | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) - end. - -(** Assigning the result of a builtin *) - -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := - match res with - | BR r => rs#r <- v - | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) - end. - -Section RELSEM. - -(** Looking up instructions in a code sequence by position. *) - -Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction := - match c with - | nil => None - | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il - end. - -(** Position corresponding to a label *) - -Definition is_label (lbl: label) (instr: instruction) : bool := - match instr with - | Plabel lbl' => if peq lbl lbl' then true else false - | _ => false - end. - -Lemma is_label_correct: - forall lbl instr, - if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl. -Proof. - intros. destruct instr; simpl; try discriminate. - case (peq lbl l); intro; congruence. -Qed. - -Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := - match c with - | nil => None - | instr :: c' => - if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c' - end. - -Variable ge: genv. - -(** Evaluating an addressing mode *) - -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) - (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 *) - -(** Integer comparison between x and y: -- ZF = 1 if x = y, 0 if x != y -- CF = 1 if x <u y, 0 if x >=u y -- SF = 1 if x - y is negative, 0 if x - y is positive -- OF = 1 if x - y overflows (signed), 0 if not -- PF is undefined -*) - -Definition compare_ints (x y: val) (rs: regset) (m: mem): regset := - rs #ZF <- (Val.cmpu (Mem.valid_pointer m) Ceq x y) - #CF <- (Val.cmpu (Mem.valid_pointer m) Clt x y) - #SF <- (Val.negative (Val.sub x y)) - #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 or unordered, 0 if x>=y -- PF = 1 if unordered, 0 if ordered. -- SF and 0F are undefined -*) - -Definition compare_floats (vx vy: val) (rs: regset) : regset := - match vx, vy with - | Vfloat x, Vfloat y => - rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y))) - #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y))) - #SF <- Vundef - #OF <- Vundef - | _, _ => - undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs - end. - -Definition compare_floats32 (vx vy: val) (rs: regset) : regset := - match vx, vy with - | Vsingle x, Vsingle y => - rs #ZF <- (Val.of_bool (negb (Float32.cmp Cne x y))) - #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float32.cmp Ceq x y || Float32.cmp Clt x y || Float32.cmp Cgt x y))) - #SF <- Vundef - #OF <- Vundef - | _, _ => - undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs - end. - -(** Testing a condition *) - -Definition eval_testcond (c: testcond) (rs: regset) : option bool := - match c with - | Cond_e => - match rs ZF with - | Vint n => Some (Int.eq n Int.one) - | _ => None - end - | Cond_ne => - match rs ZF with - | Vint n => Some (Int.eq n Int.zero) - | _ => None - end - | Cond_b => - match rs CF with - | Vint n => Some (Int.eq n Int.one) - | _ => None - end - | Cond_be => - match rs CF, rs ZF with - | Vint c, Vint z => Some (Int.eq c Int.one || Int.eq z Int.one) - | _, _ => None - end - | Cond_ae => - match rs CF with - | Vint n => Some (Int.eq n Int.zero) - | _ => None - end - | Cond_a => - match rs CF, rs ZF with - | Vint c, Vint z => Some (Int.eq c Int.zero && Int.eq z Int.zero) - | _, _ => None - end - | Cond_l => - match rs OF, rs SF with - | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) - | _, _ => None - end - | Cond_le => - match rs OF, rs SF, rs ZF with - | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) - | _, _, _ => None - end - | Cond_ge => - match rs OF, rs SF with - | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) - | _, _ => None - end - | Cond_g => - match rs OF, rs SF, rs ZF with - | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) - | _, _, _ => None - end - | Cond_p => - match rs PF with - | Vint n => Some (Int.eq n Int.one) - | _ => None - end - | Cond_np => - match rs PF with - | Vint n => Some (Int.eq n Int.zero) - | _ => None - end - end. - -(** The semantics is purely small-step and defined as a function - from the current state (a register set + a memory state) - to either [Next rs' m'] where [rs'] and [m'] are the updated register - set and memory state after execution of the instruction at [rs#PC], - or [Stuck] if the processor is stuck. *) - -Inductive outcome: Type := - | Next: regset -> mem -> outcome - | Stuck: outcome. - -(** Manipulations over the [PC] register: continuing with the next - instruction ([nextinstr]) or branching to a label ([goto_label]). - [nextinstr_nf] is a variant of [nextinstr] that sets condition flags - to [Vundef] in addition to incrementing the [PC]. *) - -Definition nextinstr (rs: regset) := - 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). - -Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := - match label_pos lbl 0 (fn_code f) with - | None => Stuck - | Some pos => - match rs#PC with - | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m - | _ => Stuck - end - end. - -(** Auxiliaries for memory accesses. *) - -Definition exec_load (chunk: memory_chunk) (m: mem) - (a: addrmode) (rs: regset) (rd: preg) := - match Mem.loadv chunk m (eval_addrmode a rs) with - | Some v => Next (nextinstr_nf (rs#rd <- v)) m - | None => Stuck - end. - -Definition exec_store (chunk: memory_chunk) (m: mem) - (a: addrmode) (rs: regset) (r1: preg) - (destroyed: list preg) := - match Mem.storev chunk m (eval_addrmode a rs) (rs r1) with - | Some m' => Next (nextinstr_nf (undef_regs destroyed rs)) m' - | None => Stuck - end. - -(** Execution of a single instruction [i] in initial state - [rs] and [m]. Return updated state. For instructions - that correspond to actual IA32 instructions, the cases are - straightforward transliterations of the informal descriptions - given in the IA32 reference manuals. For pseudo-instructions, - refer to the informal descriptions given above. - - Note that we set to [Vundef] the registers used as temporaries by - the expansions of the pseudo-instructions, so that the IA32 code - we generate cannot use those registers to hold values that must - survive the execution of the pseudo-instruction. - - Concerning condition flags, the comparison instructions set them - accurately; other instructions (moves, [lea]) preserve them; - and all other instruction set those flags to [Vundef], to reflect - the fact that the processor updates some or all of those flags, - but we do not need to model this precisely. -*) - -Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := - match i with - (** Moves *) - | Pmov_rr rd r1 => - Next (nextinstr (rs#rd <- (rs r1))) m - | Pmovl_ri rd n => - Next (nextinstr_nf (rs#rd <- (Vint n))) m - | 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 - | 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 => - Next (nextinstr (rs#rd <- (Vfloat n))) m - | Pmovsd_fm rd a => - exec_load Mfloat64 m a rs rd - | Pmovsd_mf a r1 => - exec_store Mfloat64 m a rs r1 nil - | Pmovss_fi rd n => - Next (nextinstr (rs#rd <- (Vsingle n))) m - | Pmovss_fm rd a => - exec_load Mfloat32 m a rs rd - | Pmovss_mf a r1 => - exec_store Mfloat32 m a rs r1 nil - | Pfldl_m a => - exec_load Mfloat64 m a rs ST0 - | Pfstpl_m a => - exec_store Mfloat64 m a rs ST0 (ST0 :: nil) - | Pflds_m a => - exec_load Mfloat32 m a rs ST0 - | Pfstps_m a => - exec_store Mfloat32 m a rs ST0 (ST0 :: nil) - (** Moves with conversion *) - | Pmovb_mr a r1 => - exec_store Mint8unsigned m a rs r1 nil - | Pmovw_mr a r1 => - exec_store Mint16unsigned m a rs r1 nil - | Pmovzb_rr rd r1 => - Next (nextinstr (rs#rd <- (Val.zero_ext 8 rs#r1))) m - | Pmovzb_rm rd a => - exec_load Mint8unsigned m a rs rd - | Pmovsb_rr rd r1 => - Next (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m - | Pmovsb_rm rd a => - exec_load Mint8signed m a rs rd - | Pmovzw_rr rd r1 => - Next (nextinstr (rs#rd <- (Val.zero_ext 16 rs#r1))) m - | Pmovzw_rm rd a => - exec_load Mint16unsigned m a rs rd - | Pmovsw_rr rd r1 => - 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 => - Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m - | Pcvttsd2si_rf rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m - | Pcvtsi2sd_fr rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m - | Pcvttss2si_rf rd r1 => - 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 *) - | 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 - | 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 - | 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 - | 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 - | 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 - | Pimulq_r r1 => - Next (nextinstr_nf (rs#RAX <- (Val.mull rs#RAX rs#r1) - #RDX <- (Val.mullhs 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 - | Pmulq_r r1 => - Next (nextinstr_nf (rs#RAX <- (Val.mull rs#RAX rs#r1) - #RDX <- (Val.mullhu rs#RAX rs#r1))) m - | Pcltd => - 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#RAX <- (Vint q) #RDX <- (Vint r))) m - | None => Stuck - end - | _, _, _ => Stuck - end - | 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#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 - | Pandl_rr rd r1 => - Next (nextinstr_nf (rs#rd <- (Val.and rs#rd rs#r1))) m - | 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 - | 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 - | 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 - | 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 - | 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 - | 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 - | 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 - | 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 - | 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 - | 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 - | Prorl_ri rd n => - Next (nextinstr_nf (rs#rd <- (Val.ror rs#rd (Vint n)))) m - | 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 - | 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 - | 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 - | 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 - | Some false => Next (nextinstr rs) m - | None => Next (nextinstr (rs#rd <- Vundef)) m - end - | Psetcc c rd => - Next (nextinstr (rs#rd <- (Val.of_optbool (eval_testcond c rs)))) m - (** Arithmetic operations over double-precision floats *) - | Paddd_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.addf rs#rd rs#r1))) m - | Psubd_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.subf rs#rd rs#r1))) m - | Pmuld_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.mulf rs#rd rs#r1))) m - | Pdivd_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.divf rs#rd rs#r1))) m - | Pnegd rd => - Next (nextinstr (rs#rd <- (Val.negf rs#rd))) m - | Pabsd rd => - Next (nextinstr (rs#rd <- (Val.absf rs#rd))) m - | Pcomisd_ff r1 r2 => - Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m - | Pxorpd_f rd => - Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m - (** Arithmetic operations over single-precision floats *) - | Padds_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.addfs rs#rd rs#r1))) m - | Psubs_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.subfs rs#rd rs#r1))) m - | Pmuls_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.mulfs rs#rd rs#r1))) m - | Pdivs_ff rd r1 => - Next (nextinstr (rs#rd <- (Val.divfs rs#rd rs#r1))) m - | Pnegs rd => - Next (nextinstr (rs#rd <- (Val.negfs rs#rd))) m - | Pabss rd => - Next (nextinstr (rs#rd <- (Val.absfs rs#rd))) m - | Pcomiss_ff r1 r2 => - Next (nextinstr (compare_floats32 (rs r1) (rs r2) rs)) m - | Pxorps_f rd => - Next (nextinstr_nf (rs#rd <- (Vsingle Float32.zero))) m - (** Branches and calls *) - | Pjmp_l lbl => - goto_label f lbl rs m - | Pjmp_s id sg => - Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m - | Pjmp_r r sg => - Next (rs#PC <- (rs r)) m - | Pjcc cond lbl => - match eval_testcond cond rs with - | Some true => goto_label f lbl rs m - | Some false => Next (nextinstr rs) m - | None => Stuck - end - | Pjcc2 cond1 cond2 lbl => - match eval_testcond cond1 rs, eval_testcond cond2 rs with - | Some true, Some true => goto_label f lbl rs m - | Some _, Some _ => Next (nextinstr rs) m - | _, _ => Stuck - end - | Pjmptbl r tbl => - match rs#r with - | Vint n => - match list_nth_z tbl (Int.unsigned n) with - | None => Stuck - | Some lbl => goto_label f lbl (rs #RAX <- Vundef #RDX <- Vundef) m - end - | _ => Stuck - end - | Pcall_s id sg => - 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.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 (if Archi.ptr64 then Many64 else Many32) m a rs rd - | Pmov_mr_a a r1 => - 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 => - exec_store Many64 m a rs r1 nil - (** Pseudo-instructions *) - | Plabel lbl => - Next (nextinstr rs) m - | Pallocframe sz ofs_ra ofs_link => - let (m1, stk) := Mem.alloc m 0 sz in - 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 Mptr m2 (Val.offset_ptr sp ofs_ra) rs#RA with - | None => Stuck - | Some m3 => Next (nextinstr (rs #RAX <- (rs#RSP) #RSP <- sp)) m3 - end - end - | Pfreeframe sz ofs_ra ofs_link => - match Mem.loadv Mptr m (Val.offset_ptr rs#RSP ofs_ra) with - | None => Stuck - | Some ra => - match Mem.loadv Mptr m (Val.offset_ptr rs#RSP ofs_link) with - | None => Stuck - | Some sp => - match rs#RSP with - | Vptr stk ofs => - match Mem.free m stk 0 sz with - | None => Stuck - | Some m' => Next (nextinstr (rs#RSP <- sp #RA <- ra)) m' - end - | _ => Stuck - end - end - 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_ri _ _ - | Padcl_rr _ _ - | Paddl_mi _ _ - | Paddl_rr _ _ - | Pbsfl _ _ - | Pbsfq _ _ - | Pbsrl _ _ - | Pbsrq _ _ - | Pbswap64 _ - | Pbswap32 _ - | Pbswap16 _ - | Pcfi_adjust _ - | Pfmadd132 _ _ _ - | Pfmadd213 _ _ _ - | Pfmadd231 _ _ _ - | Pfmsub132 _ _ _ - | Pfmsub213 _ _ _ - | Pfmsub231 _ _ _ - | Pfnmadd132 _ _ _ - | Pfnmadd213 _ _ _ - | Pfnmadd231 _ _ _ - | Pfnmsub132 _ _ _ - | Pfnmsub213 _ _ _ - | Pfnmsub231 _ _ _ - | Pmaxsd _ _ - | Pminsd _ _ - | Pmovb_rm _ _ - | Pmovsq_rm _ _ - | Pmovsq_mr _ _ - | Pmovsb - | Pmovsw - | Pmovw_rm _ _ - | Prep_movsl - | Psbbl_rr _ _ - | Psqrtsd _ _ - | Psubl_ri _ _ - | Psubq_ri _ _ => Stuck - end. - -(** Translation of the LTL/Linear/Mach view of machine registers - to the Asm view. *) - -Definition preg_of (r: mreg) : preg := - match r with - | 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 - | X3 => FR XMM3 - | X4 => FR XMM4 - | 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. - -(** Extract the values of the arguments of an external call. - We exploit the calling conventions from module [Conventions], except that - we use machine registers instead of locations. *) - -Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := - | extcall_arg_reg: forall r, - extcall_arg rs m (R r) (rs (preg_of r)) - | extcall_arg_stack: forall ofs ty bofs v, - bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> - Mem.loadv (chunk_of_type ty) m - (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 := - | extcall_arg_one: forall l v, - extcall_arg rs m l v -> - extcall_arg_pair rs m (One l) v - | extcall_arg_twolong: forall hi lo vhi vlo, - extcall_arg rs m hi vhi -> - extcall_arg rs m lo vlo -> - extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). - -Definition extcall_arguments - (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. - -Definition loc_external_result (sg: signature) : rpair preg := - map_rpair preg_of (loc_result sg). - -(** Execution of the instruction at [rs#PC]. *) - -Inductive state: Type := - | State: regset -> mem -> state. - -Inductive step: state -> trace -> state -> Prop := - | exec_step_internal: - 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 (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 (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 - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> - 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 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' -> - rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) -> - step (State rs m) t (State rs' m'). - -End RELSEM. - -(** Execution of whole programs. *) - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall m0, - Genv.init_mem p = Some m0 -> - let ge := Genv.globalenv p in - let rs0 := - (Pregmap.init Vundef) - # 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 = Vnullptr -> - rs#RAX = Vint r -> - final_state (State rs m) r. - -Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). - -(** Determinacy of the [Asm] semantics. *) - -Remark extcall_arguments_determ: - forall rs m sg args1 args2, - extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. -Proof. - intros until m. - assert (A: forall l v1 v2, - extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2). - { intros. inv H; inv H0; congruence. } - assert (B: forall p v1 v2, - extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). - { intros. inv H; inv H0. - eapply A; eauto. - f_equal; eapply A; eauto. } - assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> - forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2). - { - induction 1; intros vl2 EA; inv EA. - auto. - f_equal; eauto. } - intros. eapply C; eauto. -Qed. - -Lemma semantics_determinate: forall p, determinate (semantics p). -Proof. -Ltac Equalities := - match goal with - | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => - rewrite H1 in H2; inv H2; Equalities - | _ => idtac - end. - intros; constructor; simpl; intros. -- (* determ *) - inv H; inv H0; Equalities. -+ split. constructor. auto. -+ discriminate. -+ discriminate. -+ assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H11. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. -+ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. - exploit external_call_determ. eexact H4. eexact H9. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. -- (* trace length *) - red; intros; inv H; simpl. - omega. - eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. -- (* initial states *) - inv H; inv H0. f_equal. congruence. -- (* final no step *) - 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. - -(** Classification functions for processor registers (used in Asmgenproof). *) - -Definition data_preg (r: preg) : bool := - match r with - | PC => false - | IR _ => true - | FR _ => true - | ST0 => true - | CR _ => false - | RA => false - end. - |