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 Utils

open Format

open Lustre_types

open Corelang

open Machine_code_types

open Machine_code_common

module Mpfr = Lustrec_mpfr

let pp_print_version fmt () =

  fprintf

    fmt

    "/* @[<v>C code generated by %s@,\

     Version number %s@,\

     Code is %s compliant@,\

     Using %s numbers */@,\

     @]"

    (Filename.basename Sys.executable_name)

    Version.number

    (if !Options.ansi then "ANSI C90" else "C99")

    (if !Options.mpfr then "MPFR multi-precision"

    else "(double) floating-point")

let protect_filename s = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" s

let file_to_module_name basename =

  let baseNAME = Ocaml_utils.uppercase basename in

  let baseNAME = protect_filename baseNAME in

  baseNAME

let pp_ptr fmt = fprintf fmt "*%s"

let reset_label = "Reset"

let pp_label fmt = fprintf fmt "%s:"

let var_is name v = v.var_id = name

let mk_local n m =

  let used name =

    let open List in

    exists (var_is name) m.mstep.step_inputs

    || exists (var_is name) m.mstep.step_outputs

    || exists (var_is name) m.mstep.step_locals

    || exists (var_is name) m.mmemory

  in

  mk_new_name used n

(* Generation of a non-clashing name for the self memory variable (for step and

   reset functions) *)

let mk_self = mk_local "self"

let mk_mem = mk_local "mem"

let mk_mem_c = mk_local "mem_c"

let mk_mem_in = mk_local "mem_in"

let mk_mem_out = mk_local "mem_out"

let mk_mem_in_c = mk_local "mem_in_c"

let mk_mem_out_c = mk_local "mem_out_c"

let mk_mem_reset = mk_local "mem_reset"

(* Generation of a non-clashing name for the instance variable of static

   allocation macro *)

let mk_instance m =

  let used name =

    let open List in

    exists (var_is name) m.mstep.step_inputs || exists (var_is name) m.mmemory

  in

  mk_new_name used "inst"

(* Generation of a non-clashing name for the attribute variable of static

   allocation macro *)

let mk_attribute m =

  let used name =

    let open List in

    exists (var_is name) m.mstep.step_inputs || exists (var_is name) m.mmemory

  in

  mk_new_name used "attr"

let mk_call_var_decl loc id =

  {

    var_id = id;

    var_orig = false;

    var_dec_type = mktyp Location.dummy Tydec_any;

    var_dec_clock = mkclock Location.dummy Ckdec_any;

    var_dec_const = false;

    var_dec_value = None;

    var_parent_nodeid = None;

    var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());

    var_clock = Clocks.new_var true;

    var_loc = loc;

    var_is_contract = false;

  }

(* counter for loop variable creation *)

let loop_cpt = ref (-1)

let reset_loop_counter () = loop_cpt := -1

let mk_loop_var m () =

  let vars =

    m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstep.step_locals @ m.mmemory

  in

  let rec aux () =

    incr loop_cpt;

    let s = sprintf "__%s_%d" "i" !loop_cpt in

    if List.exists (var_is s) vars then aux () else s

  in

  aux ()

(* let addr_cpt = ref (-1)

   let reset_addr_counter () = addr_cpt := -1

   let mk_addr_var m var = let vars = m.mmemory in let rec aux () = incr

   addr_cpt; let s = Printf.sprintf "%s_%s_%d" var "addr" !addr_cpt in if

   List.exists (fun v -> v.var_id = s) vars then aux () else s in aux () *)

let pp_global_init_name fmt id = fprintf fmt "%s_INIT" id

let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id

let pp_machine_memtype_name ?(ghost = false) fmt id =

  fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")

let pp_machine_decl ?(ghost = false) pp_var fmt (id, var) =

  fprintf fmt "%a %a" (pp_machine_memtype_name ~ghost) id pp_var var

let pp_machine_decl' ?(ghost = false) fmt =

  pp_machine_decl ~ghost pp_print_string fmt

let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id

let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id

let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id

let pp_machine_static_declare_name ?(ghost = false) fmt id =

  fprintf fmt "%s_DECLARE%s" id (if ghost then "_GHOST" else "")

