Revision c226a3ba
Added by Lélio Brun over 3 years ago
| 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
start generating ACSL spec