CristalCaveGem » LustreC

      (module C_backend_spec.SrcMod : C_backend_src.MODIFIERS_SRC),

let mk_local n m =

  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_in = mk_local "mem_in"

let mk_mem_out = mk_local "mem_out"

let pp_machine_memtype_name ?(ghost=false) fmt id =

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

let pp_c_type ?var_opt var_id fmt t =

    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt

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

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

    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt

      (pp_c_type ~var_opt:id id.var_id)

      (pp_c_type ~var_opt:id id.var_id) 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 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 = fun 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)

let print_machine_struct ?(ghost=false) fmt m =

      (pp_machine_memtype_name ~ghost) m.mname.node_id

      (if ghost 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)

         ~pp_open_box:pp_open_vbox0

         (pp_c_decl_instance_var ~ghost))

    (pp_machine_memtype_name ~ghost:false) name

    (pp_machine_memtype_name ~ghost:false) name

    (pp_machine_memtype_name ~ghost:false) name

    (pp_machine_memtype_name ~ghost:false) name

    (pp_machine_memtype_name ~ghost:false) name

    (pp_machine_memtype_name ~ghost:false) name

      (pp_machine_memtype_name ~ghost:false) m.mname.node_id

        (pp_machine_memtype_name ~ghost:false) inode.nodei_id

               (pp_machine_memtype_name ~ghost:false) mname

open Utils.Format

open Machine_code_types

open C_backend_common

open Machine_code_common

open Corelang

   (* TODO ACSL

let pp_spec pp fmt =

  fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp

let pp_spec_cut pp fmt =

  fprintf fmt "%a@," (pp_spec pp)

let pp_spec_line pp fmt =

  fprintf fmt "//%@ %a@," pp

let pp_requires pp_req fmt =

  fprintf fmt "requires %a;" pp_req

let pp_ensures pp_ens fmt =

  fprintf fmt "ensures %a;" pp_ens

let pp_assigns pp_asg fmt =

  fprintf fmt "assigns %a;" pp_asg

let pp_ghost pp_gho fmt =

  fprintf fmt "ghost %a" pp_gho

let pp_assert pp_ast fmt =

  fprintf fmt "assert %a;" pp_ast

let pp_mem_valid pp_var fmt (name, var) =

  fprintf fmt "%s_valid(%a)" name pp_var var

let pp_mem_valid' = pp_mem_valid pp_print_string

let pp_indirect pp_field fmt (ptr, field) =

  fprintf fmt "%s->%a" ptr pp_field field

let pp_indirect' = pp_indirect pp_print_string

let pp_access pp_field fmt (stru, field) =

  fprintf fmt "%s.%a" stru pp_field field

let pp_access' = pp_access pp_print_string

let pp_inst self fmt (name, _) =

  pp_indirect' fmt (self, name)

let pp_true fmt () =

  pp_print_string fmt "\\true"

let pp_separated self fmt =

  fprintf fmt "\\separated(@[<h>%s%a@])"

    self

    (pp_print_list

       ~pp_prologue:pp_print_comma

       ~pp_sep:pp_print_comma

       (pp_inst self))

let pp_forall pp_l pp_r fmt (l, r) =

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

    pp_l l

    pp_r r

let pp_valid =

  pp_print_parenthesized

    ~pp_nil:pp_true

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

let pp_equal pp_l pp_r fmt (l, r) =

  fprintf fmt "%a == %a"

    pp_l l

    pp_r r

let pp_implies pp_l pp_r fmt (l, r) =

  fprintf fmt "%a ==>@ %a"

    pp_l l

    pp_r r

let pp_and pp_l pp_r fmt (l, r) =

  fprintf fmt "%a @ && %a"

    pp_l l

    pp_r r

let pp_and_l pp_v fmt =

  pp_print_list

    ~pp_open_box:pp_open_vbox0

    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")

    pp_v

    fmt

let pp_machine_decl fmt (id, mem_type, var) =

  fprintf fmt "struct %s_%s %s" id mem_type var

let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =

  fprintf fmt "%s_ghost%a(%a, %a)"

    name

    (pp_print_option pp_print_int) i

    pp_mem mem

    pp_self self

let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string

let pp_mem_init fmt (name, mem) =

  fprintf fmt "%s_init(%s)" name mem

let pp_var_decl fmt v =

  pp_print_string fmt v.var_id

let pp_ptr_decl fmt v =

  fprintf fmt "*%s" v.var_id

let pp_mem_trans ?i fmt (m, mem_in, mem_out) =

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

    m.mname.node_id

    (pp_print_option pp_print_int) i

    mem_in

    (pp_print_list

       ~pp_epilogue:pp_print_comma

       ~pp_sep:pp_print_comma

       pp_var_decl) m.mstep.step_inputs

    mem_out

    (pp_print_list

       ~pp_prologue:pp_print_comma

       ~pp_sep:pp_print_comma

       pp_ptr_decl) m.mstep.step_outputs

let pp_nothing fmt () =

  pp_print_string fmt "\\nothing"

let pp_predicate pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"

    pp_l l

    pp_r r

let print_machine_valid_predicate fmt m =

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

    let name = m.mname.node_id in

    let self = mk_self m in

    pp_spec

      (pp_predicate

         (pp_mem_valid pp_machine_decl)

         (pp_and

            (pp_and_l (fun fmt (_, (td, _) as inst) ->

                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))

            (pp_valid pp_print_string)))

      fmt

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

       (m.minstances, [self]))

