From 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 3 May 2017 11:18:32 +0200 Subject: 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. --- x86/SelectLongproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'x86/SelectLongproof.v') diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v index 2262a70b..3bef632d 100644 --- a/x86/SelectLongproof.v +++ b/x86/SelectLongproof.v @@ -399,7 +399,7 @@ Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Va Proof. unfold mullimm. intros; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_mullimm; eauto. + eapply SplitLongproof.eval_mullimm; eauto. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists (Vlong Int64.zero); split. apply eval_longconst. destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto. @@ -426,14 +426,14 @@ Proof. - TrivialExists. 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. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto. red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. 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. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto. -- cgit