Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Handle Duff's device and other unstructured switch statements #459

Merged
merged 5 commits into from
Nov 9, 2022
Merged

Handle Duff's device and other unstructured switch statements #459

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
efc51af
Revised passing of options to `Parse.preprocessed_file`
xavierleroy Sep 27, 2022
dfc6b66
Unblock: never put debug info before a label
xavierleroy Oct 24, 2022
a1dabb4
Handle unstructured 'switch' statements such as Duff's device
xavierleroy Sep 27, 2022
8eadd08
Update man-page for `-funstructured-switch` (also for new `-std` opti…
m-schmidt Nov 3, 2022
5a9f24b
Ignore debug statements before the first case of a `switch`
xavierleroy Nov 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 18 additions & 84 deletions cfrontend/C2C.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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 _, _) ->
Expand All @@ -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 *)

Expand Down
53 changes: 24 additions & 29 deletions cparser/Parse.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
18 changes: 13 additions & 5 deletions cparser/Parse.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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). *)
179 changes: 179 additions & 0 deletions cparser/SwitchNorm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading