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/CMparser.mly | 75 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 65 insertions(+), 10 deletions(-) (limited to 'backend/CMparser.mly') 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 } ; + -- cgit v1.2.3