Project

General

Profile

« Previous | Next » 

Revision c4780a6a

Added by LĂ©lio Brun 7 months ago

work on new reset functions generation

View differences:

src/backends/C/c_backend_src.ml
20 20
  module GhostProto: MODIFIERS_GHOST_PROTO
21 21
  val pp_predicates: formatter -> machine_t list -> unit
22 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
23
  val pp_clear_reset_spec: formatter -> ident -> ident -> machine_t -> unit
24 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
25
  val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_parameter: ident -> formatter -> ident option -> unit
27 27
end
28 28

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

  
39 39
module Main = functor (Mod: MODIFIERS_SRC) -> struct
......
55 55
  let rec static_loop_profile v =
56 56
    match v.value_desc with
57 57
    | Cst cst  -> static_loop_profile_cst cst
58
    | Var _  -> []
58
    | Var _  | ResetFlag -> []
59 59
    | Fun (_, vl) ->
60 60
      List.fold_right
61 61
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
......
81 81
  let pp_c_val m self pp_var fmt v =
82 82
    pp_value_suffix m self v.value_type [] pp_var fmt v
83 83

  
84
  let pp_basic_assign pp_var fmt typ var_name value =
85
    if Types.is_real_type typ && !Options.mpfr
86
    then
87
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
88
    else
89
      fprintf fmt "%a = %a;"
90
        pp_var var_name
91
        pp_var value
92

  
93
  (* type_directed assignment: array vs. statically sized type
94
     - [var_type]: type of variable to be assigned
95
     - [var_name]: name of variable to be assigned
96
     - [value]: assigned value
97
     - [pp_var]: printer for variables
98
  *)
99
  let pp_assign m self pp_var fmt var_type var_name value =
100
    let depth = expansion_depth value in
101
    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
102
    let loop_vars = mk_loop_variables m var_type depth in
103
    let reordered_loop_vars = reorder_loop_variables loop_vars in
104
    let rec aux typ fmt vars =
105
      match vars with
106
      | [] ->
107
        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
108
          fmt typ var_name value
109
      | (d, LVar i) :: q ->
110
        let typ' = Types.array_element_type typ in
111
        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
112
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
113
          i i i pp_c_dimension d i
114
          (aux typ') q
115
      | (d, LInt r) :: q ->
116
        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
117
        let typ' = Types.array_element_type typ in
118
        let szl = Utils.enumerate (Dimension.size_const_dimension d) in
119
        fprintf fmt "@[<v 2>{@,%a@]@,}"
120
          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
121
      | _ -> assert false
122
    in
123
    begin
124
      reset_loop_counter ();
125
      (*reset_addr_counter ();*)
126
      aux var_type fmt reordered_loop_vars;
127
      (*eprintf "end pp_assign@.";*)
128
    end
129

  
130
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
131
    let name, static =
84
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
85
    let name, is_arrow, static =
132 86
      match inst with
133 87
      | Some inst ->
134 88
        let node, static = try List.assoc inst m.minstances with Not_found ->
......
136 90
            fn_name m.mname.node_id self inst;
137 91
          raise Not_found
138 92
        in
139
        node_name node, static
93
        node_name node, Arrow.td_is_arrow node, static
140 94
      | None ->
141
        m.mname.node_id, []
95
        m.mname.node_id, false, []
142 96
    in
143
    fprintf fmt "%a(%a%s%a);"
144
      pp_machine_name name
97
    let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
98
    fprintf fmt "%a(%a%s%a)%a;"
99
      (if is_arrow_reset then
100
         (fun fmt -> fprintf fmt "%s_reset")
101
       else
102
         pp_machine_name) name
145 103
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
146 104
      self
147 105
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
106
      (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
107
      inst
148 108

  
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
109
  let pp_machine_set_reset m self mem fmt inst =
110
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
111
      self mem
151 112

  
152
  let pp_machine_clear_reset m self fmt =
153
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt self
113
  let pp_machine_clear_reset m self mem fmt =
114
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
115
      self mem
154 116

  
155
  let pp_machine_init m self fmt inst =
156
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
117
  let pp_machine_init m self mem fmt inst =
118
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
157 119

  
158
  let pp_machine_clear m self fmt inst =
159
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
120
  let pp_machine_clear m self mem fmt inst =
121
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
160 122

  
161
  let pp_call m self pp_read pp_write fmt i inputs outputs =
123
  let pp_call m self mem pp_read pp_write fmt i inputs outputs =
162 124
    try (* stateful node instance *)
163 125
      let n, _ = List.assoc i m.minstances in
164
      fprintf fmt "%a(%a%a%s->%s);"
126
      fprintf fmt "%a(%a%a%s->%s)%a;"
165 127
        pp_machine_step_name (node_name n)
166 128
        (pp_comma_list ~pp_eol:pp_print_comma
167 129
           (pp_c_val m self pp_read)) inputs
......
169 131
           pp_write) outputs
170 132
        self
171 133
        i
134
        (Mod.pp_ghost_parameter mem) (Some i)
172 135
    with Not_found -> (* stateless node instance *)
173 136
      let n, _ = List.assoc i m.mcalls in
174 137
      fprintf fmt "%a(%a%a);"
......
177 140
           (pp_c_val m self pp_read)) inputs
