Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/backends/C/c_backend_common.ml
37 37
  let baseNAME = protect_filename baseNAME in
38 38
  baseNAME
39 39

  
40
let pp_ptr fmt =
41
  fprintf fmt "*%s"
42

  
43
let reset_label = "Reset"
44

  
45
let pp_label fmt =
46
  fprintf fmt "%s:"
47

  
40 48
let var_is name v =
41 49
  v.var_id = name
42 50

  
......
55 63
let mk_mem = mk_local "mem"
56 64
let mk_mem_in = mk_local "mem_in"
57 65
let mk_mem_out = mk_local "mem_out"
66
let mk_mem_reset = mk_local "mem_reset"
58 67

  
59 68
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
60 69
let mk_instance m =
......
118 127
let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
119 128
let pp_machine_memtype_name ?(ghost=false) fmt id =
120 129
  fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")
130
let pp_machine_decl ?(ghost=false) pp_var fmt (id, var) =
131
  fprintf fmt "%a %a" (pp_machine_memtype_name ~ghost) id pp_var var
132
let pp_machine_decl' ?(ghost=false) fmt =
133
  pp_machine_decl ~ghost pp_print_string fmt
121 134
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
122 135
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
123 136
let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id
124 137
let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id
125 138
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id
126 139
let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id
127
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
140
let pp_machine_set_reset_name fmt id = fprintf fmt "%s_set_reset" id
141
let pp_machine_clear_reset_name fmt id = fprintf fmt "%s_clear_reset" id
128 142
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
129 143
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
130 144
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
......
583 597
      then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
584 598
      else fprintf fmt "%s%s_reg.%a%a"
585 599
          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
600
    else if is_reset_flag v then
601
      fprintf fmt "%s%s%a%a"
602
          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
586 603
    else
587 604
      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
588 605
  | _, Cst cst ->
......
610 627
let print_machine_struct ?(ghost=false) fmt m =
611 628
  if not (fst (Machine_code_common.get_stateless_status m)) then
612 629
    (* Define struct *)
613
    fprintf fmt "@[<v 2>%a {%a%a@]@,};"
630
    fprintf fmt "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"
614 631
      (pp_machine_memtype_name ~ghost) m.mname.node_id
615 632
      (if ghost then
616 633
         (fun fmt -> function
......
658 675
    pp_machine_dealloc_name name
659 676
    (pp_machine_memtype_name ~ghost:false) name
660 677

  
661
let print_reset_prototype self fmt (name, static) =
662
  fprintf fmt "void %a (%a%a *%s)"
663
    pp_machine_reset_name name
664
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
665
       pp_c_decl_input_var) static
666
    (pp_machine_memtype_name ~ghost:false) name
667
    self
668

  
669
let print_init_prototype self fmt (name, static) =
670
  fprintf fmt "void %a (%a%a *%s)"
671
    pp_machine_init_name name
672
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
673
       pp_c_decl_input_var) static
674
    (pp_machine_memtype_name ~ghost:false) name
675
    self
676

  
677
let print_clear_prototype self fmt (name, static) =
678
  fprintf fmt "void %a (%a%a *%s)"
679
    pp_machine_clear_name name
680
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
681
       pp_c_decl_input_var) static
682
    (pp_machine_memtype_name ~ghost:false) name
683
    self
684

  
685
let print_stateless_prototype fmt (name, inputs, outputs) =
686
  fprintf fmt "void %a (@[<v>%a%a@])"
687
    pp_machine_step_name name
688
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
689
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
690
    (pp_print_list ~pp_sep:pp_print_comma pp_c_decl_output_var) outputs
691

  
692
let print_step_prototype self fmt (name, inputs, outputs) =
693
  fprintf fmt "void %a (@[<v>%a%a%a *%s@])"
694
    pp_machine_step_name name
695
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
696
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
697
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
698
       ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
699
    (pp_machine_memtype_name ~ghost:false) name
700
    self
678
module type MODIFIERS_GHOST_PROTO = sig
679
  val pp_ghost_parameters: formatter -> (string * (formatter -> string -> unit)) list -> unit
680
end
681

  
682
module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct
683
  let pp_ghost_parameters _ _ = ()
684
end
685

  
686
module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
687

  
688
  let pp_mem_ghost name fmt mem =
689
    pp_machine_decl ~ghost:true
690
      (fun fmt mem -> fprintf fmt "\ghost %a" pp_ptr mem) fmt
691
      (name, mem)
692

  
693
  let print_clear_reset_prototype self mem fmt (name, static) =
694
    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
695
      pp_machine_clear_reset_name name
696
      (pp_comma_list ~pp_eol:pp_print_comma
697
         pp_c_decl_input_var) static
698
      (pp_machine_memtype_name ~ghost:false) name
699
      self
700
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
701

  
702
  let print_set_reset_prototype self mem fmt (name, static) =
703
    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
704
      pp_machine_set_reset_name name
705
      (pp_comma_list ~pp_eol:pp_print_comma
706
         pp_c_decl_input_var) static
707
      (pp_machine_memtype_name ~ghost:false) name
708
      self
709
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
710

  
711
  let print_step_prototype self mem fmt (name, inputs, outputs) =
712
    fprintf fmt "@[<v>void %a (@[<v>%a%a%a *%s@])%a@]"
713
      pp_machine_step_name name
714
      (pp_comma_list ~pp_eol:pp_print_comma
715
         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
716
      (pp_comma_list ~pp_eol:pp_print_comma
717
         ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
718
      (pp_machine_memtype_name ~ghost:false) name
719
      self
720
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
721

  
722
  let print_init_prototype self fmt (name, static) =
723
    fprintf fmt "void %a (%a%a *%s)"
724
      pp_machine_init_name name
725
      (pp_comma_list ~pp_eol:pp_print_comma
726
         pp_c_decl_input_var) static
727
      (pp_machine_memtype_name ~ghost:false) name
728
      self
729

  
730
  let print_clear_prototype self fmt (name, static) =
731
    fprintf fmt "void %a (%a%a *%s)"
732
      pp_machine_clear_name name
733
      (pp_comma_list ~pp_eol:pp_print_comma
734
         pp_c_decl_input_var) static
735
      (pp_machine_memtype_name ~ghost:false) name
736
      self
737

  
738
  let print_stateless_prototype fmt (name, inputs, outputs) =
739
    fprintf fmt "void %a (@[<v>%a%a@])"
740
      pp_machine_step_name name
741
      (pp_comma_list ~pp_eol:pp_print_comma
742
         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
743
      (pp_comma_list pp_c_decl_output_var) outputs
744

  
745
end
701 746

  
702 747
let print_import_prototype fmt dep =
703 748
  fprintf fmt "#include \"%s.h\"" dep.name

Also available in: Unified diff