diff options
| -rw-r--r-- | caml/PrintCsyntax.ml | 32 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 23 | ||||
| -rw-r--r-- | common/AST.v | 3 | ||||
| -rw-r--r-- | common/Mem.v | 7 |
4 files changed, 61 insertions, 4 deletions
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml index 6e88da9..052581c 100644 --- a/caml/PrintCsyntax.ml +++ b/caml/PrintCsyntax.ml @@ -309,6 +309,34 @@ let print_fundef p (Coq_pair(id, fd)) = | Internal f -> print_function p id f +let string_of_init id = + try + let s = String.create (length_coqlist id) in + let i = ref 0 in + coqlist_iter + (function + | Init_int8 n -> + s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n)); + incr i + | _ -> raise Not_found) + id; + Some s + with Not_found -> None + +let print_escaped_string p s = + fprintf p "\""; + for i = 0 to String.length s - 1 do + match s.[i] with + | ('\"' | '\\') as c -> fprintf p "\\%c" c + | '\n' -> fprintf p "\\n" + | '\t' -> fprintf p "\\t" + | '\r' -> fprintf p "\\r" + | c -> if c >= ' ' && c <= '~' + then fprintf p "%c" c + else fprintf p "\\x%02x" (Char.code c) + done; + fprintf p "\"" + let print_init p = function | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) @@ -316,6 +344,10 @@ let print_init p = function | Init_float32 n -> fprintf p "%F,@ " n | Init_float64 n -> fprintf p "%F,@ " n | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n) + | 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/caml/PrintPPC.ml b/caml/PrintPPC.ml index b7db501..85d695e 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -382,7 +382,9 @@ let print_fundef oc (Coq_pair(name, defn)) = | Internal code -> print_function oc name code | External ef -> print_external_function oc name -let print_init_data oc = function +let init_data_queue = ref [] + +let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) | Init_int16 n -> @@ -401,6 +403,23 @@ let print_init_data oc = function | Init_space n -> let n = camlint_of_z n in if n > 0l then fprintf oc " .space %ld\n" n + | Init_pointer id -> + let lbl = new_label() in + fprintf oc " .long L%d\n" lbl; + init_data_queue := (lbl, id) :: !init_data_queue + +let print_init_data oc id = + init_data_queue := []; + coqlist_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; + coqlist_iter (print_init oc) id; + print_remainder() + in print_remainder() let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = match init_data with @@ -409,7 +428,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = fprintf oc " .data\n"; fprintf oc " .globl %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; - coqlist_iter (print_init_data oc) init_data + print_init_data oc init_data let print_program oc p = extfuns := IdentSet.empty; diff --git a/common/AST.v b/common/AST.v index 673f1d8..5b8c997 100644 --- a/common/AST.v +++ b/common/AST.v @@ -62,7 +62,8 @@ Inductive init_data: Set := | Init_int32: int -> init_data | Init_float32: float -> init_data | Init_float64: float -> init_data - | Init_space: Z -> init_data. + | Init_space: Z -> init_data + | Init_pointer: list init_data -> init_data. (** Whole programs consist of: - a collection of function definitions (name and description); diff --git a/common/Mem.v b/common/Mem.v index 7af696e..679c41e 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -636,6 +636,9 @@ Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentma store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f) | Init_space n :: id' => contents_init_data (pos + Zmax n 0) id' + | Init_pointer x :: id' => + (* Not handled properly yet *) + contents_init_data (pos + 4) id' end. Definition size_init_data (id: init_data) : Z := @@ -646,6 +649,7 @@ Definition size_init_data (id: init_data) : Z := | Init_float32 _ => 4 | Init_float64 _ => 8 | Init_space n => Zmax n 0 + | Init_pointer _ => 4 end. Definition size_init_data_list (id: list init_data): Z := @@ -679,6 +683,7 @@ Proof. unfold size_init_data in H; destruct a; try (apply H1; [reflexivity|assumption]). apply IHid. generalize (Zmax2 z 0). omega. + apply IHid. omega. Qed. Definition block_init_data (id: list init_data) : block_contents := @@ -2136,7 +2141,7 @@ Proof. destruct a; try (apply H1; [reflexivity|repeat constructor]). apply IHid. generalize (Zmax2 z 0). omega. simpl in H0; omega. - + apply IHid. omega. simpl size_init_data in H0. omega. apply H. omega. unfold sz0. omega. Qed. |