elvis/lci
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added back edges to cfg

Browse Source
This commit is contained in:
elvis
2024-11-18 15:56:53 +01:00
parent 57f32da348
commit b64108ba69
1 changed files with 29 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
lib/miniImp/Cfg.ml
View File

@ -83,6 +83,7 @@ module Cfg = struct
empty: bool; empty: bool;
nodes: NodeSet.t; nodes: NodeSet.t;
edges: (Node.t * (Node.t option)) NodeMap.t; edges: (Node.t * (Node.t option)) NodeMap.t;
reverseedges: (Node.t list) NodeMap.t;
initial: Node.t option; initial: Node.t option;
terminal: Node.t option; terminal: Node.t option;
code: (simpleStatements list) NodeMap.t code: (simpleStatements list) NodeMap.t
@ -92,6 +93,7 @@ module Cfg = struct
{ empty = true; { empty = true;
nodes = NodeSet.empty; nodes = NodeSet.empty;
edges = NodeMap.empty; edges = NodeMap.empty;
reverseedges = NodeMap.empty;
initial = None; initial = None;
terminal = None; terminal = None;
code = NodeMap.empty } code = NodeMap.empty }
@ -114,6 +116,12 @@ module Cfg = struct
NodeMap.add entryNode (cfg1initial, Some cfg2initial) |> NodeMap.add entryNode (cfg1initial, Some cfg2initial) |>
NodeMap.add cfg1terminal (exitNode, None) |> NodeMap.add cfg1terminal (exitNode, None) |>
NodeMap.add cfg2terminal (exitNode, None); NodeMap.add cfg2terminal (exitNode, None);
reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverseedges cfg2.reverseedges |>
NodeMap.add_to_list cfg1initial entryNode |>
NodeMap.add_to_list cfg2initial entryNode |>
NodeMap.add_to_list exitNode cfg1terminal |>
NodeMap.add_to_list exitNode cfg2terminal;
initial = Some entryNode; initial = Some entryNode;
terminal = Some exitNode; terminal = Some exitNode;
code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
@ -134,6 +142,9 @@ module Cfg = struct
edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.") edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.edges cfg2.edges |> cfg1.edges cfg2.edges |>
NodeMap.add cfg1terminal (cfg2initial, None); NodeMap.add cfg1terminal (cfg2initial, None);
reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverseedges cfg2.reverseedges |>
NodeMap.add_to_list cfg2initial cfg1terminal;
initial = Some cfg1initial; initial = Some cfg1initial;
terminal = Some cfg2terminal; terminal = Some cfg2terminal;
code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
@ -146,6 +157,7 @@ module Cfg = struct
{ empty = false; { empty = false;
nodes = NodeSet.singleton newnode; nodes = NodeSet.singleton newnode;
edges = NodeMap.empty; edges = NodeMap.empty;
reverseedges = NodeMap.empty;
initial = Some newnode; initial = Some newnode;
terminal = Some newnode; terminal = Some newnode;
code = NodeMap.singleton newnode [newcode] code = NodeMap.singleton newnode [newcode]
@ -170,6 +182,14 @@ module Cfg = struct
) (NodeMap.to_list c.edges); ) (NodeMap.to_list c.edges);
Printf.fprintf ppf "\n"; 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.reverseedges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Initial node's id: "; Printf.fprintf ppf "Initial node's id: ";
Printf.fprintf ppf "%d" ((Option.get c.initial).id); Printf.fprintf ppf "%d" ((Option.get c.initial).id);
Printf.fprintf ppf "\n"; Printf.fprintf ppf "\n";
@ -224,6 +244,11 @@ let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t =
NodeMap.add entrynode (guardnode, None) |> NodeMap.add entrynode (guardnode, None) |>
NodeMap.add guardnode (cfginitial, Some exitnode) |> NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None); NodeMap.add cfgterminal (guardnode, None);
reverseedges = cfg.reverseedges |>
NodeMap.add_to_list guardnode entrynode |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
initial = Some entrynode; initial = Some entrynode;
terminal = Some exitnode; terminal = Some exitnode;
code = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.code |> code = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.code |>
@ -250,6 +275,10 @@ let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t =
edges = bodyincrement.edges |> edges = bodyincrement.edges |>
NodeMap.add guardnode (cfginitial, Some exitnode) |> NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None); NodeMap.add cfgterminal (guardnode, None);
reverseedges = bodyincrement.reverseedges |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
initial = Some guardnode; initial = Some guardnode;
terminal = Some exitnode; terminal = Some exitnode;
code = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.code |> code = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.code |>