From ddc17a17408541efa8b23afa3e6ccad1e6ce0b6e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 1 Sep 2021 16:57:12 +0200 Subject: cleanup --- riscV/RTLpathSE_simplify.v | 2077 -------------------------------------------- 1 file changed, 2077 deletions(-) delete mode 100644 riscV/RTLpathSE_simplify.v (limited to 'riscV') diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v deleted file mode 100644 index 2370ad66..00000000 --- a/riscV/RTLpathSE_simplify.v +++ /dev/null @@ -1,2077 +0,0 @@ -Require Import Coqlib Floats Values Memory. -Require Import Integers. -Require Import Op Registers. -Require Import RTLpathSE_theory. -Require Import RTLpathSE_simu_specs. -Require Import Asmgen Asmgenproof1. -Require Import Lia. - -(** Useful functions for conditions/branches expansion *) - -Definition is_inv_cmp_int (cmp: comparison) : bool := - match cmp with | Cle | Cgt => true | _ => false end. - -Definition is_inv_cmp_float (cmp: comparison) : bool := - match cmp with | Cge | Cgt => true | _ => false end. - -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 *) - -Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := - let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in - let lhsv := fScons hvfirst fSnil in - fScons hvsec lhsv. - -Definition make_lhsv_single (hvs: hsval) : list_hsval := - fScons hvs fSnil. - -(** * Expansion functions *) - -(** ** Immediate loads *) - -Definition load_hilo32 (hi lo: int) := - if Int.eq lo Int.zero then - fSop (OEluiw hi) fSnil - else - let hvs := fSop (OEluiw hi) fSnil in - let hl := make_lhsv_single hvs in - fSop (OEaddiw None lo) hl. - -Definition load_hilo64 (hi lo: int64) := - if Int64.eq lo Int64.zero then - fSop (OEluil hi) fSnil - else - let hvs := fSop (OEluil hi) fSnil in - let hl := make_lhsv_single hvs in - fSop (OEaddil None lo) hl. - -Definition loadimm32 (n: int) := - match make_immed32 n with - | Imm32_single imm => - fSop (OEaddiw (Some X0_R) imm) fSnil - | Imm32_pair hi lo => load_hilo32 hi lo - end. - -Definition loadimm64 (n: int64) := - match make_immed64 n with - | Imm64_single imm => - 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) := - 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 hi lo in - let hl := make_lhsv_cmp false hv1 hvs in - fSop op hl - end. - -Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) := - match make_immed64 n with - | Imm64_single imm => - let hl := make_lhsv_single hv1 in - fSop (opimm imm) hl - | Imm64_pair hi lo => - let hvs := load_hilo64 hi lo in - let hl := make_lhsv_cmp false hv1 hvs in - fSop op hl - | Imm64_large imm => - let hvs := fSop (OEloadli imm) fSnil in - let hl := make_lhsv_cmp false hv1 hvs in - fSop op hl - end. - -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 *) - -Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := - match cmp with - | Ceq => fSop (OEseqw optR) lhsv - | Cne => fSop (OEsnew optR) lhsv - | Clt | Cgt => fSop (OEsltw optR) lhsv - | Cle | Cge => - 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) (optR: option oreg) := - match cmp with - | Ceq => fSop (OEsequw optR) lhsv - | Cne => fSop (OEsneuw optR) lhsv - | Clt | Cgt => fSop (OEsltuw optR) lhsv - | Cle | Cge => - 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) (optR: option oreg) := - match cmp with - | Ceq => fSop (OEseql optR) lhsv - | Cne => fSop (OEsnel optR) lhsv - | Clt | Cgt => fSop (OEsltl optR) lhsv - | Cle | Cge => - 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) (optR: option oreg) := - match cmp with - | Ceq => fSop (OEsequl optR) lhsv - | Cne => fSop (OEsneul optR) lhsv - | Clt | Cgt => fSop (OEsltul optR) lhsv - | Cle | Cge => - let hvs := (fSop (OEsltul optR) lhsv) in - let hl := make_lhsv_single hvs in - fSop (OExoriw Int.one) hl - end. - -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 optR := make_optR true is_inv in - let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int32s cmp hl optR - else - match cmp with - | Ceq | Cne => - 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 optR - | Clt => sltimm32 hv1 n - | Cle => - if Int.eq n (Int.repr Int.max_signed) then - 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 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 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 optR := make_optR true is_inv in - let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int32u cmp hl optR - else - match cmp with - | Clt => sltuimm32 hv1 n - | _ => - 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 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 optR := make_optR true is_inv in - let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int64s cmp hl optR - else - match cmp with - | Ceq | Cne => - 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 optR - | Clt => sltimm64 hv1 n - | Cle => - if Int64.eq n (Int64.repr Int64.max_signed) then - 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 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 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 optR := make_optR true is_inv in - let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int64u cmp hl optR - else - match cmp with - | Clt => sltuimm64 hv1 n - | _ => - 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 optR - end. - -Definition cond_float (cmp: comparison) (lhsv: list_hsval) := - match cmp with - | Ceq | Cne => fSop OEfeqd lhsv - | Clt | Cgt => fSop OEfltd lhsv - | Cle | Cge => fSop OEfled lhsv - end. - -Definition cond_single (cmp: comparison) (lhsv: list_hsval) := - match cmp with - | Ceq | Cne => fSop OEfeqs lhsv - | Clt | Cgt => fSop OEflts lhsv - | Cle | Cge => fSop OEfles lhsv - end. - -Definition is_normal_cmp cmp := - match cmp with | Cne => false | _ => true end. - -Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := - let normal := is_normal_cmp cmp in - let normal' := if cnot then negb normal else normal in - let hvs := fn_cond cmp lhsv in - let hl := make_lhsv_single hvs in - if normal' then hvs else fSop (OExoriw Int.one) hl. - -(** ** Branches instructions *) - -Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := - match cmp with - | 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) (optR: option oreg) := - match cmp with - | 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) (optR: option oreg) := - match cmp with - | 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) (optR: option oreg) := - match cmp with - | 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) := - let normal := is_normal_cmp cmp in - 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 X0_R)), hl) else ((CEbeqw (Some X0_R)), hl). - -(** * Target simplifications using "fake" values *) - -Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := - match op, lr with - | Ocmp (Ccomp 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 optR := make_optR false is_inv in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - 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 optR := make_optR false is_inv in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - 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) - | Ocmp (Ccompuimm c imm), a1 :: nil => - let hv1 := fsi_sreg_get hst a1 in - Some (expanse_condimm_int32u c hv1 imm) - | Ocmp (Ccompl 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 optR := make_optR false is_inv in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - 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 optR := make_optR false is_inv in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - 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) - | Ocmp (Ccompluimm c imm), a1 :: nil => - let hv1 := fsi_sreg_get hst a1 in - Some (expanse_condimm_int64u c hv1 imm) - | Ocmp (Ccompf c), f1 :: f2 :: nil => - let hv1 := fsi_sreg_get hst f1 in - let hv2 := fsi_sreg_get hst f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cond_fp false cond_float c lhsv) - | Ocmp (Cnotcompf c), f1 :: f2 :: nil => - let hv1 := fsi_sreg_get hst f1 in - let hv2 := fsi_sreg_get hst f2 in - 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_float c lhsv) - | Ocmp (Ccompfs c), f1 :: f2 :: nil => - let hv1 := fsi_sreg_get hst f1 in - let hv2 := fsi_sreg_get hst f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cond_fp false cond_single c lhsv) - | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => - let hv1 := fsi_sreg_get hst f1 in - let hv2 := fsi_sreg_get hst f2 in - 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. - -Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) := - 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_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_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) - | (Ccompimm 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_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_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_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_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_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_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) - | (Ccomplimm 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_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_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_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_optR false is_inv) in - Some (cond, lhsv)) - | (Ccompf c), (f1 :: f2 :: nil) => - let hv1 := fsi_sreg_get prev f1 in - let hv2 := fsi_sreg_get prev f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cbranch_fp false cond_float c lhsv) - | (Cnotcompf c), (f1 :: f2 :: nil) => - let hv1 := fsi_sreg_get prev f1 in - let hv2 := fsi_sreg_get prev f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cbranch_fp true cond_float c lhsv) - | (Ccompfs c), (f1 :: f2 :: nil) => - let hv1 := fsi_sreg_get prev f1 in - let hv2 := fsi_sreg_get prev f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cbranch_fp false cond_single c lhsv) - | (Cnotcompfs c), (f1 :: f2 :: nil) => - let hv1 := fsi_sreg_get prev f1 in - let hv2 := fsi_sreg_get prev f2 in - let is_inv := is_inv_cmp_float c in - let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (expanse_cbranch_fp true cond_single c lhsv) - | _, _ => None - end. - -(** * Auxiliary lemmas on comparisons *) - -(** ** Signed ints *) - -Lemma xor_neg_ltle_cmp: forall v1 v2, - Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmp; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. -Qed. - -(** ** 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)) = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmpu; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. - 1,2: - unfold Val.cmpu, Val.cmpu_bool; - destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _); - try destruct (eq_block _ _); auto. - unfold Val.cmpu, Val.cmpu_bool; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - -Remark ltu_12_wordsize: - Int.ltu (Int.repr 12) Int.iwordsize = true. -Proof. - unfold Int.iwordsize, Int.zwordsize. simpl. - unfold Int.ltu. apply zlt_true. - rewrite !Int.unsigned_repr; try cbn; try lia. -Qed. - -(** ** Signed longs *) - -Lemma xor_neg_ltle_cmpl: forall v1 v2, - Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.lt _ _); auto. -Qed. - -Lemma xor_neg_ltge_cmpl: forall v1 v2, - Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.lt _ _); auto. -Qed. - -Lemma xorl_zero_eq_cmpl: forall c v1 v2, - c = Ceq \/ c = Cne -> - Some - (Val.maketotal - (option_map Val.of_bool - (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) = - Some (Val.of_optbool (Val.cmpl_bool c v1 v2)). -Proof. - intros. destruct c; inv H; try discriminate; - destruct v1, v2; simpl; auto; - destruct (Int64.eq i i0) eqn:EQ0. - 1,3: - apply Int64.same_if_eq in EQ0; subst; - rewrite Int64.xor_idem; - rewrite Int64.eq_true; trivial. - 1,2: - destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence; - rewrite Int64.xor_is_zero in EQ1; congruence. -Qed. - -Lemma cmp_ltle_add_one: forall v n, - Int.eq n (Int.repr Int.max_signed) = false -> - Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) = - Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))). -Proof. - intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. - unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). - destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by lia. auto. - rewrite zlt_true by lia. auto. - rewrite Int.add_signed. symmetry; apply Int.signed_repr. - specialize (Int.eq_spec n (Int.repr Int.max_signed)). - rewrite EQMAX; simpl; intros. - assert (Int.signed n <> Int.max_signed). - { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); lia. -Qed. - -Lemma cmpl_ltle_add_one: forall v n, - Int64.eq n (Int64.repr Int64.max_signed) = false -> - Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) = - Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))). -Proof. - intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. - unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). - destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by lia. auto. - rewrite zlt_true by lia. auto. - rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. - specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). - rewrite EQMAX; simpl; intros. - assert (Int64.signed n <> Int64.max_signed). - { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); lia. -Qed. - -Remark lt_maxsgn_false_int: forall i, - Int.lt (Int.repr Int.max_signed) i = false. -Proof. - intros; unfold Int.lt. - specialize Int.signed_range with i; intros. - rewrite zlt_false; auto. destruct H. - rewrite Int.signed_repr; try (cbn; lia). - apply Z.le_ge. trivial. -Qed. - -Remark lt_maxsgn_false_long: forall i, - Int64.lt (Int64.repr Int64.max_signed) i = false. -Proof. - intros; unfold Int64.lt. - specialize Int64.signed_range with i; intros. - rewrite zlt_false; auto. destruct H. - rewrite Int64.signed_repr; try (cbn; lia). - apply Z.le_ge. trivial. -Qed. - -(** ** 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)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.ltu _ _); auto. - 1,2: unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. - unfold Val.cmplu; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - -Lemma xor_neg_ltge_cmplu: forall mptr v1 v2, - Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - destruct (Int64.ltu _ _); auto. - 1,2: unfold Val.cmplu; simpl; auto; - destruct (Archi.ptr64); simpl; - try destruct (eq_block _ _); simpl; - try destruct (_ && _); simpl; - try destruct (Ptrofs.cmpu _ _); - try destruct cmp; simpl; auto. - unfold Val.cmplu; simpl; - destruct Archi.ptr64; try destruct (_ || _); simpl; auto; - destruct (eq_block b b0); destruct (eq_block b0 b); - try congruence; - try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); - simpl; auto; - repeat destruct (_ && _); simpl; auto. -Qed. - -(** ** Floats *) - -Lemma xor_neg_eqne_cmpf: forall v1 v2, - Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpf; simpl. - rewrite Float.cmp_ne_eq. - destruct (Float.cmp _ _ _); simpl; auto. -Qed. - -(** ** Singles *) - -Lemma xor_neg_eqne_cmpfs: forall v1 v2, - Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpfs; simpl. - rewrite Float32.cmp_ne_eq. - destruct (Float32.cmp _ _ _); simpl; auto. -Qed. - -(** ** More useful lemmas *) - -Lemma xor_neg_optb: forall v, - Some (Val.xor (Val.of_optbool (option_map negb v)) - (Vint Int.one)) = Some (Val.of_optbool v). -Proof. - intros. - destruct v; simpl; trivial. - destruct b; simpl; auto. -Qed. - -Lemma xor_neg_optb': forall v, - Some (Val.xor (Val.of_optbool v) (Vint Int.one)) = - Some (Val.of_optbool (option_map negb v)). -Proof. - intros. - destruct v; simpl; trivial. - destruct b; simpl; auto. -Qed. - -Lemma optbool_mktotal: forall v, - Val.maketotal (option_map Val.of_bool v) = - Val.of_optbool v. -Proof. - intros. - destruct v; simpl; auto. -Qed. - -(** * 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, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (cond_int32s c - (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)) None)) rs0 m0 = - Some (Val.of_optbool (Val.cmp_bool c v v0)). -Proof. - intros. - unfold cond_int32s in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmp. - - apply xor_neg_ltle_cmp. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmp_bool; trivial. - - replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmp_bool. - rewrite xor_neg_optb; trivial. -Qed. - -Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj - (cond_int32u c - (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)) None)) rs0 m0 = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)). -Proof. - intros. - erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). - 2: eauto. - unfold cond_int32u in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpu. - - apply xor_neg_ltle_cmpu. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpu_bool; trivial. - - replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool. - rewrite xor_neg_optb; trivial. -Qed. - -Lemma simplify_ccompimm_correct ge sp hst st c r n rs0 m m0 v: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj (expanse_condimm_int32s c (fsi_sreg_get hst r) n)) rs0 m0 = - Some (Val.of_optbool (Val.cmp_bool c v (Vint n))). -Proof. - intros. - unfold expanse_condimm_int32s, cond_int32s in *; destruct c; - intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; - try apply Int.same_if_eq in EQIMM; subst; - unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - unfold Val.cmp, zero32. - all: - try apply xor_neg_ltle_cmp; - try apply xor_neg_ltge_cmp; trivial. - 4: - try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst; - try apply Int.same_if_eq in EQMAX; subst; simpl. - 4: - intros; try (specialize make_immed32_sound with (Int.one); - destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. - 6: - intros; try (specialize make_immed32_sound with (Int.add n Int.one); - destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl. - 1,2,3,8,9: - intros; try (specialize make_immed32_sound with (n); - destruct (make_immed32 n) eqn:EQMKI); intros; simpl. - all: - try destruct (Int.eq lo Int.zero) eqn:EQLO32; - try apply Int.same_if_eq in EQLO32; subst; - try erewrite fSop_correct; eauto; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - try rewrite OK2; - try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; - 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; - try destruct (Int.lt _ _) eqn:EQLT; trivial; - try rewrite lt_maxsgn_false_int in EQLT; - simpl; trivial; try discriminate; fail). -Qed. - -Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))). -Proof. - intros. - assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) = - Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)). - erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. - unfold expanse_condimm_int32u, cond_int32u in *; destruct c; - intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; - try apply Int.same_if_eq in EQIMM; subst; - unfold loadimm32, sltuimm32, opimm32, load_hilo32; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; trivial; - try rewrite xor_neg_ltle_cmpu; - unfold Val.cmpu, zero32. - all: - try (specialize make_immed32_sound with n; - destruct (make_immed32 n) eqn:EQMKI); - try destruct (Int.eq lo Int.zero) eqn:EQLO; - try apply Int.same_if_eq in EQLO; subst; - intros; subst; - try erewrite fSop_correct; eauto; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - try rewrite OK2; - rewrite HMEM; - unfold eval_may_undef, Val.cmpu; - destruct v; simpl; auto; - 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 in *; - try rewrite Int.add_zero_l; - try destruct (Int.ltu _ _) eqn:EQLTU; simpl; - 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 - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (cond_int64s c - (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)) None)) rs0 m0 = - Some (Val.of_optbool (Val.cmpl_bool c v v0)). -Proof. - intros. - unfold cond_int64s in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpl. - 1,2,3: rewrite optbool_mktotal; trivial. - - apply xor_neg_ltle_cmpl. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpl_bool; trivial. - rewrite optbool_mktotal; trivial. - - apply xor_neg_ltge_cmpl. -Qed. - -Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj - (cond_int64u c - (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)) None)) rs0 m0 = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)). -Proof. - intros. - erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). - 2: eauto. - unfold cond_int64u in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmplu. - 1,2,3: rewrite optbool_mktotal; trivial. - - apply xor_neg_ltle_cmplu. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmplu_bool; trivial. - rewrite optbool_mktotal; trivial. - - apply xor_neg_ltge_cmplu. -Qed. - -Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 = - Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))). -Proof. - intros. - unfold expanse_condimm_int64s, cond_int64s in *; destruct c; - intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; - try apply Int64.same_if_eq in EQIMM; subst; - unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - unfold Val.cmpl, zero64. - all: - try apply xor_neg_ltle_cmpl; - try apply xor_neg_ltge_cmpl; - try rewrite optbool_mktotal; trivial. - 4: - try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst; - try apply Int64.same_if_eq in EQMAX; subst; simpl. - 4: - intros; try (specialize make_immed32_sound with (Int.one); - destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. - 6: - intros; try (specialize make_immed64_sound with (Int64.add n Int64.one); - destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl. - 1,2,3,9,10: - intros; try (specialize make_immed64_sound with (n); - destruct (make_immed64 n) eqn:EQMKI); intros; simpl. - all: - try destruct (Int.eq lo Int.zero) eqn:EQLO32; - try apply Int.same_if_eq in EQLO32; subst; - try destruct (Int64.eq lo Int64.zero) eqn:EQLO64; - try apply Int64.same_if_eq in EQLO64; subst; - try erewrite fSop_correct; eauto; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - try rewrite OK2; - 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, Val.addl; - try rewrite xorl_zero_eq_cmpl; trivial; - try rewrite optbool_mktotal; trivial; - unfold eval_may_undef, zero32, Val.add; simpl; - destruct v; auto. - 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)); - try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); - 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. -Qed. - -Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall - (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), - seval_smem ge sp (si_smem st) rs0 m0 = Some m -> - Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp - (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 = - Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))). -Proof. - intros. - assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) = - Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)). - erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. - unfold expanse_condimm_int64u, cond_int64u in *; destruct c; - intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; - unfold loadimm64, sltuimm64, opimm64, load_hilo64; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - unfold Val.cmplu, zero64. - (* Simplify make immediate and decompose subcases *) - all: - try (specialize make_immed64_sound with n; - destruct (make_immed64 n) eqn:EQMKI); - try destruct (Int64.eq lo Int64.zero) eqn:EQLO; - try erewrite fSop_correct; eauto; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try rewrite OKv1; - try rewrite OK2; - rewrite HMEM. - (* Ceq, Cne, Clt = itself *) - all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial. - (* Cle = xor (Clt) *) - all: try apply xor_neg_ltle_cmplu; trivial. - (* Others subcases with swap/negation *) - all: - 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; - rewrite Val.swap_cmplu_bool; trivial; fail); - try (replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail); - try rewrite optbool_mktotal; trivial. - all: - try destruct v; simpl; auto; - try destruct (Archi.ptr64); simpl; - try rewrite EQIMM; - try rewrite HMEM; trivial; - try destruct (Int64.ltu _ _); - try rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; - try rewrite <- optbool_mktotal; trivial. -Qed. - -Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (expanse_cond_fp false cond_float c - (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)))) rs0 m0 = - Some (Val.of_optbool (Val.cmpf_bool c v v0)). -Proof. - intros. - unfold expanse_cond_fp in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpf. - - apply xor_neg_eqne_cmpf. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpf_bool; trivial. - - replace (Cle) with (swap_comparison Cge) by auto; - rewrite Val.swap_cmpf_bool; trivial. -Qed. - -Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (expanse_cond_fp true cond_float c - (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)))) rs0 m0 = - Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))). -Proof. - intros. - unfold expanse_cond_fp in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpf. - 1,3,4: apply xor_neg_optb'. - all: destruct v, v0; simpl; trivial. - rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial. - 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl. - 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl. - all: destruct (Float.cmp _ _ _); trivial. -Qed. - -Lemma simplify_ccompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (expanse_cond_fp false cond_single c - (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)))) rs0 m0 = - Some (Val.of_optbool (Val.cmpfs_bool c v v0)). -Proof. - intros. - unfold expanse_cond_fp in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpfs. - - apply xor_neg_eqne_cmpfs. - - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpfs_bool; trivial. - - replace (Cle) with (swap_comparison Cge) by auto; - rewrite Val.swap_cmpfs_bool; trivial. -Qed. - -Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall - (SREG: forall r: positive, - hsi_sreg_eval ge sp hst r rs0 m0 = - seval_sval ge sp (si_sreg st r) rs0 m0) - (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) - (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), - seval_sval ge sp - (hsval_proj - (expanse_cond_fp true cond_single c - (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) - (fsi_sreg_get hst r0)))) rs0 m0 = - Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))). -Proof. - intros. - unfold expanse_cond_fp in *; destruct c; simpl; - erewrite !fsi_sreg_get_correct; eauto; - rewrite OKv1, OKv2; trivial; - unfold Val.cmpfs. - 1,3,4: apply xor_neg_optb'. - all: destruct v, v0; simpl; trivial. - rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial. - 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. - 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. - all: destruct (Float32.cmp _ _ _); trivial. -Qed. - -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) - (REF: hsilocal_refines ge sp rs0 m0 hst st) - (OK0: hsok_local ge sp rs0 m0 hst) - (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args) - (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m), - seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m. -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. - - eapply simplify_ccomp_correct; eauto. - - eapply simplify_ccompu_correct; eauto. - - eapply simplify_ccompimm_correct; eauto. - - eapply simplify_ccompuimm_correct; eauto. - - eapply simplify_ccompl_correct; eauto. - - eapply simplify_ccomplu_correct; eauto. - - eapply simplify_ccomplimm_correct; eauto. - - eapply simplify_ccompluimm_correct; eauto. - - eapply simplify_ccompf_correct; eauto. - - eapply simplify_cnotcompf_correct; eauto. - - eapply simplify_ccompfs_correct; eauto. - - eapply simplify_cnotcompfs_correct; eauto. -Qed. - -Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall - (TARGET: target_cbranch_expanse hst c l = Some (c', l')) - (LREF : hsilocal_refines ge sp rs0 m0 hst st) - (OK: hsok_local ge sp rs0 m0 hst), - seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = - seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. -Proof. - unfold target_cbranch_expanse, seval_condition; simpl. - intros H (LREF & SREF & SREG & SMEM) ?. - destruct c; try congruence; - repeat (destruct l; simpl in H; try congruence). - 1,2,5,6: - destruct c; inv H; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); - 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); - try replace (Cle) with (swap_comparison Cge) by auto; - try replace (Clt) with (swap_comparison Cgt) by auto; - try rewrite Val.swap_cmp_bool; trivial; - try rewrite Val.swap_cmpu_bool; trivial; - try rewrite Val.swap_cmpl_bool; trivial; - try rewrite Val.swap_cmplu_bool; trivial. - 1,2,3,4: - try destruct (Int.eq n Int.zero) eqn: EQIMM; - try apply Int.same_if_eq in EQIMM; - try destruct (Int64.eq n Int64.zero) eqn: EQIMM; - try apply Int64.same_if_eq in EQIMM; - destruct c; inv H; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); - 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); - unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32; - unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64; - intros; try (specialize make_immed32_sound with (n); - destruct (make_immed32 n) eqn:EQMKI); intros; simpl; - intros; try (specialize make_immed64_sound with (n); - destruct (make_immed64 n) eqn:EQMKI); intros; simpl; - try rewrite EQLO; simpl; - try destruct (Int.eq lo Int.zero) eqn:EQLO; - 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 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; - try rewrite Int.add_commut, Int.add_zero_l in EQIMM; - try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM; - try rewrite EQIMM; simpl; - try destruct (Archi.ptr64); trivial. - - 1,2,3,4: - destruct c; inv H; simpl; - try erewrite !fsi_sreg_get_correct; eauto; - try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); - 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); - unfold zero32, zero64, Val.cmpf, Val.cmpfs; - destruct v, v0; simpl; trivial; - try rewrite Float.cmp_ne_eq; - try rewrite Float32.cmp_ne_eq; - try rewrite <- Float.cmp_swap; simpl; - try rewrite <- Float32.cmp_swap; simpl; - try destruct (Float.cmp _ _); simpl; - try destruct (Float32.cmp _ _); simpl; - try rewrite Int.eq_true; simpl; - try rewrite Int.eq_false; try apply Int.one_not_zero; - simpl; trivial. -Qed. -Global Opaque target_op_simplify. -Global Opaque target_cbranch_expanse. -- cgit