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 From dfc6b66ec21e148d29b2a6e8b5d77873a0a47511 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Oct 2022 15:20:21 +0200 Subject: Unblock: never put debug info before a label This ensures that normalized switch statements remain normalized. However, if the label and the labeled statement are on different lines, add an extra line directive corresponding to the label before the labeled statement. --- cparser/Unblock.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 4b1f2262..71d800c3 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -215,14 +215,12 @@ let debug_scope ctx = debug_annot 6L (empty_string :: List.rev_map integer_const ctx) (* Add line number debug annotation if the line number changes. - Labels are ignored since the code before the label can become - unreachable. Add scope debug annotation regardless. *) + Add scope debug annotation regardless. *) - -let add_lineno ?(label=false) ctx prev_loc this_loc s = +let add_lineno ctx prev_loc this_loc s = if !Clflags.option_g then sseq no_loc (debug_scope ctx) - (if this_loc <> prev_loc && this_loc <> no_loc && not label + (if this_loc <> prev_loc && this_loc <> no_loc then sseq no_loc (debug_lineno this_loc) s else s) else s @@ -295,12 +293,15 @@ let rec unblock_stmt env ctx ploc s = {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env ctx s.sloc s1)} | Slabeled(lbl, s1) -> - let loc,label = if s.sloc <> s1.sloc then - s.sloc,false (* Label and code are on different lines *) - else - ploc,true in - add_lineno ~label:label ctx ploc s.sloc - {s with sdesc = Slabeled(lbl, unblock_stmt env ctx loc s1)} + (* Do not put debug info before label, only after. *) + (* If the label and the statement are on different lines, + put extra debug info before s1, referring to the line of the label. *) + let s1' = + if s.sloc <> s1.sloc then + add_lineno ctx ploc s.sloc (unblock_stmt env ctx s.sloc s1) + else + unblock_stmt env cts ploc s1 in + {s with sdesc = Slabeled(lbl, s1')} | Sgoto lbl -> add_lineno ctx ploc s.sloc s | Sreturn None -> -- cgit From a1dabb4792446538cce24eb87bcd3ccb3c09f18b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 27 Sep 2022 12:31:07 +0200 Subject: Handle unstructured 'switch' statements such as Duff's device - New elaboration pass: SwitchNorm - recognizes structured 'switch' statements and puts them in a normalized form; - if selected, transforms unstructured 'switch' statements into a structured switch with goto actions + the original switch body with appropriate labels and gotos. - C2C treatment of 'switch' statements is simplified accordingly. - New language support option `-funstructured-switch`. - Some tests were added (test/regression/switch3.c). --- cfrontend/C2C.ml | 102 ++++------------------ cparser/Parse.ml | 16 +++- cparser/Parse.mli | 5 +- cparser/SwitchNorm.ml | 173 ++++++++++++++++++++++++++++++++++++++ cparser/SwitchNorm.mli | 28 +++++++ cparser/Unblock.ml | 2 +- driver/Clflags.ml | 1 + driver/CommonOptions.ml | 4 +- driver/Frontend.ml | 12 +-- test/regression/Makefile | 2 +- test/regression/Results/switch3 | 10 +++ test/regression/switch3.c | 182 ++++++++++++++++++++++++++++++++++++++++ 12 files changed, 439 insertions(+), 98 deletions(-) create mode 100644 cparser/SwitchNorm.ml create mode 100644 cparser/SwitchNorm.mli create mode 100644 test/regression/Results/switch3 create mode 100644 test/regression/switch3.c diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 89b9139c..2ea38ddd 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1028,61 +1028,6 @@ let convertAsm loc env txt outputs inputs clobber = | None -> e | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e) -(* Separate the cases of a switch statement body *) - -type switchlabel = - | Case of C.exp - | Default - -type switchbody = - | Label of switchlabel - | Stmt of C.stmt - -let rec flattenSwitch = function - | {sdesc = C.Sseq(s1, s2)} -> - flattenSwitch s1 @ flattenSwitch s2 - | {sdesc = C.Slabeled(C.Scase(e, _), s1)} -> - Label(Case e) :: flattenSwitch s1 - | {sdesc = C.Slabeled(C.Sdefault, s1)} -> - Label Default :: flattenSwitch s1 - | {sdesc = C.Slabeled(C.Slabel lbl, s1); sloc = loc} -> - Stmt {sdesc = C.Slabeled(C.Slabel lbl, Cutil.sskip); sloc = loc} - :: flattenSwitch s1 - | s -> - [Stmt s] - -let rec groupSwitch = function - | [] -> - (Cutil.sskip, []) - | Label case :: rem -> - let (fst, cases) = groupSwitch rem in - (Cutil.sskip, (case, fst) :: cases) - | Stmt s :: rem -> - let (fst, cases) = groupSwitch rem in - (Cutil.sseq s.sloc s fst, cases) - -(* Test whether the statement contains case and give an *) -let rec contains_case s = - match s.sdesc with - | C.Sskip - | C.Sdo _ - | C.Sbreak - | C.Scontinue - | C.Sswitch _ (* Stop at a switch *) - | C.Sgoto _ - | C.Sreturn _ - | C.Sdecl _ - | C.Sasm _ -> () - | C.Sseq (s1,s2) - | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 - | C.Swhile (_,s1) - | C.Sdowhile (s1,_) -> contains_case s1 - | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 - | C.Slabeled(C.Scase _, _) -> - unsupported "'case' statement not in 'switch' statement" - | C.Slabeled(_,s) -> contains_case s - | C.Sblock b -> List.iter contains_case b - (** Annotations for line numbers *) (** Statements *) @@ -1122,20 +1067,8 @@ let rec convertStmt env s = | C.Scontinue -> Csyntax.Scontinue | C.Sswitch(e, s1) -> - let (init, cases) = groupSwitch (flattenSwitch s1) in - let rec init_debug s = - match s.sdesc with - | Sseq (a,b) -> init_debug a && init_debug b - | C.Sskip -> true - | _ -> Cutil.is_debug_stmt s in - if init.sdesc <> C.Sskip && not (init_debug init) then - begin - warning Diagnostics.Unnamed "ignored code at beginning of 'switch'"; - contains_case init - end; let te = convertExpr env e in - swrap (Ctyping.sswitch te - (convertSwitch env (is_int64 env e.etyp) cases)) + swrap (Ctyping.sswitch te (convertSwitch env (is_int64 env e.etyp) s1)) | C.Slabeled(C.Slabel lbl, s1) -> Csyntax.Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> @@ -1158,23 +1091,24 @@ let rec convertStmt env s = Csyntax.Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function - | [] -> + | {sdesc = C.Sskip} -> LSnil - | (lbl, s) :: rem -> - updateLoc s.sloc; - let lbl' = - match lbl with - | Default -> - None - | Case e -> - match Ceval.integer_expr env e with - | None -> unsupported "expression is not an integer constant expression"; - None - | Some v -> Some (if is_64 - then Z.of_uint64 v - else Z.of_uint32 (Int64.to_int32 v)) - in - LScons(lbl', convertStmt env s, convertSwitch env is_64 rem) + | {sdesc = C.Slabeled(lbl, s)} -> + convertSwitchCase env is_64 lbl s LSnil + | {sdesc = C.Sseq ({sdesc = C.Slabeled(lbl, s)}, rem)} -> + convertSwitchCase env is_64 lbl s (convertSwitch env is_64 rem) + | _ -> + assert false + +and convertSwitchCase env is_64 lbl s k = + let lbl' = + match lbl with + | C.Sdefault -> + None + | C.Scase(e, v) -> + Some (if is_64 then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) + | _ -> assert false in + LScons(lbl', convertStmt env s, k) (** Function definitions *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c0419301..607d8927 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -16,13 +16,20 @@ (* Entry point for the library: parse, elaborate, and transform *) -let transform_program ~unblock ~struct_passing ~packed_structs p = +let transform_program ~unblock ~switch_norm ~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 + if flag then run_pass pass p else p + and run_opt_pass3 pass flag p = + match flag with + | `Off -> p + | `Partial -> run_pass (pass false) p + | `Full -> run_pass (pass true) p in + let unblock = unblock || switch_norm <> `Off || packed_structs in p - |> run_opt_pass Unblock.program (unblock || packed_structs) + |> run_opt_pass Unblock.program unblock + |> run_opt_pass3 SwitchNorm.program switch_norm |> run_opt_pass PackedStructs.program packed_structs |> run_opt_pass StructPassing.program struct_passing |> Rename.program @@ -49,6 +56,7 @@ let parse_string name text = Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" let preprocessed_file ?(unblock = false) + ?(switch_norm = `Off) ?(struct_passing = false) ?(packed_structs = false) name sourcefile = @@ -66,5 +74,5 @@ let preprocessed_file ?(unblock = false) |> Timing.time "Elaboration" Elab.elab_file |> check_errors |> Timing.time "Emulations" - (transform_program ~unblock ~struct_passing ~packed_structs) + (transform_program ~unblock ~switch_norm ~struct_passing ~packed_structs) |> check_errors diff --git a/cparser/Parse.mli b/cparser/Parse.mli index 7b33cc5b..a37bd0e0 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -18,6 +18,7 @@ val preprocessed_file: ?unblock: bool -> + ?switch_norm: [`Off | `Partial | `Full] -> ?struct_passing: bool -> ?packed_structs: bool -> string -> string -> C.program @@ -26,5 +27,5 @@ val preprocessed_file: [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). - *) + transformations to perform. They default to [false] or [`Off] + (do not perform). *) diff --git a/cparser/SwitchNorm.ml b/cparser/SwitchNorm.ml new file mode 100644 index 00000000..2493c63d --- /dev/null +++ b/cparser/SwitchNorm.ml @@ -0,0 +1,173 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) +(* *) +(* *********************************************************************) + +(* Normalization of structured "switch" statements + and emulation of unstructured "switch" statements (e.g. Duff's device) *) + +(* Assumes: code without blocks + Produces: code without blocks and with normalized "switch" statements *) + +(* A normalized switch has the following form: + Sswitch(e, Sseq (Slabeled(lbl1, case1), + Sseq (... + Sseq (Slabeled(lblN,caseN), Sskip) ...))) +*) + +open Printf +open C +open Cutil + +let support_unstructured = ref false + +type switchlabel = + | Case of exp * int64 + | Default + +type switchbody = + | Label of switchlabel * location + | Stmt of stmt + +let rec flatten_switch = function + | {sdesc = Sseq(s1, s2)} :: rem -> + flatten_switch (s1 :: s2 :: rem) + | {sdesc = Slabeled(Scase(e, n), s1); sloc = loc} :: rem -> + Label(Case(e, n), loc) :: flatten_switch (s1 :: rem) + | {sdesc = Slabeled(Sdefault, s1); sloc = loc} :: rem -> + Label(Default, loc) :: flatten_switch (s1 :: rem) + | {sdesc = Slabeled(Slabel lbl, s1); sloc = loc} :: rem -> + Stmt {sdesc = Slabeled(Slabel lbl, Cutil.sskip); sloc = loc} + :: flatten_switch (s1 :: rem) + | s :: rem -> + Stmt s :: flatten_switch rem + | [] -> + [] + +let rec group_switch = function + | [] -> + (Cutil.sskip, []) + | Label(case, loc) :: rem -> + let (fst, cases) = group_switch rem in + (Cutil.sskip, (case, loc, fst) :: cases) + | Stmt s :: rem -> + let (fst, cases) = group_switch rem in + (Cutil.sseq s.sloc s fst, cases) + +let label_of_switchlabel = function + | Case(e, n) -> Scase(e, n) + | Default -> Sdefault + +let make_slabeled (l, loc, s) = + { sdesc = Slabeled(label_of_switchlabel l, s); sloc = loc } + +let make_sequence sl = + List.fold_right (Cutil.sseq no_loc) sl Cutil.sskip + +let make_normalized_switch e cases = + Sswitch(e, make_sequence (List.map make_slabeled cases)) + +let rec all_cases accu s = + match s.sdesc with + | Sseq(s1, s2) -> all_cases (all_cases accu s1) s2 + | Sif(_, s1, s2) -> all_cases (all_cases accu s1) s2 + | Swhile(_, s1) -> all_cases accu s1 + | Sdowhile(s1, _) -> all_cases accu s1 + | Sfor(s1, _, s2, s3) -> all_cases (all_cases (all_cases accu s1) s2) s3 + | Sswitch(_, _) -> accu + | Slabeled(Scase(e, n), s1) -> all_cases (Case(e, n) :: accu) s1 + | Slabeled(Sdefault, s1) -> all_cases (Default :: accu) s1 + | Slabeled(Slabel _, s1) -> all_cases accu s1 + | Sblock _ -> assert false + | _ -> accu + +let substitute_cases case_table body end_label = + let sub = Hashtbl.create 32 in + List.iter + (fun (case, lbl) -> Hashtbl.add sub case (Slabel lbl)) + case_table; + let transf_label = function + | Scase(e, n) -> + (try Hashtbl.find sub (Case(e, n)) with Not_found -> assert false) + | Sdefault -> + (try Hashtbl.find sub Default with Not_found -> assert false) + | Slabel _ as lbl -> lbl in + let rec transf inloop s = + {s with sdesc = + match s.sdesc with + | Sseq(s1, s2) -> Sseq(transf inloop s1, transf inloop s2) + | Sif(e, s1, s2) -> Sif(e, transf inloop s1, transf inloop s2) + | Swhile(e, s1) -> Swhile(e, transf true s1) + | Sdowhile(s1, e) -> Sdowhile(transf true s1, e) + | Sfor(s1, e, s2, s3) -> + Sfor(transf inloop s1, e, transf inloop s2, transf true s3) + | Sbreak -> if inloop then Sbreak else Sgoto end_label + | Slabeled(lbl, s1) -> Slabeled(transf_label lbl, transf inloop s1) + | Sblock _ -> assert false + | sd -> sd } + in transf false body + +let new_label = ref 0 + +let gen_label () = incr new_label; sprintf "@%d" !new_label + +let normalize_switch loc e body = + let (init, cases) = [body] |> flatten_switch |> group_switch + and allcases = List.rev (all_cases [] body) in + if init.sdesc = Sskip && List.length cases = List.length allcases then + (* This is a structured switch *) + make_normalized_switch e cases + else begin + (* This switch needs to be converted *) + if not !support_unstructured then + Diagnostics.error loc + "unsupported feature: non-structured 'switch' statement \ + (consider adding option [-funstructured-switch])"; + let case_table = List.map (fun case -> (case, gen_label())) allcases in + let end_lbl = gen_label() in + let newbody = substitute_cases case_table body end_lbl in + let goto_case (case, lbl) = + (case, no_loc, {sdesc = Sgoto lbl; sloc = no_loc}) in + let case_table' = + if List.mem_assoc Default case_table + then case_table + else (Default, end_lbl) :: case_table in + Sseq({sdesc = make_normalized_switch e (List.map goto_case case_table'); + sloc = loc}, + sseq no_loc newbody + {sdesc = Slabeled(Slabel end_lbl, sskip); sloc = no_loc}) + end + +let rec transform_stmt s = + { s with sdesc = + match s.sdesc with + | Sseq(s1, s2) -> Sseq(transform_stmt s1, transform_stmt s2) + | Sif(e, s1, s2) -> Sif(e, transform_stmt s1, transform_stmt s2) + | Swhile(e, s1) -> Swhile(e, transform_stmt s1) + | Sdowhile(s1, e) -> Sdowhile(transform_stmt s1, e) + | Sfor(s1, e, s2, s3) -> + Sfor(transform_stmt s1, e, transform_stmt s2, transform_stmt s3) + | Sswitch(e, s1) -> normalize_switch s.sloc e (transform_stmt s1) + | Slabeled(lbl, s1) -> Slabeled(lbl, transform_stmt s1) + | Sblock sl -> Sblock(List.map transform_stmt sl) + | sd -> sd} + +let transform_fundef env loc fd = + { fd with fd_body = transform_stmt fd.fd_body } + +(* Entry point *) + +let program unstructured p = + support_unstructured := unstructured; + Transform.program ~fundef: transform_fundef p diff --git a/cparser/SwitchNorm.mli b/cparser/SwitchNorm.mli new file mode 100644 index 00000000..88e50dcd --- /dev/null +++ b/cparser/SwitchNorm.mli @@ -0,0 +1,28 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) +(* *) +(* *********************************************************************) + +(* Normalization of structured "switch" statements + and emulation of unstructured "switch" statements (e.g. Duff's device) *) + +(* Assumes: nothing + Produces: code with normalized "switch" statements *) + +(* A normalized switch has the following form: + Sswitch(e, Sblock [ Slabeled(lbl1, case1); ... + Slabeled(lblN,caseN) ]) +*) + +val program: bool -> C.program -> C.program diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 71d800c3..32e09399 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -300,7 +300,7 @@ let rec unblock_stmt env ctx ploc s = if s.sloc <> s1.sloc then add_lineno ctx ploc s.sloc (unblock_stmt env ctx s.sloc s1) else - unblock_stmt env cts ploc s1 in + unblock_stmt env ctx ploc s1 in {s with sdesc = Slabeled(lbl, s1')} | Sgoto lbl -> add_lineno ctx ploc s.sloc s diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8fbda738..995be34d 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -20,6 +20,7 @@ let option_fstruct_passing = ref false let option_fvararg_calls = ref true let option_funprototyped = ref true let option_fpacked_structs = ref false +let option_funstructured_switch = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index 2a3bd740..773c5c7d 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -35,7 +35,7 @@ let version_options tool_name = let all_language_support_options = [ option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; - option_fpacked_structs; option_finline_asm + option_fpacked_structs; option_finline_asm; option_funstructured_switch ] let f_opt name ref = @@ -65,6 +65,7 @@ let language_support_options = @ f_opt "struct-passing" option_fstruct_passing @ f_opt "vararg-calls" option_fvararg_calls @ f_opt "unprototyped" option_funprototyped + @ f_opt "unstructured-switch" option_funstructured_switch @ f_opt "packed-structs" option_fpacked_structs @ f_opt "inline-asm" option_finline_asm @@ -78,6 +79,7 @@ let language_support_help = -fstruct-return Like -fstruct-passing (deprecated) -fvararg-calls Support calls to variable-argument functions [on] -funprototyped Support calls to old-style functions without prototypes [on] + -funstructured-switch Support non-structured 'switch' statements [off] -fpacked-structs Emulate packed structs [off] -finline-asm Support inline 'asm' statements [off] -fall Activate all language support options above diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 5132f730..c8131662 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -80,11 +80,13 @@ let parse_c_file sourcename ifile = Sections.initialize(); CPragmas.reset(); (* Parsing and production of a simplified C AST *) - let ast = Parse.preprocessed_file - ~unblock: true - ~struct_passing: !option_fstruct_passing - ~packed_structs: !option_fpacked_structs - sourcename ifile in + let ast = + Parse.preprocessed_file + ~unblock: true + ~switch_norm: (if !option_funstructured_switch then `Full else `Partial) + ~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 *) diff --git a/test/regression/Makefile b/test/regression/Makefile index 536b7264..0cc0fa3f 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -25,7 +25,7 @@ TESTS=int32 int64 floats floats-basics floats-lit \ TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t bitfields10 \ builtins-common builtins-$(ARCH) packedstruct1 packedstruct2 alignas \ - varargs1 varargs2 varargs3 sections alias aligned + varargs1 varargs2 varargs3 sections alias aligned switch3 # Can run, both in compiled mode and in interpreter mode, # but produce processor-dependent results, so no reference output in Results diff --git a/test/regression/Results/switch3 b/test/regression/Results/switch3 new file mode 100644 index 00000000..8d8b09b8 --- /dev/null +++ b/test/regression/Results/switch3 @@ -0,0 +1,10 @@ +0123456789AB +\(ab\$cd\) +(ab\$cd) +abcccdee +10001 10004 20002 20022 30007 30008 +30008 30007 20022 20002 10004 10001 +30007 30008 20002 20022 10001 10004 +0 1 1 2 L1 L2 3 L2 4 3 L2 +5 55 555 +60Y 61Y 6XY diff --git a/test/regression/switch3.c b/test/regression/switch3.c new file mode 100644 index 00000000..f411a3fb --- /dev/null +++ b/test/regression/switch3.c @@ -0,0 +1,182 @@ +#include +#include + +/* Unstructured switch statements */ + +/* Duff's device */ + +void send(char * to, char * from, int count) +{ + register int n = (count + 7) / 8; + switch (count % 8) { + case 0: do { *to++ = *from++; + case 7: *to++ = *from++; + case 6: *to++ = *from++; + case 5: *to++ = *from++; + case 4: *to++ = *from++; + case 3: *to++ = *from++; + case 2: *to++ = *from++; + case 1: *to++ = *from++; + } while (--n > 0); + } +} + +/* OpenBSD, usr.bin/locale */ + +void quotestring(char * value, int double_quoted) +{ + char c; + while ((c = *value++) != '\0') + switch (c) { + case ' ': case '\t': case '\n': case '\'': + case '(': case ')': case '<': case '>': + case '&': case ';': case '|': case '~': + if (!double_quoted) + case '"': case '\\': case '$': case '`': + putchar('\\'); + default: + putchar(c); + break; + } +} + +/* Simon Tatham's coroutines */ + +int nextchar(void) +{ + static unsigned char input[] = { + 'a', 'b', 0xFF, 3, 'c', 'd', 0xFF, 2, 'e', '\n', 0 + }; + static unsigned char * next = input; + if (*next == 0) + return EOF; + else + return *next++; +} + +#define crBegin static int state=0; switch(state) { case 0: +#define crReturn(x) do { state=__LINE__; return x; \ + case __LINE__:; } while (0) +#define crFinish } + +int decompressor(void) { + static int c, len; + crBegin; + while (1) { + c = nextchar(); + if (c == EOF) + break; + if (c == 0xFF) { + len = nextchar(); + c = nextchar(); + while (len--) + crReturn(c); + } else + crReturn(c); + } + crReturn(EOF); + crFinish; +} + +/* Pigeon's device */ + +static enum { REVDFWDT, FORWARD, REVERSE } sorting_mode; + +#define DAYOF(stamp) ((stamp) / 10000) +#define TIMEOF(stamp) ((stamp) % 10000) + +static inline int intcmp(unsigned int x, unsigned int y) +{ + if (x < y) return -1; + if (x > y) return 1; + return 0; +} + +int lfdcmp(const void *a, const void *b) { + unsigned int ta = *((unsigned int *) a); + unsigned int tb = *((unsigned int *) b); + /* Isn't C a wonderful language? */ + switch (sorting_mode) { + case REVDFWDT: if (DAYOF(ta) == DAYOF(tb)) { + case FORWARD : return intcmp(ta, tb); + } else { + case REVERSE : return intcmp(tb, ta); + } + } + return 0; +} + +void testpigeon(int mode) +{ + unsigned int data[6] = { + 10001, 10004, 20022, 20002, 30008, 30007 + }; + sorting_mode = mode; + qsort(data, 6, sizeof(unsigned int), lfdcmp); + for (int i = 0; i < 6; i++) printf("%5u ", data[i]); + printf("\n"); +} + +/* Delicate cases: unstructured switch containing + early break + loop w/ break + regular switch +*/ + +void torture(int a, int b) +{ + switch(a) { + L1: printf("L1 "); /*fallthrough*/ + L2: printf("L2 "); break; + case 0: + printf("0 "); /*fallthrough*/ + case 1: + printf("1 "); break; + case 2: + printf("2 "); goto L1; + case 3: + L3: + printf("3 "); goto L2; + case 4: + printf("4 "); goto L3; + case 5: + while (1) { printf("5"); b--; if (b <= 0) { printf(" "); break; }}; + break; + case 6: + switch (b) { + case 1: printf("60"); break; + case 2: printf("61"); break; + default: printf("6X"); + } + printf("Y "); + break; + default: + printf("? "); + } +} + +int main() +{ + char dest[16]; + send(dest, "0123456789AB", 13); + printf("%s\n", dest); + + quotestring("(ab$cd)", 0); putchar('\n'); + quotestring("(ab$cd)", 1); putchar('\n'); + + char c; + while ((c = decompressor()) != EOF) putchar(c); + + testpigeon(FORWARD); + testpigeon(REVERSE); + testpigeon(REVDFWDT); + + torture(0, 0); torture(1, 0); torture(2, 0); torture(3, 0); torture(4, 0); + printf("\n"); + for (int b = 1; b <= 3; b++) torture(5, b); + printf("\n"); + for (int b = 1; b <= 3; b++) torture(6, b); + printf("\n"); + + return 0; +} -- cgit From 8eadd08af4602de399a94313d4fb2b8980f7ceb0 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Thu, 3 Nov 2022 14:27:34 +0100 Subject: Update man-page for `-funstructured-switch` (also for new `-std` option, `-finput-charset` and other small fixes) --- doc/ccomp.1 | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/doc/ccomp.1 b/doc/ccomp.1 index edae57e1..4164b7c3 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -110,7 +110,7 @@ Pass comma separated arguments in to the preprocessor. Pass argument to the preprocessor. . .TP -.BR \-C ", " \-CC ", " \-idirafter ", " \-imacros ", " \-iquote ", " \-isystem ", " \-M ", " \-MF ", " \-MG ", " \-MM ", " \-MP ", " \-MQ ", " \-MT ", " \-nostdinc ", " \-P +.BR \-C ", " \-CC ", " \-finput-charset ", " \-idirafter ", " \-imacros ", " \-iquote ", " \-isystem ", " \-M ", " \-MF ", " \-MG ", " \-MM ", " \-MP ", " \-MQ ", " \-MT ", " \-nostdinc ", " \-P For GNU backends these options are recognized by CompCert and passed through to the preprocessor. . .SS @@ -238,12 +238,12 @@ Code Generation Options (ARM Targets) .TP .B \-mthumb Generate code using the Thumb 2 instruction encoding. -This is the default if CompCert is configured for the ARMv7R profile. +This is the default if CompCert is configured for the ARMv7M profile. . .TP .B \-marm Generate code using the ARM instruction encoding. -This is the default if CompCert is configured for a profile other than ARMv7R. +This is the default if CompCert is configured for a profile other than ARMv7M. . .SS Assembling Options @@ -327,6 +327,11 @@ Language Support Options .INDENT 0.0 . .TP +.BR \-std= +Choose the ISO C language standard to be used: \fBc99\fP, \fBc11\fP, or \fBc18\fP. +Defaults to \fBc99\fP. +. +.TP .BR \-flongdouble ", " \-fno\-longdouble Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP. Disabled by default. @@ -347,6 +352,11 @@ Turn on/off support calls to old-style functions without prototypes. Enabled by default. . .TP +.BR \-funstructured-switch ", " \-fno\-unstructured-switch +Turn on/off support for non-structured \fBswitch\fP statements. +Disabled by default. +. +.TP .BR \-fvararg\-calls ", " \-fno\-vararg\-calls Turn on/off support for calls to variable-argument functions. Enabled by default. @@ -418,7 +428,7 @@ Type of parameter or return type is implicitly assumed to be int. Enabled by default. .sp \fIinline\-asm\-sdump\fP: -Use of unsupported features in combination with dump of abstract syntax tree. +Use of inline assembly in combination with dump of abstract syntax tree. Enabled by default. .sp \fIint\-conversion\fP: @@ -429,6 +439,10 @@ Enabled by default. Functions declared as noreturn that actually contain a return statement. Enabled by default. .sp +\fIinvalid\-utf8\fP: +Illegal unicode characters in string or character constants. +Enabled by default. +.sp \fIliteral\-range\fP: Floating point literals with out-of-range magnitudes or values that convert to NaN. Enabled by default. @@ -486,6 +500,10 @@ Disabled by default. Promotable vararg arguments. Enabled by default. .sp +\fIweak\-sdump\fP: +Use of attribute \fBweak\fP in combination with dump of abstract syntax tree. +Enabled by default. +.sp \fIwrong\-ais\-parameter\fP: Use of illegal parameter expressions for embedded program annotations. Enabled by default. -- cgit From 5a9f24b4e739b6ef830f526845dd4d1557d0adee Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 3 Nov 2022 16:02:44 +0100 Subject: Ignore debug statements before the first case of a `switch` This can occur in debug mode if there are declarations before the first case, as in ``` switch (x) { int x; case 0: ... } ``` Without this commit, the code above is a structured switch if -g is not given, and a non-structured switch if -g is given. Co-authored-by: Michael Schmidt --- cparser/SwitchNorm.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/cparser/SwitchNorm.ml b/cparser/SwitchNorm.ml index 2493c63d..65d10cb2 100644 --- a/cparser/SwitchNorm.ml +++ b/cparser/SwitchNorm.ml @@ -118,6 +118,12 @@ let substitute_cases case_table body end_label = | sd -> sd } in transf false body +let rec is_skip_or_debug s = + match s.sdesc with + | Sseq (a, b) -> is_skip_or_debug a && is_skip_or_debug b + | Sskip -> true + | _ -> Cutil.is_debug_stmt s + let new_label = ref 0 let gen_label () = incr new_label; sprintf "@%d" !new_label @@ -125,7 +131,7 @@ let gen_label () = incr new_label; sprintf "@%d" !new_label let normalize_switch loc e body = let (init, cases) = [body] |> flatten_switch |> group_switch and allcases = List.rev (all_cases [] body) in - if init.sdesc = Sskip && List.length cases = List.length allcases then + if is_skip_or_debug init && List.length cases = List.length allcases then (* This is a structured switch *) make_normalized_switch e cases else begin -- cgit