Loads and stores op

1 files changed, 203 insertions, 5 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")*)