let print_machine_ghost_simulation_aux ?i m pp fmt v =

  let name = m.mname.node_id in

  let self = mk_self m in

  let mem = mk_mem m in

  pp_spec

    (pp_predicate

       (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)

       pp)

    fmt

    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),

     v)

let print_machine_ghost_simulation dependencies m fmt i instr =

  let name = m.mname.node_id in

  let self = mk_self m in

  let mem = mk_mem m in

  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in

  let pred pp v = pp_and prev_ghost pp fmt ((), v) in

  print_machine_ghost_simulation_aux m

    (fun fmt -> function

       | MStateAssign (m, _) ->

         pred

           (pp_equal

              (pp_access (pp_access pp_var_decl))

              (pp_indirect (pp_access pp_var_decl)))

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

         prev_ghost fmt ()

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

         prev_ghost fmt ()

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

         prev_ghost fmt ()

       | MStep (_, i, _)

       | MReset i ->

         begin try

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

             pred

               (pp_mem_ghost pp_access' pp_indirect')

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

           with Not_found -> prev_ghost fmt ()

         end

       | _ -> prev_ghost fmt ())

    ~i:(i+1) fmt instr.instr_desc

let print_machine_ghost_struct fmt m =

  pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m

let print_machine_ghost_simulations dependencies fmt m =

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

    let name = m.mname.node_id in

    let self = mk_self m in

    let mem = mk_mem m in

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

      print_machine_ghost_struct m

      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()

      (pp_print_list_i

        ~pp_epilogue:pp_print_cut

        ~pp_open_box:pp_open_vbox0

        (print_machine_ghost_simulation dependencies m))

      m.mstep.step_instrs

      (print_machine_ghost_simulation_aux m

         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)

let pp_at pp_p fmt (p, l) =

  fprintf fmt "\\at(%a, %s)" pp_p p l

let label_pre = "Pre"

let pp_at_pre pp_p fmt p =

  pp_at pp_p fmt (p, label_pre)

