Merge pull request #459 from AbsInt/full-switch

Handle Duff's device and other unstructured `switch` statements

13 files changed, 500 insertions, 142 deletions

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 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 ->
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 <args> to the preprocessor.
 Pass argument <arg> 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=<standard>
+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.
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 5d45306d..c8131662 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -79,14 +79,14 @@ 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
+      ~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 da31c7d7..23125001 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 <stdlib.h>
+#include <stdio.h>
+
+/* 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;
+}