diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
commit | 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 (patch) | |
tree | f7adbc5ec8accc4bec3e38939bdf570a266f0e83 /caml/CMparser.mly | |
parent | 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 (diff) | |
download | compcert-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/CMparser.mly')
-rw-r--r-- | caml/CMparser.mly | 541 |
1 files changed, 0 insertions, 541 deletions
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 } -; |