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

7 files changed, 106 insertions, 114 deletions

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 "@[<v 0>";
   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 "@[<v 0>";
   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