Require Import Coqlib Floats Values Memory. Require Import Integers. Require Import Op Registers. Require Import BTL_SEtheory. Require Import BTL_SEsimuref. Require Import Asmgen Asmgenproof1. (** 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_lfsv_cmp (is_inv: bool) (fsv1 fsv2: sval) : list_sval := let (fsvfirst, fsvsec) := if is_inv then (fsv1, fsv2) else (fsv2, fsv1) in let lfsv := fScons fsvfirst fSnil in fScons fsvsec lfsv. Definition make_lfsv_single (fsv: sval) : list_sval := fScons fsv fSnil. (** * Expansion functions *) (** ** Immediate loads *) Definition load_hilo32 (hi lo: int) := if Int.eq lo Int.zero then fSop (OEluiw hi) fSnil else let fsv := fSop (OEluiw hi) fSnil in let lfsv := make_lfsv_single fsv in fSop (OEaddiw None lo) lfsv. Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then fSop (OEluil hi) fSnil else let fsv := fSop (OEluil hi) fSnil in let lfsv := make_lfsv_single fsv in fSop (OEaddil None lo) lfsv. 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 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm32_pair hi lo => let fsv := load_hilo32 hi lo in let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := match make_immed64 n with | Imm64_single imm => let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm64_pair hi lo => let fsv := load_hilo64 hi lo in let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv | Imm64_large imm => let fsv := fSop (OEloadli imm) fSnil in let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or). Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw. Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw. Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw. Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw. Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw. Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or). Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil. Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril. Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril. Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil. Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltul None) OEsltiul. (** ** Comparisons intructions *) Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := match cmp with | Ceq => fSop (OEseqw optR) lsv | Cne => fSop (OEsnew optR) lsv | Clt | Cgt => fSop (OEsltw optR) lsv | Cle | Cge => let fsv := (fSop (OEsltw optR) lsv) in let lfsv := make_lfsv_single fsv in fSop (OExoriw Int.one) lfsv end. Definition cond_int32u (cmp: comparison) (lsv: list_sval) (optR: option oreg) := match cmp with | Ceq => fSop (OEsequw optR) lsv | Cne => fSop (OEsneuw optR) lsv | Clt | Cgt => fSop (OEsltuw optR) lsv | Cle | Cge => let fsv := (fSop (OEsltuw optR) lsv) in let lfsv := make_lfsv_single fsv in fSop (OExoriw Int.one) lfsv end. Definition cond_int64s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := match cmp with | Ceq => fSop (OEseql optR) lsv | Cne => fSop (OEsnel optR) lsv | Clt | Cgt => fSop (OEsltl optR) lsv | Cle | Cge => let fsv := (fSop (OEsltl optR) lsv) in let lfsv := make_lfsv_single fsv in fSop (OExoriw Int.one) lfsv end. Definition cond_int64u (cmp: comparison) (lsv: list_sval) (optR: option oreg) := match cmp with | Ceq => fSop (OEsequl optR) lsv | Cne => fSop (OEsneul optR) lsv | Clt | Cgt => fSop (OEsltul optR) lsv | Cle | Cge => let fsv := (fSop (OEsltul optR) lsv) in let lfsv := make_lfsv_single fsv in fSop (OExoriw Int.one) lfsv end. Definition expanse_condimm_int32s (cmp: comparison) (fsv1: sval) (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 lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in cond_int32s cmp lfsv optR else match cmp with | Ceq | Cne => let optR := make_optR true is_inv in let fsv := xorimm32 fsv1 n in let lfsv := make_lfsv_cmp false fsv fsv in cond_int32s cmp lfsv optR | Clt => sltimm32 fsv1 n | Cle => if Int.eq n (Int.repr Int.max_signed) then let fsv := loadimm32 Int.one in let lfsv := make_lfsv_cmp false fsv1 fsv in fSop (OEmayundef MUint) lfsv else sltimm32 fsv1 (Int.add n Int.one) | _ => let optR := make_optR false is_inv in let fsv := loadimm32 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in cond_int32s cmp lfsv optR end. Definition expanse_condimm_int32u (cmp: comparison) (fsv1: sval) (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 lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in cond_int32u cmp lfsv optR else match cmp with | Clt => sltuimm32 fsv1 n | _ => let optR := make_optR false is_inv in let fsv := loadimm32 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in cond_int32u cmp lfsv optR end. Definition expanse_condimm_int64s (cmp: comparison) (fsv1: sval) (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 lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in cond_int64s cmp lfsv optR else match cmp with | Ceq | Cne => let optR := make_optR true is_inv in let fsv := xorimm64 fsv1 n in let lfsv := make_lfsv_cmp false fsv fsv in cond_int64s cmp lfsv optR | Clt => sltimm64 fsv1 n | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then let fsv := loadimm32 Int.one in let lfsv := make_lfsv_cmp false fsv1 fsv in fSop (OEmayundef MUlong) lfsv else sltimm64 fsv1 (Int64.add n Int64.one) | _ => let optR := make_optR false is_inv in let fsv := loadimm64 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in cond_int64s cmp lfsv optR end. Definition expanse_condimm_int64u (cmp: comparison) (fsv1: sval) (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 lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in cond_int64u cmp lfsv optR else match cmp with | Clt => sltuimm64 fsv1 n | _ => let optR := make_optR false is_inv in let fsv := loadimm64 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in cond_int64u cmp lfsv optR end. Definition cond_float (cmp: comparison) (lsv: list_sval) := match cmp with | Ceq | Cne => fSop OEfeqd lsv | Clt | Cgt => fSop OEfltd lsv | Cle | Cge => fSop OEfled lsv end. Definition cond_single (cmp: comparison) (lsv: list_sval) := match cmp with | Ceq | Cne => fSop OEfeqs lsv | Clt | Cgt => fSop OEflts lsv | Cle | Cge => fSop OEfles lsv end. Definition is_normal_cmp cmp := match cmp with | Cne => false | _ => true end. Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) := let normal := is_normal_cmp cmp in let normal' := if cnot then negb normal else normal in let fsv := fn_cond cmp lsv in let lfsv := make_lfsv_single fsv in if normal' then fsv else fSop (OExoriw Int.one) lfsv. (** ** 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 (lfsv: list_sval) : (condition * list_sval) := let normal := is_normal_cmp cmp in let normal' := if cnot then negb normal else normal in let fsv := fn_cond cmp lfsv in let lfsv' := make_lfsv_cmp false fsv fsv in if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv'). (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval := match op, lr with | Ocmp (Ccomp c), a1 :: a2 :: nil => let fsv1 := ris_sreg_get hrs a1 in let fsv2 := ris_sreg_get hrs a2 in let is_inv := is_inv_cmp_int c in let optR := make_optR false is_inv in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond_int32s c lfsv optR) | Ocmp (Ccompu c), a1 :: a2 :: nil => let fsv1 := ris_sreg_get hrs a1 in let fsv2 := ris_sreg_get hrs a2 in let is_inv := is_inv_cmp_int c in let optR := make_optR false is_inv in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond_int32u c lfsv optR) | Ocmp (Ccompimm c imm), a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (expanse_condimm_int32s c fsv1 imm) | Ocmp (Ccompuimm c imm), a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (expanse_condimm_int32u c fsv1 imm) | Ocmp (Ccompl c), a1 :: a2 :: nil => let fsv1 := ris_sreg_get hrs a1 in let fsv2 := ris_sreg_get hrs a2 in let is_inv := is_inv_cmp_int c in let optR := make_optR false is_inv in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond_int64s c lfsv optR) | Ocmp (Ccomplu c), a1 :: a2 :: nil => let fsv1 := ris_sreg_get hrs a1 in let fsv2 := ris_sreg_get hrs a2 in let is_inv := is_inv_cmp_int c in let optR := make_optR false is_inv in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond_int64u c lfsv optR) | Ocmp (Ccomplimm c imm), a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (expanse_condimm_int64s c fsv1 imm) | Ocmp (Ccompluimm c imm), a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (expanse_condimm_int64u c fsv1 imm) | Ocmp (Ccompf c), f1 :: f2 :: nil => let fsv1 := ris_sreg_get hrs f1 in let fsv2 := ris_sreg_get hrs f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cond_fp false cond_float c lfsv) | Ocmp (Cnotcompf c), f1 :: f2 :: nil => let fsv1 := ris_sreg_get hrs f1 in let fsv2 := ris_sreg_get hrs f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cond_fp true cond_float c lfsv) | Ocmp (Ccompfs c), f1 :: f2 :: nil => let fsv1 := ris_sreg_get hrs f1 in let fsv2 := ris_sreg_get hrs f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cond_fp false cond_single c lfsv) | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => let fsv1 := ris_sreg_get hrs f1 in let fsv2 := ris_sreg_get hrs f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cond_fp true cond_single c lfsv) | Ofloatconst f, nil => let fsv := loadimm64 (Float.to_bits f) in let lfsv := make_lfsv_single fsv in Some (fSop (Ofloat_of_bits) lfsv) | Osingleconst f, nil => let fsv := loadimm32 (Float32.to_bits f) in let lfsv := make_lfsv_single fsv in Some (fSop (Osingle_of_bits) lfsv) | Ointconst n, nil => Some (loadimm32 n) | Olongconst n, nil => Some (loadimm64 n) | Oaddimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (addimm32 fsv1 n None) | Oaddlimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (addimm64 fsv1 n None) | Oandimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (andimm32 fsv1 n) | Oandlimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (andimm64 fsv1 n) | Oorimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (orimm32 fsv1 n) | Oorlimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (orimm64 fsv1 n) | Oxorimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (xorimm32 fsv1 n) | Oxorlimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in Some (xorimm64 fsv1 n) | Ocast8signed, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 24)) hl') | Ocast16signed, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 16)) hl') | Ocast32unsigned, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in let lfsv := make_lfsv_single fsv1 in let cast32s_s := fSop Ocast32signed lfsv in let cast32s_l := make_lfsv_single cast32s_s in let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in let sllil_l := make_lfsv_single sllil_s in Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) | Oshrximm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrx n)) lhl) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s := fSop (Oshrimm Int.one) addw_l in let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in Some (fSop (OEmayundef (MUshrx n)) sraiw_l) else let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in let sraiw_l := make_lfsv_single sraiw_s in let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s' := fSop (Oshrimm n) addw_l in let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in Some (fSop (OEmayundef (MUshrx n)) sraiw_l') | Oshrxlimm n, a1 :: nil => let fsv1 := ris_sreg_get hrs a1 in let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrxl n)) lhl) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s := fSop (Oshrlimm Int.one) addl_l in let srail_l := make_lfsv_cmp false srail_s srail_s in Some (fSop (OEmayundef (MUshrxl n)) srail_l) else let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in let srail_l := make_lfsv_single srail_s in let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s' := fSop (Oshrlimm n) addl_l in let srail_l' := make_lfsv_cmp false srail_s' srail_s' in Some (fSop (OEmayundef (MUshrxl n)) srail_l') | _, _ => None end. Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := 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 fsv1 := ris_sreg_get prev a1 in let fsv2 := ris_sreg_get prev a2 in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond, lfsv) | (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 fsv1 := ris_sreg_get prev a1 in let fsv2 := ris_sreg_get prev a2 in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond, lfsv) | (Ccompimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let fsv1 := ris_sreg_get prev a1 in (if Int.eq n Int.zero then let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in let cond := transl_cbranch_int32s c (make_optR true is_inv) in Some (cond, lfsv) else let fsv := loadimm32 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in let cond := transl_cbranch_int32s c (make_optR false is_inv) in Some (cond, lfsv)) | (Ccompuimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let fsv1 := ris_sreg_get prev a1 in (if Int.eq n Int.zero then let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in let cond := transl_cbranch_int32u c (make_optR true is_inv) in Some (cond, lfsv) else let fsv := loadimm32 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in let cond := transl_cbranch_int32u c (make_optR false is_inv) in Some (cond, lfsv)) | (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 fsv1 := ris_sreg_get prev a1 in let fsv2 := ris_sreg_get prev a2 in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond, lfsv) | (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 fsv1 := ris_sreg_get prev a1 in let fsv2 := ris_sreg_get prev a2 in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (cond, lfsv) | (Ccomplimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let fsv1 := ris_sreg_get prev a1 in (if Int64.eq n Int64.zero then let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in let cond := transl_cbranch_int64s c (make_optR true is_inv) in Some (cond, lfsv) else let fsv := loadimm64 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in let cond := transl_cbranch_int64s c (make_optR false is_inv) in Some (cond, lfsv)) | (Ccompluimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let fsv1 := ris_sreg_get prev a1 in (if Int64.eq n Int64.zero then let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in let cond := transl_cbranch_int64u c (make_optR true is_inv) in Some (cond, lfsv) else let fsv := loadimm64 n in let lfsv := make_lfsv_cmp is_inv fsv1 fsv in let cond := transl_cbranch_int64u c (make_optR false is_inv) in Some (cond, lfsv)) | (Ccompf c), (f1 :: f2 :: nil) => let fsv1 := ris_sreg_get prev f1 in let fsv2 := ris_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cbranch_fp false cond_float c lfsv) | (Cnotcompf c), (f1 :: f2 :: nil) => let fsv1 := ris_sreg_get prev f1 in let fsv2 := ris_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cbranch_fp true cond_float c lfsv) | (Ccompfs c), (f1 :: f2 :: nil) => let fsv1 := ris_sreg_get prev f1 in let fsv2 := ris_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cbranch_fp false cond_single c lfsv) | (Cnotcompfs c), (f1 :: f2 :: nil) => let fsv1 := ris_sreg_get prev f1 in let fsv2 := ris_sreg_get prev f2 in let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cbranch_fp true cond_single c lfsv) | _, _ => 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. Local Hint Resolve xor_neg_ltle_cmp: core. (** ** 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. Local Hint Resolve xor_neg_ltle_cmpu: core. 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. Local Hint Resolve ltu_12_wordsize: core. (** ** 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. Local Hint Resolve xor_neg_ltle_cmpl: core. 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. Local Hint Resolve xor_neg_ltge_cmpl: core. 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. Local Hint Resolve xorl_zero_eq_cmpl: core. 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. Local Hint Resolve cmp_ltle_add_one: core. 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. Local Hint Resolve cmpl_ltle_add_one: core. 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. Local Hint Resolve lt_maxsgn_false_int: core. 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. Local Hint Resolve lt_maxsgn_false_long: core. (** ** 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. Local Hint Resolve xor_neg_ltle_cmplu: core. 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. Local Hint Resolve xor_neg_ltge_cmplu: core. (** ** 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. Local Hint Resolve xor_neg_eqne_cmpf: core. (** ** 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. Local Hint Resolve xor_neg_eqne_cmpfs: core. (** ** 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. Local Hint Resolve xor_neg_optb: core. 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. Local Hint Resolve xor_neg_optb': core. Lemma optbool_mktotal: forall v, Val.maketotal (option_map Val.of_bool v) = Val.of_optbool v. Proof. intros. destruct v; simpl; auto. Qed. Local Hint Resolve optbool_mktotal: core. (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (cond_int32s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = Some (Val.of_optbool (Val.cmp_bool c v v0)). Proof. intros. unfold cond_int32s in *; destruct c; simpl; erewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.cmp. eauto. - 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; eauto. Qed. Lemma simplify_ccompu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (cond_int32u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)). Proof. intros. unfold cond_int32u in *; destruct c; simpl; rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.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; eauto. Qed. Lemma simplify_ccompimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r v n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v), eval_sval ctx (expanse_condimm_int32s c (hrs r) n) = 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 rewrite !REG_EQ, 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 rewrite !REG_EQ, OKv1; try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; 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 ( 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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r v n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v), eval_sval ctx (expanse_condimm_int32u c (hrs r) n) = Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vint n))). Proof. intros. 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 rewrite !REG_EQ, 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; simpl; try rewrite !REG_EQ, OKv1; 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 destruct (Int.ltu _ _) eqn:EQLTU; simpl; try rewrite EQLTU; simpl; try rewrite EQIMM; try rewrite EQARCH; trivial. Qed. Lemma simplify_ccompl_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (cond_int64s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = Some (Val.of_optbool (Val.cmpl_bool c v v0)). Proof. intros. unfold cond_int64s in *; destruct c; simpl; rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.cmpl. 1,2,3: rewrite optbool_mktotal; trivial. replace (Clt) with (swap_comparison Cgt) by auto; rewrite Val.swap_cmpl_bool; trivial. rewrite optbool_mktotal; trivial. Qed. Lemma simplify_ccomplu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (cond_int64u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)). Proof. intros. unfold cond_int64u in *; destruct c; simpl; rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.cmplu. 1,2,3: rewrite optbool_mktotal; trivial; eauto. replace (Clt) with (swap_comparison Cgt) by auto; rewrite Val.swap_cmplu_bool; trivial. rewrite optbool_mktotal; trivial. Qed. Lemma simplify_ccomplimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r v n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v), eval_sval ctx (expanse_condimm_int64s c (hrs r) n) = 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 rewrite !REG_EQ, 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; simpl; try rewrite !REG_EQ, OKv1; try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst; unfold Val.cmpl, Val.addl; try rewrite optbool_mktotal; trivial; destruct v; auto. all: 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))). all: try rewrite <- cmpl_ltle_add_one; auto; try rewrite ltu_12_wordsize; try rewrite Int.add_commut, Int.add_zero_l in *; simpl; try rewrite lt_maxsgn_false_long; try (rewrite <- H; trivial; fail); simpl; trivial. Qed. Lemma simplify_ccompluimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r v n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v), eval_sval ctx (expanse_condimm_int64u c (hrs r) n) = Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vlong n))). Proof. intros. 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 rewrite !REG_EQ, 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; simpl; try rewrite !REG_EQ, OKv1. (* 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 <- xor_neg_ltle_cmplu; unfold Val.cmplu; trivial; fail); try rewrite optbool_mktotal; trivial. all: try destruct v; simpl; auto; try destruct (Archi.ptr64); simpl; try rewrite EQIMM; try destruct (Int64.ltu _ _); try rewrite <- optbool_mktotal; trivial. Qed. Lemma simplify_ccompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (expanse_cond_fp false cond_float c (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = Some (Val.of_optbool (Val.cmpf_bool c v v0)). Proof. intros. unfold expanse_cond_fp in *; destruct c; simpl; rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (expanse_cond_fp true cond_float c (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))). Proof. intros. unfold expanse_cond_fp in *; destruct c; simpl; rewrite !REG_EQ, 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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (expanse_cond_fp false cond_single c (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = Some (Val.of_optbool (Val.cmpfs_bool c v v0)). Proof. intros. unfold expanse_cond_fp in *; destruct c; simpl; rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) c r r0 v v0: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (OKv1 : eval_sval ctx (st r) = Some v) (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx (expanse_cond_fp true cond_single c (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))). Proof. intros. unfold expanse_cond_fp in *; destruct c; simpl; rewrite !REG_EQ, 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_intconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (H : match lr with | nil => Some (loadimm32 n) | _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Ointconst n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv OK1; inv H; simpl; unfold loadimm32, load_hilo32, make_lfsv_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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (H : match lr with | nil => Some (loadimm64 n) | _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Olongconst n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv OK1; inv H; simpl; unfold loadimm64, load_hilo64, make_lfsv_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_floatconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (H : match lr with | nil => Some (fSop Ofloat_of_bits (make_lfsv_single (loadimm64 (Float.to_bits n)))) | _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Ofloatconst n) args (cm0 ctx). 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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (H : match lr with | nil => Some (fSop Osingle_of_bits (make_lfsv_single (loadimm32 (Float32.to_bits n)))) | _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Osingleconst n) args (cm0 ctx). 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_cast8signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (fSop (Oshrimm (Int.repr 24)) (make_lfsv_single (fSop (Oshlimm (Int.repr 24)) (make_lfsv_single (hrs a1))))) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) Ocast8signed args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; rewrite !REG_EQ. destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. 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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (fSop (Oshrimm (Int.repr 16)) (make_lfsv_single (fSop (Oshlimm (Int.repr 16)) (make_lfsv_single (hrs a1))))) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) Ocast16signed args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; rewrite !REG_EQ. destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. 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_addimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (addimm32 (hrs a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oaddimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl. unfold addimm32, opimm32, load_hilo32, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. apply Int.same_if_eq in EQLO; subst; rewrite Int.add_commut, Int.add_zero_l; rewrite ltu_12_wordsize; trivial. Qed. Lemma simplify_andimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (andimm32 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oandimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl. unfold andimm32, opimm32, load_hilo32, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial. apply Int.same_if_eq in EQLO; subst; rewrite Int.add_commut, Int.add_zero_l; rewrite ltu_12_wordsize; trivial. Qed. Lemma simplify_orimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (orimm32 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oorimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl. unfold orimm32, opimm32, load_hilo32, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial. apply Int.same_if_eq in EQLO; subst; rewrite Int.add_commut, Int.add_zero_l; rewrite ltu_12_wordsize; trivial. Qed. Lemma simplify_xorimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (xorimm32 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oxorimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl. unfold xorimm32, opimm32, load_hilo32, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. apply Int.same_if_eq in EQLO; subst; rewrite Int.add_commut, Int.add_zero_l; rewrite ltu_12_wordsize; trivial. Qed. Lemma simplify_shrximm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => if Int.eq n Int.zero then Some (fSop (OEmayundef (MUshrx n)) (make_lfsv_cmp false (hrs a1) (hrs a1))) else if Int.eq n Int.one then Some (fSop (OEmayundef (MUshrx n)) (make_lfsv_cmp false (fSop (Oshrimm Int.one) (make_lfsv_single (fSop Oadd (make_lfsv_cmp false (hrs a1) (fSop (Oshruimm (Int.repr 31)) (make_lfsv_single (hrs a1))))))) (fSop (Oshrimm Int.one) (make_lfsv_single (fSop Oadd (make_lfsv_cmp false (hrs a1) (fSop (Oshruimm (Int.repr 31)) (make_lfsv_single (hrs a1))))))))) else Some (fSop (OEmayundef (MUshrx n)) (make_lfsv_cmp false (fSop (Oshrimm n) (make_lfsv_single (fSop Oadd (make_lfsv_cmp false (hrs a1) (fSop (Oshruimm (Int.sub Int.iwordsize n)) (make_lfsv_single (fSop (Oshrimm (Int.repr 31)) (make_lfsv_single (hrs a1))))))))) (fSop (Oshrimm n) (make_lfsv_single (fSop Oadd (make_lfsv_cmp false (hrs a1) (fSop (Oshruimm (Int.sub Int.iwordsize n)) (make_lfsv_single (fSop (Oshrimm (Int.repr 31)) (make_lfsv_single (hrs a1))))))))))) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oshrximm n) args (cm0 ctx). 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 H; simpl; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; 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_cast32unsigned_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (fSop (Oshrluimm (Int.repr 32)) (make_lfsv_single (fSop (Oshllimm (Int.repr 32)) (make_lfsv_single (fSop Ocast32signed (make_lfsv_single (hrs a1))))))) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) Ocast32unsigned args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl. rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. 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. Lemma simplify_addlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (addimm64 (hrs a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oaddlimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; unfold addimm64, opimm64, load_hilo64, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. apply Int64.same_if_eq in EQLO; subst. rewrite Int64.add_commut, Int64.add_zero_l; trivial. Qed. Lemma simplify_andlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (andimm64 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oandlimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; unfold andimm64, opimm64, load_hilo64, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial. apply Int64.same_if_eq in EQLO; subst; rewrite Int64.add_commut, Int64.add_zero_l; trivial. Qed. Lemma simplify_orlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (orimm64 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oorlimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; unfold orimm64, opimm64, load_hilo64, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial. apply Int64.same_if_eq in EQLO; subst; rewrite Int64.add_commut, Int64.add_zero_l; trivial. Qed. Lemma simplify_xorlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => Some (xorimm64 (hrs a1) n) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oxorlimm n) args (cm0 ctx). Proof. intros. repeat (destruct lr; simpl; try congruence); simpl in OK1; inv H; simpl; unfold xorimm64, opimm64, load_hilo64, make_lfsv_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; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. apply Int64.same_if_eq in EQLO; subst; rewrite Int64.add_commut, Int64.add_zero_l; trivial. Qed. Lemma simplify_shrxlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) args fsv lr n: forall (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) (H : match lr with | nil => None | a1 :: nil => if Int.eq n Int.zero then Some (fSop (OEmayundef (MUshrxl n)) (make_lfsv_cmp false (hrs a1) (hrs a1))) else if Int.eq n Int.one then Some (fSop (OEmayundef (MUshrxl n)) (make_lfsv_cmp false (fSop (Oshrlimm Int.one) (make_lfsv_single (fSop Oaddl (make_lfsv_cmp false (hrs a1) (fSop (Oshrluimm (Int.repr 63)) (make_lfsv_single (hrs a1))))))) (fSop (Oshrlimm Int.one) (make_lfsv_single (fSop Oaddl (make_lfsv_cmp false (hrs a1) (fSop (Oshrluimm (Int.repr 63)) (make_lfsv_single (hrs a1))))))))) else Some (fSop (OEmayundef (MUshrxl n)) (make_lfsv_cmp false (fSop (Oshrlimm n) (make_lfsv_single (fSop Oaddl (make_lfsv_cmp false (hrs a1) (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) (make_lfsv_single (fSop (Oshrlimm (Int.repr 63)) (make_lfsv_single (hrs a1))))))))) (fSop (Oshrlimm n) (make_lfsv_single (fSop Oaddl (make_lfsv_cmp false (hrs a1) (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) (make_lfsv_single (fSop (Oshrlimm (Int.repr 63)) (make_lfsv_single (hrs a1))))))))))) | a1 :: _ :: _ => None end = Some fsv) (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) (Oshrxlimm n) args (cm0 ctx). 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 H; simpl; rewrite !REG_EQ; destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; 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. (* Main proof of simplification *) Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall (H: target_op_simplify op lr hrs = Some fsv) (REF: ris_refines ctx hrs st) (OK0: ris_ok ctx hrs) (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args), eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx). Proof. unfold target_op_simplify; simpl. intros H ? ? ?; inv REF. 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 (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); try (destruct (eval_sval ctx (si_sreg st r0)) 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 hrs c l ctx st c' l': forall (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) (REF: ris_refines ctx hrs st) (OK: ris_ok ctx hrs), eval_scondition ctx c' l' = eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). Proof. unfold target_cbranch_expanse, eval_scondition; simpl. intros H ? ?. inversion REF. destruct c; try congruence; repeat (destruct l; simpl in H; try congruence). 1,2,5,6: destruct c; inv H; simpl; rewrite !REG_EQ; try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); try (destruct (eval_sval ctx (si_sreg st r0)) 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; rewrite !REG_EQ; try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); try (destruct (eval_sval ctx (si_sreg st r0)) 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; rewrite !REG_EQ; try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); try (destruct (eval_sval ctx (si_sreg st r0)) 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.