Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

.ocamlformat
3 3
wrap-comments=true
4 4
cases-exp-indent=2
5 5
break-cases=nested
6
break-fun-decl=wrap
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
src/machine_code.ml
137 137
let rec translate_act env (y, expr) =
138 138
  let translate_act = translate_act env in
139 139
  let translate_guard = translate_guard env in
140
  (* let translate_ident = translate_ident env in *)
141 140
  let translate_expr = translate_expr env in
142 141
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in
143 142
  match expr.expr_desc with
......
193 192
    * var_decl list
194 193
    (* outputs *)
195 194
    * ISet.t (* memory footprint *)
195
    * ident IMap.t
196
    (* memory instances footprint *)
196 197
    * mc_formula_t)
197 198
    (* formula *)
198 199
    list;
......
250 251
      locals_i,
251 252
      outputs_i,
252 253
      ctx.m,
254
      IMap.map (fun (td, _) -> node_name td) ctx.j,
253 255
      Exists
254 256
        ( Lustre_live.existential_vars id i eq (locals @ outputs),
255 257
          And
......
303 305
        (MStep ([ var_x ], inst, [ c1; c2 ]))
304 306
        (mk_memory_pack ~inst (node_name td))
305 307
        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
306
        ctx
308
        { ctx with j = IMap.add inst (td, []) ctx.j }
307 309
    in
308
    {
309
      ctx with
310
      si = mkinstr (MSetReset inst) :: ctx.si;
311
      j = IMap.add inst (td, []) ctx.j;
312
    }
310
    { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
313 311
  | [ x ], Expr_pre e when env.is_local x ->
314 312
    let var_x = env.get_var x in
315 313
    let e = translate_expr e in
......
354 352
        (MStep (var_p, inst, vl))
355 353
        (mk_memory_pack ~inst (node_name node_f))
356 354
        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
357
        ctx
355
        {
356
          ctx with
357
          j = IMap.add inst call_f ctx.j;
358
          s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
359
        }
358 360
    in
359 361
    (*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)
360 362
      eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:
......
365 367
      si =
366 368
        (if Stateless.check_node node_f then ctx.si
367 369
        else mkinstr (MSetReset inst) :: ctx.si);
368
      j = IMap.add inst call_f ctx.j;
369
      s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
370 370
    }
371 371
  | [ x ], _ ->
372 372
    let var_x = env.get_var x in
......
476 476
    tlocals = [];
477 477
    toutputs = [];
478 478
    tformula = True;
479
    tfootprint = ISet.empty;
479
    tmem_footprint = ISet.empty;
480
    tinst_footprint = IMap.empty;
480 481
  }
481 482

  
482 483
let transition_toplevel nd i =
......
495 496
    tformula =
496 497
      (if fst (get_stateless_status_node nd) then tr
497 498
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
498
    tfootprint = ISet.empty;
499
    tmem_footprint = ISet.empty;
500
    tinst_footprint = IMap.empty;
499 501
  }
500 502

  
501 503
let translate_decl nd sch =
......
562 564
    transition_0 nd
563 565
    ::
564 566
    List.mapi
565
      (fun i (tinputs, tlocals, toutputs, tfootprint, f) ->
567
      (fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) ->
566 568
        {
567 569
          tname = nd;
568 570
          tindex = Some (i + 1);
......
570 572
          tlocals;
571 573
          toutputs;
572 574
          tformula = red f;
573
          tfootprint;
575
          tmem_footprint;
576
          tinst_footprint;
574 577
        })
575 578
      (List.rev ctx.t)
576 579
    @ [ transition_toplevel nd (List.length ctx.t) ]
src/machine_code_common.ml
58 58
     fun fmt e -> pp_expr m fmt e
59 59
    in
60 60
    match p with
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
62 62
      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
63 63
        (pp_print_option
64 64
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
......
321 321
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
322 322

  
323 323
let mk_conditional ?lustre_eq c t e =
324
  mkinstr ?lustre_eq
325
    (* (Ternary (Val c,
326
     *           And (List.map get_instr_spec t),
327
     *           And (List.map get_instr_spec e))) *)
328
    (MBranch (c, [ tag_true, t; tag_false, e ]))
329

  
330
let mk_branch ?lustre_eq c br =
331
  mkinstr ?lustre_eq
332
    (* (And (List.map (fun (l, instrs) ->
333
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
334
     *      br)) *)
335
    (MBranch (c, br))
324
  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
325

  
326
let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
336 327

  
337 328
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
338 329

  
339
let mk_assign ?lustre_eq x v =
340
  mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))
