aboutsummaryrefslogtreecommitdiffstats
path: root/caml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-12-30 14:48:33 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-12-30 14:48:33 +0000
commit6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 (patch)
treef7adbc5ec8accc4bec3e38939bdf570a266f0e83 /caml
parent1bce6b0f9f8cd614038a6e7fc21fb984724204a4 (diff)
downloadcompcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.tar.gz
compcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.zip
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
Diffstat (limited to 'caml')
-rw-r--r--caml/CMlexer.mli17
-rw-r--r--caml/CMlexer.mll132
-rw-r--r--caml/CMparser.mly541
-rw-r--r--caml/CMtypecheck.ml370
-rw-r--r--caml/CMtypecheck.mli19
-rw-r--r--caml/Camlcoq.ml130
-rw-r--r--caml/Cil2Csyntax.ml992
-rw-r--r--caml/Clflags.ml25
-rw-r--r--caml/Coloringaux.ml625
-rw-r--r--caml/Coloringaux.mli20
-rw-r--r--caml/Driver.ml352
-rw-r--r--caml/Floataux.ml39
-rw-r--r--caml/Linearizeaux.ml85
-rw-r--r--caml/PrintCsyntax.ml501
-rw-r--r--caml/PrintPPC.ml532
-rw-r--r--caml/PrintPPC.mli13
-rw-r--r--caml/RTLgenaux.ml72
-rw-r--r--caml/RTLtypingaux.ml156
18 files changed, 0 insertions, 4621 deletions
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 }
- | "<u" { LESSU }
- | "<f" { LESSF }
- | "<=" { LESSEQUAL }
- | "<=u" { LESSEQUALU }
- | "<=f" { LESSEQUALF }
- | "<<" { LESSLESS }
- | "let" { LET }
- | "loop" { LOOP }
- | "(" { LPAREN }
- | "match" { MATCH }
- | "-" { MINUS }
- | "->" { MINUSGREATER }
- | "-f" { MINUSF }
- | "%" { PERCENT }
- | "%u" { PERCENTU }
- | "+" { PLUS }
- | "+f" { PLUSF }
- | "?" { QUESTION }
- | "}" { RBRACE }
- | "}}" { RBRACERBRACE }
- | "]" { RBRACKET }
- | "return" { RETURN }
- | ")" { RPAREN }
- | ";" { SEMICOLON }
- | "/" { SLASH }
- | "/f" { SLASHF }
- | "/u" { SLASHU }
- | "stack" { STACK }
- | "*" { STAR }
- | "*f" { STARF }
- | "switch" { SWITCH }
- | "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 <float> FLOATLIT
-%token FLOATOFINT
-%token FLOATOFINTU
-%token GREATER
-%token GREATERF
-%token GREATERU
-%token GREATEREQUAL
-%token GREATEREQUALF
-%token GREATEREQUALU
-%token GREATERGREATER
-%token GREATERGREATERU
-%token <AST.ident> IDENT
-%token IF
-%token IN
-%token INT
-%token INT16S
-%token INT16U
-%token INT32
-%token INT8S
-%token INT8U
-%token <int32> INTLIT
-%token INTOFFLOAT
-%token 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 <AST.ident> 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 <Cminor.program> 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 "<unknown atom %ld>" (camlint_of_positive a)
-
-(* Strings *)
-
-let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
- Char.chr( (if a0 then 1 else 0)
- + (if a1 then 2 else 0)
- + (if a2 then 4 else 0)
- + (if a3 then 8 else 0)
- + (if a4 then 16 else 0)
- + (if a5 then 32 else 0)
- + (if a6 then 64 else 0)
- + (if a7 then 128 else 0))
-
-let coqstring_length s =
- let rec len accu = function
- | CString.EmptyString -> accu
- | CString.CString(_, s) -> len (accu + 1) s
- in len 0 s
-
-let camlstring_of_coqstring s =
- let r = String.create (coqstring_length s) in
- let rec fill pos = function
- | CString.EmptyString -> r
- | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
- in fill 0 s
-
-(* Timing facility *)
-
-(*
-let timers = (Hashtbl.create 9 : (string, float) Hashtbl.t)
-
-let add_to_timer name time =
- let old = try Hashtbl.find timers name with Not_found -> 0.0 in
- Hashtbl.replace timers name (old +. time)
-
-let time name fn arg =
- let start = Unix.gettimeofday() in
- try
- let res = fn arg in
- add_to_timer name (Unix.gettimeofday() -. start);
- res
- with x ->
- add_to_timer name (Unix.gettimeofday() -. start);
- raise x
-
-let print_timers () =
- Hashtbl.iter
- (fun name time -> Printf.printf "%-20s %.3f\n" name time)
- timers
-
-let _ = at_exit print_timers
-*)
diff --git a/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] <source files>
-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 <file>.i
- -S Compile to assembler only, save result in <file>.s
- -c Compile to object file only (no linking), result in <file>.o
-Preprocessing options:
- -I<dir> Add <dir> to search path for #include files
- -D<symb>=<val> Define preprocessor symbol
- -U<symb> 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 <file>.light.c
- -dasm Save generated assembly in <file>.s
-Linking options:
- -l<lib> Link library <lib>
- -L<dir> Add <dir> to search path for libraries
- -o <file> Generate executable in <file> (default: a.out)
-General options:
- -stdlib <dir> 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 "@[<hov 2>%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 "@[<hov 0>%a@ %s %a@]"
- print_expr_prec (level, e1)
- (name_binop op)
- print_expr_prec (level, e2)
- | Ecast(ty, e1) ->
- fprintf p "@[<hov 2>(%s)@,%a@]"
- (name_type ty)
- print_expr_prec (level, e1)
- | Econdition(e1, e2, e3) ->
- fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
- print_expr_prec (level, e1)
- print_expr_prec (level, e2)
- print_expr_prec (level, e3)
- | Eandbool(e1, e2) ->
- fprintf p "@[<hov 0>%a@ && %a@]"
- print_expr_prec (level, e1)
- print_expr_prec (level, e2)
- | Eorbool(e1, e2) ->
- fprintf p "@[<hov 0>%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 "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
- | Scall(None, e1, el) ->
- fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
- print_expr e1
- print_expr_list (true, el)
- | Scall(Some lhs, e1, el) ->
- fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%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 "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
- print_expr e
- print_stmt s1
- | Sifthenelse(e, s1, s2) ->
- fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
- print_expr e
- print_stmt s1
- print_stmt s2
- | Swhile(e, s) ->
- fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
- print_expr e
- print_stmt s
- | Sdowhile(e, s) ->
- fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
- print_stmt s
- print_expr e
- | Sfor(s_init, e, s_iter, s_body) ->
- fprintf p "@[<v 2>for (@[<hv 0>%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 "@[<v 2>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 "@[<v 2>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 "@[<v 2>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 "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
- print_expr e1
- print_expr_list (true, el)
- | Scall(Some lhs, e1, el) ->
- fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%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 "@[<v 2>{@ ";
- 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 "@[<hov 2>%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 "@[<v 2>%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 "@[<v 0>";
- 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 _ -> "<reg>"
- | 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 _ -> "<reg>"
- | 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
generated by cgit (git 2.34.1) at 2024-07-06 01:39:11 +0000