Project

General

Profile

« Previous | Next » 

Revision c4780a6a

Added by LĂ©lio Brun 7 months ago

work on new reset functions generation

View differences:

src/backends/C/c_backend_spec.ml
49 49
let pp_acsl_line pp fmt =
50 50
  fprintf fmt "//%@ @[<h>%a@]" pp
51 51

  
52
let pp_acsl_line' pp fmt =
53
  fprintf fmt "/*%@ @[<h>%a@] */" pp
54

  
55
let pp_acsl_line_cut pp fmt =
56
  fprintf fmt "%a@," (pp_acsl_line pp)
57

  
52 58
let pp_requires pp_req fmt =
53 59
  fprintf fmt "requires %a;" pp_req
54 60

  
......
362 368

  
363 369
  let pp_reg pp_mem fmt = function
364 370
    | ResetFlag ->
365
      fprintf fmt "%t_reset" pp_mem
371
      fprintf fmt "%t%s" pp_mem reset_flag_name
366 372
    | StateVar x ->
367 373
      fprintf fmt "%t%a" pp_mem pp_var_decl x
368 374

  
......
695 701
let pp_at_pre pp_p fmt p =
696 702
  pp_at pp_p fmt (p, label_pre)
697 703

  
698
let pp_register ?(indirect=true) ptr =
704
let pp_register_chain ?(indirect=true) ptr =
699 705
  pp_print_list
700 706
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
701 707
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
......
703 709
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
704 710
    (fun fmt (i, _) -> pp_print_string fmt i)
705 711

  
706
let pp_reset_flag ?(indirect=true) ptr fmt mems =
712
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
707 713
  pp_print_list
708 714
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
709
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reset"
710
                     (if indirect then "->" else "."))
715
    ~pp_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
711 716
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
712 717
    (fun fmt (i, _) -> pp_print_string fmt i)
713 718
    fmt mems
714 719

  
720
let pp_arrow_reset_ghost mem fmt inst =
721
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
722

  
715 723
module GhostProto: MODIFIERS_GHOST_PROTO = struct
716
  let pp_ghost_parameters fmt vs =
717
    fprintf fmt "@;%a"
