Revision 15c3e4e7
Added by LĂ©lio Brun almost 4 years ago
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
generic ACSL spec generation