From 61289bf034eebcfcaf04e833876d583e47aef659 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 3 Apr 2019 10:34:34 +0200 Subject: Small refactoring and renaming of Stores and Loads --- mppa_k1c/Asmblock.v | 20 ++++++------- mppa_k1c/Asmblockdeps.v | 24 ++++++++-------- mppa_k1c/Asmblockgen.v | 76 ++++++++++++++++++------------------------------- 3 files changed, 50 insertions(+), 70 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 3656b91f..9d7b372e 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -244,7 +244,7 @@ Inductive cf_instruction : Type := . (** Loads **) -Inductive load_name_rro : Type := +Inductive load_name : Type := | Plb (**r load byte *) | Plbu (**r load byte unsigned *) | Plh (**r load half word *) @@ -258,15 +258,15 @@ Inductive load_name_rro : Type := . Inductive ld_instruction : Type := - | PLoadRRO (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset) - | PLoadRRR (i: load_name_rro) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . -Coercion PLoadRRO: load_name_rro >-> Funclass. -Coercion PLoadRRR: load_name_rro >-> Funclass. +Coercion PLoadRRO: load_name >-> Funclass. +Coercion PLoadRRR: load_name >-> Funclass. (** Stores **) -Inductive store_name_rro : Type := +Inductive store_name : Type := | Psb (**r store byte *) | Psh (**r store half byte *) | Psw (**r store int32 *) @@ -278,12 +278,12 @@ Inductive store_name_rro : Type := . Inductive st_instruction : Type := - | PStoreRRO (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset) - | PStoreRRR (i: store_name_rro) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) + | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) . -Coercion PStoreRRO: store_name_rro >-> Funclass. -Coercion PStoreRRR: store_name_rro >-> Funclass. +Coercion PStoreRRO: store_name >-> Funclass. +Coercion PStoreRRR: store_name >-> Funclass. (** Arithmetic instructions **) Inductive arith_name_r : Type := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 7e332895..e038a5ae 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -71,18 +71,18 @@ Coercion OArithRRI32: arith_name_rri32 >-> Funclass. Coercion OArithRRI64: arith_name_rri64 >-> Funclass. Inductive load_op := - | OLoadRRO (n: load_name_rro) (ofs: offset) - | OLoadRRR (n: load_name_rro) + | OLoadRRO (n: load_name) (ofs: offset) + | OLoadRRR (n: load_name) . -Coercion OLoadRRO: load_name_rro >-> Funclass. +Coercion OLoadRRO: load_name >-> Funclass. Inductive store_op := - | OStoreRRO (n: store_name_rro) (ofs: offset) - | OStoreRRR (n: store_name_rro) + | OStoreRRO (n: store_name) (ofs: offset) + | OStoreRRR (n: store_name) . -Coercion OStoreRRO: store_name_rro >-> Funclass. +Coercion OStoreRRO: store_name >-> Funclass. Inductive op_wrap := | Arith (ao: arith_op) @@ -1571,7 +1571,7 @@ Definition string_of_arith (op: arith_op): pstring := | OArithARRI64 n _ => string_of_name_arri64 n end. -Definition string_of_name_lrro (n: load_name_rro) : pstring := +Definition string_of_load_name (n: load_name) : pstring := match n with Plb => "Plb" | Plbu => "Plbu" @@ -1587,11 +1587,11 @@ Definition string_of_name_lrro (n: load_name_rro) : pstring := Definition string_of_load (op: load_op): pstring := match op with - | OLoadRRO n _ => string_of_name_lrro n - | OLoadRRR n => string_of_name_lrro n + | OLoadRRO n _ => string_of_load_name n + | OLoadRRR n => string_of_load_name n end. -Definition string_of_name_srro (n: store_name_rro) : pstring := +Definition string_of_store_name (n: store_name) : pstring := match n with Psb => "Psb" | Psh => "Psh" @@ -1605,8 +1605,8 @@ Definition string_of_name_srro (n: store_name_rro) : pstring := Definition string_of_store (op: store_op) : pstring := match op with - | OStoreRRO n _ => string_of_name_srro n - | OStoreRRR n => string_of_name_srro n + | OStoreRRO n _ => string_of_store_name n + | OStoreRRR n => string_of_store_name n end. Definition string_of_control (op: control_op) : pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 1afb627a..f207b64d 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -792,61 +792,41 @@ Definition transl_memory_access Error(msg "Asmblockgen.transl_memory_access") end. +Definition chunk2load (chunk: memory_chunk) := + match chunk with + | Mint8signed => Plb + | Mint8unsigned => Plbu + | Mint16signed => Plh + | Mint16unsigned => Plhu + | Mint32 => Plw + | Mint64 => Pld + | Mfloat32 => Pfls + | Mfloat64 => Pfld + | Many32 => Plw_a + | Many64 => Pld_a + end. + Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := + do r <- ireg_of dst; + transl_memory_access (chunk2load chunk r) addr args k. + +Definition chunk2store (chunk: memory_chunk) := match chunk with - | Mint8signed => - do r <- ireg_of dst; - transl_memory_access (Plb r) addr args k - | Mint8unsigned => - do r <- ireg_of dst; - transl_memory_access (Plbu r) addr args k - | Mint16signed => - do r <- ireg_of dst; - transl_memory_access (Plh r) addr args k - | Mint16unsigned => - do r <- ireg_of dst; - transl_memory_access (Plhu r) addr args k - | Mint32 => - do r <- ireg_of dst; - transl_memory_access (Plw r) addr args k - | Mint64 => - do r <- ireg_of dst; - transl_memory_access (Pld r) addr args k - | Mfloat32 => - do r <- freg_of dst; - transl_memory_access (Pfls r) addr args k - | Mfloat64 => - do r <- freg_of dst; - transl_memory_access (Pfld r) addr args k - | _ => - Error (msg "Asmblockgen.transl_load") + | Mint8signed | Mint8unsigned => Psb + | Mint16signed | Mint16unsigned => Psh + | Mint32 => Psw + | Mint64 => Psd + | Mfloat32 => Pfss + | Mfloat64 => Pfsd + | Many32 => Psw_a + | Many64 => Psd_a end. Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: bcode) : res bcode := - match chunk with - | Mint8signed | Mint8unsigned => - do r <- ireg_of src; - transl_memory_access (Psb r) addr args k - | Mint16signed | Mint16unsigned => - do r <- ireg_of src; - transl_memory_access (Psh r) addr args k - | Mint32 => - do r <- ireg_of src; - transl_memory_access (Psw r) addr args k - | Mint64 => - do r <- ireg_of src; - transl_memory_access (Psd r) addr args k - | Mfloat32 => - do r <- freg_of src; - transl_memory_access (Pfss r) addr args k - | Mfloat64 => - do r <- freg_of src; - transl_memory_access (Pfsd r) addr args k - | _ => - Error (msg "Asmblockgen.transl_store") - end. + do r <- ireg_of src; + transl_memory_access (chunk2store chunk r) addr args k. (** Function epilogue *) -- cgit