Commit cac0556d authored by David Monniaux's avatar David Monniaux
Browse files

Merge remote-tracking branch 'origin/aarch64-peephole' into kvx-work

parents e265be77 0bc5b0f9
......@@ -201,8 +201,8 @@ Inductive instruction: Type :=
| Pstrx_a (rs: ireg) (a: addressing) (**r store int64 as any64 *)
| Pstrb (rs: ireg) (a: addressing) (**r store int8 *)
| Pstrh (rs: ireg) (a: addressing) (**r store int16 *)
| Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
| Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
| Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
| Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
(** Integer arithmetic, immediate *)
| Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r addition *)
| Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r subtraction *)
......@@ -273,9 +273,13 @@ Inductive instruction: Type :=
| Pldrs (rd: freg) (a: addressing) (**r load float32 (single precision) *)
| Pldrd (rd: freg) (a: addressing) (**r load float64 (double precision) *)
| Pldrd_a (rd: freg) (a: addressing) (**r load float64 as any64 *)
| Pldps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two float32 *)
| Pldpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two float64 *)
| Pstrs (rs: freg) (a: addressing) (**r store float32 *)
| Pstrd (rs: freg) (a: addressing) (**r store float64 *)
| Pstrd_a (rs: freg) (a: addressing) (**r store float64 as any64 *)
| Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float32 *)
| Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float64 *)
(** Floating-point move *)
| Pfmov (rd r1: freg)
| Pfmovimms (rd: freg) (f: float32) (**r load float32 constant *)
......@@ -798,7 +802,7 @@ Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val)
(a: addressing) (rd1 rd2: preg) (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 | Many32 => 4 | _ => 8 end 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
......@@ -824,7 +828,7 @@ Definition exec_store_double (chk1 chk2: memory_chunk)
(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 | Many32 => 4 | _ => 8 end 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
......@@ -1258,17 +1262,27 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| _ => Stuck
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. *)
(** loads and stores pairs int/int64 *)
| Pldpw rd1 rd2 chk1 chk2 a =>
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
| Pldpx rd1 rd2 chk1 chk2 a =>
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
| Pnop => Next (nextinstr rs) m
| Pstpw rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
| Pstpx rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
(** loads and stores pairs floating-point *)
| Pldps rd1 rd2 chk1 chk2 a =>
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
| Pldpd rd1 rd2 chk1 chk2 a =>
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
| Pstps rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
| Pstpd rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
| Pnop => Next (nextinstr rs) m
(** The following instructions and directives are not generated directly
by Asmgen, so we do not model them. *)
| Pcls _ _ _
| Pclz _ _ _
| Prev _ _ _
......
......@@ -110,11 +110,13 @@ Inductive load_rd_a: Type :=
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: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *)
| Pldp (ld: load_rd1_rd2_a) (rd1 rd2: dreg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *)
.
Inductive store_rs_a : Type :=
......@@ -134,11 +136,13 @@ Inductive store_rs_a : Type :=
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: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
| Pstp (st: store_rs1_rs2_a) (rs1 rs2: dreg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
.
Inductive arith_p : Type :=
......@@ -481,7 +485,7 @@ 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 | Many32 => 4 | _ => 8 end 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
......@@ -505,7 +509,7 @@ Definition exec_store_double (chk1 chk2: memory_chunk)
(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 | Many32 => 4 | _ => 8 end 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
......
......@@ -1150,20 +1150,32 @@ Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (a: ad
| ADpostincr base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
end.
Definition trans_ldp_chunk (chunk: memory_chunk): load_rd_a :=
Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a :=
match chunk with
| Many32 => Pldrw_a
| Mint32 => Pldrw
| Mint64 => Pldrx
| Many64 => Pldrx_a
| _ => Pldrw
| Mfloat32 => Pldrs
| Mfloat64 => Pldrd
| Many32 => Pldrw_a
| _ => (* This case should always correspond to Many64 *)
match r with
| IR _ => Pldrx_a
| FR _ => Pldrd_a
end
end.
Definition trans_stp_chunk (chunk: memory_chunk): store_rs_a :=
Definition trans_stp_chunk (chunk: memory_chunk) (r: dreg): store_rs_a :=
match chunk with
| Many32 => Pstrw_a
| Mint32 => Pstrw
| Mint64 => Pstrx
| Many64 => Pstrx_a
| _ => Pstrw
| Mfloat32 => Pstrs
| Mfloat64 => Pstrd
| Many32 => Pstrw_a
| _ => (* This case should always correspond to Many64 *)
match r with
| IR _ => Pstrx_a
| FR _ => Pstrd_a
end
end.
Definition trans_load (ldi: ld_instruction) :=
......@@ -1171,10 +1183,10 @@ Definition trans_load (ldi: ld_instruction) :=
| PLd_rd_a ld r a =>
let lr := eval_addressing_rlocs_ld ld (chunk_load ld) a in [(#r, lr)]
| Pldp ld r1 r2 chk1 chk2 a =>
let ldi1 := trans_ldp_chunk chk1 in
let ldi2 := trans_ldp_chunk chk2 in
let ldi1 := trans_ldp_chunk chk1 r1 in
let ldi2 := trans_ldp_chunk chk2 r1 in
let lr := eval_addressing_rlocs_ld ldi1 chk1 a in
let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4%Z | _ => 8%Z end in
match a with
| ADimm base n =>
let a' := (get_offset_addr a ofs) in
......@@ -1190,10 +1202,10 @@ Definition trans_store (sti: st_instruction) :=
| PSt_rs_a st r a =>
let lr := eval_addressing_rlocs_st st (chunk_store st) r a in [(pmem, lr)]
| Pstp st r1 r2 chk1 chk2 a =>
let sti1 := trans_stp_chunk chk1 in
let sti2 := trans_stp_chunk chk2 in
let sti1 := trans_stp_chunk chk1 r1 in
let sti2 := trans_stp_chunk chk2 r1 in
let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in
let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in
match a with
| ADimm base n =>
let a' := (get_offset_addr a ofs) in
......@@ -1356,6 +1368,14 @@ Proof.
intros; destruct r; discriminate.
Qed.
Lemma dreg_not_pmem: forall (r: dreg),
(# r) <> pmem.
Proof.
intros; destruct r as [i|f].
- destruct i. apply ireg_not_pmem. discriminate.
- apply freg_not_pmem.
Qed.
Ltac DPRM pr :=
destruct pr as [drDPRF|crDPRF|];
[destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
......@@ -1463,6 +1483,7 @@ Ltac discriminate_ppos :=
try apply ireg_not_pmem;
try apply ireg_not_pc;
try apply freg_not_pmem;
try apply dreg_not_pmem;
try apply ireg_not_CN;
try apply ireg_not_CZ;
try apply ireg_not_CC;
......@@ -1706,10 +1727,10 @@ Proof.
econstructor.
Qed.
Lemma load_chunk_neutral: forall chk v,
interp_load (trans_ldp_chunk chk) v = v.
Lemma load_chunk_neutral: forall chk v r,
interp_load (trans_ldp_chunk chk r) v = v.
Proof.
intros; destruct chk; simpl; reflexivity.
intros; destruct chk; destruct r; simpl; reflexivity.
Qed.
Theorem bisimu_basic rsr mr sr bi:
......@@ -1749,8 +1770,10 @@ Local Ltac preg_eq_discr r rd :=
try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr;
rewrite !load_chunk_neutral;
try (rewrite !assign_diff; discriminate_ppos; reflexivity);
try (destruct base; discriminate_ppos);
repeat (try fold (ppos r); intros; Simpl_update).
try (destruct rd1 as [ir1|fr1]; try destruct ir1; destruct rd2 as [ir2|fr2]; try destruct ir2;
destruct base; discriminate_ppos);
repeat (try fold (ppos r); try fold (ppos r0);
try fold (ppos fr1); try fold (ppos fr2); intros; Simpl_update).
- (* Store *)
destruct st.
+ unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval;
......
......@@ -326,10 +326,16 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
| PLoad (Pldp Pldpw rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
do rd2' <- ireg_of_preg rd2;
OK (Asm.Pldpw rd1 rd2 chk1 chk2 a)
OK (Asm.Pldpw rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldpx rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
do rd2' <- ireg_of_preg rd2;
OK (Asm.Pldpx rd1 rd2 chk1 chk2 a)
OK (Asm.Pldpx rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldps rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
do rd2' <- freg_of_preg rd2;
OK (Asm.Pldps rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldpd rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
do rd2' <- freg_of_preg rd2;
OK (Asm.Pldpd rd1' rd2' chk1 chk2 a)
| PStore (PSt_rs_a Pstrw r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a)
| PStore (PSt_rs_a Pstrw_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a)
......@@ -344,10 +350,16 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
| PStore (Pstp Pstpw rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
do rs2' <- ireg_of_preg rs2;
OK (Asm.Pstpw rs1 rs2 chk1 chk2 a)
OK (Asm.Pstpw rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstpx rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
do rs2' <- ireg_of_preg rs2;
OK (Asm.Pstpx rs1 rs2 chk1 chk2 a)
OK (Asm.Pstpx rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstps rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstps rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstpd rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstpd rs1' rs2' chk1 chk2 a)
| Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs)
| Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs)
......
......@@ -1100,7 +1100,7 @@ Proof.
destruct (Mem.loadv chk2 m2
(eval_addressing lk
(get_offset_addr a match chk1 with
| Mint32 | Many32 => 4
| Mint32 | Mfloat32| Many32 => 4
| _ => 8
end) rs1));
inversion HLOAD; auto.
......@@ -1150,7 +1150,7 @@ Proof.
(eval_addressing lk
(get_offset_addr a
match chk1 with
| Mint32 | Many32 => 4
| Mint32 | Mfloat32 | Many32 => 4
| _ => 8
end) rs1) v2);
inversion HSTORE; auto.
......@@ -1331,12 +1331,14 @@ Proof.
destruct ld.
- destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto;
intros; simpl in *; destruct sz; eauto.
- destruct ld; monadInv TRANSBI; exploit load_double_preserved; eauto. }
- destruct ld; monadInv TRANSBI; destruct rd1 as [[rd1'|]|]; destruct rd2 as [[rd2'|]|];
inv EQ; inv EQ1; exploit load_double_preserved; eauto. }
{ (* PStore *)
destruct st.
- destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto;
simpl in *; inv_matchi; find_rwrt_ag.
- destruct st; monadInv TRANSBI; exploit store_double_preserved; eauto;
- destruct st; monadInv TRANSBI; destruct rs0 as [[rs0'|]|]; destruct rs3 as [[rs3'|]|];
inv EQ; inv EQ1; exploit store_double_preserved; eauto;
simpl in *; inv_matchi; find_rwrt_ag. }
{ (* Pallocframe *)
monadInv TRANSBI;
......@@ -2224,8 +2226,7 @@ Proof.
- apply senv_preserved.
- eexact transf_initial_states.
- eexact transf_final_states.
- (* TODO step_simulation *)
unfold match_states.
- unfold match_states.
simpl; intros; subst; eexists; split; eauto.
eapply step_simulation; eauto.
Qed.
......
This diff is collapsed.
......@@ -137,8 +137,8 @@ let load_rec ldi =
| PLd_rd_a (ld, rd, a) ->
load_rd_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd) a
| Pldp (ld, rd1, rd2, _, _, a) ->
load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_ireg rd1)
(reg_of_ireg rd2) a
load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd1)
(reg_of_dreg rd2) a
let store_rs_a_rec st rs a =
{
......@@ -161,8 +161,8 @@ let store_rec sti =
| PSt_rs_a (st, rs, a) ->
store_rs_a_rec (PBasic (PStore sti)) (reg_of_dreg rs) a
| Pstp (st, rs1, rs2, _, _, a) ->
store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_ireg rs1)
(reg_of_ireg rs2) a
store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_dreg rs1)
(reg_of_dreg rs2) a
let loadsymbol_rec i rd id =
{ inst = i; write_locs = [ rd ]; read_locs = [ Mem ]; is_control = false }
......
......@@ -417,6 +417,14 @@ module Target (*: TARGET*) =
fprintf oc " str %a, %a\n" sreg rd addressing a
| Pstrd(rd, a) | Pstrd_a(rd, a) ->
fprintf oc " str %a, %a\n" dreg rd addressing a
| Pldps(rd1, rd2, _, _, a) ->
fprintf oc " ldp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
| Pldpd(rd1, rd2, _, _, a) ->
fprintf oc " ldp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
| Pstps(rd1, rd2, _, _, a) ->
fprintf oc " stp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
| Pstpd(rd1, rd2, _, _, a) ->
fprintf oc " stp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
(* Floating-point move *)
| Pfmov(rd, r1) ->
fprintf oc " fmov %a, %a\n" dreg rd dreg r1
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment