diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Parse.ml | 53 | ||||
| -rw-r--r-- | cparser/Parse.mli | 18 | ||||
| -rw-r--r-- | cparser/SwitchNorm.ml | 179 | ||||
| -rw-r--r-- | cparser/SwitchNorm.mli | 28 | ||||
| -rw-r--r-- | cparser/Unblock.ml | 23 |
5 files changed, 256 insertions, 45 deletions
diff --git a/cparser/Parse.ml b/cparser/Parse.ml index a54af0cc..607d8927 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -16,33 +16,23 @@ (* 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 ~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 + 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 + |> run_opt_pass3 SwitchNorm.program switch_norm + |> 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 +55,11 @@ 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) + ?(switch_norm = `Off) + ?(struct_passing = false) + ?(packed_structs = false) + name sourcefile = Diagnostics.reset(); let check_errors x = Diagnostics.check_errors(); x in @@ -79,5 +73,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 ~switch_norm ~struct_passing ~packed_structs) |> check_errors diff --git a/cparser/Parse.mli b/cparser/Parse.mli index c406d96c..a37bd0e0 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -16,8 +16,16 @@ (* 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 -> + ?switch_norm: [`Off | `Partial | `Full] -> + ?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] or [`Off] + (do not perform). *) diff --git a/cparser/SwitchNorm.ml b/cparser/SwitchNorm.ml new file mode 100644 index 00000000..65d10cb2 --- /dev/null +++ b/cparser/SwitchNorm.ml @@ -0,0 +1,179 @@ +(* *********************************************************************) +(* *) +(* 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 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 + +let normalize_switch loc e body = + let (init, cases) = [body] |> flatten_switch |> group_switch + and allcases = List.rev (all_cases [] body) in + 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 + (* 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 4b1f2262..32e09399 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 ctx ploc s1 in + {s with sdesc = Slabeled(lbl, s1')} | Sgoto lbl -> add_lineno ctx ploc s.sloc s | Sreturn None -> |