CristalCaveGem » LustreC

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

(*                                                                  *)

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

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

(*                                                                  *)

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

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

(*  version 2.1.                                                    *)

(*                                                                  *)

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

open Machine_code_types

open Spec_common

open Clocks

open Causality

   nodes. But they do not seem to be used by c_backend *)

(*                      si : initialization instructions *)

(*                       j : node aka machine instances  *)

(*                       d : local variables             *)

(*                       s : step instructions           *)

   Local could be memories while other could not. *)

type machine_env = { is_local : string -> bool; get_var : string -> var_decl }

  let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in

    is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);

    get_var =

      (fun id ->

        try List.find (fun v -> v.var_id = id) all

        with Not_found ->

          (* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id

             * VSet.pp all; *)

          raise Not_found);

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

let translate_ident env id =

  try

    (* id is a constant *)

    try

      let vdecl =

        Corelang.var_decl_of_const

          (const_of_top (Hashtbl.find Corelang.consts_table id))

      in

      vdecl_to_val vdecl

    with Not_found -> (

      (* id is a tag, getting its type in the list of declared enums *)

      try id_to_tag id

      with Not_found ->

        Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;

        assert false))

(* specialize predefined (polymorphic) operators wrt their instances, so that

   the C semantics is preserved *)

  | Expr_appl (id, e, r) ->

      List.exists

        (fun e -> Types.is_bool_type e.expr_type)

        (expr_list_of_expr e)

    then

      let id = match id with "=" -> "equi" | "!=" -> "xor" | _ -> id in

    else expr

    expr

let specialize_op expr =

      Cst v

    | Expr_ident x ->

      (translate_ident env x).value_desc

    | Expr_array el ->

      Array (List.map translate_expr el)

    | Expr_access (t, i) ->

      Access (translate_expr t, translate_expr (expr_of_dimension i))

    | Expr_when (e1, _, _) ->

      (translate_expr e1).value_desc

      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))

      (* special treatment depending on the active backend. For functional ones,

         like horn backend, ite are preserved in expression. While they are

         removed for C or Java backends. *)

      Fun ("ite", [ translate_expr g; translate_expr t; translate_expr e ])

      raise NormalizationError

  mk_val value_desc expr.expr_type

    translate_ident env x

    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;

    assert false

  let translate_act = translate_act env in

  let translate_guard = translate_guard env in

    let t, spec_t = translate_act (y, t) in

    let e, spec_e = translate_act (y, e) in

      List.(

        split

          (map

             (fun (t, h) ->

               let h, spec_h = translate_act (y, h) in

               (t, [ h ]), (t, spec_h))

             hl))

    in

    mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl

  match eq.eq_lhs, eq.eq_rhs.expr_desc with

  | ([ x ], Expr_pre _ | [ x ], Expr_fby _) when env.is_local x ->

    VSet.add var_x mems

    mems

(* Datastructure updated while visiting equations *)

type machine_ctx = {

    (var_decl list

    (* inputs *)

    * var_decl list

    (* locals *)

    * var_decl list

    (* outputs *)

    * ISet.t (* memory footprint *)

    * mc_formula_t)

    (* formula *)

    list;

  { m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }

   building *)

    | Con (ck, cr, l) ->

      let id = Clocks.const_of_carrier cr in

        ( (fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),

          mk_control v l inst )

      acc

  fspec, inst

