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 /common/AST.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 'common/AST.v')
| -rw-r--r-- | common/AST.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/common/AST.v b/common/AST.v index 34f29bb3..8a46a153 100644 --- a/common/AST.v +++ b/common/AST.v @@ -111,7 +111,7 @@ Definition cc_default := Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}. Proof. - decide equality; apply bool_dec. + decide equality; apply bool_dec. Defined. Global Opaque calling_convention_eq. @@ -301,7 +301,7 @@ Lemma prog_defmap_unique: ~In id (map fst defs2) -> (prog_defmap p)!id = Some g. Proof. - unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. + unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. Qed. Lemma prog_defmap_norepet: @@ -408,7 +408,7 @@ Proof. OK (List.map (transform_program_globdef transf_fun) l)). { induction l as [ | [id g] l]; simpl. - auto. - - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. + - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. } rewrite EQ; simpl. auto. Qed. @@ -563,7 +563,7 @@ End TRANSF_PARTIAL_FUNDEF. Set Contextual Implicit. (** In some intermediate languages (LTL, Mach), 64-bit integers can be - split into two 32-bit halves and held in a pair of registers. + split into two 32-bit halves and held in a pair of registers. Syntactically, this is captured by the type [rpair] below. *) Inductive rpair (A: Type) : Type := @@ -589,7 +589,7 @@ Definition regs_of_rpair (A: Type) (p: rpair A): list A := end. Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A := - match l with + match l with | nil => nil | p :: l => regs_of_rpair p ++ regs_of_rpairs l end. @@ -603,8 +603,8 @@ Qed. Lemma in_regs_of_rpairs_inv: forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p). Proof. - induction l; simpl; intros. contradiction. - rewrite in_app_iff in H; destruct H. + induction l; simpl; intros. contradiction. + rewrite in_app_iff in H; destruct H. exists a; auto. apply IHl in H. firstorder auto. Qed. |