diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-02 15:12:27 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-02 15:12:27 +0000 |
commit | 6a989706fd7fd4a29418c1c6711e2736382cdb8a (patch) | |
tree | 0216afc78b8946153554708b55a3cd4f2e4064c5 /backend/Cminorgen.v | |
parent | 53ff175479ca9993c4c57e3bb71c527b9c2a5053 (diff) | |
download | compcert-kvx-6a989706fd7fd4a29418c1c6711e2736382cdb8a.tar.gz compcert-kvx-6a989706fd7fd4a29418c1c6711e2736382cdb8a.zip |
Revu gestion des variables globales dans Csharpminor
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@30 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Cminorgen.v')
-rw-r--r-- | backend/Cminorgen.v | 94 |
1 files changed, 60 insertions, 34 deletions
diff --git a/backend/Cminorgen.v b/backend/Cminorgen.v index 032b287f..eeb7b7c8 100644 --- a/backend/Cminorgen.v +++ b/backend/Cminorgen.v @@ -120,49 +120,61 @@ Definition make_store (chunk: memory_chunk) (e1 e2: expr): expr := 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] denotes a global variable, stored in - the global symbol with the same name. *) + 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: var_info. + | Var_global_scalar: memory_chunk -> var_info + | Var_global_array: var_info. -Definition compilenv := PMap.t var_info. +Definition compilenv := PTree.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_stack_array ofs => None - | Var_global => None + match PTree.get id cenv with + | Some(Var_local chunk) => + Some(Evar id) + | Some(Var_stack_scalar chunk ofs) => + Some(make_load chunk (make_stackaddr ofs)) + | Some(Var_global_scalar chunk) => + Some(make_load chunk (make_globaladdr id)) + | _ => + None end. Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option expr := - match PMap.get id cenv with - | Var_local chunk => Some(Eassign id (make_cast chunk rhs)) - | Var_stack_scalar chunk ofs => + match PTree.get id cenv with + | Some(Var_local chunk) => + Some(Eassign id (make_cast chunk rhs)) + | Some(Var_stack_scalar chunk ofs) => Some(make_store chunk (make_stackaddr ofs) rhs) - | Var_stack_array ofs => None - | Var_global => None + | Some(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) - | Var_global => Some (Eop (Oaddrsymbol id Int.zero) Enil) + match PTree.get id cenv with + | Some(Var_stack_scalar chunk ofs) => Some (make_stackaddr ofs) + | Some(Var_stack_array ofs) => Some (make_stackaddr ofs) + | Some(Var_global_scalar chunk) => Some (make_globaladdr id) + | Some(Var_global_array) => Some (make_globaladdr id) + | _ => None end. (** The translation from Csharpminor to Cminor can fail, which we @@ -314,25 +326,25 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := Definition assign_variable (atk: Identset.t) - (id_lv: ident * local_variable) + (id_lv: ident * variable_info) (cenv_stacksize: compilenv * Z) : compilenv * Z := let (cenv, stacksize) := cenv_stacksize in match id_lv with - | (id, LVarray sz) => + | (id, Varray sz) => let ofs := align stacksize 8 in - (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) - | (id, LVscalar chunk) => + (PTree.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) + (PTree.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) else - (PMap.set id (Var_local chunk) cenv, stacksize) + (PTree.set id (Var_local chunk) cenv, stacksize) end. Fixpoint assign_variables (atk: Identset.t) - (id_lv_list: list (ident * local_variable)) + (id_lv_list: list (ident * variable_info)) (cenv_stacksize: compilenv * Z) {struct id_lv_list}: compilenv * Z := match id_lv_list with @@ -341,11 +353,23 @@ Fixpoint assign_variables assign_variables atk rem (assign_variable atk id_lv cenv_stacksize) end. -Definition build_compilenv (f: Csharpminor.function) : compilenv * Z := +Definition build_compilenv + (globenv: compilenv) (f: Csharpminor.function) : compilenv * Z := assign_variables (addr_taken_stmt f.(Csharpminor.fn_body)) (fn_variables f) - (PMap.init Var_global, 0). + (globenv, 0). + +Definition assign_global_variable + (ce: compilenv) (id_vi: ident * variable_info) : compilenv := + match id_vi with + | (id, Vscalar chunk) => PTree.set id (Var_global_scalar chunk) ce + | (id, Varray sz) => PTree.set id Var_global_array ce + end. + +Definition build_global_compilenv (p: Csharpminor.program) : compilenv := + List.fold_left assign_global_variable + p.(prog_vars) (PTree.empty var_info). (** Function parameters whose address is taken must be stored in their stack slots at function entry. (Cminor passes these parameters in @@ -357,11 +381,11 @@ Fixpoint store_parameters match params with | nil => Sskip | (id, chunk) :: rem => - match PMap.get id cenv with - | Var_local chunk => + match PTree.get id cenv with + | Some(Var_local chunk) => Sseq (Sexpr (Eassign id (make_cast chunk (Evar id)))) (store_parameters cenv rem) - | Var_stack_scalar chunk ofs => + | Some(Var_stack_scalar chunk ofs) => Sseq (Sexpr (make_store chunk (make_stackaddr ofs) (Evar id))) (store_parameters cenv rem) | _ => @@ -374,8 +398,9 @@ Fixpoint store_parameters otherwise address computations within the stack block could overflow machine arithmetic and lead to incorrect code. *) -Definition transl_function (f: Csharpminor.function): option function := - let (cenv, stacksize) := build_compilenv f in +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 @@ -387,4 +412,5 @@ Definition transl_function (f: Csharpminor.function): option function := else None. Definition transl_program (p: Csharpminor.program) : option program := - transform_partial_program transl_function p. + let gce := build_global_compilenv p in + transform_partial_program (transl_function gce) (program_of_program p). |