Project

General

Profile

« Previous | Next » 

Revision c226a3ba

Added by LĂ©lio Brun over 2 years ago

start generating ACSL spec

View differences:

src/backends/C/c_backend_common.ml
40 40
let var_is name v =
41 41
  v.var_id = name
42 42

  
43
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
44
let mk_self m =
43
let mk_local n m =
45 44
  let used name =
46 45
    let open List in
47 46
    exists (var_is name) m.mstep.step_inputs
48 47
    || exists (var_is name) m.mstep.step_outputs
49 48
    || exists (var_is name) m.mstep.step_locals
50 49
    || exists (var_is name) m.mmemory in
51
  mk_new_name used "self"
50
  mk_new_name used n
51

  
52
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
53
let mk_self = mk_local "self"
54

  
55
let mk_mem = mk_local "mem"
56
let mk_mem_in = mk_local "mem_in"
57
let mk_mem_out = mk_local "mem_out"
52 58

  
53 59
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
54 60
let mk_instance m =
......
110 116
*)
111 117
let pp_global_init_name fmt id = fprintf fmt "%s_INIT" id
112 118
let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
113
let pp_machine_memtype_name fmt id = fprintf fmt "struct %s_mem" id
119
let pp_machine_memtype_name ?(ghost=false) fmt id =
120
  fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")
114 121
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
115 122
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
116 123
let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id
......
216 223
  | _ ->
217 224
     fprintf fmt "%s" (pp_c_basic_type_desc t)
218 225

  
219
let pp_c_type ?(var_opt=None) var_id fmt t =
226
let pp_c_type ?var_opt var_id fmt t =
220 227
  let rec aux t pp_suffix =
221 228
    if is_basic_c_type  t then
222 229
       fprintf fmt "%a %s%a"
......
352 359
let pp_c_decl_input_var fmt id =
353 360
  if !Options.ansi && Types.is_address_type id.var_type
354 361
  then
355
    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
362
    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt
356 363
      (Types.array_base_type id.var_type)
357 364
  else
358
    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
365
    pp_c_type ~var_opt:id id.var_id fmt id.var_type
