CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *) 

(*  This file was originally from the Prelude compiler              *)

(*                                                                  *) 

(********************************************************************)

(** Simple modular syntactic causality analysis. Can reject correct

    programs, especially if the program is not flattened first. *)

open Utils

open LustreSpec

open Corelang

open Graph

open Format

type error =

  | DataCycle of ident list

  | NodeCycle of ident list

exception Error of error

module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)

(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)

module Bfs = Traverse.Bfs (IdentDepGraph)

(* Dependency of mem variables on mem variables is cut off 

   by duplication of some mem vars into local node vars.

   Thus, cylic dependency errors may only arise between no-mem vars.

   non-mem variables are:

   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars

   - read mems (fake vars): same remark as above.

   - outputs: decoupled from mems, if necessary

   - locals

   - instance vars (fake vars): simplify causality analysis

   global constants are not part of the dependency graph.

no_mem' = combinational(no_mem, mem);

=> (mem -> no_mem' -> no_mem)

mem' = pre(no_mem, mem);

=> (mem' -> no_mem), (mem -> mem')

   Global roadmap:

   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)

   - check cycles in g (a cycle means a dependency error)

   - break cycles in g' (it's legal !):

     - check cycles in g'

     - if any, introduce aux var to break cycle, then start afresh

   - insert g' into g

   - return g

*)

(* Tests whether [v] is a root of graph [g], i.e. a source *)

let is_graph_root v g =

 IdentDepGraph.in_degree g v = 0

(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)

let graph_roots g =

 IdentDepGraph.fold_vertex

   (fun v roots -> if is_graph_root v g then v::roots else roots)

   g []

let add_edges src tgt g =

(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)

 List.iter

   (fun s ->

     List.iter

       (fun t -> IdentDepGraph.add_edge g s t)

       tgt)

   src;

  g

let add_vertices vtc g =

(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)

 List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;

  g

let new_graph () =

 IdentDepGraph.create ()

module ExprDep = struct

let instance_var_cpt = ref 0

(* read vars represent input/mem read-only vars,

   they are not part of the program/schedule,

   as they are not assigned,

   but used to compute useless inputs/mems.

   a mem read var represents a mem at the beginning of a cycle  *)

let mk_read_var id =

 sprintf "#%s" id

(* instance vars represent node instance calls,

   they are not part of the program/schedule,

   but used to simplify causality analysis

    *)

let mk_instance_var id =

 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt

let is_read_var v = v.[0] = '#'

let is_instance_var v = v.[0] = '!'

let is_ghost_var v = is_instance_var v || is_read_var v

let undo_read_var id =

 assert (is_read_var id);

 String.sub id 1 (String.length id - 1)

let undo_instance_var id =

 assert (is_instance_var id);

 String.sub id 1 (String.length id - 1)

let eq_memory_variables mems eq =

  let rec match_mem lhs rhs mems =

    match rhs.expr_desc with

    | Expr_fby _

    | Expr_pre _    -> List.fold_right ISet.add lhs mems

    | Expr_tuple tl -> 

      let lhs' = (transpose_list [lhs]) in

      List.fold_right2 match_mem lhs' tl mems

    | _             -> mems in

  match_mem eq.eq_lhs eq.eq_rhs mems

let node_memory_variables nd =

 List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

let node_input_variables nd =

 List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs

let node_local_variables nd =

 List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals

let node_constant_variables nd =

  List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals

let node_output_variables nd =

 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs

let node_auxiliary_variables nd =

 ISet.diff (node_local_variables nd) (node_memory_variables nd)

let node_variables nd =

  let inputs = node_input_variables nd in

  let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in

  List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals

(* computes the equivalence relation relating variables 

   in the same equation lhs, under the form of a table 

   of class representatives *)

let node_eq_equiv nd =

  let eq_equiv = Hashtbl.create 23 in

  List.iter (fun eq ->

    let first = List.hd eq.eq_lhs in

    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs

  )

    (get_node_eqs nd);

  eq_equiv

(* Create a tuple of right dimension, according to [expr] type, *)

(* filled with variable [v] *)

let adjust_tuple v expr =

 match expr.expr_type.Types.tdesc with

 | Types.Ttuple tl -> duplicate v (List.length tl)

 | _         -> [v]

