From 2fc13a3ec46f4ef14472bf62cdd422b76b25914a Mon Sep 17 00:00:00 2001
From: Granahir2 <a1687516@gmail.com>
Date: Tue, 4 Jun 2024 17:55:32 +0200
Subject: [PATCH] Goto loop termination support

---
 examples/interval_loop/interval_goto_loop.c |  8 +++++++
 frontend/tree_to_cfg.ml                     | 25 ++++++++++++++++-----
 2 files changed, 27 insertions(+), 6 deletions(-)
 create mode 100644 examples/interval_loop/interval_goto_loop.c

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;