module SrcMod = struct

  let pp_predicates dependencies fmt machines =

    fprintf fmt

      "%a%a"

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")

         print_machine_valid_predicate

         ~pp_epilogue:pp_print_cutcut) machines

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_sep:pp_print_cutcut

         ~pp_prologue:(fun fmt () -> fprintf fmt

                          "/* ACSL ghost simulations */@,%a"

                          (pp_spec_line (pp_ghost pp_print_string))

                          "struct _arrow_mem_ghost {struct _arrow_reg _reg;};")

         (print_machine_ghost_simulations dependencies)

         ~pp_epilogue:pp_print_cutcut) machines

  let pp_reset_spec fmt self m =

    let name = m.mname.node_id in

    let mem = mk_mem m in

    pp_spec_cut (fun fmt () ->

        fprintf fmt

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

          (pp_requires pp_mem_valid') (name, self)

          (pp_requires (pp_separated self)) m.minstances

          (pp_assigns

             (pp_print_list

                ~pp_sep:pp_print_comma

                ~pp_nil:pp_nothing

                (pp_inst self))) m.minstances

          (pp_ensures

             (pp_forall

                pp_machine_decl

                (pp_implies

                   pp_mem_ghost'

                   pp_mem_init)))

          ((name, "mem_ghost", mem),

           ((name, mem, self), (name, mem))))

      fmt ()

  let pp_step_spec fmt self m =

    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_cut (fun fmt () ->

        fprintf fmt

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

          (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs

          (pp_requires pp_mem_valid') (name, self)

          (pp_requires (pp_separated self)) m.minstances

          (pp_assigns

             (if m.mstep.step_outputs = [] && m.minstances = [] then

                pp_nothing

              else

                fun fmt () ->

                  fprintf fmt "@[<h>%a%a@]"

                    (pp_print_list

                       ~pp_sep:pp_print_comma

                       ~pp_epilogue:pp_print_comma

                       pp_ptr_decl) m.mstep.step_outputs

                    (pp_print_list

                       ~pp_sep:pp_print_comma

                       (pp_inst self)) m.minstances)) ()

          (pp_ensures

             (pp_forall

                (fun fmt () ->

                   fprintf fmt "%a, %s"

                     pp_machine_decl (name, "mem_ghost", mem_in)

                     mem_out)

                (pp_implies

                   (pp_at_pre pp_mem_ghost')

                   (pp_implies

                      pp_mem_ghost'

                      pp_mem_trans))))

          ((),

           ((name, mem_in, self),

            ((name, mem_out, self),

             (m, mem_in, mem_out)))))

      fmt ()

  let pp_step_instr_spec m self fmt (i, instr) =

    let name = m.mname.node_id in

    let mem_in = mk_mem_in m in

    let mem_out = mk_mem_out m in

    fprintf fmt "@,%a"

      (pp_spec

         (pp_assert

            (pp_forall

               (fun fmt () ->

                  fprintf fmt "%a, %s"

                    pp_machine_decl (name, "mem_ghost", mem_in)

                    mem_out)

               (pp_implies

                  (pp_at_pre pp_mem_ghost')

                  (pp_implies

                     (pp_mem_ghost' ~i:(i+1))

                     (pp_mem_trans ~i:(i+1)))))))

      ((),

       ((name, mem_in, self),

        ((name, mem_out, self),

         (m, mem_in, mem_out))))

end

module MakefileMod = struct

  let other_targets fmt basename _nodename dependencies =

    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";

    (* EACSL version of library file . c *)

    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;

    fprintf fmt

      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."

      basename basename;

    fprintf fmt "@.";

    fprintf fmt "@.";

    (* EACSL version of library file . c + main .c  *)

    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;

    fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."

      basename basename basename;

    (* Ugly hack to deal with eacsl bugs *)

    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;

    fprintf fmt "@.";

    fprintf fmt "@.";

    (* EACSL version of binary *)

    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;

    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)

    C_backend_makefile.fprintf_dependencies fmt dependencies;

    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."

      basename

      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))

      (C_backend_makefile.compiled_dependencies dependencies)

      ("${FRAMACEACSL}/e_acsl.c "

       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "

       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")

      basename

      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))

      (C_backend_makefile.lib_dependencies dependencies)

    ;

    fprintf fmt "@."

  val pp_predicates: dep_t list -> formatter -> machine_t list -> unit

  val pp_reset_spec: formatter -> ident -> machine_t -> unit

  val pp_step_spec: formatter -> ident -> machine_t -> unit

  val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit

  let pp_predicates _ _ _ = ()

  let pp_reset_spec _ _ _ = ()

  let pp_step_spec _ _ _ = ()

  let pp_step_instr_spec _ _ _ _ = ()

  let pp_machine_nospec_instr dependencies m self fmt _i instr =

    pp_machine_instr dependencies m self fmt instr

  let pp_machine_step_instr dependencies m self fmt i instr =

    fprintf fmt "%a%a%a"

      (if i = 0 then

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

       else

         pp_print_nothing) ()

      (pp_machine_instr dependencies m self) instr

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

      (pp_machine_memtype_name ~ghost:false) m.mname.node_id

      (pp_machine_memtype_name ~ghost:false) m.mname.node_id

      (pp_machine_memtype_name ~ghost:false) m.mname.node_id

      ?(pp_spec=pp_print_nothing)

      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])

      "%a@[<v 2>%a {@,\

      pp_spec ()

      (pp_print_list_i

        ~pp_instr:(pp_machine_nospec_instr dependencies m self)

        ~pp_instr:(pp_machine_nospec_instr dependencies m self)

      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m)

      ~pp_instr:(pp_machine_nospec_instr dependencies m self)

        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)

        ~pp_instr:(pp_machine_step_instr dependencies m self)

        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)

        ~pp_instr:(pp_machine_step_instr dependencies m self)

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

       %a\

      (* Print the spec predicates *)

      (Mod.pp_predicates dependencies) machines

      ?(pp_eol=pp_print_nothing)

      ?(pp_nil=pp_print_nothing)

      ?pp_sep pp_v fmt l =

      (fun fmt () ->

         if l = [] then pp_nil fmt () else pp_print_list ?pp_sep pp_v fmt l) ()