Project

General

Profile

« Previous | Next » 

Revision 8d2d6fa0

Added by LĂ©lio Brun about 3 years ago

Almost works!

View differences:

src/backends/C/c_backend_spec.ml
142 142
let pp_acsl_basic_type_desc t_desc =
143 143
  if Types.is_bool_type t_desc then
144 144
    (* if !Options.cpp then "bool" else "_Bool" *)
145
    "integer"
145
    "_Bool"
146 146
  else if Types.is_int_type t_desc then
147 147
    (* !Options.int_type *)
148 148
    "integer"
......
174 174
let pp_ensures pp_ens fmt =
175 175
  fprintf fmt "ensures %a;" pp_ens
176 176

  
177
let pp_assigns pp_asg fmt =
178
  fprintf fmt "assigns %a;" pp_asg
177
let pp_assigns pp =
178
  pp_print_list
179
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
180
    ~pp_epilogue:pp_print_semicolon'
181
    ~pp_sep:pp_print_comma
182
    pp
179 183

  
180 184
let pp_ghost pp_gho fmt =
181 185
  fprintf fmt "ghost %a" pp_gho
......
188 192

  
189 193
let pp_mem_valid' = pp_mem_valid pp_print_string
190 194

  
191
let pp_indirect pp_field fmt (ptr, field) =
192
  fprintf fmt "%s->%a" ptr pp_field field
195
let pp_indirect pp_ptr pp_field fmt (ptr, field) =
196
  fprintf fmt "%a->%a" pp_ptr ptr pp_field field
193 197

  
194
let pp_indirect' = pp_indirect pp_print_string
198
let pp_indirect' = pp_indirect pp_print_string pp_print_string
195 199

  
196
let pp_access pp_field fmt (stru, field) =
197
  fprintf fmt "%s.%a" stru pp_field field
200
let pp_access pp_stru pp_field fmt (stru, field) =
201
  fprintf fmt "%a.%a" pp_stru stru pp_field field
198 202

  
199
let pp_access' = pp_access pp_print_string
203
let pp_access' = pp_access pp_print_string pp_print_string
200 204

  
201 205
let pp_inst self fmt (name, _) =
202 206
  pp_indirect' fmt (self, name)
203 207

  
208
let pp_var_decl fmt v =
209
  pp_print_string fmt v.var_id
210

  
211
let pp_reg self fmt field =
212
  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)
213

  
204 214
let pp_true fmt () =
205 215
  pp_print_string fmt "\\true"
206 216

  
207
let pp_separated self fmt =
208
  fprintf fmt "\\separated(@[<h>%s%a@])"
217
(* let memories machines m =
218
 *   let open List in
219
 *   let grow paths i =
220
 *     match paths with
221
 *     | [] -> [[i]]
222
 *     | _ -> map (cons i) paths
223
 *   in
224
 *   let rec aux paths m =
225
 *     map (fun (i, (td, _)) ->
226
 *         let paths = grow paths i in
227
 *         try
228
 *           let m = find (fun m -> m.mname.node_id = node_name td) machines in
229
 *           aux paths m
230
 *         with Not_found -> paths)
231
 *       m.minstances |> flatten
232
 *   in
233
 *   aux [] m |> map rev *)
234

  
235
let instances machines m =
236
  let open List in
237
  let grow paths i mems =
238
    match paths with
239
    | [] -> [[i, mems]]
240
    | _ -> map (cons (i, mems)) paths
241
  in
242
  let rec aux paths m =
243
    map (fun (i, (td, _)) ->
244
        try
245
          let m = find (fun m -> m.mname.node_id = node_name td) machines in
246
          aux (grow paths i m.mmemory) m
247
        with Not_found -> grow paths i [])
248
      m.minstances |> flatten
249
  in
250
  aux [] m |> map rev
251

  
252
let memories insts =
253
  List.(map (fun path ->
254
      let mems = snd (hd (rev path)) in
255
      map (fun mem -> path, mem) mems) insts |> flatten)
256

  
257
let pp_instance =
258
  pp_print_list
259
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
260
    ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
261
    (fun fmt (i, _) -> pp_print_string fmt i)
262

  
263
let pp_memory fmt (path, mem) =
264
  pp_access (pp_indirect pp_instance pp_print_string) pp_var_decl
265
    fmt ((path, "_reg"), mem)
266
  (* let mems = snd List.(hd (rev path)) in
267
   * pp_print_list
268
   *   ~pp_sep:pp_print_comma
269
   *   (fun fmt mem -> pp_access pp_instance pp_var_decl fmt (path, mem))
270
   *   fmt
271
   *   mems *)
272
  (* let mems = ref [] in
273
   * let pp fmt =
274
   *   pp_print_list
275
   *     ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
276
   *     ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
277
   *     (fun fmt (i, regs) -> mems := regs; pp_print_string fmt i)
278
   *     fmt
279
   * in
280
   * pp_print_list
281
   *   ~pp_sep:pp_print_comma
282
   *   (fun fmt mem -> pp_access pp pp_var_decl fmt (insts, mem))
283
   *   fmt !mems *)
