diff --git a/examples/interval_loop/interval_goto_loop.c b/examples/interval_loop/interval_goto_loop.c new file mode 100644 index 0000000..94dceee --- /dev/null +++ b/examples/interval_loop/interval_goto_loop.c @@ -0,0 +1,8 @@ +void main(){ + int i = 0; + L0: + if(i >= 10) goto LF; + i++; goto L0; + LF: + assert(i >= 10); +} diff --git a/frontend/tree_to_cfg.ml b/frontend/tree_to_cfg.ml index 6ac53f6..84ba344 100644 --- a/frontend/tree_to_cfg.ml +++ b/frontend/tree_to_cfg.ml @@ -550,17 +550,29 @@ and stat_list (env:env) (entry:node) (exit:node) (l:stat ext list) : env = stat_list env1 next exit rest -(* (* Decorate a function graph with widen targets until all loops have at least one *) let make_widen_target (e:node) = List.iter (fun x -> if(x.node_id = e.node_id) then x.widen_target <- true) !nodes -let rec ensure_widens (entry:node) = +module Widenator = struct type color = Unseen | Opened | Visited - let type colnode = color * node in - () -*) + type state = color NodeMap.t + let get_color n st = try( NodeMap.find n !st )with Not_found -> Unseen + let rec ensure_widens n st = + st := NodeMap.add n Opened !st; + (List.iter (fun a -> match get_color a.arc_dst st with + | Opened -> if a.arc_dst.widen_target then () else (Format.printf "Warning : raw goto loop detected!@ "; make_widen_target a.arc_dst) + | _ -> ()) n.node_out); + (List.iter (fun a -> match get_color a.arc_dst st with + | Opened | Visited -> () (* already handled *) + | Unseen -> if a.arc_dst.widen_target then () else ensure_widens a.arc_dst st) n.node_out); + st := NodeMap.add n Visited !st + + let widen_function f = + let r = ref NodeMap.empty in + ensure_widens f.func_entry r +end (* Translate a function *) let func (env:env) (f:fun_decl) : env = @@ -640,7 +652,8 @@ let prog ((t, x): prog) : cfg = (* extract program info *) let vars = List.rev (VarSet.fold (fun a acc -> a::acc) env.env_allvars []) in let funcs = List.rev (StringMap.fold (fun _ f acc -> f::acc) env.env_funcs []) in - { cfg_vars = vars; + List.iter Widenator.widen_function funcs; + { cfg_vars = vars; cfg_funcs = funcs; cfg_init_entry = entry; cfg_init_exit = exit;