ifp implemented/while analysis

lib/mdg/analyse.ml

@@ -100,8 +100,9 @@ and analyse (state : state) (statement : m Statement.t) : unit =
       Store.lub state.store state'.store;
 
     (* -------- W H I L E -------- *)
-    | _, While _ -> ()
-
+    | _, While {body; _} -> 
+      ifp (flip analyse_sequence body) state
+
     | _ -> ());
           (* failwith "statement node analysis not defined" *)
 
@@ -119,6 +120,14 @@ and analyse (state : state) (statement : m Statement.t) : unit =
 
 and analyse_sequence (state : state) = List.iter (analyse state)
 
+and ifp (f : state -> unit) (state : state) : unit =
+  let state' = State.copy state in 
+  f state;
+  if not (State.is_equal state state') 
+    then ifp f state 
+    else ()
+
+
 and eval_expr (store : Store.t) (this : LocationSet.t) (expr : m Expression.t) : LocationSet.t = 
   match expr with
     | (_, Identifier _) as id -> 

lib/mdg/graph.ml

@@ -36,6 +36,20 @@ and print_edge (from : location) (edges : EdgeSet.t) : unit =
 
 let copy (graph : t) : t = HashTable.copy graph
 
+let is_equal (graph : t) (graph' : t) : bool = 
+  let result = ref true in
+  if HashTable.length graph = HashTable.length graph'
+    then (
+        HashTable.iter ( fun key value -> 
+        if !result then
+          let value' = HashTable.find_opt graph' key in 
+          if Option.is_some value'
+            then result := EdgeSet.equal value (Option.get value')
+            else result := false
+        ) graph;
+        !result
+      )
+    else false
 
 (* ------- M A I N   F U N C T I O N S -------*)
 let lub (graph : t) (graph' : t) : unit = 
@@ -47,7 +61,7 @@ let lub (graph : t) (graph' : t) : unit =
 
 let alloc (_ : t) (id : int) : location = loc_prefix ^ (Int.to_string id)
 
-(* TODO : test*)
+(* TODO : test *)
 let rec orig (graph : t) (l : location) : location = 
   HashTable.fold (fun l' edges acc ->
     if (EdgeSet.exists (has_version_edge l) edges) 
@@ -56,7 +70,6 @@ let rec orig (graph : t) (l : location) : location =
   ) graph l 
 
 
-(* TODO *)
 let lookup (graph : t) (l : location) (property : property) : location =
   let direct_edges = HashTable.find graph l in   
 

lib/mdg/state.ml

@@ -18,5 +18,11 @@ let copy ({graph; store; _} as state : state) : state =
      store = Store.copy store;
   }
 
+let is_equal (state : state) (state' : state) : bool = 
+  Graph.is_equal state.graph state'.graph &&
+  Store.is_equal state.store state'.store &&
+  LocationSet.equal state.this state'.this
+
+
 
 

lib/mdg/store.ml

@@ -23,6 +23,20 @@ let lub (store : t) (store' : t) : unit =
 
 let copy (store : t) : t = HashTable.copy store
 
+let is_equal (store : t) (store' : t) : bool = 
+  let result = ref true in
+  if HashTable.length store = HashTable.length store'
+    then (
+        HashTable.iter ( fun key value -> 
+        if !result then
+          let value' = HashTable.find_opt store' key in 
+          if Option.is_some value'
+            then result := LocationSet.equal value (Option.get value')
+            else result := false
+        ) store;
+        !result
+      )
+    else false
 
 let rec print (store : t) : unit =
   HashTable.iter (fun id locs ->