diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
| commit | 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e (patch) | |
| tree | 2c4e87342b978883fb471559ca0c18e5f7a3cc00 /mppa_k1c/SelectLongproof.v | |
| parent | ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c (diff) | |
| download | compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.tar.gz compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.zip | |
generate multiply-sub long
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3b724c01..257c7fd9 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -208,6 +208,23 @@ Proof. - subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp. - subst. rewrite Val.subl_addl_r. apply eval_addlimm; EvalOp. +- TrivialExists. simpl. subst. reflexivity. +- TrivialExists. simpl. subst. + destruct v1; destruct x; simpl; trivial. + + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Int64.sub_add_opp. + reflexivity. + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Ptrofs.sub_add_opp. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 (Int64.mul i n)) (Int64.mul i n)). + rewrite (Ptrofs.agree64_of_int ARCHI64 (Int64.neg (Int64.mul i n))). + reflexivity. + apply (Ptrofs.agree64_of_int ARCHI64). - TrivialExists. Qed. @@ -371,7 +388,7 @@ Proof. auto. } generalize (Int64.one_bits'_decomp n); intros D. destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B. -- apply DEFAULT. +- TrivialExists. - replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)). apply eval_shllimm; auto. simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto. @@ -389,7 +406,7 @@ Proof. rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib). inv B1; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto. -- apply DEFAULT. +- TrivialExists. Qed. Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). |