From b995d85e4df6dc505558342331e34a4487719590 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 22 Jul 2021 14:07:16 +0200 Subject: renaming --- riscV/BTL_SEsimplify.v | 102 ++++++++++++++++++++++++------------------------- 1 file changed, 51 insertions(+), 51 deletions(-) (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index 30468544..0cdea5fe 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -64,44 +64,44 @@ Definition loadimm64 (n: int64) := | Imm64_large imm => fSop (OEloadli imm) fSnil end. -Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) := +Definition opimm32 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => - let lfsv := make_lfsv_single hv1 in + let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm32_pair hi lo => let fsv := load_hilo32 hi lo in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. -Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := +Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := match make_immed64 n with | Imm64_single imm => - let lfsv := make_lfsv_single hv1 in + let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm64_pair hi lo => let fsv := load_hilo64 hi lo in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv | Imm64_large imm => let fsv := fSop (OEloadli imm) fSnil in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. -Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). -Definition andimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oand OEandiw. -Definition orimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oor OEoriw. -Definition xorimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oxor OExoriw. -Definition sltimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. -Definition sltuimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. -Definition addimm64 (hv1: sval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). -Definition andimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oandl OEandil. -Definition orimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oorl OEoril. -Definition xorimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oxorl OExoril. -Definition sltimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. -Definition sltuimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. +Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or). +Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw. +Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw. +Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw. +Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw. +Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw. +Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or). +Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil. +Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril. +Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril. +Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil. +Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltul None) OEsltiul. (** ** Comparisons intructions *) Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := @@ -339,59 +339,59 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt | Olongconst n, nil => Some (loadimm64 n) | Oaddimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (addimm32 hv1 n None) + let fsv1 := ris_sreg_get hrs a1 in + Some (addimm32 fsv1 n None) | Oaddlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (addimm64 hv1 n None) + let fsv1 := ris_sreg_get hrs a1 in + Some (addimm64 fsv1 n None) | Oandimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (andimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (andimm32 fsv1 n) | Oandlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (andimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (andimm64 fsv1 n) | Oorimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (orimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (orimm32 fsv1 n) | Oorlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (orimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (orimm64 fsv1 n) | Oxorimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (xorimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (xorimm32 fsv1 n) | Oxorlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (xorimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (xorimm64 fsv1 n) | Ocast8signed, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 24)) hl') | Ocast16signed, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 16)) hl') | Ocast32unsigned, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let cast32s_s := fSop Ocast32signed lfsv in let cast32s_l := make_lfsv_single cast32s_s in let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in let sllil_l := make_lfsv_single sllil_s in Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) | Oshrximm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then - let lhl := make_lfsv_cmp false hv1 hv1 in + let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrx n)) lhl) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in - let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s := fSop (Oshrimm Int.one) addw_l in @@ -401,22 +401,22 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in let sraiw_l := make_lfsv_single sraiw_s in let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in - let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s' := fSop (Oshrimm n) addw_l in let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in Some (fSop (OEmayundef (MUshrx n)) sraiw_l') | Oshrxlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then - let lhl := make_lfsv_cmp false hv1 hv1 in + let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrxl n)) lhl) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in - let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s := fSop (Oshrlimm Int.one) addl_l in @@ -426,7 +426,7 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in let srail_l := make_lfsv_single srail_s in let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in - let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s' := fSop (Oshrlimm n) addl_l in -- cgit