diff options
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 1109 |
1 files changed, 939 insertions, 170 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 2669d4bc..2739bc5d 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 *) @@ -27,52 +30,48 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := Definition make_lhsv_single (hvs: hsval) : list_hsval := fScons hvs fSnil. -(** Expansion functions *) +(** * Expansion functions *) -(* Immediate loads *) +(** ** 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 (OEaddiw None 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. + fSop (OEaddil None 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 (OEaddiw (Some X0_R) 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 (OEaddil (Some X0_R) 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 +82,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,55 +91,61 @@ 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 addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). +Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw. +Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw. +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 addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). +Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil. +Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril. 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. -(* Comparisons intructions *) +(** ** 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. @@ -148,83 +153,87 @@ 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 hvs := xorimm32 hv1 n false 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 - | Clt => sltimm32 hv1 n false + cond_int32s cmp hl optR + | 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 MUint) 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 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 false + | Clt => sltuimm32 hv1 n | _ => - let optR0 := make_optR0 false is_inv in - let hvs := loadimm32 hv1 n false 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 - loadimm32 hv1 Int.one true + let hvs := loadimm32 Int.one in + let hl := make_lhsv_cmp false hv1 hvs in + fSop (OEmayundef MUlong) hl else sltimm64 hv1 (Int64.add n Int64.one) | _ => - let optR0 := make_optR0 false is_inv in - let hvs := loadimm64 hv1 n 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 hvs := loadimm64 hv1 n 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) := @@ -251,46 +260,46 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := let hl := make_lhsv_single hvs in if normal' then hvs else fSop (OExoriw Int.one) hl. -(* Branches instructions *) +(** ** 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) := @@ -298,9 +307,9 @@ 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). -(** Target op simplifications using "fake" values *) +(** * Target simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := match op, lr with @@ -308,16 +317,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) @@ -328,16 +337,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) @@ -368,6 +377,112 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let is_inv := is_inv_cmp_float c in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (expanse_cond_fp true cond_single c lhsv) + | Ofloatconst f, nil => + let hvs := loadimm64 (Float.to_bits f) in + let hl := make_lhsv_single hvs in + Some (fSop (Ofloat_of_bits) hl) + | Osingleconst f, nil => + let hvs := loadimm32 (Float32.to_bits f) in + let hl := make_lhsv_single hvs in + Some (fSop (Osingle_of_bits) hl) + | Ointconst n, nil => + Some (loadimm32 n) + | Olongconst n, nil => + Some (loadimm64 n) + | Oaddimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (addimm32 hv1 n None) + | Oaddlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (addimm64 hv1 n None) + | Oandimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (andimm32 hv1 n) + | Oandlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (andimm64 hv1 n) + | Oorimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (orimm32 hv1 n) + | Oorlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (orimm64 hv1 n) + | Oxorimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (xorimm32 hv1 n) + | Oxorlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (xorimm64 hv1 n) + | Ocast8signed, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let hvs := fSop (Oshlimm (Int.repr 24)) hl in + let hl' := make_lhsv_single hvs in + Some (fSop (Oshrimm (Int.repr 24)) hl') + | Ocast16signed, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let hvs := fSop (Oshlimm (Int.repr 16)) hl in + let hl' := make_lhsv_single hvs in + Some (fSop (Oshrimm (Int.repr 16)) hl') + | Ocast32unsigned, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let cast32s_s := fSop Ocast32signed hl in + let cast32s_l := make_lhsv_single cast32s_s in + let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in + let sllil_l := make_lhsv_single sllil_s in + Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) + | Oshrximm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lhsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrx n)) lhl) + else + if Int.eq n Int.one then + let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in + let srliw_l := make_lhsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lhsv_single addw_s in + let sraiw_s := fSop (Oshrimm Int.one) addw_l in + let sraiw_l := make_lhsv_cmp false sraiw_s sraiw_s in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l) + else + let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in + let sraiw_l := make_lhsv_single sraiw_s in + let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in + let srliw_l := make_lhsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lhsv_single addw_s in + let sraiw_s' := fSop (Oshrimm n) addw_l in + let sraiw_l' := make_lhsv_cmp false sraiw_s' sraiw_s' in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l') + | Oshrxlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lhsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrxl n)) lhl) + else + if Int.eq n Int.one then + let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in + let srlil_l := make_lhsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lhsv_single addl_s in + let srail_s := fSop (Oshrlimm Int.one) addl_l in + let srail_l := make_lhsv_cmp false srail_s srail_s in + Some (fSop (OEmayundef (MUshrxl n)) srail_l) + else + let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in + let srail_l := make_lhsv_single srail_s in + let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in + let srlil_l := make_lhsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lhsv_single addl_s in + let srail_s' := fSop (Oshrlimm n) addl_l in + let srail_l' := make_lhsv_cmp false srail_s' srail_s' in + Some (fSop (OEmayundef (MUshrxl n)) srail_l') | _, _ => None end. @@ -375,14 +490,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 @@ -392,35 +507,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 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 + 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 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 + 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 @@ -430,24 +545,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 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 + 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 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 + 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 @@ -476,9 +591,9 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args | _, _ => None end. -(** Auxiliary lemmas on comparisons *) +(** * Auxiliary lemmas on comparisons *) -(* Signed ints *) +(** ** Signed ints *) Lemma xor_neg_ltle_cmp: forall v1 v2, Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = @@ -493,7 +608,7 @@ Proof. auto. Qed. -(* Unsigned ints *) +(** ** Unsigned ints *) Lemma xor_neg_ltle_cmpu: forall mptr v1 v2, Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = @@ -527,7 +642,7 @@ Proof. rewrite !Int.unsigned_repr; try cbn; try lia. Qed. -(* Signed longs *) +(** ** Signed longs *) Lemma xor_neg_ltle_cmpl: forall v1 v2, Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = @@ -623,7 +738,7 @@ Proof. apply Z.le_ge. trivial. Qed. -(* Unsigned longs *) +(** ** Unsigned longs *) Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = @@ -669,7 +784,7 @@ Proof. repeat destruct (_ && _); simpl; auto. Qed. -(* Floats *) +(** ** Floats *) Lemma xor_neg_eqne_cmpf: forall v1 v2, Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = @@ -682,7 +797,7 @@ Proof. destruct (Float.cmp _ _ _); simpl; auto. Qed. -(* Singles *) +(** ** Singles *) Lemma xor_neg_eqne_cmpfs: forall v1 v2, Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = @@ -695,7 +810,7 @@ Proof. destruct (Float32.cmp _ _ _); simpl; auto. Qed. -(* More useful lemmas *) +(** ** More useful lemmas *) Lemma xor_neg_optb: forall v, Some (Val.xor (Val.of_optbool (option_map negb v)) @@ -738,7 +853,7 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. -(* Intermediates lemmas on each expansed instruction *) +(** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall (SREG: forall r: positive, @@ -842,14 +957,16 @@ 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; + unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl; destruct v; auto. all: try rewrite ltu_12_wordsize; try rewrite <- H; try (apply cmp_ltle_add_one; auto); try rewrite Int.add_commut, Int.add_zero_l in *; + try rewrite Int.add_commut; + try rewrite <- H; try rewrite cmp_ltle_add_one; + try rewrite Int.add_zero_l; try ( simpl; trivial; try rewrite Int.xor_is_zero; @@ -894,14 +1011,15 @@ Proof. try rewrite OKv1; try rewrite OK2; rewrite HMEM; - unfold may_undef_int, Val.cmpu; + unfold eval_may_undef, 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 rewrite Int.add_zero_l; 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,17 +1126,16 @@ 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; + unfold eval_may_undef, zero32, Val.add; simpl; destruct v; auto. - 6,7,8: + 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; try rewrite Int64.add_commut, Int64.add_zero_l in *; try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); @@ -1026,12 +1143,17 @@ Proof. try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); try rewrite xor_neg_ltge_cmpl; trivial; try rewrite xor_neg_ltle_cmpl; trivial. + 6: + rewrite <- H; + try apply cmpl_ltle_add_one; auto. all: try rewrite <- H; try apply cmpl_ltle_add_one; auto; + try rewrite <- cmpl_ltle_add_one; auto; try rewrite ltu_12_wordsize; try rewrite Int.add_commut, Int.add_zero_l in *; try rewrite Int64.add_commut, Int64.add_zero_l in *; + try rewrite Int64.add_zero_l; simpl; try rewrite lt_maxsgn_false_long; try (rewrite <- H; trivial; fail); simpl; trivial. @@ -1076,9 +1198,10 @@ Proof. all: try apply xor_neg_ltle_cmplu; trivial. (* Others subcases with swap/negation *) all: - unfold Val.cmplu, may_undef_int, zero64, Val.addl; + unfold Val.cmplu, eval_may_undef, zero64, Val.addl; try apply Int64.same_if_eq in EQLO; subst; try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; + try rewrite Int64.add_zero_l; try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; trivial; fail); try (replace (Clt) with (swap_comparison Cgt) by auto; @@ -1198,7 +1321,645 @@ Proof. all: destruct (Float32.cmp _ _ _); trivial. Qed. -(* Main proof of simplification *) +Lemma simplify_floatconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => + Some + (fSop Ofloat_of_bits + (make_lhsv_single (loadimm64 (Float.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Ofloatconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm64, load_hilo64; simpl; + specialize make_immed64_sound with (Float.to_bits n); + destruct (make_immed64 (Float.to_bits n)) eqn:EQMKI; intros; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + simpl. + - try rewrite Int64.add_commut, Int64.add_zero_l; inv H; + try rewrite Float.of_to_bits; trivial. + - apply Int64.same_if_eq in EQLO; subst. + try rewrite Int64.add_commut, Int64.add_zero_l in H. + rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. +Qed. + +Lemma simplify_singleconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => + Some + (fSop Osingle_of_bits + (make_lhsv_single (loadimm32 (Float32.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Osingleconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm32, load_hilo32; simpl; + specialize make_immed32_sound with (Float32.to_bits n); + destruct (make_immed32 (Float32.to_bits n)) eqn:EQMKI; intros; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + simpl. + { try rewrite Int.add_commut, Int.add_zero_l; inv H; + try rewrite Float32.of_to_bits; trivial. } + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l in H; simpl; + rewrite ltu_12_wordsize; simpl; try rewrite <- H; + try rewrite Float32.of_to_bits; trivial. +Qed. + +Lemma simplify_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n None) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oaddimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold addimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.add (Vint imm) v); rewrite Val.add_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n None) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oaddlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold addimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.addl (Vlong imm) v); rewrite Val.addl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_andimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oandimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold andimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_andlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oandlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold andimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_orimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oorimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold orimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_orlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oorlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold orimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_xorimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (xorimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oxorimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold xorimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.xor (Vint imm) v); rewrite Val.xor_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_xorlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (xorimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oxorlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold xorimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.xorl (Vlong imm) v); rewrite Val.xorl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_intconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => Some (loadimm32 n) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Ointconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm32, load_hilo32, make_lhsv_single; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; try rewrite H; trivial. +Qed. + +Lemma simplify_longconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => Some (loadimm64 n) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Olongconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm64, load_hilo64, make_lhsv_single; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; try rewrite H; trivial. +Qed. + +Lemma simplify_cast8signed_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 24)) + (make_lhsv_single + (fSop (Oshlimm (Int.repr 24)) + (make_lhsv_single (fsi_sreg_get hst a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast8signed args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shr, Val.shl, Val.sign_ext; + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. + rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia. +Qed. + +Lemma simplify_cast16signed_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 16)) + (make_lhsv_single + (fSop (Oshlimm (Int.repr 16)) + (make_lhsv_single (fsi_sreg_get hst a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast16signed args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shr, Val.shl, Val.sign_ext; + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. + rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia. +Qed. + +Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) + else + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oshrximm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence). + assert (A: Int.ltu Int.zero (Int.repr 31) = true) by auto. + assert (B: Int.ltu (Int.repr 31) Int.iwordsize = true) by auto. + assert (C: Int.ltu Int.one Int.iwordsize = true) by auto. + destruct (Int.eq n Int.zero) eqn:EQ0; + destruct (Int.eq n Int.one) eqn:EQ1. + { apply Int.same_if_eq in EQ0. + apply Int.same_if_eq in EQ1; subst. discriminate. } + all: + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; + destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn; + unfold eval_may_undef. + 2,4,6: + unfold Val.shrx in TOTAL; + destruct v; simpl in TOTAL; simpl; try congruence; + try rewrite B; simpl; try rewrite C; simpl; + try destruct (Val.shr _ _); + destruct (Int.ltu n (Int.repr 31)); try congruence. + - destruct v; simpl in TOTAL; try congruence; + apply Int.same_if_eq in EQ0; subst; + rewrite A, Int.shrx_zero in TOTAL; + [auto | cbn; lia]. + - apply Int.same_if_eq in EQ1; subst; + unfold Val.shr, Val.shru, Val.shrx, Val.add; simpl; + destruct v; simpl in *; try discriminate; trivial. + rewrite B, C. + rewrite Int.shrx1_shr in TOTAL; auto. + - exploit Val.shrx_shr_2; eauto. rewrite EQ0. + intros; subst. + destruct v; simpl in *; try discriminate; trivial. + rewrite B in *. + destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate. + simpl in *. + destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate. + replace Int.iwordsize with (Int.repr 32) in * by auto. + rewrite !EQN1. simpl in *. + destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. + rewrite !EQN2. rewrite EQN0. + reflexivity. +Qed. + +Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) + else + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oshrxlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence). + assert (A: Int.ltu Int.zero (Int.repr 63) = true) by auto. + assert (B: Int.ltu (Int.repr 63) Int64.iwordsize' = true) by auto. + assert (C: Int.ltu Int.one Int64.iwordsize' = true) by auto. + destruct (Int.eq n Int.zero) eqn:EQ0; + destruct (Int.eq n Int.one) eqn:EQ1. + { apply Int.same_if_eq in EQ0. + apply Int.same_if_eq in EQ1; subst. discriminate. } + all: + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; + destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn; + unfold eval_may_undef. + 2,4,6: + unfold Val.shrxl in TOTAL; + destruct v; simpl in TOTAL; simpl; try congruence; + try rewrite B; simpl; try rewrite C; simpl; + try destruct (Val.shrl _ _); + destruct (Int.ltu n (Int.repr 63)); try congruence. + - destruct v; simpl in TOTAL; try congruence; + apply Int.same_if_eq in EQ0; subst; + rewrite A, Int64.shrx'_zero in *. + assumption. + - apply Int.same_if_eq in EQ1; subst; + unfold Val.shrl, Val.shrlu, Val.shrxl, Val.addl; simpl; + destruct v; simpl in *; try discriminate; trivial. + rewrite B, C. + rewrite Int64.shrx'1_shr' in TOTAL; auto. + - exploit Val.shrxl_shrl_2; eauto. rewrite EQ0. + intros; subst. + destruct v; simpl in *; try discriminate; trivial. + rewrite B in *. + destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate. + simpl in *. + destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate. + replace Int64.iwordsize' with (Int.repr 64) in * by auto. + rewrite !EQN1. simpl in *. + destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. + rewrite !EQN2. rewrite EQN0. + reflexivity. +Qed. + +Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrluimm (Int.repr 32)) + (make_lhsv_single + (fSop (Oshllimm (Int.repr 32)) + (make_lhsv_single + (fSop Ocast32signed + (make_lhsv_single (fsi_sreg_get hst a1))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast32unsigned args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shrlu, Val.shll, Val.longofint, Val.longofintu. + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. + rewrite A. rewrite Int64.shru'_shl'; auto. + replace (Int.ltu (Int.repr 32) (Int.repr 32)) with (false) by auto. + rewrite cast32unsigned_from_cast32signed. + replace Int64.zwordsize with 64 by auto. + rewrite Int.unsigned_repr; cbn; try lia. + replace (Int.sub (Int.repr 32) (Int.repr 32)) with (Int.zero) by auto. + rewrite Int64.shru'_zero. reflexivity. +Qed. + +(** * Main proof of simplification *) Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (H: target_op_simplify op lr hst = Some fsv) @@ -1211,34 +1972,40 @@ Proof. unfold target_op_simplify; simpl. intros H (LREF & SREF & SREG & SMEM) ? ? ?. destruct op; try congruence. + eapply simplify_intconst_correct; eauto. + eapply simplify_longconst_correct; eauto. + eapply simplify_floatconst_correct; eauto. + eapply simplify_singleconst_correct; eauto. + eapply simplify_cast8signed_correct; eauto. + eapply simplify_cast16signed_correct; eauto. + eapply simplify_addimm_correct; eauto. + eapply simplify_andimm_correct; eauto. + eapply simplify_orimm_correct; eauto. + eapply simplify_xorimm_correct; eauto. + eapply simplify_shrximm_correct; eauto. + eapply simplify_cast32unsigned_correct; eauto. + eapply simplify_addlimm_correct; eauto. + eapply simplify_andlimm_correct; eauto. + eapply simplify_orlimm_correct; eauto. + eapply simplify_xorlimm_correct; eauto. + eapply simplify_shrxlimm_correct; eauto. + (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); simpl in OK1; try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); inv H; inv OK1. - (* Ccomp *) - eapply simplify_ccomp_correct; eauto. - (* Ccompu *) - eapply simplify_ccompu_correct; eauto. - (* Ccompimm *) - eapply simplify_ccompimm_correct; eauto. - (* Ccompuimm *) - eapply simplify_ccompuimm_correct; eauto. - (* Ccompl *) - eapply simplify_ccompl_correct; eauto. - (* Ccomplu *) - eapply simplify_ccomplu_correct; eauto. - (* Ccomplimm *) - eapply simplify_ccomplimm_correct; eauto. - (* Ccompluimm *) - eapply simplify_ccompluimm_correct; eauto. - (* Ccompf *) - eapply simplify_ccompf_correct; eauto. - (* Cnotcompf *) - eapply simplify_cnotcompf_correct; eauto. - (* Ccompfs *) - eapply simplify_ccompfs_correct; eauto. - (* Cnotcompfs *) - eapply simplify_cnotcompfs_correct; eauto. Qed. @@ -1286,13 +2053,15 @@ 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 eval_may_undef; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; simpl; trivial; try destruct v; try rewrite H; try rewrite ltu_12_wordsize; try rewrite EQLO; try rewrite Int.add_commut, Int.add_zero_l; try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l; auto; simpl; try rewrite H in EQIMM; try rewrite EQLO in EQIMM; |