CristalCaveGem » LustreC

open Machine_code_common

(* Computes the depth to which multi-dimension array assignments should be expanded.

   It equals the maximum number of nested static array constructions accessible from root [v].

*)

let rec expansion_depth v =

  match v.value_desc with

  | Cst cst -> expansion_depth_cst cst

  | Var _ -> 0

  | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0

  | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0

  | Access (v, _) -> max 0 (expansion_depth v - 1)

  | Power _  -> 0 (*1 + expansion_depth v*)

and expansion_depth_cst c =

  match c with

  | Const_array cl ->

    1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0

  | _ -> 0

type loop_index = LVar of ident | LInt of int ref | LAcc of value_t

(*

let rec value_offsets v offsets =

 match v, offsets with

 | _                        , []          -> v

 | Power (v, n)             , _ :: q      -> value_offsets v q

 | Array vl                 , LInt r :: q -> value_offsets (List.nth vl !r) q

 | Cst (Const_array cl)     , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q

 | Fun (f, vl)              , _           -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)

 | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q

 | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q

*)

(* Computes the list of nested loop variables together with their dimension bounds.

   - LInt r stands for loop expansion (no loop variable, but int loop index)

   - LVar v stands for loop variable v

*)

let rec mk_loop_variables m ty depth =

  match (Types.repr ty).Types.tdesc, depth with

  | Types.Tarray (d, ty'), 0 ->

    let v = mk_loop_var m () in

    (d, LVar v) :: mk_loop_variables m ty' 0

  | Types.Tarray (d, ty'), _ ->

    let r = ref (-1) in

    (d, LInt r) :: mk_loop_variables m ty' (depth - 1)

  | _, 0 -> []

  | _ -> assert false

let reorder_loop_variables loop_vars =

  let (int_loops, var_loops) =

    List.partition (function (_, LInt _) -> true | _ -> false) loop_vars

  in

  var_loops @ int_loops

(* Prints a one loop variable suffix for arrays *)

let pp_loop_var pp_val fmt lv =

  match snd lv with

  | LVar v -> fprintf fmt "[%s]" v

  | LInt r -> fprintf fmt "[%d]" !r

  | LAcc i -> fprintf fmt "[%a]" pp_val i

(* Prints a suffix of loop variables for arrays *)

let pp_suffix pp_val =

  pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)

let rec is_const_index v =

  match v.value_desc with

  | Cst (Const_int _) -> true

  | Fun (_, vl)       -> List.for_all is_const_index vl

  | _                 -> false

(* Prints a value expression [v], with internal function calls only.

   [pp_var] is a printer for variables (typically [pp_c_var_read]),

   but an offset suffix may be added for array variables

*)

(* Prints a constant value before a suffix (needs casting) *)

let rec pp_c_const_suffix var_type fmt c =

  match c with

  | Const_int i ->

    pp_print_int fmt i

  | Const_real r ->

    Real.pp fmt r

  | Const_tag t ->

    pp_c_tag fmt t

  | Const_array ca ->

    let var_type = Types.array_element_type var_type in

    fprintf fmt "(%a[])%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_c_const_suffix var_type)) ca

  | Const_struct fl ->

    pp_print_braced

      (fun fmt (f, c) ->

         (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)

      fmt fl

  | Const_string _

  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)

(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)

let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt value =

  (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)

  let pp_suffix = pp_suffix (pp_value_suffix ~indirect m self var_type [] pp_var) in

  match loop_vars, value.value_desc with

  | (x, LAcc i) :: q, _ when is_const_index i ->

    let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in

    pp_value_suffix ~indirect m self var_type ((x, LInt r)::q) pp_var fmt value

  | (_, LInt r) :: q, Cst (Const_array cl) ->

    let var_type = Types.array_element_type var_type in

    pp_value_suffix ~indirect m self var_type q pp_var fmt

      (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)

  | (_, LInt r) :: q, Array vl ->

    let var_type = Types.array_element_type var_type in

    pp_value_suffix ~indirect m self var_type q pp_var fmt (List.nth vl !r)

  | loop_var :: q, Array vl      ->

    let var_type = Types.array_element_type var_type in

    fprintf fmt "(%a[])%a%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_value_suffix ~indirect m self var_type q pp_var)) vl

      pp_suffix [loop_var]

  | [], Array vl      ->

    let var_type = Types.array_element_type var_type in

    fprintf fmt "(%a[])%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_value_suffix ~indirect m self var_type [] pp_var)) vl

  | _ :: q, Power (v, _)  ->

    pp_value_suffix ~indirect m self var_type q pp_var fmt v

  | _, Fun (n, vl)   ->

    pp_basic_lib_fun (Types.is_int_type value.value_type) n

      (pp_value_suffix ~indirect m self var_type loop_vars pp_var) fmt vl

  | _, Access (v, i) ->

    let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in

    pp_value_suffix m self var_type

      ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v

  | _, Var v ->

    if is_memory m v then

      (* array memory vars are represented by an indirection to a local var with the right type,

         in order to avoid casting everywhere. *)

      if Types.is_array_type v.var_type

      then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

      else fprintf fmt "%s%s_reg.%a%a"

          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars

    else

      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

  | _, Cst cst ->

    pp_c_const_suffix var_type fmt cst

  | _, _ ->

    eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."

      Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;

    assert false

module VarDecl = struct

  type t = var_decl

  let compare v1 v2 = compare v1.var_id v2.var_id

end

module VDSet = Set.Make(VarDecl)

module Live = Map.Make(Int)

let pp_exists pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"

    pp_l l

    pp_r r

  fprintf fmt "@[<v>%a ==>@ %a@]"

  fprintf fmt "@[<v>%a @ && %a@]"

let pp_paren pp fmt v =

  fprintf fmt "(%a)" pp v

let pp_locals m fmt vs =

  pp_print_list

    ~pp_open_box:pp_open_hbox

    ~pp_sep:pp_print_comma

    (pp_c_decl_local_var m) fmt vs

let rec assigned s instr =

  let open VDSet in

  match instr.instr_desc with

  | MLocalAssign (x, _) ->

    add x s

  | MStep (xs, _, _) ->

    union s (of_list xs)

  | MBranch (_, brs) ->

    List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)

  | _ -> s

