Project

General

Profile

« Previous | Next » 

Revision 7f03f62d

Added by LĂ©lio Brun 9 months ago

first version that is parsed correctly by Frama-C

View differences:

src/backends/C/c_backend_spec.ml
139 139
  Format.fprintf fmt "";
140 140
  ()
141 141

  
142
let pp_acsl_basic_type_desc t_desc =
143
  if Types.is_bool_type t_desc then
144
    (* if !Options.cpp then "bool" else "_Bool" *)
145
    "integer"
146
  else if Types.is_int_type t_desc then
147
    (* !Options.int_type *)
148
    "integer"
149
  else if Types.is_real_type t_desc then
150
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
151
  else
152
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
153

  
142 154
module VarDecl = struct
143 155
  type t = var_decl
144 156
  let compare v1 v2 = compare v1.var_id v2.var_id
......
211 223
    pp_r r
212 224

  
213 225
let pp_valid =
214
  pp_print_parenthesized
226
  pp_print_braced
215 227
    ~pp_nil:pp_true
216
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid")
228
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid(")
229
    ~pp_epilogue:pp_print_cpar
217 230

  
218 231
let pp_equal pp_l pp_r fmt (l, r) =
219 232
  fprintf fmt "%a == %a"
220 233
    pp_l l
221 234
    pp_r r
222 235

  
236
let pp_different pp_l pp_r fmt (l, r) =
237
  fprintf fmt "%a != %a"
238
    pp_l l
239
    pp_r r
240

  
223 241
let pp_implies pp_l pp_r fmt (l, r) =
224 242
  fprintf fmt "@[<v>%a ==>@ %a@]"
225 243
    pp_l l
......
259 277
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
260 278

  
261 279
let pp_mem_init pp_mem fmt (name, mem) =
262
  fprintf fmt "%s_init(%a)" name pp_mem mem
280
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
263 281

  
264 282
let pp_mem_init' = pp_mem_init pp_print_string
265 283

  
......
270 288
  pp_print_list
271 289
    ~pp_open_box:pp_open_hbox
272 290
    ~pp_sep:pp_print_comma
273
    (pp_c_decl_local_var m) fmt vs
291
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs
274 292

  
275 293
let pp_ptr_decl fmt v =
276 294
  fprintf fmt "*%s" v.var_id
277 295

  
296
let pp_basic_assign_spec pp_var fmt typ var_name value =
297
  if Types.is_real_type typ && !Options.mpfr
298
  then
299
    assert false
300
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
301
  else
302
    pp_equal pp_var pp_var fmt (var_name, value)
303

  
304
let pp_assign_spec m self pp_var fmt (var_type, var_name, value) =
305
  let depth = expansion_depth value in
306
  let loop_vars = mk_loop_variables m var_type depth in
307
  let reordered_loop_vars = reorder_loop_variables loop_vars in
308
  let rec aux typ fmt vars =
309
    match vars with
310
    | [] ->
311
      pp_basic_assign_spec
312
        (pp_value_suffix ~indirect:false m self var_type loop_vars pp_var)
313
        fmt typ var_name value
314
    | (d, LVar i) :: q ->
315
      assert false
316
      (* let typ' = Types.array_element_type typ in
317
       * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
318
       *   i i i pp_c_dimension d i
319
       *   (aux typ') q *)
320
    | (d, LInt r) :: q ->
321
      assert false
322
      (* let typ' = Types.array_element_type typ in
323
       * let szl = Utils.enumerate (Dimension.size_const_dimension d) in
324
       * fprintf fmt "@[<v 2>{@,%a@]@,}"
325
       *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
326
    | _ -> assert false
327
  in
328
  begin
329
    reset_loop_counter ();
330
    aux var_type fmt reordered_loop_vars;
331
  end
332

  
333
let pp_c_var_read m fmt id =
334
  (* mpfr_t is a static array, not treated as general arrays *)
335
  if Types.is_address_type id.var_type
336
  then
337
    if Machine_code_common.is_memory m id
338
    && not (Types.is_real_type id.var_type && !Options.mpfr)
339
    then fprintf fmt "(*%s)" id.var_id
340
    else fprintf fmt "%s" id.var_id
341
  else
342
    fprintf fmt "%s" id.var_id
343

  
278 344
let rec assigned s instr =
279 345
  let open VDSet in
280 346
  match instr.instr_desc with
......
336 402

  
337 403
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
338 404
    (name, inputs, locals, outputs, mem_in, mem_out) =
339
  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a%a@])"
405
  fprintf fmt "%s_transition%a(@[<hov>%a,@ %a%a%a%a@])"
340 406
    name
341 407
    (pp_print_option pp_print_int) i
342 408
    pp_mem_in mem_in
......
380 446
     mem_out)
381 447

  
382 448
let pp_mem_trans' ?i fmt =
449
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt
450
let pp_mem_trans'' ?i fmt =
383 451
  pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
384 452

  
385 453
let pp_nothing fmt () =
......
479 547
      (print_machine_ghost_simulation_aux m
480 548
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
481 549

  
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 550
let print_machine_trans_simulation_aux ?i m pp fmt v =
520 551
  let name = m.mname.node_id in
521 552
  let mem_in = mk_mem_in m in
......
523 554
  pp_spec
524 555
    (pp_predicate
525 556
       (pp_mem_trans pp_machine_decl pp_machine_decl
526
          (pp_c_decl_local_var m) pp_c_decl_output_var ?i)
557
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
558
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
559
          ?i)
527 560
       pp)
528 561
    fmt
529 562
    ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
......
532 565
let print_trans_simulation machines dependencies m fmt (i, instr) =
533 566
  let mem_in = mk_mem_in m in
534 567
  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"
568
  let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
569
                   (live_i m (i+1))) in
