From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgen.v | 554 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 554 insertions(+) create mode 100644 arm/Asmgen.v (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v new file mode 100644 index 00000000..a360bded --- /dev/null +++ b/arm/Asmgen.v @@ -0,0 +1,554 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Translation from Mach to ARM. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Errors. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import Mach. +Require Import Asm. + +(** Translation of the LTL/Linear/Mach view of machine registers + to the ARM view. ARM has two different types for registers + (integer and float) while LTL et al have only one. The + [ireg_of] and [freg_of] are therefore partial in principle. + To keep things simpler, we make them return nonsensical + results when applied to a LTL register of the wrong type. + The proof in [ARMgenproof] will show that this never happens. + + Note that no LTL register maps to [IR14]. + This register is reserved as temporary, to be used + by the generated ARM code. *) + +Definition ireg_of (r: mreg) : ireg := + match r with + | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 + | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 + | R8 => IR8 | R9 => IR9 | R11 => IR11 + | IT1 => IR10 | IT2 => IR12 + | _ => IR0 (* should not happen *) + end. + +Definition freg_of (r: mreg) : freg := + match r with + | F0 => FR0 | F1 => FR1 + | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7 + | FT1 => FR2 | FT2 => FR3 + | _ => FR0 (* should not happen *) + end. + +(** Recognition of integer immediate arguments. +- For arithmetic operations, immediates are + 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. +- For memory accesses of type [Mint32], immediate offsets are + 12-bit quantities plus a sign bit. +- For other memory accesses, immediate offsets are + 8-bit quantities plus a sign bit. *) + +Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool := + match n with + | O => false + | Datatypes.S n' => + Int.eq (Int.and x (Int.not msk)) Int.zero || + is_immed_arith_aux n' x (Int.ror msk (Int.repr 2)) + end. + +Definition is_immed_arith (x: int) : bool := + is_immed_arith_aux 16%nat x (Int.repr 255). + +Definition is_immed_mem_word (x: int) : bool := + Int.lt x (Int.repr 4096) && Int.lt (Int.repr (-4096)) x. + +Definition is_immed_mem_small (x: int) : bool := + Int.lt x (Int.repr 256) && Int.lt (Int.repr (-256)) x. + +Definition is_immed_mem_float (x: int) : bool := + Int.eq (Int.and x (Int.repr 3)) Int.zero + && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x. + +(** Smart constructor for integer immediate arguments. *) + +Definition loadimm (r: ireg) (n: int) (k: code) := + if is_immed_arith n then + Pmov r (SOimm n) :: k + else if is_immed_arith (Int.not n) then + Pmvn r (SOimm (Int.not n)) :: k + else (* could be much improved! *) + Pmov r (SOimm (Int.and n (Int.repr 255))) :: + Porr r r (SOimm (Int.and n (Int.repr 65280))) :: + Porr r r (SOimm (Int.and n (Int.repr 16711680))) :: + Porr r r (SOimm (Int.and n (Int.repr 4278190080))) :: + k. + +Definition addimm (r1 r2: ireg) (n: int) (k: code) := + if is_immed_arith n then + Padd r1 r2 (SOimm n) :: k + else if is_immed_arith (Int.neg n) then + Psub r1 r2 (SOimm (Int.neg n)) :: k + else + Padd r1 r2 (SOimm (Int.and n (Int.repr 255))) :: + Padd r1 r1 (SOimm (Int.and n (Int.repr 65280))) :: + Padd r1 r1 (SOimm (Int.and n (Int.repr 16711680))) :: + Padd r1 r1 (SOimm (Int.and n (Int.repr 4278190080))) :: + k. + +Definition andimm (r1 r2: ireg) (n: int) (k: code) := + if is_immed_arith n then + Pand r1 r2 (SOimm n) :: k + else if is_immed_arith (Int.not n) then + Pbic r1 r2 (SOimm (Int.not n)) :: k + else + loadimm IR14 n (Pand r1 r2 (SOreg IR14) :: k). + +Definition makeimm (instr: ireg -> ireg -> shift_op -> instruction) + (r1 r2: ireg) (n: int) (k: code) := + if is_immed_arith n then + instr r1 r2 (SOimm n) :: k + else + loadimm IR14 n (instr r1 r2 (SOreg IR14) :: k). + +(** Translation of a shift immediate operation (type [Op.shift]) *) + +Definition transl_shift (s: shift) (r: ireg) : shift_op := + match s with + | Slsl n => SOlslimm r (s_amount n) + | Slsr n => SOlsrimm r (s_amount n) + | Sasr n => SOasrimm r (s_amount n) + | Sror n => SOrorimm r (s_amount n) + end. + +(** Translation of a condition. Prepends to [k] the instructions + that evaluate the condition and leave its boolean result in one of + the bits of the condition register. The bit in question is + determined by the [crbit_for_cond] function. *) + +Definition transl_cond + (cond: condition) (args: list mreg) (k: code) := + match cond, args with + | Ccomp c, a1 :: a2 :: nil => + Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Ccompu c, a1 :: a2 :: nil => + Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Ccompshift c s, a1 :: a2 :: nil => + Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Ccompushift c s, a1 :: a2 :: nil => + Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Ccompimm c n, a1 :: nil => + if is_immed_arith n then + Pcmp (ireg_of a1) (SOimm n) :: k + else + loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + | Ccompuimm c n, a1 :: nil => + if is_immed_arith n then + Pcmp (ireg_of a1) (SOimm n) :: k + else + loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + | Ccompf cmp, a1 :: a2 :: nil => + Pcmf (freg_of a1) (freg_of a2) :: k + | Cnotcompf cmp, a1 :: a2 :: nil => + Pcmf (freg_of a1) (freg_of a2) :: k + | _, _ => + k (**r never happens for well-typed code *) + end. + +Definition crbit_for_signed_cmp (cmp: comparison) := + match cmp with + | Ceq => CReq + | Cne => CRne + | Clt => CRlt + | Cle => CRle + | Cgt => CRgt + | Cge => CRge + end. + +Definition crbit_for_unsigned_cmp (cmp: comparison) := + match cmp with + | Ceq => CReq + | Cne => CRne + | Clt => CRlo + | Cle => CRls + | Cgt => CRhi + | Cge => CRhs + end. + +Definition crbit_for_float_cmp (cmp: comparison) := + match cmp with + | Ceq => CReq + | Cne => CRne + | Clt => CRmi + | Cle => CRls + | Cgt => CRgt + | Cge => CRge + end. + +Definition crbit_for_float_not_cmp (cmp: comparison) := + match cmp with + | Ceq => CRne + | Cne => CReq + | Clt => CRpl + | Cle => CRhi + | Cgt => CRle + | Cge => CRlt + end. + +Definition crbit_for_cond (cond: condition) := + match cond with + | Ccomp cmp => crbit_for_signed_cmp cmp + | Ccompu cmp => crbit_for_unsigned_cmp cmp + | Ccompshift cmp s => crbit_for_signed_cmp cmp + | Ccompushift cmp s => crbit_for_unsigned_cmp cmp + | Ccompimm cmp n => crbit_for_signed_cmp cmp + | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp + | Ccompf cmp => crbit_for_float_cmp cmp + | Cnotcompf cmp => crbit_for_float_not_cmp cmp + end. + +(** Translation of the arithmetic operation [r <- op(args)]. + The corresponding instructions are prepended to [k]. *) + +Definition transl_op + (op: operation) (args: list mreg) (r: mreg) (k: code) := + match op, args with + | Omove, a1 :: nil => + match mreg_type a1 with + | Tint => Pmov (ireg_of r) (SOreg (ireg_of a1)) :: k + | Tfloat => Pmvfd (freg_of r) (freg_of a1) :: k + end + | Ointconst n, nil => + loadimm (ireg_of r) n k + | Ofloatconst f, nil => + Plifd (freg_of r) f :: k + | Oaddrsymbol s ofs, nil => + Ploadsymbol (ireg_of r) s ofs :: k + | Oaddrstack n, nil => + addimm (ireg_of r) IR13 n k + | Ocast8signed, a1 :: nil => + Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 24)) :: + Pmov (ireg_of r) (SOasrimm (ireg_of r) (Int.repr 24)) :: k + | Ocast8unsigned, a1 :: nil => + Pand (ireg_of r) (ireg_of a1) (SOimm (Int.repr 255)) :: k + | Ocast16signed, a1 :: nil => + Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 16)) :: + Pmov (ireg_of r) (SOasrimm (ireg_of r) (Int.repr 16)) :: k + | Ocast16unsigned, a1 :: nil => + Pmov (ireg_of r) (SOlslimm (ireg_of a1) (Int.repr 16)) :: + Pmov (ireg_of r) (SOlsrimm (ireg_of r) (Int.repr 16)) :: k + | Oadd, a1 :: a2 :: nil => + Padd (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Oaddshift s, a1 :: a2 :: nil => + Padd (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Oaddimm n, a1 :: nil => + addimm (ireg_of r) (ireg_of a1) n k + | Osub, a1 :: a2 :: nil => + Psub (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Osubshift s, a1 :: a2 :: nil => + Psub (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Orsubshift s, a1 :: a2 :: nil => + Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Orsubimm n, a1 :: nil => + makeimm Prsb (ireg_of r) (ireg_of a1) n k + | Omul, a1 :: a2 :: nil => + if ireg_eq (ireg_of r) (ireg_of a1) + || ireg_eq (ireg_of r) (ireg_of a2) + then Pmul IR14 (ireg_of a1) (ireg_of a2) :: Pmov (ireg_of r) (SOreg IR14) :: k + else Pmul (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Odiv, a1 :: a2 :: nil => + Psdiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Odivu, a1 :: a2 :: nil => + Pudiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oand, a1 :: a2 :: nil => + Pand (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Oandshift s, a1 :: a2 :: nil => + Pand (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Oandimm n, a1 :: nil => + andimm (ireg_of r) (ireg_of a1) n k + | Oor, a1 :: a2 :: nil => + Porr (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Oorshift s, a1 :: a2 :: nil => + Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Oorimm n, a1 :: nil => + makeimm Porr (ireg_of r) (ireg_of a1) n k + | Oxor, a1 :: a2 :: nil => + Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Oxorshift s, a1 :: a2 :: nil => + Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Oxorimm n, a1 :: nil => + makeimm Peor (ireg_of r) (ireg_of a1) n k + | Obic, a1 :: a2 :: nil => + Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + | Obicshift s, a1 :: a2 :: nil => + Pbic (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + | Onot, a1 :: nil => + Pmvn (ireg_of r) (SOreg (ireg_of a1)) :: k + | Onotshift s, a1 :: nil => + Pmvn (ireg_of r) (transl_shift s (ireg_of a1)) :: k + | Oshl, a1 :: a2 :: nil => + Pmov (ireg_of r) (SOlslreg (ireg_of a1) (ireg_of a2)) :: k + | Oshr, a1 :: a2 :: nil => + Pmov (ireg_of r) (SOasrreg (ireg_of a1) (ireg_of a2)) :: k + | Oshru, a1 :: a2 :: nil => + Pmov (ireg_of r) (SOlsrreg (ireg_of a1) (ireg_of a2)) :: k + | Oshift s, a1 :: nil => + Pmov (ireg_of r) (transl_shift s (ireg_of a1)) :: k + | Oshrximm n, a1 :: nil => + Pcmp (ireg_of a1) (SOimm Int.zero) :: + addimm IR14 (ireg_of a1) (Int.sub (Int.shl Int.one n) Int.one) + (Pmovc CRge IR14 (SOreg (ireg_of a1)) :: + Pmov (ireg_of r) (SOasrimm IR14 n) :: k) + | Onegf, a1 :: nil => + Pmnfd (freg_of r) (freg_of a1) :: k + | Oabsf, a1 :: nil => + Pabsd (freg_of r) (freg_of a1) :: k + | Oaddf, a1 :: a2 :: nil => + Padfd (freg_of r) (freg_of a1) (freg_of a2) :: k + | Osubf, a1 :: a2 :: nil => + Psufd (freg_of r) (freg_of a1) (freg_of a2) :: k + | Omulf, a1 :: a2 :: nil => + Pmufd (freg_of r) (freg_of a1) (freg_of a2) :: k + | Odivf, a1 :: a2 :: nil => + Pdvfd (freg_of r) (freg_of a1) (freg_of a2) :: k + | Osingleoffloat, a1 :: nil => + Pmvfs (freg_of r) (freg_of a1) :: k + | Ointoffloat, a1 :: nil => + Pfixz (ireg_of r) (freg_of a1) :: k + | Ointuoffloat, a1 :: nil => + Pfixzu (ireg_of r) (freg_of a1) :: k + | Ofloatofint, a1 :: nil => + Pfltd (freg_of r) (ireg_of a1) :: k + | Ofloatofintu, a1 :: nil => + Pfltud (freg_of r) (ireg_of a1) :: k + | Ocmp cmp, _ => + transl_cond cmp args + (Pmov (ireg_of r) (SOimm Int.zero) :: + Pmovc (crbit_for_cond cmp) (ireg_of r) (SOimm Int.one) :: + k) + | _, _ => + k (**r never happens for well-typed code *) + end. + +(** Common code to translate [Mload] and [Mstore] instructions. *) + +Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr := + match s with + | Slsl n => SAlsl r (s_amount n) + | Slsr n => SAlsr r (s_amount n) + | Sasr n => SAasr r (s_amount n) + | Sror n => SAror r (s_amount n) + end. + +Definition transl_load_store + (mk_instr_imm: ireg -> int -> instruction) + (mk_instr_gen: option (ireg -> shift_addr -> instruction)) + (is_immed: int -> bool) + (addr: addressing) (args: list mreg) (k: code) : code := + match addr, args with + | Aindexed n, a1 :: nil => + if is_immed n then + mk_instr_imm (ireg_of a1) n :: k + else + addimm IR14 (ireg_of a1) n + (mk_instr_imm IR14 Int.zero :: k) + | Aindexed2, a1 :: a2 :: nil => + match mk_instr_gen with + | Some f => + f (ireg_of a1) (SAreg (ireg_of a2)) :: k + | None => + Padd IR14 (ireg_of a1) (SOreg (ireg_of a2)) :: + mk_instr_imm IR14 Int.zero :: k + end + | Aindexed2shift s, a1 :: a2 :: nil => + match mk_instr_gen with + | Some f => + f (ireg_of a1) (transl_shift_addr s (ireg_of a2)) :: k + | None => + Padd IR14 (ireg_of a1) (transl_shift s (ireg_of a2)) :: + mk_instr_imm IR14 Int.zero :: k + end + | Ainstack n, nil => + if is_immed n then + mk_instr_imm IR13 n :: k + else + addimm IR14 IR13 n + (mk_instr_imm IR14 Int.zero :: k) + | _, _ => + (* should not happen *) k + end. + +Definition transl_load_store_int + (mk_instr: ireg -> ireg -> shift_addr -> instruction) + (is_immed: int -> bool) + (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := + transl_load_store + (fun r n => mk_instr (ireg_of rd) r (SAimm n)) + (Some (mk_instr (ireg_of rd))) + is_immed addr args k. + +Definition transl_load_store_float + (mk_instr: freg -> ireg -> int -> instruction) + (is_immed: int -> bool) + (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := + transl_load_store + (mk_instr (freg_of rd)) + None + is_immed addr args k. + +Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := + if is_immed_mem_word ofs then + Pldr dst base (SAimm ofs) :: k + else + addimm IR14 base ofs + (Pldr dst IR14 (SAimm Int.zero) :: k). + +Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := + if is_immed_mem_float ofs then + Pldfd dst base ofs :: k + else + addimm IR14 base ofs + (Pldfd dst IR14 Int.zero :: k). + +Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := + match ty with + | Tint => loadind_int base ofs (ireg_of dst) k + | Tfloat => loadind_float base ofs (freg_of dst) k + end. + +Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := + if is_immed_mem_word ofs then + Pstr src base (SAimm ofs) :: k + else + addimm IR14 base ofs + (Pstr src IR14 (SAimm Int.zero) :: k). + +Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := + if is_immed_mem_float ofs then + Pstfd src base ofs :: k + else + addimm IR14 base ofs + (Pstfd src IR14 Int.zero :: k). + +Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := + match ty with + | Tint => storeind_int (ireg_of src) base ofs k + | Tfloat => storeind_float (freg_of src) base ofs k + end. + +(** Translation of a Mach instruction. *) + +Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := + match i with + | Mgetstack ofs ty dst => + loadind IR13 ofs ty dst k + | Msetstack src ofs ty => + storeind src IR13 ofs ty k + | Mgetparam ofs ty dst => + loadind_int IR13 f.(fn_link_ofs) IR14 (loadind IR14 ofs ty dst k) + | Mop op args res => + transl_op op args res k + | Mload chunk addr args dst => + match chunk with + | Mint8signed => + transl_load_store_int Pldrsb is_immed_mem_small dst addr args k + | Mint8unsigned => + transl_load_store_int Pldrb is_immed_mem_small dst addr args k + | Mint16signed => + transl_load_store_int Pldrsh is_immed_mem_small dst addr args k + | Mint16unsigned => + transl_load_store_int Pldrh is_immed_mem_small dst addr args k + | Mint32 => + transl_load_store_int Pldr is_immed_mem_word dst addr args k + | Mfloat32 => + transl_load_store_float Pldfs is_immed_mem_float dst addr args k + | Mfloat64 => + transl_load_store_float Pldfd is_immed_mem_float dst addr args k + end + | Mstore chunk addr args src => + match chunk with + | Mint8signed => + transl_load_store_int Pstrb is_immed_mem_small src addr args k + | Mint8unsigned => + transl_load_store_int Pstrb is_immed_mem_small src addr args k + | Mint16signed => + transl_load_store_int Pstrh is_immed_mem_small src addr args k + | Mint16unsigned => + transl_load_store_int Pstrh is_immed_mem_small src addr args k + | Mint32 => + transl_load_store_int Pstr is_immed_mem_word src addr args k + | Mfloat32 => + transl_load_store_float Pstfs is_immed_mem_float src addr args k + | Mfloat64 => + transl_load_store_float Pstfd is_immed_mem_float src addr args k + end + | Mcall sig (inl r) => + Pblreg (ireg_of r) :: k + | Mcall sig (inr symb) => + Pblsymb symb :: k + | Mtailcall sig (inl r) => + loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k) + | Mtailcall sig (inr symb) => + loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k) + | Malloc => + Pallocblock :: k + | Mlabel lbl => + Plabel lbl :: k + | Mgoto lbl => + Pb lbl :: k + | Mcond cond args lbl => + transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k) + | Mreturn => + loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: k) + end. + +Definition transl_code (f: Mach.function) (il: list Mach.instruction) := + List.fold_right (transl_instr f) nil il. + +(** Translation of a whole function. Note that we must check + that the generated code contains less than [2^32] instructions, + otherwise the offset part of the [PC] code pointer could wrap + around, leading to incorrect executions. *) + +Definition transl_function (f: Mach.function) := + Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: + transl_code f f.(fn_code). + +Fixpoint code_size (c: code) : Z := + match c with + | nil => 0 + | instr :: c' => code_size c' + 1 + end. + +Open Local Scope string_scope. + +Definition transf_function (f: Mach.function) : res Asm.code := + let c := transl_function f in + if zlt Int.max_unsigned (code_size c) + then Errors.Error (msg "code size exceeded") + else Errors.OK c. + +Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Mach.program) : res Asm.program := + transform_partial_program transf_fundef p. + -- cgit