aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/RTLpathSE_simplify.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
-rw-r--r--riscV/RTLpathSE_simplify.v185
1 files changed, 94 insertions, 91 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 08c1a6a0..5b44caba 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -14,8 +14,11 @@ Definition is_inv_cmp_int (cmp: comparison) : bool :=
Definition is_inv_cmp_float (cmp: comparison) : bool :=
match cmp with | Cge | Cgt => true | _ => false end.
-Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
- if is_x0 then Some is_inv else None.
+Definition make_optR (is_x0 is_inv: bool) : option oreg :=
+ if is_x0 then
+ (if is_inv then Some (X0_L)
+ else Some (X0_R))
+ else None.
(** Functions to manage lists of "fake" values *)
@@ -103,46 +106,46 @@ Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEs
(* Comparisons intructions *)
-Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
- | Ceq => fSop (OEseqw optR0) lhsv
- | Cne => fSop (OEsnew optR0) lhsv
- | Clt | Cgt => fSop (OEsltw optR0) lhsv
+ | Ceq => fSop (OEseqw optR) lhsv
+ | Cne => fSop (OEsnew optR) lhsv
+ | Clt | Cgt => fSop (OEsltw optR) lhsv
| Cle | Cge =>
- let hvs := (fSop (OEsltw optR0) lhsv) in
+ let hvs := (fSop (OEsltw optR) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
-Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
- | Ceq => fSop (OEsequw optR0) lhsv
- | Cne => fSop (OEsneuw optR0) lhsv
- | Clt | Cgt => fSop (OEsltuw optR0) lhsv
+ | Ceq => fSop (OEsequw optR) lhsv
+ | Cne => fSop (OEsneuw optR) lhsv
+ | Clt | Cgt => fSop (OEsltuw optR) lhsv
| Cle | Cge =>
- let hvs := (fSop (OEsltuw optR0) lhsv) in
+ let hvs := (fSop (OEsltuw optR) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
-Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
- | Ceq => fSop (OEseql optR0) lhsv
- | Cne => fSop (OEsnel optR0) lhsv
- | Clt | Cgt => fSop (OEsltl optR0) lhsv
+ | Ceq => fSop (OEseql optR) lhsv
+ | Cne => fSop (OEsnel optR) lhsv
+ | Clt | Cgt => fSop (OEsltl optR) lhsv
| Cle | Cge =>
- let hvs := (fSop (OEsltl optR0) lhsv) in
+ let hvs := (fSop (OEsltl optR) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
-Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
- | Ceq => fSop (OEsequl optR0) lhsv
- | Cne => fSop (OEsneul optR0) lhsv
- | Clt | Cgt => fSop (OEsltul optR0) lhsv
+ | Ceq => fSop (OEsequl optR) lhsv
+ | Cne => fSop (OEsneul optR) lhsv
+ | Clt | Cgt => fSop (OEsltul optR) lhsv
| Cle | Cge =>
- let hvs := (fSop (OEsltul optR0) lhsv) in
+ let hvs := (fSop (OEsltul optR) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
@@ -150,16 +153,16 @@ Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool)
Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hl := make_lhsv_cmp is_inv hv1 hv1 in
- cond_int32s cmp hl optR0
+ cond_int32s cmp hl optR
else
match cmp with
| Ceq | Cne =>
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hvs := xorimm32 hv1 n in
let hl := make_lhsv_cmp false hvs hvs in
- cond_int32s cmp hl optR0
+ cond_int32s cmp hl optR
| Clt => sltimm32 hv1 n
| Cle =>
if Int.eq n (Int.repr Int.max_signed) then
@@ -168,41 +171,41 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
fSop (OEmayundef MUint) hl
else sltimm32 hv1 (Int.add n Int.one)
| _ =>
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let hvs := loadimm32 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
- cond_int32s cmp hl optR0
+ cond_int32s cmp hl optR
end.
Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hl := make_lhsv_cmp is_inv hv1 hv1 in
- cond_int32u cmp hl optR0
+ cond_int32u cmp hl optR
else
match cmp with
| Clt => sltuimm32 hv1 n
| _ =>
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let hvs := loadimm32 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
- cond_int32u cmp hl optR0
+ cond_int32u cmp hl optR
end.
Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hl := make_lhsv_cmp is_inv hv1 hv1 in
- cond_int64s cmp hl optR0
+ cond_int64s cmp hl optR
else
match cmp with
| Ceq | Cne =>
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hvs := xorimm64 hv1 n in
let hl := make_lhsv_cmp false hvs hvs in
- cond_int64s cmp hl optR0
+ cond_int64s cmp hl optR
| Clt => sltimm64 hv1 n
| Cle =>
if Int64.eq n (Int64.repr Int64.max_signed) then
@@ -211,26 +214,26 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
fSop (OEmayundef MUlong) hl
else sltimm64 hv1 (Int64.add n Int64.one)
| _ =>
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let hvs := loadimm64 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
- cond_int64s cmp hl optR0
+ cond_int64s cmp hl optR
end.
Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
- let optR0 := make_optR0 true is_inv in
+ let optR := make_optR true is_inv in
let hl := make_lhsv_cmp is_inv hv1 hv1 in
- cond_int64u cmp hl optR0
+ cond_int64u cmp hl optR
else
match cmp with
| Clt => sltuimm64 hv1 n
| _ =>
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let hvs := loadimm64 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
- cond_int64u cmp hl optR0
+ cond_int64u cmp hl optR
end.
Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
@@ -259,44 +262,44 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
(* Branches instructions *)
-Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
+Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
match cmp with
- | Ceq => CEbeqw optR0
- | Cne => CEbnew optR0
- | Clt => CEbltw optR0
- | Cle => CEbgew optR0
- | Cgt => CEbltw optR0
- | Cge => CEbgew optR0
+ | Ceq => CEbeqw optR
+ | Cne => CEbnew optR
+ | Clt => CEbltw optR
+ | Cle => CEbgew optR
+ | Cgt => CEbltw optR
+ | Cge => CEbgew optR
end.
-Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) :=
+Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) :=
match cmp with
- | Ceq => CEbequw optR0
- | Cne => CEbneuw optR0
- | Clt => CEbltuw optR0
- | Cle => CEbgeuw optR0
- | Cgt => CEbltuw optR0
- | Cge => CEbgeuw optR0
+ | Ceq => CEbequw optR
+ | Cne => CEbneuw optR
+ | Clt => CEbltuw optR
+ | Cle => CEbgeuw optR
+ | Cgt => CEbltuw optR
+ | Cge => CEbgeuw optR
end.
-Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) :=
+Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) :=
match cmp with
- | Ceq => CEbeql optR0
- | Cne => CEbnel optR0
- | Clt => CEbltl optR0
- | Cle => CEbgel optR0
- | Cgt => CEbltl optR0
- | Cge => CEbgel optR0
+ | Ceq => CEbeql optR
+ | Cne => CEbnel optR
+ | Clt => CEbltl optR
+ | Cle => CEbgel optR
+ | Cgt => CEbltl optR
+ | Cge => CEbgel optR
end.
-Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
+Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) :=
match cmp with
- | Ceq => CEbequl optR0
- | Cne => CEbneul optR0
- | Clt => CEbltul optR0
- | Cle => CEbgeul optR0
- | Cgt => CEbltul optR0
- | Cge => CEbgeul optR0
+ | Ceq => CEbequl optR
+ | Cne => CEbneul optR
+ | Clt => CEbltul optR
+ | Cle => CEbgeul optR
+ | Cgt => CEbltul optR
+ | Cge => CEbgeul optR
end.
Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) :=
@@ -304,7 +307,7 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con
let normal' := if cnot then negb normal else normal in
let hvs := fn_cond cmp lhsv in
let hl := make_lhsv_cmp false hvs hvs in
- if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl).
+ if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl).
(** Add pointer expansion *)
@@ -325,16 +328,16 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let hv1 := fsi_sreg_get hst a1 in
let hv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
- Some (cond_int32s c lhsv optR0)
+ Some (cond_int32s c lhsv optR)
| Ocmp (Ccompu c), a1 :: a2 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
let hv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
- Some (cond_int32u c lhsv optR0)
+ Some (cond_int32u c lhsv optR)
| Ocmp (Ccompimm c imm), a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (expanse_condimm_int32s c hv1 imm)
@@ -345,16 +348,16 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let hv1 := fsi_sreg_get hst a1 in
let hv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
- Some (cond_int64s c lhsv optR0)
+ Some (cond_int64s c lhsv optR)
| Ocmp (Ccomplu c), a1 :: a2 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
let hv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
- let optR0 := make_optR0 false is_inv in
+ let optR := make_optR false is_inv in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
- Some (cond_int64u c lhsv optR0)
+ Some (cond_int64u c lhsv optR)
| Ocmp (Ccomplimm c imm), a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (expanse_condimm_int64s c hv1 imm)
@@ -497,14 +500,14 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
match cond, args with
| (Ccomp c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in
- let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int32s c (make_optR false is_inv) in
let hv1 := fsi_sreg_get prev a1 in
let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
Some (cond, lhsv)
| (Ccompu c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in
- let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int32u c (make_optR false is_inv) in
let hv1 := fsi_sreg_get prev a1 in
let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
@@ -514,35 +517,35 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let hv1 := fsi_sreg_get prev a1 in
(if Int.eq n Int.zero then
let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
- let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
+ let cond := transl_cbranch_int32s c (make_optR true is_inv) in
Some (cond, lhsv)
else
let hvs := loadimm32 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in
- let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int32s c (make_optR false is_inv) in
Some (cond, lhsv))
| (Ccompuimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
let hv1 := fsi_sreg_get prev a1 in
(if Int.eq n Int.zero then
let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
- let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
+ let cond := transl_cbranch_int32u c (make_optR true is_inv) in
Some (cond, lhsv)
else
let hvs := loadimm32 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in
- let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int32u c (make_optR false is_inv) in
Some (cond, lhsv))
| (Ccompl c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in
- let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int64s c (make_optR false is_inv) in
let hv1 := fsi_sreg_get prev a1 in
let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
Some (cond, lhsv)
| (Ccomplu c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in
- let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int64u c (make_optR false is_inv) in
let hv1 := fsi_sreg_get prev a1 in
let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
@@ -552,24 +555,24 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let hv1 := fsi_sreg_get prev a1 in
(if Int64.eq n Int64.zero then
let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
- let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
+ let cond := transl_cbranch_int64s c (make_optR true is_inv) in
Some (cond, lhsv)
else
let hvs := loadimm64 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in
- let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int64s c (make_optR false is_inv) in
Some (cond, lhsv))
| (Ccompluimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
let hv1 := fsi_sreg_get prev a1 in
(if Int64.eq n Int64.zero then
let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
- let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
+ let cond := transl_cbranch_int64u c (make_optR true is_inv) in
Some (cond, lhsv)
else
let hvs := loadimm64 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in
- let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
+ let cond := transl_cbranch_int64u c (make_optR false is_inv) in
Some (cond, lhsv))
| (Ccompf c), (f1 :: f2 :: nil) =>
let hv1 := fsi_sreg_get prev f1 in
generated by cgit (git 2.34.1) at 2024-05-19 22:44:45 +0000