aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-27 12:04:31 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-27 12:04:31 +0200
commitefc51afc7c8298ecd3b511b8d0faf9ff6d2df22e (patch)
tree232bf0f11a5fbc6a8f1c219f1234fad452a38b80
parenta1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 (diff)
downloadcompcert-efc51afc7c8298ecd3b511b8d0faf9ff6d2df22e.tar.gz
compcert-efc51afc7c8298ecd3b511b8d0faf9ff6d2df22e.zip
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.
-rw-r--r--cparser/Parse.ml45
-rw-r--r--cparser/Parse.mli17
-rw-r--r--driver/Frontend.ml12
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 *)