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_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 -> ident -> machine_t -> unit
22
  val pp_step_spec: formatter -> ident -> machine_t -> unit
23
  val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
20 24
end
21 25

  
22 26
module EmptyMod = struct
27
  let pp_predicates _ _ _ = ()
28
  let pp_reset_spec _ _ _ = ()
29
  let pp_step_spec _ _ _ = ()
30
  let pp_step_instr_spec _ _ _ _ = ()
23 31
end
24 32

  
25 33
module Main = functor (Mod: MODIFIERS_SRC) -> struct
......
274 282
  let pp_machine_clear =
275 283
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
276 284

  
277
  let has_c_prototype funname dependencies =
278
    (* We select the last imported node with the name funname.
279
       The order of evaluation of dependencies should be
280
       compatible with overloading. (Not checked yet) *)
281
    let imported_node_opt =
282
      List.fold_left
283
        (fun res dep ->
284
           match res with
285
           | Some _ -> res
286
           | None ->
287
             let decls = dep.content in
288
             let matched = fun t -> match t.top_decl_desc with
289
               | ImportedNode nd -> nd.nodei_id = funname
290
               | _ -> false
291
             in
292
             if List.exists matched decls then
293
               match (List.find matched decls).top_decl_desc with
294
               | ImportedNode nd -> Some nd
295
               | _ -> assert false
296
             else
297
               None) None dependencies in
298
    match imported_node_opt with
299
    | None -> false
300
    | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
301

  
302 285
  let pp_call m self pp_read pp_write fmt i
303 286
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
304 287
    try (* stateful node instance *)
......
406 389
      (pp_print_list ~pp_open_box:pp_open_vbox0
407 390
         (pp_machine_instr dependencies m self)) h
408 391

  
392
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
393
    pp_machine_instr dependencies m self fmt instr
394

  
395
  let pp_machine_step_instr dependencies m self fmt i instr =
396
    fprintf fmt "%a%a%a"
397
      (if i = 0 then
398
         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr))
399
       else
400
         pp_print_nothing) ()
401
      (pp_machine_instr dependencies m self) instr
402
      (Mod.pp_step_instr_spec m self) (i, instr)
409 403

  
410 404
  (********************************************************************************************)
411 405
  (*                         C file Printing functions                                        *)
......
474 468
       _alloc = (%a *) malloc(sizeof(%a));@,\
475 469
       assert(_alloc);@,\
476 470
       %a%areturn _alloc;"
477
      pp_machine_memtype_name m.mname.node_id
478
      pp_machine_memtype_name m.mname.node_id
479
      pp_machine_memtype_name m.mname.node_id
471
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
472
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
473
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
480 474
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
481 475
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
482 476

  
......
524 518

  
525 519
  let pp_print_function
526 520
      ~pp_prototype ~prototype
521
      ?(pp_spec=pp_print_nothing)
527 522
      ?(pp_local=pp_print_nothing) ?(base_locals=[])
528 523
      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
529 524
      ?(pp_init_mpfr_local=pp_print_nothing)
......
531 526
      ?(mpfr_locals=[])
532 527
      ?(pp_check=pp_print_nothing) ?(checks=[])
533 528
      ?(pp_extra=pp_print_nothing)
534
      ?(pp_instr=pp_print_nothing) ?(instrs=[])
529
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
535 530
      fmt =
536 531
    fprintf fmt
537
      "@[<v 2>%a {@,\
532
      "%a@[<v 2>%a {@,\
538 533
       %a%a\
539 534
       %a%a%a%a%areturn;@]@,\
540 535
       }"
536
      pp_spec ()
541 537
      pp_prototype prototype
542 538
      (* locals *)
