diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 18 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 4 | ||||
| -rw-r--r-- | common/AST.v | 3 | ||||
| -rw-r--r-- | common/Mem.v | 4 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 42 |
6 files changed, 25 insertions, 47 deletions
@@ -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 25d9db2..64f8be2 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 fa1d048..0388c2e 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 13e84dd..2d20276 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 6510828..252ee29 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 8bf40a9..10170f9 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; |