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_src.ml
17 17
open C_backend_common
18 18

  
19 19
module type MODIFIERS_SRC = sig
20
  val pp_predicates: dep_t list -> formatter -> machine_t list -> unit
21
  val pp_reset_spec: formatter -> machine_t list -> ident -> machine_t -> unit
22
  val pp_step_spec: formatter -> machine_t list -> ident -> machine_t -> unit
23
  val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
20
  module GhostProto: MODIFIERS_GHOST_PROTO
21
  val pp_predicates: formatter -> machine_t list -> unit
22
  val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit
23
  val pp_clear_reset_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
24
  val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
25
  val pp_step_instr_spec: machine_t -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_set_reset_spec: formatter -> ident -> unit
24 27
end
25 28

  
26 29
module EmptyMod = struct
27
  let pp_predicates _ _ _ = ()
28
  let pp_reset_spec _ _ _ _ = ()
29
  let pp_step_spec _ _ _ _ = ()
30
  module GhostProto = EmptyGhostProto
31
  let pp_predicates _ _ = ()
32
  let pp_set_reset_spec _ _ _ _ = ()
33
  let pp_clear_reset_spec _ _ _ _ _ = ()
34
  let pp_step_spec _ _ _ _ _ = ()
30 35
  let pp_step_instr_spec _ _ _ _ = ()
36
  let pp_ghost_set_reset_spec _ _ = ()
31 37
end
32 38

  
33 39
module Main = functor (Mod: MODIFIERS_SRC) -> struct
34 40

  
41
  module Protos = Protos(Mod.GhostProto)
42

  
35 43
  (********************************************************************************************)
36 44
  (*                    Instruction Printing functions                                        *)
37 45
  (********************************************************************************************)
......
119 127
      (*eprintf "end pp_assign@.";*)
120 128
    end
121 129

  
122
  let pp_machine_ pp_machine_name fn_name m self fmt inst =
123
    let (node, static) = try List.assoc inst m.minstances with Not_found ->
124
      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
125
      raise Not_found
130
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
131
    let name, static =
132
      match inst with
133
      | Some inst ->
134
        let node, static = try List.assoc inst m.minstances with Not_found ->
135
          eprintf "internal error: %s %s %s %s:@."
136
            fn_name m.mname.node_id self inst;
137
          raise Not_found
138
        in
139
        node_name node, static
140
      | None ->
141
        m.mname.node_id, []
126 142
    in
127
    fprintf fmt "%a(%a%s->%s);"
128
      pp_machine_name (node_name node)
129
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
130
         Dimension.pp_dimension) static
131
      self inst
143
    fprintf fmt "%a(%a%s%a);"
144
      pp_machine_name name
145
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
146
      self
147
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
148

  
149
  let pp_machine_set_reset m self fmt inst =
150
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst self
132 151

  
133
  let pp_machine_reset =
134
    pp_machine_ pp_machine_reset_name "pp_machine_reset"
152
  let pp_machine_clear_reset m self fmt =
153
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt self
135 154

  
136
  let pp_machine_init =
137
    pp_machine_ pp_machine_init_name "pp_machine_init"
155
  let pp_machine_init m self fmt inst =
156
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
138 157

  
139
  let pp_machine_clear =
140
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
158
  let pp_machine_clear m self fmt inst =
159
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
141 160

  
142
  let pp_call m self pp_read pp_write fmt i
143
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
161
  let pp_call m self pp_read pp_write fmt i inputs outputs =
144 162
    try (* stateful node instance *)
145 163
      let n, _ = List.assoc i m.minstances in
146
      fprintf fmt "%a (%a%a%s->%s);"
164
      fprintf fmt "%a(%a%a%s->%s);"
147 165
        pp_machine_step_name (node_name n)
148
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
166
        (pp_comma_list ~pp_eol:pp_print_comma
149 167
           (pp_c_val m self pp_read)) inputs
150
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
168
        (pp_comma_list ~pp_eol:pp_print_comma
151 169
           pp_write) outputs
152 170
        self
153 171
        i
