diff options
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 55 |
1 files changed, 38 insertions, 17 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 54e9c847..946007c1 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -308,6 +308,16 @@ Inductive cf_instruction : Type := . (** Loads **) +Definition concrete_default_notrap_load_value (chunk : memory_chunk) := + match chunk with + | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned + | Mint32 => Vint Int.zero + | Mint64 => Vlong Int64.zero + | Many32 | Many64 => Vundef + | Mfloat32 => Vsingle Float32.zero + | Mfloat64 => Vfloat Float.zero + end. + Inductive load_name : Type := | Plb (**r load byte *) | Plbu (**r load byte unsigned *) @@ -322,9 +332,9 @@ Inductive load_name : Type := . Inductive ld_instruction : Type := - | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) - | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) - | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRO (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRRXS (trap: trapping_mode) (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) | PLoadQRRO (rd: gpreg_q) (ra: ireg) (ofs: offset) | PLoadORRO (rd: gpreg_o) (ra: ireg) (ofs: offset) . @@ -545,6 +555,8 @@ Inductive ar_instruction : Type := | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . +Module PArithCoercions. + Coercion PArithR: arith_name_r >-> Funclass. Coercion PArithRR: arith_name_rr >-> Funclass. Coercion PArithRI32: arith_name_ri32 >-> Funclass. @@ -559,6 +571,8 @@ Coercion PArithARR: arith_name_arr >-> Funclass. Coercion PArithARRI32: arith_name_arri32 >-> Funclass. Coercion PArithARRI64: arith_name_arri64 >-> Funclass. +End PArithCoercions. + Inductive basic : Type := | PArith (i: ar_instruction) | PLoad (i: ld_instruction) @@ -1202,10 +1216,16 @@ Definition eval_offset (ofs: offset) : res ptrofs := OK ofs. (** * load/store *) -Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := +Definition parexec_incorrect_load trap chunk d rsw mw := + match trap with + | TRAP => Stuck + | NOTRAP => Next (rsw#d <- (concrete_default_notrap_load_value chunk)) mw + end. + +Definition parexec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end | _ => Stuck @@ -1250,15 +1270,15 @@ Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a end end. -Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := +Definition parexec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end. -Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := +Definition parexec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with - | None => Stuck + | None => parexec_incorrect_load trap chunk d rsw mw | Some v => Next (rsw#d <- v) mw end. @@ -1271,7 +1291,8 @@ Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: | _ => Stuck end. -Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := +Definition parexec_store_reg + (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := match Mem.storev chunk mr (Val.addl (rsr a) (rsr ro)) (rsr s) with | None => Stuck | Some m' => Next rsw m' @@ -1329,7 +1350,7 @@ Definition load_chunk n := | Pfls => Mfloat32 | Pfld => Mfloat64 end. - + Definition store_chunk n := match n with | Psb => Mint8unsigned @@ -1348,12 +1369,12 @@ Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) := match bi with | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw - | PLoadRRO n d a ofs => parexec_load_offset (load_chunk n) rsr rsw mr mw d a ofs - | PLoadRRR n d a ro => parexec_load_reg (load_chunk n) rsr rsw mr mw d a ro - | PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro - | PLoadQRRO d a ofs => + | PLoad (PLoadRRO trap n d a ofs) => parexec_load_offset trap (load_chunk n) rsr rsw mr mw d a ofs + | PLoad (PLoadRRR trap n d a ro) => parexec_load_reg trap (load_chunk n) rsr rsw mr mw d a ro + | PLoad (PLoadRRRXS trap n d a ro) => parexec_load_regxs trap (load_chunk n) rsr rsw mr mw d a ro + | PLoad (PLoadQRRO d a ofs) => parexec_load_q_offset rsr rsw mr mw d a ofs - | PLoadORRO d a ofs => + | PLoad (PLoadORRO d a ofs) => parexec_load_o_offset rsr rsw mr mw d a ofs | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs @@ -1692,7 +1713,7 @@ Proof. Qed. -Local Hint Resolve parexec_bblock_write_in_order. +Local Hint Resolve parexec_bblock_write_in_order: core. Lemma det_parexec_write_in_order f b rs m rs' m': det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'. |