From 9ce1b23f6361d8070490df1269a7bc53aa215efb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 12:16:27 +0200 Subject: expansions btl proofs --- riscV/BTL_SEsimplify.v | 999 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 998 insertions(+), 1 deletion(-) mode change 120000 => 100644 riscV/BTL_SEsimplify.v (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v deleted file mode 120000 index f190e6d5..00000000 --- a/riscV/BTL_SEsimplify.v +++ /dev/null @@ -1 +0,0 @@ -../aarch64/BTL_SEsimplify.v \ No newline at end of file diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v new file mode 100644 index 00000000..a4a2785a --- /dev/null +++ b/riscV/BTL_SEsimplify.v @@ -0,0 +1,998 @@ +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 hl := make_lfsv_single fsv in + fSop (OEaddiw None lo) hl. + +Definition load_hilo64 (hi lo: int64) := + if Int64.eq lo Int64.zero then + fSop (OEluil hi) fSnil + else + let fsv := fSop (OEluil hi) fSnil in + let hl := make_lfsv_single fsv in + fSop (OEaddil None lo) hl. + +Definition loadimm32 (n: int) := + match make_immed32 n with + | Imm32_single imm => + fSop (OEaddiw (Some X0_R) imm) fSnil + | Imm32_pair hi lo => load_hilo32 hi lo + end. + +Definition loadimm64 (n: int64) := + match make_immed64 n with + | Imm64_single imm => + fSop (OEaddil (Some X0_R) imm) fSnil + | Imm64_pair hi lo => load_hilo64 hi lo + | Imm64_large imm => fSop (OEloadli imm) fSnil + end. + +Definition opimm32 (hv1: 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 + | Imm32_pair hi lo => + let fsv := load_hilo32 hi lo in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + 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 + | Imm64_pair hi lo => + let fsv := load_hilo64 hi lo in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + | Imm64_large imm => + let fsv := fSop (OEloadli imm) fSnil in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + end. + +Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). +Definition andimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oand OEandiw. +Definition orimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oor OEoriw. +Definition xorimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oxor OExoriw. +Definition sltimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. +Definition sltuimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. +Definition addimm64 (hv1: sval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). +Definition andimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oandl OEandil. +Definition orimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oorl OEoril. +Definition xorimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oxorl OExoril. +Definition sltimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. +Definition sltuimm64 (hv1: sval) (n: int64) := opimm64 hv1 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. + +(** 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) + | _, _ => None + end. + +Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := + None. + +(** * 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. + +(* TODO gourdinl move to common/Values ? *) +Theorem swap_cmpf_bool: + forall c x y, + Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. +Qed. +Local Hint Resolve swap_cmpf_bool: core. + +Theorem swap_cmpfs_bool: + forall c x y, + Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. +Qed. +Local Hint Resolve swap_cmpfs_bool: 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 swap_cmpf_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite 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 swap_cmpfs_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite 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. + +(* 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. + (* 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 ge sp rs0 m0 st c' l': forall + (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) + (LREF : hsilocal_refines ge sp rs0 m0 hrs st) + (OK: hsok_local ge sp rs0 m0 hrs), + seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = + seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Proof. + unfold target_cbranch_expanse, seval_condition; simpl. + intros H (LREF & SREF & SREG & SMEM) ?. + congruence. +Qed. +Global Opaque target_op_simplify. + Global Opaque target_cbranch_expanse.*) -- cgit