From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/Allocationaux.ml | 39 ++++ caml/Allocationaux.mli | 5 + caml/CMlexer.mli | 4 + caml/CMlexer.mll | 112 +++++++++ caml/CMparser.mly | 327 ++++++++++++++++++++++++++ caml/Camlcoq.ml | 98 ++++++++ caml/Coloringaux.ml | 615 +++++++++++++++++++++++++++++++++++++++++++++++++ caml/Coloringaux.mli | 8 + caml/Floataux.ml | 23 ++ caml/Main2.ml | 34 +++ caml/PrintPPC.ml | 336 +++++++++++++++++++++++++++ caml/PrintPPC.mli | 1 + caml/RTLgenaux.ml | 3 + 13 files changed, 1605 insertions(+) create mode 100644 caml/Allocationaux.ml create mode 100644 caml/Allocationaux.mli create mode 100644 caml/CMlexer.mli create mode 100644 caml/CMlexer.mll create mode 100644 caml/CMparser.mly create mode 100644 caml/Camlcoq.ml create mode 100644 caml/Coloringaux.ml create mode 100644 caml/Coloringaux.mli create mode 100644 caml/Floataux.ml create mode 100644 caml/Main2.ml create mode 100644 caml/PrintPPC.ml create mode 100644 caml/PrintPPC.mli create mode 100644 caml/RTLgenaux.ml (limited to 'caml') diff --git a/caml/Allocationaux.ml b/caml/Allocationaux.ml new file mode 100644 index 00000000..8e4f3284 --- /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 00000000..0cf3b944 --- /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 00000000..573c5305 --- /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 00000000..b8d3ae74 --- /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 } + | "" { 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 00000000..0b19bce9 --- /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 FLOATLIT +%token FLOATOFINT +%token FLOATOFINTU +%token GREATER +%token GREATERF +%token GREATERU +%token GREATEREQUAL +%token GREATEREQUALF +%token GREATEREQUALU +%token GREATERGREATER +%token GREATERGREATERU +%token IDENT +%token IF +%token IN +%token INT +%token INT16S +%token INT16U +%token INT32 +%token INT8S +%token INT8U +%token 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 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 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 00000000..c3d96658 --- /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 -> + "" + +(* 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 00000000..f4f4bcd3 --- /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 00000000..ff4cfeaa --- /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 00000000..f43efa27 --- /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 00000000..b7014193 --- /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 \nOptions are:" diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml new file mode 100644 index 00000000..3edcb2ba --- /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 00000000..fbd40045 --- /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 00000000..3e6ca3d3 --- /dev/null +++ b/caml/RTLgenaux.ml @@ -0,0 +1,3 @@ +open Cminor + +let more_likely (c: condexpr) (ifso: stmtlist) (ifnot: stmtlist) = false -- cgit