330
let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
341 331

  
342 332
let arrow_machine =
343 333
  let state = "_first" in
344
  let var_state =
345
    dummy_var_decl state Type_predef.type_bool
346
    (* (Types.new_ty Types.Tbool) *)
347
  in
334
  let var_state = dummy_var_decl state Type_predef.type_bool in
348 335
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
349 336
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
350 337
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
src/spec_common.ml
1 1
open Spec_types
2
open Utils
2 3

  
3 4
(* a small reduction engine *)
4 5
let is_true = function True -> true | _ -> false
......
73 74
    f
74 75

  
75 76
(* smart constructors *)
76
(* let mk_condition x l =
77
 *   if l = tag_true then Ternary (Val x, True, False)
78
 *   else if l = tag_false then Ternary (Val x, False, True)
79
 *   else Equal (Val x, Tag l) *)
80 77

  
81 78
let vals vs = List.map (fun v -> Val v) vs
82 79

  
83 80
let mk_pred_call pred = Predicate pred
84 81

  
85
(* let mk_clocked_on id =
86
 *   mk_pred_call (Clocked_on id) *)
87

  
88
let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
89
    outputs =
82
let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id
83
    inputs locals outputs =
90 84
  let tr =
91 85
    mk_pred_call
92 86
      (Transition
......
97 91
           vals locals,
98 92
           vals outputs,
99 93
           (match r with Some _ -> true | None -> false),
100
           mems ))
94
           mems,
95
           insts ))
101 96
  in
102 97
  match r, inst with
103 98
  | Some r, Some inst ->
......
113 108

  
114 109
let mk_conditional_tr v t f = Ternary (Val v, t, f)
115 110

  
116
let mk_branch_tr x hl =
117
  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
111
let mk_branch_tr x =
112
  let open Lustre_types in
113
  function
114
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_true && h2 = tag_false ->
115
    Ternary (Var x, spec1, spec2)
116
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
117
    Ternary (Var x, spec2, spec1)
118
  | hl ->
119
    And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
118 120

  
119 121
let mk_assign_tr x v = Equal (Var x, Val v)
src/spec_types.ml
39 39
      (* outputs *)
40 40
      * bool (* reset *)
41 41
      * Utils.ISet.t (* memory footprint *)
42
      * ident Utils.IMap.t
43
      (* memory instances footprint *)
42 44
      -> 'a predicate_t
43 45
  | Reset of ident * ident * 'a
44 46
  | MemoryPack of ident * ident option * int option
......
80 82
  tlocals : var_decl list;
81 83
  toutputs : var_decl list;
82 84
  tformula : 'a formula_t;
83
  tfootprint : Utils.ISet.t;
85
  tmem_footprint : Utils.ISet.t;
86
  tinst_footprint : ident Utils.IMap.t;
84 87
}
src/utils/env.ml
35 35
    x y
36 36

  
37 37
let pp_env pp_fun fmt env =
38
  let lid, lty = list_of_imap env in
39
  let l' = List.combine lid lty in
38
  let l' = IMap.bindings env in
40 39
  let pp_fun fmt (id, value) = Format.fprintf fmt "%s |-> %a" id pp_fun value in
41 40
  Format.fprintf fmt "{ @[<v 2>%a@] }" (fprintf_list ~sep:"@," pp_fun) l'
42 41

  
src/utils/utils.ml
41 41
module IMap = struct
42 42
  include Map.Make (IdentModule)
43 43

  
44
  let union_l m1 m2 =
44
  let diff m1 m2 =
45 45
    merge
46 46
      (fun _ o1 o2 ->
47 47
        match o1, o2 with
48
        | None, None ->
49
          None
50
        | Some _, _ ->
51
          o1
52
        | _, Some _ ->
53
          o2)
48
        | Some v1, Some v2 ->
49
          if v1 = v2 then None else o1
50
        | _ ->
51
          o1)
54 52
      m1 m2
53

  
54
  let of_list l = List.fold_left (fun m (x, v) -> add x v m) empty l
55 55
end
56 56

  
57 57
module ISet = Set.Make (IdentModule)
......
123 123
    | t :: q ->
124 124
      if p t then t :: filter_upto p (n - 1) q else filter_upto p n q
125 125

  
126
(* Warning: bad complexity *)
127
let list_of_imap imap =
128
  IMap.fold (fun i v (il, vl) -> i :: il, v :: vl) imap ([], [])
129

  
130 126
(** [gcd a b] returns the greatest common divisor of [a] and [b]. *)
131 127
let rec gcd a b = if b = 0 then a else gcd b (a mod b)
132 128

  

Also available in: Unified diff