diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 12:00:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 12:00:33 +0200 |
| commit | c455f69d66b186414c8bb1c5cd28ce8f29e965aa (patch) | |
| tree | 569ef74216e5bce1e2a1d1457b0c8b930b14ef7e /aarch64/SelectOpproof.v | |
| parent | 827bdabf1242720979848cf473263a54fcf212f5 (diff) | |
| download | compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.tar.gz compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.zip | |
AArch64 division no longer "traps"
Diffstat (limited to 'aarch64/SelectOpproof.v')
| -rw-r--r-- | aarch64/SelectOpproof.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/aarch64/SelectOpproof.v b/aarch64/SelectOpproof.v index 3379cbd8..c7898193 100644 --- a/aarch64/SelectOpproof.v +++ b/aarch64/SelectOpproof.v @@ -666,7 +666,8 @@ Theorem eval_divs_base: Val.divs x y = Some z -> exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold divs_base; TrivialExists. + intros; unfold divs_base; TrivialExists; cbn. + rewrite H1. reflexivity. Qed. Theorem eval_mods_base: @@ -678,7 +679,8 @@ Theorem eval_mods_base: Proof. intros; unfold mods_base, mod_aux. exploit Val.mods_divs; eauto. intros (q & A & B). subst z. - TrivialExists. repeat (econstructor; eauto with evalexpr). exact A. + TrivialExists. repeat (econstructor; eauto with evalexpr). + cbn. rewrite A. reflexivity. Qed. Theorem eval_divu_base: @@ -689,6 +691,7 @@ Theorem eval_divu_base: exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. intros; unfold divu_base; TrivialExists. + cbn. rewrite H1. reflexivity. Qed. Theorem eval_modu_base: @@ -700,7 +703,8 @@ Theorem eval_modu_base: Proof. intros; unfold modu_base, mod_aux. exploit Val.modu_divu; eauto. intros (q & A & B). subst z. - TrivialExists. repeat (econstructor; eauto with evalexpr). exact A. + TrivialExists. repeat (econstructor; eauto with evalexpr). + rewrite A. reflexivity. Qed. Theorem eval_shrximm: @@ -715,7 +719,7 @@ Proof. destruct x; simpl in H0; try discriminate. change (Int.ltu Int.zero (Int.repr 31)) with true in H0; inv H0. rewrite Int.shrx_zero by (compute; auto). auto. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. (** General shifts *) |