From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/CMlexer.mli | 17 - caml/CMlexer.mll | 132 ------- caml/CMparser.mly | 541 ---------------------------- caml/CMtypecheck.ml | 370 ------------------- caml/CMtypecheck.mli | 19 - caml/Camlcoq.ml | 130 ------- caml/Cil2Csyntax.ml | 992 --------------------------------------------------- caml/Clflags.ml | 25 -- caml/Coloringaux.ml | 625 -------------------------------- caml/Coloringaux.mli | 20 -- caml/Driver.ml | 352 ------------------ caml/Floataux.ml | 39 -- caml/Linearizeaux.ml | 85 ----- caml/PrintCsyntax.ml | 501 -------------------------- caml/PrintPPC.ml | 532 --------------------------- caml/PrintPPC.mli | 13 - caml/RTLgenaux.ml | 72 ---- caml/RTLtypingaux.ml | 156 -------- 18 files changed, 4621 deletions(-) delete mode 100644 caml/CMlexer.mli delete mode 100644 caml/CMlexer.mll delete mode 100644 caml/CMparser.mly delete mode 100644 caml/CMtypecheck.ml delete mode 100644 caml/CMtypecheck.mli delete mode 100644 caml/Camlcoq.ml delete mode 100644 caml/Cil2Csyntax.ml delete mode 100644 caml/Clflags.ml delete mode 100644 caml/Coloringaux.ml delete mode 100644 caml/Coloringaux.mli delete mode 100644 caml/Driver.ml delete mode 100644 caml/Floataux.ml delete mode 100644 caml/Linearizeaux.ml delete mode 100644 caml/PrintCsyntax.ml delete mode 100644 caml/PrintPPC.ml delete mode 100644 caml/PrintPPC.mli delete mode 100644 caml/RTLgenaux.ml delete mode 100644 caml/RTLtypingaux.ml (limited to 'caml') diff --git a/caml/CMlexer.mli b/caml/CMlexer.mli deleted file mode 100644 index c6afb72c..00000000 --- a/caml/CMlexer.mli +++ /dev/null @@ -1,17 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val token: Lexing.lexbuf -> CMparser.token -exception Error of string diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll deleted file mode 100644 index 9854117c..00000000 --- a/caml/CMlexer.mll +++ /dev/null @@ -1,132 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -{ -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 } - | "alloc" { ALLOC } - | "&" { AMPERSAND } - | "&&" { AMPERSANDAMPERSAND } - | "!" { BANG } - | "!=" { BANGEQUAL } - | "!=f" { BANGEQUALF } - | "!=u" { BANGEQUALU } - | "|" { BAR } - | "||" { BARBAR } - | "^" { CARET } - | "case" { CASE } - | ":" { COLON } - | "," { COMMA } - | "default" { DEFAULT } - | "$" { DOLLAR } - | "else" { ELSE } - | "=" { EQUAL } - | "==" { EQUALEQUAL } - | "==f" { EQUALEQUALF } - | "==u" { EQUALEQUALU } - | "exit" { EXIT } - | "extern" { EXTERN } - | "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 } - | "intuoffloat" { INTUOFFLOAT } - | "{" { 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 } - | "tailcall" { TAILCALL } - | "~" { 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 deleted file mode 100644 index 25fb0321..00000000 --- a/caml/CMparser.mly +++ /dev/null @@ -1,541 +0,0 @@ -/* *********************************************************************/ -/* */ -/* The Compcert verified compiler */ -/* */ -/* Xavier Leroy, INRIA Paris-Rocquencourt */ -/* */ -/* Copyright Institut National de Recherche en Informatique et en */ -/* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ -/* */ -/* *********************************************************************/ - -%{ -open Datatypes -open CList -open Camlcoq -open BinPos -open BinInt -open Integers -open AST -open Cminor - -(** Naming function calls in expressions *) - -type rexpr = - | Rvar of ident - | Rconst of constant - | Runop of unary_operation * rexpr - | Rbinop of binary_operation * rexpr * rexpr - | Rload of memory_chunk * rexpr - | Rcondition of rexpr * rexpr * rexpr - | Rcall of signature * rexpr * rexpr list - | Ralloc of rexpr - -let temp_counter = ref 0 - -let temporaries = ref [] - -let mktemp () = - incr temp_counter; - let n = Printf.sprintf "__t%d" !temp_counter in - let id = intern_string n in - temporaries := id :: !temporaries; - id - -let convert_accu = ref [] - -let rec convert_rexpr = function - | Rvar id -> Evar id - | Rconst c -> Econst c - | Runop(op, e1) -> Eunop(op, convert_rexpr e1) - | Rbinop(op, e1, e2) -> - let c1 = convert_rexpr e1 in - let c2 = convert_rexpr e2 in - Ebinop(op, c1, c2) - | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1) - | Rcondition(e1, e2, e3) -> - let c1 = convert_rexpr e1 in - let c2 = convert_rexpr e2 in - let c3 = convert_rexpr e3 in - Econdition(c1, c2, c3) - | Rcall(sg, e1, el) -> - let c1 = convert_rexpr e1 in - let cl = convert_rexpr_list el in - let t = mktemp() in - convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu; - Evar t - | Ralloc e1 -> - let c1 = convert_rexpr e1 in - let t = mktemp() in - convert_accu := Salloc(t, c1) :: !convert_accu; - Evar t - -and convert_rexpr_list = function - | [] -> [] - | e1 :: el -> - let c1 = convert_rexpr e1 in - let cl = convert_rexpr_list el in - c1 :: cl - -let rec prepend_seq stmts last = - match stmts with - | [] -> last - | s1 :: sl -> prepend_seq sl (Sseq(s1, last)) - -let mkeval e = - convert_accu := []; - match e with - | Rcall(sg, e1, el) -> - let c1 = convert_rexpr e1 in - let cl = convert_rexpr_list el in - prepend_seq !convert_accu (Scall(None, sg, c1, cl)) - | _ -> - ignore (convert_rexpr e); - prepend_seq !convert_accu Sskip - -let mkassign id e = - convert_accu := []; - match e with - | Rcall(sg, e1, el) -> - let c1 = convert_rexpr e1 in - let cl = convert_rexpr_list el in - prepend_seq !convert_accu (Scall(Some id, sg, c1, cl)) - | Ralloc(e1) -> - let c1 = convert_rexpr e1 in - prepend_seq !convert_accu (Salloc(id, c1)) - | _ -> - let c = convert_rexpr e in - prepend_seq !convert_accu (Sassign(id, c)) - -let mkstore chunk e1 e2 = - convert_accu := []; - let c1 = convert_rexpr e1 in - let c2 = convert_rexpr e2 in - prepend_seq !convert_accu (Sstore(chunk, c1, c2)) - -let mkifthenelse e s1 s2 = - convert_accu := []; - let c = convert_rexpr e in - prepend_seq !convert_accu (Sifthenelse(c, s1, s2)) - -let mkreturn_some e = - convert_accu := []; - let c = convert_rexpr e in - prepend_seq !convert_accu (Sreturn (Some c)) - -let mktailcall sg e1 el = - convert_accu := []; - let c1 = convert_rexpr e1 in - let cl = convert_rexpr_list el in - prepend_seq !convert_accu (Stailcall(sg, c1, cl)) - -(** Other constructors *) - -let intconst n = - Rconst(Ointconst(coqint_of_camlint n)) - -let andbool e1 e2 = - Rcondition(e1, e2, intconst 0l) -let orbool e1 e2 = - Rcondition(e1, intconst 1l, e2) - -let exitnum n = nat_of_camlint(Int32.pred n) - -let mkswitch expr (cases, dfl) = - convert_accu := []; - let c = convert_rexpr expr in - let rec mktable = function - | [] -> [] - | (key, exit) :: rem -> - Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in - prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl)) - -(*** - match (a) { case 0: s0; case 1: s1; case 2: s2; } ---> - - block { - block { - block { - block { - switch(a) { case 0: exit 0; case 1: exit 1; default: exit 2; } - }; s0; exit 2; - }; s1; exit 1; - }; s2; - } - - Note that matches are assumed to be exhaustive -***) - -let mkmatch_aux expr cases = - let ncases = Int32.of_int (List.length cases) in - let rec mktable n = function - | [] -> assert false - | [key, action] -> [] - | (key, action) :: rem -> - Coq_pair(coqint_of_camlint key, nat_of_camlint n) - :: mktable (Int32.succ n) rem in - let sw = - Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in - let rec mkblocks body n = function - | [] -> assert false - | [key, action] -> - Sblock(Sseq(body, action)) - | (key, action) :: rem -> - mkblocks - (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n))))) - (Int32.pred n) - rem in - mkblocks (Sblock sw) (Int32.pred ncases) cases - -let mkmatch expr cases = - convert_accu := []; - let c = convert_rexpr expr in - let s = - match cases with - | [] -> Sskip (* ??? *) - | [key, action] -> action - | _ -> mkmatch_aux c cases in - prepend_seq !convert_accu s - -%} - -%token ABSF -%token AMPERSAND -%token AMPERSANDAMPERSAND -%token ALLOC -%token BANG -%token BANGEQUAL -%token BANGEQUALF -%token BANGEQUALU -%token BAR -%token BARBAR -%token CARET -%token CASE -%token COLON -%token COMMA -%token DEFAULT -%token DOLLAR -%token ELSE -%token EQUAL -%token EQUALEQUAL -%token EQUALEQUALF -%token EQUALEQUALU -%token EOF -%token EXIT -%token EXTERN -%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 INTUOFFLOAT -%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 MATCH -%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 TAILCALL -%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 INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC -%left LPAREN - -/* Entry point */ - -%start prog -%type prog - -%% - -/* Programs */ - -prog: - global_declarations proc_list EOF - { { prog_funct = CList.rev $2; - prog_main = intern_string "main"; - prog_vars = CList.rev $1; } } -; - -global_declarations: - /* empty */ { [] } - | global_declarations global_declaration { $2 :: $1 } -; - -global_declaration: - VAR STRINGLIT LBRACKET INTLIT RBRACKET - { Coq_pair(Coq_pair($2, [ Init_space (z_of_camlint $4) ]), ()) } -; - -proc_list: - /* empty */ { [] } - | proc_list proc { $2 :: $1 } -; - -/* Procedures */ - -proc: - STRINGLIT LPAREN parameters RPAREN COLON signature - LBRACE - stack_declaration - var_declarations - stmt_list - RBRACE - { let tmp = !temporaries in - temporaries := []; - temp_counter := 0; - Coq_pair($1, - Internal { fn_sig = $6; - fn_params = CList.rev $3; - fn_vars = CList.rev (CList.app tmp $9); - fn_stackspace = $8; - fn_body = $10 }) } - | EXTERN STRINGLIT COLON signature - { Coq_pair($2, - External { ef_id = $2; - ef_sig = $4 }) } -; - -signature: - type_ - { {sig_args = []; sig_res = Some $1} } - | VOID - { {sig_args = []; sig_res = None} } - | type_ MINUSGREATER signature - { let s = $3 in {s with sig_args = $1 :: s.sig_args} } -; - -parameters: - /* empty */ { [] } - | parameter_list { $1 } -; - -parameter_list: - IDENT { $1 :: [] } - | parameter_list COMMA IDENT { $3 :: $1 } -; - -stack_declaration: - /* empty */ { Z0 } - | STACK INTLIT SEMICOLON { z_of_camlint $2 } -; - -var_declarations: - /* empty */ { [] } - | var_declarations var_declaration { CList.app $2 $1 } -; - -var_declaration: - VAR parameter_list SEMICOLON { $2 } -; - -/* Statements */ - -stmt: - expr SEMICOLON { mkeval $1 } - | IDENT EQUAL expr SEMICOLON { mkassign $1 $3 } - | memory_chunk LBRACKET expr RBRACKET EQUAL expr SEMICOLON - { mkstore $1 $3 $6 } - | IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 } - | IF LPAREN expr RPAREN stmts { mkifthenelse $3 $5 Sskip } - | LOOP stmts { Sloop($2) } - | LBRACELBRACE stmt_list RBRACERBRACE { Sblock($2) } - | EXIT SEMICOLON { Sexit O } - | EXIT INTLIT SEMICOLON { Sexit (exitnum $2) } - | RETURN SEMICOLON { Sreturn None } - | RETURN expr SEMICOLON { mkreturn_some $2 } - | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE - { mkswitch $3 $6 } - | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE - { mkmatch $3 $6 } - | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON - { mktailcall $7 $2 $4 } -; - -stmts: - LBRACE stmt_list RBRACE { $2 } - | stmt { $1 } -; - -stmt_list: - /* empty */ { Sskip } - | stmt stmt_list { Sseq($1, $2) } -; - -switch_cases: - DEFAULT COLON EXIT INTLIT SEMICOLON - { ([], $4) } - | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases - { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) } -; - -match_cases: - /* empty */ { [] } - | CASE INTLIT COLON stmt_list match_cases { ($2, $4) :: $5 } -; - -/* Expressions */ - -expr: - LPAREN expr RPAREN { $2 } - | IDENT { Rvar $1 } - | INTLIT { intconst $1 } - | FLOATLIT { Rconst(Ofloatconst $1) } - | STRINGLIT { Rconst(Oaddrsymbol($1, Int.zero)) } - | AMPERSAND INTLIT { Rconst(Oaddrstack(coqint_of_camlint $2)) } - | MINUS expr %prec p_uminus { Rbinop(Osub, intconst 0l, $2) } /***FIXME***/ - | MINUSF expr %prec p_uminus { Runop(Onegf, $2) } - | ABSF expr { Runop(Oabsf, $2) } - | INTOFFLOAT expr { Runop(Ointoffloat, $2) } - | INTUOFFLOAT expr { Runop(Ointuoffloat, $2) } - | FLOATOFINT expr { Runop(Ofloatofint, $2) } - | FLOATOFINTU expr { Runop(Ofloatofintu, $2) } - | TILDE expr { Runop(Onotint, $2) } - | BANG expr { Runop(Onotbool, $2) } - | INT8S expr { Runop(Ocast8signed, $2) } - | INT8U expr { Runop(Ocast8unsigned, $2) } - | INT16S expr { Runop(Ocast16signed, $2) } - | INT16U expr { Runop(Ocast16unsigned, $2) } - | FLOAT32 expr { Runop(Osingleoffloat, $2) } - | expr PLUS expr { Rbinop(Oadd, $1, $3) } - | expr MINUS expr { Rbinop(Osub, $1, $3) } - | expr STAR expr { Rbinop(Omul, $1, $3) } - | expr SLASH expr { Rbinop(Odiv, $1, $3) } - | expr PERCENT expr { Rbinop(Omod, $1, $3) } - | expr SLASHU expr { Rbinop(Odivu, $1, $3) } - | expr PERCENTU expr { Rbinop(Omodu, $1, $3) } - | expr AMPERSAND expr { Rbinop(Oand, $1, $3) } - | expr BAR expr { Rbinop(Oor, $1, $3) } - | expr CARET expr { Rbinop(Oxor, $1, $3) } - | expr LESSLESS expr { Rbinop(Oshl, $1, $3) } - | expr GREATERGREATER expr { Rbinop(Oshr, $1, $3) } - | expr GREATERGREATERU expr { Rbinop(Oshru, $1, $3) } - | expr PLUSF expr { Rbinop(Oaddf, $1, $3) } - | expr MINUSF expr { Rbinop(Osubf, $1, $3) } - | expr STARF expr { Rbinop(Omulf, $1, $3) } - | expr SLASHF expr { Rbinop(Odivf, $1, $3) } - | expr EQUALEQUAL expr { Rbinop(Ocmp Ceq, $1, $3) } - | expr BANGEQUAL expr { Rbinop(Ocmp Cne, $1, $3) } - | expr LESS expr { Rbinop(Ocmp Clt, $1, $3) } - | expr LESSEQUAL expr { Rbinop(Ocmp Cle, $1, $3) } - | expr GREATER expr { Rbinop(Ocmp Cgt, $1, $3) } - | expr GREATEREQUAL expr { Rbinop(Ocmp Cge, $1, $3) } - | expr EQUALEQUALU expr { Rbinop(Ocmpu Ceq, $1, $3) } - | expr BANGEQUALU expr { Rbinop(Ocmpu Cne, $1, $3) } - | expr LESSU expr { Rbinop(Ocmpu Clt, $1, $3) } - | expr LESSEQUALU expr { Rbinop(Ocmpu Cle, $1, $3) } - | expr GREATERU expr { Rbinop(Ocmpu Cgt, $1, $3) } - | expr GREATEREQUALU expr { Rbinop(Ocmpu Cge, $1, $3) } - | expr EQUALEQUALF expr { Rbinop(Ocmpf Ceq, $1, $3) } - | expr BANGEQUALF expr { Rbinop(Ocmpf Cne, $1, $3) } - | expr LESSF expr { Rbinop(Ocmpf Clt, $1, $3) } - | expr LESSEQUALF expr { Rbinop(Ocmpf Cle, $1, $3) } - | expr GREATERF expr { Rbinop(Ocmpf Cgt, $1, $3) } - | expr GREATEREQUALF expr { Rbinop(Ocmpf Cge, $1, $3) } - | memory_chunk LBRACKET expr RBRACKET { Rload($1, $3) } - | expr AMPERSANDAMPERSAND expr { andbool $1 $3 } - | expr BARBAR expr { orbool $1 $3 } - | expr QUESTION expr COLON expr { Rcondition($1, $3, $5) } - | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) } - | ALLOC expr { Ralloc $2 } -; - -expr_list: - /* empty */ { [] } - | expr_list_1 { $1 } -; - -expr_list_1: - expr %prec COMMA { $1 :: [] } - | expr COMMA expr_list_1 { $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/CMtypecheck.ml b/caml/CMtypecheck.ml deleted file mode 100644 index d761f759..00000000 --- a/caml/CMtypecheck.ml +++ /dev/null @@ -1,370 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* A type-checker for Cminor *) - -open Printf -open Datatypes -open CList -open Camlcoq -open AST -open Integers -open Cminor - -exception Error of string - -let name_of_typ = function Tint -> "int" | Tfloat -> "float" - -type ty = Base of typ | Var of ty option ref - -let newvar () = Var (ref None) -let tint = Base Tint -let tfloat = Base Tfloat - -let ty_of_typ = function Tint -> tint | Tfloat -> tfloat - -let ty_of_sig_args tyl = List.map ty_of_typ tyl - -let rec repr t = - match t with - | Base _ -> t - | Var r -> match !r with None -> t | Some t' -> repr t' - -let unify t1 t2 = - match (repr t1, repr t2) with - | Base b1, Base b2 -> - if b1 <> b2 then - raise (Error (sprintf "Expected type %s, actual type %s\n" - (name_of_typ b1) (name_of_typ b2))) - | Base b, Var r -> r := Some (Base b) - | Var r, Base b -> r := Some (Base b) - | Var r1, Var r2 -> r1 := Some (Var r2) - -let unify_list l1 l2 = - let ll1 = List.length l1 and ll2 = List.length l2 in - if ll1 <> ll2 then - raise (Error (sprintf "Arity mismatch: expected %d, actual %d\n" ll1 ll2)); - List.iter2 unify l1 l2 - -let type_var env id = - try - List.assoc id env - with Not_found -> - raise (Error (sprintf "Unbound variable %s\n" (extern_atom id))) - -let type_letvar env n = - let n = camlint_of_nat n in - try - List.nth env n - with Not_found -> - raise (Error (sprintf "Unbound let variable #%d\n" n)) - -let name_of_comparison = function - | Ceq -> "eq" - | Cne -> "ne" - | Clt -> "lt" - | Cle -> "le" - | Cgt -> "gt" - | Cge -> "ge" - -let type_constant = function - | Ointconst _ -> tint - | Ofloatconst _ -> tfloat - | Oaddrsymbol _ -> tint - | Oaddrstack _ -> tint - -let type_unary_operation = function - | Ocast8signed -> tint, tint - | Ocast16signed -> tint, tint - | Ocast8unsigned -> tint, tint - | Ocast16unsigned -> tint, tint - | Onegint -> tint, tint - | Onotbool -> tint, tint - | Onotint -> tint, tint - | Onegf -> tfloat, tfloat - | Oabsf -> tfloat, tfloat - | Osingleoffloat -> tfloat, tfloat - | Ointoffloat -> tfloat, tint - | Ointuoffloat -> tfloat, tint - | Ofloatofint -> tint, tfloat - | Ofloatofintu -> tint, tfloat - -let type_binary_operation = function - | Oadd -> tint, tint, tint - | Osub -> tint, tint, tint - | Omul -> tint, tint, tint - | Odiv -> tint, tint, tint - | Odivu -> tint, tint, tint - | Omod -> tint, tint, tint - | Omodu -> tint, tint, tint - | Oand -> tint, tint, tint - | Oor -> tint, tint, tint - | Oxor -> tint, tint, tint - | Oshl -> tint, tint, tint - | Oshr -> tint, tint, tint - | Oshru -> tint, tint, tint - | Oaddf -> tfloat, tfloat, tfloat - | Osubf -> tfloat, tfloat, tfloat - | Omulf -> tfloat, tfloat, tfloat - | Odivf -> tfloat, tfloat, tfloat - | Ocmp _ -> tint, tint, tint - | Ocmpu _ -> tint, tint, tint - | Ocmpf _ -> tfloat, tfloat, tint - -let name_of_constant = function - | Ointconst n -> sprintf "intconst %ld" (camlint_of_coqint n) - | Ofloatconst n -> sprintf "floatconst %g" n - | Oaddrsymbol (s, ofs) -> sprintf "addrsymbol %s %ld" (extern_atom s) (camlint_of_coqint ofs) - | Oaddrstack n -> sprintf "addrstack %ld" (camlint_of_coqint n) - -let name_of_unary_operation = function - | Ocast8signed -> "cast8signed" - | Ocast16signed -> "cast16signed" - | Ocast8unsigned -> "cast8unsigned" - | Ocast16unsigned -> "cast16unsigned" - | Onegint -> "negint" - | Onotbool -> "notbool" - | Onotint -> "notint" - | Onegf -> "negf" - | Oabsf -> "absf" - | Osingleoffloat -> "singleoffloat" - | Ointoffloat -> "intoffloat" - | Ointuoffloat -> "intuoffloat" - | Ofloatofint -> "floatofint" - | Ofloatofintu -> "floatofintu" - -let name_of_binary_operation = function - | Oadd -> "add" - | Osub -> "sub" - | Omul -> "mul" - | Odiv -> "div" - | Odivu -> "divu" - | Omod -> "mod" - | Omodu -> "modu" - | Oand -> "and" - | Oor -> "or" - | Oxor -> "xor" - | Oshl -> "shl" - | Oshr -> "shr" - | Oshru -> "shru" - | Oaddf -> "addf" - | Osubf -> "subf" - | Omulf -> "mulf" - | Odivf -> "divf" - | Ocmp c -> sprintf "cmp %s" (name_of_comparison c) - | Ocmpu c -> sprintf "cmpu %s" (name_of_comparison c) - | Ocmpf c -> sprintf "cmpf %s" (name_of_comparison c) - -let type_chunk = function - | Mint8signed -> tint - | Mint8unsigned -> tint - | Mint16signed -> tint - | Mint16unsigned -> tint - | Mint32 -> tint - | Mfloat32 -> tfloat - | Mfloat64 -> tfloat - -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - -let rec type_expr env lenv e = - match e with - | Evar id -> - type_var env id - | Econst cst -> - type_constant cst - | Eunop(op, e1) -> - let te1 = type_expr env lenv e1 in - let (targ, tres) = type_unary_operation op in - begin try - unify targ te1 - with Error s -> - raise (Error (sprintf "In application of operator %s:\n%s" - (name_of_unary_operation op) s)) - end; - tres - | Ebinop(op, e1, e2) -> - let te1 = type_expr env lenv e1 in - let te2 = type_expr env lenv e2 in - let (targ1, targ2, tres) = type_binary_operation op in - begin try - unify targ1 te1; unify targ2 te2 - with Error s -> - raise (Error (sprintf "In application of operator %s:\n%s" - (name_of_binary_operation op) s)) - end; - tres - | Eload(chunk, e) -> - let te = type_expr env lenv e in - begin try - unify tint te - with Error s -> - raise (Error (sprintf "In load %s:\n%s" - (name_of_chunk chunk) s)) - end; - type_chunk chunk - | Econdition(e1, e2, e3) -> - type_condexpr env lenv e1; - let te2 = type_expr env lenv e2 in - let te3 = type_expr env lenv e3 in - begin try - unify te2 te3 - with Error s -> - raise (Error (sprintf "In conditional expression:\n%s" s)) - end; - te2 -(* - | Elet(e1, e2) -> - let te1 = type_expr env lenv e1 in - let te2 = type_expr env (te1 :: lenv) e2 in - te2 - | Eletvar n -> - type_letvar lenv n -*) - -and type_exprlist env lenv el = - match el with - | [] -> [] - | e1 :: et -> - let te1 = type_expr env lenv e1 in - let tet = type_exprlist env lenv et in - (te1 :: tet) - -and type_condexpr env lenv e = - let te = type_expr env lenv e in - begin try - unify tint te - with Error s -> - raise (Error (sprintf "In condition:\n%s" s)) - end - -let rec type_stmt env blk ret s = - match s with - | Sskip -> () - | Sassign(id, e1) -> - let tid = type_var env id in - let te1 = type_expr env [] e1 in - begin try - unify tid te1 - with Error s -> - raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s)) - end - | Sstore(chunk, e1, e2) -> - let te1 = type_expr env [] e1 in - let te2 = type_expr env [] e2 in - begin try - unify tint te1; - unify (type_chunk chunk) te2 - with Error s -> - raise (Error (sprintf "In store %s:\n%s" - (name_of_chunk chunk) s)) - end - | Scall(optid, sg, e1, el) -> - let te1 = type_expr env [] e1 in - let tel = type_exprlist env [] el in - begin try - unify tint te1; - unify_list (ty_of_sig_args sg.sig_args) tel; - let ty_res = - match sg.sig_res with - | None -> tint (*???*) - | Some t -> ty_of_typ t in - begin match optid with - | None -> () - | Some id -> unify (type_var env id) ty_res - end - with Error s -> - raise (Error (sprintf "In call:\n%s" s)) - end - | Salloc(id, e) -> - let tid = type_var env id in - let te = type_expr env [] e in - begin try - unify tint te; - unify tint tid - with Error s -> - raise (Error (sprintf "In alloc:\n%s" s)) - end - | Sseq(s1, s2) -> - type_stmt env blk ret s1; - type_stmt env blk ret s2 - | Sifthenelse(ce, s1, s2) -> - type_condexpr env [] ce; - type_stmt env blk ret s1; - type_stmt env blk ret s2 - | Sloop s1 -> - type_stmt env blk ret s1 - | Sblock s1 -> - type_stmt env (blk + 1) ret s1 - | Sexit n -> - if camlint_of_nat n >= blk then - raise (Error (sprintf "Bad exit(%d)\n" (camlint_of_nat n))) - | Sswitch(e, cases, deflt) -> - unify (type_expr env [] e) tint - | Sreturn None -> - begin match ret with - | None -> () - | Some tret -> raise (Error ("return without argument")) - end - | Sreturn (Some e) -> - begin match ret with - | None -> raise (Error "return with argument") - | Some tret -> - begin try - unify (type_expr env [] e) (ty_of_typ tret) - with Error s -> - raise (Error (sprintf "In return:\n%s" s)) - end - end - | Stailcall(sg, e1, el) -> - let te1 = type_expr env [] e1 in - let tel = type_exprlist env [] el in - begin try - unify tint te1; - unify_list (ty_of_sig_args sg.sig_args) tel - with Error s -> - raise (Error (sprintf "In tail call:\n%s" s)) - end - | Slabel(lbl, s1) -> - type_stmt env blk ret s1 - | Sgoto lbl -> - () - -let rec env_of_vars idl = - match idl with - | [] -> [] - | id1 :: idt -> (id1, newvar()) :: env_of_vars idt - -let type_function id f = - try - type_stmt - (env_of_vars f.fn_vars @ env_of_vars f.fn_params) - 0 f.fn_sig.sig_res f.fn_body - with Error s -> - raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) - -let type_fundef (Coq_pair (id, fd)) = - match fd with - | Internal f -> type_function id f - | External ef -> () - -let type_program p = - List.iter type_fundef p.prog_funct; p diff --git a/caml/CMtypecheck.mli b/caml/CMtypecheck.mli deleted file mode 100644 index 44c76544..00000000 --- a/caml/CMtypecheck.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -exception Error of string - -val type_program: Cminor.program -> Cminor.program - diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml deleted file mode 100644 index 98fd79c8..00000000 --- a/caml/Camlcoq.ml +++ /dev/null @@ -1,130 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Library of useful Caml <-> Coq conversions *) - -open Datatypes -open CList -open BinPos -open BinInt - -(* Integers *) - -let rec camlint_of_positive = function - | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l - | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1 - | Coq_xH -> 1l - -let camlint_of_z = function - | Z0 -> 0l - | Zpos p -> camlint_of_positive p - | Zneg p -> Int32.neg (camlint_of_positive p) - -let camlint_of_coqint : Integers.int -> int32 = camlint_of_z - -let rec camlint_of_nat = function - | O -> 0 - | S n -> camlint_of_nat n + 1 - -let rec nat_of_camlint n = - assert (n >= 0l); - if n = 0l then O else S (nat_of_camlint (Int32.sub n 1l)) - -let rec positive_of_camlint n = - if n = 0l then assert false else - if n = 1l then Coq_xH else - if Int32.logand n 1l = 0l - then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1)) - else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1)) - -let z_of_camlint n = - if n = 0l then Z0 else - if n > 0l then Zpos (positive_of_camlint n) - else Zneg (positive_of_camlint (Int32.neg n)) - -let coqint_of_camlint (n: int32) : Integers.int = - (* Interpret n as unsigned so that resulting Z is in range *) - if n = 0l then Z0 else Zpos (positive_of_camlint n) - -(* Atoms (positive integers representing strings) *) - -let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t) -let string_of_atom = (Hashtbl.create 17 : (positive, string) Hashtbl.t) -let next_atom = ref Coq_xH - -let intern_string s = - try - Hashtbl.find atom_of_string s - with Not_found -> - let a = !next_atom in - next_atom := coq_Psucc !next_atom; - Hashtbl.add atom_of_string s a; - Hashtbl.add string_of_atom a s; - a - -let extern_atom a = - try - Hashtbl.find string_of_atom a - with Not_found -> - Printf.sprintf "" (camlint_of_positive a) - -(* Strings *) - -let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) = - Char.chr( (if a0 then 1 else 0) - + (if a1 then 2 else 0) - + (if a2 then 4 else 0) - + (if a3 then 8 else 0) - + (if a4 then 16 else 0) - + (if a5 then 32 else 0) - + (if a6 then 64 else 0) - + (if a7 then 128 else 0)) - -let coqstring_length s = - let rec len accu = function - | CString.EmptyString -> accu - | CString.CString(_, s) -> len (accu + 1) s - in len 0 s - -let camlstring_of_coqstring s = - let r = String.create (coqstring_length s) in - let rec fill pos = function - | CString.EmptyString -> r - | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s - in fill 0 s - -(* Timing facility *) - -(* -let timers = (Hashtbl.create 9 : (string, float) Hashtbl.t) - -let add_to_timer name time = - let old = try Hashtbl.find timers name with Not_found -> 0.0 in - Hashtbl.replace timers name (old +. time) - -let time name fn arg = - let start = Unix.gettimeofday() in - try - let res = fn arg in - add_to_timer name (Unix.gettimeofday() -. start); - res - with x -> - add_to_timer name (Unix.gettimeofday() -. start); - raise x - -let print_timers () = - Hashtbl.iter - (fun name time -> Printf.printf "%-20s %.3f\n" name time) - timers - -let _ = at_exit print_timers -*) diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml deleted file mode 100644 index 41fe1d4f..00000000 --- a/caml/Cil2Csyntax.ml +++ /dev/null @@ -1,992 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Thomas Moniot, INRIA Paris-Rocquencourt *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(************************************************************************** -CIL -> CabsCoq translator -**************************************************************************) - -open Cil -open CList -open Camlcoq -open AST -open Csyntax - - - - -module type TypeSpecifierTranslator = - sig - val convertIkind: Cil.ikind -> (intsize * signedness) option - val convertFkind: Cil.fkind -> floatsize option - end - - - - - -module Make(TS: TypeSpecifierTranslator) = struct -(*-----------------------------------------------------------------------*) - - -(** Pre-defined constants *) -let constInt32 = Tint (I32, Signed) -let constInt32uns = Tint (I32, Unsigned) -let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32) - - -(** Global variables *) -let currentLocation = ref Cil.locUnknown -let currentGlobalPrefix = ref "" -let stringNum = ref 0 (* number of next global for string literals *) -let stringTable = Hashtbl.create 47 - -(** ** Functions related to [struct]s and [union]s *) - -(* Unroll recursion in struct or union types: - substitute [Tcomp_ptr id] by [Tpointer compty] in [ty]. *) - -let unrollType id compty ty = - let rec unrType ty = - match ty with - | Tvoid -> ty - | Tint(sz, sg) -> ty - | Tfloat sz -> ty - | Tpointer ty -> Tpointer (unrType ty) - | Tarray(ty, sz) -> Tarray (unrType ty, sz) - | Tfunction(args, res) -> Tfunction(unrTypelist args, unrType res) - | Tstruct(id', fld) -> - if id' = id then ty else Tstruct(id', unrFieldlist fld) - | Tunion(id', fld) -> - if id' = id then ty else Tunion(id', unrFieldlist fld) - | Tcomp_ptr id' -> - if id' = id then Tpointer compty else ty - and unrTypelist = function - | Tnil -> Tnil - | Tcons(hd, tl) -> Tcons(unrType hd, unrTypelist tl) - and unrFieldlist = function - | Fnil -> Fnil - | Fcons(id, ty, tl) -> Fcons(id, unrType ty, unrFieldlist tl) - in unrType ty - -(* Return the type of a [struct] field *) -let rec getFieldType f = function - | Fnil -> raise Not_found - | Fcons(idf, t, rem) -> if idf = f then t else getFieldType f rem - -(** ** Some functions over lists *) - -(** Keep the elements in a list from [elt] (included) to the end - (used for the translation of the [switch] statement) *) -let rec keepFrom elt = function - | [] -> [] - | (x :: l) as l' -> if x == elt then l' else keepFrom elt l - -(** Keep the elements in a list before [elt'] (excluded) - (used for the translation of the [switch] statement) *) -let rec keepUntil elt' = function - | [] -> [] - | x :: l -> if x == elt' then [] else x :: (keepUntil elt' l) - -(** Keep the elements in a list from [elt] (included) to [elt'] (excluded) - (used for the translation of the [switch] statement) *) -let keepBetween elt elt' l = - keepUntil elt' (keepFrom elt l) - -(** ** Functions used to handle locations *) - -(** Update the current location *) -let updateLoc loc = - currentLocation := loc - -(** Convert the current location into a string *) -let currentLoc() = - match !currentLocation with { line=l; file=f } -> - f ^ ":" ^ (if l = -1 then "?" else string_of_int l) ^ ": " - -(** Exception raised when an unsupported feature is encountered *) -exception Unsupported of string -let unsupported msg = - raise (Unsupported(currentLoc() ^ "Unsupported C feature: " ^ msg)) - -(** Exception raised when an internal error is encountered *) -exception Internal_error of string -let internal_error msg = - raise (Internal_error(currentLoc() ^ "Internal error: " ^ msg)) - -(** Warning messages *) -let warning msg = - prerr_string (currentLoc()); - prerr_string "Warning: "; - prerr_endline msg - -(** ** Functions used to handle string literals *) -let name_for_string_literal s = - try - Hashtbl.find stringTable s - with Not_found -> - incr stringNum; - let symbol_name = - Printf.sprintf "_%s__stringlit_%d" - !currentGlobalPrefix !stringNum in - let symbol_ident = intern_string symbol_name in - Hashtbl.add stringTable s symbol_ident; - symbol_ident - -let typeStringLiteral s = - Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1))) - -let global_for_string s id = - let init = ref [] in - let add_char c = - init := - AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))) - :: !init in - add_char '\000'; - for i = String.length s - 1 downto 0 do add_char s.[i] done; - Datatypes.Coq_pair(Datatypes.Coq_pair(id, !init), typeStringLiteral s) - -let globals_for_strings globs = - Hashtbl.fold - (fun s id l -> global_for_string s id :: l) - stringTable globs - -(** ** Handling of stubs for variadic functions *) - -let stub_function_table = Hashtbl.create 47 - -let register_stub_function name tres targs = - let rec letters_of_type = function - | Tnil -> [] - | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl - | Tcons(_, tl) -> "i" :: letters_of_type tl in - let stub_name = - name ^ "$" ^ String.concat "" (letters_of_type targs) in - try - (stub_name, Hashtbl.find stub_function_table stub_name) - with Not_found -> - let rec types_of_types = function - | Tnil -> Tnil - | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) - | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in - let stub_type = Tfunction (types_of_types targs, tres) in - Hashtbl.add stub_function_table stub_name stub_type; - (stub_name, stub_type) - -let declare_stub_function stub_name stub_type = - match stub_type with - | Tfunction(targs, tres) -> - Datatypes.Coq_pair(intern_string stub_name, - External(intern_string stub_name, targs, tres)) - | _ -> assert false - -let declare_stub_functions k = - Hashtbl.fold (fun n i k -> declare_stub_function n i :: k) - stub_function_table k - -(** ** Generation of temporary variable names *) - -let current_function = ref (None: Cil.fundec option) - -let make_temp typ = - match !current_function with - | None -> assert false - | Some f -> - let v = Cil.makeTempVar f typ in - intern_string v.vname - -(** Detect and report GCC's __builtin_ functions *) - -let check_builtin s = - let b = "__builtin_" in - if String.length s >= String.length b - && String.sub s 0 (String.length b) = b - then unsupported ("GCC `" ^ s ^ "' built-in function") - -(** ** Translation functions *) - -(** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) -let convertIkind ik = - match TS.convertIkind ik with - | Some p -> p - | None -> unsupported "integer type specifier" - - -(** Convert a [Cil.fkind] into a [floatsize] *) -let convertFkind fk = - match TS.convertFkind fk with - | Some fs -> fs - | None -> unsupported "floating-point type specifier" - - -(** Convert a [Cil.constant] into a [CabsCoq.expr] *) -let rec convertConstant = function - | CInt64 (i64, _, _) -> - let i = coqint_of_camlint (Int64.to_int32 i64) in - Expr (Econst_int i, constInt32) - | CStr s -> - let symb = name_for_string_literal s in - Expr (Evar symb, typeStringLiteral s) - | CWStr _ -> - unsupported "wide string literal" - | CChr c -> - let i = coqint_of_camlint (Int32.of_int (Char.code c)) in - Expr (Econst_int i, constInt32) - | CReal (f, _, _) -> - Expr (Econst_float f, Tfloat F64) - | (CEnum (exp, str, enumInfo)) as enum -> - (* do constant folding on an enum constant *) - let e = Cil.constFold false (Const enum) in - convertExp e - - -(** Convert a [Cil.UnOp] into a [CabsCoq.expr] - ([t] is the type of the result of applying [uop] to [e]) *) -and convertUnop uop e t = - let e' = convertExp e in - let t' = convertTyp t in - let uop' = match uop with - | Neg -> Eunop (Oneg, e') - | BNot -> Eunop (Onotint, e') - | LNot -> Eunop (Onotbool, e') - in - Expr (uop', t') - - -(** Convert a [Cil.BinOp] into a [CabsCoq.expr] - ([t] is the type of the result of applying [bop] to [(e1, e2)], every - arithmetic conversion being made explicit by CIL for both arguments] *) -and convertBinop bop e1 e2 t = - let e1' = convertExp e1 in - let e2' = convertExp e2 in - let t' = convertTyp t in - let bop' = match bop with - | PlusA -> Ebinop (Oadd, e1', e2') - | PlusPI -> Ebinop (Oadd, e1', e2') - | IndexPI -> Ebinop (Oadd, e1', e2') - | MinusA -> Ebinop (Osub, e1', e2') - | MinusPI -> Ebinop (Osub, e1', e2') - | MinusPP -> Ebinop (Osub, e1', e2') - | Mult -> Ebinop (Omul, e1', e2') - | Div -> Ebinop (Odiv, e1', e2') - | Mod -> Ebinop (Omod, e1', e2') - | Shiftlt -> Ebinop (Oshl, e1', e2') - | Shiftrt -> Ebinop (Oshr, e1', e2') - | Lt -> Ebinop (Olt, e1', e2') - | Gt -> Ebinop (Ogt, e1', e2') - | Le -> Ebinop (Ole, e1', e2') - | Ge -> Ebinop (Oge, e1', e2') - | Eq -> Ebinop (Oeq, e1', e2') - | Ne -> Ebinop (One, e1', e2') - | BAnd -> Ebinop (Oand, e1', e2') - | BXor -> Ebinop (Oxor, e1', e2') - | BOr -> Ebinop (Oor, e1', e2') - | LAnd -> Eandbool (e1', e2') - | LOr -> Eorbool (e1', e2') - in - Expr (bop', t') - - -(** Test if two types are compatible - (in order to cast one of the types to the other) *) -and compatibleTypes t1 t2 = true -(* - let isArithmeticType = function - | Tint _ | Tfloat _ -> true - | _ -> false - in - let isPointerType = function - | Tpointer _ | Tarray _ -> true - | _ -> false - in - (t1 = t2) - || (isArithmeticType t1 && isArithmeticType t2) - || match (t1, t2) with - | (Tpointer Tvoid, t) | (t, Tpointer Tvoid) -> isPointerType t - | (Tint _, t) | (t, Tint _) -> isPointerType t - | _ -> false -*) - - -(** Convert a [Cil.CastE] into a [CabsCoq.expr] - (fail if the cast is illegal) *) -and processCast t e = - let t' = convertTyp t in - let te = convertTyp (Cil.typeOf e) in - if compatibleTypes t' te then - let e' = convertExp e in - Expr (Ecast (t', e'), t') - else internal_error "processCast: illegal cast" - - -(** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *) -and processParamsE = function - | [] -> [] - | e :: l -> - let (Expr (_, t)) as e' = convertExp e in - match t with - | Tstruct _ | Tunion _ -> - unsupported "function parameter of struct or union type" - | _ -> e' :: processParamsE l - - -(** Convert a [Cil.exp] into a [CabsCoq.expr] *) -and convertExp = function - | Const c -> - convertConstant c - | Lval lv -> - convertLval lv - | SizeOf t -> - Expr (Esizeof (convertTyp t), constInt32uns) - | SizeOfE e -> - let ty = convertTyp (Cil.typeOf e) in - Expr (Esizeof ty, constInt32uns) - | SizeOfStr str -> - let n = coqint_of_camlint (Int32.of_int(String.length str)) in - Expr (Econst_int n, constInt32uns) - | AlignOf t -> - unsupported "GCC `alignof' construct" - | AlignOfE e -> - unsupported "GCC `alignof' construct" - | UnOp (uop, e, t) -> - convertUnop uop e t - | BinOp (bop, e1, e2, t) -> - convertBinop bop e1 e2 t - | CastE (t, e) -> - processCast t e - | AddrOf lv -> - let (Expr (_, t)) as e = convertLval lv in - Expr (Eaddrof e, Tpointer t) - | StartOf lv -> - (* convert an array into a pointer to the beginning of the array *) - match Cil.unrollType (Cil.typeOfLval lv) with - | TArray (t, _, _) -> - let t' = convertTyp t in - let tPtr = Tpointer t' in - let e = convertLval lv in - (* array A of type T replaced by (T* )A *) - Expr (Ecast (tPtr, e), tPtr) - | _ -> internal_error "convertExp: StartOf applied to a \ - lvalue whose type is not an array" - - -(** Convert a [Cil.lval] into a [CabsCoq.expression] *) -and convertLval lv = - (* convert the offset of the lvalue *) - let rec processOffset ((Expr (_, t)) as e) = function - | NoOffset -> e - | Field (f, ofs) -> - begin match t with - | Tstruct(id, fList) -> - begin try - let idf = intern_string f.fname in - let t' = unrollType id t (getFieldType idf fList) in - processOffset (Expr (Efield (e, idf), t')) ofs - with Not_found -> - internal_error "processOffset: no such struct field" - end - | Tunion(id, fList) -> - begin try - let idf = intern_string f.fname in - let t' = unrollType id t (getFieldType idf fList) in - processOffset (Expr (Efield (e, idf), t')) ofs - with Not_found -> - internal_error "processOffset: no such union field" - end - | _ -> - internal_error "processOffset: Field on a non-struct nor union" - end - | Index (e', ofs) -> - match t with - | Tarray (t', _) -> - let e'' = Ederef(Expr (Ebinop(Oadd, e, convertExp e'), t)) in - processOffset (Expr (e'', t')) ofs - | _ -> internal_error "processOffset: Index on a non-array" - in - (* convert the lvalue *) - match lv with - | (Var v, ofs) -> - check_builtin v.vname; - let id = intern_string v.vname in - processOffset (Expr (Evar id, convertTyp v.vtype)) ofs - | (Mem e, ofs) -> - match Cil.unrollType (Cil.typeOf e) with - | TPtr (t, _) -> let e' = Ederef (convertExp e) in - processOffset (Expr (e', convertTyp t)) ofs - | _ -> internal_error "convertLval: Mem on a non-pointer" - - -(** Convert a [(Cil.string * Cil.typ * Cil.attributes)] list - into a [typelist] *) -and processParamsT convert = function - | [] -> Tnil - | (_, t, _) :: l -> - let t' = convert t in - match t' with - | Tstruct _ | Tunion _ -> - unsupported "function parameter of struct or union type" - | _ -> Tcons (t', processParamsT convert l) - - -(** Convert a [Cil.typ] into a [coq_type] *) -and convertTypGen env = function - | TVoid _ -> Tvoid - | TInt (k, _) -> let (x, y) = convertIkind k in Tint (x, y) - | TFloat (k, _) -> Tfloat (convertFkind k) - | TPtr (TComp(c, _), _) when List.mem c.ckey env -> - Tcomp_ptr (intern_string (Cil.compFullName c)) - | TPtr (t, _) -> Tpointer (convertTypGen env t) - | TArray (t, eOpt, _) -> - begin match eOpt with - | None -> - warning "array type of unspecified size"; - Tarray (convertTypGen env t, coqint_of_camlint 0l) - | Some e -> - match Cil.constFold true e with - | Const (CInt64 (i64, _, _)) -> - Tarray (convertTypGen env t, - coqint_of_camlint (Int64.to_int32 i64)) - | _ -> unsupported "size of array type not an integer constant" - end - | TFun (t, argListOpt, vArg, _) -> - if vArg then unsupported "variadic function type"; - let argList = - match argListOpt with - | None -> unsupported "un-prototyped function type" - | Some l -> l - in - let t' = convertTypGen env t in - begin match t' with - | Tstruct _ | Tunion _ -> - unsupported "return type is a struct or union" - | _ -> Tfunction (processParamsT (convertTypGen env) argList, t') - end - | TNamed (tinfo, _) -> convertTypGen env tinfo.ttype - | TComp (c, _) -> - let rec convertFieldList = function - | [] -> Fnil - | {fname=str; ftype=t} :: rem -> - let idf = intern_string str in - let t' = convertTypGen (c.ckey :: env) t in - Fcons(idf, t', convertFieldList rem) in - let fList = convertFieldList c.cfields in - let id = intern_string (Cil.compFullName c) in - if c.cstruct then Tstruct(id, fList) else Tunion(id, fList) - | TEnum _ -> constInt32 (* enum constants are integers *) - | TBuiltin_va_list _ -> unsupported "GCC `builtin va_list' type" - -and convertTyp ty = convertTypGen [] ty - -(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] *) -let convertVarinfo v = - updateLoc(v.vdecl); - let id = intern_string v.vname in - Datatypes.Coq_pair (id, convertTyp v.vtype) - - -(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] - (fail if the variable is of type struct or union) *) -let convertVarinfoParam v = - updateLoc(v.vdecl); - let id = intern_string v.vname in - let t' = convertTyp v.vtype in - match t' with - | Tstruct _ | Tunion _ -> - unsupported "function parameter of struct or union type" - | _ -> Datatypes.Coq_pair (id, t') - - -(** Convert a [Cil.exp] which has a function type into a [CabsCoq.expr] - (used only to translate function calls) *) -let convertExpFuncall e eList = - match typeOf e with - | TFun (res, argListOpt, vArg, _) -> - begin match argListOpt, vArg with - | Some argList, false -> - (* Prototyped, non-variadic function *) - if List.length argList <> List.length eList then - internal_error "convertExpFuncall: wrong number of arguments"; - (convertExp e, processParamsE eList) - | _, _ -> - (* Variadic or unprototyped function: generate a call to - a stub function with the appropriate number and types - of arguments. Works only if the function expression e - is a global variable. *) - let params = processParamsE eList in - let fun_name = - match e with - | Lval(Var v, NoOffset) -> - warning "working around a call to a variadic function"; - v.vname - | _ -> - unsupported "call to variadic function" in - let rec typeOfExprList = function - | [] -> Tnil - | Expr (_, ty) :: rem -> Tcons (ty, typeOfExprList rem) in - let targs = typeOfExprList params in - let tres = convertTyp res in - let (stub_fun_name, stub_fun_typ) = - register_stub_function fun_name tres targs in - (Expr(Evar(intern_string stub_fun_name), stub_fun_typ), - params) - end - | _ -> internal_error "convertExpFuncall: not a function" - -(** Auxiliaries for function calls *) - -let makeFuncall1 tyfun (Expr(_, tlhs) as elhs) efun eargs = - match tyfun with - | TFun (t, _, _, _) -> - let tres = convertTyp t in - if tlhs = tres then - Scall(Datatypes.Some elhs, efun, eargs) - else begin - let tmp = make_temp t in - let elhs' = Expr(Evar tmp, tres) in - Ssequence(Scall(Datatypes.Some elhs', efun, eargs), - Sassign(elhs, Expr(Ecast(tlhs, elhs'), tlhs))) - end - | _ -> internal_error "wrong type for function in call" - -let makeFuncall2 tyfun tylhs elhs efun eargs = - match elhs with - | Expr(Evar _, _) -> - makeFuncall1 tyfun elhs efun eargs - | Expr(_, tlhs) -> - let tmp = make_temp tylhs in - let elhs' = Expr(Evar tmp, tlhs) in - Ssequence(makeFuncall1 tyfun elhs' efun eargs, - Sassign(elhs, elhs')) - - -(** Convert a [Cil.instr list] into a [CabsCoq.statement] *) -let rec processInstrList l = - (* convert an instruction *) - let convertInstr = function - | Set (lv, e, loc) -> - updateLoc(loc); - begin match convertTyp (Cil.typeOf e) with - | Tstruct _ | Tunion _ -> unsupported "struct or union assignment" - | t -> Sassign (convertLval lv, convertExp e) - end - | Call (None, e, eList, loc) -> - updateLoc(loc); - let (efun, params) = convertExpFuncall e eList in - Scall(Datatypes.None, efun, params) - | Call (Some lv, e, eList, loc) -> - updateLoc(loc); - let (efun, params) = convertExpFuncall e eList in - makeFuncall2 (Cil.typeOf e) (Cil.typeOfLval lv) (convertLval lv) efun params - | Asm (_, _, _, _, _, loc) -> - updateLoc(loc); - unsupported "inline assembly" - in - (* convert a list of instructions *) - match l with - | [] -> Sskip - | [s] -> convertInstr s - | s :: l -> - let cs = convertInstr s in - let cl = processInstrList l in - Ssequence (cs, cl) - - -(** Convert a [Cil.stmt list] into a [CabsCoq.statement] *) -let rec processStmtList = function - | [] -> Sskip - | [s] -> convertStmt s - | s :: l -> - let cs = convertStmt s in - let cl = processStmtList l in - Ssequence (cs, cl) - - -(** Return the list of the constant expressions in a label list - (return [None] if this is the default case) - (fail if the constant expression is not of type integer) *) -and getCaseList lblList = - match lblList with - | [] -> Some [] - | Label (_, loc, _) :: l -> updateLoc(loc); getCaseList l - | Default loc :: _ -> updateLoc(loc); None - | Case (e, loc) :: l -> - updateLoc(loc); - begin match convertExp e with - | Expr (Econst_int n, _) -> - begin match getCaseList l with - | None -> None - | Some cl -> Some (n :: cl) - end - | _ -> internal_error "getCaseList: case label does not \ - reduce to an integer constant" - end - - -(** Convert a list of integers into a [CabsCoq.lblStatementList] *) -and processCaseList cl s lrem = - match cl with - | [] -> internal_error "processCaseList: syntax error in switch statement" - | [n] -> LScase (n, s, lrem) - | n1 :: l -> LScase (n1, Sskip, processCaseList l s lrem) - - -(** Convert a [Cil.stmt list] which is the body of a Switch structure - into a [CabsCoq.lblStatementList] - (Pre-condition: all the Case labels are supposed to be at the same level, - ie. no nested structures) *) -and processLblStmtList switchBody = function - | [] -> LSdefault Sskip - | [ls] -> - let s = processStmtList (keepFrom ls switchBody) in - begin match getCaseList ls.labels with - | None -> LSdefault s - | Some cl -> processCaseList cl s (LSdefault Sskip) - end - | ls :: ((ls' :: _) as l) -> - if ls.labels = ls'.labels then processLblStmtList switchBody l - else - begin match getCaseList ls.labels with - | None -> unsupported "default case is not at the end of this `switch' statement" - | Some cl -> - let s = processStmtList (keepBetween ls ls' switchBody) in - let lrem = processLblStmtList switchBody l in - processCaseList cl s lrem - end - - -(** Convert a [Cil.stmt] into a [CabsCoq.statement] *) -and convertStmt s = - match s.skind with - | Instr iList -> processInstrList iList - | Return (eOpt, loc) -> - updateLoc(loc); - let eOpt' = match eOpt with - | None -> Datatypes.None - | Some e -> Datatypes.Some (convertExp e) - in - Sreturn eOpt' - | Goto (_, loc) -> - updateLoc(loc); - unsupported "`goto' statement" - | Break loc -> - updateLoc(loc); - Sbreak - | Continue loc -> - updateLoc(loc); - Scontinue - | If (e, b1, b2, loc) -> - updateLoc(loc); - let e1 = processStmtList b1.bstmts in - let e2 = processStmtList b2.bstmts in - Sifthenelse (convertExp e, e1, e2) - | Switch (e, b, l, loc) -> - updateLoc(loc); - Sswitch (convertExp e, processLblStmtList b.bstmts l) - | While (e, b, loc) -> - updateLoc(loc); - Swhile (convertExp e, processStmtList b.bstmts) - | DoWhile (e, b, loc) -> - updateLoc(loc); - Sdowhile (convertExp e, processStmtList b.bstmts) - | For (bInit, e, bIter, b, loc) -> - updateLoc(loc); - let sInit = processStmtList bInit.bstmts in - let e' = convertExp e in - let sIter = processStmtList bIter.bstmts in - Sfor (sInit, e', sIter, processStmtList b.bstmts) - | Block b -> processStmtList b.bstmts - | TryFinally (_, _, loc) -> - updateLoc(loc); - unsupported "`try'...`finally' statement" - | TryExcept (_, _, _, loc) -> - updateLoc(loc); - unsupported "`try'...`except' statement" - -(** Convert a [Cil.GFun] into a pair [(ident * coq_fundecl)] *) -let convertGFun fdec = - current_function := Some fdec; - let v = fdec.svar in - let ret = match v.vtype with - | TFun (t, _, vArg, _) -> - if vArg then unsupported "variadic function"; - begin match convertTyp t with - | Tstruct _ | Tunion _ -> - unsupported "return value of struct or union type" - | t' -> t' - end - | _ -> internal_error "convertGFun: incorrect function type" - in - let s = processStmtList fdec.sbody.bstmts in (* function body -- do it first because of generated temps *) - let args = List.map convertVarinfoParam fdec.sformals in (* parameters*) - let varList = List.map convertVarinfo fdec.slocals in (* local vars *) - if v.vname = "main" then begin - match ret with - | Tint(_, _) -> () - | _ -> updateLoc v.vdecl; - unsupported "the return type of main() must be an integer type" - end; - current_function := None; - Datatypes.Coq_pair - (intern_string v.vname, - Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s }) - -(** Auxiliary for [convertInit] *) - -let rec initDataLen accu = function - | [] -> accu - | i1 :: il -> - let sz = match i1 with - | Init_int8 _ -> 1l - | Init_int16 _ -> 2l - | Init_int32 _ -> 4l - | Init_float32 _ -> 4l - | Init_float64 _ -> 8l - | Init_space n -> camlint_of_z n - | Init_pointer _ -> 4l in - initDataLen (Int32.add sz accu) il - -(** Convert a [Cil.init] into a list of [AST.init_data] prepended to - the given list [k]. Result is in reverse order. *) - -(* Cil.constFold does not reduce floating-point operations. - We treat here those that appear naturally in initializers. *) - -type init_constant = - | ICint of int64 * intsize - | ICfloat of float * floatsize - | ICstring of string - | ICnone - -let rec extract_constant e = - match e with - | Const (CInt64(n, ikind, _)) -> - ICint(n, fst (convertIkind ikind)) - | Const (CReal(n, fkind, _)) -> - ICfloat(n, convertFkind fkind) - | Const (CStr s) -> - ICstring s - | CastE (ty, e1) -> - begin match extract_constant e1, convertTyp ty with - | ICfloat(n, _), Tfloat sz -> - ICfloat(n, sz) - | ICint(n, _), Tfloat sz -> - ICfloat(Int64.to_float n, sz) - | ICint(n, sz), Tpointer _ -> - ICint(n, sz) - | ICstring s, (Tint _ | Tpointer _) -> - ICstring s - | _, _ -> - ICnone - end - | UnOp (Neg, e1, _) -> - begin match extract_constant e1 with - | ICfloat(n, sz) -> ICfloat(-. n, sz) - | _ -> ICnone - end - | _ -> ICnone - -let init_data_of_string s = - let id = ref [] in - let enter_char c = - let n = coqint_of_camlint(Int32.of_int(Char.code c)) in - id := Init_int8 n :: !id in - enter_char '\000'; - for i = String.length s - 1 downto 0 do enter_char s.[i] done; - !id - -let convertInit init = - let k = ref [] - and pos = ref 0 in - let emit size datum = - k := datum :: !k; - pos := !pos + size in - let emit_space size = - emit size (Init_space (z_of_camlint (Int32.of_int size))) in - let check_align size = - assert (!pos land (size - 1) = 0) in - let align size = - let n = !pos land (size - 1) in - if n > 0 then emit_space (size - n) in - - let rec cvtInit init = - match init with - | SingleInit e -> - begin match extract_constant(Cil.constFold true e) with - | ICint(n, I8) -> - let n' = coqint_of_camlint (Int64.to_int32 n) in - emit 1 (Init_int8 n') - | ICint(n, I16) -> - check_align 2; - let n' = coqint_of_camlint (Int64.to_int32 n) in - emit 2 (Init_int16 n') - | ICint(n, I32) -> - check_align 4; - let n' = coqint_of_camlint (Int64.to_int32 n) in - emit 4 (Init_int32 n') - | ICfloat(n, F32) -> - check_align 4; - emit 4 (Init_float32 n) - | ICfloat(n, F64) -> - check_align 8; - emit 8 (Init_float64 n) - | ICstring s -> - check_align 4; - emit 4 (Init_pointer(init_data_of_string s)) - | ICnone -> - unsupported "this kind of expression is not supported in global initializers" - end - | CompoundInit(ty, data) -> - let ty' = convertTyp ty in - let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in - let pos0 = !pos in - Cil.foldLeftCompoundAll - ~doinit: cvtCompoundInit - ~ct: ty - ~initl: data - ~acc: (); - let pos1 = !pos in - assert (pos1 <= pos0 + sz); - if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1) - - and cvtCompoundInit ofs init ty () = - let ty' = convertTyp ty in - let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in - align al; - cvtInit init - - in cvtInit init; CList.rev !k - -(** Convert a [Cil.initinfo] into a list of [AST.init_data] *) - -let convertInitInfo ty info = - match info.init with - | None -> - [ Init_space(Csyntax.sizeof (convertTyp ty)) ] - | Some init -> - convertInit init - -(** Convert a [Cil.GVar] into a global variable definition *) - -let convertGVar v i = - updateLoc(v.vdecl); - let id = intern_string v.vname in - Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i), - convertTyp v.vtype) - - -(** Convert a [Cil.GVarDecl] into a global variable declaration *) - -let convertExtVar v = - updateLoc(v.vdecl); - let id = intern_string v.vname in - Datatypes.Coq_pair (Datatypes.Coq_pair(id, []), - convertTyp v.vtype) - -(** Convert a [Cil.GVarDecl] into an external function declaration *) - -let convertExtFun v = - updateLoc(v.vdecl); - match convertTyp v.vtype with - | Tfunction(args, res) -> - let id = intern_string v.vname in - Datatypes.Coq_pair (id, External(id, args, res)) - | _ -> - assert false - -(** Convert a [Cil.global list] into a pair whose first component, - of type [(ident * coq_function) coqlist], represents the definitions of the - functions and the second component, of type [(ident * coq_type) coqlist], - the definitions of the global variables of the program *) -let rec processGlobals = function - | [] -> ([], []) - | g :: l -> - match g with - | GType _ -> processGlobals l (* typedefs are unrolled... *) - | GCompTag _ -> processGlobals l - | GCompTagDecl _ -> processGlobals l - | GEnumTag _ -> processGlobals l (* enum constants are folded... *) - | GEnumTagDecl _ -> processGlobals l - | GVarDecl (v, loc) -> - updateLoc(loc); - (* Functions become external declarations, - variadic and unprototyped functions are skipped, - variables become uninitialized variables *) - begin match Cil.unrollType v.vtype with - | TFun (tres, Some targs, false, _) -> - let fn = convertExtFun v in - let (fList, vList) = processGlobals l in - (fn :: fList, vList) - | TFun (tres, _, _, _) -> - processGlobals l - | _ -> - let var = convertExtVar v in - let (fList, vList) = processGlobals l in - (fList, var :: vList) - end - | GVar (v, init, loc) -> - updateLoc(loc); - let var = convertGVar v init in - let (fList, vList) = processGlobals l in - (fList, var :: vList) - | GFun (fdec, loc) -> - updateLoc(loc); - let fn = convertGFun fdec in - let (fList, vList) = processGlobals l in - (fn :: fList, vList) - | GAsm (_, loc) -> - updateLoc(loc); - unsupported "inline assembly" - | GPragma (_, loc) -> - updateLoc(loc); - warning "#pragma directive ignored"; - processGlobals l - | GText _ -> processGlobals l (* comments are ignored *) - -(** Eliminate forward declarations of globals that are defined later *) - -let cleanupGlobals globs = - let defined = - List.fold_right - (fun g def -> - match g with GVar (v, init, loc) -> v.vname :: def - | GFun (fdec, loc) -> fdec.svar.vname :: def - | _ -> def) - globs [] in - List.filter - (function GVarDecl(v, loc) -> not(List.mem v.vname defined) - | g -> true) - globs - -(** Convert a [Cil.file] into a [CabsCoq.program] *) -let convertFile f = - currentGlobalPrefix := - Filename.chop_extension (Filename.basename f.fileName); - stringNum := 0; - Hashtbl.clear stringTable; - Hashtbl.clear stub_function_table; - let (funList, defList) = processGlobals (cleanupGlobals f.globals) in - let funList' = declare_stub_functions funList in - let funList'' = match f.globinit with - | Some fdec -> convertGFun fdec :: funList' - | None -> funList' in - let defList' = globals_for_strings defList in - { AST.prog_funct = funList''; - AST.prog_vars = defList'; - AST.prog_main = intern_string "main" } - - -(*-----------------------------------------------------------------------*) -end - diff --git a/caml/Clflags.ml b/caml/Clflags.ml deleted file mode 100644 index 08e4a536..00000000 --- a/caml/Clflags.ml +++ /dev/null @@ -1,25 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Command-line flags *) - -let prepro_options = ref ([]: string list) -let linker_options = ref ([]: string list) -let exe_name = ref "a.out" -let option_flonglong = ref false -let option_fmadd = ref false -let option_dclight = ref false -let option_dasm = ref false -let option_E = ref false -let option_S = ref false -let option_c = ref false -let option_v = ref false diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml deleted file mode 100644 index f11738df..00000000 --- a/caml/Coloringaux.ml +++ /dev/null @@ -1,625 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Camlcoq -open 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 = [| - Array.of_list Conventions.int_caller_save_regs; - Array.of_list Conventions.float_caller_save_regs -|] - -let callee_save_registers = [| - Array.of_list Conventions.int_callee_save_regs; - Array.of_list Conventions.float_callee_save_regs -|] - -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 deleted file mode 100644 index c5070f20..00000000 --- a/caml/Coloringaux.mli +++ /dev/null @@ -1,20 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Registers -open Locations -open RTL -open RTLtyping -open InterfGraph - -val graph_coloring: - coq_function -> graph -> regenv -> Regset.t -> (reg -> loc) diff --git a/caml/Driver.ml b/caml/Driver.ml deleted file mode 100644 index 8fffcaa0..00000000 --- a/caml/Driver.ml +++ /dev/null @@ -1,352 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Printf -open Clflags - -(* Location of the standard library *) - -let stdlib_path = ref( - try - Sys.getenv "COMPCERT_LIBRARY" - with Not_found -> - Configuration.stdlib_path) - -let command cmd = - if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" - end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) - -let safe_remove file = - try Sys.remove file with Sys_error _ -> () - -(* Printing of error messages *) - -let print_error oc msg = - let print_one_error = function - | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s) - | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i) - in List.iter print_one_error msg - -(* For the CIL -> Csyntax translator: - - * The meaning of some type specifiers may depend on compiler options: - the size of an int or the default signedness of char, for instance. - - * Those type conversions may be parameterized thanks to a functor. - - * Remark: [None] means that the type specifier is not supported - (that is, an Unsupported exception will be raised if that type - specifier is encountered in the program). -*) - -module TypeSpecifierTranslator = struct - - open Cil - open Csyntax - - (** Convert a Cil.ikind into an (intsize * signedness) option *) - let convertIkind = function - | IChar -> Some (I8, Unsigned) - | ISChar -> Some (I8, Signed) - | IUChar -> Some (I8, Unsigned) - | IInt -> Some (I32, Signed) - | IUInt -> Some (I32, Unsigned) - | IShort -> Some (I16, Signed) - | IUShort -> Some (I16, Unsigned) - | ILong -> Some (I32, Signed) - | IULong -> Some (I32, Unsigned) - | ILongLong -> if !option_flonglong then Some (I32, Signed) else None - | IULongLong -> if !option_flonglong then Some (I32, Unsigned) else None - - (** Convert a Cil.fkind into an floatsize option *) - let convertFkind = function - | FFloat -> Some F32 - | FDouble -> Some F64 - | FLongDouble -> if !option_flonglong then Some F64 else None - -end - -module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator) - -(* From C to preprocessed C *) - -let preprocess ifile ofile = - let cmd = - sprintf "%s -D__COMPCERT__ -I%s %s %s > %s" - Configuration.prepro - !stdlib_path - (quote_options !prepro_options) - ifile ofile in - if command cmd <> 0 then begin - safe_remove ofile; - eprintf "Error during preprocessing.\n"; - exit 2 - end - -(* From preprocessed C to asm *) - -let compile_c_file sourcename ifile ofile = - (* Parsing and production of a CIL.file *) - let cil = - try - Frontc.parse ifile () - with - | Frontc.ParseError msg -> - eprintf "Error during parsing: %s\n" msg; - exit 2 - | Errormsg.Error -> - exit 2 in - (* Remove preprocessed file (always a temp file) *) - safe_remove ifile; - (* Restore original source file name *) - cil.Cil.fileName <- sourcename; - (* Cleanup in the CIL.file *) - Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil; - (* Conversion to Csyntax *) - let csyntax = - try - Cil2CsyntaxTranslator.convertFile cil - with - | Cil2CsyntaxTranslator.Unsupported msg -> - eprintf "%s\n" msg; - exit 2 - | Cil2CsyntaxTranslator.Internal_error msg -> - eprintf "%s\nPlease report it.\n" msg; - exit 2 in - (* Save Csyntax if requested *) - if !option_dclight then begin - let targetname = Filename.chop_suffix sourcename ".c" in - let oc = open_out (targetname ^ ".light.c") in - PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; - close_out oc - end; - (* Convert to PPC *) - let ppc = - match Main.transf_c_program csyntax with - | Errors.OK x -> x - | Errors.Error msg -> - print_error stderr msg; - exit 2 in - (* Save PPC asm *) - let oc = open_out ofile in - PrintPPC.print_program oc ppc; - close_out oc - -(* From Cminor to asm *) - -let compile_cminor_file ifile ofile = - let ic = open_in ifile in - let lb = Lexing.from_channel ic in - try - match Main.transf_cminor_program - (CMtypecheck.type_program - (CMparser.prog CMlexer.token lb)) with - | Errors.Error msg -> - print_error stderr msg; - exit 2 - | Errors.OK p -> - let oc = open_out ofile in - PrintPPC.print_program oc p; - close_out oc - with Parsing.Parse_error -> - eprintf "File %s, character %d: Syntax error\n" - ifile (Lexing.lexeme_start lb); - exit 2 - | CMlexer.Error msg -> - eprintf "File %s, character %d: %s\n" - ifile (Lexing.lexeme_start lb) msg; - exit 2 - | CMtypecheck.Error msg -> - eprintf "File %s, type-checking error:\n%s" - ifile msg; - exit 2 - -(* From asm to object file *) - -let assemble ifile ofile = - let cmd = - sprintf "%s -o %s %s" - Configuration.asm ofile ifile in - let retcode = command cmd in - if not !option_dasm then safe_remove ifile; - if retcode <> 0 then begin - safe_remove ofile; - eprintf "Error during assembling.\n"; - exit 2 - end - -(* Linking *) - -let linker exe_name files = - let cmd = - sprintf "%s -o %s %s -L%s -lcompcert" - Configuration.linker - (Filename.quote exe_name) - (quote_options files) - !stdlib_path in - if command cmd <> 0 then exit 2 - -(* Processing of a .c file *) - -let process_c_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".c" in - if !option_E then begin - preprocess sourcename (prefixname ^ ".i") - end else begin - let preproname = Filename.temp_file "compcert" ".i" in - preprocess sourcename preproname; - if !option_S then begin - compile_c_file sourcename preproname (prefixname ^ ".s") - end else begin - let asmname = - if !option_dasm - then prefixname ^ ".s" - else Filename.temp_file "compcert" ".s" in - compile_c_file sourcename preproname asmname; - assemble asmname (prefixname ^ ".o") - end - end; - prefixname ^ ".o" - -(* Processing of a .cm file *) - -let process_cminor_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".cm" in - if !option_S then begin - compile_cminor_file sourcename (prefixname ^ ".s") - end else begin - let asmname = - if !option_dasm - then prefixname ^ ".s" - else Filename.temp_file "compcert" ".s" in - compile_cminor_file sourcename asmname; - assemble asmname (prefixname ^ ".o") - end; - prefixname ^ ".o" - -(* Command-line parsing *) - -let starts_with s1 s2 = - String.length s1 >= String.length s2 && - String.sub s1 0 (String.length s2) = s2 - -let usage_string = -"ccomp [options] -Recognized source files: - .c C source file - .cm Cminor source file - .o Object file - .a Library file -Processing options: - -E Preprocess only, save result in .i - -S Compile to assembler only, save result in .s - -c Compile to object file only (no linking), result in .o -Preprocessing options: - -I Add to search path for #include files - -D= Define preprocessor symbol - -U Undefine preprocessor symbol -Compilation options: - -flonglong Treat 'long long' as 'long' and 'long double' as 'double' - -fmadd Use fused multiply-add and multiply-sub instructions - -dclight Save generated Clight in .light.c - -dasm Save generated assembly in .s -Linking options: - -l Link library - -L Add to search path for libraries - -o Generate executable in (default: a.out) -General options: - -stdlib Set the path of the Compcert run-time library - -v Print external commands before invoking them -" - -let rec parse_cmdline i = - if i < Array.length Sys.argv then begin - let s = Sys.argv.(i) in - if starts_with s "-I" || starts_with s "-D" || starts_with s "-U" - then begin - prepro_options := s :: !prepro_options; - parse_cmdline (i + 1) - end else - if starts_with s "-l" || starts_with s "-L" then begin - linker_options := s :: !linker_options; - parse_cmdline (i + 1) - end else - if s = "-o" && i + 1 < Array.length Sys.argv then begin - exe_name := Sys.argv.(i + 1); - parse_cmdline (i + 2) - end else - if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin - stdlib_path := Sys.argv.(i + 1); - parse_cmdline (i + 2) - end else - if s = "-flonglong" then begin - option_flonglong := true; - parse_cmdline (i + 1) - end else - if s = "-fmadd" then begin - option_fmadd := true; - parse_cmdline (i + 1) - end else - if s = "-dclight" then begin - option_dclight := true; - parse_cmdline (i + 1) - end else - if s = "-dasm" then begin - option_dasm := true; - parse_cmdline (i + 1) - end else - if s = "-E" then begin - option_E := true; - parse_cmdline (i + 1) - end else - if s = "-S" then begin - option_S := true; - parse_cmdline (i + 1) - end else - if s = "-c" then begin - option_c := true; - parse_cmdline (i + 1) - end else - if s = "-v" then begin - option_v := true; - parse_cmdline (i + 1) - end else - if Filename.check_suffix s ".c" then begin - let objfile = process_c_file s in - linker_options := objfile :: !linker_options; - parse_cmdline (i + 1) - end else - if Filename.check_suffix s ".cm" then begin - let objfile = process_cminor_file s in - linker_options := objfile :: !linker_options; - parse_cmdline (i + 1) - end else - if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin - linker_options := s :: !linker_options; - parse_cmdline (i + 1) - end else begin - eprintf "Unknown argument `%s'\n" s; - eprintf "Usage: %s" usage_string; - exit 2 - end - end - -let _ = - parse_cmdline 1; - if not (!option_c || !option_S || !option_E) then begin - linker !exe_name !linker_options - end diff --git a/caml/Floataux.ml b/caml/Floataux.ml deleted file mode 100644 index 6b3b825f..00000000 --- a/caml/Floataux.ml +++ /dev/null @@ -1,39 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Camlcoq -open Integers - -let singleoffloat f = - Int32.float_of_bits (Int32.bits_of_float f) - -let intoffloat f = - coqint_of_camlint (Int32.of_float f) - -let intuoffloat f = - coqint_of_camlint (Int64.to_int32 (Int64.of_float f)) - -let floatofint i = - Int32.to_float (camlint_of_coqint i) - -let floatofintu i = - Int64.to_float (Int64.logand (Int64.of_int32 (camlint_of_coqint i)) - 0xFFFFFFFFL) - -let cmp c (x: float) (y: float) = - match c with - | Ceq -> x = y - | Cne -> x <> y - | Clt -> x < y - | Cle -> x <= y - | Cgt -> x > y - | Cge -> x >= y diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml deleted file mode 100644 index 2f2333fb..00000000 --- a/caml/Linearizeaux.ml +++ /dev/null @@ -1,85 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open BinPos -open Coqlib -open Datatypes -open LTL -open Lattice -open CList -open Maps -open Camlcoq - -(* Trivial enumeration, in decreasing order of PC *) - -(*** -let enumerate_aux f reach = - positive_rec - Coq_nil - (fun pc nodes -> - if PMap.get pc reach - then Coq_cons (pc, nodes) - else nodes) - f.fn_nextpc -***) - -(* More clever enumeration that flattens basic blocks *) - -let rec int_of_pos = function - | Coq_xI p -> (int_of_pos p lsl 1) + 1 - | Coq_xO p -> int_of_pos p lsl 1 - | Coq_xH -> 1 - -let rec pos_of_int n = - if n = 0 then assert false else - if n = 1 then Coq_xH else - if n land 1 = 0 - then Coq_xO (pos_of_int (n lsr 1)) - else Coq_xI (pos_of_int (n lsr 1)) - -(* Build the enumeration *) - -module IntSet = Set.Make(struct type t = int let compare = compare end) - -let enumerate_aux f reach = - let enum = ref [] in - let emitted = Array.make (int_of_pos f.fn_nextpc) false in - let rec emit_block pending pc = - let npc = int_of_pos pc in - if emitted.(npc) - then emit_restart pending - else begin - enum := pc :: !enum; - emitted.(npc) <- true; - match PTree.get pc f.fn_code with - | None -> assert false - | Some i -> - match i with - | Lnop s -> emit_block pending s - | Lop (op, args, res, s) -> emit_block pending s - | Lload (chunk, addr, args, dst, s) -> emit_block pending s - | Lstore (chunk, addr, args, src, s) -> emit_block pending s - | Lcall (sig0, ros, args, res, s) -> emit_block pending s - | Ltailcall (sig0, ros, args) -> emit_restart pending - | Lalloc (arg, res, s) -> emit_block pending s - | Lcond (cond, args, ifso, ifnot) -> - emit_restart (IntSet.add (int_of_pos ifso) - (IntSet.add (int_of_pos ifnot) pending)) - | Lreturn optarg -> emit_restart pending - end - and emit_restart pending = - if not (IntSet.is_empty pending) then begin - let npc = IntSet.max_elt pending in - emit_block (IntSet.remove npc pending) (pos_of_int npc) - end in - emit_block IntSet.empty f.fn_entrypoint; - CList.rev !enum diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml deleted file mode 100644 index bb25339a..00000000 --- a/caml/PrintCsyntax.ml +++ /dev/null @@ -1,501 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Pretty-printer for Csyntax *) - -open Format -open Camlcoq -open CList -open Datatypes -open AST -open Csyntax - -let name_unop = function - | Onotbool -> "!" - | Onotint -> "~" - | Oneg -> "-" - - -let name_binop = function - | Oadd -> "+" - | Osub -> "-" - | Omul -> "*" - | Odiv -> "/" - | Omod -> "%" - | Oand -> "&" - | Oor -> "|" - | Oxor -> "^" - | Oshl -> "<<" - | Oshr -> ">>" - | Oeq -> "==" - | One -> "!=" - | Olt -> "<" - | Ogt -> ">" - | Ole -> "<=" - | Oge -> ">=" - -let name_inttype sz sg = - match sz, sg with - | I8, Signed -> "signed char" - | I8, Unsigned -> "unsigned char" - | I16, Signed -> "short" - | I16, Unsigned -> "unsigned short" - | I32, Signed -> "int" - | I32, Unsigned -> "unsigned int" - -let name_floattype sz = - match sz with - | F32 -> "float" - | F64 -> "double" - -(* Collecting the names and fields of structs and unions *) - -module StructUnionSet = Set.Make(struct - type t = string * fieldlist - let compare (n1, _ : t) (n2, _ : t) = compare n1 n2 -end) - -let struct_unions = ref StructUnionSet.empty - -let register_struct_union id fld = - struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions - -(* Declarator (identifier + type) *) - -let name_optid id = - if id = "" then "" else " " ^ id - -let parenthesize_if_pointer id = - if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id - -let rec name_cdecl id ty = - match ty with - | Tvoid -> - "void" ^ name_optid id - | Tint(sz, sg) -> - name_inttype sz sg ^ name_optid id - | Tfloat sz -> - name_floattype sz ^ name_optid id - | Tpointer t -> - name_cdecl ("*" ^ id) t - | Tarray(t, n) -> - name_cdecl - (sprintf "%s[%ld]" (parenthesize_if_pointer id) (camlint_of_coqint n)) - t - | Tfunction(args, res) -> - let b = Buffer.create 20 in - if id = "" - then Buffer.add_string b "(*)" - else Buffer.add_string b (parenthesize_if_pointer id); - Buffer.add_char b '('; - begin match args with - | Tnil -> - Buffer.add_string b "void" - | _ -> - let rec add_args first = function - | Tnil -> () - | Tcons(t1, tl) -> - if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl "" t1); - add_args false tl in - add_args true args - end; - Buffer.add_char b ')'; - name_cdecl (Buffer.contents b) res - | Tstruct(name, fld) -> - extern_atom name ^ name_optid id - | Tunion(name, fld) -> - extern_atom name ^ name_optid id - | Tcomp_ptr name -> - extern_atom name ^ " *" ^ id - -(* Type *) - -let name_type ty = name_cdecl "" ty - -(* Expressions *) - -let parenthesis_level (Expr (e, ty)) = - match e with - | Econst_int _ -> 0 - | Econst_float _ -> 0 - | Evar _ -> 0 - | Eunop(_, _) -> 30 - | Ederef _ -> 20 - | Eaddrof _ -> 30 - | Ebinop(op, _, _) -> - begin match op with - | Oand | Oor | Oxor -> 75 - | Oeq | One | Olt | Ogt | Ole | Oge -> 70 - | Oadd | Osub | Oshl | Oshr -> 60 - | Omul | Odiv | Omod -> 40 - end - | Ecast _ -> 30 - | Econdition(_, _, _) -> 80 - | Eandbool(_, _) -> 80 - | Eorbool(_, _) -> 80 - | Esizeof _ -> 20 - | Efield _ -> 20 - -let rec print_expr p (Expr (eb, ty) as e) = - let level = parenthesis_level e in - match eb with - | Econst_int n -> - fprintf p "%ld" (camlint_of_coqint n) - | Econst_float f -> - fprintf p "%F" f - | Evar id -> - fprintf p "%s" (extern_atom id) - | Eunop(op, e1) -> - fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1) - | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) -> - fprintf p "@[%a@,[%a]@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - | Ederef (Expr (Efield(e1, id), _)) -> - fprintf p "%a->%s" print_expr_prec (level, e1) (extern_atom id) - | Ederef e -> - fprintf p "*%a" print_expr_prec (level, e) - | Eaddrof e -> - fprintf p "&%a" print_expr_prec (level, e) - | Ebinop(op, e1, e2) -> - fprintf p "@[%a@ %s %a@]" - print_expr_prec (level, e1) - (name_binop op) - print_expr_prec (level, e2) - | Ecast(ty, e1) -> - fprintf p "@[(%s)@,%a@]" - (name_type ty) - print_expr_prec (level, e1) - | Econdition(e1, e2, e3) -> - fprintf p "@[%a@ ? %a@ : %a@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - print_expr_prec (level, e3) - | Eandbool(e1, e2) -> - fprintf p "@[%a@ && %a@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - | Eorbool(e1, e2) -> - fprintf p "@[%a@ || %a@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - | Esizeof ty -> - fprintf p "sizeof(%s)" (name_type ty) - | Efield(e1, id) -> - fprintf p "%a.%s" print_expr_prec (level, e1) (extern_atom id) - -and print_expr_prec p (context_prec, e) = - let this_prec = parenthesis_level e in - if this_prec >= context_prec - then fprintf p "(%a)" print_expr e - else print_expr p e - -let rec print_expr_list p (first, el) = - match el with - | [] -> () - | e1 :: et -> - if not first then fprintf p ",@ "; - print_expr p e1; - print_expr_list p (false, et) - -let rec print_stmt p s = - match s with - | Sskip -> - fprintf p "/*skip*/;" - | Sassign(e1, e2) -> - fprintf p "@[%a =@ %a;@]" print_expr e1 print_expr e2 - | Scall(None, e1, el) -> - fprintf p "@[%a@,(@[%a@]);@]" - print_expr e1 - print_expr_list (true, el) - | Scall(Some lhs, e1, el) -> - fprintf p "@[%a =@ %a@,(@[%a@]);@]" - print_expr lhs - print_expr e1 - print_expr_list (true, el) - | Ssequence(s1, s2) -> - fprintf p "%a@ %a" print_stmt s1 print_stmt s2 - | Sifthenelse(e, s1, Sskip) -> - fprintf p "@[if (%a) {@ %a@;<0 -2>}@]" - print_expr e - print_stmt s1 - | Sifthenelse(e, s1, s2) -> - fprintf p "@[if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" - print_expr e - print_stmt s1 - print_stmt s2 - | Swhile(e, s) -> - fprintf p "@[while (%a) {@ %a@;<0 -2>}@]" - print_expr e - print_stmt s - | Sdowhile(e, s) -> - fprintf p "@[do {@ %a@;<0 -2>} while(%a);@]" - print_stmt s - print_expr e - | Sfor(s_init, e, s_iter, s_body) -> - fprintf p "@[for (@[%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" - print_stmt_for s_init - print_expr e - print_stmt_for s_iter - print_stmt s_body - | Sbreak -> - fprintf p "break;" - | Scontinue -> - fprintf p "continue;" - | Sswitch(e, cases) -> - fprintf p "@[switch (%a) {@ %a@;<0 -2>}@]" - print_expr e - print_cases cases - | Sreturn None -> - fprintf p "return;" - | Sreturn (Some e) -> - fprintf p "return %a;" print_expr e - -and print_cases p cases = - match cases with - | LSdefault Sskip -> - () - | LSdefault s -> - fprintf p "@[default:@ %a@]" print_stmt s - | LScase(lbl, Sskip, rem) -> - fprintf p "case %ld:@ %a" - (camlint_of_coqint lbl) - print_cases rem - | LScase(lbl, s, rem) -> - fprintf p "@[case %ld:@ %a@]@ %a" - (camlint_of_coqint lbl) - print_stmt s - print_cases rem - -and print_stmt_for p s = - match s with - | Sskip -> - fprintf p "/*nothing*/" - | Sassign(e1, e2) -> - fprintf p "%a = %a" print_expr e1 print_expr e2 - | Ssequence(s1, s2) -> - fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2 - | Scall(None, e1, el) -> - fprintf p "@[%a@,(@[%a@])@]" - print_expr e1 - print_expr_list (true, el) - | Scall(Some lhs, e1, el) -> - fprintf p "@[%a =@ %a@,(@[%a@])@]" - print_expr lhs - print_expr e1 - print_expr_list (true, el) - | _ -> - fprintf p "({ %a })" print_stmt s - -let name_function_parameters fun_name params = - let b = Buffer.create 20 in - Buffer.add_string b fun_name; - Buffer.add_char b '('; - begin match params with - | [] -> - Buffer.add_string b "void" - | _ -> - let rec add_params first = function - | [] -> () - | Coq_pair(id, ty) :: rem -> - if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl (extern_atom id) ty); - add_params false rem in - add_params true params - end; - Buffer.add_char b ')'; - Buffer.contents b - -let print_function p id f = - fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params) - f.fn_return); - fprintf p "@[{@ "; - List.iter - (fun (Coq_pair(id, ty)) -> - fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) - f.fn_vars; - print_stmt p f.fn_body; - fprintf p "@;<0 -2>}@]@ @ " - -let print_fundef p (Coq_pair(id, fd)) = - match fd with - | External(_, args, res) -> - fprintf p "extern %s;@ @ " - (name_cdecl (extern_atom id) (Tfunction(args, res))) - | Internal f -> - print_function p id f - -let string_of_init id = - try - let s = String.create (List.length id) in - let i = ref 0 in - List.iter - (function - | Init_int8 n -> - s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n)); - incr i - | _ -> raise Not_found) - id; - Some s - with Not_found -> None - -let print_escaped_string p s = - fprintf p "\""; - for i = 0 to String.length s - 1 do - match s.[i] with - | ('\"' | '\\') as c -> fprintf p "\\%c" c - | '\n' -> fprintf p "\\n" - | '\t' -> fprintf p "\\t" - | '\r' -> fprintf p "\\r" - | c -> if c >= ' ' && c <= '~' - then fprintf p "%c" c - else fprintf p "\\x%02x" (Char.code c) - done; - fprintf p "\"" - -let print_init p = function - | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) - | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) - | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n) - | Init_float32 n -> fprintf p "%F,@ " n - | Init_float64 n -> fprintf p "%F,@ " n - | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n) - | Init_pointer id -> - match string_of_init id with - | None -> fprintf p "/* pointer to other init*/,@ " - | Some s -> fprintf p "%a,@ " print_escaped_string s - -let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = - match init with - | [] -> - fprintf p "extern %s;@ @ " - (name_cdecl (extern_atom id) ty) - | [Init_space _] -> - fprintf p "%s;@ @ " - (name_cdecl (extern_atom id) ty) - | _ -> - fprintf p "@[%s = {@ " - (name_cdecl (extern_atom id) ty); - List.iter (print_init p) init; - fprintf p "};@]@ @ " - -(* Collect struct and union types *) - -let rec collect_type = function - | Tvoid -> () - | Tint(sz, sg) -> () - | Tfloat sz -> () - | Tpointer t -> collect_type t - | Tarray(t, n) -> collect_type t - | Tfunction(args, res) -> collect_type_list args; collect_type res - | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld - | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld - | Tcomp_ptr _ -> () - -and collect_type_list = function - | Tnil -> () - | Tcons(hd, tl) -> collect_type hd; collect_type_list tl - -and collect_fields = function - | Fnil -> () - | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl - -let rec collect_expr (Expr(ed, ty)) = - match ed with - | Econst_int n -> () - | Econst_float f -> () - | Evar id -> () - | Eunop(op, e1) -> collect_expr e1 - | Ederef e -> collect_expr e - | Eaddrof e -> collect_expr e - | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2 - | Ecast(ty, e1) -> collect_type ty; collect_expr e1 - | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3 - | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2 - | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2 - | Esizeof ty -> collect_type ty - | Efield(e1, id) -> collect_expr e1 - -let rec collect_expr_list = function - | [] -> () - | hd :: tl -> collect_expr hd; collect_expr_list tl - -let rec collect_stmt = function - | Sskip -> () - | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el - | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Swhile(e, s) -> collect_expr e; collect_stmt s - | Sdowhile(e, s) -> collect_stmt s; collect_expr e - | Sfor(s_init, e, s_iter, s_body) -> - collect_stmt s_init; collect_expr e; - collect_stmt s_iter; collect_stmt s_body - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - -and collect_cases = function - | LSdefault s -> collect_stmt s - | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars; - collect_stmt f.fn_body - -let collect_fundef (Coq_pair(id, fd)) = - match fd with - | External(_, args, res) -> collect_type_list args; collect_type res - | Internal f -> collect_function f - -let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) = - collect_type ty - -let collect_program p = - List.iter collect_globvar p.prog_vars; - List.iter collect_fundef p.prog_funct - -let declare_struct_or_union p (name, fld) = - fprintf p "%s;@ @ " name - -let print_struct_or_union p (name, fld) = - fprintf p "@[%s {" name; - let rec print_fields = function - | Fnil -> () - | Fcons(id, ty, rem) -> - fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); - print_fields rem in - print_fields fld; - fprintf p "@;<0 -2>};@]@ " - -let print_program p prog = - struct_unions := StructUnionSet.empty; - collect_program prog; - fprintf p "@["; - StructUnionSet.iter (declare_struct_or_union p) !struct_unions; - StructUnionSet.iter (print_struct_or_union p) !struct_unions; - List.iter (print_globvar p) prog.prog_vars; - List.iter (print_fundef p) prog.prog_funct; - fprintf p "@]@." - - diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml deleted file mode 100644 index 94c3a7b3..00000000 --- a/caml/PrintPPC.ml +++ /dev/null @@ -1,532 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing PPC assembly code in asm syntax *) - -open Printf -open Datatypes -open CList -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' - -(* Record identifiers of external functions *) - -module IdentSet = Set.Make(struct type t = ident let compare = compare end) - -let extfuns = ref IdentSet.empty - -let record_extfun (Coq_pair(name, defn)) = - match defn with - | Internal _ -> () - | External _ -> extfuns := IdentSet.add name !extfuns - -(* Basic printing functions *) - -let print_symb oc symb = - if IdentSet.mem symb !extfuns - then fprintf oc "L%s$stub" (extern_atom symb) - else 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(s, n) -> - fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n) - | Csymbol_high(s, n) -> - fprintf oc "ha16(%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 - | Pallocblock -> - fprintf oc " bl _compcert_alloc\n" - | Pallocframe(lo, hi, ofs) -> - let lo = camlint_of_coqint lo - and hi = camlint_of_coqint hi - and ofs = camlint_of_coqint ofs in - let sz = Int32.sub hi lo in - (* Keep stack 16-aligned *) - let sz16 = Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l in - assert (ofs = 0l); - fprintf oc " stwu r1, %ld(r1)\n" (Int32.neg sz16) - | 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 - | Pbs s -> - fprintf oc " b %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 ofs -> - fprintf oc " lwz r1, %ld(r1)\n" (camlint_of_coqint ofs) - | 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 " stfd f13, -8(r1)\n"; - fprintf oc " lwz %a, -4(r1)\n" ireg r1 - | Pfctiu(r1, r2) -> - let lbl1 = new_label() in - let lbl2 = new_label() in - let lbl3 = new_label() in - fprintf oc " addis r12, 0, ha16(L%d)\n" lbl1; - fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl1; - fprintf oc " fcmpu cr7, %a, f13\n" freg r2; - fprintf oc " cror 30, 29, 30\n"; - fprintf oc " beq cr7, L%d\n" lbl2; - 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 " b L%d\n" lbl3; - fprintf oc "L%d: fsub f13, %a, f13\n" lbl2 freg r2; - fprintf oc " fctiwz f13, f13\n"; - fprintf oc " stfdu f13, -8(r1)\n"; - fprintf oc " lwz %a, 4(r1)\n" ireg r1; - fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1; - fprintf oc "L%d: addi r1, r1, 8\n" lbl3; - fprintf oc " .const_data\n"; - fprintf oc "L%d: .long 0x41e00000, 0x00000000\n" lbl1; - fprintf oc " .text\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 r12, 0, 0x4330\n"; - fprintf oc " stw r12, -8(r1)\n"; - fprintf oc " addis r12, %a, 0x8000\n" ireg r2; - fprintf oc " stw r12, -4(r1)\n"; - fprintf oc " addis r12, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl; - fprintf oc " lfd %a, -8(r1)\n" freg r1; - 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 r12, 0, 0x4330\n"; - fprintf oc " stw r12, -8(r1)\n"; - fprintf oc " stw %a, -4(r1)\n" ireg r2; - fprintf oc " addis r12, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl; - fprintf oc " lfd %a, -8(r1)\n" freg r1; - fprintf oc " fsub %a, %a, f13\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 r12, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd %a, lo16(L%d)(r12)\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 - -let rec labels_of_code = function - | [] -> Labelset.empty - | (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c -> - Labelset.add lbl (labels_of_code c) - | _ :: c -> labels_of_code c - -let print_function oc 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; - List.iter (print_instruction oc (labels_of_code code)) code - -(* Generation of stub code for variadic functions, e.g. printf. - Calling conventions for variadic functions are: - - always reserve 8 stack words (offsets 24 to 52) so that the - variadic function can save there the integer registers parameters - r3 ... r10 - - treat float arguments as pairs of integers, i.e. if we - must pass them in registers, use a pair of integer registers - for this purpose. - The code we generate is: - - allocate large enough stack frame - - save return address - - copy our arguments (registers and stack) to the stack frame, - starting at offset 24 - - load relevant integer parameter registers r3...r10 from the - stack frame, limited by the actual number of arguments - - call the variadic thing - - deallocate stack frame and return -*) - -let variadic_stub oc stub_name fun_name ty_args = - (* Compute total size of arguments *) - let arg_size = - CList.fold_left - (fun sz ty -> match ty with Tint -> sz + 4 | Tfloat -> sz + 8) - ty_args 0 in - (* Stack size is linkage area + argument size, with a minimum of 56 bytes *) - let frame_size = max 56 (24 + arg_size) in - fprintf oc " mflr r0\n"; - fprintf oc " stwu r1, %d(r1)\n" (-frame_size); - fprintf oc " stw r0, %d(r1)\n" (frame_size + 4); - (* Copy our parameters to our stack frame. - As an optimization, don't copy parameters that are already in - integer registers, since these stay in place. *) - let rec copy gpr fpr src_ofs dst_ofs = function - | [] -> () - | Tint :: rem -> - if gpr > 10 then begin - fprintf oc " lwz r0, %d(r1)\n" src_ofs; - fprintf oc " stw r0, %d(r1)\n" dst_ofs - end; - copy (gpr + 1) fpr (src_ofs + 4) (dst_ofs + 4) rem - | Tfloat :: rem -> - if fpr <= 10 then begin - fprintf oc " stfd f%d, %d(r1)\n" fpr dst_ofs - end else begin - fprintf oc " lfd f0, %d(r1)\n" src_ofs; - fprintf oc " stfd f0, %d(r1)\n" dst_ofs - end; - copy (gpr + 2) (fpr + 1) (src_ofs + 8) (dst_ofs + 8) rem - in copy 3 1 (frame_size + 24) 24 ty_args; - (* Load the first parameters into integer registers. - As an optimization, don't load parameters that are already - in the correct integer registers. *) - let rec load gpr ofs = function - | [] -> () - | Tint :: rem -> - load (gpr + 1) (ofs + 4) rem - | Tfloat :: rem -> - if gpr <= 10 then - fprintf oc " lwz r%d, %d(r1)\n" gpr ofs; - if gpr + 1 <= 10 then - fprintf oc " lwz r%d, %d(r1)\n" (gpr + 1) (ofs + 4); - load (gpr + 2) (ofs + 8) rem - in load 3 24 ty_args; - (* Call the function *) - fprintf oc " addis r11, 0, ha16(L%s$ptr)\n" stub_name; - fprintf oc " lwz r11, lo16(L%s$ptr)(r11)\n" stub_name; - fprintf oc " mtctr r11\n"; - fprintf oc " bctrl\n"; - (* Free our frame and return *) - fprintf oc " lwz r0, %d(r1)\n" (frame_size + 4); - fprintf oc " mtlr r0\n"; - fprintf oc " addi r1, r1, %d\n" frame_size; - fprintf oc " blr\n"; - (* The function pointer *) - fprintf oc " .non_lazy_symbol_pointer\n"; - fprintf oc "L%s$ptr:\n" stub_name; - fprintf oc " .indirect_symbol _%s\n" fun_name; - fprintf oc " .long 0\n" - -(* Stubs for fixed-type functions are much simpler *) - -let non_variadic_stub oc name = - fprintf oc " addis r11, 0, ha16(L%s$ptr)\n" name; - fprintf oc " lwz r11, lo16(L%s$ptr)(r11)\n" name; - fprintf oc " mtctr r11\n"; - fprintf oc " bctr\n"; - fprintf oc " .non_lazy_symbol_pointer\n"; - fprintf oc "L%s$ptr:\n" name; - fprintf oc " .indirect_symbol _%s\n" name; - fprintf oc " .long 0\n" - -let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$" - -let print_external_function oc name ef = - let name = extern_atom name in - fprintf oc " .text\n"; - fprintf oc " .align 2\n"; - fprintf oc "L%s$stub:\n" name; - if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args - else non_variadic_stub oc name - -let print_fundef oc (Coq_pair(name, defn)) = - match defn with - | Internal code -> print_function oc name code - | External ef -> print_external_function oc name ef - -let init_data_queue = ref [] - -let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_float32 n -> - fprintf oc " .long %ld ; %g \n" (Int32.bits_of_float n) n - | Init_float64 n -> - (* .quad not working on all versions of the MacOSX assembler *) - let b = Int64.bits_of_float n in - fprintf oc " .long %Ld, %Ld ; %g \n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - n - | Init_space n -> - let n = camlint_of_z n in - if n > 0l then fprintf oc " .space %ld\n" n - | Init_pointer id -> - let lbl = new_label() in - fprintf oc " .long L%d\n" lbl; - init_data_queue := (lbl, id) :: !init_data_queue - -let print_init_data oc id = - init_data_queue := []; - List.iter (print_init oc) id; - let rec print_remainder () = - match !init_data_queue with - | [] -> () - | (lbl, id) :: rem -> - init_data_queue := rem; - fprintf oc "L%d:\n" lbl; - List.iter (print_init oc) id; - print_remainder() - in print_remainder() - -let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = - match init_data with - | [] -> () - | _ -> - fprintf oc " .data\n"; - fprintf oc " .align 3\n"; - fprintf oc " .globl %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; - print_init_data oc init_data - -let print_program oc p = - extfuns := IdentSet.empty; - List.iter record_extfun p.prog_funct; - List.iter (print_var oc) p.prog_vars; - List.iter (print_fundef oc) p.prog_funct - diff --git a/caml/PrintPPC.mli b/caml/PrintPPC.mli deleted file mode 100644 index 2ebbb955..00000000 --- a/caml/PrintPPC.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val print_program: out_channel -> PPC.program -> unit diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml deleted file mode 100644 index 4c1fc05c..00000000 --- a/caml/RTLgenaux.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Camlcoq -open Switch -open CminorSel - -let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false - -module IntOrd = - struct - type t = Integers.int - let compare x y = - if Integers.Int.eq x y then 0 else - if Integers.Int.ltu x y then -1 else 1 - end - -module IntSet = Set.Make(IntOrd) - -let normalize_table tbl = - let rec norm seen = function - | [] -> [] - | Datatypes.Coq_pair(key, act) :: rem -> - if IntSet.mem key seen - then norm seen rem - else (key, act) :: norm (IntSet.add key seen) rem - in norm IntSet.empty tbl - -let compile_switch default table = - let sw = Array.of_list (normalize_table table) in - Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw; - let rec build lo hi minval maxval = - match hi - lo with - | 0 -> - CTaction default - | 1 -> - let (key, act) = sw.(lo) in - if Integers.Int.sub maxval minval = Integers.Int.zero - then CTaction act - else CTifeq(key, act, CTaction default) - | 2 -> - let (key1, act1) = sw.(lo) - and (key2, act2) = sw.(lo+1) in - CTifeq(key1, act1, - if Integers.Int.sub maxval minval = Integers.Int.one - then CTaction act2 - else CTifeq(key2, act2, CTaction default)) - | 3 -> - let (key1, act1) = sw.(lo) - and (key2, act2) = sw.(lo+1) - and (key3, act3) = sw.(lo+2) in - CTifeq(key1, act1, - CTifeq(key2, act2, - if Integers.Int.sub maxval minval = coqint_of_camlint 2l - then CTaction act3 - else CTifeq(key3, act3, CTaction default))) - | _ -> - let mid = (lo + hi) / 2 in - let (pivot, _) = sw.(mid) in - CTiflt(pivot, - build lo mid minval (Integers.Int.sub pivot Integers.Int.one), - build mid hi pivot maxval) - in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml deleted file mode 100644 index ff704ebe..00000000 --- a/caml/RTLtypingaux.ml +++ /dev/null @@ -1,156 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Type inference for RTL *) - -open Datatypes -open CList -open Camlcoq -open Maps -open AST -open Op -open Registers -open RTL - -exception Type_error of string - -let env = ref (PTree.empty : typ PTree.t) - -let set_type r ty = - match PTree.get r !env with - | None -> env := PTree.set r ty !env - | Some ty' -> if ty <> ty' then raise (Type_error "type mismatch") - -let rec set_types rl tyl = - match rl, tyl with - | [], [] -> () - | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys - | _, _ -> raise (Type_error "arity mismatch") - -(* First pass: process constraints of the form typeof(r) = ty *) - -let type_instr retty (Coq_pair(pc, i)) = - match i with - | Inop(_) -> - () - | Iop(Omove, _, _, _) -> - () - | Iop(op, args, res, _) -> - let (Coq_pair(targs, tres)) = type_of_operation op in - set_types args targs; set_type res tres - | Iload(chunk, addr, args, dst, _) -> - set_types args (type_of_addressing addr); - set_type dst (type_of_chunk chunk) - | Istore(chunk, addr, args, src, _) -> - set_types args (type_of_addressing addr); - set_type src (type_of_chunk chunk) - | Icall(sg, ros, args, res, _) -> - begin try - begin match ros with - | Coq_inl r -> set_type r Tint - | Coq_inr _ -> () - end; - set_types args sg.sig_args; - set_type res (match sg.sig_res with None -> Tint | Some ty -> ty) - with Type_error msg -> - let name = - match ros with - | Coq_inl _ -> "" - | Coq_inr id -> extern_atom id in - raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s" - name msg)) - end - | Itailcall(sg, ros, args) -> - begin try - begin match ros with - | Coq_inl r -> set_type r Tint - | Coq_inr _ -> () - end; - set_types args sg.sig_args; - if sg.sig_res <> retty then - raise (Type_error "mismatch on return type") - with Type_error msg -> - let name = - match ros with - | Coq_inl _ -> "" - | Coq_inr id -> extern_atom id in - raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" - name msg)) - end - | Ialloc(arg, res, _) -> - set_type arg Tint; set_type res Tint - | Icond(cond, args, _, _) -> - set_types args (type_of_condition cond) - | Ireturn(optres) -> - begin match optres, retty with - | None, None -> () - | Some r, Some ty -> set_type r ty - | _, _ -> raise (Type_error "type mismatch in Ireturn") - end - -let type_pass1 retty instrs = - List.iter (type_instr retty) instrs - -(* Second pass: extract move constraints typeof(r1) = typeof(r2) - and solve them iteratively *) - -let rec extract_moves = function - | [] -> [] - | Coq_pair(pc, i) :: rem -> - match i with - | Iop(Omove, [r1], r2, _) -> - (r1, r2) :: extract_moves rem - | Iop(Omove, _, _, _) -> - raise (Type_error "wrong Omove") - | _ -> - extract_moves rem - -let changed = ref false - -let rec solve_moves = function - | [] -> [] - | (r1, r2) :: rem -> - match (PTree.get r1 !env, PTree.get r2 !env) with - | Some ty1, Some ty2 -> - if ty1 = ty2 - then (changed := true; solve_moves rem) - else raise (Type_error "type mismatch in Omove") - | Some ty1, None -> - env := PTree.set r2 ty1 !env; changed := true; solve_moves rem - | None, Some ty2 -> - env := PTree.set r1 ty2 !env; changed := true; solve_moves rem - | None, None -> - (r1, r2) :: solve_moves rem - -let rec iter_solve_moves mvs = - changed := false; - let mvs' = solve_moves mvs in - if !changed then iter_solve_moves mvs' - -let type_pass2 instrs = - iter_solve_moves (extract_moves instrs) - -let typeof e r = - match PTree.get r e with Some ty -> ty | None -> Tint - -let infer_type_environment f instrs = - try - env := PTree.empty; - set_types f.fn_params f.fn_sig.sig_args; - type_pass1 f.fn_sig.sig_res instrs; - type_pass2 instrs; - let e = !env in - env := PTree.empty; - Some(typeof e) - with Type_error msg -> - Printf.eprintf "Error during RTL type inference: %s\n" msg; - None -- cgit