AStat/iterator/iterator.ml
2024-06-01 19:29:10 +02:00

109 lines
3.9 KiB
OCaml
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
open Cfg
open Domain
let pp_asserts out a =
ArcSet.iter (fun arc -> match arc.arc_inst with
| CFG_assert (b, ext) -> Format.fprintf out "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> failwith "Failed on non-assert") a
module Iterator (D : DOMAIN) = struct
(*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
(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
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
| 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
Format.printf "@[<v 0>";
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 rec do_main l = match l with
| x::_ when x.func_name = "main" -> do_fun x init_st
| _::q -> do_main q
| [] -> failwith "function main() not found" in
let _ = do_main cfg.cfg_funcs in
Format.printf "@]";
!failed_asserts
end
end
open Sign
open Constant
open Naked
open Value_domain
module ConstIterator = Iterator(NonRelational(AddTopBot(Constants)))
module SignIterator = Iterator(NonRelational(AddTopBot(Signs)))
(*
let iterate cfg =
let () = Random.self_init () in
let iter_arc arc: unit =
match arc.arc_inst with
| CFG_assert (b, ext) ->
Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> () in
(* let iter_arc arc: unit =
match arc.arc_inst with
| CFG_assert (b, ext) ->
Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> () in
let iter_node node: unit =
Format.printf "<%i>: @ " node.node_id in
List.iter iter_arc cfg.cfg_arcs;
Format.printf "Node Values:@ @[<v 0>";
List.iter iter_node cfg.cfg_nodes;
Format.printf "@]"*)
*)