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

2 files changed, 32 insertions, 120 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 6fbfacd..e6e8cc2 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -184,91 +184,6 @@ Proof.
   intros; unfold print. destruct (printer prog); auto. 
 Qed.
 
-Lemma map_partial_compose:
-  forall (X A B C: Type)
-         (ctx: X -> errmsg)
-         (f1: A -> res B) (f2: B -> res C)
-         (pa: list (X * A)) (pc: list (X * C)),
-  map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
-  { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }.
-Proof.
-  induction pa; simpl.
-  intros. inv H. econstructor; eauto.
-  intro pc. destruct a as [x a].
-  destruct (f1 a) as [] _eqn; simpl; try congruence.
-  destruct (f2 b) as [] _eqn; simpl; try congruence.
-  destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence.
-  intros. inv H.
-  destruct (IHpa l) as [pb [P Q]]; auto.
-  rewrite P; simpl.
-  econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto.
-Qed.
-
-Lemma transform_partial_program_compose:
-  forall (A B C V: Type)
-         (f1: A -> res B) (f2: B -> res C)
-         (pa: program A V) (pc: program C V),
-  transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
-  { pb | transform_partial_program f1 pa = OK pb /\
-         transform_partial_program f2 pb = OK pc }.
-Proof.
-  intros. unfold transform_partial_program in H. 
-  destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn;
-  simpl in H; inv H.
-  destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]].
-  exists (mkprogram xb (prog_main pa) (prog_vars pa)); split.
-  unfold transform_partial_program. rewrite P; auto. 
-  unfold transform_partial_program. simpl. rewrite Q; auto.
-Qed.
-
-Lemma transform_program_partial_program:
-  forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V),
-  transform_partial_program (fun x => OK (f x)) p = OK tp ->
-  transform_program f p = tp.
-Proof.
-  intros until tp. unfold transform_partial_program. 
-  rewrite map_partial_total. simpl. intros. inv H. auto. 
-Qed.
-
-Lemma transform_program_compose:
-  forall (A B C V: Type)
-         (f1: A -> res B) (f2: B -> C)
-         (pa: program A V) (pc: program C V),
-  transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
-  { pb | transform_partial_program f1 pa = OK pb /\
-         transform_program f2 pb = pc }.
-Proof.
-  intros. 
-  replace (fun f : A => f1 f @@ f2)
-     with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _  _ H) as [pb [X Y]].
-  exists pb; split. auto. 
-  apply transform_program_partial_program. auto. 
-  apply extensionality; intro. destruct(f1 x); auto. 
-Qed.
-
-Lemma transform_partial_program_identity:
-  forall (A V: Type) (pa pb: program A V),
-  transform_partial_program (@OK A) pa = OK pb ->
-  pa = pb.
-Proof.
-  intros until pb. unfold transform_partial_program. 
-  replace (@OK A) with (fun b => @OK A b).
-  rewrite map_partial_identity. simpl. destruct pa; simpl; congruence.
-  apply extensionality; auto. 
-Qed.
-
-Lemma transform_program_print_identity:
-  forall (A V: Type) (p: program A V) (f: A -> unit),
-  transform_program (print f) p = p.
-Proof.
-  intros until f. unfold transform_program, transf_program. 
-  destruct p; simpl; f_equal. 
-  transitivity (map (fun x => x) prog_funct). 
-  apply list_map_exten; intros. destruct x; simpl. rewrite print_identity. auto.
-  apply list_map_identity.
-Qed.
-
 Lemma compose_print_identity:
   forall (A: Type) (x: res A) (f: A -> unit), 
   x @@ print f = x.
@@ -290,18 +205,6 @@ Qed.
 
 These results establish the correctness of the whole compiler! *)
 
-Ltac TransfProgInv :=
-  match goal with
-  | [ H: transform_partial_program (fun f => _ @@@ _) _ = OK _ |- _ ] =>
-      let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
-      destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
-      clear H
-  | [ H: transform_partial_program (fun f => _ @@ _) _ = OK _ |- _ ] =>
-      let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
-      destruct (transform_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
-      clear H
-  end.
-
 Theorem transf_rtl_program_correct:
   forall p tp,
   transf_rtl_program p = OK tp ->
diff --git a/driver/Interp.ml b/driver/Interp.ml
index fc0526a..9031042 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -87,9 +87,11 @@ let print_event p = function
 let name_of_fundef prog fd =
   let rec find_name = function
   | [] -> "<unknown function>"
-  | (id, fd') :: rem ->
+  | (id, Gfun fd') :: rem ->
       if fd = fd' then extern_atom id else find_name rem
-  in find_name prog.prog_funct
+  | (id, Gvar v) :: rem ->
+      find_name rem
+  in find_name prog.prog_defs
 
 let name_of_function prog fn =
   name_of_fundef prog (Internal fn)
@@ -468,11 +470,13 @@ let rec explore p prog ge time ss =
 (* Massaging the source program *)
 
 let unvolatile prog =
-  let unvolatile_globvar (id, gv) =
-    (id, if gv.gvar_volatile
-         then {gv with gvar_readonly = false; gvar_volatile = false}
-         else gv) in
-  {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
+  let unvolatile_globdef = function
+  | (id, Gvar gv) ->
+      (id, Gvar(if gv.gvar_volatile
+                then {gv with gvar_readonly = false; gvar_volatile = false}
+                else gv))
+  | idfd -> idfd in
+  {prog with prog_defs = List.map unvolatile_globdef prog.prog_defs}
 
 let change_main_function p old_main old_main_ty =
   let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in
@@ -483,24 +487,29 @@ let change_main_function p old_main old_main_ty =
   let new_main_fn =
     { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in
   let new_main_id = intern_string "___main" in
-  { p with
-    prog_main = new_main_id;
-    prog_funct = (new_main_id, Internal new_main_fn) :: p.prog_funct }
+  { prog_main = new_main_id;
+    prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs }
+
+let rec find_main_function name = function
+  | [] -> None
+  | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl
+  | (id, Gvar v) :: gdl -> find_main_function name gdl
 
 let fixup_main p =
-  try
-    match type_of_fundef (List.assoc p.prog_main p.prog_funct) with
-    | Tfunction(Tnil, Tint(I32, Signed, _)) ->
-        Some p
-    | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
-                Tint _) as ty ->
-        Some (change_main_function p p.prog_main ty)
-    | _ ->
-        fprintf err_formatter "ERROR: wrong type for main() function";
-        None
-  with Not_found ->
-    fprintf err_formatter "ERROR: no main() function";
-    None
+  match find_main_function p.prog_main p.prog_defs with
+  | None ->
+      fprintf err_formatter "ERROR: no main() function";
+      None
+  | Some main_fd ->
+      match type_of_fundef main_fd with
+      | Tfunction(Tnil, Tint(I32, Signed, _)) ->
+          Some p
+      | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
+                  Tint _) as ty ->
+          Some (change_main_function p p.prog_main ty)
+      | _ ->
+          fprintf err_formatter "ERROR: wrong type for main() function";
+          None
 
 (* Execution of a whole program *)