284

  
285
let prefixes l =
286
  let rec pref acc = function
287
    | x :: l -> pref ([x] :: List.map (List.cons x) acc) l
288
    | [] -> acc
289
  in
290
  pref [] (List.rev l)
291

  
292
let powerset_instances paths =
293
  List.map prefixes paths |> List.flatten
294

  
295
let pp_separated self fmt (paths, ptrs) =
296
  fprintf fmt "\\separated(@[<h>%s%a%a@])"
209 297
    self
210 298
    (pp_print_list
211 299
       ~pp_prologue:pp_print_comma
212 300
       ~pp_sep:pp_print_comma
213
       (pp_inst self))
301
       pp_instance)
302
    paths
303
    (pp_print_list
304
       ~pp_prologue:pp_print_comma
305
       ~pp_sep:pp_print_comma
306
       pp_var_decl)
307
    ptrs
214 308

  
215 309
let pp_forall pp_l pp_r fmt (l, r) =
216 310
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
......
281 375

  
282 376
let pp_mem_init' = pp_mem_init pp_print_string
283 377

  
284
let pp_var_decl fmt v =
285
  pp_print_string fmt v.var_id
286

  
287 378
let pp_locals m fmt vs =
288 379
  pp_print_list
289 380
    ~pp_open_box:pp_open_hbox
......
293 384
let pp_ptr_decl fmt v =
294 385
  fprintf fmt "*%s" v.var_id
295 386

  
296
let pp_basic_assign_spec pp_var fmt typ var_name value =
387
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
297 388
  if Types.is_real_type typ && !Options.mpfr
298 389
  then
299 390
    assert false
300 391
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
301 392
  else
302
    pp_equal pp_var pp_var fmt (var_name, value)
393
    pp_equal pp_l pp_r fmt (var_name, value)
303 394

  
304
let pp_assign_spec m self pp_var fmt (var_type, var_name, value) =
395
let pp_assign_spec
396
    m self_l pp_var_l self_r pp_var_r fmt (var_type, var_name, value) =
305 397
  let depth = expansion_depth value in
306 398
  let loop_vars = mk_loop_variables m var_type depth in
307 399
  let reordered_loop_vars = reorder_loop_variables loop_vars in
......
309 401
    match vars with
310 402
    | [] ->
311 403
      pp_basic_assign_spec
312
        (pp_value_suffix ~indirect:false m self var_type loop_vars pp_var)
404
        (pp_value_suffix ~indirect:false m self_l var_type loop_vars pp_var_l)
405
        (pp_value_suffix ~indirect:false m self_r var_type loop_vars pp_var_r)
313 406
        fmt typ var_name value
314 407
    | (d, LVar i) :: q ->
315 408
      assert false
......
495 588
    match instr.instr_desc with
496 589
    | MStateAssign (m, _) ->
497 590
      pp_equal
498
        (pp_access (pp_access pp_var_decl))
499
        (pp_indirect (pp_access pp_var_decl))
591
        (pp_access pp_print_string (pp_access pp_print_string pp_var_decl))
592
        (pp_indirect pp_print_string (pp_access pp_print_string pp_var_decl))
500 593
        fmt
501 594
        ((mem, ("_reg", m)), (self, ("_reg", m)))
502 595
    | MStep ([i0], i, vl)
......
586 679
  let rec aux fmt instr = match instr.instr_desc with
587 680
    | MLocalAssign (x, v)
588 681
    | MStateAssign (x, v) ->
589
      pp_assign_spec m mem_in (pp_c_var_read m) fmt
682
      pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m)fmt
590 683
        (x.var_type, mk_val (Var x) x.var_type, v)
591 684
    | MStep ([i0], i, vl)
592 685
      when Basic_library.is_value_internal_fun
......
614 707
        with Not_found -> pp_true fmt ()
615 708
      end
616 709
    | MBranch (v, brs) ->
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 *\) *)
710
      if let t = fst (List.hd brs) in t = tag_true || t = tag_false
711
      then (* boolean case *)
712
        pp_ite (pp_c_val m mem_in (pp_c_var_read m))
713
          (fun fmt () ->
714
             try
715
               let l = List.assoc tag_true brs in
716
               pp_paren (pp_and_l aux) fmt l
717
             with Not_found -> pp_true fmt ())
718
          (fun fmt () ->
719
             try
720
               let l = List.assoc tag_false brs in
721
               pp_paren (pp_and_l aux) fmt l
722
             with Not_found -> pp_true fmt ())
723
          
724
          (* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux)) *)
725
          fmt (v, (), ())
726
      else (* enum type case *)