178 141
        (pp_comma_list pp_write) outputs
179 142

  
180
  let pp_basic_instance_call m self =
181
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
143
  let pp_basic_instance_call m self mem =
144
    pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
182 145

  
183
  let pp_arrow_call m self fmt i outputs =
146
  let pp_arrow_call m self mem fmt i outputs =
184 147
    match outputs with
185 148
    | [x] ->
186
      fprintf fmt "%a = %a(%s->%s);"
149
      fprintf fmt "%a = %a(%s->%s)%a;"
187 150
        (pp_c_var_read m) x
188 151
        pp_machine_step_name Arrow.arrow_id
189 152
        self
190 153
        i
154
        (Mod.pp_ghost_parameter mem) (Some i)
191 155
    | _ -> assert false
192 156

  
193
  let pp_instance_call m self fmt i inputs outputs =
157
  let pp_instance_call m self mem fmt i inputs outputs =
194 158
    let pp_offset pp_var indices fmt var =
195 159
      fprintf fmt "%a%a"
196 160
        pp_var var
......
208 172
      else
209 173
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
210 174
        let pp_write = pp_offset (pp_c_var_write m) indices in
211
        pp_call m self pp_read pp_write fmt i inputs outputs
175
        pp_call m self mem pp_read pp_write fmt i inputs outputs
212 176
    in
213 177
    reset_loop_counter ();
214 178
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
215 179

  
216
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
217
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
218
      (pp_c_val m self (pp_c_var_read m)) c
219
      (pp_print_list ~pp_prologue:pp_print_cut
220
         (pp_machine_instr dependencies m self)) tl
221
      (pp_print_list ~pp_prologue:pp_print_cut
222
         (pp_machine_instr dependencies m self)) el
223

  
224
  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
225
    match get_instr_desc instr with
226
    | MNoReset _ -> ()
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
232
    | MLocalAssign (i,v) ->
233
      pp_assign
234
        m self (pp_c_var_read m) fmt
235
        i.var_type (mk_val (Var i) i.var_type) v
236
    | MStateAssign (i,v) ->
237
      pp_assign
238
        m self (pp_c_var_read m) fmt
239
        i.var_type (mk_val (Var i) i.var_type) v
240
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
241
      pp_machine_instr dependencies m self fmt
242
        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
243
    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
244
      pp_instance_call m self fmt i vl il
245
    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
246
      fprintf fmt "%a = %s%a;"
247
        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
248
        i
249
        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
250
    | MStep (il, i, vl) ->
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
256
    | MBranch (_, []) ->
257
      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
258
        (pp_instr m) instr;
259
      assert false
260
    | MBranch (g, hl) ->
261
      if let t = fst (List.hd hl) in t = tag_true || t = tag_false
262
      then (* boolean case, needs special treatment in C because truth value is not unique *)
263
        (* may disappear if we optimize code by replacing last branch test with default *)
264
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
265
        let el = try List.assoc tag_false hl with Not_found -> [] in
266
        pp_conditional dependencies m self fmt g tl el
267
      else (* enum type case *)
268
        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
269
        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
270
          (pp_c_val m self (pp_c_var_read m)) g
271
          (pp_print_list ~pp_open_box:pp_open_vbox0
272
             (pp_machine_branch dependencies m self)) hl
273
    | MSpec s ->
274
      fprintf fmt "@[/*@@ %s */@]@ " s
275
    | MComment s  ->
276
      fprintf fmt "/*%s*/@ " s
277

  
278
  and pp_machine_branch dependencies m self fmt (t, h) =
180
  let rec pp_conditional dependencies m self mem fmt c tl el =
181
    let pp_machine_instrs =
182
      pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
183
        (pp_machine_instr dependencies m self mem) in
184
    let pp_cond = pp_c_val m self (pp_c_var_read m) in
