Project

General

Profile

« Previous | Next » 

Revision 15c3e4e7

Added by LĂ©lio Brun 11 months ago

generic ACSL spec generation

View differences:

src/backends/C/c_backend_spec.ml
135 135
let preprocess_acsl machines = machines, []
136 136
                          
137 137
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
138
let pp_acsl_preamble fmt preamble =
138
let pp_acsl_preamble fmt _preamble =
139 139
  Format.fprintf fmt "";
140 140
  ()
141 141

  
......
224 224
    pp_v
225 225
    fmt
226 226

  
227
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
228
  fprintf fmt "%a @[<hov>? %a@ : %a@]"
229
    pp_c c
230
    pp_t t
231
    pp_f f
232

  
227 233
let pp_machine_decl fmt (id, mem_type, var) =
228 234
  fprintf fmt "struct %s_%s %s" id mem_type var
229 235

  
230 236
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
231
  fprintf fmt "%s_ghost%a(%a, %a)"
237
  fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
232 238
    name
233 239
    (pp_print_option pp_print_int) i
234 240
    pp_mem mem
......
236 242

  
237 243
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
238 244

  
239
let pp_mem_init fmt (name, mem) =
240
  fprintf fmt "%s_init(%s)" name mem
245
let pp_mem_init pp_mem fmt (name, mem) =
246
  fprintf fmt "%s_init(%a)" name pp_mem mem
247

  
248
let pp_mem_init' = pp_mem_init pp_print_string
241 249

  
242 250
let pp_var_decl fmt v =
243 251
  pp_print_string fmt v.var_id
......
245 253
let pp_ptr_decl fmt v =
246 254
  fprintf fmt "*%s" v.var_id
247 255

  
248
let pp_mem_trans ?i fmt (m, mem_in, mem_out) =
249
  fprintf fmt "%s_trans%a(@[<h>%s, %a%s%a@])"
250
    m.mname.node_id
256
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
257
    (name, inputs, outputs, mem_in, mem_out) =
258
  fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a@])"
259
    name
251 260
    (pp_print_option pp_print_int) i
252
    mem_in
261
    pp_mem_in mem_in
253 262
    (pp_print_list
254 263
       ~pp_epilogue:pp_print_comma
255 264
       ~pp_sep:pp_print_comma
256
       pp_var_decl) m.mstep.step_inputs
257
    mem_out
265
       pp_input) inputs
266
    pp_mem_out mem_out
258 267
    (pp_print_list
259 268
       ~pp_prologue:pp_print_comma
260 269
       ~pp_sep:pp_print_comma
261
       pp_ptr_decl) m.mstep.step_outputs
270
       pp_output) outputs
271

  
272
let pp_mem_trans ?i pp_mem_in pp_mem_out fmt (m, mem_in, mem_out) =
273
  pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_var_decl pp_ptr_decl fmt
274
    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, mem_in, mem_out)
275

  
276
let pp_mem_trans' ?i fmt = pp_mem_trans ?i pp_print_string pp_print_string fmt
262 277

  
263 278
let pp_nothing fmt () =
264 279
  pp_print_string fmt "\\nothing"
