diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
commit | ce4951549999f403446415c135ad1403a16a15c3 (patch) | |
tree | cac9bbb2fea29fce331916b277c38ed8fe29e471 /backend/Inlining.v | |
parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
download | compcert-ce4951549999f403446415c135ad1403a16a15c3.tar.gz compcert-ce4951549999f403446415c135ad1403a16a15c3.zip |
Globalenvs: allocate one-byte block with permissions Nonempty for each
function definition, so that comparisons between function pointers
are correctly defined.
AST, Globalenvs, and many other files:
represent programs as a list of (function or variable) definitions
instead of two lists, one for functions and the other for variables.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Inlining.v')
-rw-r--r-- | backend/Inlining.v | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index 406447b7..3ddfe9a4 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -28,7 +28,7 @@ Ltac xomega := unfold Plt, Ple in *; zify; omega. (** ** Environment of inlinable functions *) (** We maintain a mapping from function names to their definitions. - In this mapping, we only include functions that are eligible for + In this mapping, we only include internal functions that are eligible for inlining, as determined by the external heuristic [should_inline]. *) @@ -38,22 +38,18 @@ Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv. Parameter should_inline: ident -> function -> bool. -Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv := - match idf with - | (id, External ef) => - PTree.remove id fenv - | (id, Internal f) => +Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funenv := + match idg with + | (id, Gfun (Internal f)) => if should_inline id f then PTree.set id f fenv else PTree.remove id fenv + | (id, _) => + PTree.remove id fenv end. -Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv := - PTree.remove (fst idv) fenv. - Definition funenv_program (p: program) : funenv := - List.fold_left remove_vardef p.(prog_vars) - (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)). + List.fold_left add_globdef p.(prog_defs) (PTree.empty function). (** Resources used by a function. *) |