Project

General

Profile

« Previous | Next » 

Revision 4b596770

Added by LĂ©lio Brun 10 months ago

first draft: to be tested with frama-c

View differences:

src/backends/C/c_backend_common.ml
13 13
open Lustre_types
14 14
open Corelang
15 15
open Machine_code_types
16
(*open Machine_code_common*)
16
open Machine_code_common
17 17
module Mpfr = Lustrec_mpfr
18 18

  
19 19
let pp_print_version fmt () =
......
447 447
  | None -> false
448 448
  | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
449 449

  
450
(* Computes the depth to which multi-dimension array assignments should be expanded.
451
   It equals the maximum number of nested static array constructions accessible from root [v].
452
*)
453
let rec expansion_depth v =
454
  match v.value_desc with
455
  | Cst cst -> expansion_depth_cst cst
456
  | Var _ -> 0
457
  | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
458
  | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
459
  | Access (v, _) -> max 0 (expansion_depth v - 1)
460
  | Power _  -> 0 (*1 + expansion_depth v*)
461
and expansion_depth_cst c =
462
  match c with
463
  | Const_array cl ->
464
    1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
465
  | _ -> 0
466

  
467
type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
468
(*
469
let rec value_offsets v offsets =
470
 match v, offsets with
471
 | _                        , []          -> v
472
 | Power (v, n)             , _ :: q      -> value_offsets v q
473
 | Array vl                 , LInt r :: q -> value_offsets (List.nth vl !r) q
474
 | Cst (Const_array cl)     , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
475
 | Fun (f, vl)              , _           -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
476
 | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
477
 | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q
478
*)
479
(* Computes the list of nested loop variables together with their dimension bounds.
480
   - LInt r stands for loop expansion (no loop variable, but int loop index)
481
   - LVar v stands for loop variable v
482
*)
483
let rec mk_loop_variables m ty depth =
484
  match (Types.repr ty).Types.tdesc, depth with
