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

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 <AST.ident> IDENT
+%token <string> IDENT
 %token IF
 %token IN
 %token INLINE
@@ -273,7 +328,7 @@ let mkmatch expr cases =
 %token STACK
 %token STAR
 %token STARF
-%token <AST.ident> STRINGLIT
+%token <string> 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 "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ "
-    (extern_atom id) print_sig (ef_sig ef)
+  fprintf p "@[<v 0>extern @[<hov 2>\"%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) ->