From 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 10:21:59 +0200 Subject: generate multiply-sub long --- mppa_k1c/SelectLongproof.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/SelectLongproof.v') diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3b724c01..257c7fd9 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -208,6 +208,23 @@ Proof. - subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp. - subst. rewrite Val.subl_addl_r. apply eval_addlimm; EvalOp. +- TrivialExists. simpl. subst. reflexivity. +- TrivialExists. simpl. subst. + destruct v1; destruct x; simpl; trivial. + + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Int64.sub_add_opp. + reflexivity. + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Ptrofs.sub_add_opp. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 (Int64.mul i n)) (Int64.mul i n)). + rewrite (Ptrofs.agree64_of_int ARCHI64 (Int64.neg (Int64.mul i n))). + reflexivity. + apply (Ptrofs.agree64_of_int ARCHI64). - TrivialExists. Qed. @@ -371,7 +388,7 @@ Proof. auto. } generalize (Int64.one_bits'_decomp n); intros D. destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B. -- apply DEFAULT. +- TrivialExists. - replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)). apply eval_shllimm; auto. simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto. @@ -389,7 +406,7 @@ Proof. rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib). inv B1; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto. -- apply DEFAULT. +- TrivialExists. Qed. Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). -- cgit From 17a8d91a82f67d7f62f8cbad41ba76a4b0b82a30 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 20:17:09 +0200 Subject: apply .xs onto addx4 etc --- mppa_k1c/SelectLongproof.v | 107 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) (limited to 'mppa_k1c/SelectLongproof.v') diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 257c7fd9..3c9f64d5 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -119,6 +119,67 @@ Proof. - TrivialExists. Qed. + +Theorem eval_addlimm_shllimm: + forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)). +Proof. + red; unfold addlimm_shllimm; intros. + destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. + - TrivialExists. simpl. + f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e1. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e1. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e2. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e2. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e3. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e3. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e4. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e4. + rewrite Int.repr_unsigned. + reflexivity. + } + discriminate. + - unfold addxl. rewrite Val.addl_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. +Qed. + Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). Proof. unfold addlimm; intros; red; intros. @@ -136,9 +197,47 @@ Proof. destruct sp; simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists. +- pose proof eval_addlimm_shllimm as ADDXL. + unfold unary_constructor_sound in ADDXL. + unfold addxl in ADDXL. + rewrite Val.addl_commut. + subst x. + apply ADDXL; assumption. - TrivialExists. Qed. +Lemma eval_addxl: forall n, binary_constructor_sound (addl_shllimm n) (ExtValues.addxl n). +Proof. + red. + intros. + unfold addl_shllimm. + destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT. + - TrivialExists. + simpl. + f_equal. f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + rewrite <- e1. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + rewrite <- e2. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + rewrite <- e3. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + rewrite <- e4. + apply Int.repr_unsigned. } + discriminate. + (* Oaddxl *) + - TrivialExists; + repeat econstructor; eassumption. +Qed. + Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl. destruct Archi.splitlong eqn:SL. @@ -193,6 +292,14 @@ Proof. - subst. rewrite Val.addl_commut. TrivialExists. - subst. TrivialExists. - subst. rewrite Val.addl_commut. TrivialExists. + - subst. pose proof eval_addxl as ADDXL. + unfold binary_constructor_sound in ADDXL. + rewrite Val.addl_commut. + apply ADDXL; assumption. + (* Oaddxl *) + - subst. pose proof eval_addxl as ADDXL. + unfold binary_constructor_sound in ADDXL. + apply ADDXL; assumption. - TrivialExists. Qed. -- cgit From 66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 21:54:18 +0200 Subject: option -faddx (off by default until questions cleared) --- mppa_k1c/SelectLongproof.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/SelectLongproof.v') diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3c9f64d5..58a4c39a 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -124,6 +124,8 @@ Theorem eval_addlimm_shllimm: forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)). Proof. red; unfold addlimm_shllimm; intros. + destruct (Compopts.optim_addx tt). + { destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. - TrivialExists. simpl. f_equal. @@ -178,6 +180,13 @@ Proof. repeat (try eassumption; try econstructor). simpl. reflexivity. + } + { unfold addxl. rewrite Val.addl_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } Qed. Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). @@ -188,7 +197,7 @@ Proof. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. -- destruct (Compopts.optim_fglobaladdroffset _). +- destruct (Compopts.optim_globaladdroffset _). + econstructor; split. EvalOp. simpl; eauto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. @@ -211,6 +220,8 @@ Proof. red. intros. unfold addl_shllimm. + destruct (Compopts.optim_addx tt). + { destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT. - TrivialExists. simpl. @@ -235,7 +246,11 @@ Proof. discriminate. (* Oaddxl *) - TrivialExists; - repeat econstructor; eassumption. + repeat econstructor; eassumption. + } + { TrivialExists; + repeat econstructor; eassumption. + } Qed. Theorem eval_addl: binary_constructor_sound addl Val.addl. -- cgit From 005093b87250b6b27b320eb789574da4bda616c0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 22:40:50 +0200 Subject: correct -faddx option and propagate addim over addxim --- mppa_k1c/SelectLongproof.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'mppa_k1c/SelectLongproof.v') diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 58a4c39a..78a2bb31 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -206,6 +206,11 @@ Proof. destruct sp; simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists. +- TrivialExists; simpl. subst x. + destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + rewrite Int64.add_assoc. rewrite Int64.add_commut. + reflexivity. - pose proof eval_addlimm_shllimm as ADDXL. unfold unary_constructor_sound in ADDXL. unfold addxl in ADDXL. -- cgit