485
  | Types.Tarray (d, ty'), 0 ->
486
    let v = mk_loop_var m () in
487
    (d, LVar v) :: mk_loop_variables m ty' 0
488
  | Types.Tarray (d, ty'), _ ->
489
    let r = ref (-1) in
490
    (d, LInt r) :: mk_loop_variables m ty' (depth - 1)
491
  | _, 0 -> []
492
  | _ -> assert false
493

  
494
let reorder_loop_variables loop_vars =
495
  let (int_loops, var_loops) =
496
    List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
497
  in
498
  var_loops @ int_loops
499

  
500
(* Prints a one loop variable suffix for arrays *)
501
let pp_loop_var pp_val fmt lv =
502
  match snd lv with
503
  | LVar v -> fprintf fmt "[%s]" v
504
  | LInt r -> fprintf fmt "[%d]" !r
505
  | LAcc i -> fprintf fmt "[%a]" pp_val i
506

  
507
(* Prints a suffix of loop variables for arrays *)
508
let pp_suffix pp_val =
509
  pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
510

  
511
let rec is_const_index v =
512
  match v.value_desc with
513
  | Cst (Const_int _) -> true
514
  | Fun (_, vl)       -> List.for_all is_const_index vl
515
  | _                 -> false
516

  
517
(* Prints a value expression [v], with internal function calls only.
518
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
519
   but an offset suffix may be added for array variables
520
*)
521
(* Prints a constant value before a suffix (needs casting) *)
522
let rec pp_c_const_suffix var_type fmt c =
523
  match c with
524
  | Const_int i ->
525
    pp_print_int fmt i
526
  | Const_real r ->
527
    Real.pp fmt r
528
  | Const_tag t ->
529
    pp_c_tag fmt t
530
  | Const_array ca ->
531
    let var_type = Types.array_element_type var_type in
532
    fprintf fmt "(%a[])%a"
533
      (pp_c_type "") var_type
534
      (pp_print_braced (pp_c_const_suffix var_type)) ca
535
  | Const_struct fl ->
536
    pp_print_braced
537
      (fun fmt (f, c) ->
538
         (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)
539
      fmt fl
540
  | Const_string _
541
  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
542

  
543
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
544
let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt value =
545
  (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
546
  let pp_suffix = pp_suffix (pp_value_suffix ~indirect m self var_type [] pp_var) in
547
  match loop_vars, value.value_desc with
548
  | (x, LAcc i) :: q, _ when is_const_index i ->
549
    let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
550
    pp_value_suffix ~indirect m self var_type ((x, LInt r)::q) pp_var fmt value
551
  | (_, LInt r) :: q, Cst (Const_array cl) ->
552
    let var_type = Types.array_element_type var_type in
553
    pp_value_suffix ~indirect m self var_type q pp_var fmt
554
      (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
555
  | (_, LInt r) :: q, Array vl ->
556
    let var_type = Types.array_element_type var_type in
557
    pp_value_suffix ~indirect m self var_type q pp_var fmt (List.nth vl !r)
558
  | loop_var :: q, Array vl      ->
559
    let var_type = Types.array_element_type var_type in
560
    fprintf fmt "(%a[])%a%a"
561
      (pp_c_type "") var_type
562
      (pp_print_braced (pp_value_suffix ~indirect m self var_type q pp_var)) vl
563
      pp_suffix [loop_var]
564
  | [], Array vl      ->
565
    let var_type = Types.array_element_type var_type in
566
    fprintf fmt "(%a[])%a"
567
      (pp_c_type "") var_type
568
      (pp_print_braced (pp_value_suffix ~indirect m self var_type [] pp_var)) vl
569
  | _ :: q, Power (v, _)  ->
570
    pp_value_suffix ~indirect m self var_type q pp_var fmt v
571
  | _, Fun (n, vl)   ->
572
    pp_basic_lib_fun (Types.is_int_type value.value_type) n
573
      (pp_value_suffix ~indirect m self var_type loop_vars pp_var) fmt vl
574
  | _, Access (v, i) ->
575
    let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
576
    pp_value_suffix m self var_type
577
      ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
578
  | _, Var v ->
579
    if is_memory m v then
580
      (* array memory vars are represented by an indirection to a local var with the right type,
581
         in order to avoid casting everywhere. *)
582
      if Types.is_array_type v.var_type
583
      then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
584
      else fprintf fmt "%s%s_reg.%a%a"
585
          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
586
    else
587
      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
588
  | _, Cst cst ->
589
    pp_c_const_suffix var_type fmt cst
590
  | _, _ ->
591
    eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
592
      Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
593
    assert false
594

  
450 595
(********************************************************************************************)
451 596
(*                       Struct Printing functions                                          *)
452 597
(********************************************************************************************)
src/backends/C/c_backend_spec.ml
139 139
  Format.fprintf fmt "";
140 140
  ()
141 141

  
142
module VarDecl = struct
143
  type t = var_decl
144
  let compare v1 v2 = compare v1.var_id v2.var_id
145
end
146
module VDSet = Set.Make(VarDecl)
147

  
148
module Live = Map.Make(Int)
149

  
142 150
let pp_spec pp fmt =
143 151
  fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
144 152

  
......
197 205
    pp_l l
198 206
    pp_r r
199 207

  
208
let pp_exists pp_l pp_r fmt (l, r) =
209
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
210
    pp_l l
211
    pp_r r
212

  
200 213
let pp_valid =
201 214
  pp_print_parenthesized
202 215
    ~pp_nil:pp_true
......
208 221
    pp_r r
209 222

  
210 223
let pp_implies pp_l pp_r fmt (l, r) =
211
  fprintf fmt "%a ==>@ %a"
224
  fprintf fmt "@[<v>%a ==>@ %a@]"
212 225
    pp_l l
213 226
    pp_r r
214 227

  
215 228
let pp_and pp_l pp_r fmt (l, r) =
216
  fprintf fmt "%a @ && %a"
229
  fprintf fmt "@[<v>%a @ && %a@]"
217 230
    pp_l l
218 231
    pp_r r
219 232

  
......
230 243
    pp_t t
231 244
    pp_f f
232 245

  
246
let pp_paren pp fmt v =
247
  fprintf fmt "(%a)" pp v
248

  
233 249
let pp_machine_decl fmt (id, mem_type, var) =
234 250
  fprintf fmt "struct %s_%s %s" id mem_type var
235 251

  
......
250 266
let pp_var_decl fmt v =
251 267
  pp_print_string fmt v.var_id
252 268

  
269
let pp_locals m fmt vs =
270
  pp_print_list
271
    ~pp_open_box:pp_open_hbox
272
    ~pp_sep:pp_print_comma
273
    (pp_c_decl_local_var m) fmt vs
274

  
253 275
let pp_ptr_decl fmt v =
254 276
  fprintf fmt "*%s" v.var_id
255 277

  
278
let rec assigned s instr =
279
  let open VDSet in
280
  match instr.instr_desc with
281
  | MLocalAssign (x, _) ->
282
    add x s
283
  | MStep (xs, _, _) ->
284
    union s (of_list xs)
285
  | MBranch (_, brs) ->
286
    List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)
287
  | _ -> s
288

  
289
let rec occur_val s v =
290
  let open VDSet in
291
  match v.value_desc with
292
  | Var x ->
293
    add x s
294
  | Fun (_, vs)
295
  | Array vs ->
296
    List.fold_left occur_val s vs
297
  | Access (v1, v2)
298
  | Power (v1, v2) ->
299
    occur_val (occur_val s v1) v2
300
  | _ -> s
301

  
302
let rec occur s instr =
303
  let open VDSet in
304
  match instr.instr_desc with
305
  | MLocalAssign (_, v)
306
  | MStateAssign (_, v) ->
307
    occur_val s v
308
  | MStep (_, _, vs) ->
309
    List.fold_left occur_val s vs
310
  | MBranch (v, brs) ->
311
    List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)
312
            (occur_val s v) brs)
313
  | _ -> s
314

  
315
let live = Hashtbl.create 32
316

  
317
let set_live_of m =
318
  let open VDSet in
319
  let locals = of_list m.mstep.step_locals in
320
  let outputs = of_list m.mstep.step_outputs in
321
  let vars = union locals outputs in
322
  let no_occur_after i =
323
    let occ, _ = List.fold_left (fun (s, j) instr ->
324
        if j <= i then (s, j+1) else (occur s instr, j+1))
325
        (empty, 0) m.mstep.step_instrs in
326
    diff locals occ
327
  in
328
  let l, _, _ = List.fold_left (fun (l, asg, i) instr ->
329
      let asg = inter (assigned asg instr) vars in
330
      Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)
331
      (Live.empty, empty, 0) m.mstep.step_instrs in
332
  Hashtbl.add live m.mname.node_id (Live.add 0 empty l)
333

  
334
let live_i m i =
335
  Live.find i (Hashtbl.find live m.mname.node_id)
336

  
256 337
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
257
    (name, inputs, outputs, mem_in, mem_out) =
258
  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a@])"
