From 9b8348b2e3fcbb8394cec54d6fb4e9ac443b21fe Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 8 Mar 2019 11:05:57 +0100 Subject: Refactorized Asmblock exec_basic_instr --- mppa_k1c/Asmblock.v | 224 ++++++++++++++++++++----------------- mppa_k1c/PostpassSchedulingproof.v | 2 +- 2 files changed, 121 insertions(+), 105 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 39b1c45c..f2ad60e6 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1030,119 +1030,135 @@ TODO: subsplitting by instruction type ? Could be useful for expressing auxiliar Variable ge: genv. +Definition arith_eval_r n := + match n with + | Ploadsymbol s ofs => Genv.symbol_address ge s ofs + end +. -Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := - match ai with - | PArithR n d => - match n with - | Ploadsymbol s ofs => rs#d <- (Genv.symbol_address ge s ofs) - end +Definition arith_eval_rr n v := + match n with + | Pmv => v + | Pnegw => Val.neg v + | Pnegl => Val.negl v + | Pcvtl2w => Val.loword v + | Psxwd => Val.longofint v + | Pzxwd => Val.longofintu v + | Pfnegd => Val.negf v + | Pfnegw => Val.negfs v + | Pfabsd => Val.absf v + | Pfabsw => Val.absfs v + | Pfnarrowdw => Val.singleoffloat v + | Pfwidenlwd => Val.floatofsingle v + | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end + | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end + | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end + | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end + | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end + | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end + | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end + | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end + | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end + | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end + end. - | PArithRR n d s => - match n with - | Pmv => rs#d <- (rs#s) - | Pnegw => rs#d <- (Val.neg rs#s) - | Pnegl => rs#d <- (Val.negl rs#s) - | Pcvtl2w => rs#d <- (Val.loword rs#s) - | Psxwd => rs#d <- (Val.longofint rs#s) - | Pzxwd => rs#d <- (Val.longofintu rs#s) - | Pfnegd => rs#d <- (Val.negf rs#s) - | Pfnegw => rs#d <- (Val.negfs rs#s) - | Pfabsd => rs#d <- (Val.absf rs#s) - | Pfabsw => rs#d <- (Val.absfs rs#s) - | Pfnarrowdw => rs#d <- (Val.singleoffloat rs#s) - | Pfwidenlwd => rs#d <- (Val.floatofsingle rs#s) - | Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end) - | Pfloatuwrnsz => rs#d <- (match Val.singleofintu rs#s with Some f => f | _ => Vundef end) - | Pfloatudrnsz => rs#d <- (match Val.floatoflongu rs#s with Some f => f | _ => Vundef end) - | Pfloatudrnsz_i32 => rs#d <- (match Val.floatofintu rs#s with Some f => f | _ => Vundef end) - | Pfloatdrnsz => rs#d <- (match Val.floatoflong rs#s with Some f => f | _ => Vundef end) - | Pfloatdrnsz_i32 => rs#d <- (match Val.floatofint rs#s with Some f => f | _ => Vundef end) - | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) - | Pfixeduwrzz => rs#d <- (match Val.intuofsingle rs#s with Some i => i | _ => Vundef end) - | Pfixeddrzz => rs#d <- (match Val.longoffloat rs#s with Some i => i | _ => Vundef end) - | Pfixeddrzz_i32 => rs#d <- (match Val.intoffloat rs#s with Some i => i | _ => Vundef end) - | Pfixedudrzz => rs#d <- (match Val.longuoffloat rs#s with Some i => i | _ => Vundef end) - | Pfixedudrzz_i32 => rs#d <- (match Val.intuoffloat rs#s with Some i => i | _ => Vundef end) - end +Definition arith_eval_ri32 n i := + match n with + | Pmake => Vint i + end. - | PArithRI32 n d i => - match n with - | Pmake => rs#d <- (Vint i) - end +Definition arith_eval_ri64 n i := + match n with + | Pmakel => Vlong i + end. - | PArithRI64 n d i => - match n with - | Pmakel => rs#d <- (Vlong i) - end +Definition arith_eval_rf32 n i := + match n with + | Pmakefs => Vsingle i + end. - | PArithRF32 n d i => - match n with - | Pmakefs => rs#d <- (Vsingle i) - end +Definition arith_eval_rf64 n i := + match n with + | Pmakef => Vfloat i + end. - | PArithRF64 n d i => - match n with - | Pmakef => rs#d <- (Vfloat i) - end +Definition arith_eval_rrr n v1 v2 := + match n with + | Pcompw c => compare_int c v1 v2 + | Pcompl c => compare_long c v1 v2 + | Pfcompw c => compare_single c v1 v2 + | Pfcompl c => compare_float c v1 v2 + + | Paddw => Val.add v1 v2 + | Psubw => Val.sub v1 v2 + | Pmulw => Val.mul v1 v2 + | Pandw => Val.and v1 v2 + | Porw => Val.or v1 v2 + | Pxorw => Val.xor v1 v2 + | Psrlw => Val.shru v1 v2 + | Psraw => Val.shr v1 v2 + | Psllw => Val.shl v1 v2 + + | Paddl => Val.addl v1 v2 + | Psubl => Val.subl v1 v2 + | Pandl => Val.andl v1 v2 + | Porl => Val.orl v1 v2 + | Pxorl => Val.xorl v1 v2 + | Pmull => Val.mull v1 v2 + | Pslll => Val.shll v1 v2 + | Psrll => Val.shrlu v1 v2 + | Psral => Val.shrl v1 v2 + + | Pfaddd => Val.addf v1 v2 + | Pfaddw => Val.addfs v1 v2 + | Pfsbfd => Val.subf v1 v2 + | Pfsbfw => Val.subfs v1 v2 + | Pfmuld => Val.mulf v1 v2 + | Pfmulw => Val.mulfs v1 v2 + end. - | PArithRRR n d s1 s2 => - match n with - | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2) - | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2) - | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2) - | Pfcompl c => rs#d <- (compare_float c rs#s1 rs#s2) - | Paddw => rs#d <- (Val.add rs#s1 rs#s2) - | Psubw => rs#d <- (Val.sub rs#s1 rs#s2) - | Pmulw => rs#d <- (Val.mul rs#s1 rs#s2) - | Pandw => rs#d <- (Val.and rs#s1 rs#s2) - | Porw => rs#d <- (Val.or rs#s1 rs#s2) - | Pxorw => rs#d <- (Val.xor rs#s1 rs#s2) - | Psrlw => rs#d <- (Val.shru rs#s1 rs#s2) - | Psraw => rs#d <- (Val.shr rs#s1 rs#s2) - | Psllw => rs#d <- (Val.shl rs#s1 rs#s2) - - | Paddl => rs#d <- (Val.addl rs#s1 rs#s2) - | Psubl => rs#d <- (Val.subl rs#s1 rs#s2) - | Pandl => rs#d <- (Val.andl rs#s1 rs#s2) - | Porl => rs#d <- (Val.orl rs#s1 rs#s2) - | Pxorl => rs#d <- (Val.xorl rs#s1 rs#s2) - | Pmull => rs#d <- (Val.mull rs#s1 rs#s2) - | Pslll => rs#d <- (Val.shll rs#s1 rs#s2) - | Psrll => rs#d <- (Val.shrlu rs#s1 rs#s2) - | Psral => rs#d <- (Val.shrl rs#s1 rs#s2) - - | Pfaddd => rs#d <- (Val.addf rs#s1 rs#s2) - | Pfaddw => rs#d <- (Val.addfs rs#s1 rs#s2) - | Pfsbfd => rs#d <- (Val.subf rs#s1 rs#s2) - | Pfsbfw => rs#d <- (Val.subfs rs#s1 rs#s2) - | Pfmuld => rs#d <- (Val.mulf rs#s1 rs#s2) - | Pfmulw => rs#d <- (Val.mulfs rs#s1 rs#s2) - end +Definition arith_eval_rri32 n v i := + match n with + | Pcompiw c => compare_int c v (Vint i) + | Paddiw => Val.add v (Vint i) + | Pandiw => Val.and v (Vint i) + | Poriw => Val.or v (Vint i) + | Pxoriw => Val.xor v (Vint i) + | Psraiw => Val.shr v (Vint i) + | Psrliw => Val.shru v (Vint i) + | Pslliw => Val.shl v (Vint i) + | Psllil => Val.shll v (Vint i) + | Psrlil => Val.shrlu v (Vint i) + | Psrail => Val.shrl v (Vint i) + end. - | PArithRRI32 n d s i => - match n with - | Pcompiw c => rs#d <- (compare_int c rs#s (Vint i)) - | Paddiw => rs#d <- (Val.add rs#s (Vint i)) - | Pandiw => rs#d <- (Val.and rs#s (Vint i)) - | Poriw => rs#d <- (Val.or rs#s (Vint i)) - | Pxoriw => rs#d <- (Val.xor rs#s (Vint i)) - | Psraiw => rs#d <- (Val.shr rs#s (Vint i)) - | Psrliw => rs#d <- (Val.shru rs#s (Vint i)) - | Pslliw => rs#d <- (Val.shl rs#s (Vint i)) - | Psllil => rs#d <- (Val.shll rs#s (Vint i)) - | Psrlil => rs#d <- (Val.shrlu rs#s (Vint i)) - | Psrail => rs#d <- (Val.shrl rs#s (Vint i)) - end +Definition arith_eval_rri64 n v i := + match n with + | Pcompil c => compare_long c v (Vlong i) + | Paddil => Val.addl v (Vlong i) + | Pandil => Val.andl v (Vlong i) + | Poril => Val.orl v (Vlong i) + | Pxoril => Val.xorl v (Vlong i) + end. - | PArithRRI64 n d s i => - match n with - | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i)) - | Paddil => rs#d <- (Val.addl rs#s (Vlong i)) - | Pandil => rs#d <- (Val.andl rs#s (Vlong i)) - | Poril => rs#d <- (Val.orl rs#s (Vlong i)) - | Pxoril => rs#d <- (Val.xorl rs#s (Vlong i)) - end +Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := + match ai with + | PArithR n d => rs#d <- (arith_eval_r n) + + | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s) + + | PArithRI32 n d i => rs#d <- (arith_eval_ri32 n i) + | PArithRI64 n d i => rs#d <- (arith_eval_ri64 n i) + | PArithRF32 n d i => rs#d <- (arith_eval_rf32 n i) + | PArithRF64 n d i => rs#d <- (arith_eval_rf64 n i) + + | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2) + + | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i) + + | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i) end. (** * load/store *) diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f969e5b4..8ad30e81 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -575,7 +575,7 @@ Lemma transf_exec_basic_instr: Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. exploreInst; simpl; auto; try congruence. - 1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence. + 1: unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. 1-10: apply transf_exec_load. all: apply transf_exec_store. Qed. -- cgit