getting stuck need to move offsets

4 files changed, 40 insertions, 10 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d73d00c7..8b1c9a81 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -122,7 +122,9 @@ Inductive instruction : Type :=
   | Psd     (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store int64 *)

   | Psd_a   (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store any64 *)

   | Pfss    (rs: freg) (ra: ireg) (ofs: addressing)     (**r store float *)

-  | Pfsd     (rd: freg) (ra: ireg) (ofs: addressing)    (**r store 64-bit float *)

+  | Pfsd    (rs: freg) (ra: ireg) (ofs: addressing)    (**r store 64-bit float *)

+

+  | Psq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r store 64-bit float *)

 

   (** Arith RR *)

   | Pmv     (rd rs: ireg)                           (**r register move *)

@@ -484,6 +486,7 @@ Definition basic_to_instruction (b: basic) :=
   | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro)

   | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)

 

+  | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs)

   end.

 

 Section RELSEM.

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 1ee5002c..04f02a80 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -639,6 +639,10 @@ Definition trans_basic (b: basic) : inst :=
   | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))]
   | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
   | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
+  | PStoreQRRO qs a ofs =>
+    let (s0, s1) := gpreg_q_expand qs in 
+    [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));
+     (pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))]
   | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
                            (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))]
   | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil));
@@ -884,7 +888,10 @@ Proof.
       eexists; split; try split; Simpl;
       intros rr; destruct rr; Simpl.
 
-(* Allocframe *)
+    + unfold parexec_store_q_offset.
+      destruct (gpreg_q_expand rs) as [s0 s1].
+      simpl.
+  (* Allocframe *)
   - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
     * eexists; repeat split.
       { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl.
@@ -1529,5 +1536,3 @@ Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bbloc
 Definition bblock_equiv_eq := pure_bblock_eq_test_correct true.
 
 End SECT_BBLOCK_EQUIV.
-
-
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 0cbe27e1..fb1575f9 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -236,9 +236,6 @@ Definition label := positive.
 *)
 Inductive ex_instruction : Type :=
   (* Pseudo-instructions *)
-(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
-  | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
-
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
 .
@@ -341,6 +338,7 @@ Inductive st_instruction : Type :=
   | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
   | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
   | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
+  | PStoreQRRO (rs: gpreg_q) (ra: ireg) (ofs: offset)
 .
 
 (** Arithmetic instructions **)
@@ -355,7 +353,6 @@ Inductive arith_name_rr : Type :=
   | Pcvtl2w                                         (**r Convert Long to Word *)
   | Psxwd                                           (**r Sign Extend Word to Double Word *)
   | Pzxwd                                           (**r Zero Extend Word to Double Word *)
-(*  | Pextfs (stop : int) (start : int)               (**r extract bit field, signed *) *)
   | Pextfz (stop : Z) (start : Z)               (**r extract bit field, unsigned *)
   | Pextfs (stop : Z) (start : Z)               (**r extract bit field, signed *)
   | Pextfzl (stop : Z) (start : Z)              (**r extract bit field, unsigned *)
@@ -693,7 +690,7 @@ Variable ge: genv.
   from the current state (a register set + a memory state) to either [Next rs' m']
   where [rs'] and [m'] are the updated register set and memory state after execution
   of the instruction at [rs#PC], or [Stuck] if the processor is stuck.
-
+ 
   The parallel semantics of each instructions handles two states in input:
    - the actual input state of the bundle which is only read
    - and the other on which every "write" is performed:
@@ -1198,6 +1195,23 @@ Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m
   | Some m' => Next rsw m'
   end.
 
+Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (a: ireg) (ofs: offset) :=
+  let (s0, s1) := gpreg_q_expand s in
+  match eval_offset ofs with
+  | OK eofs =>
+    let base := Val.offset_ptr (rsr a) eofs in
+    match Mem.storev Many64 mr base (rsr s0) with
+    | None => Stuck
+    | Some m1 =>
+      match Mem.storev Many64 m1 base (rsr s1) with
+      | None => Stuck
+      | Some m2 => Next rsw m2
+      end
+    end
+  | _ => Stuck
+  end.
+  
+
 Definition load_chunk n :=
   match n with
   | Plb => Mint8signed
@@ -1237,7 +1251,8 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs
   | PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro
   | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro
-
+  | PStoreQRRO s a ofs => 
+    parexec_store_q_offset rsr rsw mr mw s a ofs
   | Pallocframe sz pos =>
       let (mw, stk) := Mem.alloc mr 0 sz in
       let sp := (Vptr stk Ptrofs.zero) in
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 0a83a903..a93cb28a 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -950,6 +950,13 @@ Proof.
   1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
   1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+  - (* PStoreQRRO *)
+    unfold  parexec_store_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    destruct (eval_offset _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity.
   - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
   - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
     destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.