diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 10:07:56 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 10:07:56 +0100 |
| commit | 5ddc6e1de69aeeb1b03f4e495c8b75c2feec590d (patch) | |
| tree | d1942582584ab6c6e232f61a316bfb3c9958b26e /mppa_k1c/SelectOpproof.v | |
| parent | 50ea35fceb52c5f66ccbc4f709df3a3471b12647 (diff) | |
| parent | 69ee85006f81571a7a5cf5d13a38078f07be07c4 (diff) | |
| download | compcert-kvx-5ddc6e1de69aeeb1b03f4e495c8b75c2feec590d.tar.gz compcert-kvx-5ddc6e1de69aeeb1b03f4e495c8b75c2feec590d.zip | |
Merge branch 'mppa_postpass' into mppa-mul
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 88eeada8..7c0dea8a 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -247,6 +247,14 @@ Proof. with (Val.add (Val.add x v1) (Vint n2)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. reflexivity. + - (* Omadd *) + subst. TrivialExists. + - (* Omadd rev *) + subst. rewrite Val.add_commut. TrivialExists. + - (* Omaddimm *) + subst. TrivialExists. + - (* Omaddimm rev *) + subst. rewrite Val.add_commut. TrivialExists. - TrivialExists. Qed. @@ -362,7 +370,7 @@ Proof. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). destruct (Int.one_bits n). - - intros. auto. + - intros. TrivialExists. - destruct l. + intros. rewrite H1. simpl. rewrite Int.add_zero. @@ -380,7 +388,7 @@ Proof. rewrite Val.mul_add_distr_r. repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto. simpl. repeat rewrite H0; auto with coqlib. - intros. auto. + intros. TrivialExists. Qed. Theorem eval_mulimm: |