From a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:33:05 +0000 Subject: Revu la repartition des sources Coq en sous-repertoires git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 433 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 433 insertions(+) create mode 100644 cfrontend/Cminorgen.v (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v new file mode 100644 index 00000000..4c611b44 --- /dev/null +++ b/cfrontend/Cminorgen.v @@ -0,0 +1,433 @@ +(** Translation from Csharpminor to Cminor. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Sets. +Require Import AST. +Require Import Integers. +Require Mem. +Require Import Csharpminor. +Require Import Op. +Require Import Cminor. +Require Cmconstr. + +(** The main task in translating Csharpminor to Cminor is to explicitly + stack-allocate local variables whose address is taken: these local + variables become sub-blocks of the Cminor stack data block for the + current function. Taking the address of such a variable becomes + a [Oaddrstack] operation with the corresponding offset. Accessing + or assigning such a variable becomes a load or store operation at + that address. Only scalar local variables whose address is never + taken in the Csharpminor code can be mapped to Cminor local + variable, since the latter do not reside in memory. + + Other tasks performed during the translation to Cminor: +- Transformation of Csharpminor's standard set of operators and + trivial addressing modes to Cminor's processor-dependent operators + and addressing modes. This is done using the optimizing Cminor + constructor functions provided in file [Cmconstr], therefore performing + instruction selection on the fly. +- Insertion of truncation, zero- and sign-extension operations when + assigning to a Csharpminor local variable of ``small'' type + (e.g. [Mfloat32] or [Mint8signed]). This is necessary to preserve + the ``normalize at assignment-time'' semantics of Csharpminor. +*) + +(** Translation of operators. *) + +Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr := + match el with + | Enil => + match op with + | Csharpminor.Ointconst n => Some(Eop (Ointconst n) Enil) + | Csharpminor.Ofloatconst n => Some(Eop (Ofloatconst n) Enil) + | _ => None + end + | Econs e1 Enil => + match op with + | Csharpminor.Ocast8unsigned => Some(Cmconstr.cast8unsigned e1) + | Csharpminor.Ocast8signed => Some(Cmconstr.cast8signed e1) + | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1) + | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1) + | Csharpminor.Onotint => Some(Cmconstr.notint e1) + | Csharpminor.Onegf => Some(Cmconstr.negfloat e1) + | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1) + | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1) + | Csharpminor.Ointoffloat => Some(Cmconstr.intoffloat e1) + | Csharpminor.Ofloatofint => Some(Cmconstr.floatofint e1) + | Csharpminor.Ofloatofintu => Some(Cmconstr.floatofintu e1) + | _ => None + end + | Econs e1 (Econs e2 Enil) => + match op with + | Csharpminor.Oadd => Some(Cmconstr.add e1 e2) + | Csharpminor.Osub => Some(Cmconstr.sub e1 e2) + | Csharpminor.Omul => Some(Cmconstr.mul e1 e2) + | Csharpminor.Odiv => Some(Cmconstr.divs e1 e2) + | Csharpminor.Odivu => Some(Cmconstr.divu e1 e2) + | Csharpminor.Omod => Some(Cmconstr.mods e1 e2) + | Csharpminor.Omodu => Some(Cmconstr.modu e1 e2) + | Csharpminor.Oand => Some(Cmconstr.and e1 e2) + | Csharpminor.Oor => Some(Cmconstr.or e1 e2) + | Csharpminor.Oxor => Some(Cmconstr.xor e1 e2) + | Csharpminor.Oshl => Some(Cmconstr.shl e1 e2) + | Csharpminor.Oshr => Some(Cmconstr.shr e1 e2) + | Csharpminor.Oshru => Some(Cmconstr.shru e1 e2) + | Csharpminor.Oaddf => Some(Cmconstr.addf e1 e2) + | Csharpminor.Osubf => Some(Cmconstr.subf e1 e2) + | Csharpminor.Omulf => Some(Cmconstr.mulf e1 e2) + | Csharpminor.Odivf => Some(Cmconstr.divf e1 e2) + | Csharpminor.Ocmp c => Some(Cmconstr.cmp c e1 e2) + | Csharpminor.Ocmpu c => Some(Cmconstr.cmpu c e1 e2) + | Csharpminor.Ocmpf c => Some(Cmconstr.cmpf c e1 e2) + | _ => None + end + | _ => None + end. + +(** [make_cast chunk e] returns a Cminor expression that normalizes + the value of Cminor expression [e] as prescribed by the memory chunk + [chunk]. For instance, 8-bit sign extension is performed if + [chunk] is [Mint8signed]. *) + +Definition make_cast (chunk: memory_chunk) (e: expr): expr := + match chunk with + | Mint8signed => Cmconstr.cast8signed e + | Mint8unsigned => Cmconstr.cast8unsigned e + | Mint16signed => Cmconstr.cast16signed e + | Mint16unsigned => Cmconstr.cast16unsigned e + | Mint32 => e + | Mfloat32 => Cmconstr.singleoffloat e + | Mfloat64 => e + end. + +Definition make_load (chunk: memory_chunk) (e: expr): expr := + Cmconstr.load chunk e. + +Definition store_arg (chunk: memory_chunk) (e: expr) : expr := + match e with + | Eop op (Econs e1 Enil) => + match op with + | Ocast8signed => + match chunk with Mint8signed => e1 | _ => e end + | Ocast8unsigned => + match chunk with Mint8unsigned => e1 | _ => e end + | Ocast16signed => + match chunk with Mint16signed => e1 | _ => e end + | Ocast16unsigned => + match chunk with Mint16unsigned => e1 | _ => e end + | Osingleoffloat => + match chunk with Mfloat32 => e1 | _ => e end + | _ => e + end + | _ => e + end. + +Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt := + Sexpr(Cmconstr.store chunk e1 (store_arg chunk e2)). + +Definition make_stackaddr (ofs: Z): expr := + Eop (Oaddrstack (Int.repr ofs)) Enil. + +Definition make_globaladdr (id: ident): expr := + Eop (Oaddrsymbol id Int.zero) Enil. + +(** Compile-time information attached to each Csharpminor + variable: global variables, local variables, function parameters. + [Var_local] denotes a scalar local variable whose address is not + taken; it will be translated to a Cminor local variable of the + same name. [Var_stack_scalar] and [Var_stack_array] denote + local variables that are stored as sub-blocks of the Cminor stack + data block. [Var_global_scalar] and [Var_global_array] denote + global variables, stored in the global symbols with the same names. *) + +Inductive var_info: Set := + | Var_local: memory_chunk -> var_info + | Var_stack_scalar: memory_chunk -> Z -> var_info + | Var_stack_array: Z -> var_info + | Var_global_scalar: memory_chunk -> var_info + | Var_global_array: var_info. + +Definition compilenv := PMap.t var_info. + +(** Generation of Cminor code corresponding to accesses to Csharpminor + local variables: reads, assignments, and taking the address of. *) + +Definition var_get (cenv: compilenv) (id: ident): option expr := + match PMap.get id cenv with + | Var_local chunk => + Some(Evar id) + | Var_stack_scalar chunk ofs => + Some(make_load chunk (make_stackaddr ofs)) + | Var_global_scalar chunk => + Some(make_load chunk (make_globaladdr id)) + | _ => + None + end. + +Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt := + match PMap.get id cenv with + | Var_local chunk => + Some(Sexpr(Eassign id (make_cast chunk rhs))) + | Var_stack_scalar chunk ofs => + Some(make_store chunk (make_stackaddr ofs) rhs) + | Var_global_scalar chunk => + Some(make_store chunk (make_globaladdr id) rhs) + | _ => + None + end. + +Definition var_addr (cenv: compilenv) (id: ident): option expr := + match PMap.get id cenv with + | Var_local chunk => None + | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs) + | Var_stack_array ofs => Some (make_stackaddr ofs) + | _ => Some (make_globaladdr id) + end. + +(** The translation from Csharpminor to Cminor can fail, which we + encode by returning option types ([None] denotes error). + Propagation of errors is done in monadic style, using the following + [bind] monadic composition operator, and a [do] notation inspired + by Haskell's. *) + +Definition bind (A B: Set) (a: option A) (b: A -> option B): option B := + match a with + | None => None + | Some x => b x + end. + +Notation "'do' X <- A ; B" := (bind _ _ A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). + +(** Translation of expressions. All the hard work is done by the + [make_*] and [var_*] functions defined above. *) + +Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) + {struct e}: option expr := + match e with + | Csharpminor.Evar id => var_get cenv id + | Csharpminor.Eaddrof id => var_addr cenv id + | Csharpminor.Eop op el => + do tel <- transl_exprlist cenv el; make_op op tel + | Csharpminor.Eload chunk e => + do te <- transl_expr cenv e; Some (make_load chunk te) + | Csharpminor.Ecall sig e el => + do te <- transl_expr cenv e; + do tel <- transl_exprlist cenv el; + Some (Ecall sig te tel) + | Csharpminor.Econdition e1 e2 e3 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + do te3 <- transl_expr cenv e3; + Some (Cmconstr.conditionalexpr te1 te2 te3) + | Csharpminor.Elet e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + Some (Elet te1 te2) + | Csharpminor.Eletvar n => + Some (Eletvar n) + | Csharpminor.Ealloc e => + do te <- transl_expr cenv e; + Some (Ealloc te) + end + +with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist) + {struct el}: option exprlist := + match el with + | Csharpminor.Enil => + Some Enil + | Csharpminor.Econs e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_exprlist cenv e2; + Some (Econs te1 te2) + end. + +(** Translation of statements. Entirely straightforward. *) + +Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) + {struct s}: option stmt := + match s with + | Csharpminor.Sskip => + Some Sskip + | Csharpminor.Sexpr e => + do te <- transl_expr cenv e; Some(Sexpr te) + | Csharpminor.Sassign id e => + do te <- transl_expr cenv e; var_set cenv id te + | Csharpminor.Sstore chunk e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + Some (make_store chunk te1 te2) + | Csharpminor.Sseq s1 s2 => + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; + Some (Sseq ts1 ts2) + | Csharpminor.Sifthenelse e s1 s2 => + do te <- transl_expr cenv e; + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; + Some (Cmconstr.ifthenelse te ts1 ts2) + | Csharpminor.Sloop s => + do ts <- transl_stmt cenv s; + Some (Sloop ts) + | Csharpminor.Sblock s => + do ts <- transl_stmt cenv s; + Some (Sblock ts) + | Csharpminor.Sexit n => + Some (Sexit n) + | Csharpminor.Sswitch e cases default => + do te <- transl_expr cenv e; Some(Sswitch te cases default) + | Csharpminor.Sreturn None => + Some (Sreturn None) + | Csharpminor.Sreturn (Some e) => + do te <- transl_expr cenv e; Some (Sreturn (Some te)) + end. + +(** Computation of the set of variables whose address is taken in + a piece of Csharpminor code. *) + +Module Identset := MakeSet(PTree). + +Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := + match e with + | Csharpminor.Evar id => Identset.empty + | Csharpminor.Eaddrof id => Identset.add id Identset.empty + | Csharpminor.Eop op el => addr_taken_exprlist el + | Csharpminor.Eload chunk e => addr_taken_expr e + | Csharpminor.Ecall sig e el => + Identset.union (addr_taken_expr e) (addr_taken_exprlist el) + | Csharpminor.Econdition e1 e2 e3 => + Identset.union (addr_taken_expr e1) + (Identset.union (addr_taken_expr e2) (addr_taken_expr e3)) + | Csharpminor.Elet e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_expr e2) + | Csharpminor.Eletvar n => Identset.empty + | Csharpminor.Ealloc e => addr_taken_expr e + end + +with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t := + match e with + | Csharpminor.Enil => Identset.empty + | Csharpminor.Econs e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_exprlist e2) + end. + +Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := + match s with + | Csharpminor.Sskip => Identset.empty + | Csharpminor.Sexpr e => addr_taken_expr e + | Csharpminor.Sassign id e => addr_taken_expr e + | Csharpminor.Sstore chunk e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_expr e2) + | Csharpminor.Sseq s1 s2 => + Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2) + | Csharpminor.Sifthenelse e s1 s2 => + Identset.union (addr_taken_expr e) + (Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2)) + | Csharpminor.Sloop s => addr_taken_stmt s + | Csharpminor.Sblock s => addr_taken_stmt s + | Csharpminor.Sexit n => Identset.empty + | Csharpminor.Sswitch e cases default => addr_taken_expr e + | Csharpminor.Sreturn None => Identset.empty + | Csharpminor.Sreturn (Some e) => addr_taken_expr e + end. + +(** Layout of the Cminor stack data block and construction of the + compilation environment. Csharpminor local variables that are + arrays or whose address is taken are allocated a slot in the Cminor + stack data. While this is not important for correctness, sufficient + padding is inserted to ensure adequate alignment of addresses. *) + +Definition assign_variable + (atk: Identset.t) + (id_lv: ident * var_kind) + (cenv_stacksize: compilenv * Z) : compilenv * Z := + let (cenv, stacksize) := cenv_stacksize in + match id_lv with + | (id, Varray sz) => + let ofs := align stacksize 8 in + (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) + | (id, Vscalar chunk) => + if Identset.mem id atk then + let sz := Mem.size_chunk chunk in + let ofs := align stacksize sz in + (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) + else + (PMap.set id (Var_local chunk) cenv, stacksize) + end. + +Fixpoint assign_variables + (atk: Identset.t) + (id_lv_list: list (ident * var_kind)) + (cenv_stacksize: compilenv * Z) + {struct id_lv_list}: compilenv * Z := + match id_lv_list with + | nil => cenv_stacksize + | id_lv :: rem => + assign_variables atk rem (assign_variable atk id_lv cenv_stacksize) + end. + +Definition build_compilenv + (globenv: compilenv) (f: Csharpminor.function) : compilenv * Z := + assign_variables + (addr_taken_stmt f.(Csharpminor.fn_body)) + (fn_variables f) + (globenv, 0). + +Definition assign_global_variable + (ce: compilenv) (info: ident * var_kind * list init_data) : compilenv := + match info with + | (id, Vscalar chunk, _) => PMap.set id (Var_global_scalar chunk) ce + | (id, Varray _, _) => PMap.set id Var_global_array ce + end. + +Definition build_global_compilenv (p: Csharpminor.program) : compilenv := + List.fold_left assign_global_variable + p.(prog_vars) (PMap.init Var_global_array). + +(** Function parameters whose address is taken must be stored in their + stack slots at function entry. (Cminor passes these parameters in + local variables.) *) + +Fixpoint store_parameters + (cenv: compilenv) (params: list (ident * memory_chunk)) + {struct params} : stmt := + match params with + | nil => Sskip + | (id, chunk) :: rem => + match PMap.get id cenv with + | Var_local chunk => + Sseq (Sexpr (Eassign id (make_cast chunk (Evar id)))) + (store_parameters cenv rem) + | Var_stack_scalar chunk ofs => + Sseq (make_store chunk (make_stackaddr ofs) (Evar id)) + (store_parameters cenv rem) + | _ => + Sskip (* should never happen *) + end + end. + +(** Translation of a Csharpminor function. We must check that the + required Cminor stack block is no bigger than [Int.max_signed], + otherwise address computations within the stack block could + overflow machine arithmetic and lead to incorrect code. *) + +Definition transl_function + (gce: compilenv) (f: Csharpminor.function): option function := + let (cenv, stacksize) := build_compilenv gce f in + if zle stacksize Int.max_signed then + do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); + Some (mkfunction + (Csharpminor.fn_sig f) + (Csharpminor.fn_params_names f) + (Csharpminor.fn_vars_names f) + stacksize + (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody)) + else None. + +Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef := + transf_partial_fundef (transl_function gce) f. + +Definition transl_program (p: Csharpminor.program) : option program := + let gce := build_global_compilenv p in + transform_partial_program (transl_fundef gce) (program_of_program p). -- cgit