From f477edb7891a09d80d159762a9e023d4ffabf2b2 Mon Sep 17 00:00:00 2001 From: Granahir2 Date: Wed, 29 May 2024 22:30:48 +0200 Subject: [PATCH] Function support --- iterator/iterator.ml | 97 ++++++++++++++++++++++---------------------- 1 file changed, 48 insertions(+), 49 deletions(-) diff --git a/iterator/iterator.ml b/iterator/iterator.ml index 9f9b7ec..0dae579 100644 --- a/iterator/iterator.ml +++ b/iterator/iterator.ml @@ -17,64 +17,63 @@ let pp_asserts out a = | _ -> failwith "Failed on non-assert") a module Iterator (D : DOMAIN) = struct - let do_inst state arc asserts = - (* Returns a D.t describing the state we end up in after following the arc. May be bottom*) - match arc.arc_inst with - | CFG_skip _-> state, asserts - | CFG_assign (v, iexpr) -> (D.assign state v iexpr), asserts - | CFG_guard bexpr -> (D.guard state bexpr), asserts - | CFG_assert (bexpr, _) -> (let s = D.guard state (CFG_bool_unary (AST_NOT, bexpr)) in - if D.is_bottom s then ( - Format.printf "State %a is disjoint with %a@ " D.print state Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr))); - state, asserts) else ( - Format.printf "Failure of guard on %a@ " D.print s; - (D.guard state bexpr), ArcSet.add arc asserts)) - | CFG_call _ -> failwith "Function calls not yet supported" - let node_abst n s = try( NodeMap.find n s )with Not_found -> D.bottom - - let pp_nodes out (s,nodelist) = + (*let pp_nodes out (s,nodelist) = List.iter (fun node -> (Format.fprintf out "<%i>: %a@ " node.node_id D.print (node_abst node s))) nodelist - + *) let iterate cfg = - let global_state = ref NodeMap.empty in (* non-present nodes are Bot and assumed unreachable *) let failed_asserts = ref ArcSet.empty in - let dirty_nodes = ref NodeSet.empty in - - let update_node n s = - global_state := NodeMap.add n (D.join s (node_abst n !global_state)) !global_state in - - let rec do_init_code n = - if (Node.equal n cfg.cfg_init_exit) then () else ( - let nextarc = List.find (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in - let nextnode = nextarc.arc_dst in - let s, a = do_inst (node_abst n !global_state) nextarc !failed_asserts in - (Format.printf "@[Got node %i state %a@]@ " nextnode.node_id D.print s; - update_node nextnode s; failed_asserts := a; do_init_code nextnode)) in - - let rec do_iter n = begin - dirty_nodes := NodeSet.remove n !dirty_nodes; - let curr_abst = node_abst n !global_state in - let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin - List.iter (fun arc -> let s, a = do_inst curr_abst arc !failed_asserts in - failed_asserts := a; - if D.subset s (node_abst arc.arc_dst !global_state) then () - else (Format.printf "@[Got node %i state %a@]@ " arc.arc_dst.node_id D.print s; - update_node arc.arc_dst s; dirty_nodes := NodeSet.add arc.arc_dst !dirty_nodes)) l; - if NodeSet.is_empty !dirty_nodes then () else - do_iter (NodeSet.choose !dirty_nodes) - end end in + let rec do_fun (f : func) (ctx : D.t) = (*returns an abstraction of the result of exec*) + let func_state = ref NodeMap.empty in (*avoid losing precision between function calls*) + let func_dirty = ref NodeSet.empty in begin + func_state := NodeMap.add f.func_entry ctx (!func_state); + + 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 rec iterate n = begin + func_dirty := NodeSet.remove n !func_dirty; + let curr_abst = node_abst n in + 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 "@[Got node %i state %a@]@ " arc.arc_dst.node_id D.print s; + update_node arc.arc_dst s; func_dirty := NodeSet.add arc.arc_dst !func_dirty)) l; + if NodeSet.is_empty !func_dirty then () else + iterate (NodeSet.choose !func_dirty) + end end in + iterate f.func_entry; + node_abst f.func_exit; + end + and do_inst state arc = (* Returns a D.t describing the state we end up in after following the arc. May be bottom*) + match arc.arc_inst with + | CFG_skip _-> state + | CFG_assign (v, iexpr) -> (D.assign state v iexpr) + | CFG_guard bexpr -> D.guard state bexpr + | CFG_assert (bexpr, _) -> (let s = D.guard state (CFG_bool_unary (AST_NOT, bexpr)) in + if D.is_bottom s then ( + Format.printf "State %a is disjoint with %a@ " D.print state Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr))); + state) else ( + Format.printf "Failure of guard on %a@ " D.print s; + failed_asserts := ArcSet.add arc !failed_asserts; + (D.guard state bexpr))) + | CFG_call f -> do_fun f state + in begin - global_state := NodeMap.add (cfg.cfg_init_entry) D.init !global_state; Format.printf "@["; - do_init_code cfg.cfg_init_entry; (* do the init code *) + let init_st = do_fun {func_id = -1; func_name = "_init"; + func_pos = Lexing.dummy_pos, Lexing.dummy_pos; + func_entry = cfg.cfg_init_entry; + func_exit = cfg.cfg_init_exit; + func_args = []; + func_ret = None; + func_calls = []} D.init in let x = List.hd cfg.cfg_funcs in (* we are ASSUMING main() is function 0*) - global_state := NodeMap.add (x.func_entry) (node_abst cfg.cfg_init_exit !global_state) !global_state; - do_iter x.func_entry; + let _ = do_fun x init_st in Format.printf "@]"; - Format.printf "@[Node states :@ %a@]" pp_nodes (!global_state,cfg.cfg_nodes); - !failed_asserts; + !failed_asserts end end