From 25f9f12525d6ddaeeeb9cbbbda098b9515f05f11 Mon Sep 17 00:00:00 2001
From: elvis <elvilio98@gmail.com>
Date: Mon, 16 Dec 2024 05:15:33 +0100
Subject: [PATCH] Defined variables module, not fully working

---
 bin/main.ml                      |  20 ++-
 lib/analysis/Dataflow.ml         |  25 +++-
 lib/analysis/Dataflow.mli        |   2 +-
 lib/miniImp/CfgRISC.ml           |  36 ++---
 lib/miniImp/CfgRISC.mli          |   2 +-
 lib/miniImp/RISC.ml              |  12 +-
 lib/miniImp/RISC.mli             |   2 +-
 lib/miniImp/RISCSemantics.ml     |   4 +-
 lib/miniImp/definedVariables.ml  | 238 ++++++++++++++++++++++++++++++-
 lib/miniImp/definedVariables.mli |   4 +
 lib/utility/utility.ml           | 107 +++++++++++++-
 lib/utility/utility.mli          |  33 +++--
 12 files changed, 435 insertions(+), 50 deletions(-)

diff --git a/bin/main.ml b/bin/main.ml
index cdfc151..86c7546 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -5,10 +5,13 @@ let colorred s =
 
 let () =
   let program = "
-def main with input a output b as
-  b := 1;
-  for (i := 1, i <= a, i := i + 1) do
-    b := b * i;
+def main with input n output result as
+    result := 0;
+    s := 0;
+    while (0 == ((n - 1) / (2 ^ s)) % 2) do (
+      s := s + 1
+    );
+
 "
   in
 
@@ -34,17 +37,22 @@ def main with input a output b as
 
   Printf.printf "%s\n%a" (colorred "Analysis CFG is") DefinedVariables.DVCfg.pp analysiscfg;
 
+  Printf.printf "%s%b\n" (colorred "Analysis CFG defined variables: ") (DefinedVariables.check_defined_variables analysiscfg);
+  Printf.printf "%s\n" (colorred "Undefined Variables are:");
+  List.iter (fun v -> Printf.printf "%a, " DefinedVariables.Variable.pp v)  (DefinedVariables.undefined_variables analysiscfg);
+  Printf.printf "\n";
+
   let convertedrisccfg = DefinedVariables.compute_cfg analysiscfg in
 
   Printf.printf "%s\n%a" (colorred "Converted RISC after analysis CFG is") CfgRISC.RISCCfg.pp convertedrisccfg;
 
   (* ---------------------------------- *)
 
-  let risc = RISC.convert convertedrisccfg in
+  let _risc = RISC.convert convertedrisccfg in
 
   (* Printf.printf "%s\n%a" (colorred "RISC code is") RISC.RISCAssembly.pp risc; *)
 
-  let _computerisc = RISCSemantics.reduce risc in
+  (* let computerisc = RISCSemantics.reduce risc in *)
 
   (* Printf.printf "%s\n%d\n" (colorred "Output of RISC code is") computerisc; *)
 
diff --git a/lib/analysis/Dataflow.ml b/lib/analysis/Dataflow.ml
index f9041da..ace70be 100644
--- a/lib/analysis/Dataflow.ml
+++ b/lib/analysis/Dataflow.ml
@@ -5,7 +5,7 @@ module type C = sig
   type internalnode = {
     internalin: internal list;
     internalout: internal list;
-    internalbetween: internal list list;
+    internalbetween: (internal list * internal list) list;
   }
 
   type cfgt = elt Cfg.cfginternal
@@ -30,7 +30,7 @@ module Make (M: Cfg.PrintableType) (I: Cfg.PrintableType) = struct
   type internalnode = {
     internalin: internal list;
     internalout: internal list;
-    internalbetween: internal list list;
+    internalbetween: (internal list * internal list) list;
   }
 
   type cfgt = elt Cfg.cfginternal
@@ -66,7 +66,19 @@ module Make (M: Cfg.PrintableType) (I: Cfg.PrintableType) = struct
       in
       if newt = t then newt else helper newt
     in
