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.v90
1 files changed, 44 insertions, 46 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 6a0297e9..0180c0dd 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -31,48 +31,44 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval :=
(* Immediate loads *)
-Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) :=
- let hl := make_lhsv_single hv1 in
+Definition load_hilo32 (hi lo: int) :=
if Int.eq lo Int.zero then
- fSop (OEluiw hi is_long) hl
+ fSop (OEluiw hi) fSnil
else
- let hvs := fSop (OEluiw hi is_long) hl in
- let hl' := make_lhsv_single hvs in
- fSop (Oaddimm lo) hl'.
+ let hvs := fSop (OEluiw hi) fSnil in
+ let hl := make_lhsv_single hvs in
+ fSop (Oaddimm lo) hl.
-Definition load_hilo64 (hv1: hsval) (hi lo: int64) :=
- let hl := make_lhsv_single hv1 in
+Definition load_hilo64 (hi lo: int64) :=
if Int64.eq lo Int64.zero then
- fSop (OEluil hi) hl
+ fSop (OEluil hi) fSnil
else
- let hvs := fSop (OEluil hi) hl in
+ let hvs := fSop (OEluil hi) fSnil in
let hl := make_lhsv_single hvs in
fSop (Oaddlimm lo) hl.
-Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) :=
+Definition loadimm32 (n: int) :=
match make_immed32 n with
| Imm32_single imm =>
- let hl := make_lhsv_single hv1 in
- fSop (OEaddiwr0 imm is_long) hl
- | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long
+ fSop (OEaddiwr0 imm) fSnil
+ | Imm32_pair hi lo => load_hilo32 hi lo
end.
-Definition loadimm64 (hv1: hsval) (n: int64) :=
+Definition loadimm64 (n: int64) :=
match make_immed64 n with
| Imm64_single imm =>
- let hl := make_lhsv_single hv1 in
- fSop (OEaddilr0 imm) hl
- | Imm64_pair hi lo => load_hilo64 hv1 hi lo
+ fSop (OEaddilr0 imm) fSnil
+ | Imm64_pair hi lo => load_hilo64 hi lo
| Imm64_large imm => fSop (OEloadli imm) fSnil
end.
-Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) :=
+Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
match make_immed32 n with
| Imm32_single imm =>
let hl := make_lhsv_single hv1 in
fSop (opimm imm) hl
| Imm32_pair hi lo =>
- let hvs := load_hilo32 hv1 hi lo is_long in
+ let hvs := load_hilo32 hi lo in
let hl := make_lhsv_cmp false hv1 hvs in
fSop op hl
end.
@@ -83,7 +79,7 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
let hl := make_lhsv_single hv1 in
fSop (opimm imm) hl
| Imm64_pair hi lo =>
- let hvs := load_hilo64 hv1 hi lo in
+ let hvs := load_hilo64 hi lo in
let hl := make_lhsv_cmp false hv1 hvs in
fSop op hl
| Imm64_large imm =>
@@ -92,9 +88,9 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
fSop op hl
end.
-Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long.
-Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long.
-Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long.
+Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
+Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
@@ -155,17 +151,19 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
match cmp with
| Ceq | Cne =>
let optR0 := make_optR0 true is_inv in
- let hvs := xorimm32 hv1 n false in
+ let hvs := xorimm32 hv1 n in
let hl := make_lhsv_cmp false hvs hvs in
cond_int32s cmp hl optR0
- | Clt => sltimm32 hv1 n false
+ | Clt => sltimm32 hv1 n
| Cle =>
if Int.eq n (Int.repr Int.max_signed) then
- loadimm32 hv1 Int.one false
- else sltimm32 hv1 (Int.add n Int.one) false
+ let hvs := loadimm32 Int.one in
+ let hl := make_lhsv_cmp false hv1 hvs in
+ fSop (OEmayundef false) hl
+ else sltimm32 hv1 (Int.add n Int.one)
| _ =>
let optR0 := make_optR0 false is_inv in
- let hvs := loadimm32 hv1 n false in
+ let hvs := loadimm32 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
cond_int32s cmp hl optR0
end.
@@ -178,10 +176,10 @@ Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
cond_int32u cmp hl optR0
else
match cmp with
- | Clt => sltuimm32 hv1 n false
+ | Clt => sltuimm32 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
- let hvs := loadimm32 hv1 n false in
+ let hvs := loadimm32 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
cond_int32u cmp hl optR0
end.
@@ -202,11 +200,13 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
| Clt => sltimm64 hv1 n
| Cle =>
if Int64.eq n (Int64.repr Int64.max_signed) then
- loadimm32 hv1 Int.one true
+ let hvs := loadimm32 Int.one in
+ let hl := make_lhsv_cmp false hv1 hvs in
+ fSop (OEmayundef true) hl
else sltimm64 hv1 (Int64.add n Int64.one)
| _ =>
let optR0 := make_optR0 false is_inv in
- let hvs := loadimm64 hv1 n in
+ let hvs := loadimm64 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
cond_int64s cmp hl optR0
end.
@@ -222,7 +222,7 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
| Clt => sltuimm64 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
- let hvs := loadimm64 hv1 n in
+ let hvs := loadimm64 n in
let hl := make_lhsv_cmp is_inv hv1 hvs in
cond_int64u cmp hl optR0
end.
@@ -395,7 +395,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
Some (cond, lhsv)
else
- let hvs := loadimm32 hv1 n false in
+ 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
Some (cond, lhsv))
@@ -407,7 +407,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
Some (cond, lhsv)
else
- let hvs := loadimm32 hv1 n false in
+ 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
Some (cond, lhsv))
@@ -433,7 +433,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
Some (cond, lhsv)
else
- let hvs := loadimm64 hv1 n in
+ 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
Some (cond, lhsv))
@@ -445,7 +445,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
Some (cond, lhsv)
else
- let hvs := loadimm64 hv1 n in
+ 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
Some (cond, lhsv))
@@ -842,7 +842,6 @@ Proof.
try rewrite OKv1;
try rewrite OK2;
try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst;
- try rewrite xor_neg_ltle_cmp; trivial;
unfold Val.cmp, may_undef_int, zero32, Val.add; simpl;
destruct v; auto.
all:
@@ -896,12 +895,12 @@ Proof.
rewrite HMEM;
unfold may_undef_int, Val.cmpu;
destruct v; simpl; auto;
- try rewrite EQIMM; try destruct (Archi.ptr64); simpl;
+ try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
try rewrite ltu_12_wordsize; trivial;
- try rewrite Int.add_commut, Int.add_zero_l;
+ try rewrite Int.add_commut, Int.add_zero_l in *;
try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
- try rewrite EQLTU; simpl;
- trivial.
+ try rewrite EQLTU; simpl; try rewrite EQIMM;
+ try rewrite EQARCH; trivial.
Qed.
Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall
@@ -1008,12 +1007,11 @@ Proof.
try erewrite !fsi_sreg_get_correct; eauto;
try rewrite OKv1;
try rewrite OK2;
- unfold may_undef_luil;
try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
try fold (Val.cmpl Clt v (Vlong imm));
try rewrite xor_neg_ltge_cmpl; trivial;
try rewrite xor_neg_ltle_cmpl; trivial;
- unfold Val.cmpl, may_undef_luil, Val.addl;
+ unfold Val.cmpl, Val.addl;
try rewrite xorl_zero_eq_cmpl; trivial;
try rewrite optbool_mktotal; trivial;
unfold may_undef_int, zero32, Val.add; simpl;
@@ -1286,7 +1284,7 @@ Proof.
try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
try apply Int.same_if_eq in EQLO; simpl; trivial;
try apply Int64.same_if_eq in EQLO; simpl; trivial;
- unfold may_undef_int, may_undef_luil;
+ unfold may_undef_int;
try erewrite !fsi_sreg_get_correct; eauto;
try rewrite OKv1; simpl; trivial;
try destruct v; try rewrite H;
generated by cgit (git 2.34.1) at 2024-06-12 06:50:21 +0000