338
    (name, inputs, locals, outputs, mem_in, mem_out) =
339
  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a%a@])"
259 340
    name
260 341
    (pp_print_option pp_print_int) i
261 342
    pp_mem_in mem_in
......
263 344
       ~pp_epilogue:pp_print_comma
264 345
       ~pp_sep:pp_print_comma
265 346
       pp_input) inputs
347
    (pp_print_option
348
       (fun fmt _ ->
349
          pp_print_list
350
            ~pp_epilogue:pp_print_comma
351
            ~pp_sep:pp_print_comma
352
            pp_input fmt locals))
353
    i
266 354
    pp_mem_out mem_out
267 355
    (pp_print_list
268 356
       ~pp_prologue:pp_print_comma
269 357
       ~pp_sep:pp_print_comma
270 358
       pp_output) outputs
271 359

  
272
let pp_mem_trans ?i pp_mem_in pp_mem_out fmt (m, mem_in, mem_out) =
273
  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_var_decl pp_ptr_decl fmt
274
    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, mem_in, mem_out)
275

  
276
let pp_mem_trans' ?i fmt = pp_mem_trans ?i pp_print_string pp_print_string fmt
360
let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt
361
    (m, mem_in, mem_out) =
362
  let locals, outputs = match i with
363
    | Some 0 ->