let reset_instance env i r c =

  match r with

  | Some r ->

      control_on_clock env c

        (mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ])

    in

    None, []

  let translate_act = translate_act env in

  let outputs_pi = Lustre_live.inter_live_i_with id (i - 1) outputs in

  let outputs_i = Lustre_live.inter_live_i_with id i outputs in

      locals_i,

      outputs_i,

      ctx.m,

      Exists

        ( Lustre_live.existential_vars id i eq (locals @ outputs),

          And

            [

              mk_transition ~i:(i - 1) id (vdecls_to_vals inputs)

                (vdecls_to_vals locals_pi)

                (vdecls_to_vals outputs_pi);

              a;

            ] ) )

    :: ctx.t

  in

      ctx with

      s =

        {

          inst with

          instr_spec =

            [

                (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);

            ];

        }

        :: ctx.s;

      t = pred_t ctx (fspec spec_t);

    }

    control_on_clock ck (mkinstr' instr)

  in

     Clocks.print_ck eq.eq_rhs.expr_clock; *)

    let c2 = translate_expr e2 in

    assert (c2.value_desc = Cst (Const_tag "false"));

      ctl

        (MStep ([ var_x ], inst, [ c1; c2 ]))

      ctx with

      j = IMap.add inst (td, []) ctx.j;

    ctl

      (MStateAssign (var_x, e))

      (mk_state_variable_pack var_x)

      (mk_state_assign_tr var_x e)

      ctl

        (mk_state_variable_pack var_x)

        (mk_state_assign_tr var_x e2)

      ctx with

    }

  | p, Expr_appl (f, arg, r)

    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->

    let var_p = List.map (fun v -> env.get_var v) p in

    let el = expr_list_of_expr arg in

    let vl = List.map translate_expr el in

    let node_f = node_from_name f in

    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in

      List.fold_right

        (fun arg cks -> arg.expr_clock :: cks)

        el [ eq.eq_rhs.expr_clock ]

    in

    let call_ck =

      Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)

    in

      ctl ~ck:call_ck

        (mk_memory_pack ~inst (node_name node_f))

        ctx

      eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:

      %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple

      env_cks) Clocks.print_ck call_ck;*)

    {

      ctx with

      si =

        (if Stateless.check_node node_f then ctx.si

        else mkinstr (MSetReset inst) :: ctx.si);

    Format.eprintf "internal error: Machine_code.translate_eq %a@?"

      Printers.pp_node_eq eq;

    assert false

    (fun eqs vdecl ->

      if vdecl.var_dec_const then

        {

          eq_lhs = [ vdecl.var_id ];

        }

        :: eqs

    (fun (ctx, i) eq ->

    (ctx, 1) eqs

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

  if Backends.is_functional () then [], [], exprl

  else

    (* Each assert(e) is associated to a fresh variable v and declared as v=e;

       assert (v); *)

        (fun (i, vars, eqlist, assertlist) expr ->

          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in

          let assert_var =

              (* fresh var *)

              ( var_id,

                mktyp loc Tydec_bool,

                mkclock loc Ckdec_any,

                false,

                (* not a constant *)

                None,

                (* no default value *)

                Some nd.node_id )

          (* Types.new_ty (Types.Tbool) *);

          let eq = mkeq loc ([ var_id ], expr) in

          ( i + 1,

            assert_var :: vars,

            eq :: eqlist,

            { expr with expr_desc = Expr_ident var_id } :: assertlist ))

        (1, [], [], []) exprl

    vars, eql, assertl

  let ctx0 =

    translate_eqs env ctx_init nid inputs locals outputs constant_eqs

  in

let memory_pack_0 nd =

  {

    mpname = nd;

    mpindex = Some 0;

      And [ StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero) ];

let memory_pack_toplevel nd i =

  {

    mpname = nd;

    mpindex = None;

      Ternary

        (Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);

let transition_0 nd =

  {

    tname = nd;

    tindex = Some 0;

    tinputs = nd.node_inputs;

    tlocals = [];

    toutputs = [];

    tformula = True;

let transition_toplevel nd i =

  {

    tname = nd;

    tindex = None;

    tinputs = nd.node_inputs;

    tlocals = [];

    toutputs = nd.node_outputs;

      ExistsMem

        ( nd.node_id,

          Predicate (ResetCleared nd.node_id),

          mk_transition nd.node_id ~i

            (vdecls_to_vals nd.node_inputs)

            []

            (vdecls_to_vals nd.node_outputs) );

  let eqs, auts = get_node_eqs nd in

  (* Automata should be expanded by now *)

     to be declared for each assert *)

  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

  (* Build the env: variables visible in the current scope *)

  (* let locals = VSet.of_list locals_list in *)

  (* let inout_vars = nd.node_inputs @ nd.node_outputs in *)

  let env = build_env nd.node_inputs locals nd.node_outputs in

  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)

    Scheduling.sort_equations_from_schedule eqs schedule

  in

   *   VSet.pp locals

   *   VSet.pp inout_vars

   * ; *)

  let mems = get_memories env equations in

  (* Removing computed memories from locals. We also removed unused variables. *)

    List.filter

      (fun v -> (not (VSet.mem v mems)) && not (List.mem v.var_id unused))

      locals

  in

  Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;

  (* Translate equations *)

    translate_core env nd.node_id equations nd.node_inputs locals

      nd.node_outputs

  in

    memory_pack_0 nd

    List.mapi

      (fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f })

      (List.rev ctx.mp)

    @ [ memory_pack_toplevel nd (List.length ctx.mp) ]

  let mtransitions =

    transition_0 nd

    List.mapi

      (fun i (tinputs, tlocals, toutputs, tfootprint, f) ->

          tname = nd;

          tindex = Some (i + 1);

          tinputs;

          tlocals;

          toutputs;

          tformula = red f;

        })

      (List.rev ctx.t)

    @ [ transition_toplevel nd (List.length ctx.t) ]

  in

  let clear_reset =

    mkinstr

      ~instr_spec:

        [

          mk_memory_pack ~i:0 nd.node_id;

          mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];

        ]

      MClearReset

    mname = nd;

      List.filter (fun (_, (n, _)) -> not (Stateless.check_node n)) mmap;

    mconst = List.rev ctx0_s;

      {

        step_inputs = nd.node_inputs;

        step_outputs = nd.node_outputs;

        step_locals = locals;

        step_checks =

          List.map

            (fun d ->

              d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))

            nd.node_checks;

        step_instrs =

          clear_reset

          ::

          (* special treatment depending on the active backend. For horn

             backend, common branches are not merged while they are in C or Java

             backends. *)

          (if !Backends.join_guards then join_guards_list (List.rev ctx.s)

          else List.rev ctx.s);

        step_asserts = List.map (translate_expr env) nd_node_asserts;

      };

    (* Processing spec: there is no processing performed here. Contract have

       been processed already. Either one of the other machine is a cocospec

       node, or the current one is a cocospec node. Contract do not contain any

       statement or import. *)

    List.map

        let sch = IMap.find node.node_id node_schs in

        translate_decl node sch)

      nodes

  machines

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

(* End: *)