From efc51afc7c8298ecd3b511b8d0faf9ff6d2df22e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 27 Sep 2022 12:04:31 +0200 Subject: Revised passing of options to `Parse.preprocessed_file` Instead of passing a string that encodes the optional source-to-source transformations to perform, just pass one optional, named argument for each transformation. It is clearer and easier to extend this way. --- cparser/Parse.ml | 45 ++++++++++++++++----------------------------- cparser/Parse.mli | 17 ++++++++++++----- driver/Frontend.ml | 12 +++++------- 3 files changed, 33 insertions(+), 41 deletions(-) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index a54af0cc..c0419301 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -16,33 +16,16 @@ (* Entry point for the library: parse, elaborate, and transform *) -module CharSet = Set.Make(struct type t = char let compare = compare end) - -let transform_program t p = - let run_pass pass flag p = - if CharSet.mem flag t then begin - let p = pass p in - Diagnostics.check_errors (); - p - end else - p - in - p - |> run_pass Unblock.program 'b' - |> run_pass PackedStructs.program 'p' - |> run_pass StructPassing.program 's' - |> Rename.program - -let parse_transformations s = - let t = ref CharSet.empty in - let set s = String.iter (fun c -> t := CharSet.add c !t) s in - String.iter - (function 'b' -> set "b" - | 's' -> set "s" - | 'p' -> set "bp" - | _ -> ()) - s; - !t +let transform_program ~unblock ~struct_passing ~packed_structs p = + let run_pass pass p = + let p' = pass p in Diagnostics.check_errors (); p' in + let run_opt_pass pass flag p = + if flag then run_pass pass p else p in + p + |> run_opt_pass Unblock.program (unblock || packed_structs) + |> run_opt_pass PackedStructs.program packed_structs + |> run_opt_pass StructPassing.program struct_passing + |> Rename.program let read_file sourcefile = let ic = open_in_bin sourcefile in @@ -65,7 +48,10 @@ 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" -let preprocessed_file transfs name sourcefile = +let preprocessed_file ?(unblock = false) + ?(struct_passing = false) + ?(packed_structs = false) + name sourcefile = Diagnostics.reset(); let check_errors x = Diagnostics.check_errors(); x in @@ -79,5 +65,6 @@ let preprocessed_file transfs name sourcefile = |> Timing.time2 "Parsing" parse_string name |> Timing.time "Elaboration" Elab.elab_file |> check_errors - |> Timing.time2 "Emulations" transform_program (parse_transformations transfs) + |> Timing.time "Emulations" + (transform_program ~unblock ~struct_passing ~packed_structs) |> check_errors diff --git a/cparser/Parse.mli b/cparser/Parse.mli index c406d96c..7b33cc5b 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -16,8 +16,15 @@ (* Entry point for the library: parse, elaborate, and transform *) -val preprocessed_file: string -> string -> string -> C.program - -(* first arg: desired transformations - second arg: source file name before preprocessing - third arg: file after preprocessing *) +val preprocessed_file: + ?unblock: bool -> + ?struct_passing: bool -> + ?packed_structs: bool -> + string -> string -> C.program + (** [preprocessed_file filename sourcetext] performs parsing, + elaboration, and optional source-to-source transformations. + [filename] is the name of the source file, for error messages. + [sourcetext] is the text of the source file after preprocessing. + The optional arguments indicate which source-to-source + transformations to perform. They default to [false] (don't perform). + *) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 5d45306d..5132f730 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -79,14 +79,12 @@ let parse_c_file sourcename ifile = Debug.init_compile_unit sourcename; Sections.initialize(); CPragmas.reset(); - (* Simplification options *) - let simplifs = - "b" (* blocks: mandatory *) - ^ (if !option_fstruct_passing then "s" else "") - ^ (if !option_fpacked_structs then "p" else "") - in (* Parsing and production of a simplified C AST *) - let ast = Parse.preprocessed_file simplifs sourcename ifile in + let ast = Parse.preprocessed_file + ~unblock: true + ~struct_passing: !option_fstruct_passing + ~packed_structs: !option_fpacked_structs + sourcename ifile in (* Save C AST if requested *) Cprint.print_if ast; (* Conversion to Csyntax *) -- cgit