Dear Elnatan,
Thank you very much for your patches. I tested them, but I have some
questions before I push them upstream. Please see below.
On Fri, Jan 07, 2011 at 12:16:17AM -0500, Elnatan Reisner wrote:
> One patch, switch_default_ordering.patch, fixes an actual bug
> (although I suppose it never comes up in practice, given that it
> hasn't been found already) in CIL's transformation of switch
> statements, due to assumptions on the order of 'case' and 'default'
> labels. The patch includes a test case that exhibits the bug.
Looks fine, added the test case to the test suite.
> I'm guessing this bug hasn't been found because no one ever puts
> 'case' labels on the same block as a 'default' label, because that
> wouldn't do anything. Despite the fact that this apparently never
> arises in practice, my sense of cleanliness urged me to want to
> remove 'case' labels that occur alongside a 'default' label. This is
> remove_case_when_default.patch . Doing this also has the benefit of
> removing unnecessary 'if' statements from the transformed switch
> statements.
This is definitely a good idea (nice invariant to have).
> I noticed that this only removed 'case' labels *before* a 'default',
> but not after a 'default'. It turns out there's a strange quirk in
> the parser that makes it so that 'default' labels are always
> followed by empty statements. This isn't quite a bug (because the
> empty statement just falls through to the next statement), but it
> means that the parser accepts
> switch (x) { default: }
> while I think is not valid C. Also, fixing this makes the previous
> patch more effective, so I made this (trivial) change in
> default_parse.patch .
Thanks, I also added a test case for this one.
> Finally, since I was playing around with switch statements anyway, I
> did one further thing. You may have seen my previous posts about
> wanting to retain '&&'s and '||'s wherever possible. Well, that is
> possible for switch statements if there are multiple 'case' labels
> on a single block.
I'm afraid I do not fully understand what happens in this patch. Please
tell me if my explanations below are correct. If this is the case, do
not bother to send an updated patch, I'll apply the changes myself
before pushing to upstream. Just correct me if I'm wrong.
Index: src/cil.ml
===================================================================
--- src/cil.ml (revision 12099)
+++ src/cil.ml (working copy)
@@ -6567,19 +6570,27 @@
| stmt_hd :: stmt_tl -> begin
let rec handle_labels lab_list = begin
match lab_list with
- [] -> handle_choices stmt_tl
+ [] -> E.s (bug "Block missing 'case' and 'default' in switch
statement")
| Case(ce,cl) :: lab_tl ->
- let pred = BinOp(Eq,e,ce,intType) in
+ let make_or_from_cases labels =
+ List.fold_left
+ (fun pred label -> match label with
+ Case (exp, _) -> BinOp(LOr, pred,
BinOp(Eq,e,exp,intType), intType)
+ | _ -> E.s (bug "Non-'case' label after 'case'
label"))
] You seem to assume that:
] - there can be no "Default", which means that you assume that your code
] in rmtmps.ml has been executed. What if this is not case (e.g.
] Rmtmps.keepUnused = true)? Maybe you could sort labels, to ensure
] that Default is always at the begining of the list, or just rewrite
] handle_labels in a non-recursive fashion (probably the best).
] - there can be no "Label" after a "Case"; I fail to see why this would
] be the case (no pun intended), but the same solution than above should
] apply (ie. filter out Labels, look for a Default and use it, or
] otherwise you have only cases and can safely go on).
+ (BinOp(Eq,e,ce,intType))
+ labels
+ in
+ let pred = make_or_from_cases lab_tl in
let then_block = mkBlock [ mkStmt (Goto(ref stmt_hd,cl)) ] in
- let else_block = mkBlock [ mkStmt (handle_labels lab_tl) ] in
+ let else_block = mkBlock [ mkStmt (handle_choices stmt_tl) ] in
If(pred,then_block,else_block,cl)
| Default(dl) :: lab_tl ->
(* ww: before this was 'if (1) goto label', but as Ben points
out this might confuse someone down the line who doesn't have
special handling for if(1) into thinking that there are two
paths here. The simpler 'goto label' is what we want. *)
- Block(mkBlock [ mkStmt (Goto(ref stmt_hd,dl)) ;
- mkStmt (handle_labels lab_tl) ])
+ body_block.bstmts <- mkStmt (Goto(ref stmt_hd,dl)) ::
body_block.bstmts @ [ break_stmt ] ;
+ Block body_block
] IIUC what is going on, here you can safely ignore lab_tl because it
] should be the empty list (since the list has been sorted). I would feel
] safer with an assert(lab_tl = []).
| Label(_,_,_) :: lab_tl -> handle_labels lab_tl
end in
handle_labels stmt_hd.labels
> And, while I was making that change, I made one other change: I
> removed the 'if (0)' that gets inserted in the very center of the
> switch statement, as long as there is a 'default' label in the
> switch statement. (This 'if (0)' is needed if and only if there is
> no 'default' label.)
The comment mentionning if(0) should be updated then (it is already
wrong, btw, since break_stmt is no more protected by an if(0)).
Best regards,
--
Gabriel Kerneis
------------------------------------------------------------------------------
Protect Your Site and Customers from Malware Attacks
Learn about various malware tactics and how to avoid them. Understand
malware threats, the impact they can have on your business, and how you
can protect your company and customers by using code signing.
http://p.sf.net/sfu/oracle-sfdevnl
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
