CristalCaveGem » LustreC

   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:

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

   - outputs: decoupled from mems, if necessary

   - locals

let node_local_variables nd =

 List.fold_left (fun locals v -> ISet.add v.var_id 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 global_dependency node =

  let mems = ExprDep.node_memory_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

      if Types.get_clock_base_type vdecl.var_type <> None

      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped

      else ck in

  Env.add_value env vdecl.var_id ck

(* Clocks a variable declaration list *)

  let cuniv = new_carrier Carry_var false in

  new_ck (Carrow (new_ck (Ccarrying (cuniv, univ)) false, univ))

(* Local Variables: *)

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

(* End: *)

exception Scope_clock of clock_expr

exception Error of Location.t * error

let new_id = ref (-1)

let new_ck desc scoped =

 | Ccarrying (cr, _) -> Some cr

 | _                 -> None

let uncarrier ck =

 match ck.cdesc with

 | Ccarrying (_, ck') -> ck'

  in

  aux [] ck

(** [period ck] returns the period of [ck]. Expects a constant pclock

    expression belonging to the correct clock set. *)

let rec period ck =

    let ck = simplify ck in

    match ck.cdesc with

    | Carrow (ck1,ck2) ->

    | Ctuple cklist ->

      fprintf fmt "(%a)" 

	(fprintf_list ~sep:" * " aux) cklist

    Parse.report_error err;

    raise exc

  | Corelang.Error (loc, err) as exc ->

      Corelang.pp_error err

      Location.pp_loc loc;

    raise exc

  try

    Stateless.check_prog decls

  with (Stateless.Error (loc, err)) as exc ->

      Stateless.pp_error err

      Location.pp_loc loc;

    raise exc

      try

	Typing.type_prog env decls

      with (Types.Error (loc,err)) as exc ->

	  Types.pp_error err

	  Location.pp_loc loc;

	raise exc

      try

	Clock_calculus.clock_prog env decls

      with (Clocks.Error (loc,err)) as exc ->

	raise exc

    end

  in

    Stateless.check_compat header

  with

  | (Types.Error (loc,err)) as exc ->

    raise exc

  | Clocks.Error (loc, err) as exc ->

    raise exc

  | Stateless.Error (loc, err) as exc ->

    raise exc

let is_stateful topdecl =

    | None           -> []

    | Some (_, args) -> List.fold_right (fun e r -> match e.expr_desc with Expr_ident id -> id::r | _ -> r) args [] in

  fun v -> is_aliasable v && List.mem v.var_id inputs_var

(* replace variable [v] by [v'] in graph [g].

   [v'] is a dead variable

*)

  end

(* tests whether a variable [v] may be (re)used instead of [var]. The conditions are:

   - same type

   - [v] is not an aliasable input of the equation defining [var]

   - [v] is not one of the current heads (which contain [var])

 *)

let eligible node ctx heads var v =

  && not (is_aliasable_input node var.var_id v)

  && not (List.exists (fun h -> h.var_id = v.var_id) heads)

let compute_reuse node ctx heads var =

  let disjoint = Hashtbl.find ctx.disjoint var.var_id in

  let locally_reusable v =

    IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in

  let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in

  let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in

  try

    let disjoint_live = Disjunction.CISet.inter disjoint live in

    let reuse = Disjunction.CISet.max_elt disjoint_live in

    begin

      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;

      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;

      (*Format.eprintf "%s reused by live@." var.var_id;*)

    end

  with Not_found ->

  try

    let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in

    let reuse = Disjunction.CISet.choose dead in

    begin

      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;

      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;

      (*Format.eprintf "%s reused by dead %a@." var.var_id Disjunction.pp_ciset dead;*)

    end

    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);

    let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in

    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:");

    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@.");

    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@.");

    compute_dependencies heads ctx;

let pp_loc fmt loc =

  let filename = loc.loc_start.Lexing.pos_fname in

  let line = loc.loc_start.Lexing.pos_lnum in

  let start_char =

let report ~level:level p =

if !Options.verbose_level >= level then

(* Local Variables: *)

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

	begin

	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);

       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;

	  Lusic.print_lusic_to_h destname lusic_ext

	end

      else

	end

  end

(* compile a .lus source file *)

let rec compile_source dirname basename extension =

  (* Compatibility with Lusi *)

  (* Checking the existence of a lusi (Lustre Interface file) *)

    "C" ->

      begin

        let extension = ".lusi" in

        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;

      end

  Typing.uneval_prog_generics prog;

  Clock_calculus.uneval_prog_generics prog;

	let source_file = destname ^ ".smt2" in (* Could be changed *)

	let source_out = open_out source_file in

	let fmt = formatter_of_out_channel source_out in

	(* Tracability file if option is activated *)

	if !Options.traces then (

	)

      end

    | "lustre" ->

    | _ -> assert false

  in

  begin

  (* We stop the process here *)

    exit 0

  end

let include_path = Version.include_path

let print_version () =

  Format.printf "Include directory: %s@." include_path

let main_node = ref ""

let horntraces = ref false

let horn_cex = ref false

let options =

    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";

    "-version", Arg.Unit print_version, " displays the version";]

let get_witness_dir filename =

  (* Make sure the directory exists *)

  let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in

%nonassoc UMINUS

%start lustre_annot

%start lustre_spec

%type <LustreSpec.node_annot> lustre_spec

| STRING {Const_string $1}

lustre_annot:

lustre_annot_list:

  { [] } 

let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false

let get_current_node () = try List.hd !node_stack with _ -> assert false

%}

