From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: 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 --- cfrontend/C2C.ml | 51 ++++++++++++++++++++++------------------------ cfrontend/Cminorgen.v | 22 ++++++++++---------- cfrontend/Cminorgenproof.v | 46 +++++++++++++++++++++++------------------ cfrontend/Cshmgen.v | 12 +++++++++-- cfrontend/Cshmgenproof.v | 37 ++++++++------------------------- cfrontend/PrintClight.ml | 25 ++++++++++++----------- cfrontend/PrintCsyntax.ml | 27 ++++++++++++------------ 7 files changed, 106 insertions(+), 114 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c659b86..2cdcc03 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -137,8 +137,8 @@ let global_for_string s id = :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; - (id, {gvar_info = typeStringLiteral s; gvar_init = !init; - gvar_readonly = true; gvar_volatile = false}) + (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; + gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = Hashtbl.fold @@ -155,7 +155,7 @@ let register_special_external name ef targs tres = let declare_special_externals k = Hashtbl.fold - (fun name fd k -> (intern_string name, fd) :: k) + (fun name fd k -> (intern_string name, Gfun fd) :: k) special_externals_table k (** ** Handling of stubs for variadic functions *) @@ -709,8 +709,8 @@ let convertFundef env fd = a_sections = Sections.for_function env id' fd.fd_ret; a_small_data = false; a_inline = fd.fd_inline }; - (id', Internal {fn_return = ret; fn_params = params; - fn_vars = vars; fn_body = body'}) + (id', Gfun(Internal {fn_return = ret; fn_params = params; + fn_vars = vars; fn_body = body'})) (** External function declaration *) @@ -727,7 +727,7 @@ let convertFundecl env (sto, id, ty, optinit) = if List.mem_assoc id.name builtins.functions then EF_builtin(id', sg) else EF_external(id', sg) in - (id', External(ef, args, res)) + (id', Gfun(External(ef, args, res))) (** Initializers *) @@ -788,8 +788,8 @@ let convertGlobvar env (sto, id, ty, optinit) = a_inline = false }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in - (id', {gvar_info = ty'; gvar_init = init'; - gvar_readonly = readonly; gvar_volatile = volatile}) + (id', Gvar {gvar_info = ty'; gvar_init = init'; + gvar_readonly = readonly; gvar_volatile = volatile}) (** Sanity checks on composite declarations. *) @@ -803,13 +803,12 @@ let checkComposite env si id attr flds = in List.iter checkField flds (** Convert a list of global declarations. - Result is a pair [(funs, vars)] where [funs] are - the function definitions (internal and external) - and [vars] the variable declarations. *) + Result is a list of CompCert C global declarations (functions + + variables). *) -let rec convertGlobdecls env funs vars gl = +let rec convertGlobdecls env res gl = match gl with - | [] -> (List.rev funs, List.rev vars) + | [] -> List.rev res | g :: gl' -> updateLoc g.gloc; match g.gdesc with @@ -819,29 +818,29 @@ let rec convertGlobdecls env funs vars gl = Other types become variable declarations. *) begin match Cutil.unroll env ty with | TFun(_, Some _, false, _) -> - convertGlobdecls env (convertFundecl env d :: funs) vars gl' + convertGlobdecls env (convertFundecl env d :: res) gl' | TFun(_, None, false, _) -> error "function declaration without prototype"; - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | TFun(_, _, true, _) -> - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | _ -> - convertGlobdecls env funs (convertGlobvar env d :: vars) gl' + convertGlobdecls env (convertGlobvar env d :: res) gl' end | C.Gfundef fd -> - convertGlobdecls env (convertFundef env fd :: funs) vars gl' + convertGlobdecls env (convertFundef env fd :: res) gl' | C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ -> (* typedefs are unrolled, structs are expanded inline, and enum tags are folded. So we just skip their declarations. *) - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | C.Gcompositedef(su, id, attr, flds) -> (* sanity checks on fields *) checkComposite env su id attr flds; - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then warning ("'#pragma " ^ s ^ "' directive ignored"); - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' (** Build environment of typedefs and structs *) @@ -921,14 +920,12 @@ let convertProgram p = Hashtbl.clear special_externals_table; let p = Builtins.declarations() @ p in try - let (funs1, vars1) = - convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in - let funs2 = declare_special_externals funs1 in - let vars2 = globals_for_strings vars1 in + let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in + let gl2 = declare_special_externals gl1 in + let gl3 = globals_for_strings gl2 in if !numErrors > 0 then None - else Some { AST.prog_funct = funs2; - AST.prog_vars = vars2; + else Some { AST.prog_defs = gl3; AST.prog_main = intern_string "main" } with Env.Error msg -> error (Env.error_message msg); None diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 2c02813..a47efb2 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -565,19 +565,19 @@ Definition build_compilenv (fn_variables f) (globenv, 0). -Definition assign_global_variable - (ce: compilenv) (info: ident * globvar var_kind) : compilenv := - match info with - | (id, mkglobvar vk _ _ _) => - PMap.set id (match vk with Vscalar chunk => Var_global_scalar chunk - | Varray _ _ => Var_global_array - end) - ce - end. +Definition assign_global_def + (ce: compilenv) (gdef: ident * globdef Csharpminor.fundef var_kind) : compilenv := + let (id, gd) := gdef in + let kind := + match gd with + | Gvar (mkglobvar (Vscalar chunk) _ _ _) => Var_global_scalar chunk + | Gvar (mkglobvar (Varray _ _) _ _ _) => Var_global_array + | Gfun f => Var_global_array + end in + PMap.set id kind ce. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := - List.fold_left assign_global_variable - p.(prog_vars) (PMap.init Var_global_array). + List.fold_left assign_global_def p.(prog_defs) (PMap.init Var_global_array). (** * Translation of functions *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 0fa9ac0..42f54b3 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -109,23 +109,28 @@ Lemma global_compilenv_charact: Proof. assert (A: forall ge, global_compilenv_match (PMap.init Var_global_array) ge). intros; red; intros. rewrite PMap.gi. auto. - assert (B: forall ce ge v, + assert (B: forall ce ge idg, global_compilenv_match ce ge -> - global_compilenv_match (assign_global_variable ce v) - (Genv.add_variable ge v)). - intros; red; intros. destruct v as [id1 [info1 init1 ro1 vo1]]. - unfold assign_global_variable, Genv.find_symbol, Genv.find_var_info; simpl. - rewrite PMap.gsspec. destruct (peq id id1). subst id. + global_compilenv_match (assign_global_def ce idg) + (Genv.add_global ge idg)). + intros; red; intros. unfold assign_global_def. + destruct idg as [id1 gd]. rewrite PMap.gsspec. destruct (peq id id1). + (* same var *) + subst id1. destruct gd as [f | [info1 init1 ro1 vo1]]. auto. destruct info1; auto. - rewrite PTree.gss. intros. inv H0. rewrite ZMap.gss in H1. inv H1. auto. - generalize (H id). destruct (ce!!id); auto. - rewrite PTree.gso; auto. intros. rewrite ZMap.gso in H2. eapply H0; eauto. + unfold Genv.find_symbol, Genv.find_var_info. simpl; intros. + rewrite PTree.gss in H0. inv H0. rewrite ZMap.gss in H1. inv H1; auto. + (* different var *) + generalize (H id). unfold Genv.find_symbol, Genv.find_var_info. simpl. intros. + destruct (ce!!id); auto. intros. + rewrite PTree.gso in H1; auto. + destruct gd as [f|v]. eauto. rewrite ZMap.gso in H2. eauto. exploit Genv.genv_symb_range; eauto. unfold block, ZIndexed.t; omega. - assert (C: forall vl ce ge, + assert (C: forall gl ce ge, global_compilenv_match ce ge -> - global_compilenv_match (fold_left assign_global_variable vl ce) - (Genv.add_variables ge vl)). - induction vl; simpl; intros. auto. apply IHvl. apply B. auto. + global_compilenv_match (fold_left assign_global_def gl ce) + (Genv.add_globals ge gl)). + induction gl; simpl; intros. auto. apply IHgl. apply B. auto. unfold gce, build_global_compilenv, ge, Genv.globalenv. apply C. apply A. @@ -680,7 +685,8 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop := (DOMAIN: forall b, b < bound -> f b = Some(b, 0)) (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). (** Matching of call stacks imply: - matching of environments for each of the frames @@ -1132,7 +1138,7 @@ Remark inj_preserves_globals: Proof. intros. inv H. split. intros. apply DOMAIN. eapply SYMBOLS. eauto. - split. intros. apply DOMAIN. eapply INFOS. eauto. + split. intros. apply DOMAIN. eapply VARINFOS. eauto. intros. symmetry. eapply IMAGE; eauto. Qed. @@ -2822,16 +2828,15 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := Remark val_inject_function_pointer: forall bound v fd f tv, - Genv.find_funct tge v = Some fd -> + Genv.find_funct ge v = Some fd -> match_globalenvs f bound -> val_inject f v tv -> tv = v. Proof. intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite Genv.find_funct_find_funct_ptr in H. - assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto. - assert (f b = Some(b, 0)). inv H0. apply DOMAIN. omega. - inv H1. rewrite H3 in H6; inv H6. reflexivity. + rewrite Genv.find_funct_find_funct_ptr in H. + assert (f b = Some(b, 0)). inv H0. apply DOMAIN. eapply FUNCTIONS; eauto. + inv H1. rewrite H2 in H5; inv H5. reflexivity. Qed. Lemma match_call_cont: @@ -3426,6 +3431,7 @@ Proof. intros. unfold Mem.flat_inj in H0. destruct (zlt b1 (Mem.nextblock m)); congruence. intros. eapply Genv.find_symbol_not_fresh; eauto. + intros. eapply Genv.find_funct_ptr_not_fresh; eauto. intros. eapply Genv.find_var_info_not_fresh; eauto. Qed. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c5e9b8d..a459297 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -546,8 +546,16 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) Definition prefix_var_name (id: ident) : errmsg := MSG "In local variable " :: CTX id :: MSG ": " :: nil. -Definition transl_vars (l: list (ident * type)) := - AST.map_partial prefix_var_name var_kind_of_type l. +Fixpoint transl_vars (l: list (ident * type)) : res (list (ident * var_kind)) := + match l with + | nil => OK nil + | (id, ty) :: l' => + match var_kind_of_type ty with + | Error msg => Error (MSG "In local variable " :: CTX id :: MSG ": " :: msg) + | OK vk => + do tl' <- transl_vars l'; OK ((id, vk) :: tl') + end + end. Definition transl_function (f: Clight.function) : res function := do tparams <- transl_vars (Clight.fn_params f); diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 9f73467..2f319d0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -214,39 +214,15 @@ Qed. (** * Properties of the translation functions *) -Lemma map_partial_names: - forall (A B: Type) (f: A -> res B) - (l: list (ident * A)) (tl: list (ident * B)), - map_partial prefix_var_name f l = OK tl -> - List.map (@fst ident B) tl = List.map (@fst ident A) l. -Proof. - induction l; simpl. - intros. inversion H. reflexivity. - intro tl. destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence. - inv H0. simpl. decEq. auto. -Qed. - -Lemma map_partial_append: - forall (A B: Type) (f: A -> res B) - (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)), - map_partial prefix_var_name f l1 = OK tl1 -> - map_partial prefix_var_name f l2 = OK tl2 -> - map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2). -Proof. - induction l1; intros until tl2; simpl. - intros. inversion H. simpl; auto. - destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence. - inv H0. rewrite (IHl1 _ _ _ H H1). auto. -Qed. - Lemma transl_vars_names: forall vars tvars, transl_vars vars = OK tvars -> List.map variable_name tvars = var_names vars. Proof. - exact (map_partial_names _ _ var_kind_of_type). + induction vars; simpl; intros. + monadInv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + simpl. decEq; auto. Qed. Lemma transl_names_norepet: @@ -268,7 +244,10 @@ Lemma transl_vars_append: transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). Proof. - exact (map_partial_append _ _ var_kind_of_type). + induction l1; simpl; intros. + inv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + erewrite IHl1; eauto. simpl. auto. Qed. Lemma transl_fn_variables: diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 7b9f3d3..0e8b494 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -249,7 +249,7 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (id, fd) = +let print_fundef p id fd = match fd with | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " @@ -259,6 +259,11 @@ let print_fundef p (id, fd) = | Internal f -> print_function p id f +let print_globdef p (id, gd) = + match gd with + | Gfun f -> print_fundef p id f + | Gvar v -> print_globvar p id v (* from PrintCsyntax *) + (* Collect struct and union types *) let rec collect_expr e = @@ -307,17 +312,14 @@ let collect_function f = List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; collect_stmt f.fn_body -let collect_fundef (id, fd) = - match fd with - | External(_, args, res) -> collect_type_list args; collect_type res - | Internal f -> collect_function f - -let collect_globvar (id, v) = - collect_type v.gvar_info +let collect_globdef (id, gd) = + match gd with + | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(Internal f) -> collect_function f + | Gvar v -> collect_type v.gvar_info let collect_program p = - List.iter collect_globvar p.prog_vars; - List.iter collect_fundef p.prog_funct + List.iter collect_globdef p.prog_defs let declare_struct_or_union p (name, fld) = fprintf p "%s;@ @ " name @@ -338,8 +340,7 @@ let print_program p prog = fprintf p "@["; StructUnionSet.iter (declare_struct_or_union p) !struct_unions; StructUnionSet.iter (print_struct_or_union p) !struct_unions; - List.iter (print_globvar p) prog.prog_vars; - List.iter (print_fundef p) prog.prog_funct; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 5490321..7858545 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -372,7 +372,7 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (id, fd) = +let print_fundef p id fd = match fd with | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " @@ -414,7 +414,7 @@ let print_init p = function let re_string_literal = Str.regexp "__stringlit_[0-9]+" -let print_globvar p (id, v) = +let print_globvar p id v = let name1 = extern_atom id in let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in @@ -439,6 +439,11 @@ let print_globvar p (id, v) = end; fprintf p ";@]@ @ " +let print_globdef p (id, gd) = + match gd with + | Gfun f -> print_fundef p id f + | Gvar v -> print_globvar p id v + (* Collect struct and union types *) let rec collect_type = function @@ -519,17 +524,14 @@ let collect_function f = List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; collect_stmt f.fn_body -let collect_fundef (id, fd) = - match fd with - | External(_, args, res) -> collect_type_list args; collect_type res - | Internal f -> collect_function f - -let collect_globvar (id, v) = - collect_type v.gvar_info +let collect_globdef (id, gd) = + match gd with + | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(Internal f) -> collect_function f + | Gvar v -> collect_type v.gvar_info let collect_program p = - List.iter collect_globvar p.prog_vars; - List.iter collect_fundef p.prog_funct + List.iter collect_globdef p.prog_defs let declare_struct_or_union p (name, fld) = fprintf p "%s;@ @ " name @@ -550,8 +552,7 @@ let print_program p prog = fprintf p "@["; StructUnionSet.iter (declare_struct_or_union p) !struct_unions; StructUnionSet.iter (print_struct_or_union p) !struct_unions; - List.iter (print_globvar p) prog.prog_vars; - List.iter (print_fundef p) prog.prog_funct; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None -- cgit v1.2.3