Delete TODO to use git Issues instead

TODO

@@ -1,5 +0,0 @@
-# Parseur
-
- - ajustement des automates
-
-# ...

src/ast.ml

@@ -77,3 +77,4 @@ type t_ck = base_ck list
 and base_ck = 
     | Base
     | On of base_ck * t_expression
+    | Unknown

src/cprint.ml

@@ -95,7 +95,7 @@ let cp_state_frees fmt (iprog, sts) =
         then
           Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\
             \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\
-            \t\tfree (st->aux_state[%d]);\n\t}\n%a"
+            \t\tfree (st->aux_states[%d]);\n\t}\n%a"
             idx callee_name callee_name idx
             idx cp_free_aux (i+1, caller_name)
         else Format.fprintf fmt "\tif (st->aux_states[%d])\n\

src/lustre_pp.ml

@@ -160,6 +160,7 @@ and pp_nexts fmt: t_expression list * string list -> unit = function
       pp_expression e
       n
       pp_nexts (exprs, nexts)
+  | _, _ -> () (*This should never happen*)
 
 and pp_translist fmt: t_state list -> unit = function
   | [] -> ()

src/main.ml

@@ -25,8 +25,6 @@ let exec_passes ast verbose debug passes f =
     | [] ->  f ast
     | (n, p) :: passes ->
         verbose (Format.asprintf "Executing pass %s:\n" n);
