Commit ec1a33e6 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Big improvment in peephole, changing LDP/STP semantics

parent 9d5f379c
......@@ -193,16 +193,16 @@ Inductive instruction: Type :=
| Pldrsh (sz: isize) (rd: ireg) (a: addressing) (**r load int16, sign-extend *)
| Pldrzw (rd: ireg) (a: addressing) (**r load int32, zero-extend to int64 *)
| Pldrsw (rd: ireg) (a: addressing) (**r load int32, sign-extend to int64 *)
| Pldpw (rd1 rd2: ireg) (a: addressing) (**r load two int32 *)
| Pldpx (rd1 rd2: ireg) (a: addressing) (**r load two int64 *)
| Pldpw (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int32 *)
| Pldpx (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *)
| Pstrw (rs: ireg) (a: addressing) (**r store int32 *)
| Pstrw_a (rs: ireg) (a: addressing) (**r store int32 as any32 *)
| Pstrx (rs: ireg) (a: addressing) (**r store int64 *)
| 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) (a: addressing) (**r store two int64 *)
| Pstpx (rs1 rs2: ireg) (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 *)
......@@ -845,16 +845,16 @@ Definition exec_load (chunk: memory_chunk) (transf: val -> val)
| Some v => Next (nextinstr (rs#r <- (transf v))) m
end.
Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
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 chunk with | Mint32 => 4 | _ => 8 end in
let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
match Mem.loadv chunk m addr with
match Mem.loadv chk1 m addr with
| None => Stuck
| Some v1 =>
match Mem.loadv chunk m addr' with
match Mem.loadv chk2 m addr' with
| None => Stuck
| Some v2 =>
Next (nextinstr ((rs#rd1 <- (transf v1))#rd2 <- (transf v2))) m
......@@ -870,16 +870,16 @@ Definition exec_store (chunk: memory_chunk)
| Some m' => Next (nextinstr rs) m'
end.
Definition exec_store_double (chunk: memory_chunk)
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 chunk with | Mint32 => 4 | _ => 8 end in
let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
match Mem.storev chunk m addr v1 with
match Mem.storev chk1 m addr v1 with
| None => Stuck
| Some m' => match Mem.storev chunk m' addr' v2 with
| Some m' => match Mem.storev chk2 m' addr' v2 with
| None => Stuck
| Some m'' => Next (nextinstr rs) m''
end
......@@ -1311,15 +1311,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| 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. *)
| Pldpw rd1 rd2 a =>
exec_load_double Mint32 (fun v => v) a rd1 rd2 rs m
| Pldpx rd1 rd2 a =>
exec_load_double Mint64 (fun v => v) a rd1 rd2 rs m
| 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 a =>
exec_store_double Mint32 a rs#rs1 rs#rs2 rs m
| Pstpx rs1 rs2 a =>
exec_store_double Mint64 a rs#rs1 rs#rs2 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
| Pcls _ _ _
| Pclz _ _ _
| Prev _ _ _
......
......@@ -112,7 +112,7 @@ Inductive load_rd1_rd2_a: Type :=
Inductive ld_instruction: Type :=
| PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing)
| Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (a: addressing) (**r load two int64 *)
| Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *)
.
Inductive store_rs_a : Type :=
......@@ -136,7 +136,7 @@ Inductive store_rs1_rs2_a : Type :=
Inductive st_instruction : Type :=
| PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing)
| Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (a: addressing) (**r store two int64 *)
| Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
.
Inductive arith_p : Type :=
......@@ -459,16 +459,16 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val)
SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN
Next (rs#r <- (transf v)) m.
Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
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 chunk with | Mint32 => 4 | _ => 8 end in
let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
match Mem.loadv chunk m addr with
match Mem.loadv chk1 m addr with
| None => Stuck
| Some v1 =>
match Mem.loadv chunk m addr' with
match Mem.loadv chk2 m addr' with
| None => Stuck
| Some v2 =>
Next ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m
......@@ -482,16 +482,16 @@ Definition exec_store_rs_a (chunk: memory_chunk)
SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
Next rs m'.
Definition exec_store_double (chunk: memory_chunk)
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 chunk with | Mint32 => 4 | _ => 8 end in
let ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in
let addr' := (eval_addressing (get_offset_addr a ofs) rs) in
match Mem.storev chunk m addr v1 with
match Mem.storev chk1 m addr v1 with
| None => Stuck
| Some m' => match Mem.storev chunk m' addr' v2 with
| Some m' => match Mem.storev chk2 m' addr' v2 with
| None => Stuck
| Some m'' => Next rs m''
end
......@@ -501,67 +501,62 @@ Definition exec_store_double (chunk: memory_chunk)
(** execution of loads
*)
Definition chunk_load (ld: ld_instruction): memory_chunk :=
Definition chunk_load (ld: load_rd_a): memory_chunk :=
match ld with
| PLd_rd_a Pldrw _ _ => Mint32
| PLd_rd_a Pldrw_a _ _ => Many32
| PLd_rd_a Pldrx _ _ => Mint64
| PLd_rd_a Pldrx_a _ _ => Many64
| PLd_rd_a (Pldrb _) _ _ => Mint8unsigned
| PLd_rd_a (Pldrsb _) _ _ => Mint8signed
| PLd_rd_a (Pldrh _) _ _ => Mint16unsigned
| PLd_rd_a (Pldrsh _) _ _ => Mint16signed
| PLd_rd_a Pldrzw _ _ => Mint32
| PLd_rd_a Pldrsw _ _ => Mint32
| PLd_rd_a Pldrs _ _ => Mfloat32
| PLd_rd_a Pldrd _ _ => Mfloat64
| PLd_rd_a Pldrd_a _ _ => Many64
| Pldp Pldpw _ _ _ => Mint32
| Pldp Pldpx _ _ _ => Mint64
| 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: st_instruction) : memory_chunk :=
Definition chunk_store (st: store_rs_a) : memory_chunk :=
match st with
| PSt_rs_a Pstrw _ _ => Mint32
| PSt_rs_a Pstrw_a _ _ => Many32
| PSt_rs_a Pstrx _ _ => Mint64
| PSt_rs_a Pstrx_a _ _ => Many64
| PSt_rs_a Pstrb _ _ => Mint8unsigned
| PSt_rs_a Pstrh _ _ => Mint16unsigned
| PSt_rs_a Pstrs _ _ => Mfloat32
| PSt_rs_a Pstrd _ _ => Mfloat64
| PSt_rs_a Pstrd_a _ _ => Many64
| Pstp Pstpw _ _ _ => Mint32
| Pstp Pstpx _ _ _ => Mint64
| 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: ld_instruction): val -> val :=
Definition interp_load (ld: load_rd_a): val -> val :=
match ld with
| PLd_rd_a (Pldrb X) _ _ => Val.longofintu
| PLd_rd_a (Pldrsb X) _ _ => Val.longofint
| PLd_rd_a (Pldrh X) _ _ => Val.longofintu
| PLd_rd_a (Pldrsh X) _ _ => Val.longofint
| PLd_rd_a Pldrzw _ _ => Val.longofintu
| PLd_rd_a Pldrsw _ _ => Val.longofint
| 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. *)
| PLd_rd_a (Pldrb W) _ _ | PLd_rd_a (Pldrsb W) _ _ | PLd_rd_a (Pldrh W) _ _ | PLd_rd_a (Pldrsh W) _ _
| PLd_rd_a Pldrw _ _ | PLd_rd_a Pldrw_a _ _ | PLd_rd_a Pldrx _ _
| PLd_rd_a Pldrx_a _ _ | PLd_rd_a Pldrs _ _ | PLd_rd_a Pldrd _ _
| PLd_rd_a Pldrd_a _ _
| Pldp _ _ _ _ => fun v => v
| 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 ldi) (interp_load ldi) a rd rs m
| Pldp ld rd1 rd2 a => exec_load_double (chunk_load ldi) (interp_load ldi) a rd1 rd2 rs m
| 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 sti) a rs#rsr rs m
| Pstp st rs1 rs2 a => exec_store_double (chunk_store sti) a rs#rs1 rs#rs2 rs m
| 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 ?? *)
......
......@@ -166,15 +166,15 @@ Inductive arith_op :=
.
Inductive store_op :=
| Ostore1 (st: st_instruction) (a: addressing)
| Ostore2 (st: st_instruction) (a: addressing)
| OstoreU (st: st_instruction) (a: addressing)
| Ostore1 (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
| Ostore2 (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
| OstoreU (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
.
Inductive load_op :=
| Oload1 (ld: ld_instruction) (a: addressing)
| Oload2 (ld: ld_instruction) (a: addressing)
| OloadU (ld: ld_instruction) (a: addressing)
| Oload1 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
| Oload2 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
| OloadU (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
.
Inductive allocf_op :=
......@@ -424,16 +424,16 @@ Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) :
| None => None (* should never occurs *)
end.
Definition exec_store1 (n: st_instruction) (m: mem) (a: addressing) (vr vs: val) :=
Definition exec_store1 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (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 (chunk_store n) m v vr.
call_ll_storev chunk m v vr.
Definition exec_store2 (n: st_instruction) (m: mem) (a: addressing) (vr vs1 vs2: val) :=
Definition exec_store2 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr vs1 vs2: val) :=
let v :=
match a with
| ADreg _ _ => Some (Val.addl vs1 vs2)
......@@ -442,10 +442,10 @@ Definition exec_store2 (n: st_instruction) (m: mem) (a: addressing) (vr vs1 vs2:
| ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n)))
| _ => None
end in
call_ll_storev (chunk_store n) m v vr.
call_ll_storev chunk m v vr.
Definition exec_storeU (n: st_instruction) (m: mem) (a: addressing) (vr: val) :=
call_ll_storev (chunk_store n) m None vr.
Definition exec_storeU (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr: val) :=
call_ll_storev chunk m None vr.
Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
match label_pos lbl 0 (fn_blocks f) with
......@@ -503,9 +503,9 @@ Definition control_eval (o: control_op) (l: list value) :=
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
| Ostore1 st chunk a, [Val vr; Val vs; Memstate m] => exec_store1 st m chunk a vr vs
| Ostore2 st chunk a, [Val vr; Val vs1; Val vs2; Memstate m] => exec_store2 st m chunk a vr vs1 vs2
| OstoreU st chunk a, [Val vr; Memstate m] => exec_storeU st m chunk a vr
| _, _ => None
end.
......@@ -518,16 +518,16 @@ Definition call_ll_loadv (c: memory_chunk) (transf: val -> val) (m: mem) (v: opt
| None => None (* should never occurs *)
end.
Definition exec_load1 (ld: ld_instruction) (m: mem) (a: addressing) (vl: val) :=
Definition exec_load1 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (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 (chunk_load ld) (interp_load ld) m v.
call_ll_loadv chunk (interp_load ld) m v.
Definition exec_load2 (ld: ld_instruction) (m: mem) (a: addressing) (vl1 vl2: val) :=
Definition exec_load2 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vl1 vl2: val) :=
let v :=
match a with
| ADreg _ _ => Some (Val.addl vl1 vl2)
......@@ -536,16 +536,16 @@ Definition exec_load2 (ld: ld_instruction) (m: mem) (a: addressing) (vl1 vl2: va
| ADuxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofintu vl2) (Vint n)))
| _ => None
end in
call_ll_loadv (chunk_load ld) (interp_load ld) m v.
call_ll_loadv chunk (interp_load ld) m v.
Definition exec_loadU (n: ld_instruction) (m: mem) (a: addressing) :=
call_ll_loadv (chunk_load n) (interp_load n) m None.
Definition exec_loadU (n: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) :=
call_ll_loadv chunk (interp_load n) m None.
Definition load_eval (o: load_op) (l: list value) :=
match o, l with
| Oload1 ld a, [Val vs; Memstate m] => exec_load1 ld m a vs
| Oload2 ld a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m a vs1 vs2
| OloadU st a, [Memstate m] => exec_loadU st m a
| Oload1 ld chunk a, [Val vs; Memstate m] => exec_load1 ld m chunk a vs
| Oload2 ld chunk a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m chunk a vs1 vs2
| OloadU st chunk a, [Memstate m] => exec_loadU st m chunk a
| _, _ => None
end.
......@@ -768,12 +768,12 @@ 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 (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
| Ostore2 st1 a1 =>
match s2 with Ostore2 st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
| OstoreU st1 a1 =>
match s2 with OstoreU st2 a2 => iandb (struct_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
| Ostore1 st1 chk1 a1 =>
match s2 with Ostore1 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
| Ostore2 st1 chk1 a1 =>
match s2 with Ostore2 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
| OstoreU st1 chk1 a1 =>
match s2 with OstoreU st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
end.
Lemma store_op_eq_correct s1 s2:
......@@ -787,12 +787,12 @@ 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 (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
| Oload2 ld1 a1 =>
match l2 with Oload2 ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
| OloadU ld1 a1 =>
match l2 with OloadU ld2 a2 => iandb (struct_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
| Oload1 ld1 chk1 a1 =>
match l2 with Oload1 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
| Oload2 ld1 chk1 a1 =>
match l2 with Oload2 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
| OloadU ld1 chk1 a1 =>
match l2 with OloadU ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
end.
Lemma load_op_eq_correct l1 l2:
......@@ -1127,45 +1127,58 @@ 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: st_instruction) (rs: dreg) (a: addressing) :=
Definition eval_addressing_rlocs_st (st: store_rs_a) (chunk: memory_chunk) (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 *)
| ADimm base n => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
| ADreg base r => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADlsl base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADsxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADuxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADadr base id ofs => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
| ADpostincr base n => Op (Store (OstoreU st chunk a)) (PReg (#rs) @ PReg (pmem) @ Enil) (* not modeled yet *)
end.
Definition eval_addressing_rlocs_ld (ld: ld_instruction) (a: addressing) :=
Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (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 (Oload1 ld a)) (PReg (#base) @ PReg (pmem) @ Enil)
| ADimm base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
| ADreg base r => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADlsl base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADsxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADuxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
| ADadr base id ofs => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
| 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 :=
match chunk with
| Many32 => Pldrw_a
| Mint64 => Pldrx
| Many64 => Pldrx_a
| _ => Pldrw
end.
Definition trans_stp_chunk (chunk: memory_chunk): store_rs_a :=
match chunk with
| Many32 => Pstrw_a
| Mint64 => Pstrx
| Many64 => Pstrx_a
| _ => Pstrw
end.
Definition trans_load (ldi: ld_instruction) :=
match ldi with
| PLd_rd_a ld r a =>
let lr := eval_addressing_rlocs_ld ldi a in [(#r, lr)]
| Pldp ld r1 r2 a =>
let ldi' :=
match ld with
| Pldpw => Pldrw
| Pldpx => Pldrx
end in
let lr := eval_addressing_rlocs_ld (PLd_rd_a ldi' r1 a) a in
let ofs := match ld with | Pldpw => 4%Z | Pldpx => 8%Z end in
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 lr := eval_addressing_rlocs_ld ldi1 chk1 a in
let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
match a with
| ADimm base n =>
let a' := (get_offset_addr a ofs) in
[(#r1, lr);
(#r2, Op (Load (Oload1 (PLd_rd_a ldi' r2 a') a'))
(#r2, Op (Load (Oload1 ldi2 chk2 a'))
(Old(PReg (#base)) @ PReg (pmem) @ Enil))]
| _ => [(#PC, (Op (OError)) Enil)]
end
......@@ -1174,20 +1187,17 @@ Definition trans_load (ldi: ld_instruction) :=
Definition trans_store (sti: st_instruction) :=
match sti with
| PSt_rs_a st r a =>
let lr := eval_addressing_rlocs_st sti r a in [(pmem, lr)]
| Pstp st r1 r2 a =>
let sti' :=
match st with
| Pstpw => Pstrw
| Pstpx => Pstrx
end in
let lr := eval_addressing_rlocs_st (PSt_rs_a sti' r1 a) r1 a in
let ofs := match st with | Pstpw => 4%Z | Pstpx => 8%Z end in
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 lr := eval_addressing_rlocs_st sti1 chk1 r1 a in
let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in
match a with
| ADimm base n =>
let a' := (get_offset_addr a ofs) in
[(pmem, lr);
(pmem, Op (Store (Ostore1 (PSt_rs_a sti' r2 a') a'))
(pmem, Op (Store (Ostore1 sti2 chk2 a'))
(PReg (#r2) @ Old(PReg (#base)) @ PReg (pmem) @ Enil))]
| _ => [(#PC, (Op (OError)) Enil)]
end
......@@ -1695,6 +1705,12 @@ Proof.
econstructor.
Qed.
Lemma load_chunk_neutral: forall chk v,
interp_load (trans_ldp_chunk chk) v = v.
Proof.
intros; destruct chk; simpl; reflexivity.
Qed.
Theorem bisimu_basic rsr mr sr bi:
match_states (State rsr mr) sr ->
match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr).
......@@ -1721,14 +1737,16 @@ Local Ltac preg_eq_discr r rd :=
unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv;
try destruct (Mem.loadv _ _ _); simpl; auto.
all: try (fold (ppos rd); Simpl_exists sr; auto; intros rr; Simpl_update).
+ unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval;
+
unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval;
destruct ld; destruct a; simpl; unfold control_eval; destruct Ge; auto;
try fold (ppos base);
try erewrite !H0, H; simpl;
unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv;
try destruct (Mem.loadv _ _ _); simpl; auto;
unfold exec_load1, exec_load2; unfold call_ll_loadv;
destruct (Mem.loadv _ _ _); simpl; auto;
fold (ppos rd1); rewrite assign_diff; discriminate_ppos; rewrite H;
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).
......@@ -1746,7 +1764,7 @@ Local Ltac preg_eq_discr r rd :=
destruct st; destruct a; simpl; unfold control_eval; destruct Ge; auto;
try fold (ppos base); try fold (ppos rs1);
erewrite !H0, H; simpl;
unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev;
unfold exec_store1, exec_store2; unfold call_ll_storev;