diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 09:17:05 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 19:39:46 +0200 |
| commit | cae21e8816db863bf99f87469c9680e150d28960 (patch) | |
| tree | 19fdf188238300245e0e5e7a9b78a94bbb53df93 /riscV/SelectLongproof.v | |
| parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
| download | compcert-kvx-cae21e8816db863bf99f87469c9680e150d28960.tar.gz compcert-kvx-cae21e8816db863bf99f87469c9680e150d28960.zip | |
maketotal mod & div
Diffstat (limited to 'riscV/SelectLongproof.v')
| -rw-r--r-- | riscV/SelectLongproof.v | 46 |
1 files changed, 19 insertions, 27 deletions
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index d47b6d64..f5e8edf8 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -455,6 +455,10 @@ Proof. unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divls_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. @@ -462,6 +466,10 @@ Proof. unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modls_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. @@ -469,6 +477,10 @@ Proof. unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_divlu_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. @@ -476,6 +488,10 @@ Proof. unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_modlu_base; eauto. TrivialExists. + cbn. + rewrite H1. + cbn. + trivial. Qed. Theorem eval_shrxlimm: @@ -490,33 +506,9 @@ Proof. - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto. change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto. - TrivialExists. -(* - intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL. -+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32. -+ destruct x; simpl in H0; try discriminate. - destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0. - predSpec Int.eq Int.eq_spec n Int.zero. - - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto. - - assert (NZ: Int.unsigned n <> 0). - { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. } - assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption). - assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true). - { unfold Int.ltu; apply zlt_true. - unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. - rewrite Int.unsigned_repr. omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. } - assert (X: eval_expr ge sp e m le - (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil)) - (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))). - { EvalOp. } - assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n) - (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))). - { EvalOp. simpl. rewrite LTU2. auto. } - TrivialExists. - constructor. EvalOp. simpl; eauto. constructor. - simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. - change (Int.unsigned Int64.iwordsize') with 64; omega. -*) + cbn. + rewrite H0. + reflexivity. Qed. Theorem eval_cmplu: |