diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-06 13:51:51 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-06 13:51:51 +0200 |
commit | 906a8553570ed17a8e90831c1d1df18d76e94154 (patch) | |
tree | b8a1ecf6d8fe96aa4ece54424177cc4662950b82 /mppa_k1c/Asmvliw.v | |
parent | 20fed399133f75a10599082c9f75d9a519efff52 (diff) | |
download | compcert-kvx-906a8553570ed17a8e90831c1d1df18d76e94154.tar.gz compcert-kvx-906a8553570ed17a8e90831c1d1df18d76e94154.zip |
simplification semantique+preuve des load_q+load_o
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
-rw-r--r-- | mppa_k1c/Asmvliw.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 3fbc048c..3bef1a5c 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1186,9 +1186,9 @@ Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a: ireg) (ofs: offset) := let (rd0, rd1) := gpreg_q_expand d in - if ireg_eq rd0 a - then Stuck - else +(* NB: By construction of [gpreg_q], register rd0 and rd1 are distinct, thus, the register writes cannot overlap. + But we do not need to express/prove this in the semantics. +*) match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with | None => Stuck | Some v0 => @@ -1201,10 +1201,10 @@ Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a: ireg) (ofs: offset) := match gpreg_o_expand d with | (rd0, rd1, rd2, rd3) => - if (ireg_eq rd0 a) || (ireg_eq rd1 a) || (ireg_eq rd2 a) - then Stuck - else - match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with +(* NB: By construction of [gpreg_o], the four destination registers are pairwise distinct, thus, the register writes cannot overlap. + But we do not need to express/prove this in the semantics. +*) + match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with | None => Stuck | Some v0 => match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with |