......
349 364
      (print_machine_ghost_simulation_aux m
350 365
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
351 366

  
367
let print_machine_core_annotations dependencies fmt m =
368
  if not (fst (Machine_code_common.get_stateless_status m)) then
369
    let name = m.mname.node_id in
370
    let self = mk_self m in
371
    let mem = mk_mem m in
372
    fprintf fmt "%a@,%a@,%a%a"
373
      print_machine_ghost_struct m
374
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
375
      (pp_print_list_i
376
        ~pp_epilogue:pp_print_cut
377
        ~pp_open_box:pp_open_vbox0
378
        (print_machine_ghost_simulation dependencies m))
379
      m.mstep.step_instrs
380
      (print_machine_ghost_simulation_aux m
381
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
382

  
352 383
let pp_at pp_p fmt (p, l) =
353 384
  fprintf fmt "\\at(%a, %s)" pp_p p l
354 385

  
......
357 388
let pp_at_pre pp_p fmt p =
358 389
  pp_at pp_p fmt (p, label_pre)
359 390

  
391
module VarDecl = struct
392
  type t = var_decl
393
  let compare v1 v2 = compare v1.var_id v2.var_id
394
end
395
module VDSet = Set.Make(VarDecl)
396

  
397
let pp_arrow_spec fmt () =
398
  let name = "_arrow" in
399
  let mem_in = "mem_in" in
400
  let mem_out = "mem_out" in
401
  let reg_first = "_reg", "_first" in
402
  let mem_in_first = mem_in, reg_first in
403
  let mem_out_first = mem_out, reg_first in
404
  let mem = "mem" in
405
  let self = "self" in
406
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a"
407
    (pp_spec_line (pp_ghost pp_print_string))
408
    "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
409
    (pp_spec_cut
410
       (pp_predicate
411
          (pp_mem_init pp_machine_decl)
412
          (pp_equal
413
             (pp_access pp_access')
414
             pp_print_string)))
415
    ((name, (name, "mem_ghost", mem_in)),
416
     (mem_in_first, "true"))
417
    (pp_spec_cut
418
       (pp_predicate
419
          (pp_mem_trans_aux
420
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
421
          (pp_and
422
             (pp_equal
423
                pp_print_string
424
                (pp_access pp_access'))
425
             (pp_ite
426
                (pp_access pp_access')
427
                (pp_equal
428
                   (pp_access pp_access')
429
                   pp_print_string)
430
                (pp_equal
431
                   (pp_access pp_access')
432
                   (pp_access pp_access'))))))
433
    ((name, [], ["_Bool out"], (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
434
     (("out", mem_in_first),
435
      (mem_in_first, (mem_out_first, "false"), (mem_out_first, mem_in_first))))
436
    (pp_spec_cut
437
       (pp_predicate
438
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
439
          (pp_equal
440
             (pp_access pp_access')
441
             (pp_indirect pp_access'))))
442
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
443
    ((mem, reg_first), (self, reg_first)))
444

  
360 445
module SrcMod = struct
361 446

  
362 447
  let pp_predicates dependencies fmt machines =
363 448
    fprintf fmt
364
      "%a%a"
449
      "%a@,%a%a%a"
450
      pp_arrow_spec ()
365 451
      (pp_print_list
366 452
         ~pp_open_box:pp_open_vbox0
367 453
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
......
370 456
      (pp_print_list
371 457
         ~pp_open_box:pp_open_vbox0
372 458
         ~pp_sep:pp_print_cutcut
373
         ~pp_prologue:(fun fmt () -> fprintf fmt
374
                          "/* ACSL ghost simulations */@,%a"
375
                          (pp_spec_line (pp_ghost pp_print_string))
376
                          "struct _arrow_mem_ghost {struct _arrow_reg _reg;};")
459
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
377 460
         (print_machine_ghost_simulations dependencies)
378 461
         ~pp_epilogue:pp_print_cutcut) machines
462
      (pp_print_list
463
         ~pp_open_box:pp_open_vbox0
464
         ~pp_sep:pp_print_cutcut
465
         ~pp_prologue:(pp_print_endcut "/* ACSL core annotations */")
466
         (print_machine_core_annotations dependencies)
467
         ~pp_epilogue:pp_print_cutcut) machines
379 468

  
380 469
  let pp_reset_spec fmt self m =
381 470
    let name = m.mname.node_id in
......
395 484
                pp_machine_decl
396 485
                (pp_implies
397 486
                   pp_mem_ghost'
398
                   pp_mem_init)))
487
                   pp_mem_init')))
399 488
          ((name, "mem_ghost", mem),
400 489
           ((name, mem, self), (name, mem))))
401 490
      fmt ()
......
433 522
                   (pp_at_pre pp_mem_ghost')
434 523
                   (pp_implies
435 524
                      pp_mem_ghost'
436
                      pp_mem_trans))))
525
                      pp_mem_trans'))))
437 526
          ((),
438 527
           ((name, mem_in, self),
439 528
            ((name, mem_out, self),
440 529
             (m, mem_in, mem_out)))))
441 530
      fmt ()
442 531

  
443
  let pp_step_instr_spec m self fmt (i, instr) =
532
  let pp_step_instr_spec m self fmt (i, _instr) =
444 533
    let name = m.mname.node_id in
445 534
    let mem_in = mk_mem_in m in
446 535
    let mem_out = mk_mem_out m in
......
456 545
                  (pp_at_pre pp_mem_ghost')
457 546
                  (pp_implies
458 547
                     (pp_mem_ghost' ~i:(i+1))
459
                     (pp_mem_trans ~i:(i+1)))))))
548
                     (pp_mem_trans' ~i:(i+1)))))))
460 549
      ((),
461 550
       ((name, mem_in, self),
462 551
        ((name, mem_out, self),
src/causality.ml
544 544
     maybe removing shorter branches *)
545 545
  type disjoint_map = (ident, CISet.t) Hashtbl.t
546 546

  
547
  let pp_ciset fmt t =
548
    begin
549
      Format.fprintf fmt "{@ ";
550
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
551
      Format.fprintf fmt "}@."
552
    end
547
  let pp_ciset fmt t = let open Format in
548
    pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt
549
      (CISet.elements t)
553 550

  
554 551
  let clock_disjoint_map vdecls =
555 552
    let map = Hashtbl.create 23 in
......
602 599
    end
603 600

  
604 601
  let pp_disjoint_map fmt map =
605
    begin
606
      Format.fprintf fmt "{ /* disjoint map */@.";
607
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
608
      Format.fprintf fmt "}@."
609
    end
602
    Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }"
603
              (fun fmt ->
604
                 Hashtbl.iter (fun k v ->
605
                     fprintf fmt "@,%s # %a"
606
                       k (pp_print_braced' Printers.pp_var_name)
607
                       (CISet.elements v)) map))
610 608
end
611 609

  
612 610
  
613 611
let pp_dep_graph fmt g =
614
  begin
615
    Format.fprintf fmt "{ /* graph */@.";
616
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
617
    Format.fprintf fmt "}@."
618
  end
612
  Format.fprintf fmt "@[<v 2>{ /* graph */%t@] }"
613
    (fun fmt ->
614
       IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@,%s -> %s" s t) g)
619 615

  
620 616
let pp_error fmt err =
621 617
  match err with
src/checks/liveness.ml
141 141
  end
142 142

  
143 143
let pp_reuse_policy fmt policy =
144
  begin
145
    Format.fprintf fmt "{ /* reuse policy */@.";
146
    Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> %s@." s t.var_id) policy;
147
    Format.fprintf fmt "}@."
148
  end
144
  Format.(fprintf fmt "@[<v 2>{ /* reuse policy */%t@] }"
145
    (fun fmt -> Hashtbl.iter (fun s t -> fprintf fmt "@,%s -> %s" s t.var_id) policy))
149 146

  
150 147
let pp_context fmt ctx =
151
  begin
152
    Format.fprintf fmt "{ /*BEGIN context */@.";
153
    Format.fprintf fmt "eval=%a;@." Disjunction.pp_ciset ctx.evaluated;
154
    Format.fprintf fmt "graph=%a;@." pp_dep_graph ctx.dep_graph;
155
    Format.fprintf fmt "disjoint=%a;@." Disjunction.pp_disjoint_map ctx.disjoint;
156
    Format.fprintf fmt "policy=%a;@." pp_reuse_policy ctx.policy;
157
    Format.fprintf fmt "/* END context */ }@.";
158
  end
148
  Format.fprintf fmt
149
    "@[<v 2>{ /*BEGIN context */@,\
150
     eval     = %a;@,\
151
     graph    = %a;@,\
152
     disjoint = %a;@,\
153
     policy   = %a;@,\
154
     /* END context */ }@]"
155
    Disjunction.pp_ciset ctx.evaluated
156
    pp_dep_graph ctx.dep_graph
157
    Disjunction.pp_disjoint_map ctx.disjoint
158
    pp_reuse_policy ctx.policy
159 159

  
160 160
(* computes the reusable dependencies of variable [var] in graph [g],
161 161
   once [var] has been evaluated
......
197 197
  let locally_reusable v =
198 198
    IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in
199 199
  let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in
200
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles);
201 200
  let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in
202
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);
203
  try
204
    let disjoint_live = Disjunction.CISet.inter disjoint live in
205
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);
206
    let reuse = Disjunction.CISet.max_elt disjoint_live in
207
    begin
208
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
209
      Hashtbl.add ctx.policy var.var_id reuse;
210
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
211
      (*Format.eprintf "%s reused by live@." var.var_id;*)
212
    end
213
  with Not_found ->
214
  try
215
    let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
216
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);
217
    let reuse = Disjunction.CISet.choose dead in
218
    begin
201
  let disjoint_live = Disjunction.CISet.inter disjoint live in
202
  let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
203
  Log.report ~level:7 (fun fmt ->
204
      Format.fprintf fmt
205
        "@[<v>\
206
         eligibles    : %a@,\
207
         live         : %a@,\
208
         disjoint live: %a@,\
209
         dead         : %a@,@]"
210
        Disjunction.pp_ciset eligibles
211
        Disjunction.pp_ciset live
212
        Disjunction.pp_ciset disjoint_live
213
        Disjunction.pp_ciset dead);
214
  begin try
215
      let reuse = match Disjunction.CISet.max_elt_opt disjoint_live with
216
        | Some reuse -> reuse
217
        | None -> Disjunction.CISet.choose dead in
219 218
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
220
      Hashtbl.add ctx.policy var.var_id reuse;
221
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
222
      (*Format.eprintf "%s reused by dead %s@." var.var_id reuse.var_id;*)
223
    end
224
      with Not_found ->
225
    begin
226
      Hashtbl.add ctx.policy var.var_id var;
227
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
228
    end
219
      Hashtbl.add ctx.policy var.var_id reuse
220
    with Not_found -> Hashtbl.add ctx.policy var.var_id var
221
  end;
222
  ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated
229 223

  
230 224
let compute_reuse_policy node schedule disjoint g =
231
  let sort = ref schedule in
232 225
  let ctx = { evaluated = Disjunction.CISet.empty;
233
	      dep_graph = g;
234
	      disjoint  = disjoint;
235
	      policy    = Hashtbl.create 23; } in
236
  while !sort <> []
237
  do
238
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);
239
    let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in
240
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:");
241
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads;
242
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@.");
243
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@.");
244
    compute_dependencies heads ctx;
245
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);
246
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_REUSE@.");
247
    List.iter (compute_reuse node ctx heads) heads;
248
    (*compute_evaluated heads ctx;*)
249
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "reuse %s instead of %s@." (Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) heads;
250
    sort := List.tl !sort;
251
  done;
226
              dep_graph = g;
227
              disjoint  = disjoint;
228
              policy    = Hashtbl.create 23; } in
229
  List.iter (fun heads ->
230
      let heads = List.map (fun v -> get_node_var v node) heads in
231
      Log.report ~level:6 (fun fmt ->
232
          Format.(fprintf fmt
233
                    "@[<v>@[<v 2>new context:@,%a@]@,NEW HEADS:%a@,COMPUTE_DEPENDENCIES@,@]"
234
                    pp_context ctx
235
                    (pp_print_list
236
                       ~pp_open_box:pp_open_hbox
237
                       ~pp_sep:pp_print_space
238
                       (fun fmt head ->
239
                          fprintf fmt "%s (%a)"
240
                            head.var_id Printers.pp_node_eq
241
                            (get_node_eq head.var_id node)))
242
                    heads));
243
      compute_dependencies heads ctx;
244
      Log.report ~level:6 (fun fmt ->
245
          Format.fprintf fmt "@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]" pp_context ctx);
246
      List.iter (compute_reuse node ctx heads) heads;
247
      (*compute_evaluated heads ctx;*)
248
      Log.report ~level:6 (fun fmt ->
249
          Format.(fprintf fmt "@[<v>%a@,@]"
250
                    (pp_print_list
251
                       ~pp_open_box:pp_open_vbox0
252
                       (fun fmt head -> fprintf fmt "reuse %s instead of %s"
253
                           (Hashtbl.find ctx.policy head.var_id).var_id head.var_id))
254
                    heads)))
255
    schedule;
252 256
  IdentDepGraph.clear ctx.dep_graph;
253 257
  ctx.policy
254 258

  
src/log.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
let report ?plugin:(modulename="") ?(verbose_level=Options.verbose_level) ~level:level p =
12
let report
13
    ?plugin:(modulename="")
14
    ?(verbose_level=Options.verbose_level)
15
    ~level:level p =
13 16
if !verbose_level >= level then
14
  begin
15
    if modulename="" then
16
      Format.eprintf "%t@?" p
17
    else
18
      Format.eprintf "[%s] @[%t@]@?" modulename p
19
  end
17
  if modulename="" then
18
    Format.eprintf "%t@?" p
19
  else
20
    Format.eprintf "[%s] @[%t@]@?" modulename p
20 21

  
21 22
(* Local Variables: *)
22 23
(* compile-command:"make -C .." *)
src/utils/utils.ml
278 278
  let pp_print_cpar fmt () = pp_print_string fmt ")"
279 279
  let pp_print_obrace fmt () = pp_print_string fmt "{"
280 280
  let pp_print_cbrace fmt () = pp_print_string fmt "}"
281
  let pp_print_opar' fmt () = pp_print_string fmt "( "
282
  let pp_print_cpar' fmt () = pp_print_string fmt " )"
283
  let pp_print_obrace' fmt () = pp_print_string fmt "{ "
284
  let pp_print_cbrace' fmt () = pp_print_string fmt " }"
281 285

  
282 286
  let pp_print_comma fmt () = fprintf fmt ",@ "
283 287
  let pp_print_semicolon fmt () = fprintf fmt ";@ "
......
337 341
      ~pp_cl:pp_print_cbrace
338 342
      ~pp_sep
339 343

  
344
  let pp_print_braced' ?(pp_sep=pp_print_comma) =
345
    pp_print_list
346
      ~pp_op:pp_print_obrace'
347
      ~pp_cl:pp_print_cbrace'
348
      ~pp_sep
340 349
end
341 350

  
342 351
let fprintf_list ?(eol:('a, formatter, unit) format = "") ~sep:sep f fmt l =

Also available in: Unified diff