let pp_machine_static_link_name ?(ghost = false) fmt id =

  fprintf fmt "%s_LINK%s" id (if ghost then "_GHOST" else "")

let pp_machine_static_alloc_name ?(ghost = false) fmt id =

  fprintf fmt "%s_ALLOC%s" id (if ghost then "_GHOST" else "")

let pp_machine_set_reset_name fmt id = fprintf fmt "%s_set_reset" id

let pp_machine_clear_reset_name fmt id = fprintf fmt "%s_clear_reset" id

let pp_machine_init_name fmt id = fprintf fmt "%s_init" id

let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id

let pp_machine_step_name fmt id = fprintf fmt "%s_step" id

let pp_mod pp_val v1 v2 fmt =

  if !Options.integer_div_euclidean then

    (* (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0) *)

    fprintf

      fmt

      "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"

      pp_val

      v1

      pp_val

      v2

      pp_val

      v1

      pp_val

      v2

      pp_val

      v2

  else

    (* Regular behavior: printing a % *)

    fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

let pp_div pp_val v1 v2 fmt =

  if !Options.integer_div_euclidean then

    (* (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b *)

    fprintf fmt "(%a - %t) / %a" pp_val v1 (pp_mod pp_val v1 v2) pp_val v2

  else

    (* Regular behavior: printing a / *)

    fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

let pp_basic_lib_fun is_int i pp_val fmt vl =

  match i, vl with

  (* | "ite", [v1; v2; v3] -> fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2

     pp_val v3 *)

  | "uminus", [ v ] ->

    fprintf fmt "(- %a)" pp_val v

  | "not", [ v ] ->

    fprintf fmt "(!%a)" pp_val v

  | "impl", [ v1; v2 ] ->

    fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2

  | "=", [ v1; v2 ] ->

    fprintf fmt "(%a == %a)" pp_val v1 pp_val v2

  | "mod", [ v1; v2 ] ->

    if is_int then pp_mod pp_val v1 v2 fmt

    else fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

  | "equi", [ v1; v2 ] ->

    fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2

  | "xor", [ v1; v2 ] ->

    fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2

  | "/", [ v1; v2 ] ->

    if is_int then pp_div pp_val v1 v2 fmt

    else fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

  | _, [ v1; v2 ] ->

    fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2

  | _ ->

    (* TODO: raise proper error *)

    eprintf "internal error: C_backend_common.pp_basic_lib_fun %s@." i;

    assert false

let rec pp_c_dimension fmt dim =

  let open Dimension in

  match dim.dim_desc with

  | Dident id ->

    fprintf fmt "%s" id

  | Dint i ->

    fprintf fmt "%d" i

  | Dbool b ->

    fprintf fmt "%B" b

  | Dite (i, t, e) ->

    fprintf

      fmt

      "((%a)?%a:%a)"

      pp_c_dimension

      i

      pp_c_dimension

      t

      pp_c_dimension

      e

  | Dappl (f, args) ->

    fprintf

      fmt

      "%a"

      (pp_basic_lib_fun (Basic_library.is_numeric_operator f) f pp_c_dimension)

      args

  | Dlink dim' ->

    fprintf fmt "%a" pp_c_dimension dim'

  | Dvar ->

    fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id)

  | Dunivar ->

    fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id)

let is_basic_c_type t =

  Types.(is_int_type t || is_real_type t || is_bool_type t)

let pp_c_basic_type_desc t_desc =

  if Types.is_bool_type t_desc then if !Options.cpp then "bool" else "_Bool"

  else if Types.is_int_type t_desc then !Options.int_type

  else if Types.is_real_type t_desc then

    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type

  else assert false

(* Not a basic C type. Do not handle arrays or pointers *)

let pp_basic_c_type ?(pp_c_basic_type_desc = pp_c_basic_type_desc) ?var_opt fmt

    t =

  match var_opt with

  | Some v when Machine_types.is_exportable v ->

    Machine_types.pp_c_var_type fmt v

  | _ ->

    fprintf fmt "%s" (pp_c_basic_type_desc t)

