From 96e86f2a2daff433e7d86b3d84f0df35910d1a3f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 28 Aug 2024 09:14:57 +0200 Subject: [PATCH] Check that preprocessed source do not contain backslash-newline This is normally ensured by the preprocessor, as translation phases 1 and 2 (ISO C99, 5.1.1.2). However, these sequences could occur in hand-written .i files and confuse the CompCert lexer. Backslash-newline can also be written using trigraphs: `??/`-newline. An occurrence of this sequence in a preprocessed file is highly suspicious, so we reject it as well. --- cparser/Parse.ml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 607d8927af..caf4527319 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -55,6 +55,27 @@ let parse_string name text = Timeout_pr means that we ran for 2^50 steps. *) Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" +(* Quick checks that the preprocessed file already underwent + translation phases 1 and 2 (from ISO C99, 5.1.1.2), in particular + the removal of backslash-newline sequences. This can be assumed of + the output of a C preprocessor, but must be enforced for + hand-written .i files, since leftover backslash-newline sequences + can result in incorrect parsing. + Note that a backslash can also be written with a trigraph [??/]. *) + +let re_backslash_newline = Str.regexp_string "\\\n" +let re_trigraph_backslash_newline = Str.regexp_string "??/\n" + +let contains_regexp re text = + try ignore (Str.search_forward re text 0); true with Not_found -> false + +let check_preprocessed filename text = + if contains_regexp re_backslash_newline text then + Diagnostics.(error (file_loc filename) "illegal backslash-newline sequence in preprocessed source"); + if contains_regexp re_trigraph_backslash_newline text then + Diagnostics.(error (file_loc filename) "illegal ??/-newline sequence in preprocessed source"); + text + let preprocessed_file ?(unblock = false) ?(switch_norm = `Off) ?(struct_passing = false) @@ -70,6 +91,8 @@ let preprocessed_file ?(unblock = false) speed increase: "make -C test" speeds up by 3 seconds out of 40 on my machine. *) read_file sourcefile + |> check_preprocessed name + |> check_errors |> Timing.time2 "Parsing" parse_string name |> Timing.time "Elaboration" Elab.elab_file |> check_errors