From 2bd31db883c1a2b892551c4934019b2b0ac76c87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gwena=EBl=20Delaval?= <gwenael.delaval@inria.fr>
Date: Thu, 7 Jun 2012 15:27:07 +0200
Subject: [PATCH] Causality and scheduling with contracts

Correction of the causality analysis and scheduling (with interference)
to take contracts into account.
---
 compiler/heptagon/analysis/causality.ml          | 10 ++++++----
 compiler/minils/analysis/interference.ml         |  6 ++++++
 .../minils/transformations/schedule_interf.ml    | 16 ++++++++++++----
 3 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml
index 4bb057e..b10f85e 100644
--- a/compiler/heptagon/analysis/causality.ml
+++ b/compiler/heptagon/analysis/causality.ml
@@ -225,10 +225,12 @@ let typing_contract loc contract =
         let teq = typing_eqs b.b_equs in
         let t_contract =
           cseq
-            (typing e_a)
-            (cseq (typing e_g)
-               (cseq (typing e_a_loc)
-                  (cseq (typing e_g_loc) teq))) in
+            teq
+            (ctuplelist
+               [(typing e_a);
+                (typing e_g);
+                (typing e_a_loc);
+                (typing e_g_loc)]) in
         Causal.check loc t_contract;
         let t_contract = clear (build b.b_local) t_contract in
         t_contract
diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml
index 3b84db5..b6bebe1 100644
--- a/compiler/minils/analysis/interference.ml
+++ b/compiler/minils/analysis/interference.ml
@@ -158,6 +158,12 @@ module World = struct
     let env = build Env.empty f.n_input in
     let env = build env f.n_output in
     let env = build env f.n_local in
+    let env =
+      match f.n_contract with
+        None -> env
+      | Some c -> 
+          let env = build env c.c_local in
+          build env c.c_controllables in
       igs := [];
       vds := env;
     (* build the set of memories *)
diff --git a/compiler/minils/transformations/schedule_interf.ml b/compiler/minils/transformations/schedule_interf.ml
index 70b8945..52ae38b 100644
--- a/compiler/minils/transformations/schedule_interf.ml
+++ b/compiler/minils/transformations/schedule_interf.ml
@@ -137,14 +137,22 @@ let schedule eq_list inputs node_list =
   let rem_eqs = free_eqs node_list in
     List.rev (schedule_aux rem_eqs [] node_list Clocks.Cbase costs)
 
-let schedule_contract c =
-  c
+let schedule_contract contract c_inputs =
+  match contract with
+    None -> None, []
+  | Some c -> 
+      let node_list, _ = DataFlowDep.build c.c_eq in
+      (Some { c with c_eq = schedule c.c_eq c_inputs node_list; }),
+      c.c_controllables
 
 let node _ () f =
   Interference.World.init f;
-  let contract = optional schedule_contract f.n_contract in
+  let contract,controllables = schedule_contract f.n_contract (f.n_input@f.n_output) in
   let node_list, _ = DataFlowDep.build f.n_equs in
-  let f = { f with n_equs = schedule f.n_equs f.n_input node_list; n_contract = contract } in
+  (* Controllable variables are considered as inputs *)
+  let f = { f with 
+              n_equs = schedule f.n_equs (f.n_input@controllables) node_list;
+              n_contract = contract } in
     f, ()
 
 let program p =