(* Add dependencies from lhs to rhs in [g, g'], *)

(* no-mem/no-mem and mem/no-mem in g            *)

(* mem/mem in g'                                *)

(*     match (lhs_is_mem, ISet.mem x mems) with

      | (false, true ) -> (add_edges [x] lhs g,

			   g')

      | (false, false) -> (add_edges lhs [x] g,

			   g')

      | (true , false) -> (add_edges lhs [x] g,

			   g')

      | (true , true ) -> (g,

			   add_edges [x] lhs g')

*)

let add_eq_dependencies mems inputs node_vars eq (g, g') =

  let add_var lhs_is_mem lhs x (g, g') =

    if is_instance_var x || ISet.mem x node_vars then

      if ISet.mem x mems

      then

	let g = add_edges lhs [mk_read_var x] g in

	if lhs_is_mem

	then

	  (g, add_edges [x] lhs g')

	else

	  (add_edges [x] lhs g, g')

      else

	let x = if ISet.mem x inputs then mk_read_var x else x in

	(add_edges lhs [x] g, g')

    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)

  in

  (* Add dependencies from [lhs] to rhs clock [ck]. *)

  let rec add_clock lhs_is_mem lhs ck g =

    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)

    match (Clocks.repr ck).Clocks.cdesc with

    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)

    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g

    | _                         -> g 

  in

  let rec add_dep lhs_is_mem lhs rhs g =

    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)

    (* i.e every input is connected to every output, through a ghost var *)

    let mashup_appl_dependencies f e g =

      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in

      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)

	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 

    in

    match rhs.expr_desc with

    | Expr_const _    -> g

    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)

    | Expr_pre e      -> add_dep true lhs e g

    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)

    | Expr_access (e1, d)

    | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)

    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g

    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g

    | Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)

    | Expr_ite   (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))

    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)

    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)

    | Expr_appl (f, e, None) ->

      if Basic_library.is_expr_internal_fun rhs

      (* tuple component-wise dependency for internal operators *)

      then

	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g

      (* mashed up dependency for user-defined operators *)

      else

	mashup_appl_dependencies f e g

    | Expr_appl (f, e, Some c) ->

      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

  in

  let g =

    List.fold_left

      (fun g lhs ->

	if ISet.mem lhs mems then

	  add_vertices [lhs; mk_read_var lhs] g

	else

	  add_vertices [lhs] g

      )

      g eq.eq_lhs

  in

  add_dep false eq.eq_lhs eq.eq_rhs (g, g')

(* Returns the dependence graph for node [n] *)

let dependence_graph mems inputs node_vars n =

  instance_var_cpt := 0;

  let g = new_graph (), new_graph () in

  (* Basic dependencies *)

  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in

  (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il

     faut imposer que les outputs dépendent des asserts pour identifier que les

     fcn calls des asserts sont évalués avant le noeuds *)

  (* (\* In order to introduce dependencies between assert expressions and the node, *)

  (*    we build an artificial dependency between node output and each assert *)

  (*    expr. While these are not valid equations, they should properly propage in *)

  (*    function add_eq_dependencies *\) *)

  (* let g = *)

  (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)

  (*   List.fold_left (fun g ae -> *)

  (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)

  (*   add_eq_dependencies mems inputs node_vars fake_eq g *)

  (* ) g n.node_asserts in  *)

  g

   end

   module NodeDep = struct

   module ExprModule =

   struct

   type t = expr

   let compare = compare

   let hash n = Hashtbl.hash n

   let equal n1 n2 = n1 = n2

   end

   module ESet = Set.Make(ExprModule)

   let rec get_expr_calls prednode expr = 

   match expr.expr_desc with

   | Expr_const _ 

   | Expr_ident _ -> ESet.empty

   | Expr_access (e, _)

   | Expr_power (e, _) -> get_expr_calls prednode e

   | Expr_array t

   | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty

   | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty

   | Expr_fby (e1,e2)

   | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)

   | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))

   | Expr_pre e 

   | Expr_when (e,_,_) -> get_expr_calls prednode e

   | Expr_appl (id,e, _) ->

   if not (Basic_library.is_expr_internal_fun expr) && prednode id

   then ESet.add expr (get_expr_calls prednode e)

   else (get_expr_calls prednode e)

   let get_callee expr =

   match expr.expr_desc with

   | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)

   | _ -> None

   let get_calls prednode eqs =

   let deps =

   List.fold_left 

   (fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))

   ESet.empty

   eqs in

   ESet.elements deps

   let dependence_graph prog =

   let g = new_graph () in

   let g = List.fold_right 

   (fun td accu -> (* for each node we add its dependencies *)

      match td.top_decl_desc with 

	| Node nd ->

	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)

	  let accu = add_vertices [nd.node_id] accu in

	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in

	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)

	  add_edges [nd.node_id] deps accu

	| _ -> assert false (* should not happen *)

    ) prog g in

  g   

  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)

  let slice_graph gr v =

    begin

      let gr' = new_graph () in

      IdentDepGraph.add_vertex gr' v;

      Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v;

      gr'

    end

  let rec filter_static_inputs inputs args =

   match inputs, args with

   | []   , [] -> []

   | v::vq, a::aq -> if v.var_dec_const && Types.is_dimension_type v.var_type then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq

   | _ -> assert false

  let compute_generic_calls prog =

    List.iter

      (fun td ->

	match td.top_decl_desc with 

	| Node nd ->

	  let prednode n = is_generic_node (Hashtbl.find node_table n) in

	  nd.node_gencalls <- get_calls prednode (get_node_eqs nd)

	| _ -> ()

      ) prog