570
  (* XXX *)
571
  printf "%d : %a\n%d : %a\nocc: %a\n\n"
537 572
    i
538 573
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
539 574
    (i+1)
540
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)));
575
    (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
576
    (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr));
541 577
  let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
542 578
  let pred pp v =
543
    let locals = VDSet.(inter (of_list m.mstep.step_locals) d |> elements) in
579
    let vars = VDSet.(union (of_list m.mstep.step_locals)
580
                        (of_list m.mstep.step_outputs)) in
581
    let locals = VDSet.(inter vars d |> elements) in
544 582
    if locals = []
545 583
    then pp_and prev_trans pp fmt ((), v)
546 584
    else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
......
576 614
        with Not_found -> pp_true fmt ()
577 615
      end
578 616
    | MBranch (v, brs) ->
579
      (* TODO: handle branches *)
617
      (* if let t = fst (List.hd brs) in t = tag_true || t = tag_false
618
       * then (\* boolean case *\)
619
       *   let tl = try List.assoc tag_true  brs with Not_found -> [] in
620
       *   let el = try List.assoc tag_false brs with Not_found -> [] in
621
       *   pp_ite (pp_c_val m mem_in (pp_c_var_read m))
622
       *     (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux))
623
       *     fmt (v, tl, el)
624
       * else (\* enum type case *\) *)
580 625
      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))
626
          let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
627
          if l = tag_false then
628
            pp_paren (pp_implies
629
                        (pp_different pp_val pp_c_tag)
630
                        (pp_and_l aux))
631
              fmt
632
              ((v, tag_true), instrs)
633
          else
634
            pp_paren (pp_implies
635
                        (pp_equal pp_val pp_c_tag)
636
                        (pp_and_l aux))
637
              fmt
638
              ((v, l), instrs))
588 639
        fmt brs
589 640
    | _ -> pp_true fmt ()
590 641
  in
......
596 647
    ~i:(i+1)
597 648
    fmt (i, instr)
598 649

  
599
let print_machine_core_annotations machines dependencies fmt m =
650
let print_machine_trans_annotations machines dependencies fmt m =
600 651
  if not (fst (Machine_code_common.get_stateless_status m)) then begin
601 652
    set_live_of m;
602 653
    let i = List.length m.mstep.step_instrs in
......
622 673
      (print_machine_trans_simulation_aux m last_trans) ()
623 674
  end
624 675

  
676
let print_machine_init_predicate fmt m =
677
  if not (fst (Machine_code_common.get_stateless_status m)) then
678
    let name = m.mname.node_id in
679
    let mem_in = mk_mem_in m in
680
    pp_spec
