Goto loop termination support

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);
+}

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,6 +652,7 @@ 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
+  List.iter Widenator.widen_function funcs;
  { cfg_vars = vars;
     cfg_funcs = funcs;
     cfg_init_entry = entry;