diff options
Diffstat (limited to 'riscV/BTL_SEsimplify.v')
| -rw-r--r-- | riscV/BTL_SEsimplify.v | 752 |
1 files changed, 738 insertions, 14 deletions
diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index a4a2785a..30468544 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -38,16 +38,16 @@ Definition load_hilo32 (hi lo: int) := fSop (OEluiw hi) fSnil else let fsv := fSop (OEluiw hi) fSnil in - let hl := make_lfsv_single fsv in - fSop (OEaddiw None lo) hl. + 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 hl := make_lfsv_single fsv in - fSop (OEaddil None lo) hl. + let lfsv := make_lfsv_single fsv in + fSop (OEaddil None lo) lfsv. Definition loadimm32 (n: int) := match make_immed32 n with @@ -67,27 +67,27 @@ Definition loadimm64 (n: int64) := Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => - let hl := make_lfsv_single hv1 in - fSop (opimm imm) hl + let lfsv := make_lfsv_single hv1 in + fSop (opimm imm) lfsv | Imm32_pair hi lo => let fsv := load_hilo32 hi lo in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv end. Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := match make_immed64 n with | Imm64_single imm => - let hl := make_lfsv_single hv1 in - fSop (opimm imm) hl + let lfsv := make_lfsv_single hv1 in + fSop (opimm imm) lfsv | Imm64_pair hi lo => let fsv := load_hilo64 hi lo in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv | Imm64_large imm => let fsv := fSop (OEloadli imm) fSnil in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv end. Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). @@ -326,6 +326,113 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt 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 hv1 := ris_sreg_get hrs a1 in + Some (addimm32 hv1 n None) + | Oaddlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (addimm64 hv1 n None) + | Oandimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (andimm32 hv1 n) + | Oandlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (andimm64 hv1 n) + | Oorimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (orimm32 hv1 n) + | Oorlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (orimm64 hv1 n) + | Oxorimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (xorimm32 hv1 n) + | Oxorlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (xorimm64 hv1 n) + | Ocast8signed, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 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 hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 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 hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 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 hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lfsv_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)) lfsv in + let srliw_l := make_lfsv_cmp false hv1 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 hv1 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 hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lfsv_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)) lfsv in + let srlil_l := make_lfsv_cmp false hv1 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 hv1 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. @@ -950,6 +1057,606 @@ Proof. 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 @@ -962,6 +1669,23 @@ 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; |