end

module CycleDetection = struct

(* ---- Look for cycles in a dependency graph *)

  module Cycles = Graph.Components.Make (IdentDepGraph)

  let mk_copy_var n id =

    let used name =

         (List.exists (fun v -> v.var_id = name) n.node_locals)

      || (List.exists (fun v -> v.var_id = name) n.node_inputs)

      || (List.exists (fun v -> v.var_id = name) n.node_outputs)

    in mk_new_name used id

  let mk_copy_eq n var =

    let var_decl = get_node_var var n in

    let cp_var = mk_copy_var n var in

    let expr =

      { expr_tag = Utils.new_tag ();

	expr_desc = Expr_ident var;

	expr_type = var_decl.var_type;

	expr_clock = var_decl.var_clock;

	expr_delay = Delay.new_var ();

	expr_annot = None;

	expr_loc = var_decl.var_loc } in

    { var_decl with var_id = cp_var; var_orig = false },

    mkeq var_decl.var_loc ([cp_var], expr)

  let wrong_partition g partition =

    match partition with

    | [id]    -> IdentDepGraph.mem_edge g id id

    | _::_::_ -> true

    | []      -> assert false

(* Checks that the dependency graph [g] does not contain a cycle. Raises

   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)

  let check_cycles g =

    let scc_l = Cycles.scc_list g in

    List.iter (fun partition ->

      if wrong_partition g partition then

	raise (Error (DataCycle partition))

      else ()

    ) scc_l

(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)

  let copy_partition g partition =

    let copy_g = IdentDepGraph.create () in

    IdentDepGraph.iter_edges

      (fun src tgt ->

	if List.mem src partition && List.mem tgt partition

	then IdentDepGraph.add_edge copy_g src tgt)

      g

(* Breaks dependency cycles in a graph [g] by inserting aux variables.

  [head] is a head of a non-trivial scc of [g]. 

   In Lustre, this is legal only for mem/mem cycles *)

  let break_cycle head cp_head g =

    let succs = IdentDepGraph.succ g head in

    IdentDepGraph.add_edge g head cp_head;

    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);

    List.iter

      (fun s ->

	IdentDepGraph.remove_edge g head s;

	IdentDepGraph.add_edge    g s cp_head)

      succs

