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/SelectLongproof.v | |
| parent | 827bdabf1242720979848cf473263a54fcf212f5 (diff) | |
| download | compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.tar.gz compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.zip | |
AArch64 division no longer "traps"
Diffstat (limited to 'aarch64/SelectLongproof.v')
| -rw-r--r-- | aarch64/SelectLongproof.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/aarch64/SelectLongproof.v b/aarch64/SelectLongproof.v index 60dc1a12..c1847638 100644 --- a/aarch64/SelectLongproof.v +++ b/aarch64/SelectLongproof.v @@ -559,25 +559,29 @@ Qed. Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. Proof. red; intros; unfold divls_base; TrivialExists. + cbn. rewrite H1. reflexivity. Qed. Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. Proof. red; intros; unfold modls_base, modl_aux. exploit Val.modls_divls; 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_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. Proof. red; intros; unfold divlu_base; TrivialExists. + cbn. rewrite H1. reflexivity. Qed. Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. Proof. red; intros; unfold modlu_base, modl_aux. exploit Val.modlu_divlu; 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_shrxlimm: @@ -592,7 +596,7 @@ Proof. destruct x; simpl in H0; try discriminate. change (Int.ltu Int.zero (Int.repr 63)) with true in H0; inv H0. rewrite Int64.shrx'_zero. auto. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. (** General shifts *) |