From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/CMlexer.mll | 3 + caml/CMparser.mly | 194 ++++++++++++++++++++++++++++------------- caml/CMtypecheck.ml | 239 ++++++++++++++++++++++----------------------------- caml/Camlcoq.ml | 45 ++++++---- caml/Coloringaux.ml | 18 ++-- caml/Main2.ml | 8 +- caml/PrintPPC.ml | 6 +- caml/RTLgenaux.ml | 46 +++++++++- caml/RTLtypingaux.ml | 21 ++++- 9 files changed, 342 insertions(+), 238 deletions(-) (limited to 'caml') diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll index 49d0dbdd..ae71e0c1 100644 --- a/caml/CMlexer.mll +++ b/caml/CMlexer.mll @@ -30,8 +30,10 @@ rule token = parse | "|" { BAR } | "||" { BARBAR } | "^" { CARET } + | "case" { CASE } | ":" { COLON } | "," { COMMA } + | "default" { DEFAULT } | "$" { DOLLAR } | "else" { ELSE } | "=" { EQUAL } @@ -75,6 +77,7 @@ rule token = parse | "let" { LET } | "loop" { LOOP } | "(" { LPAREN } + | "match" { MATCH } | "-" { MINUS } | "->" { MINUSGREATER } | "-f" { MINUSF } diff --git a/caml/CMparser.mly b/caml/CMparser.mly index d9a81874..0db0af2b 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -8,16 +8,67 @@ open BinPos open BinInt open Integers open AST -open Op open Cminor let intconst n = - Eop(Ointconst(coqint_of_camlint n), Enil) + Econst(Ointconst(coqint_of_camlint n)) let andbool e1 e2 = - Cmconstr.conditionalexpr e1 e2 (intconst 0l) + Econdition(e1, e2, intconst 0l) let orbool e1 e2 = - Cmconstr.conditionalexpr e1 (intconst 1l) e2 + Econdition(e1, intconst 1l, e2) + +let exitnum n = nat_of_camlint(Int32.pred n) + +let mkswitch expr (cases, dfl) = + let rec mktable = function + | [] -> Coq_nil + | (key, exit) :: rem -> + Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in + Sswitch(expr, 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] -> Coq_nil + | (key, action) :: rem -> + Coq_cons(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 = + match cases with + | [] -> Sskip (* ??? *) + | [key, action] -> action + | _ -> mkmatch_aux expr cases %} @@ -32,8 +83,10 @@ let orbool e1 e2 = %token BAR %token BARBAR %token CARET +%token CASE %token COLON %token COMMA +%token DEFAULT %token DOLLAR %token ELSE %token EQUAL @@ -81,6 +134,7 @@ let orbool e1 e2 = %token LET %token LOOP %token LPAREN +%token MATCH %token MINUS %token MINUSF %token MINUSGREATER @@ -200,7 +254,7 @@ parameter_list: stack_declaration: /* empty */ { Z0 } - | STACK INTLIT { z_of_camlint $2 } + | STACK INTLIT SEMICOLON { z_of_camlint $2 } ; var_declarations: @@ -217,14 +271,18 @@ var_declaration: stmt: expr SEMICOLON { Sexpr $1 } | IDENT EQUAL expr SEMICOLON { Sassign($1, $3) } - | IF LPAREN expr RPAREN stmts ELSE stmts { Cmconstr.ifthenelse $3 $5 $7 } - | IF LPAREN expr RPAREN stmts { Cmconstr.ifthenelse $3 $5 Sskip } + | IF LPAREN expr RPAREN stmts ELSE stmts { Sifthenelse($3, $5, $7) } + | IF LPAREN expr RPAREN stmts { Sifthenelse($3, $5, Sskip) } | LOOP stmts { Sloop($2) } | LBRACELBRACE stmt_list RBRACERBRACE { Sblock($2) } | EXIT SEMICOLON { Sexit O } - | EXIT INTLIT SEMICOLON { Sexit (nat_of_camlint(Int32.pred $2)) } + | EXIT INTLIT SEMICOLON { Sexit (exitnum $2) } | RETURN SEMICOLON { Sreturn None } | RETURN expr SEMICOLON { Sreturn (Some $2) } + | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE + { mkswitch $3 $6 } + | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE + { mkmatch $3 $6 } ; stmts: @@ -237,72 +295,84 @@ stmt_list: | 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 { Evar $1 } | INTLIT { intconst $1 } - | FLOATLIT { Eop(Ofloatconst $1, Enil) } - | STRINGLIT { Eop(Oaddrsymbol($1, Int.zero), Enil) } - | AMPERSAND INTLIT { Eop(Oaddrstack(coqint_of_camlint $2), Enil) } - | MINUS expr %prec p_uminus { Cmconstr.negint $2 } - | MINUSF expr %prec p_uminus { Cmconstr.negfloat $2 } - | ABSF expr { Cmconstr.absfloat $2 } - | INTOFFLOAT expr { Cmconstr.intoffloat $2 } - | FLOATOFINT expr { Cmconstr.floatofint $2 } - | FLOATOFINTU expr { Cmconstr.floatofintu $2 } - | TILDE expr { Cmconstr.notint $2 } - | BANG expr { Cmconstr.notbool $2 } - | INT8S expr { Cmconstr.cast8signed $2 } - | INT8U expr { Cmconstr.cast8unsigned $2 } - | INT16S expr { Cmconstr.cast16signed $2 } - | INT16U expr { Cmconstr.cast16unsigned $2 } - | FLOAT32 expr { Cmconstr.singleoffloat $2 } + | FLOATLIT { Econst(Ofloatconst $1) } + | STRINGLIT { Econst(Oaddrsymbol($1, Int.zero)) } + | AMPERSAND INTLIT { Econst(Oaddrstack(coqint_of_camlint $2)) } + | MINUS expr %prec p_uminus { Eunop(Onegint, $2) } + | MINUSF expr %prec p_uminus { Eunop(Onegf, $2) } + | ABSF expr { Eunop(Oabsf, $2) } + | INTOFFLOAT expr { Eunop(Ointoffloat, $2) } + | FLOATOFINT expr { Eunop(Ofloatofint, $2) } + | FLOATOFINTU expr { Eunop(Ofloatofintu, $2) } + | TILDE expr { Eunop(Onotint, $2) } + | BANG expr { Eunop(Onotbool, $2) } + | INT8S expr { Eunop(Ocast8signed, $2) } + | INT8U expr { Eunop(Ocast8unsigned, $2) } + | INT16S expr { Eunop(Ocast16signed, $2) } + | INT16U expr { Eunop(Ocast16unsigned, $2) } + | FLOAT32 expr { Eunop(Osingleoffloat, $2) } | ALLOC expr { Ealloc $2 } - | expr PLUS expr { Cmconstr.add $1 $3 } - | expr MINUS expr { Cmconstr.sub $1 $3 } - | expr STAR expr { Cmconstr.mul $1 $3 } - | expr SLASH expr { Cmconstr.divs $1 $3 } - | expr PERCENT expr { Cmconstr.mods $1 $3 } - | expr SLASHU expr { Cmconstr.divu $1 $3 } - | expr PERCENTU expr { Cmconstr.modu $1 $3 } - | expr AMPERSAND expr { Cmconstr.coq_and $1 $3 } - | expr BAR expr { Cmconstr.coq_or $1 $3 } - | expr CARET expr { Cmconstr.xor $1 $3 } - | expr LESSLESS expr { Cmconstr.shl $1 $3 } - | expr GREATERGREATER expr { Cmconstr.shr $1 $3 } - | expr GREATERGREATERU expr { Cmconstr.shru $1 $3 } - | expr PLUSF expr { Cmconstr.addf $1 $3 } - | expr MINUSF expr { Cmconstr.subf $1 $3 } - | expr STARF expr { Cmconstr.mulf $1 $3 } - | expr SLASHF expr { Cmconstr.divf $1 $3 } - | expr EQUALEQUAL expr { Cmconstr.cmp Ceq $1 $3 } - | expr BANGEQUAL expr { Cmconstr.cmp Cne $1 $3 } - | expr LESS expr { Cmconstr.cmp Clt $1 $3 } - | expr LESSEQUAL expr { Cmconstr.cmp Cle $1 $3 } - | expr GREATER expr { Cmconstr.cmp Cgt $1 $3 } - | expr GREATEREQUAL expr { Cmconstr.cmp Cge $1 $3 } - | expr EQUALEQUALU expr { Cmconstr.cmpu Ceq $1 $3 } - | expr BANGEQUALU expr { Cmconstr.cmpu Cne $1 $3 } - | expr LESSU expr { Cmconstr.cmpu Clt $1 $3 } - | expr LESSEQUALU expr { Cmconstr.cmpu Cle $1 $3 } - | expr GREATERU expr { Cmconstr.cmpu Cgt $1 $3 } - | expr GREATEREQUALU expr { Cmconstr.cmpu Cge $1 $3 } - | expr EQUALEQUALF expr { Cmconstr.cmpf Ceq $1 $3 } - | expr BANGEQUALF expr { Cmconstr.cmpf Cne $1 $3 } - | expr LESSF expr { Cmconstr.cmpf Clt $1 $3 } - | expr LESSEQUALF expr { Cmconstr.cmpf Cle $1 $3 } - | expr GREATERF expr { Cmconstr.cmpf Cgt $1 $3 } - | expr GREATEREQUALF expr { Cmconstr.cmpf Cge $1 $3 } - | memory_chunk LBRACKET expr RBRACKET { Cmconstr.load $1 $3 } + | expr PLUS expr { Ebinop(Oadd, $1, $3) } + | expr MINUS expr { Ebinop(Osub, $1, $3) } + | expr STAR expr { Ebinop(Omul, $1, $3) } + | expr SLASH expr { Ebinop(Odiv, $1, $3) } + | expr PERCENT expr { Ebinop(Omod, $1, $3) } + | expr SLASHU expr { Ebinop(Odivu, $1, $3) } + | expr PERCENTU expr { Ebinop(Omodu, $1, $3) } + | expr AMPERSAND expr { Ebinop(Oand, $1, $3) } + | expr BAR expr { Ebinop(Oor, $1, $3) } + | expr CARET expr { Ebinop(Oxor, $1, $3) } + | expr LESSLESS expr { Ebinop(Oshl, $1, $3) } + | expr GREATERGREATER expr { Ebinop(Oshr, $1, $3) } + | expr GREATERGREATERU expr { Ebinop(Oshru, $1, $3) } + | expr PLUSF expr { Ebinop(Oaddf, $1, $3) } + | expr MINUSF expr { Ebinop(Osubf, $1, $3) } + | expr STARF expr { Ebinop(Omulf, $1, $3) } + | expr SLASHF expr { Ebinop(Odivf, $1, $3) } + | expr EQUALEQUAL expr { Ebinop(Ocmp Ceq, $1, $3) } + | expr BANGEQUAL expr { Ebinop(Ocmp Cne, $1, $3) } + | expr LESS expr { Ebinop(Ocmp Clt, $1, $3) } + | expr LESSEQUAL expr { Ebinop(Ocmp Cle, $1, $3) } + | expr GREATER expr { Ebinop(Ocmp Cgt, $1, $3) } + | expr GREATEREQUAL expr { Ebinop(Ocmp Cge, $1, $3) } + | expr EQUALEQUALU expr { Ebinop(Ocmpu Ceq, $1, $3) } + | expr BANGEQUALU expr { Ebinop(Ocmpu Cne, $1, $3) } + | expr LESSU expr { Ebinop(Ocmpu Clt, $1, $3) } + | expr LESSEQUALU expr { Ebinop(Ocmpu Cle, $1, $3) } + | expr GREATERU expr { Ebinop(Ocmpu Cgt, $1, $3) } + | expr GREATEREQUALU expr { Ebinop(Ocmpu Cge, $1, $3) } + | expr EQUALEQUALF expr { Ebinop(Ocmpf Ceq, $1, $3) } + | expr BANGEQUALF expr { Ebinop(Ocmpf Cne, $1, $3) } + | expr LESSF expr { Ebinop(Ocmpf Clt, $1, $3) } + | expr LESSEQUALF expr { Ebinop(Ocmpf Cle, $1, $3) } + | expr GREATERF expr { Ebinop(Ocmpf Cgt, $1, $3) } + | expr GREATEREQUALF expr { Ebinop(Ocmpf Cge, $1, $3) } + | memory_chunk LBRACKET expr RBRACKET { Eload($1, $3) } | memory_chunk LBRACKET expr RBRACKET EQUAL expr - { Cmconstr.store $1 $3 $6 } + { Estore($1, $3, $6) } | expr LPAREN expr_list RPAREN COLON signature { Ecall($6, $1, $3) } | expr AMPERSANDAMPERSAND expr { andbool $1 $3 } | expr BARBAR expr { orbool $1 $3 } - | expr QUESTION expr COLON expr { Cmconstr.conditionalexpr $1 $3 $5 } + | expr QUESTION expr COLON expr { Econdition($1, $3, $5) } | LET expr IN expr %prec p_let { Elet($2, $4) } | DOLLAR INTLIT { Eletvar (nat_of_camlint $2) } ; diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index a926039d..495ded0c 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -6,7 +6,6 @@ open CList open Camlcoq open AST open Integers -open Op open Cminor exception Error of string @@ -67,135 +66,91 @@ let name_of_comparison = function | Cgt -> "gt" | Cge -> "ge" -let type_condition = function - | Ccomp _ -> [tint;tint] - | Ccompu _ -> [tint;tint] - | Ccompimm _ -> [tint] - | Ccompuimm _ -> [tint] - | Ccompf _ -> [tfloat;tfloat] - | Cnotcompf _ -> [tfloat;tfloat] - | Cmaskzero _ -> [tint] - | Cmasknotzero _ -> [tint] +let type_constant = function + | Ointconst _ -> tint + | Ofloatconst _ -> tfloat + | Oaddrsymbol _ -> tint + | Oaddrstack _ -> tint -let name_of_condition = function - | Ccomp c -> sprintf "comp %s" (name_of_comparison c) - | Ccompu c -> sprintf "compu %s" (name_of_comparison c) - | Ccompimm(c, n) -> sprintf "compimm %s %ld" (name_of_comparison c) (camlint_of_coqint n) - | Ccompuimm(c, n) -> sprintf "compuimm %s %ld" (name_of_comparison c) (camlint_of_coqint n) - | Ccompf c -> sprintf "compf %s" (name_of_comparison c) - | Cnotcompf c -> sprintf "notcompf %s" (name_of_comparison c) - | Cmaskzero n -> sprintf "maskzero %ld" (camlint_of_coqint n) - | Cmasknotzero n -> sprintf "masknotzero %ld" (camlint_of_coqint n) +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 + | Ofloatofint -> tint, tfloat + | Ofloatofintu -> tint, tfloat -let type_operation = function - | Omove -> let v = newvar() in [v], v - | Ointconst _ -> [], tint - | Ofloatconst _ -> [], tfloat - | Oaddrsymbol _ -> [], tint - | Oaddrstack _ -> [], tint - | Oundef -> [], newvar() - | Ocast8signed -> [tint], tint - | Ocast16signed -> [tint], tint - | Ocast8unsigned -> [tint], tint - | Ocast16unsigned -> [tint], tint - | Oadd -> [tint;tint], tint - | Oaddimm _ -> [tint], tint - | Osub -> [tint;tint], tint - | Osubimm _ -> [tint], tint - | Omul -> [tint;tint], tint - | Omulimm _ -> [tint], tint - | Odiv -> [tint;tint], tint - | Odivu -> [tint;tint], tint - | Oand -> [tint;tint], tint - | Oandimm _ -> [tint], tint - | Oor -> [tint;tint], tint - | Oorimm _ -> [tint], tint - | Oxor -> [tint;tint], tint - | Oxorimm _ -> [tint], tint - | Onand -> [tint;tint], tint - | Onor -> [tint;tint], tint - | Onxor -> [tint;tint], tint - | Oshl -> [tint;tint], tint - | Oshr -> [tint;tint], tint - | Oshrimm _ -> [tint], tint - | Oshrximm _ -> [tint], tint - | Oshru -> [tint;tint], tint - | Orolm _ -> [tint], tint - | Onegf -> [tfloat], tfloat - | Oabsf -> [tfloat], tfloat - | Oaddf -> [tfloat;tfloat], tfloat - | Osubf -> [tfloat;tfloat], tfloat - | Omulf -> [tfloat;tfloat], tfloat - | Odivf -> [tfloat;tfloat], tfloat - | Omuladdf -> [tfloat;tfloat;tfloat], tfloat - | Omulsubf -> [tfloat;tfloat;tfloat], tfloat - | Osingleoffloat -> [tfloat], tfloat - | Ointoffloat -> [tfloat], tint - | Ofloatofint -> [tint], tfloat - | Ofloatofintu -> [tint], tfloat - | Ocmp c -> type_condition c, tint +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_operation = function - | Omove -> "move" +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) - | Oundef -> "undef" + +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" + | Ofloatofint -> "floatofint" + | Ofloatofintu -> "floatofintu" + +let name_of_binary_operation = function | Oadd -> "add" - | Oaddimm n -> sprintf "addimm %ld" (camlint_of_coqint n) | Osub -> "sub" - | Osubimm n -> sprintf "subimm %ld" (camlint_of_coqint n) | Omul -> "mul" - | Omulimm n -> sprintf "mulimm %ld" (camlint_of_coqint n) | Odiv -> "div" | Odivu -> "divu" + | Omod -> "mod" + | Omodu -> "modu" | Oand -> "and" - | Oandimm n -> sprintf "andimm %ld" (camlint_of_coqint n) | Oor -> "or" - | Oorimm n -> sprintf "orimm %ld" (camlint_of_coqint n) | Oxor -> "xor" - | Oxorimm n -> sprintf "xorimm %ld" (camlint_of_coqint n) - | Onand -> "nand" - | Onor -> "nor" - | Onxor -> "nxor" | Oshl -> "shl" | Oshr -> "shr" - | Oshrimm n -> sprintf "shrimm %ld" (camlint_of_coqint n) - | Oshrximm n -> sprintf "shrximm %ld" (camlint_of_coqint n) | Oshru -> "shru" - | Orolm(n, m) -> sprintf "rolm %ld %ld" (camlint_of_coqint n) (camlint_of_coqint m) - | Onegf -> "negf" - | Oabsf -> "absf" | Oaddf -> "addf" | Osubf -> "subf" | Omulf -> "mulf" | Odivf -> "divf" - | Omuladdf -> "muladdf" - | Omulsubf -> "mulsubf" - | Osingleoffloat -> "singleoffloat" - | Ointoffloat -> "intoffloat" - | Ofloatofint -> "floatofint" - | Ofloatofintu -> "floatofintu" - | Ocmp c -> name_of_condition c - -let type_addressing = function - | Aindexed _ -> [tint] - | Aindexed2 -> [tint;tint] - | Aglobal _ -> [] - | Abased _ -> [tint] - | Ainstack _ -> [] - -let name_of_addressing = function - | Aindexed n -> sprintf "indexed %ld" (camlint_of_coqint n) - | Aindexed2 -> sprintf "indexed2" - | Aglobal(s, ofs) -> sprintf "global %s %ld" (extern_atom s) (camlint_of_coqint ofs) - | Abased(s, ofs) -> sprintf "based %s %ld" (extern_atom s) (camlint_of_coqint ofs) - | Ainstack n -> sprintf "instack %ld" (camlint_of_coqint n) + | 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 @@ -219,34 +174,47 @@ let rec type_expr env lenv e = match e with | Evar id -> type_var env id - | Eop(op, el) -> - let tel = type_exprlist env lenv el in - let (targs, tres) = type_operation op in + | 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_list targs tel + unify targ te1 with Error s -> raise (Error (sprintf "In application of operator %s:\n%s" - (name_of_operation op) s)) + (name_of_unary_operation op) s)) end; tres - | Eload(chunk, addr, el) -> - let tel = type_exprlist env lenv el in + | 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_list (type_addressing addr) tel + unify targ1 te1; unify targ2 te2 with Error s -> - raise (Error (sprintf "In load %s %s:\n%s" - (name_of_chunk chunk) (name_of_addressing addr) 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 - | Estore(chunk, addr, el, e1) -> - let tel = type_exprlist env lenv el in + | Estore(chunk, e1, e2) -> let te1 = type_expr env lenv e1 in + let te2 = type_expr env lenv e2 in begin try - unify_list (type_addressing addr) tel; - unify (type_chunk chunk) te1 + unify tint te1; + unify (type_chunk chunk) te2 with Error s -> - raise (Error (sprintf "In store %s %s:\n%s" - (name_of_chunk chunk) (name_of_addressing addr) s)) + raise (Error (sprintf "In store %s:\n%s" + (name_of_chunk chunk) s)) end; te1 | Ecall(sg, e1, el) -> @@ -295,21 +263,13 @@ and type_exprlist env lenv el = let tet = type_exprlist env lenv et in (te1 :: tet) -and type_condexpr env lenv ce = - match ce with - | CEtrue -> () - | CEfalse -> () - | CEcond(c, el) -> - let tel = type_exprlist env lenv el in - begin try - unify_list (type_condition c) tel - with Error s -> - raise (Error (sprintf "In condition %s:\n%s" (name_of_condition c) s)) - end - | CEcondition(ce1, ce2, ce3) -> - type_condexpr env lenv ce1; - type_condexpr env lenv ce2; - type_condexpr env lenv ce3 +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 @@ -355,6 +315,15 @@ let rec type_stmt env blk ret 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 let rec env_of_vars idl = match idl with diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index c2115dfb..ec2447fa 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -41,7 +41,7 @@ let z_of_camlint n = let coqint_of_camlint : int32 -> Integers.int = z_of_camlint -(* Strings *) +(* 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) @@ -69,24 +69,6 @@ let rec coqlist_iter f = function Coq_nil -> () | Coq_cons(a,l) -> f a; coqlist_iter f l -(* Helpers *) - -let rec list_iter f = function - [] -> () - | a::l -> f a; list_iter f l - -let rec list_memq x = function - [] -> false - | a::l -> a == x || list_memq x l - -let rec list_exists p = function - [] -> false - | a::l -> p a || list_exists p l - -let rec list_filter p = function - [] -> [] - | x :: l -> if p x then x :: list_filter p l else list_filter p l - let rec length_coqlist = function | Coq_nil -> 0 | Coq_cons (x, l) -> 1 + length_coqlist l @@ -100,6 +82,31 @@ let array_of_coqlist = function | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in fill 1 tl +(* 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 *) (* diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml index a7c8db5c..b3f4515e 100644 --- a/caml/Coloringaux.ml +++ b/caml/Coloringaux.ml @@ -185,8 +185,8 @@ let init() = let interfere n1 n2 = if n1.degree < n2.degree - then list_memq n2 n1.adjlist - else list_memq n1 n2.adjlist + 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 *) @@ -199,7 +199,7 @@ let addEdge n1 n2 = (* Apply the given function to the relevant adjacent nodes of a node *) let iterAdjacent f n = - list_iter + List.iter (fun n -> match n.nstate with | SelectStack | CoalescedNodes -> () @@ -214,12 +214,12 @@ let moveIsActiveOrWorklist m = | _ -> false let nodeMoves n = - list_filter moveIsActiveOrWorklist n.movelist + List.filter moveIsActiveOrWorklist n.movelist (* Determine whether a node is involved in a move *) let moveRelated n = - list_exists moveIsActiveOrWorklist n.movelist + List.exists moveIsActiveOrWorklist n.movelist (*i (* Check invariants *) @@ -361,7 +361,7 @@ let build g typenv spillcosts = (* Enable moves that have become low-degree related *) let enableMoves n = - list_iter + List.iter (fun m -> if m.mstate = ActiveMoves then DLinkMove.move m activeMoves worklistMoves) @@ -481,7 +481,7 @@ let freezeMoves u = && v.degree < num_available_registers.(v.regclass) && v.nstate <> Colored then DLinkNode.move v freezeWorklist simplifyWorklist in - list_iter freeze (nodeMoves u) + List.iter freeze (nodeMoves u) (* Pick a move and freeze it *) @@ -577,7 +577,7 @@ let find_slot conflicts typ = let assign_color n = let conflicts = ref Locset.empty in - list_iter + List.iter (fun n' -> match (getAlias n').color with | None -> () @@ -607,7 +607,7 @@ let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t) init(); Array.fill start_points 0 num_register_classes 0; let mapping = build g env (spill_costs f) in - list_iter assign_color (nodeOrder []); + 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/Main2.ml b/caml/Main2.ml index ff9f3509..e3399fb9 100644 --- a/caml/Main2.ml +++ b/caml/Main2.ml @@ -94,8 +94,8 @@ let process_c_file sourcename = (* Convert to PPC *) let ppc = match Main.transf_c_program csyntax with - | Datatypes.Some x -> x - | Datatypes.None -> + | Errors.OK x -> x + | Errors.Error msg -> eprintf "Error in translation Csyntax -> PPC\n"; exit 2 in (* Save PPC asm *) @@ -111,10 +111,10 @@ let process_cminor_file sourcename = match Main.transf_cminor_program (CMtypecheck.type_program (CMparser.prog CMlexer.token lb)) with - | Datatypes.None -> + | Errors.Error msg -> eprintf "Compiler failure\n"; exit 2 - | Datatypes.Some p -> + | Errors.OK p -> let oc = open_out targetname in PrintPPC.print_program oc p; close_out oc diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 3ee79d12..bf7b2cc7 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -137,6 +137,8 @@ let print_instruction oc labels = function 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) -> @@ -318,10 +320,6 @@ let print_instruction oc labels = function fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 print_constant c | Plabel lbl -> if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl - | Piundef r -> - fprintf oc " # undef %a\n" ireg r - | Pfundef r -> - fprintf oc " # undef %a\n" freg r let rec labels_of_code = function | Coq_nil -> Labelset.empty diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml index 336346af..61abecfa 100644 --- a/caml/RTLgenaux.ml +++ b/caml/RTLgenaux.ml @@ -1,3 +1,47 @@ -open Cminor +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 + | CList.Coq_nil -> [] + | CList.Coq_cons(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 = + match hi - lo with + | 0 -> + CTaction default + | 1 -> + CTifeq(fst sw.(lo), snd sw.(lo), CTaction default) + | 2 -> + CTifeq(fst sw.(lo), snd sw.(lo), + CTifeq(fst sw.(lo+1), snd sw.(lo+1), + CTaction default)) + | 3 -> + CTifeq(fst sw.(lo), snd sw.(lo), + CTifeq(fst sw.(lo+1), snd sw.(lo+1), + CTifeq(fst sw.(lo+2), snd sw.(lo+2), + CTaction default))) + | _ -> + let mid = (lo + hi) / 2 in + CTiflt(fst sw.(mid), build lo mid, build mid hi) + in build 0 (Array.length sw) + diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml index 64f839a2..5ed7e6e2 100644 --- a/caml/RTLtypingaux.ml +++ b/caml/RTLtypingaux.ml @@ -32,10 +32,6 @@ let type_instr retty (Coq_pair(pc, i)) = () | Iop(Omove, _, _, _) -> () - | Iop(Oundef, Coq_nil, res, _) -> - () - | Iop(Oundef, _, _, _) -> - raise (Type_error "wrong Oundef") | Iop(op, args, res, _) -> let (Coq_pair(targs, tres)) = type_of_operation op in set_types args targs; set_type res tres @@ -61,6 +57,23 @@ let type_instr retty (Coq_pair(pc, i)) = raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s" name msg)) end + | Itailcall(sg, ros, args) -> + begin try + begin match ros with + | Coq_inl r -> set_type r Tint + | Coq_inr _ -> () + end; + set_types args sg.sig_args; + if sg.sig_res <> retty then + raise (Type_error "mismatch on return type") + with Type_error msg -> + let name = + match ros with + | Coq_inl _ -> "" + | Coq_inr id -> extern_atom id in + raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" + name msg)) + end | Ialloc(arg, res, _) -> set_type arg Tint; set_type res Tint | Icond(cond, args, _, _) -> -- cgit