From 53b57751c1981e0bce3aa470e426a12034bb165e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Sep 2006 08:58:05 +0000
Subject: [PATCH] Ajout de Init_pointer (experimental)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
caml/PrintCsyntax.ml | 32 ++++++++++++++++++++++++++++++++
caml/PrintPPC.ml | 23 +++++++++++++++++++++--
common/AST.v | 3 ++-
common/Mem.v | 7 ++++++-
4 files changed, 61 insertions(+), 4 deletions(-)
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 6e88da982..052581cdc 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 b7db50145..85d695e10 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 673f1d81d..5b8c997ab 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 7af696e1c..679c41e17 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.
--
GitLab