Honor "static" modifier on C globals.

Put "const" globals in read-only section.
Revised printing of rlwinm instruction.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1018 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 104 insertions, 32 deletions

diff --git a/Changelog b/Changelog
index e3deb96..3e6840d 100644
--- a/Changelog
+++ b/Changelog
@@ -13,6 +13,8 @@ Release 1.4,
 - Clight: added support for conditional expressions (a ? b : c);
   removed support for array accesses a[i], now a derived form.
 
+- C front-end: honor "static" modifiers on globals.
+
 - New optimization over RTL: turning calls into tail calls when possible.
 
 - Instruction selection pass: elimination of redundant casts following
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index e5ef64a..e9feb53 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -23,6 +23,10 @@ open Camlcoq
 open AST
 open Csyntax
 
+(* To associate CIL varinfo to the atoms representing global variables *)
+
+let varinfo_atom : (BinPos.positive, Cil.varinfo) Hashtbl.t =
+  Hashtbl.create 103
 
 
 
@@ -48,7 +52,6 @@ let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32)
 
 (** Global variables *)
 let currentLocation = ref Cil.locUnknown
-let currentGlobalPrefix = ref ""
 let stringNum = ref 0   (* number of next global for string literals *)
 let stringTable = Hashtbl.create 47
 
@@ -132,17 +135,21 @@ let warning msg =
   prerr_endline msg
 
 (** ** Functions used to handle string literals *)
+
 let name_for_string_literal s =
   try
     Hashtbl.find stringTable s
   with Not_found ->
     incr stringNum;
-    let symbol_name =
-      Printf.sprintf "_%s__stringlit_%d"
-                     !currentGlobalPrefix !stringNum in
-    let symbol_ident = intern_string symbol_name in
-    Hashtbl.add stringTable s symbol_ident;
-    symbol_ident
+    let name = Printf.sprintf "__stringlit_%d" !stringNum in
+    let id = intern_string name in
+    let v =
+      makeVarinfo true s (typeAddAttributes [Attr("const",[])] charPtrType) in
+    v.vstorage <- Static;
+    v.vreferenced <- true;
+    Hashtbl.add varinfo_atom id v;
+    Hashtbl.add stringTable s id;
+    id
 
 let typeStringLiteral s =
   Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1)))
@@ -737,8 +744,10 @@ let convertGFun fdec =
            unsupported "the return type of main() must be an integer type"
   end;
   current_function := None;
+  let id = intern_string v.vname in
+  Hashtbl.add varinfo_atom id v;
   Datatypes.Coq_pair
-    (intern_string v.vname,
+    (id,
      Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
 
 (** Auxiliary for [convertInit] *)
@@ -881,6 +890,7 @@ let convertInitInfo ty info =
 let convertGVar v i =
   updateLoc(v.vdecl);
   let id = intern_string v.vname in
+  Hashtbl.add varinfo_atom id v;
   Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i),
                       convertTyp v.vtype)
 
@@ -890,6 +900,7 @@ let convertGVar v i =
 let convertExtVar v =
   updateLoc(v.vdecl);
   let id = intern_string v.vname in
+  Hashtbl.add varinfo_atom id v;
   Datatypes.Coq_pair (Datatypes.Coq_pair(id, []),
                       convertTyp v.vtype)
 
@@ -900,6 +911,7 @@ let convertExtFun v =
   match convertTyp v.vtype with
   | Tfunction(args, res) ->
       let id = intern_string v.vname in
+      Hashtbl.add varinfo_atom id v;
       Datatypes.Coq_pair (id, External(id, args, res))
   | _ ->
       assert false
@@ -970,9 +982,8 @@ let cleanupGlobals globs =
 
 (** Convert a [Cil.file] into a [CabsCoq.program] *)
 let convertFile f =
-  currentGlobalPrefix :=
-    Filename.chop_extension (Filename.basename f.fileName);
   stringNum := 0;
+  Hashtbl.clear varinfo_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear stub_function_table;
   let (funList, defList) = processGlobals (cleanupGlobals f.globals) in