364
      [], []
365
    | Some i when i < List.length m.mstep.step_instrs ->
366
      let li = live_i m i in
367
      VDSet.(inter (of_list m.mstep.step_locals) li |> elements,
368
             inter (of_list m.mstep.step_outputs) li |> elements)
369
    | Some _ ->
370
      [], m.mstep.step_outputs
371
    | _ ->
372
      m.mstep.step_locals, m.mstep.step_outputs
373
  in
374
  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
375
    (m.mname.node_id,
376
     m.mstep.step_inputs,
377
     locals,
378
     outputs,
379
     mem_in,
380
     mem_out)
381

  
382
let pp_mem_trans' ?i fmt =
383
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
277 384

  
278 385
let pp_nothing fmt () =
279 386
  pp_print_string fmt "\\nothing"
......
310 417
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
311 418
     v)
312 419

  
313
let print_machine_ghost_simulation dependencies m fmt i instr =
420
let print_ghost_simulation dependencies m fmt (i, instr) =
314 421
  let name = m.mname.node_id in
315 422
  let self = mk_self m in
316 423
  let mem = mk_mem m in
317 424
  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
318 425
  let pred pp v = pp_and prev_ghost pp fmt ((), v) in
426
  let rec aux fmt instr =
427
    match instr.instr_desc with
428
    | MStateAssign (m, _) ->
429
      pp_equal
430
        (pp_access (pp_access pp_var_decl))
431
        (pp_indirect (pp_access pp_var_decl))
432
        fmt
433
        ((mem, ("_reg", m)), (self, ("_reg", m)))
434
    | MStep ([i0], i, vl)
435
      when Basic_library.is_value_internal_fun
436
          (mk_val (Fun (i, vl)) i0.var_type)  ->
437
      pp_true fmt ()
438
    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
439
      pp_true fmt ()
440
    | MStep ([_], i, _) when has_c_prototype i dependencies ->
441
      pp_true fmt ()
442
    | MStep (_, i, _)
443
    | MReset i ->
444
      begin try
445
          let n, _ = List.assoc i m.minstances in
446
          pp_mem_ghost pp_access' pp_indirect' fmt
447
            (node_name n, (mem, i), (self, i))
448
        with Not_found -> pp_true fmt ()
449
      end
450
    | MBranch (_, brs) ->
451
      (* TODO: handle branches *)
452
      pp_and_l aux fmt List.(flatten (map snd brs))
453
    | _ -> pp_true fmt ()
454
  in
455
  pred aux instr
456

  
457
let print_machine_ghost_simulation dependencies m fmt i instr =
319 458
  print_machine_ghost_simulation_aux m
320
    (fun fmt -> function
321
       | MStateAssign (m, _) ->
322
         pred
323
           (pp_equal
324
              (pp_access (pp_access pp_var_decl))
325
              (pp_indirect (pp_access pp_var_decl)))
326
           ((mem, ("_reg", m)),
327
            (self, ("_reg", m)))
328
       | MStep ([i0], i, vl)
329
         when Basic_library.is_value_internal_fun
330
             (mk_val (Fun (i, vl)) i0.var_type)  ->
331
         prev_ghost fmt ()
332
       | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
333
         prev_ghost fmt ()
334
       | MStep ([_], i, _) when has_c_prototype i dependencies ->
335
         prev_ghost fmt ()
336
       | MStep (_, i, _)
337
       | MReset i ->
338
         begin try
339
             let n, _ = List.assoc i m.minstances in
340
             pred
341
               (pp_mem_ghost pp_access' pp_indirect')
342
               (node_name n, (mem, i), (self, i))
343
           with Not_found -> prev_ghost fmt ()
344
         end
345
       | _ -> prev_ghost fmt ())
346
    ~i:(i+1) fmt instr.instr_desc
459
    (print_ghost_simulation dependencies m)
460
    ~i:(i+1)
461
    fmt (i, instr)
