From 8e5f68c1a6d921a46bb817fe0a82fca1c3494dde Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 7 Jan 2013 10:30:16 +0000 Subject: Update Cminor parser and printer so that the parser can parse the whole Cminor language and can reparse the output of the printer. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2090 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CMlexer.mll | 12 ++++-- backend/CMparser.mly | 107 +++++++++++++++++++++++++++++++++++++++++-------- backend/PrintCminor.ml | 14 +------ common/PrintAST.ml | 8 ++-- driver/Interp.ml | 4 +- 5 files changed, 107 insertions(+), 38 deletions(-) diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 2eaa488..eac48e0 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -21,10 +21,11 @@ exception Error of string let blank = [' ' '\009' '\012' '\010' '\013'] let floatlit = - ['0'-'9'] ['0'-'9' '_']* + ("-"? (['0'-'9'] ['0'-'9' '_']* ('.' ['0'-'9' '_']* )? - (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? + (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? )) | "inf" | "nan" let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']* +let qident = '\'' [ ^ '\'' ]+ '\'' let temp = "$" ['1'-'9'] ['0'-'9']* let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+ | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ ) @@ -40,6 +41,7 @@ rule token = parse | "!=f" { BANGEQUALF } | "!=u" { BANGEQUALU } | "|" { BAR } + | "builtin" { BUILTIN } | "^" { CARET } | "case" { CASE } | ":" { COLON } @@ -124,8 +126,10 @@ rule token = parse | 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 | temp { IDENT(intern_string(Lexing.lexeme lexbuf)) } + STRINGLIT(String.sub s 1 (String.length s - 2)) } + | ident | temp { IDENT(Lexing.lexeme lexbuf) } + | qident { let s = Lexing.lexeme lexbuf in + IDENT(String.sub s 1 (String.length s - 2)) } | eof { EOF } | _ { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index ce9bd08..ff77c03 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -25,6 +25,45 @@ open Integers open AST open Cminor +(** Parsing external functions *) + +type ef_token = + | EFT_tok of string + | EFT_int of int32 + | EFT_string of string + | EFT_chunk of memory_chunk + +let mkef sg toks = + match toks with + | [EFT_tok "extern"; EFT_string s] -> + EF_external(intern_string s, sg) + | [EFT_tok "builtin"; EFT_string s] -> + EF_builtin(intern_string s, sg) + | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> + EF_vload c + | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> + EF_vstore c + | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c; + EFT_tok "global"; EFT_string s; EFT_int n] -> + EF_vload_global(c, intern_string s, z_of_camlint n) + | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c; + EFT_tok "global"; EFT_string s; EFT_int n] -> + EF_vstore_global(c, intern_string s, z_of_camlint n) + | [EFT_tok "malloc"] -> + EF_malloc + | [EFT_tok "free"] -> + EF_free + | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> + EF_memcpy(z_of_camlint sz, z_of_camlint al) + | [EFT_tok "annot"; EFT_string txt] -> + EF_annot(intern_string txt, sg.sig_args) + | [EFT_tok "annot_val"; EFT_string txt] -> + if sg.sig_args = [] then raise Parsing.Parse_error; + EF_annot_val(intern_string txt, List.hd sg.sig_args) + | [EFT_tok "inline_asm"; EFT_string txt] -> + EF_inline_asm(intern_string txt) + | _ -> + raise Parsing.Parse_error (** Naming function calls in expressions *) @@ -35,6 +74,7 @@ type rexpr = | Rbinop of binary_operation * rexpr * rexpr | Rload of memory_chunk * rexpr | Rcall of signature * rexpr * rexpr list + | Rbuiltin of signature * ef_token list * rexpr list let temp_counter = ref 0 @@ -64,6 +104,12 @@ let rec convert_rexpr = function let t = mktemp() in convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu; Evar t + | Rbuiltin(sg, pef, el) -> + let ef = mkef sg pef in + let cl = convert_rexpr_list el in + let t = mktemp() in + convert_accu := Sbuiltin(Some t, ef, cl) :: !convert_accu; + Evar t and convert_rexpr_list = function | [] -> [] @@ -84,6 +130,10 @@ let mkeval e = let c1 = convert_rexpr e1 in let cl = convert_rexpr_list el in prepend_seq !convert_accu (Scall(None, sg, c1, cl)) + | Rbuiltin(sg, pef, el) -> + let ef = mkef sg pef in + let cl = convert_rexpr_list el in + prepend_seq !convert_accu (Sbuiltin(None, ef, cl)) | _ -> ignore (convert_rexpr e); prepend_seq !convert_accu Sskip @@ -95,6 +145,10 @@ let mkassign id e = let c1 = convert_rexpr e1 in let cl = convert_rexpr_list el in prepend_seq !convert_accu (Scall(Some id, sg, c1, cl)) + | Rbuiltin(sg, pef, el) -> + let ef = mkef sg pef in + let cl = convert_rexpr_list el in + prepend_seq !convert_accu (Sbuiltin(Some id, ef, cl)) | _ -> let c = convert_rexpr e in prepend_seq !convert_accu (Sassign(id, c)) @@ -196,6 +250,7 @@ let mkmatch expr cases = %token BANGEQUALF %token BANGEQUALU %token BAR +%token BUILTIN %token CARET %token CASE %token COLON @@ -224,7 +279,7 @@ let mkmatch expr cases = %token GREATEREQUALU %token GREATERGREATER %token GREATERGREATERU -%token IDENT +%token IDENT %token IF %token IN %token INLINE @@ -273,7 +328,7 @@ let mkmatch expr cases = %token STACK %token STAR %token STARF -%token STRINGLIT +%token STRINGLIT %token SWITCH %token TILDE %token TAILCALL @@ -321,11 +376,13 @@ global_declaration: proc { $1 } | VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ - { ($2, Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; - gvar_readonly = false; gvar_volatile = false}) } + { (intern_string $2, + Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; + gvar_readonly = false; gvar_volatile = false}) } | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE - { ($2, Gvar{gvar_info = (); gvar_init = List.rev $6; - gvar_readonly = $3; gvar_volatile = $4; } ) } + { (intern_string $2, + Gvar{gvar_info = (); gvar_init = List.rev $6; + gvar_readonly = $3; gvar_volatile = $4; } ) } ; is_readonly: @@ -357,7 +414,7 @@ init_data: | FLOAT FLOATLIT { Init_float64 (coqfloat_of_camlfloat $2) } | FLOATLIT { Init_float64 (coqfloat_of_camlfloat $1) } | LBRACKET INTLIT RBRACKET { Init_space (z_of_camlint $2) } - | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof ($3, coqint_of_camlint $1) } + | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof (intern_string $3, coqint_of_camlint $1) } ; /* Procedures */ @@ -372,14 +429,16 @@ proc: { let tmp = !temporaries in temporaries := []; temp_counter := 0; - ($1, + (intern_string $1, Gfun(Internal { fn_sig = $6; fn_params = List.rev $3; fn_vars = List.rev (tmp @ $9); fn_stackspace = $8; fn_body = $10 })) } | EXTERN STRINGLIT COLON signature - { ($2, Gfun(External(EF_external($2,$4)))) } + { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) } + | EXTERN STRINGLIT EQUAL eftoks COLON signature + { (intern_string $2, Gfun(External(mkef $6 $4))) } ; signature: @@ -397,8 +456,8 @@ parameters: ; parameter_list: - IDENT { $1 :: [] } - | parameter_list COMMA IDENT { $3 :: $1 } + IDENT { intern_string $1 :: [] } + | parameter_list COMMA IDENT { intern_string $3 :: $1 } ; stack_declaration: @@ -419,7 +478,7 @@ var_declaration: stmt: expr SEMICOLON { mkeval $1 } - | IDENT EQUAL expr SEMICOLON { mkassign $1 $3 } + | IDENT EQUAL expr SEMICOLON { mkassign (intern_string $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 } @@ -437,8 +496,8 @@ stmt: | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON { mktailcall $7 $2 $4 } | WHILE LPAREN expr RPAREN stmts { mkwhile $3 $5 } - | IDENT COLON stmts { Slabel ($1,$3) } - | GOTO IDENT SEMICOLON { Sgoto $2 } + | IDENT COLON stmts { Slabel (intern_string $1,$3) } + | GOTO IDENT SEMICOLON { Sgoto(intern_string $2) } ; stmts: @@ -467,10 +526,10 @@ match_cases: expr: LPAREN expr RPAREN { $2 } - | IDENT { Rvar $1 } + | IDENT { Rvar(intern_string $1) } | INTLIT { intconst $1 } | FLOATLIT { Rconst(Ofloatconst (coqfloat_of_camlfloat $1)) } - | STRINGLIT { Rconst(Oaddrsymbol($1, Int.zero)) } + | STRINGLIT { Rconst(Oaddrsymbol(intern_string $1, Int.zero)) } | AMPERSAND INTLIT { Rconst(Oaddrstack(coqint_of_camlint $2)) } | MINUS expr %prec p_uminus { Runop(Onegint, $2) } | MINUSF expr %prec p_uminus { Runop(Onegf, $2) } @@ -523,6 +582,7 @@ expr: | expr GREATEREQUALF expr { Rbinop(Ocmpf Cge, $1, $3) } | memory_chunk LBRACKET expr RBRACKET { Rload($1, $3) } | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) } + | BUILTIN eftoks LPAREN expr_list RPAREN COLON signature{ Rbuiltin($7, $2, $4) } ; expr_list: @@ -554,3 +614,18 @@ type_: | FLOAT { Tfloat } ; +/* External functions */ + +eftok: + IDENT { EFT_tok $1 } + | STRINGLIT { EFT_string $1 } + | INTLIT { EFT_int $1 } + | VOLATILE { EFT_tok "volatile" } + | EXTERN { EFT_tok "extern" } + | BUILTIN { EFT_tok "builtin" } +; + +eftoks: + eftok eftoks { $1 :: $2 } + | /*empty*/ { [] } +; diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index dfcabb3..4806275 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -92,16 +92,6 @@ let name_of_binop = function | Ocmpu c -> comparison_name c ^ "u" | Ocmpf c -> comparison_name c ^ "f" -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - | Mfloat64al32 -> "float64al32" - (* Expressions *) let rec expr p (prec, e) = @@ -266,8 +256,8 @@ let print_function p id f = fprintf p "@;<0 -2>}@]@ " let print_extfun p id ef = - fprintf p "@[extern @[\"%s\":@ %a@]@ " - (extern_atom id) print_sig (ef_sig ef) + fprintf p "@[extern @[\"%s\" =@ %s :@ %a@]@ " + (extern_atom id) (name_of_external ef) print_sig (ef_sig ef) let print_init_data p = function | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i) diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 6a66c30..53741d5 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -29,15 +29,15 @@ let name_of_chunk = function | Mfloat64al32 -> "float64al32" let name_of_external = function - | EF_external(name, sg) -> extern_atom name - | EF_builtin(name, sg) -> extern_atom name + | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name) + | EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name) | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) | EF_vload_global(chunk, id, ofs) -> - sprintf "volatile load %s global %s %ld" + sprintf "volatile load %s global %S %ld" (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | EF_vstore_global(chunk, id, ofs) -> - sprintf "volatile store %s global %s %ld" + sprintf "volatile store %s global %S %ld" (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | EF_malloc -> "malloc" | EF_free -> "free" diff --git a/driver/Interp.ml b/driver/Interp.ml index 9031042..63d51a4 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -69,12 +69,12 @@ let print_event p = function print_eventval res | Event_vload(chunk, id, ofs, res) -> fprintf p "volatile load %s[&%s%+ld] -> %a" - (PrintCminor.name_of_chunk chunk) + (PrintAST.name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) print_eventval res | Event_vstore(chunk, id, ofs, arg) -> fprintf p "volatile store %s[&%s%+ld] <- %a" - (PrintCminor.name_of_chunk chunk) + (PrintAST.name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) print_eventval arg | Event_annot(text, args) -> -- cgit v1.2.3