-        try
-        begin
           match p verbose debug ast with
           | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
           | Some ast -> (
@@ -34,8 +32,6 @@ let exec_passes ast verbose debug passes f =
               (Format.asprintf
                 "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
             aux ast passes)
-        end with
-        | _ -> failwith ("The pass "^n^" should have caught me!")
   in
   aux ast passes
 
@@ -44,10 +40,12 @@ let exec_passes ast verbose debug passes f =
 let _ =
   (** Usage and argument parsing. *)
   let default_passes =
-      ["linearization_reset"; "automata_translation"; "remove_if";
+    ["linearization_reset"; "automata_translation"; "remove_if";
+      "linearization_merge"; "linearization_when";
       "linearization_pre"; "linearization_tuples"; "linearization_app";
       "ensure_assign_val";
-      "equations_ordering"] in
+      "equations_ordering";
+      "clock_unification"] in
   let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
   let usage_msg =
     "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@@ -85,6 +83,8 @@ let _ =
   List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
     [
       ("remove_if", Passes.pass_if_removal);
+      ("linearization_merge", Passes.pass_merge_lin);
+      ("linearization_when", Passes.pass_when_lin);
       ("linearization_tuples", Passes.pass_linearization_tuples);
       ("linearization_app", Passes.pass_linearization_app);
       ("linearization_pre", Passes.pass_linearization_pre);

src/passes.ml

@@ -6,6 +6,183 @@ open Utils
 
 
 
+(** [pass_when_lin] linearizes the when construct so that it only appears as
+  * main construction of right members of equations. *)
+let pass_when_lin verbose debug =
+  (* prefix of the fresh variables to use and counter to make them unique. *)
+  let varname_prefix = "_whenlin" in
+  let count = ref 0 in
+  (** Auxiliary function that linearizes an expression. *)
+  let rec aux_expr vars expr toplevel conds =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+      let eqs, vars, l = List.fold_right
+        (fun e (eqs, vars, l) ->
+          let eqs', vars, e = aux_expr vars e false conds in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (t, op, e, e', e'') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      let eqs'', vars, e'' = aux_expr vars e'' false conds in
+      eqs''@eqs'@eqs, vars, ETriOp (t, op, e, e', e'')
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false (e :: conds) in
+      let e =
+        List.fold_left
+          (fun e e' -> EBinOp ([TBool], BOp_and, e,e'))
+          e conds
+      in
+      if toplevel
+        then
+          eqs'@eqs, vars, EWhen (t, e, e')
+        else
+          begin
+            if List.length t = 1
+              then
+                begin
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                ((t, [newvar]), EWhen (t, e, e')) :: eqs'@eqs, vars, EVar (t, newvar)
+                end
+              else
+                  raise (PassExn "When should only happen on unary expressions.")
+          end
+  in
+  (** For each node: *)
+  let aux_when_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true [] in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_when_lin
+
+
+
+(** [pass_merge_lin] linearizes the merges so that they only appear as main
+  * construct of right sides of equations.
+  * This simplifies their handling in next passes and in the C printer. *)
+let pass_merge_lin verbose debug =
+  (* prefix of the fresh variables to use and counter to make them unique. *)
+  let varname_prefix = "_mergelin" in
+  let count = ref 0 in
+  (** Auxiliary function that linearizes an expression. *)
+  let rec aux_expr vars expr toplevel =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+      let eqs, vars, l = List.fold_right
+        (fun e (eqs, vars, l) ->
+          let eqs', vars, e = aux_expr vars e false in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (_, TOp_if, _, _, _) ->
+        raise (PassExn "There should no longer be any condition.")
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs @ eqs', vars, EWhen (t, e, e')
+    | ETriOp (t, TOp_merge, c, e, e') ->
+      begin
+        if toplevel
+          then
+            begin
+            let eqs, vars, c = aux_expr vars c false in
+            let eqs', vars, e = aux_expr vars e false in
+            let eqs'', vars, e' = aux_expr vars e' false in
+            eqs@eqs'@eqs'', vars, ETriOp (t, TOp_merge, c, e, e')
+            end
+          else
+            begin
+            if List.length t = 1
+              then
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                let eqs, vars, c = aux_expr vars c false in
+                let eqs', vars, e = aux_expr vars e false in
+                let eqs'', vars, e' = aux_expr vars e' false in
+                ((t, [newvar]), ETriOp (t, TOp_merge, c, e, e')) :: eqs @ eqs' @ eqs'', vars, EVar (t, newvar)
+              else
+                raise (PassExn "Merges should only happen on unary expressions.")
+            end
+      end
+  in
+  (** For each node: *)
+  let aux_merge_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_merge_lin
+
+
+
 (** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
   *
   *     [x1, ..., xn = if c then e_l else e_r;]
@@ -244,7 +421,7 @@ let pass_linearization_pre verbose debug =
                           | [TInt]  -> IVar nvar
                           | [TBool] -> BVar nvar
                           | [TReal] -> RVar nvar
-                          | _ -> failwith "Should not happened." in
+                          | _ -> failwith "Should not happened. (pass_linearization_pre)" in
               let neq_patt: t_varlist = (t, [nvar]) in
               let neq_expr: t_expression = e in
               let vars = varlist_concat (t, [nvar]) vars in
@@ -749,7 +926,7 @@ let pass_typing verbose debug ast =
           else None
   in aux ast
 
-let check_automata_validity verbos debug = 
+let check_automata_validity verbose debug = 
   let check_automaton_branch_vars automaton = 
     let (init, states) = automaton in
     let left_side = Hashtbl.create 10 in
@@ -774,8 +951,11 @@ let check_automata_validity verbos debug =
     end
   in
   let aux node = 
+    try
     List.iter check_automaton_branch_vars node.n_automata;
     Some node
+    with
+    | PassExn err -> (verbose err; None)
   in
   node_pass aux
 
@@ -922,112 +1102,150 @@ let automata_translation_pass verbose debug =
                 eqs@eqs_end, (ty@ty_end, vars@vars_end)
     in
     let aux node = 
-        let eqs, (ty, vars) = iter_automata node.n_automata in
+        try
-        let (ty_old, vars_old) = node.n_local_vars in
+            let eqs, (ty, vars) = iter_automata node.n_automata in
-        Some { node with n_local_vars = (ty@ty_old, vars@vars_old); n_equations = node.n_equations@eqs; n_automata = []}
+            let (ty_old, vars_old) = node.n_local_vars in
+            Some { node with n_local_vars = (ty@ty_old, vars@vars_old); n_equations = node.n_equations@eqs; n_automata = []}
+        with
+        |PassExn err -> (verbose err; None)
     in
   node_pass aux
 
 let clock_unification_pass verbose debug ast = 
 
-  let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
-    
   let known_clocks = Hashtbl.create 100 in
+  let used = Hashtbl.create 100 in (*keep track of variables that appear on right side of equation*)
+  let changed = ref false in
 
-  let find_clock_var var = 
+  let rec count_not e acc = match e with
-      match Hashtbl.find_opt known_clocks var with
+    | EVar([TBool], var) -> acc, e
-      | None -> 
+    | EConst([TBool], cons) -> acc, e
-        begin
+    | EMonOp([TBool], MOp_not, e) -> count_not e (acc + 1)
-          match var with
+    | _ -> acc, e
-          | BVar(name)
-          | IVar(name)
-          | RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
-        end
-      | Some c -> c
   in
 
-  let rec compute_clock_exp exp = match exp with
+  let verify_when e1 e2 =
-  | EConst(_, _) -> [Base]
+      let n1, var1 = count_not e1 0
-  | EVar(_, var) -> find_clock_var var
+      and n2, var2 = count_not e2 0 in
-  | EMonOp(_, MOp_pre, _) -> [Base]
+      if n1 mod 2 <> n2 mod 2 || var1 <> var2 then
-  | EMonOp(_, _, e) -> compute_clock_exp e
+          raise (PassExn "verify_when failure")
+  in
+
+  let get_var_name var = match var with
+  | RVar(name)
+  | BVar(name)
+  | IVar(name) -> name
+  in
+
+  let rec clk_to_string clk = match clk with
+  | Base -> "Base"
+  | Unknown -> "Unknown"
+  | On(clk, exp) -> 
+          let n, var = count_not exp 0 in
+          let s = if n mod 2 = 1 then "not " else "" in
+          let v = match var with |EVar(_, var) -> get_var_name var | EConst(_, CBool(false)) -> "false" |_ -> "true" in
+          (clk_to_string clk) ^ " on " ^ s ^ v
+  in
+
+  let add_clock var clock = 
+      match Hashtbl.find known_clocks var with
+      | Unknown -> changed := true; (debug ("Found clock for "^(get_var_name var)^": "^(clk_to_string clock))); Hashtbl.replace known_clocks var clock
+      | c when c = clock -> ()
+      | c -> raise (PassExn ("Clock conflict "^(get_var_name var) ^" "^(clk_to_string c) ^ " " ^ (clk_to_string clock)))
+  in
+
+  let rec update_clock exp clk = match exp with
+  | EConst(_, _) -> ()
+  | EVar(_, var) -> add_clock var clk; Hashtbl.replace used var var
+  | EMonOp(_, _, e) -> update_clock e clk
 
   | EComp(_, _, e1, e2)
   | EReset(_, e1, e2)
-  | EBinOp(_, _, e1, e2) -> 
+  | EBinOp(_, _, e1, e2) -> update_clock e1 clk; update_clock e2 clk
-    begin
-      let c1 = compute_clock_exp e1
-      and c2 = compute_clock_exp e2 in
-      if c1 <> c2 then
-        failure "Binop"
-      else
-        c1
-    end
-  | EWhen(_, e1, e2) -> 
-      begin
-        match compute_clock_exp e1 with
-        | [c1] -> [On (c1, e2)]
-        | _ -> failure "When"
-      end
   | ETriOp(_, TOp_merge, e1, e2, e3) ->
-    begin
+          update_clock e1 clk;
-      let c1 = compute_clock_exp e1
+          update_clock e2 (On(clk, e1));
-      and c2 = compute_clock_exp e2
+          update_clock e3 (On(clk, EMonOp([TBool], MOp_not, e1)))
-      and c3 = compute_clock_exp e3 in
-      match c1, c2, c3 with
-      | [c1], [On(cl2, e2)], [On(cl3, e3)] ->
-          begin
-            if cl2 <> c1 || cl3 <> c1 then
-              failure "Triop clocks"
-            else match e2, e3 with
-            | EMonOp(_, MOp_not, e), _ when e = e3 -> [c1]
-            | _, EMonOp(_, MOp_not, e) when e = e2 -> [c1]
-            | _ -> failure "Triop condition"
-          end
-      | _ -> failure ("Merge format")
-    end
   | ETriOp(_, TOp_if, e1, e2, e3) ->
-      let (* Unused: c1 = compute_clock_exp e1
+          (* The 3 expressions should have the same clock *)
-      and*) c2 = compute_clock_exp e2
+          begin
-      and c3 = compute_clock_exp e3 in
+          update_clock e1 clk;
-      if c2 <> c3 then
+          update_clock e2 clk;
-        failure "If clocks"
+          update_clock e3 clk
-      else c2
+          end
-
+  | ETuple(_, explist) -> List.iter (fun e -> update_clock e clk) explist
-  | ETuple(_, explist) -> List.concat_map compute_clock_exp explist
+  | EApp(_, node, e) -> update_clock e clk
-  | EApp(_, node, e) -> 
+  | EWhen(_, e1, e2) -> 
-      let rec aux_app clk_list = match clk_list with
+      match clk with
-      | [] -> raise (PassExn "Node called with no argument provided")
+      | On(clk2, e) -> verify_when e e2; update_clock e1 clk2
-      | [cl] -> cl
+      | _ -> raise (PassExn "Clock unification failure: when")
-      | t::q -> if t = (aux_app q) then t else failure "App diff clocks"
-      and mult_clk cl out_list = match out_list with
-      | [] -> []
-      | t::q -> cl::(mult_clk cl q)
-      in
-      mult_clk (aux_app (compute_clock_exp e)) (snd node.n_outputs)
       in
 
-  let rec compute_eq_clock eq = 
+  let rec propagate_clock eqs =
-    let rec step vars clks = match vars, clks with
+    let rec step ((ty, vars), exp)= match vars with
-    | [], [] -> ()
+    | [] -> ()
-    | [], c::q -> raise (PassExn "Mismatch between clock size")
+    | v::t -> let clk = Hashtbl.find known_clocks v in
-    | v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
+      begin
-    | l, [] -> raise (PassExn "Mismatch between clock size")
+      if clk <> Unknown then update_clock exp clk
+      else ();
+      step ((ty, t), exp)
+      end
     in
-    let (_, vars), exp = eq in
+    List.iter step eqs
-    let clk = compute_clock_exp exp in
-    step vars clk
   in
+  
+  let rec iter_til_stable eqs = 
+    changed := false;
+    propagate_clock eqs;
+    if !changed then
+        iter_til_stable eqs
+  in
+
+  let check_unification node =
+    let (_, node_inputs) = node.n_inputs in
+    let rec check_vars_aux acc = match acc with
+    | [(v, c)] -> if c = Unknown && (Hashtbl.mem used v) then raise (PassExn ("Clock unification failure: Unkwown clock for "^(get_var_name v))) else c
+    | (v, t)::q -> let c = check_vars_aux q in
+        if c <> t then raise (PassExn "Clock unification failure: Non homogeneous equation") else c
+    | [] -> raise (PassExn "Clock unification failure: empty equation")
+    in
+    let rec check_vars ((ty, vars), exp) acc = match vars with
+    | [] -> let _ = check_vars_aux acc in ()
+    | v::t -> check_vars ((ty, t), exp) ((v, Hashtbl.find known_clocks v)::acc)
+    in
+    let rec check_inputs inputs = match inputs with
+    | [] -> ()
+    | i::q -> let c = Hashtbl.find known_clocks i in
+        match c with
+        | On(_, e) -> let _, var = count_not e 0 in 
+            begin
+            match var with
+            | EConst(_, _) -> ()
+            | EVar(_, var) -> if not (List.mem var node_inputs) then raise (PassExn "Clock unification failure: input clock depends on non input clock")
+                else check_inputs q
+            | _ -> failwith "Should not happen. (clock_unification)"
+            end
+        | _ -> check_inputs q
+    in
+    (*Check that all variables used have a clock
+       and that inputs clocks do not depend on local vars or outputs*)
+    List.iter (fun eq -> check_vars eq []) node.n_equations;
+    check_inputs node_inputs;
+  in
+
 
   let compute_clock_node n = 
     begin
       Hashtbl.clear known_clocks;
-      List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
+      List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
-        snd n.n_inputs); (* Initializing inputs to base clock *)
+        snd n.n_inputs); (* Initializing inputs to Unknown clock *)
-      List.iter compute_eq_clock n.n_equations;
+      List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
-      if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
+        snd n.n_local_vars); (* Initializing local variables to Unknown clock *)
-        snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
+      List.iter (fun v -> Hashtbl.replace known_clocks v Base) (
-      else
+        snd n.n_outputs); (* Initializing outputs to base clock *)
-        Some n
+          iter_til_stable n.n_equations;
+          (* catch potential errors and test for unification *)
+          check_unification n;
+          Some n
     end
   in node_pass compute_clock_node ast

src/test.node

@@ -16,3 +16,10 @@ let
   tmp = aux (a+b, i);
 tel
 
+node test (u, v: int; c: bool) returns (o: int);
+var x, y: int; b: bool;
+let
+	x = merge c u v;
+	o = 2 * x;
+tel
+

tests/automaton.node

@@ -11,7 +11,7 @@ let
     o = (not (not (l1 = l2))) and (l1 = l2) and true;
 tel
 
-node auto (i: int) returns (o : int);
+node main (i: int) returns (o : int);
 var x, y:int;
 let
     automaton

tests/when_merge.node

@@ -1,14 +1,13 @@
-node test (i: int) returns (o: int);
+node test (i: real) returns (o: real);
-var x, y: int;
+var x, y: real;
 let
-    x = (1 / i) when (i <> 0);
+    x = (1.0 / i) when (i <> 0.0);
-    y = 0 when (not (i <> 0));
+    y = 0.0 when (not (i <> 0.0));
-    o = merge (i <> 0) x y;
+    o = merge (i <> 0.0) x y;
 tel
 
-node main (i: int) returns (o: int);
+node main (i: real) returns (o: real);
-var garbage: int;
 let
-    garbage = test(0);
+    -- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
-    o = test(1);
+    o = test(i);
 tel