let rec occur_val s v =

  let open VDSet in

  match v.value_desc with

  | Var x ->

    add x s

  | Fun (_, vs)

  | Array vs ->

    List.fold_left occur_val s vs

  | Access (v1, v2)

  | Power (v1, v2) ->

    occur_val (occur_val s v1) v2

  | _ -> s

let rec occur s instr =

  let open VDSet in

  match instr.instr_desc with

  | MLocalAssign (_, v)

  | MStateAssign (_, v) ->

    occur_val s v

  | MStep (_, _, vs) ->

    List.fold_left occur_val s vs

  | MBranch (v, brs) ->

    List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)

            (occur_val s v) brs)

  | _ -> s

let live = Hashtbl.create 32

let set_live_of m =

  let open VDSet in

  let locals = of_list m.mstep.step_locals in

  let outputs = of_list m.mstep.step_outputs in

  let vars = union locals outputs in

  let no_occur_after i =

    let occ, _ = List.fold_left (fun (s, j) instr ->

        if j <= i then (s, j+1) else (occur s instr, j+1))

        (empty, 0) m.mstep.step_instrs in

    diff locals occ

  in

  let l, _, _ = List.fold_left (fun (l, asg, i) instr ->

      let asg = inter (assigned asg instr) vars in

      Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)

      (Live.empty, empty, 0) m.mstep.step_instrs in

  Hashtbl.add live m.mname.node_id (Live.add 0 empty l)

let live_i m i =

  Live.find i (Hashtbl.find live m.mname.node_id)

    (name, inputs, locals, outputs, mem_in, mem_out) =

  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a%a@])"

    (pp_print_option

       (fun fmt _ ->

          pp_print_list

            ~pp_epilogue:pp_print_comma

            ~pp_sep:pp_print_comma

            pp_input fmt locals))

    i

