CristalCaveGem » LustreC

   - where are used the mconst. They contain initialization of constant in

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

(* Machine processing requires knowledge about variables and local variables.

   Local could be memories while other could not. *)

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

  {

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

(* Basic functions to translate to machine values, instructions *)

  with Not_found -> (

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

    if

      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

  | _ ->

    expr

  match !Options.output with "C" -> specialize_to_c expr | _ -> expr

  let value_desc =

    | Expr_power (e, n) ->

    | Expr_ite (g, t, e) when Backends.is_functional () ->

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

      Format.eprintf "Normalization error for backend %s: %a@." !Options.output

  | Expr_ident x ->

    translate_ident env x

  let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in

    mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e

    let hl, spec_hl =

      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

    mk_assign ~lustre_eq y e, mk_assign_tr y e

let get_memory env mems eq =

  match eq.eq_lhs, eq.eq_rhs.expr_desc with

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

  | _ ->

    mems

let get_memories env = List.fold_left (get_memory env) VSet.empty

  m : ISet.t;

  si : instr_t list;

  j : (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;

  s : instr_t list;

  mp : mc_formula_t list;

  t :

    (var_decl list

    (* inputs *)

    * var_decl list

    (* locals *)

    * var_decl list

    (* outputs *)

    * ISet.t (* memory footprint *)

    * mc_formula_t)

    (* formula *)

    list;

let ctx_init =

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

(* Main function to translate equations into this machine context we are

   building *)

let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))

  let rec aux ((fspec, inst) as acc) ck =

      aux

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

          mk_control v l inst )

    | _ ->

      acc

    let _, inst =

      control_on_clock env c

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

    in

  | None ->

    None, []

  let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in

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

  let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in

    ( inputs,

      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 =

            [

              mk_transition ~i id (vdecls_to_vals inputs)

                (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);

            ];

        }

        :: ctx.s;

  let ctl ?(ck = eq.eq_rhs.expr_clock) instr =

    control_on_clock ck (mkinstr' instr)

  in

  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq

     Clocks.print_ck eq.eq_rhs.expr_clock; *)

  | [ x ], Expr_arrow (e1, e2) ->

    let ctx =

      ctl

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

        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])

    {

      ctx with

  | [ x ], Expr_pre e when env.is_local x ->

  | [ x ], Expr_fby (e1, e2) when env.is_local x ->

    let ctx =

      ctl

    {

      ctx with

    let env_cks =

      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

    let ctx =

      ctl ~ck:call_ck

    (*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)

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

      s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;

  | [ x ], _ ->

  List.fold_left

    (fun eqs vdecl ->

      if vdecl.var_dec_const then

        {

          eq_lhs = [ vdecl.var_id ];

          eq_loc = vdecl.var_loc;

        }

        :: eqs

  List.fold_left

    (fun (ctx, i) eq ->

(* Processing nodes *)

  let exprl = List.map (fun assert_ -> assert_.assert_expr) nd.node_asserts in

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

  else

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

       assert (v); *)

      List.fold_left

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

            mkvar_decl loc ~orig:false

              (* fresh var *)

              ( var_id,

                mktyp loc Tydec_bool,

                mkclock loc Ckdec_any,

                false,

                (* not a constant *)

                None,

                (* no default value *)

                Some nd.node_id )

          assert_var.var_type <- Type_predef.type_bool

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

  (* Compute constants' instructions *)

  let ctx0 =

    translate_eqs env ctx_init nid inputs locals outputs constant_eqs

  in

    mpformula =

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

    mpformula =

      Ternary

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

    tfootprint = ISet.empty;

    tformula =

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

  assert (auts = []);

  (* Automata should be expanded by now *)

  let sorted_eqs, unused =

    Scheduling.sort_equations_from_schedule eqs schedule

  in

  let locals =

    List.filter

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

      locals

  in

  let ctx, ctx0_s =

    translate_core env nd.node_id equations nd.node_inputs locals

      nd.node_outputs

  in

    ::

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

    ::

    List.mapi

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

          tfootprint;

        })

      (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

    minstances =

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

    mstep =

      {

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

        let node = node_of_top decl in

        let sch = IMap.find node.node_id node_schs in

        translate_decl node sch)

      nodes