diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 21:54:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 21:54:11 +0200 |
| commit | cbe3f094b32077ce8d8569556d4ebc6341b09dd9 (patch) | |
| tree | 61824ef04196070b165e18f788b7cca153087bc0 /mppa_k1c/Asmvliw.v | |
| parent | 98be0205d9d29378fb272a9f424144651bd8afec (diff) | |
| download | compcert-kvx-cbe3f094b32077ce8d8569556d4ebc6341b09dd9.tar.gz compcert-kvx-cbe3f094b32077ce8d8569556d4ebc6341b09dd9.zip | |
it compiles
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 7a5adf5e..629d1449 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -273,9 +273,6 @@ Inductive ld_instruction : Type := | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . -Coercion PLoadRRO: load_name >-> Funclass. -Coercion PLoadRRR: load_name >-> Funclass. - (** Stores **) Inductive store_name : Type := | Psb (**r store byte *) @@ -291,11 +288,9 @@ Inductive store_name : Type := 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) . -Coercion PStoreRRO: store_name >-> Funclass. -Coercion PStoreRRR: store_name >-> Funclass. - (** Arithmetic instructions **) Inductive arith_name_r : Type := | Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) @@ -1160,6 +1155,12 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem | Some m' => Next rsw m' end. +Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := + match Mem.storev chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' + end. + Definition load_chunk n := match n with | Plb => Mint8signed @@ -1198,6 +1199,7 @@ 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 | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in |