185
    match tl, el with
186
    | [], _ :: _ ->
187
      fprintf fmt "@[<v 2>if (!%a) {%a@]@,}"
188
        pp_cond c
189
        pp_machine_instrs el
190
    | _, [] ->
191
      fprintf fmt "@[<v 2>if (%a) {%a@]@,}"
192
        pp_cond c
193
        pp_machine_instrs tl
194
    | _, _ ->
195
      fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
196
        pp_cond c
197
        pp_machine_instrs tl
198
        pp_machine_instrs el
199

  
200
  and pp_machine_instr dependencies m self mem fmt instr =
201
    let pp_instr fmt instr = match get_instr_desc instr with
202
      | MNoReset _ -> ()
203
      | MSetReset inst ->
204
        pp_machine_set_reset m self mem fmt inst
205
      | MClearReset ->
206
        fprintf fmt "%t@,%a"
207
          (pp_machine_clear_reset m self mem) pp_label reset_label
208
      | MResetAssign b ->
209
        pp_reset_assign self fmt b
210
      | MLocalAssign (i, v) ->
211
        pp_assign m self (pp_c_var_read m) fmt (i, v)
212
      | MStateAssign (i, v) ->
213
        pp_assign m self (pp_c_var_read m) fmt (i, v)
214
      | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
215
        pp_machine_instr dependencies m self mem fmt
