Causality and scheduling with contracts

Correction of the causality analysis and scheduling (with interference)
to take contracts into account.

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

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 *)

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 =