From c455f69d66b186414c8bb1c5cd28ce8f29e965aa Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 30 Sep 2020 12:00:33 +0200 Subject: AArch64 division no longer "traps" --- aarch64/ConstpropOpproof.v | 121 +++++++++++++++++++++++++++++++-------------- 1 file changed, 85 insertions(+), 36 deletions(-) (limited to 'aarch64/ConstpropOpproof.v') diff --git a/aarch64/ConstpropOpproof.v b/aarch64/ConstpropOpproof.v index deab7cd4..c777062c 100644 --- a/aarch64/ConstpropOpproof.v +++ b/aarch64/ConstpropOpproof.v @@ -335,40 +335,63 @@ Qed. Lemma make_divimm_correct: forall n r1 r2 v, - Val.divs e#r1 e#r2 = Some v -> + Val.maketotal (Val.divs e#r1 e#r2) = v -> e#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. - predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. - destruct (e#r1) eqn:?; - try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); - inv H; auto. - destruct (Int.is_power2 n) eqn:?. - destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. - exists v; auto. - exists v; auto. + predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0. + { destruct (e # r1) eqn:Er1. + all: try (cbn; exists (e # r1); split; auto; fail). + rewrite Val.divs_one. + cbn. + rewrite Er1. + exists (Vint i); split; auto. + } + destruct (Int.is_power2 n) eqn:Power2. + { + destruct (Int.ltu i (Int.repr 31)) eqn:iLT31. + { + cbn. + exists (Val.maketotal (Val.shrx e # r1 (Vint i))); split; auto. + destruct (Val.divs e # r1 (Vint n)) eqn:DIVS; cbn; auto. + rewrite Val.divs_pow2 with (y:=v) (n:=n). + cbn. + all: auto. + } + exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence. + } + exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence. Qed. + Lemma make_divuimm_correct: forall n r1 r2 v, - Val.divu e#r1 e#r2 = Some v -> + Val.maketotal (Val.divu e#r1 e#r2) = v -> e#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. - predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. - destruct (e#r1) eqn:?; - try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); - inv H; auto. - destruct (Int.is_power2 n) eqn:?. - econstructor; split. simpl; eauto. - rewrite mk_amount32_eq by (eapply Int.is_power2_range; eauto). - rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. - exists v; auto. + predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0. + { destruct (e # r1) eqn:Er1. + all: try (cbn; exists (e # r1); split; auto; fail). + rewrite Val.divu_one. + cbn. + rewrite Er1. + exists (Vint i); split; auto. + } + destruct (Int.is_power2 n) eqn:Power2. + { + cbn. + rewrite mk_amount32_eq by (eapply Int.is_power2_range; eauto). + exists (Val.shru e # r1 (Vint i)); split; auto. + destruct (Val.divu e # r1 (Vint n)) eqn:DIVU; cbn; auto. + rewrite Val.divu_pow2 with (y:=v) (n:=n). + all: auto. + } + exists (Val.maketotal (Val.divu e # r1 (Vint n))); split; cbn; auto; congruence. Qed. Lemma make_andimm_correct: @@ -503,34 +526,60 @@ Qed. Lemma make_divlimm_correct: forall n r1 r2 v, - Val.divls e#r1 e#r2 = Some v -> + Val.maketotal (Val.divls e#r1 e#r2) = v -> e#r2 = Vlong n -> let (op, args) := make_divlimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divlimm. - destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. - exists v; auto. - exists v; auto. + destruct (Int64.is_power2' n) eqn:Power2. + { + destruct (Int.ltu i (Int.repr 63)) eqn:iLT63. + { + cbn. + exists (Val.maketotal (Val.shrxl e # r1 (Vint i))); split; auto. + rewrite H0 in H. + destruct (Val.divls e # r1 (Vlong n)) eqn:DIVS; cbn in H; auto. + { + subst v0. + rewrite Val.divls_pow2 with (y:=v) (n:=n). + cbn. + all: auto. + } + subst. auto. + } + cbn. subst. rewrite H0. + exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto. + } + cbn. subst. rewrite H0. + exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto. Qed. + Lemma make_divluimm_correct: forall n r1 r2 v, - Val.divlu e#r1 e#r2 = Some v -> + Val.maketotal (Val.divlu e#r1 e#r2) = v -> e#r2 = Vlong n -> let (op, args) := make_divluimm n r1 r2 in exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divluimm. destruct (Int64.is_power2' n) eqn:?. + { econstructor; split. simpl; eauto. - rewrite mk_amount64_eq by (eapply Int64.is_power2'_range; eauto). - rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. - erewrite Int64.is_power2'_range by eauto. - erewrite Int64.divu_pow2' by eauto. auto. - exists v; auto. + rewrite H0 in H. destruct (e#r1); inv H. + all: cbn; auto. + { + rewrite mk_amount64_eq by (eapply Int64.is_power2'_range; eauto). + destruct (Int64.eq n Int64.zero); cbn; auto. + erewrite Int64.is_power2'_range by eauto. + erewrite Int64.divu_pow2' by eauto. auto. + } + } + exists v; split; auto. + cbn. + rewrite H. + reflexivity. Qed. Lemma make_andlimm_correct: @@ -679,10 +728,10 @@ Proof. InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto. - (* divs *) assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. - apply make_divimm_correct; auto. + apply make_divimm_correct; auto. congruence. - (* divu *) assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. - apply make_divuimm_correct; auto. + apply make_divuimm_correct; auto. congruence. - (* and 1 *) rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto. - (* and 2 *) @@ -745,10 +794,10 @@ Proof. InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto. - (* divl *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. - apply make_divlimm_correct; auto. + apply make_divlimm_correct; auto. congruence. - (* divlu *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. - apply make_divluimm_correct; auto. + apply make_divluimm_correct; auto. congruence. - (* andl 1 *) rewrite Val.andl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto. - (* andl 2 *) -- cgit