From 1e24932c5f5badcca3125b9c4c0df2ac113532bf Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 3 Mar 2010 13:16:21 +0000
Subject: [PATCH] Suppressed Init_pointer, now useless. Improved printing of
strings in generated .s
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
Makefile | 1 +
arm/PrintAsm.ml | 18 +----------------
cfrontend/PrintCsyntax.ml | 4 ----
common/AST.v | 3 +--
common/Mem.v | 4 ----
powerpc/PrintAsm.ml | 42 ++++++++++++++++++++-------------------
6 files changed, 25 insertions(+), 47 deletions(-)
diff --git a/Makefile b/Makefile
index 856d7773e..c9a61d723 100644
--- a/Makefile
+++ b/Makefile
@@ -23,6 +23,7 @@ COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source
OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
+ -j 2 \
-no-hygiene \
-no-links \
-I extraction $(INCLUDES)
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 25d9db2ef..64f8be2ed 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -459,8 +459,6 @@ let print_fundef oc (Coq_pair(name, defn)) =
(* Data *)
-let init_data_queue = ref []
-
let print_init oc = function
| Init_int8 n ->
fprintf oc " .byte %ld\n" (camlint_of_coqint n)
@@ -481,23 +479,9 @@ let print_init oc = function
if n > 0l then fprintf oc " .space %ld\n" n
| Init_addrof(symb, ofs) ->
fprintf oc " .word %a\n" print_symb_ofs (symb, ofs)
- | Init_pointer id ->
- let lbl = new_label() in
- fprintf oc " .word .L%d\n" lbl;
- init_data_queue := (lbl, id) :: !init_data_queue
let print_init_data oc id =
- init_data_queue := [];
- List.iter (print_init oc) id;
- let rec print_remainder () =
- match !init_data_queue with
- | [] -> ()
- | (lbl, id) :: rem ->
- init_data_queue := rem;
- fprintf oc ".L%d:\n" lbl;
- List.iter (print_init oc) id;
- print_remainder()
- in print_remainder()
+ List.iter (print_init oc) id
let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index fa1d04825..0388c2eb1 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -383,10 +383,6 @@ let print_init p = function
if ofs = 0l
then fprintf p "&%s,@ " (extern_atom symb)
else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs
- | Init_pointer id ->
- match string_of_init id with
- | None -> fprintf p "/* pointer to other init*/,@ "
- | Some s -> fprintf p "%a,@ " print_escaped_string s
let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
match init with
diff --git a/common/AST.v b/common/AST.v
index 13e84dd8f..2d2027602 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -91,8 +91,7 @@ Inductive init_data: Type :=
| Init_float32: float -> init_data
| Init_float64: float -> init_data
| Init_space: Z -> init_data
- | Init_addrof: ident -> int -> init_data (**r address of symbol + offset *)
- | Init_pointer: list init_data -> init_data.
+ | Init_addrof: ident -> int -> init_data. (**r address of symbol + offset *)
(** Whole programs consist of:
- a collection of function definitions (name and description);
diff --git a/common/Mem.v b/common/Mem.v
index 65108288d..252ee2911 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -571,9 +571,6 @@ Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentma
| Init_addrof s n :: id' =>
(* Not handled properly yet *)
contents_init_data (pos + 4) id'
- | Init_pointer x :: id' =>
- (* Not handled properly yet *)
- contents_init_data (pos + 4) id'
end.
Definition size_init_data (id: init_data) : Z :=
@@ -585,7 +582,6 @@ Definition size_init_data (id: init_data) : Z :=
| Init_float64 _ => 8
| Init_space n => Zmax n 0
| Init_addrof _ _ => 4
- | Init_pointer _ => 4
end.
Definition size_init_data_list (id: list init_data): Z :=
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 8bf40a97d..10170f9e7 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -661,8 +661,6 @@ let record_extfun (Coq_pair(name, defn)) =
if function_needs_stub name then
stubbed_functions := IdentSet.add name !stubbed_functions
-let init_data_queue = ref []
-
let print_init oc = function
| Init_int8 n ->
fprintf oc " .byte %ld\n" (camlint_of_coqint n)
@@ -684,23 +682,27 @@ let print_init oc = function
| Init_addrof(symb, ofs) ->
fprintf oc " .long %a\n"
symbol_offset (symb, camlint_of_coqint ofs)
- | Init_pointer id ->
- let lbl = new_label() in
- fprintf oc " .long %a\n" label lbl;
- init_data_queue := (lbl, id) :: !init_data_queue
-
-let print_init_data oc id =
- init_data_queue := [];
- List.iter (print_init oc) id;
- let rec print_remainder () =
- match !init_data_queue with
- | [] -> ()
- | (lbl, id) :: rem ->
- init_data_queue := rem;
- fprintf oc "%a:\n" label lbl;
- List.iter (print_init oc) id;
- print_remainder()
- in print_remainder()
+
+let print_init_char oc = function
+ | Init_int8 n ->
+ let c = Int32.to_int (camlint_of_coqint n) in
+ if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
+ then output_char oc (Char.chr c)
+ else fprintf oc "\\%03o" c
+ | _ ->
+ assert false
+
+let re_string_literal = Str.regexp "__stringlit_[0-9]+"
+
+let print_init_data oc name id =
+ if Str.string_match re_string_literal (extern_atom name) 0
+ && List.for_all (function Init_int8 _ -> true | _ -> false) id
+ then begin
+ fprintf oc " .ascii \"";
+ List.iter (print_init_char oc) id;
+ fprintf oc "\"\n"
+ end else
+ List.iter (print_init oc) id
let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with
@@ -721,7 +723,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
if not (C2Clight.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
- print_init_data oc init_data
+ print_init_data oc name init_data
let print_program oc p =
stubbed_functions := IdentSet.empty;
--
GitLab