*** ../cil/src/cil.ml 2006-05-21 06:14:15.000000000 +0200 --- ../cil_patch/src/cil.ml 2006-07-25 10:57:30.686790845 +0200 *************** *** 1,3 **** --- 1,6 ---- + (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) + (* MODIF: useLogicalOperators flag set to true by default. *) + (* * * Copyright (c) 2001-2003, *************** *** 63,69 **** * print output for the MS VC * compiler. Default is GCC *) ! let useLogicalOperators = ref false module M = Machdep --- 66,72 ---- * print output for the MS VC * compiler. Default is GCC *) ! let useLogicalOperators = ref (*false*) true module M = Machdep *************** *** 684,692 **** | Goto of stmt ref * location (** A goto statement. Appears from actual goto's in the code. *) | Break of location (** A break to the end of the nearest ! enclosing Loop or Switch *) | Continue of location (** A continue to the start of the ! nearest enclosing [Loop] *) | If of exp * block * block * location (** A conditional. Two successors, the "then" and the "else" branches. Both --- 687,695 ---- | Goto of stmt ref * location (** A goto statement. Appears from actual goto's in the code. *) | Break of location (** A break to the end of the nearest ! enclosing loop or Switch *) | Continue of location (** A continue to the start of the ! nearest enclosing loop *) | If of exp * block * block * location (** A conditional. Two successors, the "then" and the "else" branches. Both *************** *** 701,706 **** --- 704,710 ---- you can get from the labels of the statement *) + (* | Loop of block * location * (stmt option) * (stmt option) (** A [while(1)] loop. The * termination test is implemented *************** *** 713,718 **** --- 717,726 ---- * and the second will point to * the stmt containing the break * label for this loop. *) + *) + | While of exp * block * location (** A while loop. *) + | DoWhile of exp * block * location (** A do...while loop. *) + | For of block * exp * block * block * location (** A for loop. *) | Block of block (** Just a block of statements. Use it as a way to keep some attributes *************** *** 1040,1046 **** --- 1048,1059 ---- | Continue(loc) -> loc | If(_, _, _, loc) -> loc | Switch (_, _, _, loc) -> loc + (* | Loop (_, loc, _, _) -> loc + *) + | While (_, _, loc) -> loc + | DoWhile (_, _, loc) -> loc + | For (_, _, _, _, loc) -> loc | Block b -> if b.bstmts == [] then lu else get_stmtLoc ((List.hd b.bstmts).skind) | TryFinally (_, _, l) -> l *************** *** 1524,1533 **** --- 1537,1549 ---- let mkWhile ~(guard:exp) ~(body: stmt list) : stmt list = (* Do it like this so that the pretty printer recognizes it *) + (* [ mkStmt (Loop (mkBlock (mkStmt (If(guard, mkBlock [ mkEmptyStmt () ], mkBlock [ mkStmt (Break lu)], lu)) :: body), lu, None, None)) ] + *) + [ mkStmt (While (guard, mkBlock body, lu)) ] *************** *** 3448,3453 **** --- 3464,3471 ---- ++ self#pExp () e ++ text ") " ++ self#pBlock () b) + + (* | Loop(b, l, _, _) -> begin (* Maybe the first thing is a conditional. Turn it into a WHILE *) try *************** *** 3484,3489 **** --- 3502,3540 ---- ++ text "ile (1) " ++ self#pBlock () b) end + *) + + | While (e, b, l) -> + self#pLineDirective l + ++ (align + ++ text "while (" + ++ self#pExp () e + ++ text ") " + ++ self#pBlock () b) + + | DoWhile (e, b, l) -> + self#pLineDirective l + ++ (align + ++ text "do " + ++ self#pBlock () b + ++ text " while (" + ++ self#pExp () e + ++ text ");") + + | For (bInit, e, bIter, b, l) -> + ignore (E.warn + "in for loops, the 1st and 3rd expressions are not printed"); + self#pLineDirective l + ++ (align + ++ text "for (" + ++ text "/* ??? */" (* self#pBlock () bInit *) + ++ text "; " + ++ self#pExp () e + ++ text "; " + ++ text "/* ??? */" (* self#pBlock() bIter *) + ++ text ") " + ++ self#pBlock () b) + | Block b -> align ++ self#pBlock () b | TryFinally (b, h, l) -> *************** *** 4705,4713 **** --- 4756,4781 ---- | Return (Some e, l) -> let e' = fExp e in if e' != e then Return (Some e', l) else s.skind + (* | Loop (b, l, s1, s2) -> let b' = fBlock b in if b' != b then Loop (b', l, s1, s2) else s.skind + *) + | While (e, b, l) -> + let e' = fExp e in + let b' = fBlock b in + if e' != e || b' != b then While (e', b', l) else s.skind + | DoWhile (e, b, l) -> + let b' = fBlock b in + let e' = fExp e in + if e' != e || b' != b then DoWhile (e', b', l) else s.skind + | For (bInit, e, bIter, b, l) -> + let bInit' = fBlock bInit in + let e' = fExp e in + let bIter' = fBlock bIter in + let b' = fBlock b in + if bInit' != bInit || e' != e || bIter' != bIter || b' != b then + For (bInit', e', bIter', b', l) else s.skind | If(e, s1, s2, l) -> let e' = fExp e in (*if e queued any instructions, pop them here and remember them so that *************** *** 5180,5186 **** --- 5248,5262 ---- peepHole1 doone tb.bstmts; peepHole1 doone eb.bstmts | Switch (e, b, _, _) -> peepHole1 doone b.bstmts + (* | Loop (b, l, _, _) -> peepHole1 doone b.bstmts + *) + | While (_, b, _) -> peepHole1 doone b.bstmts + | DoWhile (_, b, _) -> peepHole1 doone b.bstmts + | For (bInit, _, bIter, b, _) -> + peepHole1 doone bInit.bstmts; + peepHole1 doone bIter.bstmts; + peepHole1 doone b.bstmts | Block b -> peepHole1 doone b.bstmts | TryFinally (b, h, l) -> peepHole1 doone b.bstmts; *************** *** 5214,5220 **** --- 5290,5304 ---- peepHole2 dotwo tb.bstmts; peepHole2 dotwo eb.bstmts | Switch (e, b, _, _) -> peepHole2 dotwo b.bstmts + (* | Loop (b, l, _, _) -> peepHole2 dotwo b.bstmts + *) + | While (_, b, _) -> peepHole2 dotwo b.bstmts + | DoWhile (_, b, _) -> peepHole2 dotwo b.bstmts + | For (bInit, _, bIter, b, _) -> + peepHole2 dotwo bInit.bstmts; + peepHole2 dotwo bIter.bstmts; + peepHole2 dotwo b.bstmts | Block b -> peepHole2 dotwo b.bstmts | TryFinally (b, h, l) -> peepHole2 dotwo b.bstmts; peepHole2 dotwo h.bstmts *************** *** 5887,5892 **** --- 5971,5977 ---- [] -> trylink s fallthrough | hd :: tl -> (link s hd ; succpred_block b2 fallthrough )) + (* | Loop(b,l,_,_) -> begin match b.bstmts with [] -> failwith "computeCFGInfo: empty loop" *************** *** 5894,5899 **** --- 5979,6011 ---- link s hd ; succpred_block b (Some(hd)) end + *) + + | While (e, b, l) -> begin match b.bstmts with + | [] -> failwith "computeCFGInfo: empty loop" + | hd :: tl -> link s hd ; + succpred_block b (Some(hd)) + end + + | DoWhile (e, b, l) ->begin match b.bstmts with + | [] -> failwith "computeCFGInfo: empty loop" + | hd :: tl -> link s hd ; + succpred_block b (Some(hd)) + end + + | For (bInit, e, bIter, b, l) -> + (match bInit.bstmts with + | [] -> failwith "computeCFGInfo: empty loop" + | hd :: tl -> link s hd ; + succpred_block bInit (Some(hd))) ; + (match bIter.bstmts with + | [] -> failwith "computeCFGInfo: empty loop" + | hd :: tl -> link s hd ; + succpred_block bIter (Some(hd))) ; + (match b.bstmts with + | [] -> failwith "computeCFGInfo: empty loop" + | hd :: tl -> link s hd ; + succpred_block b (Some(hd))) ; | Block(b) -> begin match b.bstmts with [] -> trylink s fallthrough *************** *** 5985,5991 **** let i = get_switch_count () in let break_stmt = mkStmt (Instr []) in break_stmt.labels <- ! [Label((Printf.sprintf "switch_%d_break" i),l,false)] ; let break_block = mkBlock [ break_stmt ] in let body_block = b in let body_if_stmtkind = (If(zero,body_block,break_block,l)) in --- 6097,6103 ---- let i = get_switch_count () in let break_stmt = mkStmt (Instr []) in break_stmt.labels <- ! [Label((Printf.sprintf "switch_%d_break" i),l,false)] ; let break_block = mkBlock [ break_stmt ] in let body_block = b in let body_if_stmtkind = (If(zero,body_block,break_block,l)) in *************** *** 6026,6039 **** s.skind <- handle_choices (List.sort compare_choices sl) ; xform_switch_block b (fun () -> ref break_stmt) cont_dest i end | Loop(b,l,_,_) -> let i = get_switch_count () in let break_stmt = mkStmt (Instr []) in break_stmt.labels <- ! [Label((Printf.sprintf "while_%d_break" i),l,false)] ; let cont_stmt = mkStmt (Instr []) in cont_stmt.labels <- ! [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; b.bstmts <- cont_stmt :: b.bstmts ; let this_stmt = mkStmt (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in --- 6138,6152 ---- s.skind <- handle_choices (List.sort compare_choices sl) ; xform_switch_block b (fun () -> ref break_stmt) cont_dest i end + (* | Loop(b,l,_,_) -> let i = get_switch_count () in let break_stmt = mkStmt (Instr []) in break_stmt.labels <- ! [Label((Printf.sprintf "while_%d_break" i),l,false)] ; let cont_stmt = mkStmt (Instr []) in cont_stmt.labels <- ! [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; b.bstmts <- cont_stmt :: b.bstmts ; let this_stmt = mkStmt (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in *************** *** 6043,6048 **** --- 6156,6217 ---- break_stmt.succs <- s.succs ; let new_block = mkBlock [ this_stmt ; break_stmt ] in s.skind <- Block new_block + *) + | While (e, b, l) -> + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- + [Label((Printf.sprintf "while_%d_break" i),l,false)] ; + let cont_stmt = mkStmt (Instr []) in + cont_stmt.labels <- + [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; + b.bstmts <- cont_stmt :: b.bstmts ; + let this_stmt = mkStmt + (While(e,b,l)) in + let break_dest () = ref break_stmt in + let cont_dest () = ref cont_stmt in + xform_switch_block b break_dest cont_dest label_index ; + break_stmt.succs <- s.succs ; + let new_block = mkBlock [ this_stmt ; break_stmt ] in + s.skind <- Block new_block + + | DoWhile (e, b, l) -> + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- + [Label((Printf.sprintf "while_%d_break" i),l,false)] ; + let cont_stmt = mkStmt (Instr []) in + cont_stmt.labels <- + [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; + b.bstmts <- cont_stmt :: b.bstmts ; + let this_stmt = mkStmt + (DoWhile(e,b,l)) in + let break_dest () = ref break_stmt in + let cont_dest () = ref cont_stmt in + xform_switch_block b break_dest cont_dest label_index ; + break_stmt.succs <- s.succs ; + let new_block = mkBlock [ this_stmt ; break_stmt ] in + s.skind <- Block new_block + + | For (bInit, e, bIter , b, l) -> + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- + [Label((Printf.sprintf "while_%d_break" i),l,false)] ; + let cont_stmt = mkStmt (Instr []) in + cont_stmt.labels <- + [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; + b.bstmts <- cont_stmt :: b.bstmts ; + let this_stmt = mkStmt + (For(bInit,e,bIter,b,l)) in + let break_dest () = ref break_stmt in + let cont_dest () = ref cont_stmt in + xform_switch_block b break_dest cont_dest label_index ; + break_stmt.succs <- s.succs ; + let new_block = mkBlock [ this_stmt ; break_stmt ] in + s.skind <- Block new_block + + | Block(b) -> xform_switch_block b break_dest cont_dest label_index | TryExcept _ | TryFinally _ ->