216
          (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
217
      | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
218
        pp_instance_call m self mem fmt i vl il
219
      | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
220
        fprintf fmt "%a = %s%a;"
221
          (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
222
          i
223
          (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
224
      | MStep (il, i, vl) ->
225
        let td, _ = List.assoc i m.minstances in
226
        if Arrow.td_is_arrow td then
227
          pp_arrow_call m self mem fmt i il
228
        else
229
          pp_basic_instance_call m self mem fmt i vl il
230
      | MBranch (_, []) ->
231
        eprintf "internal error: C_backend_src.pp_machine_instr %a@."
232
          (pp_instr m) instr;
233
        assert false
234
      | MBranch (g, hl) ->
235
        if let t = fst (List.hd hl) in t = tag_true || t = tag_false
236
        then (* boolean case, needs special treatment in C because truth value is not unique *)
237
          (* may disappear if we optimize code by replacing last branch test with default *)
238
          let tl = try List.assoc tag_true  hl with Not_found -> [] in
239
          let el = try List.assoc tag_false hl with Not_found -> [] in
240
          let no_noreset = List.filter (fun i -> match i.instr_desc with
241
              | MNoReset _ -> false
242
              | _ -> true)
243
          in
244
          pp_conditional dependencies m self mem fmt g
245
            (no_noreset tl) (no_noreset el)
246
        else (* enum type case *)
247
          (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
248
          fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
249
            (pp_c_val m self (pp_c_var_read m)) g
250
            (pp_print_list ~pp_open_box:pp_open_vbox0
251
               (pp_machine_branch dependencies m self mem)) hl
252
      | MSpec s ->
253
        fprintf fmt "@[/*@@ %s */@]@ " s
254
      | MComment s  ->
255
        fprintf fmt "/*%s*/@ " s
256
    in
257
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
258

  
259
  and pp_machine_branch dependencies m self mem fmt (t, h) =
279 260
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
280 261
      pp_c_tag t
281 262
      (pp_print_list ~pp_open_box:pp_open_vbox0
282
         (pp_machine_instr dependencies m self)) h
263
         (pp_machine_instr dependencies m self mem)) h
283 264

  
284
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
285
    pp_machine_instr dependencies m self fmt instr
286

  
287
  let pp_machine_step_instr dependencies m self fmt _i instr =
288
    fprintf fmt "%a%a"
289
      (pp_machine_instr dependencies m self) instr
290
      (Mod.pp_step_instr_spec m self) instr
265
  (* let pp_machine_nospec_instr dependencies m self fmt instr =
266
   *   pp_machine_instr dependencies m self fmt instr
267
   *
268
   * let pp_machine_step_instr dependencies m self mem fmt instr =
269
   *   fprintf fmt "%a%a"
270
   *     (pp_machine_instr dependencies m self) instr
271
   *     (Mod.pp_step_instr_spec m self mem) instr *)
291 272

  
292 273
  (********************************************************************************************)
293 274
  (*                         C file Printing functions                                        *)
......
414 395
      ?(mpfr_locals=[])
415 396
      ?(pp_check=pp_print_nothing) ?(checks=[])
416 397
      ?(pp_extra=pp_print_nothing)
417
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
398
      ?(pp_instr=fun fmt _ -> pp_print_nothing fmt ()) ?(instrs=[])
418 399
      fmt =
419 400
    fprintf fmt
420 401
      "%a@[<v 2>%a {@,\
......
444 425
      (* check assertions *)
445 426
      (pp_print_list pp_check) checks
446 427
      (* instrs *)
447
      (pp_print_list_i
428
      (pp_print_list
448 429
         ~pp_open_box:pp_open_vbox0
449 430
         ~pp_epilogue:pp_print_cut
450 431
         pp_instr) instrs
......
478 459
        ~mpfr_locals:m.mstep.step_locals
479 460
        ~pp_check:(pp_c_check m self)
480 461
        ~checks:m.mstep.step_checks
481
        ~pp_instr:(pp_machine_step_instr dependencies m self)
462
        ~pp_instr:(pp_machine_instr dependencies m self self)
482 463
        ~instrs:m.mstep.step_instrs
483 464
        fmt
484 465
    else
......
500 481
        ~mpfr_locals:m.mstep.step_locals
501 482
        ~pp_check:(pp_c_check m self)
502 483
        ~checks:m.mstep.step_checks
503
        ~pp_instr:(pp_machine_step_instr dependencies m self)
484
        ~pp_instr:(pp_machine_instr dependencies m self self)
504 485
        ~instrs:m.mstep.step_instrs
505 486
        fmt
506 487

  
507
  let print_clear_reset_code machines dependencies self mem fmt m =
488
  let print_clear_reset_code dependencies self mem fmt m =
508 489
    pp_print_function
509
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
490
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
510 491
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
511 492
      ~prototype:(m.mname.node_id, m.mstatic)
512 493
      ~pp_local:(pp_c_decl_local_var m)
513 494
      ~base_locals:(const_locals m)
514
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
515
      ~instrs:m.minit
495
      ~pp_instr:(pp_machine_instr dependencies m self mem)
496
      ~instrs:[mk_branch
497
                 (mk_val ResetFlag Type_predef.type_bool)
498
                 ["true", mkinstr (MResetAssign false) :: m.minit]]
516 499
      fmt
517 500

  
518
  let print_set_reset_code self mem fmt m =
501
  let print_set_reset_code dependencies self mem fmt m =
519 502
    pp_print_function
520 503
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
521 504
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
522 505
      ~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)
506
      ~pp_instr:(pp_machine_instr dependencies m self mem)
507
      ~instrs:[mkinstr (MResetAssign true)]
525 508
      fmt
526 509

  
527 510
  let print_init_code self fmt m =
......
541 524
          pp_print_list
542 525
            ~pp_open_box:pp_open_vbox0
543 526
            ~pp_epilogue:pp_print_cut
544
            (pp_machine_init m self)
527
            (pp_machine_init m self self)
545 528
            fmt minit)
546 529
      fmt
547 530

  
......
561 544
          pp_print_list
562 545
            ~pp_open_box:pp_open_vbox0
563 546
            ~pp_epilogue:pp_print_cut
564
            (pp_machine_clear m self)
547
            (pp_machine_clear m self self)
565 548
            fmt minit)
566 549
      fmt
567 550

  
......
582 565
        ~mpfr_locals:m.mstep.step_locals
583 566
        ~pp_check:(pp_c_check m self)
584 567
        ~checks:m.mstep.step_checks
585
        ~pp_instr:(pp_machine_step_instr dependencies m self)
568
        ~pp_instr:(pp_machine_instr dependencies m self mem)
586 569
        ~instrs:m.mstep.step_instrs
587 570
        fmt
588 571
    else
......
605 588
        ~mpfr_locals:m.mstep.step_locals
606 589
        ~pp_check:(pp_c_check m self)
607 590
        ~checks:m.mstep.step_checks
608
        ~pp_instr:(pp_machine_step_instr dependencies m self)
591
        ~pp_instr:(pp_machine_instr dependencies m self mem)
609 592
        ~instrs:m.mstep.step_instrs
610 593
        fmt
611 594

  
......
754 737
      fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
755 738
        print_alloc_function m
756 739
        (* Reset functions *)
757
        (print_clear_reset_code machines dependencies self mem) m
758
        (print_set_reset_code self mem) m
740
        (print_clear_reset_code dependencies self mem) m
741
        (print_set_reset_code dependencies self mem) m
759 742
        (* Step function *)
760 743
        (print_step_code machines dependencies self mem) m
761 744
        (print_mpfr_code self) m

Also available in: Unified diff