CristalCaveGem » LustreC

type param_t = {

  unfold_arrow_active : bool;

  force_alias_ite : bool;

  force_alias_internal_fun : bool;

}

let params =

  ref

    {

      unfold_arrow_active = false;

      force_alias_ite = false;

      force_alias_internal_fun = false;

    }

type norm_ctx_t = {

  parentid : ident;

  vars : var_decl list;

  is_output : ident -> bool;

}

let expr_true loc ck =

    expr_tag = Utils.new_tag ();

    expr_desc = Expr_const (Const_tag tag_true);

    expr_type = Type_predef.type_bool;

    expr_clock = ck;

    expr_delay = Delay.new_var ();

    expr_annot = None;

    expr_loc = loc;

  {

    expr_tag = Utils.new_tag ();

    expr_desc = Expr_const (Const_tag tag_false);

    expr_type = Type_predef.type_bool;

    expr_clock = ck;

    expr_delay = Delay.new_var ();

    expr_annot = None;

    expr_loc = loc;

  }

  {

    expr_tag = Utils.new_tag ();

    expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);

    expr_type = Type_predef.type_bool;

    expr_clock = ck;

    expr_delay = Delay.new_var ();

    expr_annot = None;

    expr_loc = loc;

  }

  match expr.expr_desc with

  | Expr_arrow (e1, e2) ->

      let loc = expr.expr_loc in

      let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in

      { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }

  | _ -> assert false

  try

    Some

      (List.find

         (fun eq ->

           Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock

           && is_eq_expr eq.eq_rhs expr)

         defs)

  with Not_found -> None

  match locals with

  | [] -> assert false

  | [ v ] ->

      { expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id }

  | _ ->

      {

        expr with

        expr_tag = Utils.new_tag ();

        expr_desc = Expr_tuple (List.map expr_of_vdecl locals);

      }

    Log.report ~plugin:"normalization" ~level:2 (fun fmt ->

        Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt

          Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck

          expr.expr_clock);

  | Expr_ident _ -> (defs, vars), expr

  | _ -> (

      match get_expr_alias defs expr with

      | Some eq ->

          (* Format.eprintf "Found a preexisting definition@."; *)

          let aliases =

            List.map

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

              eq.eq_lhs

          in

          (defs, vars), replace_expr aliases expr

      | None ->

          (*

           Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;

          * Format.eprintf "existing defs are: @[[%a@]]@."

          *   (fprintf_list ~sep:"@ "(fun fmt eq ->

          *        Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"

          *          Clocks.print_ck eq.eq_rhs.expr_clock

          *          (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)

          *          (is_eq_expr eq.eq_rhs expr)

          *          Printers.pp_node_eq eq))

          *   defs; *)

          if opt then

            let new_aliases =

              List.map2

                (mk_fresh_var

                   (norm_ctx.parentid, norm_ctx.vars @ vars)

                   expr.expr_loc)

                (Types.type_list_of_type expr.expr_type)

                (Clocks.clock_list_of_clock expr.expr_clock)

            in

            let new_def =

              mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)

            in

            (* Typing and Registering machine type *)

            let _ =

              if Machine_types.is_active then

                Machine_types.type_def

                  (norm_ctx.parentid, norm_ctx.vars)

                  new_aliases expr

            in

            (new_def :: defs, new_aliases @ vars), replace_expr new_aliases expr

          else (defs, vars), expr)

(* Similar fonctions for dimensions *)

  | Dimension.Dbool _ | Dint _ | Dident _ ->

      (defs, vars), dim (* Keep the same *)

  | _ when opt ->

      (* Cast to expression, normalizing *)

      let e = expr_of_dimension dim in

      let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in

      defvars, dimension_of_expr e

  | _ -> (defs, vars), dim

(* Keep the same *)

    let defvars, d =

      mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d

    in

    let new_e =

      {

        e with

        expr_desc = Expr_access (e, d);

      }

    (*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)

  List.fold_left add_offset (defvars, e) offsets

  let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in

  {

    ref_e with

    expr_type =

      Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type;

  }

      defvars, norm_t :: qlist)

    elist (defvars, [])

