Commit b4c9716e authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/interpreted-automata/ordered-iteration' into 'master'

[Interpreted_automata] dataflow analysis: implements an ordered iteration over results

See merge request frama-c/frama-c!4023
parents 25e7342e 748b3dd7
......@@ -1215,6 +1215,7 @@ sig
val after : result -> Cil_types.stmt -> state option
val iter_vertex : (vertex -> state -> unit) -> result -> unit
val iter_stmt : (Cil_types.stmt -> state -> unit) -> result -> unit
val iter_stmt_asc : (Cil_types.stmt -> state -> unit) -> result -> unit
val to_dot_output : (Format.formatter -> state -> unit) ->
result -> out_channel -> unit
val to_dot_file : (Format.formatter -> state -> unit) ->
......@@ -1324,6 +1325,19 @@ struct
in
States.iter f' states
let iter_stmt_asc f (_automaton,_wto,states) =
let filter (v,s) =
match v.vertex_start_of with
| None -> None
| Some stmt -> Some (stmt,s)
in
let cmp (stmt1,_) (stmt2,_) =
Cil_datatype.Stmt.compare stmt1 stmt2
in
States.to_seq states |> Seq.filter_map filter |>
List.of_seq |> List.fast_sort cmp |>
List.iter (fun (stmt,s) -> f stmt s)
let to_dot_output pp_value (automaton,wto,states) out =
let pp_vertex fmt v =
match States.find_opt states v with
......
......@@ -347,6 +347,10 @@ sig
returned None) *)
val iter_stmt : (Cil_types.stmt -> state -> unit) -> result -> unit
(** Same as [iter_stmt] but guarantee that the iteration will always
be in the same increasing order of statements sid *)
val iter_stmt_asc : (Cil_types.stmt -> state -> unit) -> result -> unit
(** Output result to the given channel. Must be supplied with a pretty
printer for abstract values *)
val to_dot_output : (Format.formatter -> state -> unit) ->
......
......@@ -50,30 +50,19 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
include Hashtbl.Make(H)
let bindings_sorted ?(cmp=Stdlib.compare) h =
to_seq h |> List.of_seq |> List.fast_sort (fun (k1,_) (k2,_) -> cmp k1 k2)
let fold_sorted ?(cmp=Stdlib.compare) f h acc =
let module Aux = struct type t = key let compare = cmp end in
let module M = Map.Make(Aux) in
let add k v m =
try
let l = v :: M.find k m in
M.add k l m
with Not_found -> M.add k [v] m
in
let map = fold add h M.empty in
let fold_k k l acc =
List.fold_left (fun acc v -> f k v acc) acc (List.rev l)
in
M.fold fold_k map acc
let l = bindings_sorted ~cmp h in
List.fold_left (fun acc (k,v) -> f k v acc) acc l
let iter_sorted ?cmp f h =
fold_sorted ?cmp (fun k v () -> f k v) h ()
let fold_sorted_by_entry (type value) ~cmp f h acc =
let module Aux = struct type t = (key*value) let compare = cmp end in
let module S = Set.Make(Aux) in
let add k v s = S.add (k,v) s in
let set = fold add h S.empty in
S.fold (fun (k,v) -> f k v) set acc
let fold_sorted_by_entry ~cmp f h acc =
let l = to_seq h |> List.of_seq |> List.fast_sort cmp in
List.fold_left (fun acc (k,v) -> f k v acc) acc l
let iter_sorted_by_entry ~cmp f h =
fold_sorted_by_entry ~cmp (fun k v () -> f k v) h ()
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment