Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


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

2 files changed, 169 insertions, 0 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
new file mode 100644
index 0000000..98fd79c
--- /dev/null
+++ b/lib/Camlcoq.ml
@@ -0,0 +1,130 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Library of useful Caml <-> Coq conversions *)
+
+open Datatypes
+open CList
+open BinPos
+open BinInt
+
+(* Integers *)
+
+let rec camlint_of_positive = function
+  | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l
+  | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1
+  | Coq_xH -> 1l
+
+let camlint_of_z = function
+  | Z0 -> 0l
+  | Zpos p -> camlint_of_positive p
+  | Zneg p -> Int32.neg (camlint_of_positive p)
+
+let camlint_of_coqint : Integers.int -> int32 = camlint_of_z
+
+let rec camlint_of_nat = function
+  | O -> 0
+  | S n -> camlint_of_nat n + 1
+
+let rec nat_of_camlint n =
+  assert (n >= 0l);
+  if n = 0l then O else S (nat_of_camlint (Int32.sub n 1l))
+
+let rec positive_of_camlint n =
+  if n = 0l then assert false else
+  if n = 1l then Coq_xH else
+  if Int32.logand n 1l = 0l
+  then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1))
+  else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1))
+
+let z_of_camlint n =
+  if n = 0l then Z0 else
+  if n > 0l then Zpos (positive_of_camlint n)
+  else Zneg (positive_of_camlint (Int32.neg n))
+
+let coqint_of_camlint (n: int32) : Integers.int = 
+  (* Interpret n as unsigned so that resulting Z is in range *)
+  if n = 0l then Z0 else Zpos (positive_of_camlint n)
+
+(* Atoms (positive integers representing strings) *)
+
+let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t)
+let string_of_atom = (Hashtbl.create 17 : (positive, string) Hashtbl.t)
+let next_atom = ref Coq_xH
+
+let intern_string s =
+  try
+    Hashtbl.find atom_of_string s
+  with Not_found ->
+    let a = !next_atom in
+    next_atom := coq_Psucc !next_atom;
+    Hashtbl.add atom_of_string s a;
+    Hashtbl.add string_of_atom a s;
+    a
+
+let extern_atom a =
+  try
+    Hashtbl.find string_of_atom a
+  with Not_found ->
+    Printf.sprintf "<unknown atom %ld>" (camlint_of_positive a)
+
+(* Strings *)
+
+let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
+  Char.chr(  (if a0 then 1 else 0)
+           + (if a1 then 2 else 0)
+           + (if a2 then 4 else 0)
+           + (if a3 then 8 else 0)
+           + (if a4 then 16 else 0)
+           + (if a5 then 32 else 0)
+           + (if a6 then 64 else 0)
+           + (if a7 then 128 else 0))
+
+let coqstring_length s =
+  let rec len accu = function
+  | CString.EmptyString -> accu
+  | CString.CString(_, s) -> len (accu + 1) s
+  in len 0 s
+
+let camlstring_of_coqstring s =
+  let r = String.create (coqstring_length s) in
+  let rec fill pos = function
+  | CString.EmptyString -> r
+  | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+  in fill 0 s
+
+(* Timing facility *)
+
+(*
+let timers = (Hashtbl.create 9 : (string, float) Hashtbl.t)
+
+let add_to_timer name time =
+  let old = try Hashtbl.find timers name with Not_found -> 0.0 in
+  Hashtbl.replace timers name (old +. time)
+
+let time name fn arg =
+  let start = Unix.gettimeofday() in
+  try
+    let res = fn arg in
+    add_to_timer name (Unix.gettimeofday() -. start);
+    res
+  with x ->
+    add_to_timer name (Unix.gettimeofday() -. start);
+    raise x
+
+let print_timers () =
+  Hashtbl.iter
+    (fun name time -> Printf.printf "%-20s %.3f\n" name time)
+    timers
+
+let _ = at_exit print_timers
+*)
diff --git a/lib/Floataux.ml b/lib/Floataux.ml
new file mode 100644
index 0000000..6b3b825
--- /dev/null
+++ b/lib/Floataux.ml
@@ -0,0 +1,39 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Camlcoq
+open Integers
+
+let singleoffloat f =
+  Int32.float_of_bits (Int32.bits_of_float f)
+
+let intoffloat f =
+  coqint_of_camlint (Int32.of_float f)
+
+let intuoffloat f =
+  coqint_of_camlint (Int64.to_int32 (Int64.of_float f))
+
+let floatofint i =
+  Int32.to_float (camlint_of_coqint i)
+
+let floatofintu i =
+  Int64.to_float (Int64.logand (Int64.of_int32 (camlint_of_coqint i))
+                               0xFFFFFFFFL)
+
+let cmp c (x: float) (y: float) =
+  match c with
+  | Ceq -> x = y
+  | Cne -> x <> y
+  | Clt -> x < y
+  | Cle -> x <= y
+  | Cgt -> x > y
+  | Cge -> x >= y