From 8a64451e6f474d20a469b939a938577bbe6d3d66 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 9 Mar 2012 09:52:04 +0000 Subject: Merge of Andrew Tolmach's HASP-related changes git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CMlexer.mll | 16 +++++++++-- backend/CMparser.mly | 75 +++++++++++++++++++++++++++++++++++++++++++------- backend/PrintCminor.ml | 47 +++++++++++++++++++++++++++---- backend/RTLgen.v | 2 +- 4 files changed, 120 insertions(+), 20 deletions(-) (limited to 'backend') diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 3506e50..780d812 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -24,7 +24,8 @@ 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 ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']* +let temp = "$" ['0'-'9'] ['0'-'9']* let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+ | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ ) let stringlit = "\"" [ ^ '"' ] * '"' @@ -46,7 +47,6 @@ rule token = parse | ":" { COLON } | "," { COMMA } | "default" { DEFAULT } - | "$" { DOLLAR } | "else" { ELSE } | "=" { EQUAL } | "==" { EQUALEQUAL } @@ -59,6 +59,7 @@ rule token = parse | "float64" { FLOAT64 } | "floatofint" { FLOATOFINT } | "floatofintu" { FLOATOFINTU } + | "goto" { GOTO } | ">" { GREATER } | ">f" { GREATERF } | ">u" { GREATERU } @@ -69,10 +70,13 @@ rule token = parse | ">>u" { GREATERGREATERU } | "if" { IF } | "in" { IN } + | "inline" { INLINE } | "int" { INT } + | "int16" { INT16 } | "int16s" { INT16S } | "int16u" { INT16U } | "int32" { INT32 } + | "int8" { INT8 } | "int8s" { INT8S } | "int8u" { INT8U } | "intoffloat" { INTOFFLOAT } @@ -102,6 +106,7 @@ rule token = parse | "}" { RBRACE } | "}}" { RBRACERBRACE } | "]" { RBRACKET } + | "readonly" { READONLY } | "return" { RETURN } | ")" { RPAREN } | ";" { SEMICOLON } @@ -116,12 +121,17 @@ rule token = parse | "~" { TILDE } | "var" { VAR } | "void" { VOID } + | "volatile" { VOLATILE } + | "while" { WHILE } | 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)) } + | ident { IDENT(BinPos.Coq_xO (intern_string(Lexing.lexeme lexbuf))) } + | temp { let s = Lexing.lexeme lexbuf in + let n = Int32.of_string(String.sub s 1 (String.length s -1)) in + IDENT(if n = 0l then BinPos.Coq_xH else BinPos.Coq_xI (positive_of_camlint n)) } | eof { EOF } | _ { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 3df3f54..c52261d 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -13,6 +13,10 @@ /* */ /* *********************************************************************/ +/* HASP: Modified to parse global data declarations, other small changes */ +/* Note that this compiles a superset of the language defined by the AST, + including function calls in expressions, matches, while statements, etc. */ + %{ open Datatypes open Camlcoq @@ -22,6 +26,7 @@ open Integers open AST open Cminor + (** Naming function calls in expressions *) type rexpr = @@ -40,7 +45,7 @@ let temporaries = ref [] let mktemp () = incr temp_counter; let n = Printf.sprintf "__t%d" !temp_counter in - let id = intern_string n in + let id = Coq_xO (intern_string n) in temporaries := id :: !temporaries; id @@ -123,6 +128,9 @@ let mktailcall sg e1 el = let cl = convert_rexpr_list el in prepend_seq !convert_accu (Stailcall(sg, c1, cl)) +let mkwhile expr body = + Sblock (Sloop (mkifthenelse expr body (Sexit O))) + (** Other constructors *) let intconst n = @@ -133,7 +141,7 @@ let andbool e1 e2 = let orbool e1 e2 = Rcondition(e1, intconst 1l, e2) -let exitnum n = nat_of_camlint(Int32.pred n) +let exitnum n = nat_of_camlint n let mkswitch expr (cases, dfl) = convert_accu := []; @@ -207,7 +215,6 @@ let mkmatch expr cases = %token COLON %token COMMA %token DEFAULT -%token DOLLAR %token ELSE %token EQUAL %token EQUALEQUAL @@ -222,6 +229,7 @@ let mkmatch expr cases = %token FLOATLIT %token FLOATOFINT %token FLOATOFINTU +%token GOTO %token GREATER %token GREATERF %token GREATERU @@ -233,10 +241,13 @@ let mkmatch expr cases = %token IDENT %token IF %token IN +%token INLINE %token INT +%token INT16 %token INT16S %token INT16U %token INT32 +%token INT8 %token INT8S %token INT8U %token INTLIT @@ -267,6 +278,7 @@ let mkmatch expr cases = %token RBRACE %token RBRACERBRACE %token RBRACKET +%token READONLY %token RETURN %token RPAREN %token SEMICOLON @@ -282,6 +294,8 @@ let mkmatch expr cases = %token TAILCALL %token VAR %token VOID +%token VOLATILE +%token WHILE /* Precedences from low to high */ @@ -323,11 +337,47 @@ global_declarations: ; global_declaration: - VAR STRINGLIT LBRACKET INTLIT RBRACKET + VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ { ($2, {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_info = (); gvar_init = List.rev $6; + gvar_readonly = $3; gvar_volatile = $4; } ) } ; +is_readonly: + /* empty */ { false } + | READONLY { true } + +is_volatile: + /* empty */ { false } + | VOLATILE { true } + +init_data_list: + /* empty */ { [] } + | init_data_list_1 { $1 } + ; + +init_data_list_1: + init_data { [$1] } + | init_data_list_1 COMMA init_data { $3 :: $1 } + ; + +init_data: + INT8 INTLIT { Init_int8 (coqint_of_camlint $2) } + | INT16 INTLIT { Init_int16 (coqint_of_camlint $2) } + | INT32 INTLIT { Init_int32 (coqint_of_camlint $2) } + | INT INTLIT { Init_int32 (coqint_of_camlint $2) } + | INTLIT { Init_int32 (coqint_of_camlint $1) } + | FLOAT32 FLOATLIT { Init_float32 ($2) } + | FLOAT64 FLOATLIT { Init_float64 ($2) } + | FLOAT FLOATLIT { Init_float64 ($2) } + | FLOATLIT { Init_float64 ($1) } + | LBRACKET INTLIT RBRACKET { Init_space (z_of_camlint $2) } + | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof ($3, coqint_of_camlint $1) } + ; + + proc_list: /* empty */ { [] } | proc_list proc { $2 :: $1 } @@ -345,13 +395,14 @@ proc: { let tmp = !temporaries in temporaries := []; temp_counter := 0; - ($1, Internal { fn_sig = $6; - fn_params = List.rev $3; - fn_vars = List.rev (tmp @ $9); - fn_stackspace = $8; - fn_body = $10 }) } + ($1, + 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, External(EF_external($2, $4))) } + { ($2, External(EF_external($2,$4))) } ; signature: @@ -408,6 +459,9 @@ stmt: { mkmatch $3 $6 } | 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 } ; stmts: @@ -525,3 +579,4 @@ type_: INT { Tint } | FLOAT { Tfloat } ; + diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 110e735..330c6c2 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -42,7 +42,7 @@ let rec precedence = function | Eload _ -> (15, RtoL) | Econdition _ -> (3, RtoL) -(* Naming idents. We assume we run after Cminorgen, which encoded idents. *) +(* Naming idents. We assume idents are encoded as in Cminorgen. *) let ident_name id = match id with @@ -185,7 +185,7 @@ let rec print_stmt p s = print_expr_list (true, el) print_sig sg | Scall(Some id, sg, e1, el) -> - fprintf p "@[%s =@ %a@,(@[%a@]);@] : @[%a@]" + fprintf p "@[%s =@ %a@,(@[%a@])@] : @[%a;@]" (ident_name id) print_expr e1 print_expr_list (true, el) @@ -245,9 +245,9 @@ let rec print_stmt p s = | Sreturn (Some e) -> fprintf p "return %a;" print_expr e | Slabel(lbl, s1) -> - fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1 + fprintf p "%s:@ %a" (ident_name lbl) print_stmt s1 (* wrong for Cminorgen output *) | Sgoto lbl -> - fprintf p "goto %s;" (extern_atom lbl) + fprintf p "goto %s;" (ident_name lbl) (* wrong for Cminorgen output *) (* Functions *) @@ -273,15 +273,50 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ " +let print_extfun p id ef = + fprintf p "@[extern @[\"%s\":@ %a@]@ " + (extern_atom id) print_sig (ef_sig ef) + let print_fundef p (id, fd) = match fd with | External ef -> - () (* Todo? *) + print_extfun p id ef | Internal f -> print_function p id f +let print_init_data p = function + | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i) + | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i) + | Init_int32 i -> fprintf p "%ld" (camlint_of_coqint i) + | Init_float32 f -> fprintf p "float32 %F" f + | Init_float64 f -> fprintf p "%F" f + | Init_space i -> fprintf p "[%ld]" (camlint_of_coqint i) + | Init_addrof(id,off) -> fprintf p "%ld(\"%s\")" (camlint_of_coqint off) (extern_atom id) + +let rec print_init_data_list p = function + | [] -> () + | [item] -> print_init_data p item + | item::rest -> + (print_init_data p item; + fprintf p ","; + print_init_data_list p rest) + +let print_globvar p gv = + if (gv.gvar_readonly) then + fprintf p "readonly "; + if (gv.gvar_volatile) then + fprintf p "volatile "; + fprintf p "{"; + print_init_data_list p gv.gvar_init; + fprintf p "}" + +let print_var p (id, gv) = + fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv + let print_program p prog = - fprintf p "@["; + fprintf p "@["; + List.iter (print_var p) prog.prog_vars; + fprintf p "@]@["; List.iter (print_fundef p) prog.prog_funct; fprintf p "@]@." diff --git a/backend/RTLgen.v b/backend/RTLgen.v index a9c8f97..28d2b06 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -319,7 +319,7 @@ Fixpoint add_vars (map: mapping) (names: list ident) Definition find_var (map: mapping) (name: ident) : mon reg := match PTree.get name map.(map_vars) with - | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil) + | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTXL name :: nil) | Some r => ret r end. -- cgit v1.2.3