let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt

    (m, mem_in, mem_out) =

  let locals, outputs = match i with

    | Some 0 ->

      [], []

    | Some i when i < List.length m.mstep.step_instrs ->

      let li = live_i m i in

      VDSet.(inter (of_list m.mstep.step_locals) li |> elements,

             inter (of_list m.mstep.step_outputs) li |> elements)

    | Some _ ->

      [], m.mstep.step_outputs

    | _ ->

      m.mstep.step_locals, m.mstep.step_outputs

  in

  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt

    (m.mname.node_id,

     m.mstep.step_inputs,

     locals,

     outputs,

     mem_in,

     mem_out)

let pp_mem_trans' ?i fmt =

  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt

let print_ghost_simulation dependencies m fmt (i, instr) =

  let rec aux fmt instr =

    match instr.instr_desc with

    | MStateAssign (m, _) ->

      pp_equal

        (pp_access (pp_access pp_var_decl))

        (pp_indirect (pp_access pp_var_decl))

        fmt

        ((mem, ("_reg", m)), (self, ("_reg", m)))

    | MStep ([i0], i, vl)

      when Basic_library.is_value_internal_fun

          (mk_val (Fun (i, vl)) i0.var_type)  ->

      pp_true fmt ()

    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->

      pp_true fmt ()

    | MStep ([_], i, _) when has_c_prototype i dependencies ->

      pp_true fmt ()

    | MStep (_, i, _)

    | MReset i ->

      begin try

          let n, _ = List.assoc i m.minstances in

          pp_mem_ghost pp_access' pp_indirect' fmt

            (node_name n, (mem, i), (self, i))

        with Not_found -> pp_true fmt ()

      end

    | MBranch (_, brs) ->

      (* TODO: handle branches *)

      pp_and_l aux fmt List.(flatten (map snd brs))

    | _ -> pp_true fmt ()

  in

  pred aux instr

let print_machine_ghost_simulation dependencies m fmt i instr =

    (print_ghost_simulation dependencies m)

    ~i:(i+1)

    fmt (i, instr)

let pp_basic_assign_spec pp_var fmt typ var_name value =

  if Types.is_real_type typ && !Options.mpfr

  then

    assert false

    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)

  else

    pp_equal pp_var pp_var fmt (var_name, value)

let pp_assign_spec m self pp_var fmt (var_type, var_name, value) =

  let depth = expansion_depth value in

  let loop_vars = mk_loop_variables m var_type depth in

  let reordered_loop_vars = reorder_loop_variables loop_vars in

  let rec aux typ fmt vars =

    match vars with

    | [] ->

      pp_basic_assign_spec

        (pp_value_suffix ~indirect:false m self var_type loop_vars pp_var)

        fmt typ var_name value

    | (d, LVar i) :: q ->

      assert false

      (* let typ' = Types.array_element_type typ in

       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

       *   i i i pp_c_dimension d i

       *   (aux typ') q *)

    | (d, LInt r) :: q ->

      assert false

      (* let typ' = Types.array_element_type typ in

       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in

       * fprintf fmt "@[<v 2>{@,%a@]@,}"

       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)

    | _ -> assert false

  in

  begin

    reset_loop_counter ();

    aux var_type fmt reordered_loop_vars;

  end

let print_machine_trans_simulation_aux ?i m pp fmt v =

  let name = m.mname.node_id in

  let mem_in = mk_mem_in m in

  let mem_out = mk_mem_out m in

  pp_spec

    (pp_predicate

       (pp_mem_trans pp_machine_decl pp_machine_decl

          (pp_c_decl_local_var m) pp_c_decl_output_var ?i)

       pp)

    fmt

    ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),

     v)