625 727
      pp_and_l (fun fmt (l, instrs) ->
626 728
          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
729
          (* if l = tag_false then
730
           *   pp_paren (pp_implies
731
           *               (pp_different pp_val pp_c_tag)
732
           *               (pp_and_l aux))
733
           *     fmt
734
           *     ((v, tag_true), instrs)
735
           * else *)
634 736
            pp_paren (pp_implies
635 737
                        (pp_equal pp_val pp_c_tag)
636 738
                        (pp_and_l aux))
......
717 819
       (pp_predicate
718 820
          (pp_mem_init pp_machine_decl)
719 821
          (pp_equal
720
             (pp_access pp_access')
822
             (pp_access pp_print_string pp_access')
721 823
             pp_print_int)))
722 824
    ((name, (name, "mem_ghost", mem_in)),
723 825
     (mem_in_first, 1))
......
727 829
          (pp_mem_trans_aux
728 830
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
729 831
          (pp_ite
730
             (pp_access pp_access')
832
             (pp_access pp_print_string pp_access')
731 833
             (pp_paren
732 834
                (pp_and
733 835
                   (pp_equal
734
                      (pp_access pp_access')
836
                      (pp_access pp_print_string pp_access')
735 837
                      pp_print_int)
736 838
                   (pp_equal pp_print_string pp_print_string)))
737 839
                (pp_paren
738 840
                   (pp_and
739 841
                      (pp_equal
740
                         (pp_access pp_access')
741
                         (pp_access pp_access'))
842
                         (pp_access pp_print_string pp_access')
843
                         (pp_access pp_print_string pp_access'))
742 844
                      (pp_equal pp_print_string pp_print_string))))))
743
    ((name, ["integer x"; "integer y"], [], ["integer out"],
845
    ((name, ["integer x"; "integer y"], [], ["_Bool out"],
744 846
      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
745 847
     (* (("out", mem_in_first), *)
746 848
     (mem_in_first, ((mem_out_first, 0), ("out", "x")),
......
750 852
       (pp_predicate
751 853
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
752 854
          (pp_equal
753
             (pp_access pp_access')
754
             (pp_indirect pp_access'))))
855
             (pp_access pp_print_string pp_access')
856
             (pp_indirect pp_print_string pp_access'))))
755 857
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
756 858
    ((mem, reg_first), (self, reg_first)))
757 859

  
......
785 887
         (print_machine_trans_annotations machines dependencies)
786 888
         ~pp_epilogue:pp_print_cutcut) machines
787 889

  
788
  let pp_reset_spec fmt self m =
890
  let pp_register =
891
    pp_print_list
892
      ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
893
      ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
894
      ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
895
      (fun fmt (i, _) -> pp_print_string fmt i)
896

  
897
  let pp_reset_spec fmt machines self m =
789 898
    let name = m.mname.node_id in
790 899
    let mem = mk_mem m in
900
    let insts = instances machines m in
791 901
    pp_spec_cut (fun fmt () ->
792 902
        fprintf fmt
793 903
          "%a@,%a@,%a@,%a"
794 904
          (pp_requires pp_mem_valid') (name, self)
795
          (pp_requires (pp_separated self)) m.minstances
796
          (pp_assigns
797
             (pp_print_list
798
                ~pp_sep:pp_print_comma
799
                ~pp_nil:pp_nothing
800
                (pp_inst self))) m.minstances
905
          (pp_requires (pp_separated self)) (powerset_instances insts, [])
906
          (pp_assigns pp_register) insts
801 907
          (pp_ensures
802 908
             (pp_forall
803 909
                pp_machine_decl
......
808 914
           ((name, mem, self), (name, mem))))
809 915
      fmt ()
810 916

  
811
  let pp_step_spec fmt self m =
917
  let pp_step_spec fmt machines self m =
812 918
    let name = m.mname.node_id in
813 919
    let mem_in = mk_mem_in m in
814 920
    let mem_out = mk_mem_out m in
921
    let insts = instances machines m in
922
    let insts' = powerset_instances insts in
815 923
    pp_spec_cut (fun fmt () ->
816 924
        fprintf fmt
817
          "%a@,%a@,%a@,%a@,%a"
925
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
818 926
          (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
819 927
          (pp_requires pp_mem_valid') (name, self)
820
          (pp_requires (pp_separated self)) m.minstances
821
          (pp_assigns
822
             (if m.mstep.step_outputs = [] && m.minstances = [] then
823
                pp_nothing
824
              else
825
                fun fmt () ->
826
                  fprintf fmt "@[<h>%a%a@]"
827
                    (pp_print_list
828
                       ~pp_sep:pp_print_comma
829
                       ~pp_epilogue:pp_print_comma
830
                       pp_ptr_decl) m.mstep.step_outputs
831
                    (pp_print_list
832
                       ~pp_sep:pp_print_comma
833
                       (pp_inst self)) m.minstances)) ()
928
          (pp_requires (pp_separated self)) (insts', m.mstep.step_outputs)
929
          (pp_assigns pp_ptr_decl) m.mstep.step_outputs
930
          (pp_assigns (pp_reg self)) m.mmemory
931
          (pp_assigns pp_memory) (memories insts')
932
          (pp_assigns pp_register) insts
834 933
          (pp_ensures
835 934
             (pp_forall
836 935
                (fun fmt () ->

Also available in: Unified diff