CristalCaveGem » LustreC

let pp_acsl_basic_type_desc t_desc =

  if Types.is_bool_type t_desc then

    (* if !Options.cpp then "bool" else "_Bool" *)

    "integer"

  else if Types.is_int_type t_desc then

    (* !Options.int_type *)

    "integer"

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

  pp_print_braced

    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid(")

    ~pp_epilogue:pp_print_cpar

let pp_different pp_l pp_r fmt (l, r) =

  fprintf fmt "%a != %a"

    pp_l l

    pp_r r

  fprintf fmt "%s_initialization(%a)" name pp_mem mem

    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs

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 pp_c_var_read 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

    fprintf fmt "%s" id.var_id

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

  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt

let pp_mem_trans'' ?i fmt =

          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)

          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)

          ?i)

  let d = VDSet.(diff (union (live_i m i) (assigned empty instr))

                   (live_i m (i+1))) in

  (* XXX *)

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

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

    (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr));

    let vars = VDSet.(union (of_list m.mstep.step_locals)

                        (of_list m.mstep.step_outputs)) in

    let locals = VDSet.(inter vars d |> elements) in

      (* if let t = fst (List.hd brs) in t = tag_true || t = tag_false

       * then (\* boolean case *\)

       *   let tl = try List.assoc tag_true  brs with Not_found -> [] in

       *   let el = try List.assoc tag_false brs with Not_found -> [] in

       *   pp_ite (pp_c_val m mem_in (pp_c_var_read m))

       *     (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux))

       *     fmt (v, tl, el)

       * else (\* enum type case *\) *)

          let pp_val = pp_c_val m mem_in (pp_c_var_read m) in

          if l = tag_false then

            pp_paren (pp_implies

                        (pp_different pp_val pp_c_tag)

                        (pp_and_l aux))

              fmt

              ((v, tag_true), instrs)

          else

            pp_paren (pp_implies

                        (pp_equal pp_val pp_c_tag)

                        (pp_and_l aux))

              fmt

              ((v, l), instrs))

let print_machine_trans_annotations machines dependencies fmt m =

let print_machine_init_predicate fmt m =

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

    let name = m.mname.node_id in

    let mem_in = mk_mem_in m in

    pp_spec

      (pp_predicate

         (pp_mem_init pp_machine_decl)

         (pp_and_l (fun fmt (i, (td, _)) ->

              pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))

      fmt

      ((name, (name, "mem_ghost", mem_in)), m.minstances)

  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"

    (pp_spec_cut

       (pp_predicate

          (pp_mem_valid pp_machine_decl)

          (pp_valid pp_print_string)))

    ((name, (name, "mem", "*" ^ self)), [self])

             pp_print_int)))

     (mem_in_first, 1))

                      pp_print_int)

    ((name, ["integer x"; "integer y"], [], ["integer out"],

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

      "%a@,%a%a%a%a"

         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")

         print_machine_init_predicate

         ~pp_epilogue:pp_print_cutcut) machines

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_sep:pp_print_cutcut

         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")

         (print_machine_trans_annotations machines dependencies)

                      pp_mem_trans''))))

                     (pp_mem_trans'' ~i))))))