let print_trans_simulation machines dependencies m fmt (i, instr) =

  let mem_in = mk_mem_in m in

  let mem_out = mk_mem_out m in

  let d = VDSet.(diff (live_i m i) (live_i m (i+1))) in

  printf "%d : %a\n%d : %a\n\n"

    i

    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))

    (i+1)

    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)));

  let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in

  let pred pp v =

    let locals = VDSet.(inter (of_list m.mstep.step_locals) d |> elements) in

    if locals = []

    then pp_and prev_trans pp fmt ((), v)

    else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))

  in

  let rec aux fmt instr = match instr.instr_desc with

    | MLocalAssign (x, v)

    | MStateAssign (x, v) ->

      pp_assign_spec m mem_in (pp_c_var_read m) fmt

        (x.var_type, mk_val (Var x) x.var_type, v)

    | MStep ([i0], i, vl)

      when Basic_library.is_value_internal_fun

          (mk_val (Fun (i, vl)) i0.var_type)  ->

      pp_true fmt ()

    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->

      pp_true fmt ()

    | MStep ([_], i, _) when has_c_prototype i dependencies ->

      pp_true fmt ()

    | MStep (xs, f, ys) ->

      begin try

          let n, _ = List.assoc f m.minstances in

            pp_mem_trans_aux

              pp_access' pp_access'

              (pp_c_val m mem_in (pp_c_var_read m))

              pp_var_decl

              fmt

              (node_name n, ys, [], xs, (mem_in, f), (mem_out, f))

        with Not_found -> pp_true fmt ()

      end

    | MReset f ->

      begin try

          let n, _ = List.assoc f m.minstances in

          pp_mem_init' fmt (node_name n, mem_out)

        with Not_found -> pp_true fmt ()

      end

    | MBranch (v, brs) ->

      (* TODO: handle branches *)

      pp_and_l (fun fmt (l, instrs) ->

          pp_paren (pp_implies

                      (pp_equal

                         (pp_c_val m mem_in (pp_c_var_read m))

                         pp_print_string)

                      (pp_and_l aux))

            fmt

            ((v, l), instrs))

        fmt brs

    | _ -> pp_true fmt ()

  in

  pred aux instr

let print_machine_trans_simulation machines dependencies m fmt i instr =

  print_machine_trans_simulation_aux m

    (print_trans_simulation machines dependencies m)

    ~i:(i+1)

    fmt (i, instr)

let print_machine_core_annotations machines dependencies fmt m =

  if not (fst (Machine_code_common.get_stateless_status m)) then begin

    set_live_of m;

    let i = List.length m.mstep.step_instrs in

    let mem_in = mk_mem_in m in

    let mem_out = mk_mem_out m in

    let last_trans fmt () =

      let locals = VDSet.(inter

                            (of_list m.mstep.step_locals)

                            (live_i m i)

                          |> elements) in

      if locals = []

      then pp_mem_trans' ~i fmt (m, mem_in, mem_out)

      else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt

          (locals, (m, mem_in, mem_out))

    in

    fprintf fmt "%a@,%a%a"

      (print_machine_trans_simulation_aux m pp_true ~i:0) ()

        (print_machine_trans_simulation machines dependencies m))

      (print_machine_trans_simulation_aux m last_trans) ()

  end

          (pp_ite

             (pp_access pp_access')

             (pp_paren

                (pp_and

                   (pp_equal

                      (pp_access pp_access')

                      pp_print_string)

                   (pp_equal pp_print_string pp_print_string)))

                (pp_paren

                   (pp_and

                      (pp_equal

                         (pp_access pp_access')

                         (pp_access pp_access'))

                      (pp_equal pp_print_string pp_print_string))))))

    ((name, ["int x"; "int y"], [], ["_Bool out"],

      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),

     (* (("out", mem_in_first), *)

     (mem_in_first, ((mem_out_first, "false"), ("out", "x")),

      ((mem_out_first, mem_in_first), ("out", "y"))))

         (print_machine_core_annotations machines dependencies)

                     (pp_mem_ghost' ~i)

                     (pp_mem_trans' ~i))))))

    fprintf fmt "%a@,%a%a"

         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i, instr))

      (Mod.pp_step_instr_spec m self) (i+1, instr)