(* Breaks cycles of the dependency graph [g] of memory variables [mems]

   belonging in node [node]. Returns:

   - a list of new auxiliary variable declarations

   - a list of new equations

   - a modified acyclic version of [g]

*)

  let break_cycles node mems g =

    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) (get_node_eqs node) in

    let rec break vdecls mem_eqs g =

      let scc_l = Cycles.scc_list g in

      let wrong = List.filter (wrong_partition g) scc_l in

      match wrong with

      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)

      | [head]::_       ->

	begin

	  IdentDepGraph.remove_edge g head head;

	  break vdecls mem_eqs g

	end

      | (head::part)::_ -> 

	begin

	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in

	  let pvar v = List.mem v part in

	  let fvar v = if v = head then vdecl_cp_head.var_id else v in

	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in

	  break_cycle head vdecl_cp_head.var_id g;

	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g

	end

      | _               -> assert false

    in break [] mem_eqs g

end

(* Module used to compute static disjunction of variables based upon their clocks. *)

module Disjunction =

struct

  module ClockedIdentModule =

  struct

    type t = var_decl

    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock

    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)

  end

  module CISet = Set.Make(ClockedIdentModule)

  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,

     maybe removing shorter branches *)

  type disjoint_map = (ident, CISet.t) Hashtbl.t

  let pp_ciset fmt t =

    begin

      Format.fprintf fmt "{@ ";

      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;

      Format.fprintf fmt "}@."

    end

  let clock_disjoint_map vdecls =

    let map = Hashtbl.create 23 in

    begin

      List.iter

	(fun v1 -> let disj_v1 =

		     List.fold_left

		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)

		       CISet.empty

		       vdecls in

		   (* disjoint vdecls are stored in increasing branch length order *)

		   Hashtbl.add map v1.var_id disj_v1)

	vdecls;

      (map : disjoint_map)

    end

  (* merge variables [v] and [v'] in disjunction [map]. Then:

      - the mapping v' becomes v' |-> (map v) inter (map v')

      - the mapping v |-> ... then disappears

      - other mappings become x |-> (map x) \ (if v in x then v else v')

  *)

  let merge_in_disjoint_map map v v' =

    begin

      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));

      Hashtbl.remove map v.var_id;

      Hashtbl.iter (fun x map_x -> Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map;

    end

  (* replace variable [v] by [v'] in disjunction [map].

    [v'] is a dead variable. Then:

      - the mapping v' becomes v' |-> (map v)

      - the mapping v |-> ... then disappears

      - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)

  *)

  let replace_in_disjoint_map map v v' =

    begin

      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);

      Hashtbl.remove  map v.var_id;

      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) else CISet.remove v' mapx)) map;

    end

  (* remove variable [v] in disjunction [map]. Then:

      - the mapping v |-> ... then disappears

      - all mappings become x |-> (map x) \ { v}

  *)

  let remove_in_disjoint_map map v =

    begin

      Hashtbl.remove map v.var_id;

      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;

    end

  let pp_disjoint_map fmt map =

    begin

      Format.fprintf fmt "{ /* disjoint map */@.";

      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;

      Format.fprintf fmt "}@."

    end

end

let pp_dep_graph fmt g =

  begin

    Format.fprintf fmt "{ /* graph */@.";

    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;

    Format.fprintf fmt "}@."

  end

let pp_error fmt err =

  match err with

  | DataCycle trace ->

     fprintf fmt "@.Causality error, cyclic data dependencies: %a@."

       (fprintf_list ~sep:", " pp_print_string) trace

  | NodeCycle trace ->

     fprintf fmt "@.Causality error, cyclic node calls: %a@."

       (fprintf_list ~sep:", " pp_print_string) trace

(* Merges elements of graph [g2] into graph [g1] *)

let merge_with g1 g2 =

  begin

    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;

    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2

  end

let world = "!!_world"

let add_external_dependency outputs mems g =

  begin

    IdentDepGraph.add_vertex g world;

    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;

    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;

  end

let global_dependency node =

  let mems = ExprDep.node_memory_variables node in

  let inputs =

    ISet.union

      (ExprDep.node_input_variables node)

      (ExprDep.node_constant_variables node) in

  let outputs = ExprDep.node_output_variables node in

  let node_vars = ExprDep.node_variables node in

  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in

  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;

  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)

  CycleDetection.check_cycles g_non_mems;

  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in

  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)

  begin

    merge_with g_non_mems g_mems';

    add_external_dependency outputs mems g_non_mems;

    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 

    g_non_mems

  end

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)