347 462

  
348 463
let print_machine_ghost_struct fmt m =
349 464
  pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
......
364 479
      (print_machine_ghost_simulation_aux m
365 480
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
366 481

  
367
let print_machine_core_annotations dependencies fmt m =
368
  if not (fst (Machine_code_common.get_stateless_status m)) then
369
    let name = m.mname.node_id in
370
    let self = mk_self m in
371
    let mem = mk_mem m in
372
    fprintf fmt "%a@,%a@,%a%a"
373
      print_machine_ghost_struct m
374
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
482
let pp_basic_assign_spec pp_var fmt typ var_name value =
483
  if Types.is_real_type typ && !Options.mpfr
484
  then
485
    assert false
486
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
487
  else
488
    pp_equal pp_var pp_var fmt (var_name, value)
489

  
490
let pp_assign_spec m self pp_var fmt (var_type, var_name, value) =
491
  let depth = expansion_depth value in
492
  let loop_vars = mk_loop_variables m var_type depth in
493
  let reordered_loop_vars = reorder_loop_variables loop_vars in
494
  let rec aux typ fmt vars =
495
    match vars with
496
    | [] ->
497
      pp_basic_assign_spec
498
        (pp_value_suffix ~indirect:false m self var_type loop_vars pp_var)
499
        fmt typ var_name value
500
    | (d, LVar i) :: q ->
501
      assert false
502
      (* let typ' = Types.array_element_type typ in
503
       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
504
       *   i i i pp_c_dimension d i
505
       *   (aux typ') q *)
506
    | (d, LInt r) :: q ->
507
      assert false
508
      (* let typ' = Types.array_element_type typ in
509
       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
510
       * fprintf fmt "@[<v 2>{@,%a@]@,}"
511
       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
512
    | _ -> assert false
513
  in
514
  begin
515
    reset_loop_counter ();
516
    aux var_type fmt reordered_loop_vars;
517
  end
518

  
519
let print_machine_trans_simulation_aux ?i m pp fmt v =
520
  let name = m.mname.node_id in
521
  let mem_in = mk_mem_in m in
522
  let mem_out = mk_mem_out m in
523
  pp_spec
524
    (pp_predicate
525
       (pp_mem_trans pp_machine_decl pp_machine_decl
526
          (pp_c_decl_local_var m) pp_c_decl_output_var ?i)
527
       pp)
528
    fmt
529
    ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
530
     v)
531

  
532
let print_trans_simulation machines dependencies m fmt (i, instr) =
533
  let mem_in = mk_mem_in m in
534
  let mem_out = mk_mem_out m in
535
  let d = VDSet.(diff (live_i m i) (live_i m (i+1))) in
536
  printf "%d : %a\n%d : %a\n\n"
537
    i
538
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
539
    (i+1)
540
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)));
541
  let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
542
  let pred pp v =
543
    let locals = VDSet.(inter (of_list m.mstep.step_locals) d |> elements) in
544
    if locals = []
545
    then pp_and prev_trans pp fmt ((), v)
546
    else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
547
  in
548
  let rec aux fmt instr = match instr.instr_desc with
549
    | MLocalAssign (x, v)
550
    | MStateAssign (x, v) ->
551
      pp_assign_spec m mem_in (pp_c_var_read m) fmt
552
        (x.var_type, mk_val (Var x) x.var_type, v)
553
    | MStep ([i0], i, vl)
554
      when Basic_library.is_value_internal_fun
555
          (mk_val (Fun (i, vl)) i0.var_type)  ->
556
      pp_true fmt ()
557
    | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
558
      pp_true fmt ()
559
    | MStep ([_], i, _) when has_c_prototype i dependencies ->
560
      pp_true fmt ()
561
    | MStep (xs, f, ys) ->
562
      begin try
563
          let n, _ = List.assoc f m.minstances in
564
            pp_mem_trans_aux
565
              pp_access' pp_access'
566
              (pp_c_val m mem_in (pp_c_var_read m))
567
              pp_var_decl
568
              fmt
