From 4e9f08347bb4cae6f35dc2e1ddd578e3c42c54f4 Mon Sep 17 00:00:00 2001 From: elvis Date: Thu, 21 Nov 2024 18:30:19 +0100 Subject: [PATCH] Changed from type to module for cfg and moved to separate lib --- bin/main.ml | 4 +- dune-project | 4 + lib/cfg/Cfg.ml | 199 ++++++++++++++++++++++++++ lib/cfg/Cfg.mli | 38 +++++ lib/cfg/dune | 5 + lib/miniImp/Cfg.ml | 316 ----------------------------------------- lib/miniImp/Cfg.mli | 40 ------ lib/miniImp/CfgImp.ml | 182 ++++++++++++++++++++++++ lib/miniImp/CfgImp.mli | 34 +++++ lib/miniImp/dune | 4 +- 10 files changed, 466 insertions(+), 360 deletions(-) create mode 100644 lib/cfg/Cfg.ml create mode 100644 lib/cfg/Cfg.mli create mode 100644 lib/cfg/dune delete mode 100644 lib/miniImp/Cfg.ml delete mode 100644 lib/miniImp/Cfg.mli create mode 100644 lib/miniImp/CfgImp.ml create mode 100644 lib/miniImp/CfgImp.mli diff --git a/bin/main.ml b/bin/main.ml index 9d63d55..832d583 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,5 +1,5 @@ open MiniImp -open MiniImp.Cfg +open MiniImp.CfgImp let () = let program = "def main with input x output y as @@ -17,4 +17,4 @@ let () = let converted = convert p in - Printf.printf "%a" Cfg.pp converted + Printf.printf "%a" SSCfg.pp converted diff --git a/dune-project b/dune-project index 900aba8..bbe1b2e 100644 --- a/dune-project +++ b/dune-project @@ -10,6 +10,10 @@ (name utility) (depends ocaml dune)) +(package + (name cfg) + (depends ocaml dune)) + (package (name miniImp) (depends ocaml dune utility)) diff --git a/lib/cfg/Cfg.ml b/lib/cfg/Cfg.ml new file mode 100644 index 0000000..b0b61e2 --- /dev/null +++ b/lib/cfg/Cfg.ml @@ -0,0 +1,199 @@ +module type PrintableType = sig + type t + val pp : out_channel -> t -> unit + val pplist : out_channel -> t list -> unit +end + +let globalIdNode = ref 0; + +module Node = struct + type t = { + id: int + } + let compare a b = compare a.id b.id + + let create () = + globalIdNode := !globalIdNode + 1; + {id = !globalIdNode} +end +;; + +module NodeMap = Map.Make(Node) +module NodeSet = Set.Make(Node) + +module type C = sig + type elt + type t = { + empty: bool; + nodes: NodeSet.t; + edges: (Node.t * (Node.t option)) NodeMap.t; + reverseEdges: (Node.t list) NodeMap.t; + inputVal: elt option; + outputVal: elt option; + initial: Node.t option; + terminal: Node.t option; + content: elt list NodeMap.t + } + + val create : unit -> t + val merge : t -> t -> Node.t -> Node.t -> t + val concat : t -> t -> t + val addToLastNode : elt -> t -> t + + val pp : out_channel -> t -> unit +end + +module Make(M: PrintableType) = struct + type elt = M.t + type t = { + empty: bool; + nodes: NodeSet.t; + edges: (Node.t * (Node.t option)) NodeMap.t; + reverseEdges: (Node.t list) NodeMap.t; + inputVal: elt option; + outputVal: elt option; + initial: Node.t option; + terminal: Node.t option; + content: elt list NodeMap.t + } + + let create () : t = + { empty = true; + nodes = NodeSet.empty; + edges = NodeMap.empty; + reverseEdges = NodeMap.empty; + inputVal = None; + outputVal = None; + initial = None; + terminal = None; + content = NodeMap.empty } + + let merge (cfg1: t) (cfg2: t) (entryNode: Node.t) (exitNode: Node.t) : t = + match (cfg1.empty, cfg2.empty) with + true, _ -> cfg2 + | _, true -> cfg1 + | false, false -> + let cfg1initial = Option.get cfg1.initial in + let cfg2initial = Option.get cfg2.initial in + let cfg1terminal = Option.get cfg1.terminal in + let cfg2terminal = Option.get cfg2.terminal in + { empty = false; + nodes = NodeSet.union cfg1.nodes cfg2.nodes |> + NodeSet.add entryNode |> + NodeSet.add exitNode; + edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.") + cfg1.edges cfg2.edges |> + NodeMap.add entryNode (cfg1initial, Some cfg2initial) |> + NodeMap.add cfg1terminal (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; + inputVal = cfg1.inputVal; + outputVal = cfg1.outputVal; + initial = Some entryNode; + terminal = Some exitNode; + content = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") + cfg1.content cfg2.content + } + + let concat (cfg1: t) (cfg2: t) : t = + match (cfg1.empty, cfg2.empty) with + true, _ -> cfg2 + | _, true -> cfg1 + | false, false -> + let cfg1initial = Option.get cfg1.initial in + let cfg2initial = Option.get cfg2.initial in + let cfg1terminal = Option.get cfg1.terminal in + let cfg2terminal = Option.get cfg2.terminal in + { empty = false; + nodes = NodeSet.union cfg1.nodes cfg2.nodes; + edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.") + cfg1.edges cfg2.edges |> + 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; + inputVal = cfg1.inputVal; + outputVal = cfg1.outputVal; + initial = Some cfg1initial; + terminal = Some cfg2terminal; + content = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") + cfg1.content cfg2.content + } + + let addToLastNode (newcontent: elt) (cfg: t) : t = + match cfg.empty with + | true -> let newnode = Node.create () in + { empty = false; + nodes = NodeSet.singleton newnode; + edges = NodeMap.empty; + reverseEdges = NodeMap.empty; + inputVal = None; + outputVal = None; + initial = Some newnode; + terminal = Some newnode; + content = NodeMap.singleton newnode [newcontent] + } + | false -> + let prevcfgterminal = Option.get cfg.terminal in + { cfg with + content = (NodeMap.add_to_list + prevcfgterminal + newcontent + cfg.content) } + + let pp (ppf) (c: t) : unit = + Printf.fprintf ppf "Nodes' ids: "; + List.iter (fun (x : Node.t) -> Printf.fprintf ppf "%d " x.id) (NodeSet.to_list c.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.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.reverseEdges); + Printf.fprintf ppf "\n"; + + Printf.fprintf ppf "Input Value: "; + (match c.inputVal with + Some i -> Printf.fprintf ppf "%a" M.pp (i); + | None -> Printf.fprintf ppf "None";); + Printf.fprintf ppf "\n"; + + Printf.fprintf ppf "Output Value: "; + (match c.outputVal with + Some i -> Printf.fprintf ppf "%a" M.pp (i); + | None -> Printf.fprintf ppf "None";); + Printf.fprintf ppf "\n"; + + Printf.fprintf ppf "Initial node's id: "; + (match c.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.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 (List.rev stms) + ) (NodeMap.to_list c.content); + Printf.fprintf ppf "\n"; +end +;; diff --git a/lib/cfg/Cfg.mli b/lib/cfg/Cfg.mli new file mode 100644 index 0000000..6a61e03 --- /dev/null +++ b/lib/cfg/Cfg.mli @@ -0,0 +1,38 @@ +module type PrintableType = sig + type t + val pp : out_channel -> t -> unit + val pplist : out_channel -> t list -> unit +end + +module Node : sig + type t + val compare : t -> t -> int + val create : unit -> t +end + +module NodeMap : Map.S with type key = Node.t +module NodeSet : Set.S with type elt = Node.t + +module type C = sig + type elt + type t = { + empty: bool; + nodes: NodeSet.t; + edges: (Node.t * (Node.t option)) NodeMap.t; + reverseEdges: (Node.t list) NodeMap.t; + inputVal: elt option; + outputVal: elt option; + initial: Node.t option; + terminal: Node.t option; + content: elt list NodeMap.t + } + + val create : unit -> t + val merge : t -> t -> Node.t -> Node.t -> t + val concat : t -> t -> t + val addToLastNode : elt -> t -> t + + val pp : out_channel -> t -> unit +end + +module Make (M: PrintableType) : C with type elt = M.t diff --git a/lib/cfg/dune b/lib/cfg/dune new file mode 100644 index 0000000..772e4a7 --- /dev/null +++ b/lib/cfg/dune @@ -0,0 +1,5 @@ +(library + (name cfg) + (public_name cfg)) + +(include_subdirs qualified) diff --git a/lib/miniImp/Cfg.ml b/lib/miniImp/Cfg.ml deleted file mode 100644 index 7e92de6..0000000 --- a/lib/miniImp/Cfg.ml +++ /dev/null @@ -1,316 +0,0 @@ -type simpleStatements = - | SimpleSkip - | SimpleAssignment of Types.variable * simpleArithmetic - | SimpleGuard of simpleBoolean -and simpleBoolean = - | SimpleBoolean of bool - | SimpleBAnd of simpleBoolean * simpleBoolean - | SimpleBOr of simpleBoolean * simpleBoolean - | SimpleBNot of simpleBoolean - | SimpleBCmp of simpleArithmetic * simpleArithmetic - | SimpleBCmpLess of simpleArithmetic * simpleArithmetic - | SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic - | SimpleBCmpGreater of simpleArithmetic * simpleArithmetic - | SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic -and simpleArithmetic = - | SimpleVariable of Types.variable - | SimpleInteger of int - | SimplePlus of simpleArithmetic * simpleArithmetic - | SimpleMinus of simpleArithmetic * simpleArithmetic - | SimpleTimes of simpleArithmetic * simpleArithmetic - | SimpleDivision of simpleArithmetic * simpleArithmetic - | SimpleModulo of simpleArithmetic * simpleArithmetic - | SimplePower of simpleArithmetic * simpleArithmetic - | SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic - | SimpleRand of simpleArithmetic - -let printSingleStatement (ppf) (c: simpleStatements) : unit = - let rec helper_c (ppf) (c: simpleStatements) : unit = - match c with - | SimpleSkip -> Printf.fprintf ppf "Skip" - | SimpleAssignment (v, a) -> Printf.fprintf ppf "Assignment {%s, %a}" v helper_a a - | SimpleGuard (b) -> Printf.fprintf ppf "Guard {%a}" helper_b b - and helper_b (ppf) (c: simpleBoolean) : unit = - match c with - | SimpleBoolean b -> Printf.fprintf ppf "%b" b - | SimpleBAnd (b1, b2) -> Printf.fprintf ppf "{%a && %a}" helper_b b1 helper_b b2 - | SimpleBOr (b1, b2) -> Printf.fprintf ppf "{%a || %a}" helper_b b1 helper_b b2 - | SimpleBNot b -> Printf.fprintf ppf "{not %a}" helper_b b - | SimpleBCmp (a1, a2) -> Printf.fprintf ppf "{%a == %a}" helper_a a1 helper_a a2 - | SimpleBCmpLess (a1, a2) -> Printf.fprintf ppf "{%a < %a}" helper_a a1 helper_a a2 - | SimpleBCmpLessEq (a1, a2) -> Printf.fprintf ppf "{%a <= %a}" helper_a a1 helper_a a2 - | SimpleBCmpGreater (a1, a2) -> Printf.fprintf ppf "{%a > %a}" helper_a a1 helper_a a2 - | SimpleBCmpGreaterEq (a1, a2) -> Printf.fprintf ppf "{%a >= %a}" helper_a a1 helper_a a2 - and helper_a (ppf) (c: simpleArithmetic) : unit = - match c with - | SimpleVariable (v) -> Printf.fprintf ppf "%s" v - | SimpleInteger (i) -> Printf.fprintf ppf "%d" i - | SimplePlus (a1, a2) -> Printf.fprintf ppf "{%a + %a}" helper_a a1 helper_a a2 - | SimpleMinus (a1, a2) -> Printf.fprintf ppf "{%a - %a}" helper_a a1 helper_a a2 - | SimpleTimes (a1, a2) -> Printf.fprintf ppf "{%a * %a}" helper_a a1 helper_a a2 - | SimpleDivision (a1, a2) -> Printf.fprintf ppf "{%a / %a}" helper_a a1 helper_a a2 - | SimpleModulo (a1, a2) -> Printf.fprintf ppf "{%a %% %a}" helper_a a1 helper_a a2 - | SimplePower (a1, a2) -> Printf.fprintf ppf "{%a ^ %a}" helper_a a1 helper_a a2 - | SimplePowerMod (a1, a2, a3) -> Printf.fprintf ppf "{powmod %a %a %a}" helper_a a1 helper_a a2 helper_a a3 - | SimpleRand (a) -> Printf.fprintf ppf "{rand %a}" helper_a a - in - helper_c ppf c - -let printSimpleStatements (ppf) (c: simpleStatements list) : unit = - List.iter (fun x -> printSingleStatement ppf x; Printf.printf "; ") c - - - -let globalIdNode = ref 0; - -module Node = struct - type t = { - id: int - } - let compare a b = compare a.id b.id - - let newNode () = - globalIdNode := !globalIdNode + 1; - {id = !globalIdNode} -end -;; - -module NodeMap = Map.Make(Node) -module NodeSet = Set.Make(Node) - -module Cfg = struct - type t = { - empty: bool; - nodes: NodeSet.t; - edges: (Node.t * (Node.t option)) NodeMap.t; - reverseedges: (Node.t list) NodeMap.t; - initial: Node.t option; - terminal: Node.t option; - code: (simpleStatements list) NodeMap.t - } - - let newCfg () = - { empty = true; - nodes = NodeSet.empty; - edges = NodeMap.empty; - reverseedges = NodeMap.empty; - initial = None; - terminal = None; - code = NodeMap.empty } - - let mergeCfg (cfg1: t) (cfg2: t) (entryNode: Node.t) (exitNode: Node.t) : t = - match (cfg1.empty, cfg2.empty) with - true, _ -> cfg2 - | _, true -> cfg1 - | false, false -> - let cfg1initial = Option.get cfg1.initial in - let cfg2initial = Option.get cfg2.initial in - let cfg1terminal = Option.get cfg1.terminal in - let cfg2terminal = Option.get cfg2.terminal in - { empty = false; - nodes = NodeSet.union cfg1.nodes cfg2.nodes |> - NodeSet.add entryNode |> - NodeSet.add exitNode; - edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.") - cfg1.edges cfg2.edges |> - NodeMap.add entryNode (cfg1initial, Some cfg2initial) |> - NodeMap.add cfg1terminal (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; - terminal = Some exitNode; - code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") - cfg1.code cfg2.code - } - - let concatCfg (cfg1: t) (cfg2: t) : t = - match (cfg1.empty, cfg2.empty) with - true, _ -> cfg2 - | _, true -> cfg1 - | false, false -> - let cfg1initial = Option.get cfg1.initial in - let cfg2initial = Option.get cfg2.initial in - let cfg1terminal = Option.get cfg1.terminal in - let cfg2terminal = Option.get cfg2.terminal in - { empty = false; - nodes = NodeSet.union cfg1.nodes cfg2.nodes; - edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.") - cfg1.edges cfg2.edges |> - 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; - terminal = Some cfg2terminal; - code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.") - cfg1.code cfg2.code - } - - let addToLastNode (newcode: simpleStatements) (cfg: t) : t = - match cfg.empty with - | true -> let newnode = Node.newNode () in - { empty = false; - nodes = NodeSet.singleton newnode; - edges = NodeMap.empty; - reverseedges = NodeMap.empty; - initial = Some newnode; - terminal = Some newnode; - code = NodeMap.singleton newnode [newcode] - } - | false -> - let prevcfgterminal = Option.get cfg.terminal in - { cfg with - code = (NodeMap.add_to_list - prevcfgterminal - newcode - cfg.code) } - - let pp (ppf) (c: t) : unit = - Printf.fprintf ppf "Nodes' ids: "; - List.iter (fun (x : Node.t) -> Printf.fprintf ppf "%d " x.id) (NodeSet.to_list c.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.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.reverseedges); - Printf.fprintf ppf "\n"; - - Printf.fprintf ppf "Initial node's id: "; - Printf.fprintf ppf "%d" ((Option.get c.initial).id); - Printf.fprintf ppf "\n"; - - Printf.fprintf ppf "Terminal node's id: "; - Printf.fprintf ppf "%d" ((Option.get c.terminal).id); - Printf.fprintf ppf "\n"; - - Printf.fprintf ppf "Code:\n"; - List.iter (fun ((n, stms) : Node.t * simpleStatements list) : unit -> - Printf.fprintf ppf "\tid %d --> %a\n%!" n.id printSimpleStatements (List.rev stms) - ) (NodeMap.to_list c.code); - Printf.fprintf ppf "\n"; -end -;; - - -let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t = - match prg with - | Skip -> prevcfg |> Cfg.addToLastNode SimpleSkip - | Assignment (x, a) -> prevcfg |> Cfg.addToLastNode (SimpleAssignment (x, convert_a a)) - | Sequence (c1, c2) -> - let cfg1 = convert_c prevcfg c1 in - let cfg2 = convert_c cfg1 c2 in - cfg2 - | If (b, c1, c2) -> - let convertedb = convert_b b in - let cfg1 = convert_c (Cfg.newCfg ()) c1 in - let cfg2 = convert_c (Cfg.newCfg ()) c2 in - let entrynode = Node.newNode () in - let exitnode = Node.newNode () in - let newcfg = Cfg.mergeCfg cfg1 cfg2 entrynode exitnode in - let mergedcfg = Cfg.concatCfg prevcfg newcfg in - { mergedcfg with - code = mergedcfg.code |> - NodeMap.add_to_list entrynode (SimpleGuard convertedb) |> - NodeMap.add_to_list exitnode (SimpleSkip) } - | While (b, c) -> - let convertedb = convert_b b in - let cfg = convert_c (Cfg.newCfg ()) c in - let cfginitial = Option.get cfg.initial in - let cfgterminal = Option.get cfg.terminal in - let entrynode = Node.newNode () in - let guardnode = Node.newNode () in - let exitnode = Node.newNode () in - { empty = false; - nodes = cfg.nodes |> - NodeSet.add entrynode |> - NodeSet.add guardnode |> - NodeSet.add exitnode; - edges = cfg.edges |> - NodeMap.add entrynode (guardnode, None) |> - NodeMap.add guardnode (cfginitial, Some exitnode) |> - 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; - terminal = Some exitnode; - code = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.code |> - NodeMap.add_to_list exitnode (SimpleSkip) - } |> Cfg.concatCfg prevcfg - | For (assignment, guard, increment, body) -> - let cfgassignment = convert_c (Cfg.newCfg ()) assignment in - let convertedguard = convert_b guard in - let cfgincrement = convert_c (Cfg.newCfg ()) increment in - let cfgbody = convert_c (Cfg.newCfg ()) body in - - let prevassignment = Cfg.concatCfg prevcfg cfgassignment in - let bodyincrement = Cfg.concatCfg cfgbody cfgincrement in - - let cfginitial = Option.get bodyincrement.initial in - let cfgterminal = Option.get bodyincrement.terminal in - - let guardnode = Node.newNode () in - let exitnode = Node.newNode () in - { empty = false; - nodes = bodyincrement.nodes |> - NodeSet.add guardnode |> - NodeSet.add exitnode; - edges = bodyincrement.edges |> - NodeMap.add guardnode (cfginitial, Some exitnode) |> - 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; - terminal = Some exitnode; - code = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.code |> - NodeMap.add_to_list exitnode (SimpleSkip) - } |> Cfg.concatCfg prevassignment - -and convert_b (prg: Types.b_exp) : simpleBoolean = - match prg with - | Boolean (b) -> SimpleBoolean b - | BAnd (b1, b2) -> SimpleBAnd (convert_b b1, convert_b b2) - | BOr (b1, b2) -> SimpleBOr (convert_b b1, convert_b b2) - | BNot (b) -> SimpleBNot (convert_b b) - | BCmp (a1, a2) -> SimpleBCmp (convert_a a1, convert_a a2) - | BCmpLess (a1, a2) -> SimpleBCmpLess (convert_a a1, convert_a a2) - | BCmpLessEq (a1, a2) -> SimpleBCmpLessEq (convert_a a1, convert_a a2) - | BCmpGreater (a1, a2) -> SimpleBCmpGreater (convert_a a1, convert_a a2) - | BCmpGreaterEq (a1, a2) -> SimpleBCmpGreaterEq (convert_a a1, convert_a a2) - -and convert_a (prg: Types.a_exp) : simpleArithmetic = - match prg with - | Variable x -> SimpleVariable x - | Integer n -> SimpleInteger n - | Plus (a1, a2) -> SimplePlus (convert_a a1, convert_a a2) - | Minus (a1, a2) -> SimpleMinus (convert_a a1, convert_a a2) - | Times (a1, a2) -> SimpleTimes (convert_a a1, convert_a a2) - | Division (a1, a2) -> SimpleDivision (convert_a a1, convert_a a2) - | Modulo (a1, a2) -> SimpleModulo (convert_a a1, convert_a a2) - | Power (a1, a2) -> SimplePower (convert_a a1, convert_a a2) - | PowerMod (a1, a2, a3) -> SimplePowerMod (convert_a a1, convert_a a2, convert_a a3) - | Rand (a) -> SimpleRand (convert_a a) - -let convert (prg: Types.p_exp) : Cfg.t = - match prg with - | Main (_, _, exp) -> - convert_c (Cfg.newCfg ()) exp diff --git a/lib/miniImp/Cfg.mli b/lib/miniImp/Cfg.mli deleted file mode 100644 index 46a0f7a..0000000 --- a/lib/miniImp/Cfg.mli +++ /dev/null @@ -1,40 +0,0 @@ -type simpleStatements = - | SimpleSkip - | SimpleAssignment of Types.variable * simpleArithmetic - | SimpleGuard of simpleBoolean -and simpleBoolean = - | SimpleBoolean of bool - | SimpleBAnd of simpleBoolean * simpleBoolean - | SimpleBOr of simpleBoolean * simpleBoolean - | SimpleBNot of simpleBoolean - | SimpleBCmp of simpleArithmetic * simpleArithmetic - | SimpleBCmpLess of simpleArithmetic * simpleArithmetic - | SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic - | SimpleBCmpGreater of simpleArithmetic * simpleArithmetic - | SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic -and simpleArithmetic = - | SimpleVariable of Types.variable - | SimpleInteger of int - | SimplePlus of simpleArithmetic * simpleArithmetic - | SimpleMinus of simpleArithmetic * simpleArithmetic - | SimpleTimes of simpleArithmetic * simpleArithmetic - | SimpleDivision of simpleArithmetic * simpleArithmetic - | SimpleModulo of simpleArithmetic * simpleArithmetic - | SimplePower of simpleArithmetic * simpleArithmetic - | SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic - | SimpleRand of simpleArithmetic - -module Node : sig - type t - val compare : t -> t -> int -end - -module NodeMap : Map.S with type key = Node.t -module NodeSet : Set.S with type elt = Node.t - -module Cfg : sig - type t - val pp : out_channel -> t -> unit -end - -val convert : Types.p_exp -> Cfg.t diff --git a/lib/miniImp/CfgImp.ml b/lib/miniImp/CfgImp.ml new file mode 100644 index 0000000..be8db0e --- /dev/null +++ b/lib/miniImp/CfgImp.ml @@ -0,0 +1,182 @@ +open Cfg + +module SimpleStatements = struct + type t = + | SimpleSkip + | SimpleAssignment of Types.variable * simpleArithmetic + | SimpleGuard of simpleBoolean + and simpleBoolean = + | SimpleBoolean of bool + | SimpleBAnd of simpleBoolean * simpleBoolean + | SimpleBOr of simpleBoolean * simpleBoolean + | SimpleBNot of simpleBoolean + | SimpleBCmp of simpleArithmetic * simpleArithmetic + | SimpleBCmpLess of simpleArithmetic * simpleArithmetic + | SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic + | SimpleBCmpGreater of simpleArithmetic * simpleArithmetic + | SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic + and simpleArithmetic = + | SimpleVariable of Types.variable + | SimpleInteger of int + | SimplePlus of simpleArithmetic * simpleArithmetic + | SimpleMinus of simpleArithmetic * simpleArithmetic + | SimpleTimes of simpleArithmetic * simpleArithmetic + | SimpleDivision of simpleArithmetic * simpleArithmetic + | SimpleModulo of simpleArithmetic * simpleArithmetic + | SimplePower of simpleArithmetic * simpleArithmetic + | SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic + | SimpleRand of simpleArithmetic + + let pp (ppf: out_channel) (c: t) : unit = + let rec helper_c (ppf) (c: t) : unit = + match c with + | SimpleSkip -> Printf.fprintf ppf "Skip" + | SimpleAssignment (v, a) -> Printf.fprintf ppf "Assignment {%s, %a}" v helper_a a + | SimpleGuard (b) -> Printf.fprintf ppf "Guard {%a}" helper_b b + and helper_b (ppf) (c: simpleBoolean) : unit = + match c with + | SimpleBoolean b -> Printf.fprintf ppf "%b" b + | SimpleBAnd (b1, b2) -> Printf.fprintf ppf "{%a && %a}" helper_b b1 helper_b b2 + | SimpleBOr (b1, b2) -> Printf.fprintf ppf "{%a || %a}" helper_b b1 helper_b b2 + | SimpleBNot b -> Printf.fprintf ppf "{not %a}" helper_b b + | SimpleBCmp (a1, a2) -> Printf.fprintf ppf "{%a == %a}" helper_a a1 helper_a a2 + | SimpleBCmpLess (a1, a2) -> Printf.fprintf ppf "{%a < %a}" helper_a a1 helper_a a2 + | SimpleBCmpLessEq (a1, a2) -> Printf.fprintf ppf "{%a <= %a}" helper_a a1 helper_a a2 + | SimpleBCmpGreater (a1, a2) -> Printf.fprintf ppf "{%a > %a}" helper_a a1 helper_a a2 + | SimpleBCmpGreaterEq (a1, a2) -> Printf.fprintf ppf "{%a >= %a}" helper_a a1 helper_a a2 + and helper_a (ppf) (c: simpleArithmetic) : unit = + match c with + | SimpleVariable (v) -> Printf.fprintf ppf "%s" v + | SimpleInteger (i) -> Printf.fprintf ppf "%d" i + | SimplePlus (a1, a2) -> Printf.fprintf ppf "{%a + %a}" helper_a a1 helper_a a2 + | SimpleMinus (a1, a2) -> Printf.fprintf ppf "{%a - %a}" helper_a a1 helper_a a2 + | SimpleTimes (a1, a2) -> Printf.fprintf ppf "{%a * %a}" helper_a a1 helper_a a2 + | SimpleDivision (a1, a2) -> Printf.fprintf ppf "{%a / %a}" helper_a a1 helper_a a2 + | SimpleModulo (a1, a2) -> Printf.fprintf ppf "{%a %% %a}" helper_a a1 helper_a a2 + | SimplePower (a1, a2) -> Printf.fprintf ppf "{%a ^ %a}" helper_a a1 helper_a a2 + | SimplePowerMod (a1, a2, a3) -> Printf.fprintf ppf "{powmod %a %a %a}" helper_a a1 helper_a a2 helper_a a3 + | SimpleRand (a) -> Printf.fprintf ppf "{rand %a}" helper_a a + in + helper_c ppf c + + let pplist (ppf: out_channel) (c: t list) : unit = + List.iter (fun x -> pp ppf x; Printf.printf "; ") c +end + +module SSCfg = Cfg.Make(SimpleStatements) + +let rec convert_c (prevcfg: SSCfg.t) (prg: Types.c_exp) : SSCfg.t = + let open SimpleStatements in + match prg with + | Skip -> prevcfg |> SSCfg.addToLastNode SimpleSkip + | Assignment (x, a) -> prevcfg |> SSCfg.addToLastNode (SimpleAssignment (x, convert_a a)) + | Sequence (c1, c2) -> + let cfg1 = convert_c prevcfg c1 in + let cfg2 = convert_c cfg1 c2 in + cfg2 + | If (b, c1, c2) -> + let convertedb = convert_b b in + let cfg1 = convert_c (SSCfg.create ()) c1 in + let cfg2 = convert_c (SSCfg.create ()) c2 in + let entrynode = Node.create () in + let exitnode = Node.create () in + let newcfg = SSCfg.merge cfg1 cfg2 entrynode exitnode in + let mergedcfg = SSCfg.concat prevcfg newcfg in + { mergedcfg with + content = mergedcfg.content |> + NodeMap.add_to_list entrynode (SimpleGuard convertedb) |> + NodeMap.add_to_list exitnode (SimpleSkip) } + | While (b, c) -> + let convertedb = convert_b b in + let cfg = convert_c (SSCfg.create ()) c in + let cfginitial = Option.get cfg.initial in + let cfgterminal = Option.get cfg.terminal in + let entrynode = Node.create () in + let guardnode = Node.create () in + let exitnode = Node.create () in + { empty = false; + nodes = cfg.nodes |> + NodeSet.add entrynode |> + NodeSet.add guardnode |> + NodeSet.add exitnode; + edges = cfg.edges |> + NodeMap.add entrynode (guardnode, None) |> + NodeMap.add guardnode (cfginitial, Some exitnode) |> + 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; + inputVal = prevcfg.inputVal; + outputVal = prevcfg.outputVal; + initial = Some entrynode; + terminal = Some exitnode; + content = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.content |> + NodeMap.add_to_list exitnode (SimpleSkip) + } |> SSCfg.concat prevcfg + | For (assignment, guard, increment, body) -> + let cfgassignment = convert_c (SSCfg.create ()) assignment in + let convertedguard = convert_b guard in + let cfgincrement = convert_c (SSCfg.create ()) increment in + let cfgbody = convert_c (SSCfg.create ()) body in + + let prevassignment = SSCfg.concat prevcfg cfgassignment in + let bodyincrement = SSCfg.concat cfgbody cfgincrement in + + let cfginitial = Option.get bodyincrement.initial in + let cfgterminal = Option.get bodyincrement.terminal in + + let guardnode = Node.create () in + let exitnode = Node.create () in + { empty = false; + nodes = bodyincrement.nodes |> + NodeSet.add guardnode |> + NodeSet.add exitnode; + edges = bodyincrement.edges |> + NodeMap.add guardnode (cfginitial, Some exitnode) |> + 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; + inputVal = prevcfg.inputVal; + outputVal = prevcfg.outputVal; + initial = Some guardnode; + terminal = Some exitnode; + content = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.content |> + NodeMap.add_to_list exitnode (SimpleSkip) + } |> SSCfg.concat prevassignment + +and convert_b (prg: Types.b_exp) : SimpleStatements.simpleBoolean = + match prg with + | Boolean (b) -> SimpleBoolean b + | BAnd (b1, b2) -> SimpleBAnd (convert_b b1, convert_b b2) + | BOr (b1, b2) -> SimpleBOr (convert_b b1, convert_b b2) + | BNot (b) -> SimpleBNot (convert_b b) + | BCmp (a1, a2) -> SimpleBCmp (convert_a a1, convert_a a2) + | BCmpLess (a1, a2) -> SimpleBCmpLess (convert_a a1, convert_a a2) + | BCmpLessEq (a1, a2) -> SimpleBCmpLessEq (convert_a a1, convert_a a2) + | BCmpGreater (a1, a2) -> SimpleBCmpGreater (convert_a a1, convert_a a2) + | BCmpGreaterEq (a1, a2) -> SimpleBCmpGreaterEq (convert_a a1, convert_a a2) + +and convert_a (prg: Types.a_exp) : SimpleStatements.simpleArithmetic = + match prg with + | Variable x -> SimpleVariable x + | Integer n -> SimpleInteger n + | Plus (a1, a2) -> SimplePlus (convert_a a1, convert_a a2) + | Minus (a1, a2) -> SimpleMinus (convert_a a1, convert_a a2) + | Times (a1, a2) -> SimpleTimes (convert_a a1, convert_a a2) + | Division (a1, a2) -> SimpleDivision (convert_a a1, convert_a a2) + | Modulo (a1, a2) -> SimpleModulo (convert_a a1, convert_a a2) + | Power (a1, a2) -> SimplePower (convert_a a1, convert_a a2) + | PowerMod (a1, a2, a3) -> SimplePowerMod (convert_a a1, convert_a a2, convert_a a3) + | Rand (a) -> SimpleRand (convert_a a) + +let convert (prg: Types.p_exp) : SSCfg.t = + let result = + match prg with + | Main (_, _, exp) -> + convert_c (SSCfg.create ()) exp + in + {result with inputVal = None; outputVal = None} diff --git a/lib/miniImp/CfgImp.mli b/lib/miniImp/CfgImp.mli new file mode 100644 index 0000000..6f73010 --- /dev/null +++ b/lib/miniImp/CfgImp.mli @@ -0,0 +1,34 @@ +module SimpleStatements : sig + type t = + | SimpleSkip + | SimpleAssignment of Types.variable * simpleArithmetic + | SimpleGuard of simpleBoolean + and simpleBoolean = + | SimpleBoolean of bool + | SimpleBAnd of simpleBoolean * simpleBoolean + | SimpleBOr of simpleBoolean * simpleBoolean + | SimpleBNot of simpleBoolean + | SimpleBCmp of simpleArithmetic * simpleArithmetic + | SimpleBCmpLess of simpleArithmetic * simpleArithmetic + | SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic + | SimpleBCmpGreater of simpleArithmetic * simpleArithmetic + | SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic + and simpleArithmetic = + | SimpleVariable of Types.variable + | SimpleInteger of int + | SimplePlus of simpleArithmetic * simpleArithmetic + | SimpleMinus of simpleArithmetic * simpleArithmetic + | SimpleTimes of simpleArithmetic * simpleArithmetic + | SimpleDivision of simpleArithmetic * simpleArithmetic + | SimpleModulo of simpleArithmetic * simpleArithmetic + | SimplePower of simpleArithmetic * simpleArithmetic + | SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic + | SimpleRand of simpleArithmetic + + val pp : out_channel -> t -> unit + val pplist : out_channel -> t list -> unit +end + +module SSCfg : Cfg.C with type elt = SimpleStatements.t + +val convert : Types.p_exp -> SSCfg.t diff --git a/lib/miniImp/dune b/lib/miniImp/dune index 37cb1c9..ffeaddc 100644 --- a/lib/miniImp/dune +++ b/lib/miniImp/dune @@ -10,7 +10,7 @@ (library (name miniImp) (public_name miniImp) - (modules Lexer Parser Types Semantics Cfg) - (libraries utility menhirLib)) + (modules Lexer Parser Types Semantics CfgImp) + (libraries cfg utility menhirLib)) (include_subdirs qualified)