let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets

    defvars expr =

  | Expr_const _ | Expr_ident _ -> unfold_offsets norm_ctx defvars expr offsets

      let defvars, norm_elist =

        normalize_list alias norm_ctx offsets

          (fun _ -> normalize_array_expr ~alias:true)

          defvars elist

      in

      let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

      let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1

      normalize_expr ~alias norm_ctx (d :: offsets) defvars e1

      let defvars, norm_elist =

        normalize_list alias norm_ctx offsets

          (fun alias -> normalize_expr ~alias ~alias_basic:false)

          defvars elist

      in

      defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

    when Basic_library.is_homomorphic_fun id

         && Types.is_array_type expr.expr_type ->

      let defvars, norm_args =

        normalize_list alias norm_ctx offsets

          (fun _ -> normalize_array_expr ~alias:true)

          defvars (expr_list_of_expr args)

      in

      ( defvars,

        mk_norm_expr offsets expr

          (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )

  | Expr_appl (id, args, None)

    when Basic_library.is_expr_internal_fun expr

         && not (!params.force_alias_internal_fun || alias_basic) ->

      let defvars, norm_args =

        normalize_expr ~alias:true norm_ctx offsets defvars args

      in

      defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))

      let defvars, r =

        match r with

        | None -> defvars, None

        | Some r ->

            let defvars, norm_r =

              normalize_expr ~alias_basic:true norm_ctx [] defvars r

            in

            defvars, Some norm_r

      in

      let defvars, norm_args = normalize_expr norm_ctx [] defvars args in

      let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in

      if offsets <> [] then

        let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in

        normalize_expr ~alias norm_ctx offsets defvars norm_expr

      else

        mk_expr_alias_opt

          (alias

          && (!params.force_alias_internal_fun || alias_basic

             || not (Basic_library.is_expr_internal_fun expr)))

          norm_ctx defvars norm_expr

      (* Here we differ from Colaco paper: arrows are pushed to the top *)

      normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr)

  | Expr_arrow (e1, e2) ->

      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

      let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

      let norm_expr =

        mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2))

      in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

      let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

      let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

      let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

      defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))

      let defvars, norm_c = normalize_guard norm_ctx defvars c in

      let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

      let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

      let norm_expr =

        mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))

      in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

      let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in

      mk_expr_alias_opt alias norm_ctx defvars norm_expr

      let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in

      defvars, (t, norm_h) :: norm_q)

