From df9aab806ae8d20393b56e4175e210ed6cff1ef1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 12:48:51 +0200 Subject: a more general way to manage special registers before introducing SP --- riscV/RTLpathSE_simplify.v | 185 +++++++++++++++++++++++---------------------- 1 file changed, 94 insertions(+), 91 deletions(-) (limited to 'riscV/RTLpathSE_simplify.v') 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 -- cgit