154 172
    with Not_found -> (* stateless node instance *)
155 173
      let n, _ = List.assoc i m.mcalls in
156
      fprintf fmt "%a (%a%a);"
174
      fprintf fmt "%a(%a%a);"
157 175
        pp_machine_step_name (node_name n)
158
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
176
        (pp_comma_list ~pp_eol:pp_print_comma
159 177
           (pp_c_val m self pp_read)) inputs
160
        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
178
        (pp_comma_list pp_write) outputs
161 179

  
162 180
  let pp_basic_instance_call m self =
163 181
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
164 182

  
165
  let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
183
  let pp_arrow_call m self fmt i outputs =
184
    match outputs with
185
    | [x] ->
186
      fprintf fmt "%a = %a(%s->%s);"
187
        (pp_c_var_read m) x
188
        pp_machine_step_name Arrow.arrow_id
189
        self
190
        i
191
    | _ -> assert false
192

  
193
  let pp_instance_call m self fmt i inputs outputs =
166 194
    let pp_offset pp_var indices fmt var =
167 195
      fprintf fmt "%a%a"
168 196
        pp_var var
......
196 224
  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
197 225
    match get_instr_desc instr with
198 226
    | MNoReset _ -> ()
199
    | MReset i ->
200
      pp_machine_reset m self fmt i
227
    | MSetReset inst ->
228
      pp_machine_set_reset m self fmt inst
229
    | MClearReset ->
230
      fprintf fmt "%t@,%a"
231
        (pp_machine_clear_reset m self) pp_label reset_label
201 232
    | MLocalAssign (i,v) ->
202 233
      pp_assign
203 234
        m self (pp_c_var_read m) fmt
......
217 248
        i
218 249
        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
219 250
    | MStep (il, i, vl) ->
220
      pp_basic_instance_call m self fmt i vl il
251
      let td, _ = List.assoc i m.minstances in
252
      if Arrow.td_is_arrow td then
253
        pp_arrow_call m self fmt i il
254
      else
255
        pp_basic_instance_call m self fmt i vl il
221 256
    | MBranch (_, []) ->
222 257
      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
223 258
        (pp_instr m) instr;
......
249 284
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
250 285
    pp_machine_instr dependencies m self fmt instr
251 286

  
252
  let pp_machine_step_instr dependencies m self fmt i instr =
253
    fprintf fmt "%a%a%a"
254
      (if i = 0 then
255
         (fun fmt () -> fprintf fmt "%a@,"
256
             (Mod.pp_step_instr_spec m self) (i, instr))
257
       else
258
         pp_print_nothing) ()
287
  let pp_machine_step_instr dependencies m self fmt _i instr =
288
    fprintf fmt "%a%a"
259 289
      (pp_machine_instr dependencies m self) instr
260
      (Mod.pp_step_instr_spec m self) (i+1, instr)
290
      (Mod.pp_step_instr_spec m self) instr
261 291

  
262 292
  (********************************************************************************************)
263 293
  (*                         C file Printing functions                                        *)
......
438 468
    then
439 469
      (* C99 code *)
440 470
      pp_print_function
441
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
442
        ~pp_prototype:print_stateless_prototype
471
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
472
        ~pp_prototype:Protos.print_stateless_prototype
443 473
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
444 474
        ~pp_local:(pp_c_decl_local_var m)
445 475
        ~base_locals:m.mstep.step_locals
......
459 489
          let (id, _, _) = call_of_expr e
460 490
          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
461 491
      pp_print_function
462
        ~pp_prototype:print_stateless_prototype
492
        ~pp_prototype:Protos.print_stateless_prototype
463 493
        ~prototype:(m.mname.node_id,
464 494
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
465 495
                    m.mstep.step_outputs)
......
474 504
        ~instrs:m.mstep.step_instrs
475 505
        fmt
476 506

  
477
  let print_reset_code machines dependencies self fmt m =
507
  let print_clear_reset_code machines dependencies self mem fmt m =
478 508
    pp_print_function
479
      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt machines self m)
