Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

src/backends/C/c_backend_spec.ml
8 8
(*  version 2.1.                                                    *)
9 9
(*                                                                  *)
10 10
(********************************************************************)
11

  
12
open Utils.Format
11
open Utils
12
open Format
13 13
open Lustre_types
14 14
open Machine_code_types
15 15
open C_backend_common
......
299 299

  
300 300
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
301 301

  
302
let pp_functional_update mems fmt mem =
303
  let rec aux fmt mems =
304
    match mems with
302
let pp_functional_update mems insts fmt mem =
303
  let rec aux fmt = function
305 304
    | [] ->
306 305
      pp_print_string fmt mem
307
    | x :: mems ->
308
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
306
    | (x, is_mem) :: fields ->
307
      fprintf fmt "{ @[<hov>%a@ \\with .%s%s = %s@] }" aux fields
308
        (if is_mem then "_reg." else "")
309
        x x
309 310
  in
310 311
  aux fmt
311
    (* if Utils.ISet.is_empty mems then
312
     *   pp_print_string fmt mem
313
     *     else
314
     *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
315
     *     mem
316
     *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
317
     *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
318
    (Utils.ISet.elements mems)
312
    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
313
    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
319 314

  
320 315
module PrintSpec = struct
321 316
  type mode =
......
365 360
     fun ?output fmt e -> pp_expr ?output m mem_out fmt e
366 361
    in
367 362
    match p with
368
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
363
    | Transition (f, inst, i, inputs, locals, outputs, r, mems, insts) ->
369 364
      let pp_mem_in, pp_mem_out =
370 365
        match inst with
371 366
        | None ->
372 367
          ( pp_print_string,
373
            if mem_update then pp_functional_update mems else pp_print_string )
368
            if mem_update then pp_functional_update mems insts
369
            else pp_print_string )
374 370
        | Some inst ->
375 371
          ( (fun fmt mem_in ->
376 372
              if r then pp_print_string fmt mem_in
......
422 418
      eprintf "Internal error: arrow not found";
423 419
      raise Not_found
424 420

  
425
  let pp_spec mode m fmt f =
421
  let pp_spec mode m =
426 422
    let rec pp_spec mode fmt f =
427 423
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
428 424
        let self = mk_self m in
......
504 500
          fmt
505 501
          ((f, mk_mem_reset m), (rc, tr))
506 502
    in
507
    match mode with
508
    | TransitionFootprintMode ->
509
      let mem_in = mk_mem_in m in
510
      let mem_out = mk_mem_out m in
511
      pp_forall
512
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
513
        (pp_spec mode) fmt
514
        ((m.mname.node_id, [ mem_in; mem_out ]), f)
515
    | _ ->
516
      pp_spec mode fmt f
503
    pp_spec mode
517 504
end
518 505

  
519 506
let pp_predicate pp_l pp_r fmt (l, r) =
......
583 570
    t.tindex
584 571

  
585 572
let pp_transition_footprint_lemma m fmt t =
586
  let open Utils.ISet in
587 573
  let name = t.tname.node_id in
574
  let mem_in = mk_mem_in m in
575
  let mem_out = mk_mem_out m in
588 576
  let mems =
589
    diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint
577
    ISet.(
578
      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
579
  in
580
  let insts =
581
    IMap.(
582
      diff
583
        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
584
        t.tinst_footprint)
590 585
  in
591 586
  let memories =
592 587
    List.map
593 588
      (fun v -> { v with var_type = { v.var_type with tid = -1 } })
594
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
589
      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
590
  in
591
  let mems_empty = ISet.is_empty mems in
592
  let insts_empty = IMap.is_empty insts in
593
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
594
  let tr ?mems ?insts () =
595
    Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
596
      (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
597
      (vdecls_to_vals t.toutputs)
595 598
  in
596
  if not (is_empty mems) then
599
  if not (mems_empty && insts_empty) then
597 600
    pp_acsl
598 601
      (pp_lemma pp_transition_footprint
599
         (PrintSpec.pp_spec TransitionFootprintMode m))
602
         (pp_forall
603
            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
604
            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
605
             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
606
               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
607
                else pp_forall (pp_locals m))
608
                  (PrintSpec.pp_spec TransitionFootprintMode m)))))
600 609
      fmt
601 610
      ( t,
602
        Forall
603
          ( memories @ t.tinputs @ t.tlocals @ t.toutputs,
604
            Imply
605
              ( Spec_common.mk_transition ?i:t.tindex name
606
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
607
                  (vdecls_to_vals t.toutputs),
608
                Spec_common.mk_transition ~mems ?i:t.tindex name
609
                  (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
610
                  (vdecls_to_vals t.toutputs) ) ) )
611
        ( (m.mname.node_id, [ mem_in; mem_out ]),
612
          ( instances,
613
            ( memories,
614
              Forall
615
                ( t.tinputs @ t.tlocals @ t.toutputs,
616
                  Imply (tr (), tr ~mems ~insts ()) ) ) ) ) )
611 617

  
612 618
let pp_transition_footprint_lemmas fmt m =
613 619
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0

Also available in: Unified diff