On Jan 14, 2011, at 10:18 AM, Gabriel Kerneis wrote: > 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: >> 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 just noticed a problem with this patch: '&&'s and '||'s are inserted even if useLogicalOperators is false, and they don't later get converted away. This is probably easy to fix, but it's not immediately obvious to me how. > 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). Yes, you're right. Note that the patch to rmtmps.ml that I sent before actually enforces *both* of the invariants you mention. But I think you're right that there is probably a cleaner nonrecursive solution. > | 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 = []). I totally agree. I think I had an assert here at some point, but I guess not when I submitted the patch. > | 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)). I'm not sure I fully understand your comment, but notice that there still *will* be an 'if(0)' guarding body_block if there is no 'default' in the switch statement. Elnatan ------------------------------------------------------------------------------ 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
