Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

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) ]

Also available in: Unified diff