let pp_c_type ?(var_is_contract = false) ?pp_c_basic_type_desc ?var_opt var_id

    fmt t =

  let rec aux t pp_suffix =

    if is_basic_c_type t then

      fprintf

        fmt

        "%a %s%s%a"

        (pp_basic_c_type ?pp_c_basic_type_desc ?var_opt)

        t

        (if var_is_contract then "\\ghost " else "")

        var_id

        pp_suffix

        ()

    else

      let open Types in

      match (repr t).tdesc with

      | Tclock t' ->

        aux t' pp_suffix

      | Tarray (d, t') ->

        let pp_suffix' fmt () =

          fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d

        in

        aux t' pp_suffix'

      | Tstatic (_, t') ->

        fprintf fmt "const ";

        aux t' pp_suffix

      | Tconst ty ->

        fprintf fmt "%s %s" ty var_id

      | Tarrow (_, _) ->

        fprintf fmt "void (*%s)()" var_id

      | _ ->

        (* TODO: raise proper error *)

        eprintf "internal error: C_backend_common.pp_c_type %a@." pp t;

        assert false

  in

  aux t (fun _ () -> ())

(* let rec pp_c_initialize fmt t = match (Types.repr t).Types.tdesc with |

   Types.Tint -> pp_print_string fmt "0" | Types.Tclock t' -> pp_c_initialize

   fmt t' | Types.Tbool -> pp_print_string fmt "0" | Types.Treal when not

   !Options.mpfr -> pp_print_string fmt "0." | Types.Tarray (d, t') when

   Dimension.is_dimension_const d -> fprintf fmt "{%a}" (Utils.fprintf_list

   ~sep:"," (fun fmt _ -> pp_c_initialize fmt t')) (Utils.duplicate 0

   (Dimension.size_const_dimension d)) | _ -> assert false *)

let pp_c_tag fmt t =

  pp_print_string

    fmt

    (if t = tag_true then "1" else if t = tag_false then "0" else t)

(* Prints a constant value *)

let rec pp_c_const fmt c =

  match c with

  | Const_int i ->

    pp_print_int fmt i

  | Const_real r ->

    Real.pp fmt r

  (* | Const_float r -> pp_print_float fmt r *)

  | Const_tag t ->

    pp_c_tag fmt t

  | Const_array ca ->

    pp_print_braced pp_c_const fmt ca

  | Const_struct fl ->

    pp_print_braced (fun fmt (_, c) -> pp_c_const fmt c) fmt fl

  | Const_string _ | Const_modeid _ ->

    assert false

(* string occurs in annotations not in C *)

let reset_flag_name = "_reset"

let pp_reset_flag ?(indirect = true) pp_stru fmt stru =

  fprintf

    fmt

    "%a%s%s"

    pp_stru

    stru

    (if indirect then "->" else ".")

    reset_flag_name

let pp_reset_flag' ?indirect fmt = pp_reset_flag ?indirect pp_print_string fmt

let pp_reset_assign self fmt b =

  fprintf

    fmt

    "%a = %i;"

    (pp_reset_flag' ~indirect:true)

    self

    (if b then 1 else 0)

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

let rec pp_c_val m self pp_var fmt v =

  let pp_c_val = pp_c_val m self pp_var in

  match v.value_desc with

  | Cst c ->

    pp_c_const fmt c

  | Array vl ->

    pp_print_braced pp_c_val fmt vl

  | Access (t, i) ->

    fprintf fmt "%a[%a]" pp_c_val t pp_c_val i

  | Power (v, _) ->

    (* TODO: raise proper error *)

    eprintf

      "internal error: C_backend_common.pp_c_val %a@."

      (Machine_code_common.pp_val m)

      v;

    assert false

  | Var v ->

    if Machine_code_common.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

        && not (Types.is_real_type v.var_type && !Options.mpfr)

      then fprintf fmt "%a" pp_var v

      else fprintf fmt "%s->_reg.%a" self pp_var v

    else pp_var fmt v

  | Fun (n, vl) ->

    pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl

  | ResetFlag ->

    pp_reset_flag' fmt self

(* Access to the value of a variable: - if it's not a scalar output, then its

   name is enough - otherwise, dereference it (it has been declared as a

   pointer, despite its scalar Lustre type) - moreover, dereference memory array

   variables. *)

let pp_c_var_read ?(test_output = true) m fmt id =

  (* mpfr_t is a static array, not treated as general arrays *)

  if Types.is_address_type id.var_type then

    if

      Machine_code_common.is_memory m id

      && not (Types.is_real_type id.var_type && !Options.mpfr)

    then fprintf fmt "(*%s)" id.var_id

    else fprintf fmt "%s" id.var_id

  else if test_output && Machine_code_common.is_output m id then

    fprintf fmt "*%s" id.var_id

  else fprintf fmt "%s" id.var_id

(* Addressable value of a variable, the one that is passed around in calls: - if

   it's not a scalar non-output, then its name is enough - otherwise, reference

   it (it must be passed as a pointer, despite its scalar Lustre type) *)

let pp_c_var_write m fmt id =

  if Types.is_address_type id.var_type then fprintf fmt "%s" id.var_id

  else if Machine_code_common.is_output m id then fprintf fmt "%s" id.var_id

  else fprintf fmt "&%s" id.var_id

(* Declaration of an input variable: - if its type is array/matrix/etc, then

   declare it as a mere pointer, in order to cope with unknown/parametric array

   dimensions, as it is the case for generics *)

let pp_c_decl_input_var fmt id =

  if !Options.ansi && Types.is_address_type id.var_type then

    pp_c_type

      ~var_opt:id

      (sprintf "(*%s)" id.var_id)

      fmt

      (Types.array_base_type id.var_type)

  else pp_c_type ~var_opt:id id.var_id fmt id.var_type

(* Declaration of an output variable: - if its type is scalar, then pass its

   address - if its type is array/matrix/struct/etc, then declare it as a mere

   pointer, in order to cope with unknown/parametric array dimensions, as it is

   the case for generics *)

let pp_c_decl_output_var fmt id =

  if (not !Options.ansi) && Types.is_address_type id.var_type then

    pp_c_type

      ~var_is_contract:id.var_is_contract

      ~var_opt:id

      id.var_id

      fmt

      id.var_type

  else

    pp_c_type

      ~var_is_contract:id.var_is_contract

      ~var_opt:id

      (sprintf "(*%s)" id.var_id)

      fmt

      (Types.array_base_type id.var_type)

(* Declaration of a local/mem variable: - if it's an array/matrix/etc, its

   size(s) should be known in order to statically allocate memory, so we print

   the full type *)

let pp_c_decl_local_var ?pp_c_basic_type_desc m fmt id =

  if id.var_dec_const then

    fprintf

      fmt

      "%a = %a"

      (pp_c_type ?pp_c_basic_type_desc ~var_opt:id id.var_id)

      id.var_type

      (pp_c_val m "" (pp_c_var_read m))

      (Machine_code_common.get_const_assign m id)

  else

    fprintf

      fmt

      "%a"

      (pp_c_type ?pp_c_basic_type_desc ~var_opt:id id.var_id)

      id.var_type

(* Declaration of a struct variable: - if it's an array/matrix/etc, we declare

   it as a pointer *)

let pp_c_decl_struct_var fmt id =

  if Types.is_array_type id.var_type then

    pp_c_type

      (sprintf "(*%s)" id.var_id)

      fmt

      (Types.array_base_type id.var_type)

  else pp_c_type id.var_id fmt id.var_type

let pp_c_decl_instance_var ?(ghost = false) fmt (name, (node, _)) =

  fprintf

    fmt

    "%a %s%s"

    (pp_machine_memtype_name ~ghost)

    (node_name node)

    (if ghost then "" else "*")

    name

(* let pp_c_checks self fmt m =

 *   pp_print_list

 *     (fun fmt (loc, check) ->

 *        fprintf fmt

 *          "@[<v>%a@,assert (%a);@]"

 *          Location.pp_c_loc loc

 *          (pp_c_val m self (pp_c_var_read m)) check)

 *     fmt

 *     m.mstep.step_checks *)

let has_c_prototype funname dependencies =

  (* We select the last imported node with the name funname. The order of

     evaluation of dependencies should be compatible with overloading. (Not

     checked yet) *)

  let imported_node_opt =

    List.fold_left

      (fun res dep ->

        match res with

        | Some _ ->

          res

        | None ->

          let decls = dep.content in

          let matched t =

            match t.top_decl_desc with

            | ImportedNode nd ->

              nd.nodei_id = funname

            | _ ->

              false

          in

          if List.exists matched decls then

            match (List.find matched decls).top_decl_desc with

            | ImportedNode nd ->

              Some nd

            | _ ->

              assert false

          else None)

      None

      dependencies

  in

  match imported_node_opt with

  | None ->

    false

  | Some nd -> (

    match nd.nodei_prototype with Some "C" -> true | _ -> false)

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

  | ResetFlag ->

    0

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.pp 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_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 if is_reset_flag v then

      fprintf

        fmt

        "%s%s%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

  | _, ResetFlag ->

    pp_reset_flag' fmt self

  | _, _ ->

    eprintf

      "internal error: C_backend_common.pp_value_suffix %a %a %a@."

      Types.pp

      var_type

      (pp_val m)

      value

      pp_suffix

      loop_vars;

    assert false

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

(* Struct Printing functions *)

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

(* let pp_registers_struct fmt m =

 *   pp_print_braced

 *     ~pp_prologue:(fun fmt () ->

 *         fprintf fmt "@[%a " pp_machine_regtype_name m.mname.node_id)

 *     ~pp_open_box:pp_open_vbox0

 *     ~pp_sep:pp_print_semicolon

 *     ~pp_eol:pp_print_semicolon

 *     ~pp_epilogue:(fun fmt () -> pp_print_string fmt "@] _reg;")

 *     pp_c_decl_struct_var

 *     fmt m.mmemory *)

let pp_machine_struct ?(ghost = false) fmt m =

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

    (* Define struct *)

    fprintf

      fmt

      "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"

      (pp_machine_memtype_name ~ghost)

      m.mname.node_id

      (if ghost && not m.mis_contract then

       fun fmt -> function

         | [] ->

           pp_print_nothing fmt ()

         | _ ->

           fprintf fmt "@,%a _reg;" pp_machine_regtype_name m.mname.node_id

      else

        pp_print_list

          ~pp_open_box:pp_open_vbox0

          ~pp_prologue:(fun fmt () ->

            fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)

          ~pp_sep:pp_print_semicolon

          ~pp_eol:pp_print_semicolon'

          ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")

          pp_c_decl_struct_var)

      m.mmemory

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_prologue:pp_print_cut

         ~pp_sep:pp_print_semicolon

         ~pp_eol:pp_print_semicolon'

         (pp_c_decl_instance_var ~ghost))

      m.minstances

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

(* Prototype Printing functions *)

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

let pp_global_init_prototype fmt baseNAME =

  fprintf fmt "void %a ()" pp_global_init_name baseNAME

let pp_global_clear_prototype fmt baseNAME =

  fprintf fmt "void %a ()" pp_global_clear_name baseNAME

let pp_alloc_prototype fmt (name, static) =

  fprintf

    fmt

    "%a * %a %a"

    (pp_machine_memtype_name ~ghost:false)

    name

    pp_machine_alloc_name

    name

    (pp_print_parenthesized pp_c_decl_input_var)

    static

let pp_dealloc_prototype fmt name =

  fprintf

    fmt

    "void %a (%a * _alloc)"

    pp_machine_dealloc_name

    name

    (pp_machine_memtype_name ~ghost:false)

    name

module type MODIFIERS_GHOST_PROTO = sig

  val pp_ghost_parameters :

    ?cut:bool ->

    formatter ->

    (string * (formatter -> string -> unit)) list ->

    unit

end

module EmptyGhostProto : MODIFIERS_GHOST_PROTO = struct

  let pp_ghost_parameters ?cut _ _ = ignore cut

end

module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct

  let pp_mem_ghost name fmt mem =

    pp_machine_decl

      ~ghost:true

      (fun fmt mem -> fprintf fmt "\\ghost %a" pp_ptr mem)

      fmt

      (name, mem)

  let pp_clear_reset_prototype self mem fmt (name, static) =

    fprintf

      fmt

      "@[<v>void %a (%a%a *%s)%a@]"

      pp_machine_clear_reset_name

      name

      (pp_comma_list ~pp_eol:pp_print_comma pp_c_decl_input_var)

      static

      (pp_machine_memtype_name ~ghost:false)

      name