diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /backend/PPCgen.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
download | compcert-355b4abcee015c3fae9ac5653c25259e104a886c.tar.gz compcert-355b4abcee015c3fae9ac5653c25259e104a886c.zip |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/PPCgen.v')
-rw-r--r-- | backend/PPCgen.v | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/backend/PPCgen.v b/backend/PPCgen.v index ba8ea285..d7a83b0b 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. @@ -268,11 +269,6 @@ Definition transl_op Pori (ireg_of r) (ireg_of r) (Csymbol_low_unsigned s ofs) :: k | Oaddrstack n, nil => addimm (ireg_of r) GPR1 n k - | Oundef, nil => - match mreg_type r with - | Tint => Piundef (ireg_of r) :: k - | Tfloat => Pfundef (freg_of r) :: k - end | Ocast8signed, a1 :: nil => Pextsb (ireg_of r) (ireg_of a1) :: k | Ocast8unsigned, a1 :: nil => @@ -474,6 +470,17 @@ Definition transl_instr (i: Mach.instruction) (k: code) := Pmtctr (ireg_of r) :: Pbctrl :: k | Mcall sig (inr symb) => Pbl symb :: k + | Mtailcall sig (inl r) => + Pmtctr (ireg_of r) :: + Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: + Pmtlr GPR2 :: + Pfreeframe :: + Pbctr :: k + | Mtailcall sig (inr symb) => + Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: + Pmtlr GPR2 :: + Pfreeframe :: + Pbs symb :: k | Malloc => Pallocblock :: k | Mlabel lbl => @@ -510,14 +517,17 @@ Fixpoint code_size (c: code) : Z := | instr :: c' => code_size c' + 1 end. -Definition transf_function (f: Mach.function) : option PPC.code := +Open Local Scope string_scope. + +Definition transf_function (f: Mach.function) : res PPC.code := let c := transl_function f in if zlt Int.max_unsigned (code_size c) - then None - else Some c. + then Errors.Error (msg "code size exceeded") + else Errors.OK c. -Definition transf_fundef (f: Mach.fundef) : option PPC.fundef := +Definition transf_fundef (f: Mach.fundef) : res PPC.fundef := transf_partial_fundef transf_function f. -Definition transf_program (p: Mach.program) : option PPC.program := +Definition transf_program (p: Mach.program) : res PPC.program := transform_partial_program transf_fundef p. + |