681
      (pp_predicate
682
         (pp_mem_init pp_machine_decl)
683
         (pp_and_l (fun fmt (i, (td, _)) ->
684
              pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))
685
      fmt
686
      ((name, (name, "mem_ghost", mem_in)), m.minstances)
687

  
625 688
let pp_at pp_p fmt (p, l) =
626 689
  fprintf fmt "\\at(%a, %s)" pp_p p l
627 690

  
......
639 702
  let mem_out_first = mem_out, reg_first in
640 703
  let mem = "mem" in
641 704
  let self = "self" in
642
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a"
705
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"
706

  
643 707
    (pp_spec_line (pp_ghost pp_print_string))
644 708
    "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
709

  
710
    (pp_spec_cut
711
       (pp_predicate
712
          (pp_mem_valid pp_machine_decl)
713
          (pp_valid pp_print_string)))
714
    ((name, (name, "mem", "*" ^ self)), [self])
715

  
645 716
    (pp_spec_cut
646 717
       (pp_predicate
647 718
          (pp_mem_init pp_machine_decl)
648 719
          (pp_equal
649 720
             (pp_access pp_access')
650
             pp_print_string)))
721
             pp_print_int)))
651 722
    ((name, (name, "mem_ghost", mem_in)),
652
     (mem_in_first, "true"))
723
     (mem_in_first, 1))
724

  
653 725
    (pp_spec_cut
654 726
       (pp_predicate
655 727
          (pp_mem_trans_aux
......
660 732
                (pp_and
661 733
                   (pp_equal
662 734
                      (pp_access pp_access')
663
                      pp_print_string)
735
                      pp_print_int)
664 736
                   (pp_equal pp_print_string pp_print_string)))
665 737
                (pp_paren
666 738
                   (pp_and
......
668 740
                         (pp_access pp_access')
669 741
                         (pp_access pp_access'))
670 742
                      (pp_equal pp_print_string pp_print_string))))))
671
    ((name, ["int x"; "int y"], [], ["_Bool out"],
743
    ((name, ["integer x"; "integer y"], [], ["integer out"],
672 744
      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
673 745
     (* (("out", mem_in_first), *)
674
     (mem_in_first, ((mem_out_first, "false"), ("out", "x")),
746
     (mem_in_first, ((mem_out_first, 0), ("out", "x")),
675 747
      ((mem_out_first, mem_in_first), ("out", "y"))))
748

  
676 749
    (pp_spec_cut
677 750
       (pp_predicate
678 751
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
......
686 759

  
687 760
  let pp_predicates dependencies fmt machines =
688 761
    fprintf fmt
689
      "%a@,%a%a%a"
762
      "%a@,%a%a%a%a"
690 763
      pp_arrow_spec ()
691 764
      (pp_print_list
692 765
         ~pp_open_box:pp_open_vbox0
......
702 775
      (pp_print_list
703 776
         ~pp_open_box:pp_open_vbox0
704 777
         ~pp_sep:pp_print_cutcut
705
         ~pp_prologue:(pp_print_endcut "/* ACSL core annotations */")
706
         (print_machine_core_annotations machines dependencies)
778
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
779
         print_machine_init_predicate
780
         ~pp_epilogue:pp_print_cutcut) machines
781
      (pp_print_list
782
         ~pp_open_box:pp_open_vbox0
783
         ~pp_sep:pp_print_cutcut
784
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
785
         (print_machine_trans_annotations machines dependencies)
707 786
         ~pp_epilogue:pp_print_cutcut) machines
708 787

  
709 788
  let pp_reset_spec fmt self m =
......
762 841
                   (pp_at_pre pp_mem_ghost')
763 842
                   (pp_implies
764 843
                      pp_mem_ghost'
765
                      pp_mem_trans'))))
844
                      pp_mem_trans''))))
766 845
          ((),
767 846
           ((name, mem_in, self),
768 847
            ((name, mem_out, self),
......
785 864
                  (pp_at_pre pp_mem_ghost')
786 865
                  (pp_implies
787 866
                     (pp_mem_ghost' ~i)
788
                     (pp_mem_trans' ~i))))))
867
                     (pp_mem_trans'' ~i))))))
789 868
      ((),
790 869
       ((name, mem_in, self),
791 870
        ((name, mem_out, self),

Also available in: Unified diff