@@ -989,3 +1000,26 @@ let convertFile f =
 (*-----------------------------------------------------------------------*)
 end
 
+(* Extracting information about global variables from their atom *)
+
+let atom_is_static a =
+  try
+    let v = Hashtbl.find varinfo_atom a in
+    v.vstorage = Static
+  with Not_found ->
+    false
+
+let atom_is_readonly a =
+  try
+    let v = Hashtbl.find varinfo_atom a in
+    let a = typeAttrs v.vtype in
+    if hasAttribute "volatile" a then false else
+    if hasAttribute "const" a then true else
+    match Cil.unrollType v.vtype with
+    | TArray(ty, _, _) ->
+        let a' = typeAttrs ty in
+        hasAttribute "const" a' && not (hasAttribute "volatile" a')
+    | _ -> false
+  with Not_found ->
+    false
+
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index b75d135..15b558d 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -98,12 +98,12 @@ let constant oc cst =
   | Csymbol_low(s, n) ->
       begin match target with
       | MacOS -> fprintf oc "lo16(%a)" symbol_offset (s, camlint_of_coqint n)
-      | EABI  -> fprintf oc "%a@l" symbol_offset (s, camlint_of_coqint n)
+      | EABI  -> fprintf oc "(%a)@l" symbol_offset (s, camlint_of_coqint n)
       end
   | Csymbol_high(s, n) ->
       begin match target with
       | MacOS -> fprintf oc "ha16(%a)" symbol_offset (s, camlint_of_coqint n)
-      | EABI  -> fprintf oc "%a@ha" symbol_offset (s, camlint_of_coqint n)
+      | EABI  -> fprintf oc "(%a)@ha" symbol_offset (s, camlint_of_coqint n)
       end
 
 let num_crbit = function
@@ -157,14 +157,42 @@ let creg oc r =
   | MacOS -> fprintf oc "cr%d" r
   | EABI  -> fprintf oc "%d" r
 
-let text oc =
-  fprintf oc "	.text\n"
-let data oc =
-  fprintf oc "	.data\n"
-let const oc =
+let section oc name =
+  fprintf oc "	%s\n" name
+
+(* Names of sections *)
+
+let (text, data, const_data, float_literal) =
   match target with
-  | MacOS -> fprintf oc "	.const_data\n"
-  | EABI  -> fprintf oc "	.section	.rodata.cst8,\"aM\",@progbits,8\n"
+  | MacOS ->
+      (".text",
+       ".data",
+       ".const",
+       ".const_data")
+  | EABI ->
+      (".text",
+       ".data",
+       ".rodata",
+       ".section	.rodata.cst8,\"aM\",@progbits,8")
+
+(* Encoding masks for rlwinm instructions *)
+
+let rolm_mask n =
+  let mb = ref 0       (* location of last 0->1 transition *)
+  and me = ref 32      (* location of last 1->0 transition *)
+  and last = ref ((Int32.logand n 1l) <> 0l)  (* last bit seen *)
+  and count = ref 0    (* number of transitions *)
+  and mask = ref 0x8000_0000l in
+  for mx = 0 to 31 do
+    if Int32.logand n !mask <> 0l then
+      if !last then () else (incr count; mb := mx; last := true)
+    else
+      if !last then (incr count; me := mx; last := false) else ();
+    mask := Int32.shift_right_logical !mask 1
+  done;
+  if !me = 0 then me := 32;
+  assert (!count = 2 || (!count = 0 && !last));
+  (!mb, !me-1)
 
 (* Printing of instructions *)
 
@@ -264,9 +292,9 @@ let print_instruction oc labels = function
       fprintf oc "	lwz	%a, 4(%a)\n" ireg r1  ireg GPR1;
       fprintf oc "	addis	%a, %a, 0x8000\n" ireg r1 ireg r1;
       fprintf oc "%a:	addi	%a, %a, 8\n" label lbl3  ireg GPR1  ireg GPR1;
-      const oc;
+      section oc float_literal;
       fprintf oc "%a:	.long	0x41e00000, 0x00000000\n" label lbl1;
