Initial import of compcert

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

13 files changed, 1605 insertions, 0 deletions

diff --git a/caml/Allocationaux.ml b/caml/Allocationaux.ml
new file mode 100644
index 0000000..8e4f328
--- /dev/null
+++ b/caml/Allocationaux.ml
@@ -0,0 +1,39 @@
+open Camlcoq
+open Datatypes
+open List
+open AST
+open Locations
+
+type status = To_move | Being_moved | Moved
+
+let parallel_move_order lsrc ldst =
+  let src = array_of_coqlist lsrc
+  and dst = array_of_coqlist ldst in
+  let n = Array.length src in
+  let status = Array.make n To_move in
+  let moves = ref Coq_nil in
+  let rec move_one i =
+    if src.(i) <> dst.(i) then begin
+      status.(i) <- Being_moved;
+      for j = 0 to n - 1 do
+        if src.(j) = dst.(i) then
+          match status.(j) with
+            To_move ->
+              move_one j
+          | Being_moved ->
+              let tmp =
+                match Loc.coq_type src.(j) with
+                | Tint -> R IT2
+                | Tfloat -> R FT2 in
+              moves := Coq_cons (Coq_pair(src.(j), tmp), !moves);
+              src.(j) <- tmp
+          | Moved ->
+              ()
+      done;
+      moves := Coq_cons(Coq_pair(src.(i), dst.(i)), !moves);
+      status.(i) <- Moved
+    end in
+  for i = 0 to n - 1 do
+    if status.(i) = To_move then move_one i
+  done;
+  List.rev !moves
diff --git a/caml/Allocationaux.mli b/caml/Allocationaux.mli
new file mode 100644
index 0000000..0cf3b94
--- /dev/null
+++ b/caml/Allocationaux.mli
@@ -0,0 +1,5 @@
+open Datatypes
+open List
+open Locations
+
+val parallel_move_order: loc list -> loc list -> (loc, loc) prod list
diff --git a/caml/CMlexer.mli b/caml/CMlexer.mli
new file mode 100644
index 0000000..573c530
--- /dev/null
+++ b/caml/CMlexer.mli
@@ -0,0 +1,4 @@
+(* $Id: CMlexer.mli,v 1.1 2005/01/21 13:11:07 xleroy Exp $ *)
+
+val token: Lexing.lexbuf -> CMparser.token
+exception Error of string
diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll
new file mode 100644
index 0000000..b8d3ae7
--- /dev/null
+++ b/caml/CMlexer.mll
@@ -0,0 +1,112 @@
+(* $Id: CMlexer.mll,v 1.3 2005/03/21 15:53:00 xleroy Exp $ *)
+
+{
+open Camlcoq
+open CMparser
+exception Error of string
+}
+
+let blank = [' ' '\009' '\012' '\010' '\013']
+let floatlit = 
+  ['0'-'9'] ['0'-'9' '_']* 
+  ('.' ['0'-'9' '_']* )?
+  (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)?
+let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '0'-'9']*
+let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+
+                               | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ )
+let stringlit = "\"" [ ^ '"' ] * '"'
+
+rule token = parse
+  | blank +      { token lexbuf }
+  | "/*"         { comment lexbuf; token lexbuf }
+  | "absf" { ABSF }
+  | "&" { AMPERSAND }
+  | "&&" { AMPERSANDAMPERSAND }
+  | "!"    { BANG }
+  | "!="    { BANGEQUAL }
+  | "!=f"    { BANGEQUALF }
+  | "!=u"    { BANGEQUALU }
+  | "|"     { BAR }
+  | "||"    { BARBAR }
+  | "^"     { CARET }
+  | ":"    { COLON }
+  | ","    { COMMA }
+  | "$"    { DOLLAR }
+  | "else"    { ELSE }
+  | "="    { EQUAL }
+  | "=="    { EQUALEQUAL }
+  | "==f"    { EQUALEQUALF }
+  | "==u"    { EQUALEQUALU }
+  | "exit"    { EXIT }
+  | "float"    { FLOAT }
+  | "float32"    { FLOAT32 }
+  | "float64"    { FLOAT64 }
+  | "floatofint"    { FLOATOFINT }
+  | "floatofintu"    { FLOATOFINTU }
+  | ">"    { GREATER }
+  | ">f"    { GREATERF }
+  | ">u"    { GREATERU }
+  | ">="    { GREATEREQUAL }
+  | ">=f"    { GREATEREQUALF }
+  | ">=u"    { GREATEREQUALU }
+  | ">>"    { GREATERGREATER }
+  | ">>u"    { GREATERGREATERU }
+  | "if"    { IF }
+  | "in"    { IN }
+  | "int"    { INT }
+  | "int16s"    { INT16S }
+  | "int16u"    { INT16U }
+  | "int32"    { INT32 }
+  | "int8s"    { INT8S }
+  | "int8u"    { INT8U }
+  | "intoffloat"    { INTOFFLOAT }
+  | "{"    { LBRACE }
+  | "{{"    { LBRACELBRACE }
+  | "["    { LBRACKET }
+  | "<"    { LESS }
+  | "<u"    { LESSU }
+  | "<f"    { LESSF }
+  | "<="    { LESSEQUAL }
+  | "<=u"    { LESSEQUALU }
+  | "<=f"    { LESSEQUALF }
+  | "<<"    { LESSLESS }
+  | "let"     { LET }
+  | "loop"    { LOOP }
+  | "("    { LPAREN }
+  | "-"    { MINUS }
+  | "->"    { MINUSGREATER }
+  | "-f"    { MINUSF }
+  | "%"    { PERCENT }
+  | "%u"    { PERCENTU }
+  | "+"    { PLUS }
+  | "+f"    { PLUSF }
+  | "?"    { QUESTION }
+  | "}"    { RBRACE }
+  | "}}"    { RBRACERBRACE }
+  | "]"    { RBRACKET }
+  | "return"    { RETURN }
+  | ")"    { RPAREN }
+  | ";"    { SEMICOLON }
+  | "/"    { SLASH }
+  | "/f"    { SLASHF }
+  | "/u"    { SLASHU }
+  | "stack"    { STACK }
+  | "*" { STAR }
+  | "*f"    { STARF }
+  | "switch"    { SWITCH }
+  | "~"    { TILDE }
+  | "var"    { VAR }
+  | "void"    { VOID }
+
+  | intlit    { INTLIT(Int32.of_string(Lexing.lexeme lexbuf)) }
+  | floatlit     { FLOATLIT(float_of_string(Lexing.lexeme lexbuf)) }
+  | stringlit { let s = Lexing.lexeme lexbuf in
+                STRINGLIT(intern_string(String.sub s 1 (String.length s - 2))) }
+  | ident    { IDENT(intern_string(Lexing.lexeme lexbuf)) }
+  | eof      { EOF }
+  | _        { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) }
+
+and comment = parse
+    "*/"     { () }
+  | eof      { raise(Error "unterminated comment") }
+  | _        { comment lexbuf }
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
new file mode 100644
index 0000000..0b19bce
--- /dev/null
+++ b/caml/CMparser.mly
@@ -0,0 +1,327 @@
+/* $Id: CMparser.mly,v 1.2 2005/03/21 15:53:00 xleroy Exp $ */
+
+%{
+open Datatypes
+open List
+open Camlcoq
+open BinPos
+open BinInt
+open Integers
+open AST
+open Op
+open Cminor
+
+let intconst n =
+  Eop(Ointconst(coqint_of_camlint n), Enil)
+
+let andbool e1 e2 =
+  Cmconstr.conditionalexpr e1 e2 (intconst 0l)
+let orbool e1 e2 =
+  Cmconstr.conditionalexpr e1 (intconst 1l) e2
+
+%}
+
+%token ABSF
+%token AMPERSAND
+%token AMPERSANDAMPERSAND
+%token BANG
+%token BANGEQUAL
+%token BANGEQUALF
+%token BANGEQUALU
+%token BAR
+%token BARBAR
+%token CARET
+%token COLON
+%token COMMA
+%token DOLLAR
+%token ELSE
+%token EQUAL
+%token EQUALEQUAL
+%token EQUALEQUALF
+%token EQUALEQUALU
+%token EOF
+%token EXIT
+%token FLOAT
+%token FLOAT32
+%token FLOAT64
+%token <float> FLOATLIT
+%token FLOATOFINT
+%token FLOATOFINTU
+%token GREATER
+%token GREATERF
+%token GREATERU
+%token GREATEREQUAL
+%token GREATEREQUALF
+%token GREATEREQUALU
+%token GREATERGREATER
+%token GREATERGREATERU
+%token <AST.ident> IDENT
+%token IF
+%token IN
+%token INT
+%token INT16S
+%token INT16U
+%token INT32
+%token INT8S
+%token INT8U
+%token <int32> INTLIT
+%token INTOFFLOAT
+%token LBRACE
+%token LBRACELBRACE
+%token LBRACKET
+%token LESS
+%token LESSU
+%token LESSF
+%token LESSEQUAL
+%token LESSEQUALU
+%token LESSEQUALF
+%token LESSLESS
+%token LET
+%token LOOP
+%token LPAREN
+%token MINUS
+%token MINUSF
+%token MINUSGREATER
+%token PERCENT
+%token PERCENTU
+%token PLUS
+%token PLUSF
+%token QUESTION
+%token RBRACE
+%token RBRACERBRACE
+%token RBRACKET
+%token RETURN
+%token RPAREN
+%token SEMICOLON
+%token SLASH
+%token SLASHF
+%token SLASHU
+%token STACK
+%token STAR
+%token STARF
+%token <AST.ident> STRINGLIT
+%token SWITCH
+%token TILDE
+%token VAR
+%token VOID
+
+/* Precedences from low to high */
+
+%left COMMA
+%left p_let
+%right EQUAL
+%right QUESTION COLON
+%left BARBAR
+%left AMPERSANDAMPERSAND
+%left BAR
+%left CARET
+%left AMPERSAND
+%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF 
+%left LESSLESS GREATERGREATER GREATERGREATERU
+%left PLUS PLUSF MINUS MINUSF
+%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
+%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32
+%left LPAREN
+
+/* Entry point */
+
+%start prog
+%type <Cminor.program> prog
+
+%%
+
+/* Programs */
+
+prog:
+    global_declarations proc_list EOF
+      { { prog_funct = List.rev $2;
+          prog_main = intern_string "main";
+          prog_vars = List.rev $1; } }
+;
+
+global_declarations:
+    /* empty */                                 { Coq_nil }
+  | global_declarations global_declaration      { Coq_cons($2, $1) }
+;
+
+global_declaration:
+    VAR STRINGLIT LBRACKET INTLIT RBRACKET      { Coq_pair($2, z_of_camlint $4) }
+;
+
+proc_list:
+    /* empty */                                 { Coq_nil }
+  | proc_list proc                              { Coq_cons($2, $1) }
+;
+
+/* Procedures */
+
+proc:
+    STRINGLIT LPAREN parameters RPAREN COLON signature
+    LBRACE
+      stack_declaration
+      var_declarations
+      stmt_list
+    RBRACE
+      { Coq_pair($1,
+         { fn_sig = $6;
+           fn_params = List.rev $3;
+           fn_vars = List.rev $9;
+           fn_stackspace = $8;
+           fn_body = $10 }) }
+;
+
+signature:
+    type_ 
+               { {sig_args = Coq_nil; sig_res = Some $1} }
+  | VOID
+               { {sig_args = Coq_nil; sig_res = None} }
+  | type_ MINUSGREATER signature
+               { let s = $3 in {s with sig_args = Coq_cons($1, s.sig_args)} }
+;
+
+parameters:
+    /* empty */                                 { Coq_nil }
+  | parameter_list                              { $1 }
+;
+
+parameter_list:
+    IDENT                                       { Coq_cons($1, Coq_nil) }
+  | parameter_list COMMA IDENT                  { Coq_cons($3, $1) }
+;
+
+stack_declaration:
+    /* empty */                                 { Z0 }
+  | STACK INTLIT                                { z_of_camlint $2 }
+;
+
+var_declarations:
+    /* empty */                                 { Coq_nil }
+  | var_declarations var_declaration            { List.app $2 $1 }
+;
+
+var_declaration:
+    VAR parameter_list SEMICOLON                { $2 }
+;
+
+/* Statements */
+
+stmt:
+    expr SEMICOLON                              { Sexpr $1 }
+  | IF LPAREN expr RPAREN stmts ELSE stmts      { Cmconstr.ifthenelse $3 $5 $7 }
+  | IF LPAREN expr RPAREN stmts                 { Cmconstr.ifthenelse $3 $5 Snil }
+  | LOOP stmts                                  { Sloop($2) }
+  | LBRACELBRACE stmts RBRACERBRACE             { Sblock($2) }
+  | EXIT SEMICOLON                              { Sexit O }
+  | EXIT INTLIT SEMICOLON                       { Sexit (nat_of_camlint(Int32.pred $2)) }
+  | RETURN SEMICOLON                            { Sreturn None }
+  | RETURN expr SEMICOLON                       { Sreturn (Some $2) }
+;
+
+stmts:
+    LBRACE stmt_list RBRACE                     { $2 }
+  | stmt                                        { Scons($1, Snil) }
+;
+
+stmt_list:
+    /* empty */                                 { Snil }
+  | stmt stmt_list                              { Scons($1, $2) }
+;
+
+/* Expressions */
+
+expr:
+    LPAREN expr RPAREN                          { $2 }
+  | IDENT                                       { Evar $1 }
+  | IDENT EQUAL expr                            { Eassign($1, $3) }
+  | INTLIT                                      { intconst $1 }
+  | FLOATLIT                                    { Eop(Ofloatconst $1, Enil) }
+  | STRINGLIT                                   { Eop(Oaddrsymbol($1, Int.zero), Enil) }
+  | AMPERSAND INTLIT                            { Eop(Oaddrstack(coqint_of_camlint $2), Enil) }
+  | MINUS expr    %prec p_uminus                { Cmconstr.negint $2 }
+  | MINUSF expr   %prec p_uminus                { Cmconstr.negfloat $2 }
+  | ABSF expr                                   { Cmconstr.absfloat $2 }
+  | INTOFFLOAT expr                             { Cmconstr.intoffloat $2 }
+  | FLOATOFINT expr                             { Cmconstr.floatofint $2 }
+  | FLOATOFINTU expr                            { Cmconstr.floatofintu $2 }
+  | TILDE expr                                  { Cmconstr.notint $2 }
+  | BANG expr                                   { Cmconstr.notbool $2 }
+  | INT8S expr                                  { Cmconstr.cast8signed $2 }
+  | INT8U expr                                  { Cmconstr.cast8unsigned $2 }
+  | INT16S expr                                 { Cmconstr.cast16signed $2 }
+  | INT16U expr                                 { Cmconstr.cast16unsigned $2 }
+  | FLOAT32 expr                                { Cmconstr.singleoffloat $2 }
+  | expr PLUS expr                              { Cmconstr.add $1 $3 }
+  | expr MINUS expr                             { Cmconstr.sub $1 $3 }
+  | expr STAR expr                              { Cmconstr.mul $1 $3 }
+  | expr SLASH expr                             { Cmconstr.divs $1 $3 }
+  | expr PERCENT expr                           { Cmconstr.mods $1 $3 }
+  | expr SLASHU expr                            { Cmconstr.divu $1 $3 }
+  | expr PERCENTU expr                          { Cmconstr.modu $1 $3 }
+  | expr AMPERSAND expr                         { Cmconstr.coq_and $1 $3 }
+  | expr BAR expr                               { Cmconstr.coq_or $1 $3 }
+  | expr CARET expr                             { Cmconstr.xor $1 $3 }
+  | expr LESSLESS expr                          { Cmconstr.shl $1 $3 }
+  | expr GREATERGREATER expr                    { Cmconstr.shr $1 $3 }
+  | expr GREATERGREATERU expr                   { Cmconstr.shru $1 $3 }
+  | expr PLUSF expr                             { Cmconstr.addf $1 $3 }
+  | expr MINUSF expr                            { Cmconstr.subf $1 $3 }
+  | expr STARF expr                             { Cmconstr.mulf $1 $3 }
+  | expr SLASHF expr                            { Cmconstr.divf $1 $3 }
+  | expr EQUALEQUAL expr                        { Cmconstr.cmp Ceq $1 $3 }
+  | expr BANGEQUAL expr                         { Cmconstr.cmp Cne $1 $3 }
+  | expr LESS expr                              { Cmconstr.cmp Clt $1 $3 }
+  | expr LESSEQUAL expr                         { Cmconstr.cmp Cle $1 $3 }
+  | expr GREATER expr                           { Cmconstr.cmp Cgt $1 $3 }
+  | expr GREATEREQUAL expr                      { Cmconstr.cmp Cge $1 $3 }
+  | expr EQUALEQUALU expr                       { Cmconstr.cmpu Ceq $1 $3 }
+  | expr BANGEQUALU expr                        { Cmconstr.cmpu Cne $1 $3 }
+  | expr LESSU expr                             { Cmconstr.cmpu Clt $1 $3 }
+  | expr LESSEQUALU expr                        { Cmconstr.cmpu Cle $1 $3 }
+  | expr GREATERU expr                          { Cmconstr.cmpu Cgt $1 $3 }
+  | expr GREATEREQUALU expr                     { Cmconstr.cmpu Cge $1 $3 }
+  | expr EQUALEQUALF expr                       { Cmconstr.cmpf Ceq $1 $3 }
+  | expr BANGEQUALF expr                        { Cmconstr.cmpf Cne $1 $3 }
+  | expr LESSF expr                             { Cmconstr.cmpf Clt $1 $3 }
+  | expr LESSEQUALF expr                        { Cmconstr.cmpf Cle $1 $3 }
+  | expr GREATERF expr                          { Cmconstr.cmpf Cgt $1 $3 }
+  | expr GREATEREQUALF expr                     { Cmconstr.cmpf Cge $1 $3 }
+  | memory_chunk LBRACKET expr RBRACKET         { Cmconstr.load $1 $3 }
+  | memory_chunk LBRACKET expr RBRACKET EQUAL expr
+                                                { Cmconstr.store $1 $3 $6 }
+  | expr LPAREN expr_list RPAREN COLON signature
+                                                { Ecall($6, $1, $3) }
+  | expr AMPERSANDAMPERSAND expr                { andbool $1 $3 }
+  | expr BARBAR expr                            { orbool $1 $3 }
+  | expr QUESTION expr COLON expr               { Cmconstr.conditionalexpr $1 $3 $5 }
+  | LET expr IN expr %prec p_let                { Elet($2, $4) }
+  | DOLLAR INTLIT                               { Eletvar (nat_of_camlint $2) }
+;
+
+expr_list:
+    /* empty */                                 { Enil }
+  | expr_list_1                                 { $1 }
+;
+
+expr_list_1:
+    expr                     %prec COMMA        { Econs($1, Enil) }
+  | expr COMMA expr_list_1                      { Econs($1, $3) }
+;
+
+memory_chunk:
+    INT8S                                       { Mint8signed }
+  | INT8U                                       { Mint8unsigned }
+  | INT16S                                      { Mint16signed }
+  | INT16U                                      { Mint16unsigned }
+  | INT32                                       { Mint32 }
+  | INT                                         { Mint32 }
+  | FLOAT32                                     { Mfloat32 }
+  | FLOAT64                                     { Mfloat64 }
+  | FLOAT                                       { Mfloat64 }
+;
+
+/* Types */
+
+type_:
+    INT                                         { Tint }
+  | FLOAT                                       { Tfloat }
+;
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
new file mode 100644
index 0000000..c3d9665
--- /dev/null
+++ b/caml/Camlcoq.ml
@@ -0,0 +1,98 @@
+(* Library of useful Caml <-> Coq conversions *)
+
+open Datatypes
+open List
+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 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 n 1))
+  else Coq_xI (positive_of_camlint (Int32.shift_right 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 : int32 -> Integers.int = z_of_camlint
+
+(* 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 ->
+    "<unknown atom>"
+
+(* Lists *)
+
+let rec coqlist_iter f = function
+    Coq_nil -> ()
+  | Coq_cons(a,l) -> f a; coqlist_iter f l
+
+(* Helpers *)
+
+let rec list_iter f = function
+    [] -> ()
+  | a::l -> f a; list_iter f l
+
+let rec list_memq x = function
+    [] -> false
+  | a::l -> a == x || list_memq x l
+
+let rec list_exists p = function
+    [] -> false
+  | a::l -> p a || list_exists p l
+
+let rec list_filter p = function
+    [] -> []
+  | x :: l -> if p x then x :: list_filter p l else list_filter p l
+
+let rec length_coqlist = function
+  | Coq_nil -> 0
+  | Coq_cons (x, l) -> 1 + length_coqlist l
+
+let array_of_coqlist = function
+  | Coq_nil -> [||]
+  | Coq_cons(hd, tl) as l ->
+      let a = Array.create (length_coqlist l) hd in
+      let rec fill i = function
+        | Coq_nil -> a
+        | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in
+      fill 1 tl
+
diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml
new file mode 100644
index 0000000..f4f4bcd
--- /dev/null
+++ b/caml/Coloringaux.ml
@@ -0,0 +1,615 @@
+open Camlcoq
+open Datatypes
+open BinPos
+open BinInt
+open AST
+open Maps
+open Registers
+open Locations
+open RTL
+open RTLtyping
+open InterfGraph
+open Conventions
+
+(* George-Appel graph coloring *)
+
+(* \subsection{Internal representation of the interference graph} *)
+
+(* To implement George-Appel coloring, we first transform the representation
+   of the interference graph, switching to the following 
+   imperative representation that is well suited to the coloring algorithm. *)
+
+(* Each node of the graph (i.e. each pseudo-register) is represented as
+   follows. *)
+
+type node =
+  { ident: reg;                         (*r register identifier *)
+    typ: typ;                           (*r its type *)
+    regclass: int;                      (*r identifier of register class *)
+    spillcost: float;                   (*r estimated cost of spilling *)
+    mutable adjlist: node list;         (*r all nodes it interferes with *)
+    mutable degree: int;                (*r number of adjacent nodes *)
+    mutable movelist: move list;        (*r list of moves it is involved in *)
+    mutable alias: node option;         (*r [Some n] if coalesced with [n] *)
+    mutable color: loc option;          (*r chosen color *)
+    mutable nstate: nodestate;          (*r in which set of nodes it is *)
+    mutable nprev: node;                (*r for double linking *)
+    mutable nnext: node                 (*r for double linking *)
+  }
+
+(* These are the possible states for nodes. *)
+
+and nodestate =
+  | Colored
+  | Initial
+  | SimplifyWorklist
+  | FreezeWorklist
+  | SpillWorklist
+  | CoalescedNodes
+  | SelectStack
+
+(* Each move (i.e. wish to be put in the same location) is represented
+   as follows. *)
+
+and move =
+  { src: node;                          (*r source of the move *)
+    dst: node;                          (*r destination of the move *)
+    mutable mstate: movestate;          (*r in which set of moves it is *)
+    mutable mprev: move;                (*r for double linking *)
+    mutable mnext: move                 (*r for double linking *)
+  }
+
+(* These are the possible states for moves *)
+
+and movestate =
+  | CoalescedMoves
+  | ConstrainedMoves
+  | FrozenMoves
+  | WorklistMoves
+  | ActiveMoves
+
+(* The algorithm manipulates partitions of the nodes and of the moves
+   according to their states, frequently moving a node or a move from
+   a state to another, and frequently enumerating all nodes or all moves
+   of a given state.  To support these operations efficiently,
+   nodes or moves having the same state are put into imperative doubly-linked
+   lists, allowing for constant-time insertion and removal, and linear-time
+   scanning.  We now define the operations over these doubly-linked lists. *)
+
+module DLinkNode = struct
+  type t = node
+  let make state =
+    let rec empty =
+      { ident = Coq_xH; typ = Tint; regclass = 0;
+        adjlist = []; degree = 0; spillcost = 0.0;
+        movelist = []; alias = None; color = None;
+        nstate = state; nprev = empty; nnext = empty }
+    in empty
+  let dummy = make Colored
+  let clear dl = dl.nnext <- dl; dl.nprev <- dl
+  let notempty dl = dl.nnext != dl
+  let insert n dl =
+    n.nstate <- dl.nstate;
+    n.nnext <- dl.nnext; n.nprev <- dl;
+    dl.nnext.nprev <- n; dl.nnext <- n
+  let remove n dl =
+    assert (n.nstate = dl.nstate);
+    n.nnext.nprev <- n.nprev; n.nprev.nnext <- n.nnext
+  let move n dl1 dl2 =
+    remove n dl1; insert n dl2
+  let pick dl =
+    let n = dl.nnext in remove n dl; n
+  let iter f dl =
+    let rec iter n = if n != dl then (f n; iter n.nnext)
+    in iter dl.nnext
+  let fold f dl accu =
+    let rec fold n accu = if n == dl then accu else fold n.nnext (f n accu)
+    in fold dl.nnext accu
+end
+
+module DLinkMove = struct
+  type t = move
+  let make state =
+    let rec empty =
+      { src = DLinkNode.dummy; dst = DLinkNode.dummy; 
+        mstate = state; mprev = empty; mnext = empty }
+    in empty
+  let dummy = make CoalescedMoves
+  let clear dl = dl.mnext <- dl; dl.mprev <- dl
+  let notempty dl = dl.mnext != dl
+  let insert m dl =
+    m.mstate <- dl.mstate;
+    m.mnext <- dl.mnext; m.mprev <- dl;
+    dl.mnext.mprev <- m; dl.mnext <- m
+  let remove m dl =
+    assert (m.mstate = dl.mstate);
+    m.mnext.mprev <- m.mprev; m.mprev.mnext <- m.mnext
+  let move m dl1 dl2 =
+    remove m dl1; insert m dl2
+  let pick dl =
+    let m = dl.mnext in remove m dl; m
+  let iter f dl =
+    let rec iter m = if m != dl then (f m; iter m.mnext)
+    in iter dl.mnext
+  let fold f dl accu =
+    let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu)
+    in fold dl.mnext accu
+end
+
+(* \subsection{The George-Appel algorithm} *)
+
+(* Below is a straigthforward translation of the pseudo-code at the end
+   of the TOPLAS article by George and Appel.  Two bugs were fixed
+   and are marked as such.  Please refer to the article for explanations. *)
+
+(* Low-degree, non-move-related nodes *)
+let simplifyWorklist = DLinkNode.make SimplifyWorklist
+
+(* Low-degree, move-related nodes *)
+let freezeWorklist = DLinkNode.make FreezeWorklist
+
+(* High-degree nodes *)
+let spillWorklist = DLinkNode.make SpillWorklist
+
+(* Nodes that have been coalesced *)
+let coalescedNodes = DLinkNode.make CoalescedNodes
+
+(* Moves that have been coalesced *)
+let coalescedMoves = DLinkMove.make CoalescedMoves
+
+(* Moves whose source and destination interfere *)
+let constrainedMoves = DLinkMove.make ConstrainedMoves
+
+(* Moves that will no longer be considered for coalescing *)
+let frozenMoves = DLinkMove.make FrozenMoves
+
+(* Moves enabled for possible coalescing *)
+let worklistMoves = DLinkMove.make WorklistMoves
+
+(* Moves not yet ready for coalescing *)
+let activeMoves = DLinkMove.make ActiveMoves
+
+(* Initialization of all global data structures *)
+
+let init() =
+  DLinkNode.clear simplifyWorklist;
+  DLinkNode.clear freezeWorklist;
+  DLinkNode.clear spillWorklist;
+  DLinkNode.clear coalescedNodes;
+  DLinkMove.clear coalescedMoves;
+  DLinkMove.clear frozenMoves;
+  DLinkMove.clear worklistMoves;
+  DLinkMove.clear activeMoves
+
+(* Determine if two nodes interfere *)
+
+let interfere n1 n2 =
+  if n1.degree < n2.degree
+  then list_memq n2 n1.adjlist
+  else list_memq n1 n2.adjlist
+
+(* Add an edge to the graph.  Assume edge is not in graph already *)
+
+let addEdge n1 n2 =
+  n1.adjlist <- n2 :: n1.adjlist;
+  n1.degree  <- 1 + n1.degree;
+  n2.adjlist <- n1 :: n2.adjlist;
+  n2.degree  <- 1 + n2.degree
+
+(* Apply the given function to the relevant adjacent nodes of a node *)
+
+let iterAdjacent f n =
+  list_iter
+    (fun n ->
+      match n.nstate with
+      | SelectStack | CoalescedNodes -> ()
+      | _ -> f n)
+    n.adjlist
+
+(* Determine the moves affecting a node *)
+
+let moveIsActiveOrWorklist m =
+  match m.mstate with
+  | ActiveMoves | WorklistMoves -> true
+  | _ -> false
+
+let nodeMoves n =
+  list_filter moveIsActiveOrWorklist n.movelist
+
+(* Determine whether a node is involved in a move *)
+
+let moveRelated n =
+  list_exists moveIsActiveOrWorklist n.movelist
+
+(*i
+(* Check invariants *)
+
+let degreeInvariant n =
+  let c = ref 0 in
+  iterAdjacent (fun n -> incr c) n;
+  if !c <> n.degree then
+    fatal_error("degree invariant violated by " ^ name_of_node n)
+
+let simplifyWorklistInvariant n =
+  if n.degree < num_available_registers.(n.regclass)
+  && not (moveRelated n)
+  then ()
+  else fatal_error("simplify worklist invariant violated by " ^ name_of_node n)
+
+let freezeWorklistInvariant n =
+  if n.degree < num_available_registers.(n.regclass)
+  && moveRelated n
+  then ()
+  else fatal_error("freeze worklist invariant violated by " ^ name_of_node n)
+
+let spillWorklistInvariant n =
+  if n.degree >= num_available_registers.(n.regclass)
+  then ()
+  else fatal_error("spill worklist invariant violated by " ^ name_of_node n)
+
+let checkInvariants () =
+  DLinkNode.iter
+    (fun n -> degreeInvariant n; simplifyWorklistInvariant n)
+    simplifyWorklist;
+  DLinkNode.iter
+    (fun n -> degreeInvariant n; freezeWorklistInvariant n)
+    freezeWorklist;
+  DLinkNode.iter
+    (fun n -> degreeInvariant n; spillWorklistInvariant n)
+    spillWorklist
+i*)
+
+(* Register classes *)
+
+let class_of_type = function Tint -> 0 | Tfloat -> 1
+
+let num_register_classes = 2
+
+let caller_save_registers = [|
+  [| R3; R4; R5; R6; R7; R8; R9; R10 |];
+  [| F1; F2; F3; F4; F5; F6; F7; F8; F9; F10 |]
+|]
+
+let callee_save_registers = [|
+  [| R13; R14; R15; R16; R17; R18; R19; R20; R21; R22; 
+     R23; R24; R25; R26; R27; R28; R29; R30; R31 |];
+  [| F14; F15; F16; F17; F18; F19; F20; F21; F22; 
+     F23; F24; F25; F26; F27; F28; F29; F30; F31 |]
+|]
+
+let num_available_registers = 
+  [| Array.length caller_save_registers.(0)
+           + Array.length callee_save_registers.(0);
+     Array.length caller_save_registers.(1)
+           + Array.length callee_save_registers.(1) |]
+
+(* Build the internal representation of the graph *)
+
+let nodeOfReg r typenv spillcosts =
+  let ty = typenv r in
+  { ident = r; typ = ty; regclass = class_of_type ty;
+    spillcost = (try float(Hashtbl.find spillcosts r) with Not_found -> 0.0);
+    adjlist = []; degree = 0; movelist = []; alias = None;
+    color = None;
+    nstate = Initial;
+    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
+
+let nodeOfMreg mr =
+  let ty = mreg_type mr in
+  { ident = Coq_xH; typ = ty; regclass = class_of_type ty;
+    spillcost = 0.0;
+    adjlist = []; degree = 0; movelist = []; alias = None;
+    color = Some (R mr);
+    nstate = Colored;
+    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
+
+let build g typenv spillcosts =
+  (* Associate an internal node to each pseudo-register and each location *)
+  let reg_mapping = Hashtbl.create 27
+  and mreg_mapping = Hashtbl.create 27 in
+  let find_reg_node r =
+    try
+      Hashtbl.find reg_mapping r
+    with Not_found ->
+      let n = nodeOfReg r typenv spillcosts in
+      Hashtbl.add reg_mapping r n;
+      n
+  and find_mreg_node mr =
+    try
+      Hashtbl.find mreg_mapping mr
+    with Not_found ->
+      let n = nodeOfMreg mr in
+      Hashtbl.add mreg_mapping mr n;
+      n in
+  (* Fill the adjacency lists and compute the degrees. *)
+  SetRegReg.fold
+    (fun (Coq_pair(r1, r2)) () ->
+      addEdge (find_reg_node r1) (find_reg_node r2))
+    g.interf_reg_reg ();
+  SetRegMreg.fold
+    (fun (Coq_pair(r1, mr2)) () ->
+      addEdge (find_reg_node r1) (find_mreg_node mr2))
+    g.interf_reg_mreg ();
+  (* Process the moves and insert them in worklistMoves *)
+  let add_move n1 n2 =
+    let m =
+      { src = n1; dst = n2; mstate = WorklistMoves;
+        mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
+    n1.movelist <- m :: n1.movelist;
+    n2.movelist <- m :: n2.movelist;
+    DLinkMove.insert m worklistMoves in
+  SetRegReg.fold
+    (fun (Coq_pair(r1, r2)) () ->
+      add_move (find_reg_node r1) (find_reg_node r2))
+    g.pref_reg_reg ();
+  SetRegMreg.fold
+    (fun (Coq_pair(r1, mr2)) () ->
+      add_move (find_reg_node r1) (find_mreg_node mr2))
+    g.pref_reg_mreg ();
+  (* Initial partition of nodes into spill / freeze / simplify *)
+  Hashtbl.iter
+    (fun r n ->
+      assert (n.nstate = Initial);
+      let k = num_available_registers.(n.regclass) in
+      if n.degree >= k then
+        DLinkNode.insert n spillWorklist
+      else if moveRelated n then
+        DLinkNode.insert n freezeWorklist
+      else
+        DLinkNode.insert n simplifyWorklist)
+    reg_mapping;
+  reg_mapping
+
+(* Enable moves that have become low-degree related *)
+
+let enableMoves n =
+  list_iter
+    (fun m ->
+      if m.mstate = ActiveMoves
+      then DLinkMove.move m activeMoves worklistMoves)
+    (nodeMoves n)
+
+(* Simulate the removal of a node from the graph *)
+
+let decrementDegree n =
+  let k = num_available_registers.(n.regclass) in
+  let d = n.degree in
+  n.degree <- d - 1;
+  if d = k then begin
+    enableMoves n;
+    iterAdjacent enableMoves n;
+    if n.nstate <> Colored then begin
+      if moveRelated n
+      then DLinkNode.move n spillWorklist freezeWorklist
+      else DLinkNode.move n spillWorklist simplifyWorklist
+    end
+  end
+
+(* Simulate the effect of combining nodes [n1] and [n3] on [n2],
+   where [n2] is a node adjacent to [n3]. *)
+
+let combineEdge n1 n2 =
+  assert (n1 != n2);
+  if interfere n1 n2 then begin
+    decrementDegree n2
+  end else begin
+    n1.adjlist <- n2 :: n1.adjlist;
+    n2.adjlist <- n1 :: n2.adjlist;
+    n1.degree  <- n1.degree + 1
+  end
+
+(* Simplification of a low-degree node *)
+
+let simplify () =
+  let n = DLinkNode.pick simplifyWorklist in
+  (*i Printf.printf "Simplifying %s\n" (name_of_node n); i*)
+  n.nstate <- SelectStack;
+  iterAdjacent decrementDegree n;
+  n
+
+(* Briggs' conservative coalescing criterion *)
+
+let canConservativelyCoalesce n1 n2 =
+  let seen = ref Regset.empty in
+  let k = num_available_registers.(n1.regclass) in
+  let c = ref 0 in
+  let consider n =
+    if not (Regset.mem n.ident !seen) then begin
+      seen := Regset.add n.ident !seen;
+      if n.degree >= k then incr c
+    end in
+  iterAdjacent consider n1;
+  iterAdjacent consider n2;
+  !c < k
+
+(* Update worklists after a move was processed *)
+
+let addWorkList u =
+  if (not (u.nstate = Colored))
+  && u.degree < num_available_registers.(u.regclass)
+  && (not (moveRelated u))
+  then DLinkNode.move u freezeWorklist simplifyWorklist
+
+(* Return the canonical representative of a possibly coalesced node *)
+
+let rec getAlias n =
+  match n.alias with None -> n | Some n' -> getAlias n'
+
+(* Combine two nodes *)
+
+let combine u v =
+  (*i Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v); i*)
+  if v.nstate = FreezeWorklist
+  then DLinkNode.move v freezeWorklist coalescedNodes
+  else DLinkNode.move v spillWorklist coalescedNodes;
+  v.alias <- Some u;
+  u.movelist <- u.movelist @ v.movelist;
+  iterAdjacent (combineEdge u) v;  (*r original code using [decrementDegree] is buggy *)
+  enableMoves v;                   (*r added as per Appel's book erratum *)
+  if u.degree >= num_available_registers.(u.regclass)
+  && u.nstate = FreezeWorklist
+  then DLinkNode.move u freezeWorklist spillWorklist
+
+(* Attempt coalescing *)
+
+let coalesce () =
+  let m = DLinkMove.pick worklistMoves in
+  let x = getAlias m.src and y = getAlias m.dst in
+  let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in
+  if u == v then begin
+    DLinkMove.insert m coalescedMoves;
+    addWorkList u
+  end else if v.nstate = Colored || interfere u v then begin
+    DLinkMove.insert m constrainedMoves;
+    addWorkList u;
+    addWorkList v
+  end else if canConservativelyCoalesce u v then begin
+    DLinkMove.insert m coalescedMoves;
+    combine u v;
+    addWorkList u
+  end else begin
+    DLinkMove.insert m activeMoves    
+  end
+
+(* Freeze moves associated with node [u] *)
+
+let freezeMoves u =
+  let au = getAlias u in
+  let freeze m =
+    let y = getAlias m.src in
+    let v = if y == au then getAlias m.dst else y in
+    DLinkMove.move m activeMoves frozenMoves;
+    if not (moveRelated v)
+    && v.degree < num_available_registers.(v.regclass)
+    && v.nstate <> Colored
+    then DLinkNode.move v freezeWorklist simplifyWorklist in
+  list_iter freeze (nodeMoves u)
+
+(* Pick a move and freeze it *)
+
+let freeze () =
+  let u = DLinkNode.pick freezeWorklist in
+  (*i Printf.printf "Freezing %s\n" (name_of_node u); i*)
+  DLinkNode.insert u simplifyWorklist;
+  freezeMoves u
+
+(* Chaitin's cost measure *)
+
+let spillCost n = n.spillcost /. float n.degree
+
+(* Spill a node *)
+
+let selectSpill () =
+  (* Find a spillable node of minimal cost *)
+  let (n, cost) =
+    DLinkNode.fold
+      (fun n (best_node, best_cost as best) ->
+        let cost = spillCost n in
+        if cost < best_cost then (n, cost) else best)
+      spillWorklist (DLinkNode.dummy, infinity) in
+  assert (n != DLinkNode.dummy);
+  DLinkNode.remove n spillWorklist;
+  (*i Printf.printf "Spilling %s\n" (name_of_node n); i*)
+  freezeMoves n;
+  n.nstate <- SelectStack;
+  iterAdjacent decrementDegree n;
+  n
+
+(* Produce the order of nodes that we'll use for coloring *)
+
+let rec nodeOrder stack =
+  (*i checkInvariants(); i*)
+  if DLinkNode.notempty simplifyWorklist then
+    (let n = simplify() in nodeOrder (n :: stack))
+  else if DLinkMove.notempty worklistMoves then
+    (coalesce(); nodeOrder stack)
+  else if DLinkNode.notempty freezeWorklist then
+    (freeze(); nodeOrder stack)
+  else if DLinkNode.notempty spillWorklist then
+    (let n = selectSpill() in nodeOrder (n :: stack))
+  else
+    stack
+
+(* Assign a color (i.e. a hardware register or a stack location)
+   to a node.  The color is chosen among the colors that are not
+   assigned to nodes with which this node interferes.  The choice
+   is guided by the following heuristics: consider first caller-save
+   hardware register of the correct type; second, callee-save registers;
+   third, a stack location.  Callee-save registers and stack locations
+   are ``expensive'' resources, so we try to minimize their number
+   by picking the smallest available callee-save register or stack location.
+   In contrast, caller-save registers are ``free'', so we pick an
+   available one pseudo-randomly. *)
+
+module Locset =
+  Set.Make(struct type t = loc let compare = compare end)
+
+let start_points = Array.make num_register_classes 0
+
+let find_reg conflicts regclass =
+  let rec find avail curr last =
+    if curr >= last then None else begin
+      let l = R avail.(curr) in
+      if Locset.mem l conflicts
+      then find avail (curr + 1) last
+      else Some l
+    end in
+  let caller_save = caller_save_registers.(regclass)
+  and callee_save = callee_save_registers.(regclass)
+  and start = start_points.(regclass) in
+  match find caller_save start (Array.length caller_save) with
+  | Some _ as res ->
+      start_points.(regclass) <-
+        (if start + 1 < Array.length caller_save then start + 1 else 0);
+      res
+  | None ->
+      match find caller_save 0 start with
+      | Some _ as res ->
+          start_points.(regclass) <-
+            (if start + 1 < Array.length caller_save then start + 1 else 0);
+          res
+      | None ->
+          find callee_save 0 (Array.length callee_save)
+
+let find_slot conflicts typ =
+  let rec find curr =
+    let l = S(Local(curr, typ)) in
+    if Locset.mem l conflicts then find (coq_Zsucc curr) else l
+  in find Z0
+
+let assign_color n =
+  let conflicts = ref Locset.empty in
+  list_iter
+    (fun n' ->
+      match (getAlias n').color with
+      | None -> ()
+      | Some l -> conflicts := Locset.add l !conflicts)
+    n.adjlist;
+  match find_reg !conflicts n.regclass with
+  | Some loc ->
+      n.color <- Some loc
+  | None ->
+      n.color <- Some (find_slot !conflicts n.typ)
+
+(* Extract the location of a node *)
+
+let location_of_node n =
+  match n.color with
+  | None -> assert false
+  | Some loc -> loc
+
+(* Estimate spilling costs - TODO *)
+
+let spill_costs f = Hashtbl.create 7
+
+(* This is the entry point for graph coloring. *)
+
+let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
+                   : (reg -> loc) =
+  init();
+  Array.fill start_points 0 num_register_classes 0;
+  let mapping = build g env (spill_costs f) in
+  list_iter assign_color (nodeOrder []);
+  fun r ->
+    try location_of_node (getAlias (Hashtbl.find mapping r))
+    with Not_found -> R IT1 (* any location *)
diff --git a/caml/Coloringaux.mli b/caml/Coloringaux.mli
new file mode 100644
index 0000000..ff4cfea
--- /dev/null
+++ b/caml/Coloringaux.mli
@@ -0,0 +1,8 @@
+open Registers
+open Locations
+open RTL
+open RTLtyping
+open InterfGraph
+
+val graph_coloring:
+  coq_function -> graph -> regenv -> Regset.t -> (reg -> loc)
diff --git a/caml/Floataux.ml b/caml/Floataux.ml
new file mode 100644
index 0000000..f43efa2
--- /dev/null
+++ b/caml/Floataux.ml
@@ -0,0 +1,23 @@
+open Camlcoq
+
+let singleoffloat f =
+  Int32.float_of_bits (Int32.bits_of_float f)
+
+let intoffloat f =
+  coqint_of_camlint (Int32.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
+  | AST.Ceq -> x = y
+  | AST.Cne -> x <> y
+  | AST.Clt -> x < y
+  | AST.Cle -> x <= y
+  | AST.Cgt -> x > y
+  | AST.Cge -> x >= y
diff --git a/caml/Main2.ml b/caml/Main2.ml
new file mode 100644
index 0000000..b701419
--- /dev/null
+++ b/caml/Main2.ml
@@ -0,0 +1,34 @@
+open Printf
+open Datatypes
+
+let process_cminor_file sourcename =
+  let targetname = Filename.chop_suffix sourcename ".cm" ^ ".s" in
+  let ic = open_in sourcename in
+  let lb = Lexing.from_channel ic in
+  try
+    match Main.transf_cminor_program (CMparser.prog CMlexer.token lb) with
+    | None ->
+        eprintf "Compiler failure\n";
+        exit 2
+    | Some p ->
+        let oc = open_out targetname in
+        PrintPPC.print_program oc p;
+        close_out oc
+  with Parsing.Parse_error ->
+         eprintf "File %s, character %d: Syntax error\n"
+                 sourcename (Lexing.lexeme_start lb);
+         exit 2
+     | CMlexer.Error msg ->  
+         eprintf "File %s, character %d: %s\n"
+                 sourcename (Lexing.lexeme_start lb) msg;
+         exit 2
+
+let process_file filename =
+  if Filename.check_suffix filename ".cm" then
+    process_cminor_file filename
+  else
+    raise (Arg.Bad ("unknown file type " ^ filename))
+
+let _ =
+  Arg.parse [] process_file
+    "Usage: ccomp <options> <files>\nOptions are:"
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
new file mode 100644
index 0000000..3edcb2b
--- /dev/null
+++ b/caml/PrintPPC.ml
@@ -0,0 +1,336 @@
+(* $Id: PrintPPC.ml,v 1.2 2005/01/22 11:28:46 xleroy Exp $ *)
+
+(* Printing PPC assembly code in asm syntax *)
+
+open Printf
+open Datatypes
+open List
+open Camlcoq
+open AST
+open PPC
+
+(* On-the-fly label renaming *)
+
+let next_label = ref 100
+
+let new_label() =
+  let lbl = !next_label in incr next_label; lbl
+
+let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
+
+let label_for_label lbl =
+  try
+    Hashtbl.find current_function_labels lbl
+  with Not_found ->
+    let lbl' = new_label() in
+    Hashtbl.add current_function_labels lbl lbl';
+    lbl'
+
+(* Basic printing functions *)
+
+let print_symb oc symb =
+  fprintf oc "_%s" (extern_atom symb)
+
+let print_label oc lbl =
+  fprintf oc "L%d" (label_for_label lbl)
+
+let print_symb_ofs oc (symb, ofs) =
+  print_symb oc symb;
+  if ofs <> 0l then fprintf oc " + %ld" ofs
+
+let print_constant oc = function
+  | Cint n ->
+      fprintf oc "%ld" (camlint_of_coqint n)
+  | Csymbol_low_signed(s, n) ->
+      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+  | Csymbol_high_signed(s, n) ->
+      fprintf oc "ha16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+  | Csymbol_low_unsigned(s, n) ->
+      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+  | Csymbol_high_unsigned(s, n) ->
+      fprintf oc "hi16(%a)" print_symb_ofs (s, camlint_of_coqint n)
+
+let num_crbit = function
+  | CRbit_0 -> 0
+  | CRbit_1 -> 1
+  | CRbit_2 -> 2
+  | CRbit_3 -> 3
+
+let print_crbit oc bit =
+  fprintf oc "%d" (num_crbit bit)
+
+let print_coqint oc n =
+  fprintf oc "%ld" (camlint_of_coqint n)
+
+let int_reg_name = function
+  | GPR0 -> "r0"  | GPR1 -> "r1"  | GPR2 -> "r2"  | GPR3 -> "r3"
+  | GPR4 -> "r4"  | GPR5 -> "r5"  | GPR6 -> "r6"  | GPR7 -> "r7"
+  | GPR8 -> "r8"  | GPR9 -> "r9"  | GPR10 -> "r10" | GPR11 -> "r11"
+  | GPR12 -> "r12" | GPR13 -> "r13" | GPR14 -> "r14" | GPR15 -> "r15"
+  | GPR16 -> "r16" | GPR17 -> "r17" | GPR18 -> "r18" | GPR19 -> "r19"
+  | GPR20 -> "r20" | GPR21 -> "r21" | GPR22 -> "r22" | GPR23 -> "r23"
+  | GPR24 -> "r24" | GPR25 -> "r25" | GPR26 -> "r26" | GPR27 -> "r27"
+  | GPR28 -> "r28" | GPR29 -> "r29" | GPR30 -> "r30" | GPR31 -> "r31"
+
+let float_reg_name = function
+  | FPR0 -> "f0"  | FPR1 -> "f1"  | FPR2 -> "f2"  | FPR3 -> "f3"
+  | FPR4 -> "f4"  | FPR5 -> "f5"  | FPR6 -> "f6"  | FPR7 -> "f7"
+  | FPR8 -> "f8"  | FPR9 -> "f9"  | FPR10 -> "f10" | FPR11 -> "f11"
+  | FPR12 -> "f12" | FPR13 -> "f13" | FPR14 -> "f14" | FPR15 -> "f15"
+  | FPR16 -> "f16" | FPR17 -> "f17" | FPR18 -> "f18" | FPR19 -> "f19"
+  | FPR20 -> "f20" | FPR21 -> "f21" | FPR22 -> "f22" | FPR23 -> "f23"
+  | FPR24 -> "f24" | FPR25 -> "f25" | FPR26 -> "f26" | FPR27 -> "f27"
+  | FPR28 -> "f28" | FPR29 -> "f29" | FPR30 -> "f30" | FPR31 -> "f31"
+
+let ireg oc r = output_string oc (int_reg_name r)
+let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r
+let freg oc r = output_string oc (float_reg_name r)
+
+(* Printing of instructions *)
+
+module Labelset = Set.Make(struct type t = label let compare = compare end)
+
+let print_instruction oc labels = function
+  | Padd(r1, r2, r3) ->
+      fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Paddi(r1, r2, c) ->
+      fprintf oc "	addi	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
+  | Paddis(r1, r2, c) ->
+      fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
+  | Paddze(r1, r2) ->
+      fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
+  | Pallocframe(lo, hi) ->
+      let lo = camlint_of_coqint lo
+      and hi = camlint_of_coqint hi in
+      let nsz = Int32.neg (Int32.sub hi lo) in
+      fprintf oc "	stwu	r1, %ld(r1)\n" nsz
+  | Pand_(r1, r2, r3) ->
+      fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pandc(r1, r2, r3) ->
+      fprintf oc "	andc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pandi_(r1, r2, c) ->
+      fprintf oc "	andi.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Pandis_(r1, r2, c) ->
+      fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Pb lbl ->
+      fprintf oc "	b	%a\n" print_label lbl
+  | Pbctr ->
+      fprintf oc "	bctr\n"
+  | Pbctrl ->
+      fprintf oc "	bctrl\n"
+  | Pbf(bit, lbl) ->
+      fprintf oc "	bf	%a, %a\n" print_crbit bit print_label lbl
+  | Pbl s ->
+      fprintf oc "	bl	%a\n" print_symb s
+  | Pblr ->
+      fprintf oc "	blr\n"
+  | Pbt(bit, lbl) ->
+      fprintf oc "	bt	%a, %a\n" print_crbit bit print_label lbl
+  | Pcmplw(r1, r2) ->
+      fprintf oc "	cmplw	cr0, %a, %a\n" ireg r1 ireg r2
+  | Pcmplwi(r1, c) ->
+      fprintf oc "	cmplwi	cr0, %a, %a\n" ireg r1 print_constant c
+  | Pcmpw(r1, r2) ->
+      fprintf oc "	cmpw	cr0, %a, %a\n" ireg r1 ireg r2
+  | Pcmpwi(r1, c) ->
+      fprintf oc "	cmpwi	cr0, %a, %a\n" ireg r1 print_constant c
+  | Pcror(c1, c2, c3) ->
+      fprintf oc "	cror	%a, %a, %a\n" print_crbit c1 print_crbit c2 print_crbit c3
+  | Pdivw(r1, r2, r3) ->
+      fprintf oc "	divw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pdivwu(r1, r2, r3) ->
+      fprintf oc "	divwu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Peqv(r1, r2, r3) ->
+      fprintf oc "	eqv	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pextsb(r1, r2) ->
+      fprintf oc "	extsb	%a, %a\n" ireg r1 ireg r2
+  | Pextsh(r1, r2) ->
+      fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
+  | Pfreeframe ->
+      fprintf oc "	lwz	r1, 0(r1)\n"
+  | Pfabs(r1, r2) ->
+      fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
+  | Pfadd(r1, r2, r3) ->
+      fprintf oc "	fadd	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfcmpu(r1, r2) ->
+      fprintf oc "	fcmpu	cr0, %a, %a\n" freg r1 freg r2
+  | Pfcti(r1, r2) ->
+      fprintf oc "	fctiwz	f13, %a\n" freg r2;
+      fprintf oc "	stfdu	f13, -8(r1)\n";
+      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
+      fprintf oc "	addi	r1, r1, 8\n"
+  | Pfdiv(r1, r2, r3) ->
+      fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfmadd(r1, r2, r3, r4) ->
+      fprintf oc "	fmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfmr(r1, r2) ->
+      fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
+  | Pfmsub(r1, r2, r3, r4) ->
+      fprintf oc "	fmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
+  | Pfmul(r1, r2, r3) ->
+      fprintf oc "	fmul	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pfneg(r1, r2) ->
+      fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
+  | Pfrsp(r1, r2) ->
+      fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
+  | Pfsub(r1, r2, r3) ->
+      fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
+  | Pictf(r1, r2) ->
+      let lbl = new_label() in
+      fprintf oc "	addis	r2, 0, 0x4330\n";
+      fprintf oc "	stwu	r2, -8(r1)\n";
+      fprintf oc "	addis	r2, %a, 0x8000\n" ireg r2;
+      fprintf oc "	stw	r2, 4(r1)\n";
+      fprintf oc "	addis	r2, 0, ha16(L%d)\n" lbl;
+      fprintf oc "	lfd	f13, lo16(L%d)(r2)\n" lbl;
+      fprintf oc "	lfd	%a, 0(r1)\n" freg r1;
+      fprintf oc "	addi	r1, r1, 8\n";
+      fprintf oc "	fsub	%a, %a, f13\n" freg r1 freg r1;
+      fprintf oc "	.const_data\n";
+      fprintf oc "L%d:	.long	0x43300000, 0x80000000\n" lbl;
+      fprintf oc "	.text\n"
+  | Piuctf(r1, r2) ->
+      let lbl = new_label() in
+      fprintf oc "	addis	r2, 0, 0x4330\n";
+      fprintf oc "	stwu	r2, -8(r1)\n";
+      fprintf oc "	stw	%a, 4(r1)\n" ireg r2;
+      fprintf oc "	addis	r2, 0, ha16(L%d)\n" lbl;
+      fprintf oc "	lfd	f13, lo16(L%d)(r2)\n" lbl;
+      fprintf oc "	lfd	%a, 0(r1)\n" freg r1;
+      fprintf oc "	addi	r1, r1, 8\n";
+      fprintf oc "	fsub	%a, %a, f12\n" freg r1 freg r1;
+      fprintf oc "	.const_data\n";
+      fprintf oc "L%d:	.long	0x43300000, 0x00000000\n" lbl;
+      fprintf oc "	.text\n"
+  | Plbz(r1, c, r2) ->
+      fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Plbzx(r1, r2, r3) ->
+      fprintf oc "	lbzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Plfd(r1, c, r2) ->
+      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+  | Plfdx(r1, r2, r3) ->
+      fprintf oc "	lfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
+  | Plfi(r1, c) ->
+      let lbl = new_label() in
+      fprintf oc "	addis	r2, 0, ha16(L%d)\n" lbl;
+      fprintf oc "	lfd	%a, lo16(L%d)(r2)\n" freg r1 lbl;
+      fprintf oc "	.const_data\n";
+      let n = Int64.bits_of_float c in
+      let nlo = Int64.to_int32 n
+      and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
+      fprintf oc "L%d:	.long	0x%lx, 0x%lx   ; %f\n" lbl nhi nlo c;
+      fprintf oc "	.text\n"
+  | Plfs(r1, c, r2) ->
+      fprintf oc "	lfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+  | Plfsx(r1, r2, r3) ->
+      fprintf oc "	lfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
+  | Plha(r1, c, r2) ->
+      fprintf oc "	lha	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Plhax(r1, r2, r3) ->
+      fprintf oc "	lhax	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Plhz(r1, c, r2) ->
+      fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Plhzx(r1, r2, r3) ->
+      fprintf oc "	lhzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Plwz(r1, c, r2) ->
+      fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Plwzx(r1, r2, r3) ->
+      fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmfcrbit(r1, bit) ->
+      fprintf oc "	mfcr	r2\n";
+      fprintf oc "	rlwinm	%a, r2, %d, 1\n" ireg r1 (1 + num_crbit bit)
+  | Pmflr(r1) ->
+      fprintf oc "	mflr	%a\n" ireg r1
+  | Pmr(r1, r2) ->
+      fprintf oc "	mr	%a, %a\n" ireg r1 ireg r2
+  | Pmtctr(r1) ->
+      fprintf oc "	mtctr	%a\n" ireg r1
+  | Pmtlr(r1) ->
+      fprintf oc "	mtlr	%a\n" ireg r1
+  | Pmulli(r1, r2, c) ->
+      fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Pmullw(r1, r2, r3) ->
+      fprintf oc "	mullw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pnand(r1, r2, r3) ->
+      fprintf oc "	nand	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pnor(r1, r2, r3) ->
+      fprintf oc "	nor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Por(r1, r2, r3) ->
+      fprintf oc "	or	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Porc(r1, r2, r3) ->
+      fprintf oc "	orc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pori(r1, r2, c) ->
+      fprintf oc "	ori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Poris(r1, r2, c) ->
+      fprintf oc "	oris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Prlwinm(r1, r2, c1, c2) ->
+      fprintf oc "	rlwinm	%a, %a, %ld, 0x%lx\n"
+                ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
+  | Pslw(r1, r2, r3) ->
+      fprintf oc "	slw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psraw(r1, r2, r3) ->
+      fprintf oc "	sraw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psrawi(r1, r2, c) ->
+      fprintf oc "	srawi	%a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c)
+  | Psrw(r1, r2, r3) ->
+      fprintf oc "	srw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstb(r1, c, r2) ->
+      fprintf oc "	stb	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Pstbx(r1, r2, r3) ->
+      fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstfd(r1, c, r2) ->
+      fprintf oc "	stfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+  | Pstfdx(r1, r2, r3) ->
+      fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
+  | Pstfs(r1, c, r2) ->
+      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
+  | Pstfsx(r1, r2, r3) ->
+      fprintf oc "	stfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
+  | Psth(r1, c, r2) ->
+      fprintf oc "	sth	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Psthx(r1, r2, r3) ->
+      fprintf oc "	sthx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pstw(r1, c, r2) ->
+      fprintf oc "	stw	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
+  | Pstwx(r1, r2, r3) ->
+      fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psubfc(r1, r2, r3) ->
+      fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psubfic(r1, r2, c) ->
+      fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Pxor(r1, r2, r3) ->
+      fprintf oc "	xor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pxori(r1, r2, c) ->
+      fprintf oc "	xori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Pxoris(r1, r2, c) ->
+      fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
+  | Plabel lbl ->
+      if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
+  | Piundef r ->
+      fprintf oc "	# undef %a\n" ireg r
+  | Pfundef r ->
+      fprintf oc "	# undef %a\n" freg r
+
+let rec labels_of_code = function
+  | Coq_nil -> Labelset.empty
+  | Coq_cons((Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)), c) ->
+      Labelset.add lbl (labels_of_code c)
+  | Coq_cons(_, c) -> labels_of_code c
+
+let print_function oc (Coq_pair(name, code)) =
+  Hashtbl.clear current_function_labels;
+  fprintf oc "	.text\n";
+  fprintf oc "	.align 2\n";
+  fprintf oc "	.globl %a\n" print_symb name;
+  fprintf oc "%a:\n" print_symb name;
+  coqlist_iter (print_instruction oc (labels_of_code code)) code
+
+let print_var oc (Coq_pair(name, size)) =
+  fprintf oc "	.globl	%a\n" print_symb name;
+  fprintf oc "%a:\n" print_symb name;
+  fprintf oc "	.space	%ld\n" (camlint_of_z size)
+
+let print_program oc p =
+  coqlist_iter (print_var oc) p.prog_vars;
+  coqlist_iter (print_function oc) p.prog_funct
+
diff --git a/caml/PrintPPC.mli b/caml/PrintPPC.mli
new file mode 100644
index 0000000..fbd4004
--- /dev/null
+++ b/caml/PrintPPC.mli
@@ -0,0 +1 @@
+val print_program: out_channel -> PPC.program -> unit
diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
new file mode 100644
index 0000000..3e6ca3d
--- /dev/null
+++ b/caml/RTLgenaux.ml
@@ -0,0 +1,3 @@
+open Cminor
+
+let more_likely (c: condexpr) (ifso: stmtlist) (ifnot: stmtlist) = false