diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-13 12:10:46 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-13 12:10:46 +0100 |
commit | 4aa289a5066ebe3081f66c9c0a02fd873720c8ad (patch) | |
tree | 84df1486390f201a81acdf473a6ff99a5c586f9e | |
parent | df8f93225869980a0fff3df6659aca836952b720 (diff) | |
download | compcert-kvx-4aa289a5066ebe3081f66c9c0a02fd873720c8ad.tar.gz compcert-kvx-4aa289a5066ebe3081f66c9c0a02fd873720c8ad.zip |
Loads and stores op
-rw-r--r-- | aarch64/Asmblockdeps.v | 208 | ||||
-rw-r--r-- | aarch64/PostpassSchedulingOracle.ml | 61 |
2 files changed, 238 insertions, 31 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 88cca121..31ce8065 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -109,12 +109,28 @@ Inductive arith_op := | Ofnmul (fsz: fsize) . +Inductive store_op := + | Ostore1 (st: store_rs_a) (a: addressing) + | Ostore2 (st: store_rs_a) (a: addressing) + | OstoreU (st: store_rs_a) (a: addressing) +. + +Inductive load_op := + | Oload1 (ld: load_rd_a) (a: addressing) + | Oload2 (ld: load_rd_a) (a: addressing) + | OloadU (ld: load_rd_a) (a: addressing) +. + Inductive op_wrap := (* arithmetic operation *) | Arith (op: arith_op) + | Load (ld: load_op) + | Store (st: store_op) | Control (co: control_op) . +Definition op:=op_wrap. + Coercion Arith: arith_op >-> op_wrap. Definition v_compare_int (v1 v2: val) : CRflags := @@ -267,8 +283,6 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) := | D => Val.negf (Val.mulf v1 v2) end. -Definition op:=op_wrap. - Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is_set: bool) := match c, l with | TCeq, [Val vCZ] => Some (Val (csetsel_eval TCeq v1 v2 Vundef vCZ Vundef Vundef is_set)) @@ -321,6 +335,38 @@ Definition arith_op_eval (op: arith_op) (l: list value) := | _, _ => None end. +Definition call_ll_storev (n: store_rs_a) (m: mem) (v: option val) (vs: val) := + match v with + | Some va => match Mem.storev (chunk_store_rs_a n) m va vs with + | Some m' => Some (Memstate m') + | None => None + end + | None => None (* should never occurs *) + end. + +Definition exec_store1 (n: store_rs_a) (m: mem) (a: addressing) (vr vs: val) := + let v := + match a with + | ADimm _ n => Some (Val.addl vs (Vlong n)) + | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs)) + | _ => None + end in + call_ll_storev n m v vr. + +Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val) := + let v := + match a with + | ADreg _ _ => Some (Val.addl vs1 vs2) + | ADlsl _ _ n => Some (Val.addl vs1 (Val.shll vs2 (Vint n))) + | ADsxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofint vs2) (Vint n))) + | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n))) + | _ => None + end in + call_ll_storev n m v vr. + +Definition exec_storeU (n: store_rs_a) (m: mem) (a: addressing) (vr: val) := + call_ll_storev n m None vr. + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None @@ -339,11 +385,60 @@ Definition control_eval (o: control_op) (l: list value) := | _, _ => None end. +Definition store_eval (o: store_op) (l: list value) := + match o, l with + | Ostore1 st a, [Val vr; Val vs; Memstate m] => exec_store1 st m a vr vs + | Ostore2 st a, [Val vr; Val vs1; Val vs2; Memstate m] => exec_store2 st m a vr vs1 vs2 + | OstoreU st a, [Val vr; Memstate m] => exec_storeU st m a vr + | _, _ => None + end. + +Definition call_ll_loadv (n: load_rd_a) (m: mem) (v: option val) := + match v with + | Some va => match Mem.loadv (chunk_load_rd_a n) m va with + | Some v' => Some (Val ((interp_load_rd_a n) v')) + | None => None + end + | None => None (* should never occurs *) + end. + +Definition exec_load1 (n: load_rd_a) (m: mem) (a: addressing) (vl: val) := + let v := + match a with + | ADimm _ n => Some (Val.addl vl (Vlong n)) + | ADadr _ id ofs => Some (Val.addl vl (symbol_low Ge.(_lk) id ofs)) + | _ => None + end in + call_ll_loadv n m v. + +Definition exec_load2 (n: load_rd_a) (m: mem) (a: addressing) (vl1 vl2: val) := + let v := + match a with + | ADreg _ _ => Some (Val.addl vl1 vl2) + | ADlsl _ _ n => Some (Val.addl vl1 (Val.shll vl2 (Vint n))) + | ADsxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofint vl2) (Vint n))) + | ADuxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofintu vl2) (Vint n))) + | _ => None + end in + call_ll_loadv n m v. + +Definition exec_loadU (n: load_rd_a) (m: mem) (a: addressing) := + call_ll_loadv n m None. + +Definition load_eval (o: load_op) (l: list value) := + match o, l with + | Oload1 st a, [Val vs; Memstate m] => exec_load1 st m a vs + | Oload2 st a, [Val vs1; Val vs2; Memstate m] => exec_load2 st m a vs1 vs2 + | OloadU st a, [Memstate m] => exec_loadU st m a + | _, _ => None + end. + Definition op_eval (op: op) (l:list value) := match op, l with | Arith op, l => arith_op_eval op l + | Load o, l => load_eval o l + | Store o, l => store_eval o l | Control o, l => control_eval o l - (*| _, _ => None*) end. Definition vz_eq (vz1 vz2: val) : ?? bool := @@ -552,12 +647,54 @@ Qed. Hint Resolve control_op_eq_correct: wlp. Opaque control_op_eq_correct. +Definition store_op_eq (s1 s2: store_op): ?? bool := + match s1 with + | Ostore1 st1 a1 => + match s2 with Ostore1 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + | Ostore2 st1 a1 => + match s2 with Ostore2 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + | OstoreU st1 a1 => + match s2 with OstoreU st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end + end. + +Lemma store_op_eq_correct s1 s2: + WHEN store_op_eq s1 s2 ~> b THEN b = true -> s1 = s2. +Proof. + destruct s1, s2; wlp_simplify; try congruence. + all: rewrite H0 in H; rewrite H; reflexivity. +Qed. +Hint Resolve store_op_eq_correct: wlp. +Opaque store_op_eq_correct. + +Definition load_op_eq (l1 l2: load_op): ?? bool := + match l1 with + | Oload1 ld1 a1 => + match l2 with Oload1 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + | Oload2 ld1 a1 => + match l2 with Oload2 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + | OloadU ld1 a1 => + match l2 with OloadU ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end + end. + +Lemma load_op_eq_correct l1 l2: + WHEN load_op_eq l1 l2 ~> b THEN b = true -> l1 = l2. +Proof. + destruct l1, l2; wlp_simplify; try congruence. + all: rewrite H0 in H; rewrite H; reflexivity. +Qed. +Hint Resolve load_op_eq_correct: wlp. +Opaque load_op_eq_correct. + Definition op_eq (o1 o2: op): ?? bool := match o1 with | Arith i1 => match o2 with Arith i2 => arith_op_eq i1 i2 | _ => RET false end | Control i1 => match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end + | Load i1 => + match o2 with Load i2 => load_op_eq i1 i2 | _ => RET false end + | Store i1 => + match o2 with Store i2 => store_op_eq i1 i2 | _ => RET false end end. Lemma op_eq_correct o1 o2: @@ -821,9 +958,35 @@ Definition trans_arith (ai: ar_instruction) : inst := | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))] end. +Definition eval_addressing_rlocs_st (st: store_rs_a) (rs: dreg) (a: addressing) := + match a with + | ADimm base n => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil) + | ADreg base r => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADlsl base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADsxt base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADuxt base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADadr base id ofs => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil) + | ADpostincr base n => Op (Store (OstoreU st a)) (PReg (#rs) @ PReg (pmem) @ Enil) (* not modeled yet *) + end. + +Definition eval_addressing_rlocs_ld (ld: load_rd_a) (a: addressing) := + match a with + | ADimm base n => Op (Load (Oload1 ld a)) (PReg (#base) @ PReg (pmem) @ Enil) + | ADreg base r => Op (Load (Oload2 ld a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADlsl base r n => Op (Load (Oload2 ld a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADsxt base r n => Op (Load (Oload2 ld a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADuxt base r n => Op (Load (Oload2 ld a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADadr base id ofs => Op (Load (Oload1 ld a)) (PReg (#base) @ PReg (pmem) @ Enil) + | ADpostincr base n => Op (Load (OloadU ld a)) (PReg (pmem) @ Enil) (* not modeled yet *) + end. + Definition trans_basic (b: basic) : inst := match b with | PArith ai => trans_arith ai + | PLoad ld r a => + let lr := eval_addressing_rlocs_ld ld a in [(#r, lr)] + | PStore st r a => + let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)] | _ => [] (*| PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))]*) (*| PLoadRRR trap n d a ro => [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*) @@ -1435,6 +1598,27 @@ Local Ltac preg_eq_discr r rd := destruct bi; simpl. (* Arith *) exploit trans_arith_correct; eauto. + + 2: { + unfold exec_store, eval_addressing_rlocs_st, exp_eval; + destruct a; simpl; DIRN1 r; try destruct base; TARITH sr; erewrite H; + unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev; + try destruct (Mem.storev _ _ _ _); simpl; auto. + all: eexists; split; [| split]; [ eauto | eauto | + intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]]. + } + + 1: { + unfold exec_load, eval_addressing_rlocs_ld, exp_eval; + destruct a; simpl; try destruct base; TARITH sr; erewrite H; + unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv; + try destruct (Mem.loadv _ _ _); simpl; auto. + all: eexists; split; [| split]; [ eauto | DDRF rd; eauto | idtac ]; + intros rr; destruct (PregEq.eq rr rd); subst; [ rewrite Pregmap.gss; rewrite sr_gss; reflexivity | + rewrite assign_diff; try rewrite Pregmap.gso; + try rewrite H0; try (fold (ppos rd); eapply ppos_discr); auto]. + } + all: admit. (* (* Load *) - destruct i. @@ -2216,6 +2400,20 @@ Definition string_of_arith (op: arith_op): pstring := | Ofnmul _ => "Ofnmul" end. +Definition string_of_store (op: store_op) : pstring := + match op with + | Ostore1 _ _ => "Ostore1" + | Ostore2 _ _ => "Ostore2" + | OstoreU _ _ => "OstoreU" + end. + +Definition string_of_load (op: load_op) : pstring := + match op with + | Oload1 _ _ => "Oload1" + | Oload2 _ _ => "Oload2" + | OloadU _ _ => "OloadU" + end. + Definition string_of_control (op: control_op) : pstring := match op with | Ob _ => "Ob" @@ -2233,8 +2431,8 @@ Definition string_of_control (op: control_op) : pstring := Definition string_of_op (op: P.op): ?? pstring := match op with | Arith op => RET (string_of_arith op) - (*| Load op => RET (string_of_load op)*) - (*| Store op => RET (string_of_store op)*) + | Load op => RET (string_of_load op) + | Store op => RET (string_of_store op) | Control op => RET (string_of_control op) (*| Allocframe _ _ => RET (Str "Allocframe")*) (*| Allocframe2 _ _ => RET (Str "Allocframe2")*) diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 7c8bd144..79a95df9 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -207,18 +207,19 @@ let reg_of_dreg r = Reg (Asm.DR r) let reg_of_ireg r = Reg (Asm.DR (Asm.IR (Asm.RR1 r))) +let reg_of_iregsp r = Reg (Asm.DR (Asm.IR r)) + let reg_of_ireg0 r = match r with Asm.RR0 ir -> reg_of_ireg ir | Asm.XZR -> IREG0_XZR let reg_of_freg r = Reg (Asm.DR (Asm.FR r)) +let reg_of_cr r = Reg (Asm.CR r) + +let regXSP = Reg (Asm.DR (Asm.IR Asm.XSP)) + let flags_wlocs = - [ - Reg (Asm.CR Asm.CN); - Reg (Asm.CR Asm.CZ); - Reg (Asm.CR Asm.CC); - Reg (Asm.CR Asm.CV); - ] + [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CC; reg_of_cr Asm.CV ] let arith_p_rec i rd = { @@ -296,11 +297,21 @@ let arith_comparison_p_rec i r1 = is_control = false; } +let get_eval_addressing_rlocs a = + match a with + | Asm.ADimm (base, _) -> [ reg_of_iregsp base ] + | Asm.ADreg (base, r) -> [ reg_of_iregsp base; reg_of_ireg r ] + | Asm.ADlsl (base, r, _) -> [ reg_of_iregsp base; reg_of_ireg r ] + | Asm.ADsxt (base, r, _) -> [ reg_of_iregsp base; reg_of_ireg r ] + | Asm.ADuxt (base, r, _) -> [ reg_of_iregsp base; reg_of_ireg r ] + | Asm.ADadr (base, _, _) -> [ reg_of_iregsp base ] + | Asm.ADpostincr (base, _) -> [] + let load_rec ld rd a = { inst = load_rd_a_real ld; write_locs = [ rd ]; - read_locs = [ Mem ]; + read_locs = [ Mem ] @ get_eval_addressing_rlocs a; is_control = false; } @@ -308,7 +319,7 @@ let store_rec st r a = { inst = store_rs_a_real st; write_locs = [ Mem ]; - read_locs = [ r ]; + read_locs = [ r; Mem ] @ get_eval_addressing_rlocs a; is_control = false; } @@ -341,20 +352,18 @@ let cvtx2w_rec rd = let get_testcond_rlocs c = match c with - | Asm.TCeq -> [ Reg (Asm.CR Asm.CZ) ] - | Asm.TCne -> [ Reg (Asm.CR Asm.CZ) ] - | Asm.TChs -> [ Reg (Asm.CR Asm.CC) ] - | Asm.TClo -> [ Reg (Asm.CR Asm.CC) ] - | Asm.TCmi -> [ Reg (Asm.CR Asm.CN) ] - | Asm.TCpl -> [ Reg (Asm.CR Asm.CN) ] - | Asm.TChi -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] - | Asm.TCls -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] - | Asm.TCge -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] - | Asm.TClt -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] - | Asm.TCgt -> - [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] - | Asm.TCle -> - [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] + | Asm.TCeq -> [ reg_of_cr Asm.CZ ] + | Asm.TCne -> [ reg_of_cr Asm.CZ ] + | Asm.TChs -> [ reg_of_cr Asm.CC ] + | Asm.TClo -> [ reg_of_cr Asm.CC ] + | Asm.TCmi -> [ reg_of_cr Asm.CN ] + | Asm.TCpl -> [ reg_of_cr Asm.CN ] + | Asm.TChi -> [ reg_of_cr Asm.CZ; reg_of_cr Asm.CC ] + | Asm.TCls -> [ reg_of_cr Asm.CZ; reg_of_cr Asm.CC ] + | Asm.TCge -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CV ] + | Asm.TClt -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CV ] + | Asm.TCgt -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CV ] + | Asm.TCle -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CV ] let cset_rec rd c = { @@ -395,19 +404,19 @@ let allocframe_rec sz linkofs = write_locs = [ Mem; - Reg (Asm.DR (Asm.IR Asm.XSP)); + regXSP; reg_of_ireg Asm.X16; reg_of_ireg Asm.X29; ]; - read_locs = [ Reg (Asm.DR (Asm.IR Asm.XSP)) ]; + read_locs = [ regXSP ]; is_control = false; } let freeframe_rec sz linkofs = { inst = freeframe_real; - write_locs = [ Mem; Reg (Asm.DR (Asm.IR Asm.XSP)); reg_of_ireg Asm.X16 ]; - read_locs = [ Mem; Reg (Asm.DR (Asm.IR Asm.XSP)) ]; + write_locs = [ Mem; regXSP; reg_of_ireg Asm.X16 ]; + read_locs = [ Mem; regXSP ]; is_control = false; } |