and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =

      let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

      defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))

      normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1

  | Expr_access (e1, d) ->

      normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1

      let defvars, norm_elist =

        normalize_list alias norm_ctx offsets

          (fun _ -> normalize_array_expr ~alias:true)

          defvars elist

      in

      defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

      let defvars, norm_args =

        normalize_list alias norm_ctx offsets

          (fun _ -> normalize_array_expr ~alias:true)

          defvars (expr_list_of_expr args)

      in

      ( defvars,

        mk_norm_expr offsets expr

          (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )

  | _ -> normalize_expr ~alias norm_ctx offsets defvars expr

and normalize_cond_expr ?(alias = true) norm_ctx offsets defvars expr =

      normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1

      let defvars, norm_c = normalize_guard norm_ctx defvars c in

      let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

      let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

      defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))

      let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

      defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))

      (* Forcing alias creation for then/else expressions *)

      let defvars, norm_expr =

        normalize_expr ~alias norm_ctx offsets defvars expr

      in

      mk_expr_alias_opt true norm_ctx defvars norm_expr

  | _ ->

      (* default case without the force_alias_ite option *)

      normalize_expr ~alias norm_ctx offsets defvars expr

  let defvars, norm_expr =

    normalize_expr ~alias_basic:true norm_ctx [] defvars expr

  in

    | [], [], [] -> defvars, []

    | v :: qv, t :: qt, c :: qc ->

        let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in

        if norm_ctx.is_output v then

          let newvar =

            mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c

          in

          let neweq = mkeq eq.eq_loc ([ v ], expr_of_vdecl newvar) in

          (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q

        else (defs_q, vars_q), v :: lhs_q

    | _ -> assert false

  in

    fold_lhs defvars eq.eq_lhs

      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock)

  in

  defvars', { eq with eq_lhs = lhs' }

  (*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)

  | Expr_pre _ | Expr_fby _ ->

      let defvars', eq' = decouple_outputs norm_ctx defvars eq in

      let (defs', vars'), norm_rhs =

        normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs

      in

      let norm_eq = { eq' with eq_rhs = norm_rhs } in

      norm_eq :: defs', vars'

      let (defs', vars'), norm_rhs =

        normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

      in

      let norm_eq = { eq with eq_rhs = norm_rhs } in

      norm_eq :: defs', vars'

  | Expr_appl (id, _, None)

    when Basic_library.is_homomorphic_fun id

         && Types.is_array_type eq.eq_rhs.expr_type ->

      let (defs', vars'), norm_rhs =

        normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

      in

      let norm_eq = { eq with eq_rhs = norm_rhs } in

      norm_eq :: defs', vars'

      let (defs', vars'), norm_rhs =

        normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

      in

      let norm_eq = { eq with eq_rhs = norm_rhs } in

      norm_eq :: defs', vars'

      let (defs', vars'), norm_rhs =

        normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

      in

      let norm_eq = { eq with eq_rhs = norm_rhs } in

      norm_eq :: defs', vars'

    List.fold_right

      (fun eq (def, vars) ->

        if eq_defs = [ eq ] then eq :: def, vars

        else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs)

      defs ([], vars)

  with ex ->

let normalize_pred_eexpr norm_ctx (def, vars) ee =

  assert (ee.eexpr_quantifiers = []);

  (* We do not normalize quantifiers yet. This is for very far future. *)

  if skip then ee, (def, vars)

  else

    let output_var =

      mkvar_decl ee.eexpr_loc

        ( output_id,

          mktyp ee.eexpr_loc Tydec_bool,

          (* It is a predicate, hence a bool *)

          mkclock ee.eexpr_loc Ckdec_any,

          false (* not a constant *),

          None,

          None )

       result. *)

    let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in

    let defs, vars =

      List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ]

    in

    let vars = output_var :: vars in

    (* let todefine =

       List.fold_left

         (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)

         (ISet.add output_id ISet.empty) vars in

    *)

      (*

      ee', (defs, vars)

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

      eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee

        Types.pp_error err

        (Utils.fprintf_list ~sep:", " Printers.pp_node_eq)

        defs Location.pp_loc loc;

      raise exc

(*

                                                 *)

(* We use node local vars to make sure we are creating fresh variables *)

  let not_is_orig_var v = List.for_all (( != ) v) orig_vars in

  let norm_ctx =

    {

      parentid;

      is_output =

        (fun _ -> false) (* no need to introduce fresh variables for outputs *);

  let eqs, auts =

    List.fold_right

      (fun s (el, al) ->

        match s with Eq e -> e :: el, al | Aut a -> el, a :: al)

      s.stmts ([], [])

  if auts != [] then assert false;

  (* Automata should be expanded by now. *)

  let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in

    let res =

      List.fold_right

        (fun ee (accu, defvars) ->

          let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in

          ee' :: accu, defvars)

        l ([], defvars)

    List.fold_right

      (fun m (accu_m, defsvars) ->

        { m with require = require'; ensure = ensure' } :: accu_m, defsvars)

      s.modes ([], defsvars)

  let new_locals = List.filter not_is_orig_var vars in

  (* removing inouts and initial locals ones *)

  ( new_locals,

    defs,

    {

      s with

      (* locals = s.locals @ new_locals; *)

      stmts = [];

      assume = assume';

      guarantees = guarantees';

      modes = modes';

    } )

  let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in

  let not_is_orig_var v = List.for_all (( != ) v) orig_vars in

  let norm_ctx =

    {

      is_output =

        (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);

  if auts != [] then assert false;

  (* Automata should be expanded by now. *)

    (* Update mutable fields of eexpr to perform normalization of

       specification.

       Careful: we do not normalize annotations, since they can have the form

       x = (a, b, c) *)

    match node.node_spec with

    | None | Some (NodeSpec _) -> node.node_spec, [], eqs

    | Some (Contract s) ->

        let new_locals, new_stmts, s' =

          normalize_spec node.node_id

            (node.node_inputs, node.node_outputs, node.node_locals)

            s

        in

        (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;

         * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)

        Some (Contract s'), new_locals, new_stmts @ eqs

    List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs

  in

    List.fold_left

      (fun (vars, def_accu, assert_accu) assert_ ->

        let assert_expr = assert_.assert_expr in

        let (defs, vars'), expr =

          normalize_expr ~alias:true

            (* forcing introduction of new equations for fcn calls *)

            norm_ctx []

            (* empty offset for arrays *)

            ([], vars)

            (* defvar only contains vars *)

            assert_expr

        in

        ( vars',

          defs @ def_accu,

          { assert_ with assert_expr = expr } :: assert_accu ))

      (vars, [], []) node.node_asserts

  in

  let new_locals = List.filter not_is_orig_var vars in

  (* we filter out inout

     vars and initial locals ones *)

  let all_locals = node.node_locals @ new_locals in

  (* we add again, at the

     beginning of the list the

     local declared ones *)

  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)

  *)

      let diff_vars =

        List.filter (fun v -> not (List.mem v node.node_locals)) all_locals

      in

      let norm_traceability =

        {

          annots =

            List.map

              (fun v ->

                let eq =

                  try

                    List.find

                      (fun eq ->

                        List.exists (fun v' -> v' = v.var_id) eq.eq_lhs)

                      (defs @ assert_defs)

                  with Not_found ->

                    Format.eprintf

                      "Traceability annotation generation: var %s not found@."

                      v.var_id;

                    assert false

                in

                let expr =

                  substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs

                in

                let pair =

                  mkeexpr expr.expr_loc

                    (mkexpr expr.expr_loc

                       (Expr_tuple

                          [ expr_of_ident v.var_id expr.expr_loc; expr ]))

                in

                Annotations.add_expr_ann node.node_id pair.eexpr_tag

                  [ "traceability" ];

                [ "traceability" ], pair)

              diff_vars;

          annot_loc = Location.dummy_loc;

        }

      in

      norm_traceability :: node.node_annot

    else node.node_annot

    List.fold_left

      (fun annots v ->

        if Machine_types.is_active && Machine_types.is_exportable v then (

          let typ = Machine_types.get_specified_type v in

          let typ_name = Machine_types.type_name typ in

          let loc = v.var_loc in

          let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in

          let pair =

            expr_to_eexpr

              (expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])

          in

          Annotations.add_expr_ann node.node_id pair.eexpr_tag

            Machine_types.keyword;

          { annots = [ Machine_types.keyword, pair ]; annot_loc = loc }

          :: annots)

        else annots)

      new_annots new_locals

    {

      node with

  in

  (*Printers.pp_node Format.err_formatter node;*)

  node

  | None | Some (NodeSpec _) -> nd

  | Some (Contract _) -> assert false

let normalize_decl (decl : top_decl) : top_decl =

      let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in

      update_node nd.node_id decl';

      decl'

      let decl' =

        { decl with top_decl_desc = ImportedNode (normalize_inode nd) }

      in

      update_node nd.nodei_id decl';

      decl'

  | Include _ | Open _ | Const _ | TypeDef _ -> decl

  mk_expr_alias_opt opt

    { parentid; vars = ctx_vars; is_output = (fun _ -> false) }

    (defs, vars) expr

(* Local Variables: *)

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

(* End: *)