569
              (node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
570
        with Not_found -> pp_true fmt ()
571
      end
572
    | MReset f ->
573
      begin try
574
          let n, _ = List.assoc f m.minstances in
575
          pp_mem_init' fmt (node_name n, mem_out)
576
        with Not_found -> pp_true fmt ()
577
      end
578
    | MBranch (v, brs) ->
579
      (* TODO: handle branches *)
580
      pp_and_l (fun fmt (l, instrs) ->
581
          pp_paren (pp_implies
582
                      (pp_equal
583
                         (pp_c_val m mem_in (pp_c_var_read m))
584
                         pp_print_string)
585
                      (pp_and_l aux))
586
            fmt
587
            ((v, l), instrs))
588
        fmt brs
589
    | _ -> pp_true fmt ()
590
  in
591
  pred aux instr
592

  
593
let print_machine_trans_simulation machines dependencies m fmt i instr =
594
  print_machine_trans_simulation_aux m
595
    (print_trans_simulation machines dependencies m)
596
    ~i:(i+1)
597
    fmt (i, instr)
598

  
599
let print_machine_core_annotations machines dependencies fmt m =
600
  if not (fst (Machine_code_common.get_stateless_status m)) then begin
601
    set_live_of m;
602
    let i = List.length m.mstep.step_instrs in
603
    let mem_in = mk_mem_in m in
604
    let mem_out = mk_mem_out m in
605
    let last_trans fmt () =
606
      let locals = VDSet.(inter
607
                            (of_list m.mstep.step_locals)
608
                            (live_i m i)
609
                          |> elements) in
610
      if locals = []
611
      then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
612
      else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
613
          (locals, (m, mem_in, mem_out))
614
    in
615
    fprintf fmt "%a@,%a%a"
616
      (print_machine_trans_simulation_aux m pp_true ~i:0) ()
375 617
      (pp_print_list_i
376 618
        ~pp_epilogue:pp_print_cut
377 619
        ~pp_open_box:pp_open_vbox0
378
        (print_machine_ghost_simulation dependencies m))
620
        (print_machine_trans_simulation machines dependencies m))
379 621
      m.mstep.step_instrs
