Function support
This commit is contained in:
Granahir2
parent
e6ecc3e9b0
commit
f477edb789
1 changed files with 48 additions and 49 deletions
|
|
@ -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*)
|
||||
|
||||
(*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 failed_asserts = ref ArcSet.empty 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 "@[<h 0>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, asserts
|
||||
| CFG_assign (v, iexpr) -> (D.assign state v iexpr), asserts
|
||||
| CFG_guard bexpr -> (D.guard state bexpr), asserts
|
||||
| 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, asserts) else (
|
||||
state) 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) =
|
||||
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 "@[<h 0>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 "@[<h 0>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
|
||||
|
||||
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 "@[<v 0>";
|
||||
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 "@[<v 0>Node states :@ %a@]" pp_nodes (!global_state,cfg.cfg_nodes);
|
||||
!failed_asserts;
|
||||
!failed_asserts
|
||||
end
|
||||
end
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue