diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 03:33:58 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 03:33:58 +0200 |
commit | 8163278174362fb8269804a7958f6e9e7878a511 (patch) | |
tree | 443fe57bfde8cacb7806c3a8dd69f499709bdee4 /mppa_k1c/Asmvliw.v | |
parent | 5d09dd8f3194ecc90137178d6b5d18b9ad31aabf (diff) | |
download | compcert-kvx-8163278174362fb8269804a7958f6e9e7878a511.tar.gz compcert-kvx-8163278174362fb8269804a7958f6e9e7878a511.zip |
getting stuck need to move offsets
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
-rw-r--r-- | mppa_k1c/Asmvliw.v | 27 |
1 files changed, 21 insertions, 6 deletions
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 |