-    helper { t with internalvar = Cfg.NodeMap.map init t.t.content }
+    let content = List.fold_left
+        (fun cfg node -> Cfg.NodeMap.add node {internalin = [];
+                                               internalout = [];
+                                               internalbetween = []} cfg)
+        Cfg.NodeMap.empty
+        (Cfg.NodeSet.to_list t.t.nodes)
+    in
+    let content = Cfg.NodeMap.union
+        (fun _ket _empty code -> Some code)
+        content
+        (Cfg.NodeMap.map init t.t.content)
+    in
+    helper { t with internalvar = content }
 
 
   open Cfg
@@ -130,7 +142,10 @@ module Make (M: Cfg.PrintableType) (I: Cfg.PrintableType) = struct
                 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;
+                List.iter (fun (i, o) ->
+                    Printf.fprintf ppf "IN: %a;" I.pplist i;
+                    Printf.fprintf ppf "OUT: %a;" I.pplist o;) internalbetween;
                 Printf.fprintf ppf "\n";
-      ) (NodeMap.to_list c.internalvar);
+              ) (NodeMap.to_list c.internalvar);
+    Printf.fprintf ppf "\n";
 end
diff --git a/lib/analysis/Dataflow.mli b/lib/analysis/Dataflow.mli
index 6b2173a..f45667f 100644
--- a/lib/analysis/Dataflow.mli
+++ b/lib/analysis/Dataflow.mli
@@ -5,7 +5,7 @@ module type C = sig
   type internalnode = {
     internalin: internal list;
     internalout: internal list;
-    internalbetween: internal list list;
+    internalbetween: (internal list * internal list) list;
   }
 
   type cfgt = elt Cfg.cfginternal
diff --git a/lib/miniImp/CfgRISC.ml b/lib/miniImp/CfgRISC.ml
index ca51e35..f85fda2 100644
--- a/lib/miniImp/CfgRISC.ml
+++ b/lib/miniImp/CfgRISC.ml
@@ -11,7 +11,7 @@ module RISCSimpleStatements = struct
     | BImmOp of biop * register * int * register
     | URegOp of urop * register * register
     | Load of register * register
-    | LoadI of register * int
+    | LoadI of int * register
     | Store of register * register
   and brop =
     | Add
@@ -54,7 +54,7 @@ module RISCSimpleStatements = struct
       | BImmOp (b, r1, i, r3)  -> Printf.fprintf ppf "%a r%s %d => r%s" pp_biop b r1.index i r3.index
       | URegOp (u, r1, r2) -> Printf.fprintf ppf "%a r%s => r%s" pp_urop u r1.index r2.index
       | Load (r1, r2) -> Printf.fprintf ppf "Load r%s => r%s" r1.index r2.index
-      | LoadI (r2, i) -> Printf.fprintf ppf "LoadI %d => r%s" i r2.index
+      | LoadI (i, r2) -> Printf.fprintf ppf "LoadI %d => r%s" i r2.index
       | Store (r1, r2) -> Printf.fprintf ppf "Store r%s => r%s" r1.index r2.index
     and pp_brop (ppf: out_channel) (v: brop) : unit =
       match v with
