diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /backend/SplitLongproof.v | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 3b1eaa6b..fd1fdebd 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -96,7 +96,7 @@ Lemma eval_helper: Proof. intros. red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). - rewrite <- Genv.find_funct_ptr_iff in Q. + rewrite <- Genv.find_funct_ptr_iff in Q. econstructor; eauto. Qed. @@ -363,7 +363,7 @@ Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. red; intros. unfold longofint. destruct (longofint_match a). -- InvEval. econstructor; split. apply eval_longconst. auto. +- InvEval. econstructor; split. apply eval_longconst. auto. - exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. intros [v1 [A B]]. econstructor; split. EvalOp. @@ -725,7 +725,7 @@ Qed. Theorem eval_addl: Archi.ptr64 = false -> binary_constructor_sound addl Val.addl. Proof. - unfold addl; red; intros. + unfold addl; red; intros. set (default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). @@ -806,7 +806,7 @@ Proof. exists v; split; auto. destruct x; simpl; auto. erewrite Int64.mul_pow2' by eauto. - simpl in B. erewrite Int64.is_power2'_range in B by eauto. + simpl in B. erewrite Int64.is_power2'_range in B by eauto. exact B. apply eval_mull_base; auto. apply eval_longconst. Qed. @@ -828,18 +828,18 @@ Proof. - apply eval_mull_base; auto. Qed. -Theorem eval_mullhu: +Theorem eval_mullhu: forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). Proof. - unfold mullhu; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + unfold mullhu; intros; red; intros. econstructor; split; eauto. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. Qed. -Theorem eval_mullhs: +Theorem eval_mullhs: forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). Proof. - unfold mullhs; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + unfold mullhs; intros; red; intros. econstructor; split; eauto. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. Qed. Theorem eval_shrxlimm: |