359 366

  
360 367
(* Declaration of an output variable:
361 368
   - if its type is scalar, then pass its address
......
366 373
let pp_c_decl_output_var fmt id =
367 374
  if (not !Options.ansi) && Types.is_address_type id.var_type
368 375
  then
369
    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
376
    pp_c_type ~var_opt:id id.var_id fmt id.var_type
370 377
  else
371
    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
378
    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt
372 379
      (Types.array_base_type id.var_type)
373 380

  
374 381
(* Declaration of a local/mem variable:
......
380 387
  if id.var_dec_const
381 388
  then
382 389
    fprintf fmt "%a = %a"
383
      (pp_c_type ~var_opt:(Some id) id.var_id)
390
      (pp_c_type ~var_opt:id id.var_id)
384 391
      id.var_type
385 392
      (pp_c_val m "" (pp_c_var_read m))
386 393
      (Machine_code_common.get_const_assign m id)
387 394
  else
388 395
    fprintf fmt "%a"
389
      (pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
396
      (pp_c_type ~var_opt:id id.var_id) id.var_type
390 397

  
391 398
(* Declaration of a struct variable:
392 399
   - if it's an array/matrix/etc, we declare it as a pointer
......
399 406
  else
400 407
    pp_c_type id.var_id  fmt id.var_type
401 408

  
402
let pp_c_decl_instance_var fmt (name, (node, _)) =
403
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
409
let pp_c_decl_instance_var ?(ghost=false) fmt (name, (node, _)) =
410
  fprintf fmt "%a %s%s"
411
    (pp_machine_memtype_name ~ghost) (node_name node)
412
    (if ghost then "" else "*")
413
    name
404 414

  
405 415
(* let pp_c_checks self fmt m =
406 416
 *   pp_print_list
......
412 422
 *     fmt
413 423
 *     m.mstep.step_checks *)
414 424

  
425
let has_c_prototype funname dependencies =
426
  (* We select the last imported node with the name funname.
427
     The order of evaluation of dependencies should be
428
     compatible with overloading. (Not checked yet) *)
429
  let imported_node_opt =
430
    List.fold_left
431
      (fun res dep ->
432
         match res with
433
         | Some _ -> res
434
         | None ->
435
           let decls = dep.content in
436
           let matched = fun t -> match t.top_decl_desc with
437
             | ImportedNode nd -> nd.nodei_id = funname
438
             | _ -> false
439
           in
440
           if List.exists matched decls then
441
             match (List.find matched decls).top_decl_desc with
442
             | ImportedNode nd -> Some nd
443
             | _ -> assert false
444
           else
445
             None) None dependencies in
446
  match imported_node_opt with
447
  | None -> false
448
  | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
449

  
415 450
(********************************************************************************************)
416 451
(*                       Struct Printing functions                                          *)
417 452
(********************************************************************************************)
......
427 462
 *     pp_c_decl_struct_var
428 463
 *     fmt m.mmemory *)
429 464

  
430
let print_machine_struct fmt m =
465
let print_machine_struct ?(ghost=false) fmt m =
431 466
  if not (fst (Machine_code_common.get_stateless_status m)) then
432 467
    (* Define struct *)
433 468
    fprintf fmt "@[<v 2>%a {%a%a@]@,};"
434
      pp_machine_memtype_name m.mname.node_id
435
      (pp_print_list
436
         ~pp_open_box:pp_open_vbox0
437
         ~pp_prologue:(fun fmt () ->
438
             fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)
439
         ~pp_sep:pp_print_semicolon
440
         ~pp_eol:pp_print_semicolon'
441
         ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
442
         pp_c_decl_struct_var)
469
      (pp_machine_memtype_name ~ghost) m.mname.node_id
470
      (if ghost then
471
         (fun fmt -> function
472
            | [] -> pp_print_nothing fmt ()
473
            | _ -> fprintf fmt "@,%a _reg;"
474
                     pp_machine_regtype_name m.mname.node_id)
475
       else
476
         pp_print_list
477
           ~pp_open_box:pp_open_vbox0
478
           ~pp_prologue:(fun fmt () ->
479
               fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)
480
           ~pp_sep:pp_print_semicolon
481
           ~pp_eol:pp_print_semicolon'
482
           ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
483
           pp_c_decl_struct_var)
443 484
      m.mmemory
444 485
      (pp_print_list
486
         ~pp_open_box:pp_open_vbox0
445 487
         ~pp_prologue:pp_print_cut
446 488
         ~pp_sep:pp_print_semicolon
447 489
         ~pp_eol:pp_print_semicolon'
448
         pp_c_decl_instance_var)
490
         (pp_c_decl_instance_var ~ghost))
449 491
      m.minstances
450 492

  
451 493
(********************************************************************************************)
......
462 504

  
463 505
let print_alloc_prototype fmt (name, static) =
464 506
  fprintf fmt "%a * %a %a"
465
    pp_machine_memtype_name name
507
    (pp_machine_memtype_name ~ghost:false) name
466 508
    pp_machine_alloc_name name
467 509
    (pp_print_parenthesized pp_c_decl_input_var) static
468 510

  
469 511
let print_dealloc_prototype fmt name =
470 512
  fprintf fmt "void %a (%a * _alloc)"
471 513
    pp_machine_dealloc_name name
472
    pp_machine_memtype_name name
473
    
514
    (pp_machine_memtype_name ~ghost:false) name
515

  
474 516
let print_reset_prototype self fmt (name, static) =
475 517
  fprintf fmt "void %a (%a%a *%s)"
476 518
    pp_machine_reset_name name
477 519
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
478 520
       pp_c_decl_input_var) static
479
    pp_machine_memtype_name name
521
    (pp_machine_memtype_name ~ghost:false) name
480 522
    self
481 523

  
482 524
let print_init_prototype self fmt (name, static) =
......
484 526
    pp_machine_init_name name
485 527
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
486 528
       pp_c_decl_input_var) static
487
    pp_machine_memtype_name name
529
    (pp_machine_memtype_name ~ghost:false) name
488 530
    self
489 531

  
490 532
let print_clear_prototype self fmt (name, static) =
......
492 534
    pp_machine_clear_name name
493 535
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
494 536
       pp_c_decl_input_var) static
495
    pp_machine_memtype_name name
537
    (pp_machine_memtype_name ~ghost:false) name
496 538
    self
497 539

  
498 540
let print_stateless_prototype fmt (name, inputs, outputs) =
......
509 551
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
510 552
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
511 553
       ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
512
    pp_machine_memtype_name name
554
    (pp_machine_memtype_name ~ghost:false) name
513 555
    self
514 556

  
515 557
let print_import_prototype fmt dep =

Also available in: Unified diff