Project

General

Profile

« Previous | Next » 

Revision 15c3e4e7

Added by LĂ©lio Brun almost 4 years 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),

Also available in: Unified diff