From 39f938226e0bdf9ce0d7a8ad880db18721e1e3b5 Mon Sep 17 00:00:00 2001 From: Granahir2 Date: Sun, 2 Jun 2024 12:09:52 +0200 Subject: [PATCH] Ensure termination in while/for --- frontend/cfg.ml | 2 ++ frontend/cfg_printer.ml | 1 + frontend/tree_to_cfg.ml | 18 ++++++++++++++---- iterator/iterator.ml | 10 +++++++--- 4 files changed, 24 insertions(+), 7 deletions(-) diff --git a/frontend/cfg.ml b/frontend/cfg.ml index 0718571..7b8861c 100644 --- a/frontend/cfg.ml +++ b/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 = diff --git a/frontend/cfg_printer.ml b/frontend/cfg_printer.ml index 07957d8..68999d3 100644 --- a/frontend/cfg_printer.ml +++ b/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"; diff --git a/frontend/tree_to_cfg.ml b/frontend/tree_to_cfg.ml index e3d56f6..6ac53f6 100644 --- a/frontend/tree_to_cfg.ml +++ b/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 *) diff --git a/iterator/iterator.ml b/iterator/iterator.ml index a2f11ae..6a0eb2c 100644 --- a/iterator/iterator.ml +++ b/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 "@[ 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 "@[[%i -> %i] Got node %i state %a join %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id - D.print (node_abst arc.arc_dst) D.print s; + else (let str = if arc.arc_dst.widen_target then "widen" else "join" in + Format.printf "@[[%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;