From 1a78c940f46273b7146d2111b1e2da309434f021 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 27 May 2021 16:55:18 +0200
Subject: [disabled checker] BTL Scheduling and Renumbering OK!

---
 scheduling/BTLcommonaux.ml | 84 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 scheduling/BTLcommonaux.ml

(limited to 'scheduling/BTLcommonaux.ml')

diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml
new file mode 100644
index 00000000..dabf760a
--- /dev/null
+++ b/scheduling/BTLcommonaux.ml
@@ -0,0 +1,84 @@
+open Maps
+open BTL
+open BTLtypes
+open RTLcommonaux
+
+let undef_node = -1
+
+let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond; visited = false }
+
+let def_iinfo () = { inumb = undef_node; pcond = None; visited = false }
+
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
+
+let reset_visited_ibf btl =
+  PTree.map
+    (fun n ibf ->
+      ibf.binfo.visited <- false;
+      ibf)
+    btl
+
+let reset_visited_ib btl =
+  List.iter
+    (fun (n, ibf) ->
+      let ib = ibf.entry in
+      let rec reset_visited_ib_rec ib =
+        match ib with
+        | Bseq (ib1, ib2) ->
+            reset_visited_ib_rec ib1;
+            reset_visited_ib_rec ib2
+        | Bcond (_, _, ib1, ib2, iinfo) ->
+            reset_visited_ib_rec ib1;
+            reset_visited_ib_rec ib2;
+            iinfo.visited <- false
+        | Bnop (Some iinfo)
+        | Bop (_, _, _, iinfo)
+        | Bload (_, _, _, _, _, iinfo)
+        | Bstore (_, _, _, _, iinfo)
+        | BF (_, iinfo) ->
+            iinfo.visited <- false
+        | _ -> ()
+      in
+      reset_visited_ib_rec ib)
+    (PTree.elements btl);
+  btl
+
+let jump_visit = function
+  | Bcond (_, _, _, _, iinfo)
+  | Bnop (Some iinfo)
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | BF (_, iinfo) ->
+      if iinfo.visited then true
+      else (
+        iinfo.visited <- true;
+        false)
+  | Bseq (_, _) -> false
+  | Bnop None -> true
+
+let rec get_inumb_or_next = function
+  | BF (Bgoto s, _) -> p2i s
+  | BF (_, iinfo)
+  | Bnop (Some iinfo)
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | Bcond (_, _, _, _, iinfo) ->
+      iinfo.inumb
+  | Bseq (ib1, _) -> get_inumb_or_next ib1
+  | _ -> failwith "get_inumb_or_next: Bnop None"
+
+let rec set_next_inumb btl pos = function
+  | BF (Bgoto s, _) ->
+      let ib' = (get_some @@ PTree.get s btl).entry in
+      set_next_inumb btl pos ib'
+  | BF (_, iinfo)
+  | Bnop (Some iinfo)
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | Bcond (_, _, _, _, iinfo) ->
+      iinfo.inumb <- pos
+  | Bseq (ib1, _) -> set_next_inumb btl pos ib1
+  | _ -> failwith "get_inumb_or_next: Bnop None"
-- 
cgit