@@ -167,9 +167,9 @@ and c_ss_sb
     SimpleBoolean (b) -> (
       let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
       if b then
-        (convertedcode @ [LoadI (partialresreg, 1)], m)
+        (convertedcode @ [LoadI (1, partialresreg)], m)
       else
-        (convertedcode @ [LoadI (partialresreg, 0)], m)
+        (convertedcode @ [LoadI (0, partialresreg)], m)
     )
   | SimpleBAnd (b1, b2) -> (
       match (b1, b2) with
@@ -179,7 +179,7 @@ and c_ss_sb
         )
       | (SimpleBoolean (false), _)
       | (_, SimpleBoolean (false)) -> (
-          (convertedcode @ [LoadI (register, 0)], m)
+          (convertedcode @ [LoadI (0, register)], m)
         )
       | (_, _) -> (
           let partialresreg1, m, _partialresvar1 = RegisterMap.get_fresh_register m in
@@ -197,7 +197,7 @@ and c_ss_sb
         )
       | (SimpleBoolean (true), _)
       | (_, SimpleBoolean (true)) -> (
-          (LoadI (register, 1) :: convertedcode, m)
+          (LoadI (1, register) :: convertedcode, m)
         )
       | (_, _) -> (
           let partialresreg1, m, _partialresvar1 = RegisterMap.get_fresh_register m in
@@ -211,9 +211,9 @@ and c_ss_sb
       match (b) with
       | SimpleBoolean (b) -> (
         if b then
-          (LoadI (register, 0) :: convertedcode, m)
+          (LoadI (0, register) :: convertedcode, m)
         else
-          (LoadI (register, 1) :: convertedcode, m)
+          (LoadI (1, register) :: convertedcode, m)
       )
       | _ -> (
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
@@ -450,7 +450,7 @@ and c_ss_sa
       (convertedcode @ [URegOp (Copy, r1, register)], m)
     )
   | SimpleInteger (i) -> (
-      (convertedcode @ [LoadI (register, i)], m)
+      (convertedcode @ [LoadI (i, register)], m)
     )
   | SimplePlus (a1, a2) -> (
       match (a1, a2) with
@@ -490,7 +490,7 @@ and c_ss_sa
       | (SimpleInteger (i), SimpleVariable (x)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
-          (convertedcode @ [LoadI (partialresreg, i); BRegOp (Sub, partialresreg, xreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresreg); BRegOp (Sub, partialresreg, xreg, register)], m)
         )
       | (SimpleVariable (x), SimpleInteger (i)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
@@ -500,7 +500,7 @@ and c_ss_sa
           let partialresregi, m, _partialresvari = RegisterMap.get_fresh_register m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
           let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
-          (convertedcode @ [LoadI (partialresregi, i); BRegOp (Sub, partialresregi, partialresreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresregi); BRegOp (Sub, partialresregi, partialresreg, register)], m)
         )
       | (a, SimpleInteger (i)) -> (
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
@@ -570,7 +570,7 @@ and c_ss_sa
       | (SimpleInteger (i), SimpleVariable (x)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
-          (convertedcode @ [LoadI (partialresreg, i); BRegOp (Div, partialresreg, xreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresreg); BRegOp (Div, partialresreg, xreg, register)], m)
         )
       | (SimpleVariable (x), SimpleInteger (i)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
@@ -580,7 +580,7 @@ and c_ss_sa
           let partialresregi, m, _partialresvari = RegisterMap.get_fresh_register m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
           let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
-          (convertedcode @ [LoadI (partialresregi, i); BRegOp (Div, partialresregi, partialresreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresregi); BRegOp (Div, partialresregi, partialresreg, register)], m)
         )
       | (a, SimpleInteger (i)) -> (
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
@@ -617,7 +617,7 @@ and c_ss_sa
       | (SimpleInteger (i), SimpleVariable (x)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
-          (convertedcode @ [LoadI (partialresreg, i); BRegOp (Mod, partialresreg, xreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresreg); BRegOp (Mod, partialresreg, xreg, register)], m)
         )
       | (SimpleVariable (x), SimpleInteger (i)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
@@ -627,7 +627,7 @@ and c_ss_sa
           let partialresregi, m, _partialresvari = RegisterMap.get_fresh_register m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
           let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
-          (convertedcode @ [LoadI (partialresregi, i); BRegOp (Mod, partialresregi, partialresreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresregi); BRegOp (Mod, partialresregi, partialresreg, register)], m)
         )
       | (a, SimpleInteger (i)) -> (
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
@@ -664,7 +664,7 @@ and c_ss_sa
       | (SimpleInteger (i), SimpleVariable (x)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
-          (convertedcode @ [LoadI (partialresreg, i); BRegOp (Pow, partialresreg, xreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresreg); BRegOp (Pow, partialresreg, xreg, register)], m)
         )
       | (SimpleVariable (x), SimpleInteger (i)) -> (
           let xreg, m = RegisterMap.get_or_set_register x m in
@@ -674,7 +674,7 @@ and c_ss_sa
           let partialresregi, m, _partialresvari = RegisterMap.get_fresh_register m in
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
           let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
-          (convertedcode @ [LoadI (partialresregi, i); BRegOp (Pow, partialresregi, partialresreg, register)], m)
+          (convertedcode @ [LoadI (i, partialresregi); BRegOp (Pow, partialresregi, partialresreg, register)], m)
         )
       | (a, SimpleInteger (i)) -> (
           let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
@@ -770,7 +770,7 @@ let convert (prg: CfgImp.SSCfg.t) : RISCCfg.t =
     edges = edges;
     reverseEdges = reverseEdges;
     inputVal = inputVal;
-    inputOutputVar = inputOutputVar;
+    inputOutputVar = Some ("in", "out");
     initial = initial;
     terminal = terminal;
     content = helper content initial_bindings;
diff --git a/lib/miniImp/CfgRISC.mli b/lib/miniImp/CfgRISC.mli
index 2d3d778..53b56d7 100644
--- a/lib/miniImp/CfgRISC.mli
+++ b/lib/miniImp/CfgRISC.mli
@@ -11,7 +11,7 @@ module RISCSimpleStatements : sig
     | BImmOp of biop * register * int * register
     | URegOp of urop * register * register
     | Load of register * register
-    | LoadI of register * int
+    | LoadI of int * register
     | Store of register * register
   and brop =
     | Add
diff --git a/lib/miniImp/RISC.ml b/lib/miniImp/RISC.ml
index 4d59fe2..0480db6 100644
--- a/lib/miniImp/RISC.ml
+++ b/lib/miniImp/RISC.ml
@@ -19,7 +19,7 @@ module RISCAssembly = struct
     | BImmOp of biop * register * int * register
     | URegOp of urop * register * register
     | Load of register * register
-    | LoadI of register * int
+    | LoadI of int * register
     | Store of register * register
     | Jump of label
     | CJump of register * label * label
@@ -70,7 +70,7 @@ module RISCAssembly = struct
       | BImmOp (b, r1, i, r3)  -> Printf.fprintf ppf "\t%a r%s %d => r%s\n" pp_biop b r1.index i r3.index
       | URegOp (u, r1, r2) -> Printf.fprintf ppf "\t%a r%s => r%s\n" pp_urop u r1.index r2.index
       | Load (r1, r2) -> Printf.fprintf ppf "\tLoad r%s => r%s\n" r1.index r2.index
-      | LoadI (r2, i) -> Printf.fprintf ppf "\tLoadI %d => r%s\n" i r2.index
+      | LoadI (i, r2) -> Printf.fprintf ppf "\tLoadI %d => r%s\n" i r2.index
       | Store (r1, r2) -> Printf.fprintf ppf "\tStore r%s => r%s\n" r1.index r2.index
       | Jump (label) -> Printf.fprintf ppf "\tJump %s\n" label
       | CJump (r, l1, l2) -> Printf.fprintf ppf "\tCJump r%s => %s, %s\n" r.index l1 l2
@@ -139,8 +139,8 @@ let convert_cfgrisc_risci (i: CfgRISC.RISCSimpleStatements.t list) : (RISCAssemb
                                             {index = r3.index})
     | Load   (r1, r3)            -> Load   ({index = r1.index},
                                             {index = r3.index})
-    | LoadI  (r3, imm)           -> LoadI  ({index = r3.index},
-                                            imm)
+    | LoadI  (imm, r3)           -> LoadI  (imm,
+                                            {index = r3.index})
     | Store  (r1, r3)            -> Store  ({index = r1.index},
                                             {index = r3.index})
   and helper_brop (brop: CfgRISC.RISCSimpleStatements.brop) : RISCAssembly.brop =
@@ -247,7 +247,7 @@ let rec helper
             | BImmOp (_, _, _, r)
             | URegOp (_, _, r)
             | Load (_, r)
-            | LoadI (r, _) -> (([Label label1] : RISCAssembly.risci list) @
+            | LoadI (_, r) -> (([Label label1] : RISCAssembly.risci list) @
                                 currentcode @
                                ([CJump (r, label2, label3); Label label2] : RISCAssembly.risci list) @
                                res1 @
@@ -268,7 +268,7 @@ let rec helper
             | BImmOp (_, _, _, r)
             | URegOp (_, _, r)
             | Load (_, r)
-            | LoadI (r, _) -> (currentcode @
+            | LoadI (_, r) -> (currentcode @
                                ([CJump (r, label1, label2); Label label1] : RISCAssembly.risci list) @
                                res1 @
                                ([Jump label3; Label label2] : RISCAssembly.risci list) @
diff --git a/lib/miniImp/RISC.mli b/lib/miniImp/RISC.mli
index 6beb8a9..32edc36 100644
--- a/lib/miniImp/RISC.mli
+++ b/lib/miniImp/RISC.mli
@@ -10,7 +10,7 @@ module RISCAssembly : sig
     | BImmOp of biop * register * int * register
     | URegOp of urop * register * register
     | Load of register * register
-    | LoadI of register * int
+    | LoadI of int * register
     | Store of register * register
     | Jump of label
     | CJump of register * label * label
diff --git a/lib/miniImp/RISCSemantics.ml b/lib/miniImp/RISCSemantics.ml
index d01ff6e..d371482 100644
--- a/lib/miniImp/RISCSemantics.ml
+++ b/lib/miniImp/RISCSemantics.ml
@@ -142,10 +142,10 @@ let reduce_instructions (prg: RISCArchitecture.t) (lo: string list) : int =
         in
         helper {prg with registers = RegisterMap.add {index = r3.index} n prg.registers} tl current_label
       )
-    | LoadI (r1, i) :: tl -> (
+    | LoadI (i, r3) :: tl -> (
         let n = i
         in
-        helper {prg with registers = RegisterMap.add {index = r1.index} n prg.registers} tl current_label
+        helper {prg with registers = RegisterMap.add {index = r3.index} n prg.registers} tl current_label
       )
     | Store (r1, r3) :: tl -> (
         let n = RegisterMap.find {index = r1.index} prg.registers in
diff --git a/lib/miniImp/definedVariables.ml b/lib/miniImp/definedVariables.ml
index b998e13..919771b 100644
--- a/lib/miniImp/definedVariables.ml
+++ b/lib/miniImp/definedVariables.ml
@@ -7,14 +7,250 @@ module Variable = struct
 
   let pplist (ppf: out_channel) (vv: t list) : unit =
     List.iter (Printf.fprintf ppf "%s, ") vv
+
+  let compare a b =
+    String.compare a b
 end
 
 module RISCCfg = CfgRISC.RISCCfg
 
 module DVCfg = Dataflow.Make (CfgRISC.RISCSimpleStatements) (Variable)
+module DVCeltSet = Set.Make(Variable)
+
+
+let variables_used (instr : DVCfg.elt) : DVCfg.internal list =
+  let helper (acc: DVCeltSet.t) (instr: DVCfg.elt) =
+    match instr with
+    | Nop
+    | LoadI (_, _) ->
+      acc
+    | BRegOp (_, r1, r2, _) ->
+      DVCeltSet.add r1.index acc |>
+      DVCeltSet.add r2.index
+    | BImmOp (_, r1, _, _)
+    | URegOp (_, r1, _)
+    | Load (r1, _)
+    | Store (r1, _) ->
+      DVCeltSet.add r1.index acc
+  in
+
+  helper DVCeltSet.empty instr |> DVCeltSet.to_list
+
+let variables_used_all (instructions : DVCfg.elt list) : DVCfg.internal list =
+  List.fold_left (fun (acc: DVCeltSet.t) (instr: DVCfg.elt) ->
+      DVCeltSet.union acc (variables_used instr |> DVCeltSet.of_list)
+    ) DVCeltSet.empty instructions |> DVCeltSet.to_list
+
+
+let variables_defined (instructions : DVCfg.elt) : DVCfg.internal list =
+  let helper (acc: DVCeltSet.t) (instr: DVCfg.elt) =
+    match instr with
+    | Nop -> acc
+    | BRegOp (_, _, _, r3)
+    | BImmOp (_, _, _, r3)
+    | URegOp (_, _, r3)
+    | Load (_, r3)
+    | LoadI (_, r3)
+    | Store (_, r3) ->
+      DVCeltSet.add r3.index acc
+  in
+
+  helper DVCeltSet.empty instructions |> DVCeltSet.to_list
+
+let variables_defined_all (instructions : DVCfg.elt list) : DVCfg.internal list =
+  List.fold_left (fun (acc: DVCeltSet.t) (instr: DVCfg.elt) ->
+      DVCeltSet.union acc (variables_defined instr |> DVCeltSet.of_list)
+    ) DVCeltSet.empty instructions |> DVCeltSet.to_list
+
+let _variables_defined_nth (instructions : DVCfg.elt list) (i: int) : DVCfg.internal list =
+  variables_defined (List.nth instructions i)
+
+let _variables_defined_last (instructions : DVCfg.elt list) : DVCfg.internal list =
+  variables_defined (List.nth instructions ((List.length instructions) - 1))
+
+
+
+
+(* init function, assign the epmpty set to everything *)
+let init : (DVCfg.elt list -> DVCfg.internalnode) =
+  (fun l -> {internalin = [];
+             internalout = [];
+             internalbetween = (List.init (List.length l) (fun _ -> ([], [])))})
+
+
+(* piece of code that computes vout for the whole block, not used,
+   use lub below *)
+let _dumb_lub (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internalnode =
+  let previnternalvar = Cfg.NodeMap.find node t.internalvar in
+  let code = Cfg.NodeMap.find node t.t.content in
+  { previnternalvar with
+    internalout =
+      Utility.unique_union (variables_defined_all code) (previnternalvar.internalin)
+  }
+
+
+(* We consider only the propagation in the middle elements during the lub.
+   This incurs in a performance penality, but it is simpler to implement.
+   Each node is connected to one previus node.
+*)
+let lub (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internalnode =
+  let previnternalvar = Cfg.NodeMap.find node t.internalvar in
+  let code = match Cfg.NodeMap.find_opt node t.t.content with
+      None -> []
+    | Some c -> c
+  in
+  { previnternalvar with
+    internalbetween =
+      List.mapi (* we don't NEED the index but i = 0 is easier to write than
+                   to check if vinout is None *)
+        (fun i (ithcode, vinout, ithcodeprev) ->
+           if i = 0 then
+             let dvin = previnternalvar.internalin in
+             (dvin, Utility.unique_union dvin (variables_defined ithcode))
+           else (
+             let ithcodeprev = match ithcodeprev with
+                 None -> ([], [])
+               | Some x -> x
+             in
+             match vinout with
+               None ->
+               ([], variables_defined ithcode)
+             | Some prevdvbtw ->
+               (snd prevdvbtw,
+                Utility.unique_union
+                  (variables_defined ithcode)
+                  (ithcodeprev |> fst)
+               ))
+        )
+        (* ugly code that zips the three lists that we need to compute each vin
+           and vout for the middle of the code *)
+        (Utility.combine_thrice
+           code
+           (Utility.pad_opt
+              (Utility.prev previnternalvar.internalbetween None) None (List.length code))
+           (Utility.pad previnternalvar.internalbetween None (List.length code))
+        );
+    internalout =
+      match previnternalvar.internalbetween with
+        [] -> previnternalvar.internalin
+      | _ -> (snd (Utility.last_list previnternalvar.internalbetween))
+  }
+
+let lucf (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internalnode =
+  let previnternalvar = Cfg.NodeMap.find node t.internalvar in
+  if Option.equal (=) (Some node) t.t.initial then
+    { previnternalvar with
+      internalin =
+        match t.t.inputOutputVar with
+          Some (i, _) -> [i]
+        | None -> []
+    }
+  else
+    let prevnodes = Cfg.NodeMap.find node t.t.reverseEdges in
+    { previnternalvar with
+      internalin =
+        match prevnodes with
+          [] -> []
+        | [prevnode] -> (Cfg.NodeMap.find prevnode t.internalvar).internalout
+        | [prevnode1; prevnode2] ->
+          Utility.unique_intersection
+            (Cfg.NodeMap.find prevnode1 t.internalvar).internalout
+            (Cfg.NodeMap.find prevnode2 t.internalvar).internalout
+        | _ ->
+          List.fold_left (* intersection of all previous nodes' dvout *)
+            (fun acc prevnode ->
+               Utility.unique_intersection acc (Cfg.NodeMap.find prevnode t.internalvar).internalout)
+            []
+            prevnodes
+    }
+
+
+let update (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internalnode =
+  let newt = {t with internalvar = (Cfg.NodeMap.add node (lucf t node) t.internalvar)} in
+  lub newt node
+
 
 let compute_defined_variables (cfg: RISCCfg.t) : DVCfg.t =
   DVCfg.from_cfg cfg
+  |> DVCfg.fixed_point ~init:init ~update:update
 
-let compute_cfg (dvcfg : DVCfg.t) : RISCCfg.t =
+
+
+let check_defined_variables (dvcfg: DVCfg.t) : bool =
+  let helper node (dvcfg: DVCfg.t) =
+    let code = match Cfg.NodeMap.find_opt node dvcfg.t.content with
+        None -> []
+      | Some c -> c
+    in
+    let internalvar = Cfg.NodeMap.find node dvcfg.internalvar in
+    let vua = variables_used_all code in
+
+    let outvar = (* is true if we are in the last node and the out variable is
+                    not in vout, so its true if the out variable is not
+                    defined *)
+      match (Option.equal (=) (Some node) dvcfg.t.terminal,
+             dvcfg.t.inputOutputVar,
+             internalvar.internalout) with
+      | (true, Some (_, outvar), vout) ->
+        not (List.mem outvar vout)
+      | (_, _, _) ->
+        false
+    in
+
+    if Utility.inclusion vua (internalvar.internalin) then
+      not outvar
+    else
+      (* the variable might be defined inside the block, so check all vin and
+         return true only if all variables are properly defined *)
+      let vuabetween = List.map variables_used code in
+      let check = List.fold_left
+          (fun acc (codevars, (vin, _vout)) ->
+             acc && (Utility.inclusion codevars vin))
+          true
+          (List.combine vuabetween internalvar.internalbetween)
+      in
+      check && (not outvar)
+  in
+  Cfg.NodeSet.fold (fun node acc -> acc && (helper node dvcfg)) dvcfg.t.nodes true
+
+
+let undefined_variables (dvcfg: DVCfg.t) : Variable.t list =
+  let helper (node: Cfg.Node.t) (dvcfg: DVCfg.t) =
+    let code = match Cfg.NodeMap.find_opt node dvcfg.t.content with
+        None -> []
+      | Some c -> c
+    in
+    let internalvar = Cfg.NodeMap.find node dvcfg.internalvar in
+    let vua = variables_used_all code in
+
+    let outvar =
+      match (Option.equal (=) (Some node) dvcfg.t.terminal,
+             dvcfg.t.inputOutputVar,
+             internalvar.internalout) with
+      | (true, Some (_, outvar), vout) ->
+        if List.mem outvar vout
+        then None
+        else Some outvar
+      | (_, _, _) ->
+        None
+    in
+
+    if Utility.inclusion vua (internalvar.internalin) then
+      match outvar with None -> [] | Some outvar -> [outvar]
+    else
+      (* the variable might be defined inside the block, so check all vin and
+         return true only if all variables are properly defined *)
+      let vuabetween = List.map variables_used code in
+      let undef_vars = List.fold_left
+          (fun acc (codevars, (vin, _vout)) ->
+             (Utility.subtraction codevars vin) @ acc)
+          []
+          (List.combine vuabetween internalvar.internalbetween)
+      in
+      match outvar with None -> undef_vars | Some outvar -> outvar :: undef_vars
+  in
+  Cfg.NodeSet.fold (fun node acc -> acc @ (helper node dvcfg)) dvcfg.t.nodes []
+
+
+let compute_cfg (dvcfg: DVCfg.t) : RISCCfg.t =
   DVCfg.to_cfg dvcfg
diff --git a/lib/miniImp/definedVariables.mli b/lib/miniImp/definedVariables.mli
index 67d4ee4..bbb1e7c 100644
--- a/lib/miniImp/definedVariables.mli
+++ b/lib/miniImp/definedVariables.mli
@@ -13,3 +13,7 @@ module DVCfg : Dataflow.C with type elt = CfgRISC.RISCSimpleStatements.t
 val compute_defined_variables : RISCCfg.t -> DVCfg.t
 
 val compute_cfg : DVCfg.t -> RISCCfg.t
+
+val check_defined_variables : DVCfg.t -> bool
+
+val undefined_variables : DVCfg.t -> Variable.t list
diff --git a/lib/utility/utility.ml b/lib/utility/utility.ml
index 4553be5..758ba17 100644
--- a/lib/utility/utility.ml
+++ b/lib/utility/utility.ml
@@ -40,6 +40,7 @@ let int_more_eq a b =
 let int_not a =
   if a > 0 then 0 else 1
 
+(* converts an integer to a list of chars such that it is pretty and linear *)
 let rec fromIntToString (alphabet: string) (x: int) : string =
   let base = String.length alphabet in
   if x < 0 then
@@ -47,4 +48,108 @@ let rec fromIntToString (alphabet: string) (x: int) : string =
   else if x < base then
     String.get alphabet x |> String.make 1
   else
-    (fromIntToString (alphabet) (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1)
+    (fromIntToString (alphabet) (x/base - 1)) ^ (String.get alphabet (x mod base)
+                                                 |> String.make 1)
+
+
+let inclusion la lb =
+  let rec aux la =
+    function
+      [] -> true
+    | b::lb ->
+      if List.mem b la
+      then aux la lb
+      else false
+  in
+  aux lb la
+
+let subtraction la lb =
+  let rec aux la =
+    function
+      [] -> la
+    | b::lb ->
+      aux (List.filter ((<>) b) la) lb
+  in
+  aux la lb
+
+(* returns only the unique elements of l *)
+let unique l =
+  let rec aux l acc =
+    match l with
+    | [] ->
+        List.rev acc
+    | h :: t ->
+      if List.mem h acc
+      then aux t acc
+      else aux t (h :: acc)
+  in
+  aux l []
+
+(* returns the unique elements of the concat of the lists *)
+let unique_union la lb =
+  unique (la @ lb)
+
+let unique_intersection la lb =
+  let rec aux la lb acc =
+    match la with
+      [] -> acc
+    | a::la ->
+      if List.mem a lb
+      then aux la lb (a::acc)
+      else aux la lb acc
+  in
+  aux la lb [] |> unique
+
+
+(* Complicated way to drop the last element and add a new option element to the
+   beginning *)
+let prev l a =
+  match l with
+  | [] ->
+    [a]
+  | _ ->
+    a :: (List.map (fun x -> Some x) (l |> List.rev |> List.tl |> List.rev))
+
+let pad l a n =
+  let l = List.map (fun i -> Some i) l in
+  if List.length l < n
+  then
+    l @ (List.init (n - List.length l) (fun _ -> a))
+  else
+    l
+
+let pad_opt l a n =
+  if List.length l < n
+  then
+    l @ (List.init (n - List.length l) (fun _ -> a))
+  else
+    l
+
+let combine la lb =
+  List.map2 (fun a b ->
+      match b with
+        None -> None
+      | Some b -> Some (a, b)
+    ) la lb
+
+let rec last_list l =
+  match l with
+    [] -> failwith "Utility.last_list, not enough items"
+  | [a] -> a
+  | _::ll -> last_list ll
+
+let add_to_last_list (la: 'a list list) (a: 'a) : 'a list list =
+  let rec aux la a =
+    match la with
+      [] -> [[a]]
+    | [l] -> [a :: l]
+    | l::la -> l :: (aux la a)
+  in
+  aux la a
+
+let rec combine_thrice la lb lc =
+  match (la, lb, lc) with
+  | [], [], [] -> []
+  | [a], [b], [c] -> [a, b, c]
+  | a::la, b::lb, c::lc -> (a, b, c) :: (combine_thrice la lb lc)
+  | _ -> []
diff --git a/lib/utility/utility.mli b/lib/utility/utility.mli
index 4a7ad3e..fe02ef8 100644
--- a/lib/utility/utility.mli
+++ b/lib/utility/utility.mli
@@ -1,14 +1,31 @@
-val pow : int -> int -> int
-
+val pow :    int -> int -> int
 val powmod : int -> int -> int -> int
 
-val int_and : int -> int -> int
-val int_or : int -> int -> int
-val int_eq : int -> int -> int
-val int_less : int -> int -> int
+val int_and :     int -> int -> int
+val int_or :      int -> int -> int
+val int_eq :      int -> int -> int
+val int_less :    int -> int -> int
 val int_less_eq : int -> int -> int
-val int_more : int -> int -> int
+val int_more :    int -> int -> int
 val int_more_eq : int -> int -> int
-val int_not : int -> int
+val int_not :     int -> int
 
 val fromIntToString : string -> int -> string
+
+val inclusion :           'a list -> 'a list -> bool
+val subtraction :         'a list -> 'a list -> 'a list
+
+val unique :              'a list -> 'a list
+val unique_union :        'a list -> 'a list -> 'a list
+val unique_intersection : 'a list -> 'a list -> 'a list
+
+val prev :      'a        list -> 'a option        -> 'a option list
+
+val pad :       'a        list -> 'a option -> int -> 'a option list
+val pad_opt :   'a option list -> 'a option -> int -> 'a option list
+
+val combine :   'a        list -> 'b option list   -> ('a * 'b) option list
+val last_list : 'a        list -> 'a
+val add_to_last_list : 'a list list -> 'a -> 'a list list
+
+val combine_thrice : 'a list -> 'b list -> 'c list  -> ('a * 'b * 'c) list