From 4aa289a5066ebe3081f66c9c0a02fd873720c8ad Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 13 Nov 2020 12:10:46 +0100 Subject: Loads and stores op --- aarch64/Asmblockdeps.v | 208 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 203 insertions(+), 5 deletions(-) (limited to 'aarch64/Asmblockdeps.v') 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")*) -- cgit