480
      ~pp_prototype:(print_reset_prototype self)
509
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
510
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
481 511
      ~prototype:(m.mname.node_id, m.mstatic)
482 512
      ~pp_local:(pp_c_decl_local_var m)
483 513
      ~base_locals:(const_locals m)
......
485 515
      ~instrs:m.minit
486 516
      fmt
487 517

  
518
  let print_set_reset_code self mem fmt m =
519
    pp_print_function
520
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
521
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
522
      ~prototype:(m.mname.node_id, m.mstatic)
523
      ~pp_extra:(fun fmt () -> fprintf fmt "self->_reset = 1;%a"
524
                    Mod.pp_ghost_set_reset_spec mem)
525
      fmt
526

  
488 527
  let print_init_code self fmt m =
489 528
    let minit = List.map (fun i ->
490
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
529
        match get_instr_desc i with
530
        | MSetReset i -> i
531
        | _ -> assert false)
532
        m.minit in
491 533
    pp_print_function
492
      ~pp_prototype:(print_init_prototype self)
534
      ~pp_prototype:(Protos.print_init_prototype self)
493 535
      ~prototype:(m.mname.node_id, m.mstatic)
494 536
      ~pp_array_mem:(pp_c_decl_array_mem self)
495 537
      ~array_mems:(array_mems m)
......
505 547

  
506 548
  let print_clear_code self fmt m =
507 549
    let minit = List.map (fun i ->
508
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
550
        match get_instr_desc i with
551
        | MSetReset i -> i
552
        | _ -> assert false) m.minit in
509 553
    pp_print_function
510
      ~pp_prototype:(print_clear_prototype self)
554
      ~pp_prototype:(Protos.print_clear_prototype self)
511 555
      ~prototype:(m.mname.node_id, m.mstatic)
512 556
      ~pp_array_mem:(pp_c_decl_array_mem self)
513 557
      ~array_mems:(array_mems m)
......
521 565
            fmt minit)
522 566
      fmt
523 567

  
524
  let print_step_code machines dependencies self fmt m =
568
  let print_step_code machines dependencies self mem fmt m =
525 569
    if not (!Options.ansi && is_generic_node (node_of_machine m))
526 570
    then
527 571
      (* C99 code *)
528 572
      pp_print_function
529
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
530
        ~pp_prototype:(print_step_prototype self)
573
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
574
        ~pp_prototype:(Protos.print_step_prototype self mem)
531 575
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
532 576
        ~pp_local:(pp_c_decl_local_var m)
533 577
        ~base_locals:m.mstep.step_locals
......
549 593
          let id, _, _ = call_of_expr e in
550 594
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
551 595
      pp_print_function
552
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
553
        ~pp_prototype:(print_step_prototype self)
596
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
597
        ~pp_prototype:(Protos.print_step_prototype self mem)
554 598
        ~prototype:(m.mname.node_id,
555 599
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
556 600
                    m.mstep.step_outputs)
......
706 750
      print_stateless_code machines dependencies fmt m
707 751
    else
708 752
      let self = mk_self m in
709
      fprintf fmt "@[<v>%a%a@,@,%a%a@]"
753
      let mem = mk_mem m in
754
      fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
710 755
        print_alloc_function m
711
        (* Reset function *)
712
        (print_reset_code machines dependencies self) m
756
        (* Reset functions *)
757
        (print_clear_reset_code machines dependencies self mem) m
758
        (print_set_reset_code self mem) m
713 759
        (* Step function *)
714
        (print_step_code machines dependencies self) m
760
        (print_step_code machines dependencies self mem) m
715 761
        (print_mpfr_code self) m
716 762

  
717 763
  let print_import_standard source_fmt () =
......
826 872
         ~pp_epilogue:pp_print_cutcut) machines
827 873

  
828 874
      (* Print the spec predicates *)
829
      (Mod.pp_predicates dependencies) machines
875
      Mod.pp_predicates machines
830 876

  
831 877
      (* Print nodes one by one (in the previous order) *)
832 878
      (pp_print_list

Also available in: Unified diff