From 51cfd8e43bc095e567f22b1768eb2743be8ffc22 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 18 Aug 2020 19:53:51 +0200 Subject: Prove exec_body_dont_move_PC Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like --- aarch64/Asmblock.v | 71 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 39 insertions(+), 32 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index be776323..8f859d55 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -21,7 +21,7 @@ WORK IN PROGRESS: we want to define an Asmblock syntax, with an Asmblock semanti (e.g. we don't need the parallel semantics of Asmvliw) -NOTE: this file is inspired from +NOTE: this file is inspired from - aarch64/Asm.v - kvx/Asmvliw.v (only the Asmblock syntax) - kvx/Asmblock.v @@ -88,22 +88,29 @@ Inductive crbit: Type := Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. +Inductive dreg : Type := + | IR': iregsp -> dreg (**r 64- or 32-bit integer registers *) + | FR': freg -> dreg. (**r double- or single-precision float registers *) + (** We model the following registers of the ARM architecture. *) Inductive preg: Type := - | IR: iregsp -> preg (**r 64- or 32-bit integer registers *) - | FR: freg -> preg (**r double- or single-precision float registers *) + | DR: dreg -> preg (** see dreg **) | CR: crbit -> preg (**r bits in the condition register *) | PC: preg. (**r program counter *) (* XXX: ireg no longer coerces to preg *) -Coercion IR: iregsp >-> preg. +Coercion IR': iregsp >-> dreg. +Coercion FR': freg >-> dreg. +Coercion DR: dreg >-> preg. Definition SP:preg := XSP. -Coercion FR: freg >-> preg. Coercion CR: crbit >-> preg. +Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}. +Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined. + Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply iregsp_eq. apply freg_eq. apply crbit_eq. Defined. +Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined. Module PregEq. Definition t := preg. @@ -113,7 +120,7 @@ End PregEq. Module Pregmap := EMap(PregEq). Definition preg_of_iregsp (r: iregsp) : preg := - match r with RR1 r => IR r | XSP => SP end. + match r with RR1 r => IR' r | XSP => SP end. (** Conventional name for return address ([RA]) *) @@ -182,7 +189,7 @@ Inductive extend_op: Type := see example of loads below. *) -(** Control Flow instructions +(** Control Flow instructions *) Inductive cf_instruction : Type := @@ -199,7 +206,7 @@ Inductive cf_instruction : Type := | 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). @@ -217,8 +224,8 @@ Coercion PCtlFlow: cf_instruction >-> control. (** Basic instructions *) -(* Loads waiting for (rd: preg) (a: addressing) - * XXX Use preg because exec_load is defined in terms of it, thus allowing us to +(* 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 *) @@ -239,7 +246,7 @@ Inductive load_rd_a: Type := . (* Actually, Pldp is not used in the aarch64/Asm semantics! - + Thus we skip this particular case: Inductive ld_instruction: Type := @@ -426,9 +433,9 @@ Inductive arith_arrrr0 : Type := * Instead, the condition register is mutated. *) Inductive ar_instruction : Type := - | PArithP (i : arith_p) (rd : preg) - | PArithPP (i : arith_pp) (rd rs : preg) - | PArithPPP (i : arith_ppp) (rd r1 r2 : preg) + | 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) @@ -436,24 +443,24 @@ Inductive ar_instruction : Type := | 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 : preg) + | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : dreg) | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg) - | PArithComparisonP (i : arith_comparison_p) (r1 : preg) + | 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 : preg) (c : testcond) (**r int/float conditional move *) + | 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) (**r TODO *) - | PLoad (ld: load_rd_a) (rd: preg) (a: addressing) (**r TODO *) - | PStore (st: store_rs_a) (r: preg) (a: addressing) (**r TODO *) + | PLoad (ld: load_rd_a) (rd: dreg) (a: addressing) (**r TODO *) + | PStore (st: store_rs_a) (r: dreg) (a: addressing) (**r TODO *) | 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] *) @@ -694,7 +701,7 @@ Definition genv := Genv.t fundef unit. or 0. *) Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val := - match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. + match r with RR0 r => rs (IR' r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. (** Concise notations for accessing and updating the values of registers. *) @@ -735,7 +742,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) end. -(** See "Parameters" of the same names in Asm.v *) +(** See "Parameters" of the same names in Asm.v *) Record aarch64_linker: Type := { symbol_low: ident -> ptrofs -> val; symbol_high: ident -> ptrofs -> val @@ -759,7 +766,7 @@ Definition Next rs m: outcome := Some (State rs m). Definition Stuck: outcome := None. Local Open Scope option_monad_scope. -(* a few lemma on comparisons of unsigned (e.g. pointers) +(* a few lemma on comparisons of unsigned (e.g. pointers) TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!) *) @@ -963,7 +970,7 @@ Definition eval_addressing (a: addressing) (rs: regset): val := (** Auxiliaries for memory accesses *) Definition exec_load (chunk: memory_chunk) (transf: val -> val) - (a: addressing) (r: preg) (rs: regset) (m: mem) := + (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. @@ -1034,12 +1041,12 @@ Definition float64_of_bits (v: val): val := | _ => Vundef end. -(** execution of loads +(** execution of loads *) Definition chunk_load_rd_a (ld: load_rd_a): memory_chunk := match ld with - | Pldrw => Mint32 + | Pldrw => Mint32 | Pldrw_a => Many32 | Pldrx => Mint64 | Pldrx_a => Many64 @@ -1094,13 +1101,13 @@ 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. + 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. + ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. Qed. @@ -1119,7 +1126,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := | _ => Stuck end. -(** Evaluating a branch +(** Evaluating a branch Warning: PC is assumed to be already pointing on the next instruction ! @@ -1879,7 +1886,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmadd _ _ _ _ _ | Pfnmsub _ _ _ _ _ | Pnop - | Pcfi_adjust _ + | Pcfi_adjust _ | Pcfi_rel_offset _ => Stuck end. @@ -1956,7 +1963,7 @@ Definition loc_external_result (sg: signature) : rpair preg := Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with | nil => Next rs m - | bi::body' => + | bi::body' => SOME o <- exec_basic bi rs m IN exec_body body' (_rs o) (_m o) end. @@ -1986,7 +1993,7 @@ Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace) Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := match lb with | nil => None - | b :: il => + | 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 -- cgit