380
      (print_machine_ghost_simulation_aux m
381
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
622
      (print_machine_trans_simulation_aux m last_trans) ()
623
  end
382 624

  
383 625
let pp_at pp_p fmt (p, l) =
384 626
  fprintf fmt "\\at(%a, %s)" pp_p p l
......
388 630
let pp_at_pre pp_p fmt p =
389 631
  pp_at pp_p fmt (p, label_pre)
390 632

  
391
module VarDecl = struct
392
  type t = var_decl
393
  let compare v1 v2 = compare v1.var_id v2.var_id
394
end
395
module VDSet = Set.Make(VarDecl)
396

  
397 633
let pp_arrow_spec fmt () =
398 634
  let name = "_arrow" in
399 635
  let mem_in = "mem_in" in
......
418 654
       (pp_predicate
419 655
          (pp_mem_trans_aux
420 656
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
421
          (pp_and
422
             (pp_equal
423
                pp_print_string
424
                (pp_access pp_access'))
425
             (pp_ite
426
                (pp_access pp_access')
427
                (pp_equal
428
                   (pp_access pp_access')
429
                   pp_print_string)
430
                (pp_equal
431
                   (pp_access pp_access')
432
                   (pp_access pp_access'))))))
433
    ((name, [], ["_Bool out"], (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
434
     (("out", mem_in_first),
435
      (mem_in_first, (mem_out_first, "false"), (mem_out_first, mem_in_first))))
657
          (pp_ite
658
             (pp_access pp_access')
659
             (pp_paren
660
                (pp_and
661
                   (pp_equal
662
                      (pp_access pp_access')
663
                      pp_print_string)
664
                   (pp_equal pp_print_string pp_print_string)))
665
                (pp_paren
666
                   (pp_and
667
                      (pp_equal
668
                         (pp_access pp_access')
669
                         (pp_access pp_access'))
670
                      (pp_equal pp_print_string pp_print_string))))))
671
    ((name, ["int x"; "int y"], [], ["_Bool out"],
672
      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
673
     (* (("out", mem_in_first), *)
674
     (mem_in_first, ((mem_out_first, "false"), ("out", "x")),
675
      ((mem_out_first, mem_in_first), ("out", "y"))))
436 676
    (pp_spec_cut
437 677
       (pp_predicate
438 678
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
......
463 703
         ~pp_open_box:pp_open_vbox0
464 704
         ~pp_sep:pp_print_cutcut
465 705
         ~pp_prologue:(pp_print_endcut "/* ACSL core annotations */")
466
         (print_machine_core_annotations dependencies)
706
         (print_machine_core_annotations machines dependencies)
467 707
         ~pp_epilogue:pp_print_cutcut) machines
468 708

  
469 709
  let pp_reset_spec fmt self m =
......
544 784
               (pp_implies
545 785
                  (pp_at_pre pp_mem_ghost')
546 786
                  (pp_implies
547
                     (pp_mem_ghost' ~i:(i+1))
548
                     (pp_mem_trans' ~i:(i+1)))))))
787
                     (pp_mem_ghost' ~i)
788
                     (pp_mem_trans' ~i))))))
549 789
      ((),
550 790
       ((name, mem_in, self),
551 791
        ((name, mem_out, self),
src/backends/C/c_backend_src.ml
37 37
  (********************************************************************************************)
38 38

  
39 39

  
40
  (* Computes the depth to which multi-dimension array assignments should be expanded.
41
     It equals the maximum number of nested static array constructions accessible from root [v].
42
  *)
43
  let rec expansion_depth v =
44
    match v.value_desc with
45
    | Cst cst -> expansion_depth_cst cst
46
    | Var _ -> 0
47
    | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
48
    | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
49
    | Access (v, _) -> max 0 (expansion_depth v - 1)
50
    | Power _  -> 0 (*1 + expansion_depth v*)
51
  and expansion_depth_cst c = 
52
    match c with
53
    | Const_array cl ->
54
      1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
55
    | _ -> 0
56

  
57 40
  let rec merge_static_loop_profiles lp1 lp2 =
58 41
    match lp1, lp2 with
59 42
    | []      , _        -> lp2
......
82 65
        cl []
83 66
    | _ -> [] 
84 67

  
85
  let rec is_const_index v =
86
    match v.value_desc with
87
    | Cst (Const_int _) -> true
88
    | Fun (_, vl)       -> List.for_all is_const_index vl
89
    | _                 -> false
90

  
91
  type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
92
(*
93
let rec value_offsets v offsets =
94
 match v, offsets with
95
 | _                        , []          -> v
96
 | Power (v, n)             , _ :: q      -> value_offsets v q
97
 | Array vl                 , LInt r :: q -> value_offsets (List.nth vl !r) q
98
 | Cst (Const_array cl)     , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
99
 | Fun (f, vl)              , _           -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
100
 | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
101
 | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q
102
*)
103
  (* Computes the list of nested loop variables together with their dimension bounds.
104
     - LInt r stands for loop expansion (no loop variable, but int loop index)
105
     - LVar v stands for loop variable v
106
  *)
107
  let rec mk_loop_variables m ty depth =
108
    match (Types.repr ty).Types.tdesc, depth with
109
    | Types.Tarray (d, ty'), 0 ->
110
      let v = mk_loop_var m () in
111
      (d, LVar v) :: mk_loop_variables m ty' 0
112
    | Types.Tarray (d, ty'), _ ->
113
      let r = ref (-1) in
114
      (d, LInt r) :: mk_loop_variables m ty' (depth - 1)
115
    | _, 0 -> []
116
    | _ -> assert false
117

  
118
  let reorder_loop_variables loop_vars =
119
    let (int_loops, var_loops) =
120
      List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
121
    in
122
    var_loops @ int_loops
123

  
124
  (* Prints a one loop variable suffix for arrays *)
125
  let pp_loop_var pp_val fmt lv =
126
    match snd lv with
127
    | LVar v -> fprintf fmt "[%s]" v
128
    | LInt r -> fprintf fmt "[%d]" !r
129
    | LAcc i -> fprintf fmt "[%a]" pp_val i
130

  
131
  (* Prints a suffix of loop variables for arrays *)
132
  let pp_suffix pp_val =
133
    pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
134

  
135
  (* Prints a value expression [v], with internal function calls only.
136
     [pp_var] is a printer for variables (typically [pp_c_var_read]),
137
     but an offset suffix may be added for array variables
138
  *)
139
  (* Prints a constant value before a suffix (needs casting) *)
140
  let rec pp_c_const_suffix var_type fmt c =
141
    match c with
142
    | Const_int i ->
143
      pp_print_int fmt i
144
    | Const_real r ->
145
      Real.pp fmt r
146
    | Const_tag t ->
147
      pp_c_tag fmt t
148
    | Const_array ca ->
149
      let var_type = Types.array_element_type var_type in
150
      fprintf fmt "(%a[])%a"
151
        (pp_c_type "") var_type
152
        (pp_print_braced (pp_c_const_suffix var_type)) ca
153
    | Const_struct fl ->
154
      pp_print_braced
155
        (fun fmt (f, c) ->
156
           (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)
157
        fmt fl
158
    | Const_string _
159
    | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
160

  
161
  (* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
162
  let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
163
    (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
164
    let pp_suffix = pp_suffix (pp_value_suffix m self var_type [] pp_var) in
165
    match loop_vars, value.value_desc with
166
    | (x, LAcc i) :: q, _ when is_const_index i ->
167
      let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
168
      pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
169
    | (_, LInt r) :: q, Cst (Const_array cl) ->
170
      let var_type = Types.array_element_type var_type in
171
      pp_value_suffix m self var_type q pp_var fmt
172
        (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
173
    | (_, LInt r) :: q, Array vl ->
174
      let var_type = Types.array_element_type var_type in
175
      pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
176
    | loop_var :: q, Array vl      ->
177
      let var_type = Types.array_element_type var_type in
178
      fprintf fmt "(%a[])%a%a"
179
        (pp_c_type "") var_type
180
        (pp_print_braced (pp_value_suffix m self var_type q pp_var)) vl
181
        pp_suffix [loop_var]
182
    | [], Array vl      ->
183
      let var_type = Types.array_element_type var_type in
184
      fprintf fmt "(%a[])%a"
185
        (pp_c_type "") var_type
186
        (pp_print_braced (pp_value_suffix m self var_type [] pp_var)) vl
187
    | _ :: q, Power (v, _)  ->
188
      pp_value_suffix m self var_type q pp_var fmt v
189
    | _, Fun (n, vl)   ->
190
      pp_basic_lib_fun (Types.is_int_type value.value_type) n
191
        (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
192
    | _, Access (v, i) ->
193
      let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
194
      pp_value_suffix m self var_type
195
        ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
196
    | _, Var v ->
197
      if is_memory m v then
198
        (* array memory vars are represented by an indirection to a local var with the right type,
199
           in order to avoid casting everywhere. *)
200
        if Types.is_array_type v.var_type
201
        then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
202
        else fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
203
      else
204
        fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
205
    | _, Cst cst ->
206
      pp_c_const_suffix var_type fmt cst
207
    | _, _ ->
208
      eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
209
        Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
210
      assert false
211 68

  
212 69
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
213 70
     which may yield constant arrays in expressions.
......
393 250
    pp_machine_instr dependencies m self fmt instr
394 251

  
395 252
  let pp_machine_step_instr dependencies m self fmt i instr =
396
    fprintf fmt "%a%a%a"
253
    fprintf fmt "%a@,%a%a"
397 254
      (if i = 0 then
398
         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr))
255
         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i, instr))
399 256
       else
400 257
         pp_print_nothing) ()
401 258
      (pp_machine_instr dependencies m self) instr
402
      (Mod.pp_step_instr_spec m self) (i, instr)
259
      (Mod.pp_step_instr_spec m self) (i+1, instr)
403 260

  
404 261
  (********************************************************************************************)
405 262
  (*                         C file Printing functions                                        *)

Also available in: Unified diff