diff options
Diffstat (limited to 'aarch64/Asmblockdeps.v')
| -rw-r--r-- | aarch64/Asmblockdeps.v | 202 |
1 files changed, 110 insertions, 92 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index e2d788a5..1ad18889 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -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; try destruct (Mem.storev _ _ _ _); simpl; auto; fold (ppos rs2); rewrite assign_diff; try congruence; try rewrite H0; simpl; try destruct (Mem.storev _ _ _ _); simpl; auto. @@ -2473,22 +2491,22 @@ Definition string_of_ldi (ldi: ld_instruction) : ?? pstring:= DO a' <~ string_of_addressing a;; DO rd' <~ dreg_name rd;; RET (Str "PLd_rd_a (" +; (string_of_ld_rd_a ld) +; " " +; rd' +; " " +; a' +; ")") - | Pldp _ _ _ a => + | Pldp _ _ _ _ _ a => DO a' <~ string_of_addressing a;; RET (Str "Pldp (" +; a' +; ")") end. Definition string_of_load (op: load_op) : ?? pstring := match op with - | Oload1 ld a => + | Oload1 ld _ a => DO a' <~ string_of_addressing a;; - DO ld' <~ string_of_ldi ld;; - RET((Str "Oload1 ") +; " " +; ld' +; " " +; a' +; " ") - | Oload2 ld a => + (*DO ld' <~ string_of_ldi ld;;*) + RET((Str "Oload1 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ") + | Oload2 ld _ a => DO a' <~ string_of_addressing a;; - DO ld' <~ string_of_ldi ld;; - RET((Str "Oload2 ") +; " " +; ld' +; " " +; a' +; " ") - | OloadU _ _ => RET (Str "OloadU") + (*DO ld' <~ string_of_ldi ld;;*) + RET((Str "Oload2 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ") + | OloadU _ _ _ => RET (Str "OloadU") end. Definition string_of_st_rs_a (st: store_rs_a) : pstring := @@ -2510,22 +2528,22 @@ Definition string_of_sti (sti: st_instruction) : ?? pstring:= DO a' <~ string_of_addressing a;; DO rs' <~ dreg_name rs;; RET (Str "PSt_rs_a (" +; (string_of_st_rs_a st) +; " " +; rs' +; " " +; a' +; ")") - | Pstp _ _ _ a => + | Pstp _ _ _ _ _ a => DO a' <~ string_of_addressing a;; RET (Str "Pstp (" +; a' +; ")") end. Definition string_of_store (op: store_op) : ?? pstring := match op with - | Ostore1 st a => + | Ostore1 st _ a => DO a' <~ string_of_addressing a;; - DO st' <~ string_of_sti st;; - RET((Str "Ostore1 ") +; " " +; st' +; " " +; a' +; " ") - | Ostore2 st a => + (*DO st' <~ string_of_sti st;;*) + RET((Str "Ostore1 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ") + | Ostore2 st _ a => DO a' <~ string_of_addressing a;; - DO st' <~ string_of_sti st;; - RET((Str "Ostore2 ") +; " " +; st' +; " " +; a' +; " ") - | OstoreU _ _ => RET (Str "OstoreU") + (*DO st' <~ string_of_sti st;;*) + RET((Str "Ostore2 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ") + | OstoreU _ _ _ => RET (Str "OstoreU") end. Definition string_of_control (op: control_op) : pstring := |