diff options
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 1049 |
1 files changed, 1049 insertions, 0 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v new file mode 100644 index 00000000..073f1f4c --- /dev/null +++ b/aarch64/Asmblock.v @@ -0,0 +1,1049 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Justus Fasse UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + + +(* Asmblock language for aarch64 + +WORK IN PROGRESS: we want to define an Asmblock syntax, with an Asmblock semantics +(e.g. we don't need the parallel semantics of Asmvliw) + + +NOTE: this file is inspired from + - aarch64/Asm.v + - kvx/Asmvliw.v (only the Asmblock syntax) + - kvx/Asmblock.v +*) + + +(** Abstract syntax and semantics for AArch64 assembly language *) + +Require Import Coqlib Zbits Maps. +Require Import AST Integers Floats. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Locations Conventions. +Require Stacklayout. +Require Import OptionMonad Asm. +Require Import Lia. +Require Export Asm. + +Local Open Scope option_monad_scope. + +Notation regset := Asm.regset. + +(** * Abstract syntax *) + +(* First task: splitting the big [instruction] type below into CFI and basic instructions. + Actually a finer splitting in order to regroup "similar" instructions could be much better for automation of the scheduler proof! + e.g. "similar" means identical "interface" w.r.t. pseudo-registers when translated to AbstractBB, + or with a "similar" semantics. + + see example of loads below. +*) + +(** Control Flow instructions + +*) +Inductive cf_instruction : Type := + | Pb (lbl: label) (**r branch *) + | Pbc (c: testcond) (lbl: label) (**r conditional branch *) + | Pbl (id: ident) (sg: signature) (**r jump to function and link *) + | Pbs (id: ident) (sg: signature) (**r jump to function *) + | Pblr (r: ireg) (sg: signature) (**r indirect jump and link *) + | Pbr (r: ireg) (sg: signature) (**r indirect jump *) + | Pret (r: ireg) (**r return *) + | Pcbnz (sz: isize) (r: ireg) (lbl: label) (**r branch if not zero *) + | Pcbz (sz: isize) (r: ireg) (lbl: label) (**r branch if zero *) + | Ptbnz (sz: isize) (r: ireg) (n: int) (lbl: label) (**r branch if bit n is not zero *) + | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label) (**r branch if bit n is zero *) + (** Pseudo-instructions *) + | Pbtbl (r1: ireg) (tbl: list label) (**r N-way branch through a jump table *) + . + +(* +A builtin is considered as a control-flow instruction, because it could emit a trace (cf. Machblock semantics). +Here, we do not need to have builtins alone in basic-blocks (on the contrary to KVX bundles). +*) + +Inductive control: Type := + | PCtlFlow (i: cf_instruction) + (** Pseudo-instructions *) + | Pbuiltin (ef: external_function) + (args: list (builtin_arg dreg)) (res: builtin_res dreg) (**r built-in function (pseudo) *) + . + +(** Basic instructions *) + +(* Loads waiting for (rd: dreg) (a: addressing) + * XXX Use dreg because exec_load is defined in terms of it, thus allowing us to + * treat integer and floating point loads the same. *) +Inductive load_rd_a: Type := + (* Integer load *) + | Pldrw (**r load int32 *) + | Pldrw_a (**r load int32 as any32 *) + | Pldrx (**r load int64 *) + | Pldrx_a (**r load int64 as any64 *) + | Pldrb (sz: isize) (**r load int8, zero-extend *) + | Pldrsb (sz: isize) (**r load int8, sign-extend *) + | Pldrh (sz: isize) (**r load int16, zero-extend *) + | Pldrsh (sz: isize) (**r load int16, sign-extend *) + | Pldrzw (**r load int32, zero-extend to int64 *) + | Pldrsw (**r load int32, sign-extend to int64 *) + (* Floating-point load *) + | Pldrs (**r load float32 (single precision) *) + | Pldrd (**r load float64 (double precision) *) + | Pldrd_a (**r load float64 as any64 *) + . + +Inductive load_rd1_rd2_a: Type := + | Pldpw + | Pldpx + | Pldps + | Pldpd + . + +Inductive ld_instruction: Type := + | PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing) + | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: dreg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *) + . + +Inductive store_rs_a : Type := + (* Integer store *) + | Pstrw (**r store int32 *) + | Pstrw_a (**r store int32 as any32 *) + | Pstrx (**r store int64 *) + | Pstrx_a (**r store int64 as any64 *) + | Pstrb (**r store int8 *) + | Pstrh (**r store int16 *) + (* Floating-point store *) + | Pstrs (**r store float32 *) + | Pstrd (**r store float64 *) + | Pstrd_a (**r store float64 as any64 *) + . + +Inductive store_rs1_rs2_a : Type := + | Pstpw + | Pstpx + | Pstps + | Pstpd + . + +Inductive st_instruction : Type := + | PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing) + | Pstp (st: store_rs1_rs2_a) (rs1 rs2: dreg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *) + . + +Inductive arith_p : Type := + (** PC-relative addressing *) + | Padrp (id: ident) (ofs: ptrofs) (**r set [rd] to high address of [id + ofs] *) + (** Move wide immediate *) + | Pmovz (sz: isize) (n: Z) (pos: Z) (**r move [n << pos] to [rd] *) + | Pmovn (sz: isize) (n: Z) (pos: Z) (**r move [NOT(n << pos)] to [rd] *) + (** Floating-point move *) + | Pfmovimms (f: float32) (**r load float32 constant *) + | Pfmovimmd (f: float) (**r load float64 constant *) +. + +Inductive arith_comparison_p : Type := + (** Floating-point comparison *) + | Pfcmp0 (sz: fsize) (**r compare [r1] and [+0.0] *) + (** Integer arithmetic, immediate *) + | Pcmpimm (sz: isize) (n: Z) (**r compare *) + | Pcmnimm (sz: isize) (n: Z) (**r compare negative *) + (** Logical, immediate *) + | Ptstimm (sz: isize) (n: Z) (**r and, then set flags *) +. + +Inductive arith_pp : Type := + (** Move integer register *) + | Pmov + (** Move wide immediate *) + (* XXX: has to have the same register supplied both times *) + | Pmovk (sz: isize) (n: Z) (pos: Z) (**r insert 16 bits of [n] at [pos] in rd *) + (** PC-relative addressing *) + | Paddadr (id: ident) (ofs: ptrofs) (**r add the low address of [id + ofs] *) + (** Bit-field operations *) + | Psbfiz (sz: isize) (r: int) (s: Z) (**r sign extend and shift left *) + | Psbfx (sz: isize) (r: int) (s: Z) (**r shift right and sign extend *) + | Pubfiz (sz: isize) (r: int) (s: Z) (**r zero extend and shift left *) + | Pubfx (sz: isize) (r: int) (s: Z) (**r shift right and zero extend *) +(* Bit operations are not used in the aarch64/asm semantics + (** Bit operations *) + | Pcls (sz: isize) (**r count leading sign bits *) + | Pclz (sz: isize) (**r count leading zero bits *) + | Prev (sz: isize) (**r reverse bytes *) + | Prev16 (sz: isize) (**r reverse bytes in each 16-bit word *) +*) + (** Floating-point move *) + | Pfmov + (** Floating-point conversions *) + | Pfcvtds (**r convert float32 to float64 *) + | Pfcvtsd (**r convert float64 to float32 *) + (** Floating-point arithmetic *) + | Pfabs (sz: fsize) (**r absolute value *) + | Pfneg (sz: fsize) (**r negation *) + (* Pfsqrt is not used in the semantics of aarch64/asm + | Pfsqrt (sz: fsize) (**r square root *) *) + (** Floating-point conversions *) + | Pscvtf (fsz: fsize) (isz: isize) (**r convert signed int to float *) + | Pucvtf (fsz: fsize) (isz: isize) (**r convert unsigned int to float *) + | Pfcvtzs (isz: isize) (fsz: fsize) (**r convert float to signed int *) + | Pfcvtzu (isz: isize) (fsz: fsize) (**r convert float to unsigned int *) + (** Integer arithmetic, immediate *) + | Paddimm (sz: isize) (n: Z) (**r addition *) + | Psubimm (sz: isize) (n: Z) (**r subtraction *) +. + +Inductive arith_comparison_r0r : Type := + (** Integer arithmetic, shifted register *) + | Pcmp (is:isize) (s: shift_op) (**r compare *) + | Pcmn (is:isize) (s: shift_op) (**r compare negative *) + (** Logical, shifted register *) + | Ptst (is:isize) (s: shift_op) (**r and, then set flags *) +. + +Inductive arith_comparison_pp : Type := + (** Integer arithmetic, extending register *) + | Pcmpext (x: extend_op) (**r int64-int32 cmp *) + | Pcmnext (x: extend_op) (**r int64-int32 cmn *) + (** Floating-point comparison *) + | Pfcmp (sz: fsize) (**r compare [r1] and [r2] *) +. + +Inductive arith_ppp : Type := + (** Variable shifts *) + | Pasrv (sz: isize) (**r arithmetic right shift *) + | Plslv (sz: isize) (**r left shift *) + | Plsrv (sz: isize) (**r logical right shift *) + | Prorv (sz: isize) (**r rotate right *) + (** Integer multiply/divide *) + | Psmulh (**r signed multiply high *) + | Pumulh (**r unsigned multiply high *) + | Psdiv (sz: isize) (**r signed division *) + | Pudiv (sz: isize) (**r unsigned division *) + (** Integer arithmetic, extending register *) + | Paddext (x: extend_op) (**r int64-int32 add *) + | Psubext (x: extend_op) (**r int64-int32 sub *) + (** Floating-point arithmetic *) + | Pfadd (sz: fsize) (**r addition *) + | Pfdiv (sz: fsize) (**r division *) + | Pfmul (sz: fsize) (**r multiplication *) + | Pfsub (sz: fsize) (**r subtraction *) +. + +Inductive arith_rr0r : Type := + (** Integer arithmetic, shifted register *) + | Padd (sz:isize) (s: shift_op) (**r addition *) + | Psub (sz:isize) (s: shift_op) (**r subtraction *) + (** Logical, shifted register *) + | Pand (sz:isize) (s: shift_op) (**r and *) + | Pbic (sz:isize) (s: shift_op) (**r and-not *) + | Peon (sz:isize) (s: shift_op) (**r xor-not *) + | Peor (sz:isize) (s: shift_op) (**r xor *) + | Porr (sz:isize) (s: shift_op) (**r or *) + | Porn (sz:isize) (s: shift_op) (**r or-not *) +. + + +Inductive arith_rr0 : Type := + (** Logical, immediate *) + | Pandimm (sz: isize) (n: Z) (**r and *) + | Peorimm (sz: isize) (n: Z) (**r xor *) + | Porrimm (sz: isize) (n: Z) (**r or *) +. + +Inductive arith_arrrr0 : Type := + (** Integer multiply/divide *) + | Pmadd (sz: isize) (**r multiply-add *) + | Pmsub (sz: isize) (**r multiply-sub *) +. + +(* Currently not used by the semantics of aarch64/Asm + * Inductive arith_apppp : Type := + * (** Floating-point arithmetic *) + * | Pfmadd (sz: fsize) (**r [rd = r3 + r1 * r2] *) + * | Pfmsub (sz: fsize) (**r [rd = r3 - r1 * r2] *) + * . + + * Inductive arith_aapppp : Type := + * (** Floating-point arithmetic *) + * | Pfnmadd (sz: fsize) (**r [rd = - r3 - r1 * r2] *) + * | Pfnmsub (sz: fsize) (**r [rd = - r3 + r1 * r2] *) + * . *) + +(* Notes on the naming scheme used here: + * R: ireg + * R0: ireg0 + * Rsp: iregsp + * F: freg + * W/X: Occur in conjunction with R0, says whether an ireg0 should be evaluated + * as W regsiter (32 bit) or X register (64 bit) + * S/D: Used for completeness sake. Only used for copying an integer register + * to a floating point register. Could be removed. + * A: These instructions perform an additional arithmetic operation + XXX Does this interpretation match the use in kvx/Asmvliw? + * Comparison: For these instructions the first register is not the target. + * Instead, the condition register is mutated. + *) +Inductive ar_instruction : Type := + | PArithP (i : arith_p) (rd : dreg) + | PArithPP (i : arith_pp) (rd rs : dreg) + | PArithPPP (i : arith_ppp) (rd r1 r2 : dreg) + | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg) + | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0) + | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) + (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm + | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *) + (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm + | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *) + | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : dreg) + | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg) + | PArithComparisonP (i : arith_comparison_p) (r1 : dreg) + (* Instructions without indirection sine they would be the only ones *) + (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *) + | Pcset (rd : ireg) (c : testcond) (**r set to 1/0 if cond is true/false *) + (* PArithFR0 *) + | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0) (**r copy int reg to FP reg *) + (* PArithCPPP *) + | Pcsel (rd r1 r2 : dreg) (c : testcond) (**r int/float conditional move *) + (* PArithAFFF *) + | Pfnmul (fsz : fsize) (rd r1 r2 : freg) (**r multiply-negate *) +. + +Inductive basic : Type := + | PArith (i: ar_instruction) + | PLoad (ld: ld_instruction) + | PStore (st: st_instruction) + | Pallocframe (sz: Z) (linkofs: ptrofs) (**r allocate new stack frame *) + | Pfreeframe (sz: Z) (linkofs: ptrofs) (**r deallocate stack frame and restore previous frame *) + | Ploadsymbol (rd: ireg) (id: ident) (**r load the address of [id] *) + | Pcvtsw2x (rd: ireg) (r1: ireg) (**r sign-extend 32-bit int to 64-bit *) + | Pcvtuw2x (rd: ireg) (r1: ireg) (**r zero-extend 32-bit int to 64-bit *) + | Pcvtx2w (rd: ireg) (**r retype a 64-bit int as a 32-bit int *) + | Pnop (**r no operation *) +(* NOT USED IN THE SEMANTICS ! + | Pcfi_adjust (ofs: int) (**r .cfi_adjust debug directive *) + | Pcfi_rel_offset (ofs: int) (**r .cfi_rel_offset debug directive *) +*) +. + +Coercion PCtlFlow: cf_instruction >-> control. +Coercion PLoad: ld_instruction >-> basic. +Coercion PStore : st_instruction >-> basic. +Coercion PArithP: arith_p >-> Funclass. +Coercion PArithPP: arith_pp >-> Funclass. +Coercion PArithPPP: arith_ppp >-> Funclass. +Coercion PArithRR0: arith_rr0 >-> Funclass. +Coercion PArithRR0R: arith_rr0r >-> Funclass. +Coercion PArithARRRR0: arith_arrrr0 >-> Funclass. +Coercion PArithComparisonP: arith_comparison_p >-> Funclass. +Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass. +Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass. +Coercion PArith: ar_instruction >-> basic. + + +(* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml +Inductive instruction : Type := + | PBasic (i: basic) + | PControl (i: control). + +Coercion PBasic: basic >-> instruction. +Coercion PControl: control >-> instruction. *) + +(** * Definition of a bblock + +A bblock must contain at least one instruction. + +This choice simplifies the definition of [find_bblock] below: +indeed, each address of a code block identifies at most one bblock. +*) + +Definition non_empty_body (body: list basic): bool := + match body with + | nil => false + | _ => true + end. + +Definition non_empty_exit (exit: option control): bool := + match exit with + | None => false + | _ => true + end. + +Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit. + +(** A bblock is well-formed if he contains at least one instruction. *) + +Record bblock := mk_bblock { + header: list label; + body: list basic; + exit: option control; + correct: Is_true (non_empty_bblockb body exit) +}. + +(* FIXME? redundant with definition in Machblock *) +Definition length_opt {A} (o: option A) : nat := + match o with + | Some o => 1 + | None => 0 + end. + +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; cbn. assumption. +Defined. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; cbn. assumption. +Defined. + +(* This notion of size induces the notion of "valid" code address given by [find_bblock] + + The result is in Z to be compatible with operations on PC. +*) +Definition size (b:bblock): Z := Z.of_nat (length (header b) + length (body b) + length_opt (exit b)). + +Definition bblocks := list bblock. + +Fixpoint size_blocks (l: bblocks): Z := + match l with + | nil => 0 + | b :: l => + (size b) + (size_blocks l) + end + . + +Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. +Proof. + intros. destruct z; auto. + - contradict H. cbn. apply gt_irrefl. + - apply Zgt_pos_0. + - contradict H. cbn. apply gt_irrefl. +Qed. + +Lemma size_positive (b:bblock): size b > 0. +Proof. + unfold size. destruct b as [hd bdy ex cor]. cbn. + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia); + unfold non_empty_bblockb in cor; simpl in cor. + inversion cor. +Qed. + +Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }. +Definition fundef := AST.fundef function. +Definition program := AST.program fundef unit. + +(** * Operational semantics *) + +(** See "Parameters" of the same names in Asm.v *) +Record aarch64_linker: Type := { + symbol_low: ident -> ptrofs -> val; + symbol_high: ident -> ptrofs -> val +}. + +Definition genv := Genv.t fundef unit. + +Section RELSEM. + +Variable lk: aarch64_linker. +Variable ge: genv. + +(** Evaluating an addressing mode *) + +Definition eval_addressing (a: addressing) (rs: regset): val := + match a with + | ADimm base n => Val.addl rs#base (Vlong n) + | ADreg base r => Val.addl rs#base rs#r + | ADlsl base r n => Val.addl rs#base (Val.shll rs#r (Vint n)) + | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n)) + | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n)) + | ADadr base id ofs => Val.addl rs#base (symbol_low lk id ofs) + | ADpostincr base n => Vundef + end. + +(** Auxiliaries for memory accesses *) + +Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val) + (a: addressing) (r: dreg) (rs: regset) (m: mem) := + SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN + Next (rs#r <- (transf v)) m. + +Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val) + (a: addressing) (rd1 rd2: dreg) (rs: regset) (m: mem) := + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.loadv chk1 m addr with + | None => Stuck + | Some v1 => + match Mem.loadv chk2 m addr' with + | None => Stuck + | Some v2 => + Next ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m + end + end + else Stuck. + +Definition exec_store_rs_a (chunk: memory_chunk) + (a: addressing) (v: val) + (rs: regset) (m: mem) := + SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN + Next rs m'. + +Definition exec_store_double (chk1 chk2: memory_chunk) + (a: addressing) (v1 v2: val) + (rs: regset) (m: mem) := + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.storev chk1 m addr v1 with + | None => Stuck + | Some m' => match Mem.storev chk2 m' addr' v2 with + | None => Stuck + | Some m'' => Next rs m'' + end + end + else Stuck. + +(** execution of loads +*) + +Definition chunk_load (ld: load_rd_a): memory_chunk := + match ld with + | Pldrw => Mint32 + | Pldrw_a => Many32 + | Pldrx => Mint64 + | Pldrx_a => Many64 + | Pldrb _ => Mint8unsigned + | Pldrsb _ => Mint8signed + | Pldrh _ => Mint16unsigned + | Pldrsh _ => Mint16signed + | Pldrzw => Mint32 + | Pldrsw => Mint32 + | Pldrs => Mfloat32 + | Pldrd => Mfloat64 + | Pldrd_a => Many64 + end. + +Definition chunk_store (st: store_rs_a) : memory_chunk := + match st with + | Pstrw => Mint32 + | Pstrw_a => Many32 + | Pstrx => Mint64 + | Pstrx_a => Many64 + | Pstrb => Mint8unsigned + | Pstrh => Mint16unsigned + | Pstrs => Mfloat32 + | Pstrd => Mfloat64 + | Pstrd_a => Many64 + end. + +Definition interp_load (ld: load_rd_a): val -> val := + match ld with + | Pldrb X => Val.longofintu + | Pldrsb X => Val.longofint + | Pldrh X => Val.longofintu + | Pldrsh X => Val.longofint + | Pldrzw => Val.longofintu + | Pldrsw => Val.longofint + (* Changed to exhaustive list because I tend to forgot all the places I need + * to check when changing things. *) + | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W + | Pldrw | Pldrw_a | Pldrx + | Pldrx_a | Pldrs | Pldrd + | Pldrd_a => fun v => v + end. + +Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) := + match ldi with + | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ld) (interp_load ld) a rd rs m + | Pldp ld rd1 rd2 chk1 chk2 a => exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m + end. + +Definition exec_store (sti: st_instruction) (rs: regset) (m: mem) := + match sti with + | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store st) a rs#rsr rs m + | Pstp st rs1 rs2 chk1 chk2 a => exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m + end. + +(** TODO: redundant w.r.t Machblock ?? *) +Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. +Proof. + apply List.in_dec. + apply Pos.eq_dec. +Qed. + +(** Note: copy-paste from Machblock *) +Definition is_label (lbl: label) (bb: bblock) : bool := + if in_dec lbl (header bb) then true else false. + +Lemma is_label_correct_true lbl bb: + List.In lbl (header bb) <-> is_label lbl bb = true. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. +Qed. + +Lemma is_label_correct_false lbl bb: + ~(List.In lbl (header bb)) <-> is_label lbl bb = false. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. +Qed. + +(** convert a label into a position in the code *) +Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := + match lb with + | nil => None + | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' + end. + +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := + SOME pos <- label_pos lbl 0 (fn_blocks f) IN + match rs#PC with + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m + | _ => Stuck + end. + +(** Evaluating a branch + +Warning: PC is assumed to be already pointing on the next instruction ! + +*) + +Definition eval_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) := + SOME res <- ores IN + if res then goto_label f lbl rs m else Next rs m. + +Definition eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) := + SOME res <- ores IN + if res then Next rs m else goto_label f lbl rs m. + +Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) : outcome := + match cfi with + (** Branches *) + | Pb lbl => + goto_label f lbl rs m + | Pbc cond lbl => + eval_branch f lbl rs m (eval_testcond cond rs) + | Pbl id sg => + Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m + | Pbs id sg => + Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m + | Pblr r sg => + Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m + | Pbr r sg => + Next (rs#PC <- (rs#r)) m + | Pret r => + Next (rs#PC <- (rs#r)) m + | Pcbnz sz r lbl => + eval_neg_branch f lbl rs m (eval_testzero sz rs#r) + | Pcbz sz r lbl => + eval_branch f lbl rs m (eval_testzero sz rs#r) + | Ptbnz sz r n lbl => + eval_branch f lbl rs m (eval_testbit sz rs#r n) + | Ptbz sz r n lbl => + eval_neg_branch f lbl rs m (eval_testbit sz rs#r n) + (** Pseudo-instructions *) + | Pbtbl r tbl => + match (rs#X16 <- Vundef)#r with + | Vint n => + SOME lbl <- list_nth_z tbl (Int.unsigned n) IN + goto_label f lbl (rs#X16 <- Vundef) m + | _ => Stuck + end + end. + +Definition arith_eval_p (i : arith_p) : val := + match i with + | Padrp id ofs => symbol_high lk id ofs + (** Move wide immediate *) + | Pmovz W n pos => Vint (Int.repr (Z.shiftl n pos)) + | Pmovz X n pos => Vlong (Int64.repr (Z.shiftl n pos)) + | Pmovn W n pos => Vint (Int.repr (Z.lnot (Z.shiftl n pos))) + | Pmovn X n pos => Vlong (Int64.repr (Z.lnot (Z.shiftl n pos))) + (** Floating-point move *) + | Pfmovimms f => Vsingle f + | Pfmovimmd f => Vfloat f + end. + +Definition destroy_X16 (i : arith_p) : bool := + match i with + | Pfmovimms d => negb (is_immediate_float32 d) + | Pfmovimmd d => negb (is_immediate_float64 d) + | _ => false + end. + +Definition if_opt_bool_val (c: option bool) v1 v2: val := + match c with + | Some true => v1 + | Some false => v2 + | None => Vundef + end. + +Definition arith_eval_pp i v := + match i with + | Pmov => v + | Pmovk W n pos => insert_in_int v n pos 16 + | Pmovk X n pos => insert_in_long v n pos 16 + | Paddadr id ofs => Val.addl v (symbol_low lk id ofs) + | Psbfiz W r s => Val.shl (Val.sign_ext s v) (Vint r) + | Psbfiz X r s => Val.shll (Val.sign_ext_l s v) (Vint r) + | Psbfx W r s => Val.sign_ext s (Val.shr v (Vint r)) + | Psbfx X r s => Val.sign_ext_l s (Val.shrl v (Vint r)) + | Pubfiz W r s => Val.shl (Val.zero_ext s v) (Vint r) + | Pubfiz X r s => Val.shll (Val.zero_ext_l s v) (Vint r) + | Pubfx W r s => Val.zero_ext s (Val.shru v (Vint r)) + | Pubfx X r s => Val.zero_ext_l s (Val.shrlu v (Vint r)) + | Pfmov => v + | Pfcvtds => Val.floatofsingle v + | Pfcvtsd => Val.singleoffloat v + | Pfabs S => Val.absfs v + | Pfabs D => Val.absf v + | Pfneg S => Val.negfs v + | Pfneg D => Val.negf v + | Pfcvtzs W S => Val.maketotal (Val.intofsingle v) + | Pfcvtzs W D => Val.maketotal (Val.intoffloat v) + | Pfcvtzs X S => Val.maketotal (Val.longofsingle v) + | Pfcvtzs X D => Val.maketotal (Val.longoffloat v) + | Pfcvtzu W S => Val.maketotal (Val.intuofsingle v) + | Pfcvtzu W D => Val.maketotal (Val.intuoffloat v) + | Pfcvtzu X S => Val.maketotal (Val.longuofsingle v) + | Pfcvtzu X D => Val.maketotal (Val.longuoffloat v) + | Paddimm W n => Val.add v (Vint (Int.repr n)) + | Paddimm X n => Val.addl v (Vlong (Int64.repr n)) + | Psubimm W n => Val.sub v (Vint (Int.repr n)) + | Psubimm X n => Val.subl v (Vlong (Int64.repr n)) + | Pscvtf S W => Val.maketotal (Val.singleofint v) + | Pscvtf D W => Val.maketotal (Val.floatofint v) + | Pscvtf S X => Val.maketotal (Val.singleoflong v) + | Pscvtf D X => Val.maketotal (Val.floatoflong v) + | Pucvtf S W => Val.maketotal (Val.singleofintu v) + | Pucvtf D W => Val.maketotal (Val.floatofintu v) + | Pucvtf S X => Val.maketotal (Val.singleoflongu v) + | Pucvtf D X => Val.maketotal (Val.floatoflongu v) + end. + +Definition arith_eval_ppp i v1 v2 := + match i with + | Pasrv W => Val.shr v1 v2 + | Pasrv X => Val.shrl v1 v2 + | Plslv W => Val.shl v1 v2 + | Plslv X => Val.shll v1 v2 + | Plsrv W => Val.shru v1 v2 + | Plsrv X => Val.shrlu v1 v2 + | Prorv W => Val.ror v1 v2 + | Prorv X => Val.rorl v1 v2 + | Psmulh => Val.mullhs v1 v2 + | Pumulh => Val.mullhu v1 v2 + | Psdiv W => Val.maketotal (Val.divs v1 v2) + | Psdiv X => Val.maketotal (Val.divls v1 v2) + | Pudiv W => Val.maketotal (Val.divu v1 v2) + | Pudiv X => Val.maketotal (Val.divlu v1 v2) + | Paddext x => Val.addl v1 (eval_extend v2 x) + | Psubext x => Val.subl v1 (eval_extend v2 x) + | Pfadd S => Val.addfs v1 v2 + | Pfadd D => Val.addf v1 v2 + | Pfdiv S => Val.divfs v1 v2 + | Pfdiv D => Val.divf v1 v2 + | Pfmul S => Val.mulfs v1 v2 + | Pfmul D => Val.mulf v1 v2 + | Pfsub S => Val.subfs v1 v2 + | Pfsub D => Val.subf v1 v2 + end. + +Definition arith_rr0r_isize (i: arith_rr0r) := + match i with + | Padd is _ => is + | Psub is _ => is + | Pand is _ => is + | Pbic is _ => is + | Peon is _ => is + | Peor is _ => is + | Porr is _ => is + | Porn is _ => is + end. + +(* obtain v1 by [ir0 (arith_rr0r_isize i) rs s1] *) +Definition arith_eval_rr0r i v1 v2 := + match i with + | Padd W s => Val.add v1 (eval_shift_op_int v2 s) + | Padd X s => Val.addl v1 (eval_shift_op_long v2 s) + | Psub W s => Val.sub v1 (eval_shift_op_int v2 s) + | Psub X s => Val.subl v1 (eval_shift_op_long v2 s) + | Pand W s => Val.and v1 (eval_shift_op_int v2 s) + | Pand X s => Val.andl v1 (eval_shift_op_long v2 s) + | Pbic W s => Val.and v1 (Val.notint (eval_shift_op_int v2 s)) + | Pbic X s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s)) + | Peon W s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s)) + | Peon X s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s)) + | Peor W s => Val.xor v1 (eval_shift_op_int v2 s) + | Peor X s => Val.xorl v1 (eval_shift_op_long v2 s) + | Porr W s => Val.or v1 (eval_shift_op_int v2 s) + | Porr X s => Val.orl v1 (eval_shift_op_long v2 s) + | Porn W s => Val.or v1 (Val.notint (eval_shift_op_int v2 s)) + | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) + end. + +Definition arith_rr0_isize (i : arith_rr0) := + match i with + | Pandimm is _ | Peorimm is _ | Porrimm is _ => is + end. + +(* obtain v by [ir0 (arith_rr0_isize i) rs s] *) +Definition arith_eval_rr0 i v := + match i with + | Pandimm W n => Val.and v (Vint (Int.repr n)) + | Pandimm X n => Val.andl v (Vlong (Int64.repr n)) + | Peorimm W n => Val.xor v (Vint (Int.repr n)) + | Peorimm X n => Val.xorl v (Vlong (Int64.repr n)) + | Porrimm W n => Val.or v (Vint (Int.repr n)) + | Porrimm X n => Val.orl v (Vlong (Int64.repr n)) + end. + +Definition arith_arrrr0_isize (i : arith_arrrr0) := + match i with + | Pmadd is | Pmsub is => is + end. + +(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *) +Definition arith_eval_arrrr0 i v1 v2 v3 := + match i with + | Pmadd W => Val.add v3 (Val.mul v1 v2) + | Pmadd X => Val.addl v3 (Val.mull v1 v2) + | Pmsub W => Val.sub v3 (Val.mul v1 v2) + | Pmsub X => Val.subl v3 (Val.mull v1 v2) + end. + +Definition arith_prepare_comparison_pp i (v1 v2 : val) := + match i with + | Pcmpext x => (v1, (eval_extend v2 x)) + | Pcmnext x => (v1, (Val.negl (eval_extend v2 x))) + | Pfcmp _ => (v1, v2) + end. + +Definition arith_comparison_r0r_isize i := + match i with + | Pcmp is _ => is + | Pcmn is _ => is + | Ptst is _ => is + end. + +Definition arith_prepare_comparison_r0r i v1 v2 := + match i with + | Pcmp W s => (v1, (eval_shift_op_int v2 s)) + | Pcmp X s => (v1, (eval_shift_op_long v2 s)) + | Pcmn W s => (v1, (Val.neg (eval_shift_op_int v2 s))) + | Pcmn X s => (v1, (Val.negl (eval_shift_op_long v2 s))) + | Ptst W s => ((Val.and v1 (eval_shift_op_int v2 s)), (Vint Int.zero)) + | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero)) + end. + +Definition arith_prepare_comparison_p i v := + match i with + | Pcmpimm W n => (v, (Vint (Int.repr n))) + | Pcmpimm X n => (v, (Vlong (Int64.repr n))) + | Pcmnimm W n => (v, (Vint (Int.neg (Int.repr n)))) + | Pcmnimm X n => (v, (Vlong (Int64.neg (Int64.repr n)))) + | Ptstimm W n => ((Val.and v (Vint (Int.repr n))), (Vint Int.zero)) + | Ptstimm X n => ((Val.andl v (Vlong (Int64.repr n))), (Vlong Int64.zero)) + | Pfcmp0 S => (v, (Vsingle Float32.zero)) + | Pfcmp0 D => (v, (Vfloat Float.zero)) + end. + +Definition arith_comparison_pp_compare i := + match i with + | Pcmpext _ | Pcmnext _ => compare_long + | Pfcmp S => compare_single + | Pfcmp D => compare_float + end. + +Definition arith_comparison_p_compare i := + match i with + | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int + | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long + | Pfcmp0 S => compare_single + | Pfcmp0 D => compare_float + end. + +Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := + match ai with + | PArithP i d => + let rs' := rs#d <- (arith_eval_p i) in + if destroy_X16 i then rs'#X16 <- Vundef else rs' + | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s) + | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2) + + | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2) + + | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize i) rs s)) + + | PArithARRRR0 i d s1 s2 s3 => + rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3)) + + | PArithComparisonPP i s1 s2 => + let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in + arith_comparison_pp_compare i rs v1 v2 + | PArithComparisonR0R i s1 s2 => + let is := arith_comparison_r0r_isize i in + let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in + (if is (* is W *) then compare_int else compare_long) rs v1 v2 + | PArithComparisonP i s => + let (v1, v2) := arith_prepare_comparison_p i rs#s in + arith_comparison_p_compare i rs v1 v2 + | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero)) + | Pfmovi S d s => rs#d <- (float32_of_bits rs##s) + | Pfmovi D d s => rs#d <- (float64_of_bits rs###s) + | Pcsel d s1 s2 c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2)) + | Pfnmul S d s1 s2 => rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2)) + | Pfnmul D d s1 s2 => rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2)) + end. + +(* basic exec *) +Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome := + match b with + | PArith ai => Next (exec_arith_instr ai rs) m + | PLoad ldi => exec_load ldi rs m + | PStore sti => exec_store sti rs m + | Pallocframe sz pos => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + SOME m2 <- Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP IN + Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2 + | Pfreeframe sz pos => + SOME v <- Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) IN + match rs#SP with + | Vptr stk ofs => + SOME m' <- Mem.free m stk 0 sz IN + Next (rs#SP <- v #X16 <- Vundef) m' + | _ => Stuck + end + | Ploadsymbol rd id => + Next (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero)) m + | Pcvtsw2x rd r1 => + Next (rs#rd <- (Val.longofint rs#r1)) m + | Pcvtuw2x rd r1 => + Next (rs#rd <- (Val.longofintu rs#r1)) m + | Pcvtx2w rd => + Next (rs#rd <- (Val.loword rs#rd)) m + | Pnop => Next rs m + end. + +(** execution of the body of a bblock *) +Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := + match body with + | nil => Next rs m + | bi::body' => + SOME o <- exec_basic bi rs m IN + exec_body body' (_rs o) (_m o) + end. + +Definition incrPC size_b (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC size_b). + +Definition estep (f: function) oc size_b (rs: regset) (m: mem) := + match oc with + | Some (PCtlFlow cfi) => exec_cfi f cfi (incrPC size_b rs) m + | Some (Pbuiltin ef args res) => Next (incrPC size_b rs) m + | None => Next (incrPC size_b rs) m + end. + +(** execution of the exit instruction of a bblock *) +Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) -> trace -> regset -> mem -> Prop := + | none_step: + exec_exit f size_b rs m None E0 (incrPC size_b rs) m + | cfi_step (cfi: cf_instruction) rs' m': + exec_cfi f cfi (incrPC size_b rs) m = Next rs' m' -> + exec_exit f size_b rs m (Some (PCtlFlow cfi)) E0 rs' m' + | builtin_step ef args res vargs t vres rs' m': + eval_builtin_args ge (fun (r: dreg) => rs r) rs#SP m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = incrPC size_b + (set_res (map_builtin_res DR res) vres + (undef_regs (DR (IR X16) :: DR (IR X30) :: map preg_of (destroyed_by_builtin ef)) rs)) -> + exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m' + . + +(*Definition bbstep f cfi size_b bdy rs m :=*) + (*match exec_body bdy rs m with*) + (*| Some (State rs' m') => estep f cfi size_b rs' m'*) + (*| Stuck => Stuck*) + (*end.*) + +Definition bbstep f bb rs m := + match exec_body (body bb) rs m with + | Some (State rs' m') => estep f (exit bb) (Ptrofs.repr (size bb)) rs' m' + | Stuck => Stuck + end. + +Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace) (rs':regset) (m':mem): Prop + := exists rs1 m1, exec_body (body b) rs m = Next rs1 m1 /\ exec_exit f (Ptrofs.repr (size b)) rs1 m1 (exit b) t rs' m'. + +Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := + match lb with + | nil => None + | b :: il => + if zlt pos 0 then None (* NOTE: It is impossible to branch inside a block *) + else if zeq pos 0 then Some b + else find_bblock (pos - (size b)) il + end. + +(** Execution of the instruction at [rs PC]. *) + +Inductive step: state -> trace -> state -> Prop := + | exec_step_internal: + forall b ofs f bi rs m t rs' m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi -> + exec_bblock f bi rs m t rs' m' -> + 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) -> + external_call ef ge args m t res m' -> + extcall_arguments rs m (ef_sig ef) args -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs 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 + # SP <- 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#X0 = Vint r -> + final_state (State rs m) r. + +Definition semantics (lk: aarch64_linker) (p: program) := + Semantics (step lk) (initial_state p) final_state (Genv.globalenv p). |