543 539
      (pp_print_list
......
560 556
      (* check assertions *)
561 557
      (pp_print_list pp_check) checks
562 558
      (* instrs *)
563
      (pp_print_list
559
      (pp_print_list_i
564 560
         ~pp_open_box:pp_open_vbox0
565 561
         ~pp_epilogue:pp_print_cut
566 562
         pp_instr) instrs
......
593 589
        ~mpfr_locals:m.mstep.step_locals
594 590
        ~pp_check:(pp_c_check m self)
595 591
        ~checks:m.mstep.step_checks
596
        ~pp_instr:(pp_machine_instr dependencies m self)
592
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
597 593
        ~instrs:m.mstep.step_instrs
598 594
        fmt
599 595
    else
......
615 611
        ~mpfr_locals:m.mstep.step_locals
616 612
        ~pp_check:(pp_c_check m self)
617 613
        ~checks:m.mstep.step_checks
618
        ~pp_instr:(pp_machine_instr dependencies m self)
614
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
619 615
        ~instrs:m.mstep.step_instrs
620 616
        fmt
621 617

  
622 618
  let print_reset_code dependencies self fmt m =
623 619
    pp_print_function
620
      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m)
624 621
      ~pp_prototype:(print_reset_prototype self)
625 622
      ~prototype:(m.mname.node_id, m.mstatic)
626 623
      ~pp_local:(pp_c_decl_local_var m)
627 624
      ~base_locals:(const_locals m)
628
      ~pp_instr:(pp_machine_instr dependencies m self)
625
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
629 626
      ~instrs:m.minit
630 627
      fmt
631 628

  
......
670 667
    then
671 668
      (* C99 code *)
672 669
      pp_print_function
670
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
673 671
        ~pp_prototype:(print_step_prototype self)
674 672
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
675 673
        ~pp_local:(pp_c_decl_local_var m)
......
681 679
        ~mpfr_locals:m.mstep.step_locals
682 680
        ~pp_check:(pp_c_check m self)
683 681
        ~checks:m.mstep.step_checks
684
        ~pp_instr:(pp_machine_instr dependencies m self)
682
        ~pp_instr:(pp_machine_step_instr dependencies m self)
685 683
        ~instrs:m.mstep.step_instrs
686 684
        fmt
687 685
    else
......
692 690
          let id, _, _ = call_of_expr e in
693 691
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
694 692
      pp_print_function
693
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
695 694
        ~pp_prototype:(print_step_prototype self)
696 695
        ~prototype:(m.mname.node_id,
697 696
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
......
703 702
        ~mpfr_locals:m.mstep.step_locals
704 703
        ~pp_check:(pp_c_check m self)
705 704
        ~checks:m.mstep.step_checks
706
        ~pp_instr:(pp_machine_instr dependencies m self)
705
        ~pp_instr:(pp_machine_step_instr dependencies m self)
707 706
        ~instrs:m.mstep.step_instrs
708 707
        fmt
709 708

  
......
834 833
        (* Clear function *)
835 834
        (print_clear_code self) m
836 835

  
837

  
838 836
  (* TODO: ACSL
839 837
     - a contract machine shall not be directly printed in the C source
840 838
     - but a regular machine associated to a contract machine shall integrate
......
849 847
      print_stateless_code dependencies fmt m
850 848
    else
851 849
      let self = mk_self m in
852
      fprintf fmt "@[<v>%a%a@,%a%a@]"
850
      fprintf fmt "@[<v>%a%a@,@,%a%a@]"
853 851
        print_alloc_function m
854 852
        (* Reset function *)
855 853
        (print_reset_code dependencies self) m
......
889 887
       %a\
890 888
       %a\
891 889
       %a\
890
       %a\
892 891
       @]@."
893 892
      print_import_standard ()
894 893
      print_import_prototype
......
967 966
         print_machine_struct
968 967
         ~pp_epilogue:pp_print_cutcut) machines
969 968

  
969
      (* Print the spec predicates *)
970
      (Mod.pp_predicates dependencies) machines
971

  
970 972
      (* Print nodes one by one (in the previous order) *)
971 973
      (pp_print_list
972 974
         ~pp_open_box:pp_open_vbox0

Also available in: Unified diff