renaming

1 files changed, 51 insertions, 51 deletions

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