-      text oc
+      section oc text
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfmadd(r1, r2, r3, r4) ->
@@ -294,9 +322,9 @@ let print_instruction oc labels = function
       fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
       fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
-      const oc;
+      section oc float_literal;
       fprintf oc "%a:	.long	0x43300000, 0x80000000\n" label lbl;
-      text oc
+      section oc text
   | Piuctf(r1, r2) ->
       let lbl = new_label() in
       fprintf oc "	addis	%a, 0, 0x4330\n" ireg GPR12;
@@ -307,9 +335,9 @@ let print_instruction oc labels = function
       fprintf oc "	lfd	%a, 0(%a)\n" freg r1  ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1  ireg GPR1;
       fprintf oc "	fsub	%a, %a, %a\n" freg r1  freg r1  freg FPR13;
-      const oc;
+      section oc float_literal;
       fprintf oc "%a:	.long	0x43300000, 0x00000000\n" label lbl;
-      text oc
+      section oc text
   | Plbz(r1, c, r2) ->
       fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Plbzx(r1, r2, r3) ->
@@ -322,12 +350,12 @@ let print_instruction oc labels = function
       let lbl = new_label() in
       fprintf oc "	addis	%a, 0, %a\n" ireg GPR12 label_high lbl;
       fprintf oc "	lfd	%a, %a(%a)\n" freg r1 label_low lbl ireg GPR12;
-      const oc;
+      section oc float_literal;
       let n = Int64.bits_of_float c in
       let nlo = Int64.to_int32 n
       and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
       fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo;
-      text oc
+      section oc text
   | Plfs(r1, c, r2) ->
       fprintf oc "	lfs	%a, %a(%a)\n" freg r1 constant c ireg r2
   | Plfsx(r1, r2, r3) ->
@@ -346,7 +374,7 @@ let print_instruction oc labels = function
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pmfcrbit(r1, bit) ->
       fprintf oc "	mfcr	%a\n" ireg GPR12;
-      fprintf oc "	rlwinm	%a, %a, %d, 1\n" ireg r1  ireg GPR12  (1 + num_crbit bit)
+      fprintf oc "	rlwinm	%a, %a, %d, 31, 31\n" ireg r1  ireg GPR12  (1 + num_crbit bit)
   | Pmflr(r1) ->
       fprintf oc "	mflr	%a\n" ireg r1
   | Pmr(r1, r2) ->
@@ -372,8 +400,13 @@ let print_instruction oc labels = function
   | Poris(r1, r2, c) ->
       fprintf oc "	oris	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Prlwinm(r1, r2, c1, c2) ->
+      let (mb, me) = rolm_mask (camlint_of_coqint c2) in
+      fprintf oc "	rlwinm	%a, %a, %ld, %d, %d\n"
+                ireg r1 ireg r2 (camlint_of_coqint c1) mb me
+(*
       fprintf oc "	rlwinm	%a, %a, %ld, 0x%lx\n"
                 ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
+*)
   | Pslw(r1, r2, r3) ->
       fprintf oc "	slw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psraw(r1, r2, r3) ->
@@ -424,9 +457,10 @@ let rec labels_of_code = function
 
 let print_function oc name code =
   Hashtbl.clear current_function_labels;
-  fprintf oc "	.text\n";
+  section oc text;
   fprintf oc "	.align 2\n";
-  fprintf oc "	.globl %a\n" symbol name;
+  if not (Cil2Csyntax.atom_is_static name) then
+    fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
   List.iter (print_instruction oc (labels_of_code code)) code
 
@@ -632,9 +666,11 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   match init_data with
   | [] -> ()
   | _  ->
-      fprintf oc "	.data\n";
+      section oc 
+        (if Cil2Csyntax.atom_is_readonly name then const_data else data);
       fprintf oc "	.align	3\n";
-      fprintf oc "	.globl	%a\n" symbol name;
+      if not (Cil2Csyntax.atom_is_static name) then
+        fprintf oc "	.globl	%a\n" symbol name;
       fprintf oc "%a:\n" symbol name;
       print_init_data oc init_data