diff options
| -rw-r--r-- | cfrontend/CPragmas.ml | 80 | ||||
| -rw-r--r-- | lib/Tokenize.mli | 33 | ||||
| -rw-r--r-- | lib/Tokenize.mll | 45 |
3 files changed, 103 insertions, 55 deletions
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 3c0c9f1..c074632 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -41,10 +41,12 @@ let process_section_pragma classname istring ustring addrmode accmode = let re_c_ident = Str.regexp "[A-Za-z_][A-Za-z_0-9]*$" let process_use_section_pragma classname id = - if not (Str.string_match re_c_ident id 0) then - C2C.error (sprintf "bad identifier `%s' in #pragma use_section" id); - if not (Sections.use_section_for (intern_string id) classname) then - C2C.error (sprintf "unknown section name `%s'" classname) + if id = "," || id = ";" then () else begin + if not (Str.string_match re_c_ident id 0) then + C2C.error (sprintf "bad identifier `%s' in #pragma use_section" id); + if not (Sections.use_section_for (intern_string id) classname) then + C2C.error (sprintf "unknown section name `%s'" classname) + end (* #pragma reserve_register *) @@ -58,59 +60,27 @@ let process_reserve_register_pragma name = else C2C.error "cannot reserve this register (not a callee-save)" -(* Parsing of pragmas using regexps *) - -let re_start_pragma_section = Str.regexp "section\\b" - -let re_pragma_section = Str.regexp( - "section[ \t]+" -^ "\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+" (* class_name *) -^ "\"\\([^\"]*\\)\"?[ \t]*" (* istring *) -^ "\"\\([^\"]*\\)\"?[ \t]*" (* ustring *) -^ "\\([a-zA-Z-]+\\)?[ \t]*" (* addressing mode *) -^ "\\([RWXON]*\\)" (* access mode *) -) - -let re_start_pragma_use_section = Str.regexp "use_section\\b" - -let re_pragma_use_section = Str.regexp - "use_section[ \t]+\ - \\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\ - \\(.*\\)$" - -let re_split_idents = Str.regexp "[ \t,]+" - -let re_start_pragma_reserve_register = Str.regexp "reserve_register\\b" - -let re_pragma_reserve_register = Str.regexp - "reserve_register[ \t]+\\([A-Za-z0-9]+\\)" +(* Parsing of pragmas *) let process_pragma name = - if Str.string_match re_pragma_section name 0 then begin - process_section_pragma - (Str.matched_group 1 name) (* classname *) - (Str.matched_group 2 name) (* istring *) - (Str.matched_group 3 name) (* ustring *) - (Str.matched_group 4 name) (* addrmode *) - (Str.matched_group 5 name); (* accmode *) - true - end else if Str.string_match re_start_pragma_section name 0 then - (C2C.error "ill-formed `section' pragma"; true) - else if Str.string_match re_pragma_use_section name 0 then begin - let classname = Str.matched_group 1 name - and idents = Str.matched_group 2 name in - let identlist = Str.split re_split_idents idents in - if identlist = [] then C2C.warning "vacuous `use_section' pragma"; - List.iter (process_use_section_pragma classname) identlist; - true - end else if Str.string_match re_start_pragma_use_section name 0 then begin - C2C.error "ill-formed `use_section' pragma"; true - end else if Str.string_match re_pragma_reserve_register name 0 then begin - process_reserve_register_pragma (Str.matched_group 1 name); true - end else if Str.string_match re_start_pragma_reserve_register name 0 then begin - C2C.error "ill-formed `reserve_register' pragma"; true - end else - false + match Tokenize.string name with + | ["section"; classname; istring; ustring; addrmode; accmode] -> + process_section_pragma classname istring ustring addrmode accmode; + true + | "section" :: _ -> + C2C.error "ill-formed `section' pragma"; true + | "use_section" :: classname :: identlist -> + if identlist = [] then C2C.warning "vacuous `use_section' pragma"; + List.iter (process_use_section_pragma classname) identlist; + true + | "use_section" :: _ -> + C2C.error "ill-formed `use_section' pragma"; true + | ["reserve_register"; reg] -> + process_reserve_register_pragma reg; true + | "reserve_register" :: _ -> + C2C.error "ill-formed `reserve_register' pragma"; true + | _ -> + false let initialize () = C2C.process_pragma_hook := process_pragma diff --git a/lib/Tokenize.mli b/lib/Tokenize.mli new file mode 100644 index 0000000..a9f22c4 --- /dev/null +++ b/lib/Tokenize.mli @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Parse a string as a list of tokens *) + +val string: string -> string list + (** [Tokenize.string s] decomposes [s] into a list of tokens. + Whitespace separates tokens. The following substrings + constitute tokens: + - A string enclosed in double quotes. Within the string, + the escape sequences '\t' '\n' '\"' and '\\' are recognized. + The token value is the contents of the string without the + enclosing double quotes. + - A string enclosed in single quotes. No escape sequences are + recognized. The token value is the contents of the string without the + enclosing single quotes. + - A sequence of letters, digits, or the [_], [$], [-] and [.] + characters. [-] and [.] cannot appear as the first character. + - Any other non-whitespace character is treated as a separate token + of length 1. + *) diff --git a/lib/Tokenize.mll b/lib/Tokenize.mll new file mode 100644 index 0000000..422068b --- /dev/null +++ b/lib/Tokenize.mll @@ -0,0 +1,45 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Parse a string as a list of tokens *) + +let identstart = [ '0'-'9' 'A'-'Z' 'a'-'z' '$' '_' ] +let identcont = [ '0'-'9' 'A'-'Z' 'a'-'z' '$' '_' '-' '.' ] + +rule tokenize acc = parse + | eof { List.rev acc } + | [' ' '\t' '\n'] + { tokenize acc lexbuf } + | "\"" { tok_dquote acc (Buffer.create 16) lexbuf } + | "'" { tok_squote acc (Buffer.create 16) lexbuf } + | (identstart identcont*) as s + { tokenize (s :: acc) lexbuf } + | _ as c { tokenize (String.make 1 c :: acc) lexbuf } + +and tok_dquote acc buf = parse + | "\"" | eof { tokenize (Buffer.contents buf :: acc) lexbuf } + | "\\t" { Buffer.add_char buf '\t'; tok_dquote acc buf lexbuf } + | "\\n" { Buffer.add_char buf '\n'; tok_dquote acc buf lexbuf } + | "\\" ([ '\\' '\"' ] as c) + { Buffer.add_char buf c; tok_dquote acc buf lexbuf } + | _ as c { Buffer.add_char buf c; tok_dquote acc buf lexbuf } + +and tok_squote acc buf = parse + | "\'" | eof { tokenize (Buffer.contents buf :: acc) lexbuf } + | _ as c { Buffer.add_char buf c; tok_squote acc buf lexbuf } + +{ +let string s = + tokenize [] (Lexing.from_string s) +} |