718
      (pp_acsl (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
724
  let pp_ghost_parameters ?(cut=true) fmt vs =
725
    fprintf fmt "%a%a"
726
      (if cut then pp_print_cut else pp_print_nothing) ()
727
      (pp_acsl_line'
728
         (pp_ghost
729
            (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
719 730
      vs
720 731
end
721 732

  
......
763 774
         pp_transition_defs
764 775
         ~pp_epilogue:pp_print_cutcut) machines
765 776

  
766
  let pp_clear_reset_spec fmt machines self mem m =
777
  let pp_clear_reset_spec fmt self mem m =
767 778
    let name = m.mname.node_id in
768 779
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
769 780
        m.minstances in
770 781
    let mk_insts = List.map (fun x -> [x]) in
771 782
    pp_acsl_cut (fun fmt () ->
772 783
        fprintf fmt
773
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
784
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
774 785
          @[<v 2>behavior reset:@;\
775 786
          %a@,%a@]@,\
776 787
          @[<v 2>behavior no_reset:@;\
777
          %a@,%a@]"
788
          %a@,%a@]@,\
789
          complete behaviors;@,\
790
          disjoint behaviors;"
778 791
          (pp_requires pp_mem_valid') (name, self)
779 792
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
793
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
794
          (name, mem, self)
780 795
          (pp_ensures (pp_memory_pack_aux
781 796
                         ~i:(List.length m.mspec.mmemory_packs - 2)
782 797
                         pp_ptr pp_print_string))
783 798
          (name, mem, self)
784
          (pp_assigns pp_indirect') [self, "_reset"]
785
          (pp_assigns (pp_register self)) (mk_insts arws)
786
          (pp_assigns (pp_reset_flag self)) (mk_insts narws)
787
          (pp_assigns pp_indirect') [mem, "_reset"]
788
          (pp_assigns (pp_register ~indirect:false mem)) (mk_insts arws)
789
          (pp_assigns (pp_reset_flag ~indirect:false mem)) (mk_insts narws)
790
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 1)
799
          (pp_assigns pp_reset_flag) [self]
800
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
801
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
802
          (pp_assigns pp_reset_flag) [mem]
803
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
804
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
805
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
791 806
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
792
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 0)
807
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
793 808
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
794 809
      )
795 810
      fmt ()
......
800 815
        fprintf fmt
801 816
          "%a@,%a@,%a"
802 817
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
803
          (pp_ensures (pp_equal pp_indirect' pp_print_string)) ((mem, "_reset"), "1")
804
          (pp_assigns (fun fmt ptr -> pp_indirect' fmt (ptr, "_reset"))) [self; mem])
818
          (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
819
          (pp_assigns pp_reset_flag) [self; mem])
805 820
      fmt ()
806 821

  
807 822
  let pp_step_spec fmt machines self mem m =
......
833 848
            (pp_assigns pp_ptr_decl) outputs
834 849
            (pp_assigns (pp_reg self)) m.mmemory
835 850
            (pp_assigns (pp_memory self)) (memories insts')
836
            (pp_assigns (pp_register self)) insts
837
            (pp_assigns (pp_reset_flag self)) insts''
851
            (pp_assigns (pp_register_chain self)) insts
852
            (pp_assigns (pp_reset_flag_chain self)) insts''
838 853
            (pp_assigns (pp_reg mem)) m.mmemory
839 854
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
840
            (pp_assigns (pp_register ~indirect:false mem)) insts
841
            (pp_assigns (pp_reset_flag ~indirect:false mem)) insts''
855
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
856
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
842 857
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
843 858
                           pp_ptr pp_var_decl pp_ptr_decl))
844 859
            (name, inputs, [], outputs, mem, mem)
845 860
      )
846 861
      fmt ()
847 862

  
848
  let pp_step_instr_spec m self fmt instr =
849
    fprintf fmt "@,%a"
850
      (pp_print_list ~pp_open_box:pp_open_vbox0
851
         (pp_acsl (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
863
  let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
864
    | MStateAssign (x, v) ->
865
      fprintf fmt "@,%a"
866
        (pp_acsl_line
867
           (pp_ghost
868
              (pp_assign m self (pp_c_var_read m))))
869
        (x, v)
870
    | MResetAssign b ->
871
      fprintf fmt "@,%a"
872
        (pp_acsl_line
873
           (pp_ghost
874
              (pp_reset_assign self)))
875
        b
876
    | MSetReset inst ->
877
      let td, _ = List.assoc inst m.minstances in
878
      if Arrow.td_is_arrow td then
879
         fprintf fmt "@,%a"
880
           (pp_acsl_line
881
              (pp_ghost
882
                 (pp_arrow_reset_ghost self)))
883
           inst
884
    | _ -> ()
885

  
886
  let pp_step_instr_spec m self mem fmt instr =
887
    fprintf fmt "%a%a"
888
      (pp_ghost_instr_code m mem) instr
889
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
890
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
852 891
      instr.instr_spec
853 892

  
854
  let pp_ghost_set_reset_spec fmt =
855
    fprintf fmt "@;%a@;"
856
      (pp_acsl_line
857
         (pp_ghost
858
            (fun fmt mem -> fprintf fmt "%a = 1;" pp_indirect' (mem, "_reset"))))
893
  let pp_ghost_parameter mem fmt inst =
894
    GhostProto.pp_ghost_parameters ~cut:false fmt
895
      (match inst with
896
       | Some inst ->
897
         [inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)]
898
       | None ->
899
         [mem, pp_print_string])
900

  
859 901
end
860 902

  
861 903
(**************************************************************************)

Also available in: Unified diff