Ensure termination in while/for

frontend/cfg.ml

@@ -179,6 +179,8 @@ and node =
       node_pos: position;          (* position in the source *)
       mutable node_out: arc list;  (* arcs with this node as source *)
       mutable node_in: arc list;   (* arcs with this node as destination *)
+      mutable widen_target : bool; (* is node a candidate for widening : either head of structured loop
+	or destination of goto in goto-made loop that doesn't have any widen-target *)
     }
 
 and arc =

frontend/cfg_printer.ml

@@ -231,6 +231,7 @@ let print_cfg fmt p =
       List.iter (fun a -> Format.fprintf fmt "%i " a.arc_src.node_id) n.node_in;
       Format.fprintf fmt "out:";
       List.iter (fun a -> Format.fprintf fmt "%i " a.arc_dst.node_id) n.node_out;
+      if n.widen_target then Format.fprintf fmt "(widen target)";
       Format.fprintf fmt "\n";
     ) p.cfg_nodes;
   Format.fprintf fmt "\n";

frontend/tree_to_cfg.ml

@@ -36,19 +36,19 @@ let node_counter = ref 0
 let nodes = ref []
 
 (* create a new node, with a fresh identifier and accumulate into nodes *)
-let create_node (pos:position) =
+let create_node ?(widen_target) (pos:position) =
   incr node_counter;
   let node =
     { node_id = !node_counter;
       node_pos = pos;
       node_in = [];
       node_out = [];
+      widen_target = match widen_target with | None -> false | Some b -> b;
     }
   in
   nodes := node::(!nodes);
   node
 
-
 let arcs = ref []
 
 let arc_counter = ref 0
@@ -456,7 +456,7 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env =
        let env1, before, e = bool_expr env expr in
        (* entry --[before]--> entry1 *)
        let entry1 = append_inst entry before in
-       let node_t = create_node (fst x1) in
+       let node_t = create_node ~widen_target:true (fst x1) in
        (* entry1 --[expr]--> node_t *)
        add_arc entry1 node_t (CFG_guard e);
        (* entry1 --[!expr]--> node_f *)
@@ -487,7 +487,7 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env =
          | Some (expr,_) -> bool_expr env1 expr
        in
        let head1 = append_inst head before in
-       let node_t = create_node (fst x1) in
+       let node_t = create_node ~widen_target:true (fst x1) in
        add_arc head1 node_t (CFG_guard e);
        add_arc head1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e)));
        (* increment *)
@@ -550,6 +550,16 @@ 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) = 
+	type color = Unseen | Opened | Visited
+	let type colnode = color * node in
+	()	
+*)	
 
 (* Translate a function *)
 

iterator/iterator.ml

@@ -31,7 +31,8 @@ module Iterator (D : DOMAIN) = struct
 
 			let node_abst n = try( NodeMap.find n !func_state )with Not_found -> D.bottom in
 			let update_node n s =
-				func_state := NodeMap.add n (D.join s (node_abst n)) !func_state in
+				let acctor = if (n.widen_target) then D.widen else D.join in
+				func_state := NodeMap.add n (acctor (node_abst n) s) !func_state in
 
 			let rec iterate n = begin
 				(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
@@ -40,8 +41,11 @@ module Iterator (D : DOMAIN) = struct
 				let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin
 				List.iter (fun arc -> let s = do_inst curr_abst arc in
 						if D.subset s (node_abst arc.arc_dst) then ()
-						else (Format.printf "@[<h 0>[%i -> %i] Got node %i state %a join %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id
+						else (let str = if arc.arc_dst.widen_target then "widen" else "join" in
-							D.print (node_abst arc.arc_dst) D.print s;
+						Format.printf "@[<h 0>[%i -> %i] Got node %i state %a %s %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id
+							D.print (node_abst arc.arc_dst)
+							str
+							D.print s;
 						update_node arc.arc_dst s;
 						Format.printf "= %a@]@ " D.print (node_abst arc.arc_dst);
 						func_dirty := NodeSet.add arc.arc_dst !func_dirty)) l;