Added dataflow module

This commit is contained in:
elvis
2024-12-12 16:37:36 +01:00
parent 08a8d07422
commit 590123d988
17 changed files with 275 additions and 57 deletions

136
lib/analysis/Dataflow.ml Normal file
View File

@ -0,0 +1,136 @@
module type C = sig
type elt
type internal
type internalnode = {
internalin: internal list;
internalout: internal list;
internalbetween: internal list list;
}
type cfgt = elt Cfg.cfginternal
type t = {
t: cfgt;
internalvar: internalnode Cfg.NodeMap.t;
}
val from_cfg : cfgt -> t
val to_cfg : t -> cfgt
val fixed_point : ?init:(elt list -> internalnode) -> ?update:(t -> Cfg.Node.t -> internalnode) -> t -> t
val pp : out_channel -> t -> unit
end
module Make (M: Cfg.PrintableType) (I: Cfg.PrintableType) = struct
type elt = M.t
type internal = I.t
type internalnode = {
internalin: internal list;
internalout: internal list;
internalbetween: internal list list;
}
type cfgt = elt Cfg.cfginternal
type t = {
t: cfgt;
internalvar: internalnode Cfg.NodeMap.t;
}
let from_cfg (cfg: cfgt) : t =
{t = cfg; internalvar = Cfg.NodeMap.empty}
let to_cfg ({t; _}: t) : cfgt =
t
let fixed_point
?(init : (elt list -> internalnode) =
(fun _ -> {internalin = []; internalout = []; internalbetween = []}))
?(update : (t -> Cfg.Node.t -> internalnode) =
(fun t n -> Cfg.NodeMap.find n t.internalvar))
(t: t)
: t =
(* init function is applied only once to each node content,
the update function takes the node and the whole structure and is
expected to return the updated structure for the appropriate node,
update function is applied to the resulting structure until no change is
observed
*)
let rec helper t =
let newt =
{t with
internalvar = Cfg.NodeMap.mapi (fun n _ -> update t n) t.internalvar}
in
if newt = t then newt else helper newt
in
helper { t with internalvar = Cfg.NodeMap.map init t.t.content }
open Cfg
let pp (ppf: out_channel) (c: t) : unit =
Printf.fprintf ppf "Cfg:\n";
Printf.fprintf ppf "Nodes' ids: ";
List.iter (fun (x : Node.t) -> Printf.fprintf ppf "%d " x.id) (NodeSet.to_list c.t.nodes);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' edges:\n";
List.iter (fun ((n, (a, b)) : (Node.t * (Node.t * Node.t option))) : unit ->
match b with None -> Printf.fprintf ppf "\t%d -> %d\n" n.id a.id
| Some b -> Printf.fprintf ppf "\t%d -> %d, %d\n" n.id a.id b.id
) (NodeMap.to_list c.t.edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' back edges:\n";
List.iter (fun ((n, xs) : (Node.t * (Node.t list))) : unit ->
Printf.fprintf ppf "\t%d -> " n.id;
List.iter (fun (x: Node.t) -> Printf.fprintf ppf "%d, " x.id) xs;
Printf.fprintf ppf "\n"
) (NodeMap.to_list c.t.reverseEdges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input Value: ";
(match c.t.inputVal with
Some i -> Printf.fprintf ppf "%d" i;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input and Output Vars: ";
(match c.t.inputOutputVar with
Some (i, o) -> Printf.fprintf ppf "(in: %s, out: %s)" i o;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Initial node's id: ";
(match c.t.initial with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Terminal node's id: ";
(match c.t.terminal with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Code:\n";
List.iter (fun ((n, stms) : Node.t * elt list) : unit ->
Printf.fprintf ppf "\tid %d --> %a\n%!" n.id M.pplist stms
) (NodeMap.to_list c.t.content);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Analysis structure:\n";
List.iter (fun ((n, {internalin; internalout; internalbetween})
: (Node.t * internalnode)) : unit ->
Printf.fprintf ppf "Node: %d\n" n.id;
Printf.fprintf ppf "Internal Input: ";
Printf.fprintf ppf "%a\n" I.pplist internalin;
Printf.fprintf ppf "Internal Output: ";
Printf.fprintf ppf "%a\n" I.pplist internalout;
Printf.fprintf ppf "Internal Between: ";
List.iter (Printf.fprintf ppf "%a;" I.pplist) internalbetween;
Printf.fprintf ppf "\n";
) (NodeMap.to_list c.internalvar);
end