%token <int> INT

| node_ident LPAR expr RPAR EVERY expr

    {mkexpr (Expr_appl ($1, $3, Some $6))}

| node_ident LPAR tuple_expr RPAR

| node_ident LPAR tuple_expr RPAR EVERY expr

/* Boolean expr */

| expr AND expr 

    pp_set_all_formatter_output_functions fmt out flush newline spaces;

  end

let pp_var_name fmt id = fprintf fmt "%s" id.var_id

let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type

let pp_quantifiers fmt (q, vars) =

  match q with

    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 

  in

  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots

let pp_node_eq fmt eq = 

  fprintf fmt "%a = %a;" 

    pp_eq_lhs eq.eq_lhs

   For variables still unrelated, standard compare is used to choose the minimal element.

   This priority is used since it helps a lot in factorizing generated code.

   Moreover, the dependency graph is browsed in a depth-first manner whenever possible,

   In the following functions:

   - [eq_equiv] is the equivalence relation between vars of the same equation lhs

   - [g] the (imperative) graph to be topologically sorted

 List.exists ExprDep.is_instance_var (IdentDepGraph.succ g choice)

(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt [eq_equiv],

*)

let add_successors eq_equiv g v pending frontier =

  let succs_v = IdentDepGraph.succ g v in

  begin

    IdentDepGraph.remove_vertex g v;

	   else

	      frontier := ISet.add v' !frontier)

      ) succs_v;

      with Not_found -> false in

    let n', g = global_dependency n in

	Format.fprintf fmt

	  n'.node_id

	  pp_dep_graph g

      );

    (* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs

     compute: coi predecessors of outputs

     warning (no modification) when memories are non used (do not impact output) or when inputs are not used (do not impact output)

    if !Options.print_reuse

    then

      begin

	    Format.fprintf fmt

	      "OPT:%B@." (try (Hashtbl.iter (fun s1 v2 -> if s1 = v2.var_id then raise Not_found) reuse; false) with Not_found -> true)

	  );

	    Format.fprintf fmt

	      n'.node_id

	      Disjunction.pp_disjoint_map disjoint

	  );

	    Format.fprintf fmt

	      n'.node_id

	      Liveness.pp_reuse_policy reuse

	  );

  List.fold_right (

    fun top_decl (accu_prog, sch_map)  ->

      match top_decl.top_decl_desc with

	  let nd', report = schedule_node nd in

	  IMap.add nd.node_id report sch_map

	| _ -> top_decl::accu_prog, sch_map

    prog

    ([],IMap.empty)

  | []  -> assert false

  | [v] -> Format.fprintf fmt "%s" v

  | _   -> Format.fprintf fmt "(%a)" (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) vl

let pp_schedule fmt node_schs =

 IMap.iter

   (fun nd report ->

    Unbound_value of ident  

  | Already_bound of ident

  | Already_defined of ident

  | Declared_but_undefined of ident

  | Unbound_type of ident

  | Not_a_dimension

    fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2

  | Ttuple tylist ->

    fprintf fmt "(%a)"

  | Tenum taglist ->

    fprintf fmt "enum {%a }"

      (Utils.fprintf_list ~sep:", " pp_print_string) taglist

    fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2

  | Type_mismatch id ->

    fprintf fmt "Definition and declaration of type %s don't agree@." id

    fprintf fmt "No definition provided for variable(s): %a@."

      (Utils.fprintf_list ~sep:"," pp_print_string)

  | Declared_but_undefined id ->

     fprintf fmt "%s is declared but not defined@." id

  | Type_clash (ty1,ty2) ->

 | Tclock ty -> Some ty

 | _         -> None

let rec is_dimension_type ty =

 match (repr ty).tdesc with

 | Tint

let array_type_dimension ty =

  match (dynamic_type ty).tdesc with

  | Tarray (d, _) -> d

let rec array_type_multi_dimension ty =

  match (dynamic_type ty).tdesc with

let array_element_type ty =

  match (dynamic_type ty).tdesc with

  | Tarray (_, ty') -> ty'

let rec array_base_type ty =

  let ty = repr ty in

  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)

  | Tydec_array (d, ty) ->

    begin

      type_dim d;

      Type_predef.type_array d (type_coretype type_dim ty)

    end

  then raise (Error (loc, Not_a_constant))

let rec type_add_const env const arg targ =

  if const

  then let d =

	 if is_dimension_type targ

(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)

and type_dependent_call env in_main loc const f targs =

  let tins, touts = new_var (), new_var () in

  let tfun = Type_predef.type_arrow tins touts in

  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

    begin

      List.iter2 (fun (a,t) ti ->

	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t

    end

(* type a simple call without dependent types 

(** [type_eq env eq] types equation [eq] in environment [env] *)

let type_eq env in_main undefined_vars eq =

  (* Check undefined variables, type lhs *)

  let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in

  let ty_lhs = type_expr env in_main false expr_lhs in

  (* Check multiple variable definitions *)

  let define_var id uvars =

  in

  (* check assignment of declared constant, assignment of clock *)

  let ty_lhs =

 | _                   -> ()

let type_var_decl vd_env env vdecl =

  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

  let eval_const id = Types.get_static_value (Env.lookup_value env id) in

  let type_dim d =

    begin

      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;

      Dimension.eval Basic_library.eval_env eval_const d;

    end in

  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

    if vdecl.var_dec_const

    else ty in

  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;

  new_env

let type_var_decl_list vd_env env l =

  let new_env = Env.overwrite env delta_env in

  let undefined_vars_init =

    List.fold_left

  let undefined_vars =

    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)

  in

  )  nd.node_asserts;

  (* check that table is empty *)

    raise (Error (loc, Undefined_var undefined_vars));

  let ty_ins = type_of_vlist nd.node_inputs in

  let ty_outs = type_of_vlist nd.node_outputs in

      try

	type_node env nd decl.top_decl_loc

      with Error (loc, err) as exc -> (

	  Format.eprintf "Type error: failing node@.%a@.@?"

	    Printers.pp_node nd

	raise exc)

  )

  | ImportedNode nd ->

let check_typedef_top decl =

(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)

(*Format.eprintf "%a" Corelang.print_type_table ();*)

  match decl.top_decl_desc with

  | TypeDef ty ->

       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)

       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in

     let owner' = decl'.top_decl_owner in

     let itf' = decl'.top_decl_itf in

     (match decl'.top_decl_desc with

     | Const _ | Node _ | ImportedNode _ -> assert false

let prefix = "/usr/local"