Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by LĂ©lio Brun 7 months ago

it works

View differences:

src/machine_code.ml
179 179

  
180 180
(* Datastructure updated while visiting equations *)
181 181
type machine_ctx = {
182
  (* memories *)
183
  m: ISet.t;
182 184
  (* Reset instructions *)
183 185
  si: instr_t list;
184 186
  (* Instances *)
......
188 190
  (* Memory pack spec *)
189 191
  mp: mc_formula_t list;
190 192
  (* Transition spec *)
191
  t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;
193
  t: (var_decl list             (* inputs *)
194
      * var_decl list           (* locals *)
195
      * var_decl list           (* outputs *)
196
      * ISet.t                  (* memory footprint *)
197
      * mc_formula_t            (* formula *)
198
     ) list;
192 199
}
193 200

  
194 201
let ctx_init = {
202
  m = ISet.empty;
195 203
  si = [];
196 204
  j = IMap.empty;
197 205
  s = [];
......
225 233
let reset_instance env i r c =
226 234
  match r with
227 235
  | Some r ->
236
    let r = translate_guard env r in
228 237
    let _, inst = control_on_clock env c
229 238
        (mk_conditional
230
           (translate_guard env r)
239
           r
231 240
           [mkinstr (MSetReset i)]
232 241
           [mkinstr (MNoReset i)]) in
233
    [ inst ]
234
  | None -> []
242
    Some r, [ inst ]
243
  | None -> None, []
235 244

  
236 245
let translate_eq env ctx id inputs locals outputs i eq =
237 246
  let translate_expr = translate_expr env in
......
243 252
  let pred_mp ctx a =
244 253
    And [mk_memory_pack ~i:(i-1) id; a] :: ctx.mp in
245 254
  let pred_t ctx a =
246
    (inputs, locals_i, outputs_i,
255
    (inputs, locals_i, outputs_i, ctx.m,
247 256
     Exists
248 257
       (Lustre_live.existential_vars id i eq (locals @ outputs),
249 258
        And [
......
254 263
          a
255 264
        ]))
256 265
    :: ctx.t in
257
  let control_on_clock ck inst spec_mp spec_t =
266
  let control_on_clock ck inst spec_mp spec_t ctx =
258 267
    let fspec, inst = control_on_clock env ck inst in
259 268
    { ctx with
260 269
      s = { inst with
......
272 281
  in
273 282
  let reset_instance = reset_instance env in
274 283
  let mkinstr' = mkinstr ~lustre_eq:eq in
275
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =
276
    control_on_clock ck (mkinstr' instr) spec_mp spec_t in
284
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
285
    control_on_clock ck (mkinstr' instr) in
277 286

  
278 287
  (* Format.eprintf "translate_eq %a with clock %a@." 
279 288
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
......
290 299
        (MStep ([var_x], inst, [c1; c2]))
291 300
        (mk_memory_pack ~inst (node_name td))
292 301
        (mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])
302
        ctx
293 303
    in
294 304
    { ctx with
295 305
      si = mkinstr (MSetReset inst) :: ctx.si;
......
303 313
      (MStateAssign (var_x, e))
304 314
      (mk_state_variable_pack var_x)
305 315
      (mk_state_assign_tr var_x e)
316
      { ctx with m = ISet.add x ctx.m }
306 317

  
307 318
  | [x], Expr_fby (e1, e2) when env.is_local x ->
308 319
    let var_x = env.get_var x in
......
311 322
        (MStateAssign (var_x, e2))
312 323
        (mk_state_variable_pack var_x)
313 324
        (mk_state_assign_tr var_x e2)
325
        { ctx with m = ISet.add x ctx.m }
314 326
    in
315 327
    { ctx with
316 328
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
......
328 340
        el [eq.eq_rhs.expr_clock] in
329 341
    let call_ck = Clock_calculus.compute_root_clock
330 342
        (Clock_predef.ck_tuple env_cks) in
343
    let r, reset_inst = reset_instance inst r call_ck in
331 344
    let ctx = ctl
332 345
        ~ck:call_ck
333 346
        (MStep (var_p, inst, vl))
334 347
        (mk_memory_pack ~inst (node_name node_f))
335
        (mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
348
        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
349
        ctx
336 350
    in
337 351
    (*Clocks.new_var true in
338 352
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
......
341 355
      si = if Stateless.check_node node_f
342 356
        then ctx.si else mkinstr (MSetReset inst) :: ctx.si;
343 357
      j = IMap.add inst call_f ctx.j;
344
      s = (if Stateless.check_node node_f
345
           then []
346
           else reset_instance inst r call_ck)
358
      s = (if Stateless.check_node node_f then [] else reset_inst)
347 359
          @ ctx.s;
348 360
    }
349 361

  
350 362
  | [x], _ ->
351 363
    let var_x = env.get_var x in
352 364
    let instr, spec = translate_act (var_x, eq.eq_rhs) in
353
    control_on_clock eq.eq_rhs.expr_clock instr True spec
365
    control_on_clock eq.eq_rhs.expr_clock instr True spec ctx
354 366

  
355 367
  | _ ->
356 368
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
......
369 381
    [] locals
370 382

  
371 383
let translate_eqs env ctx id inputs locals outputs eqs =
372
  List.fold_right (fun eq (ctx, i) ->
384
  List.fold_left (fun (ctx, i) eq ->
373 385
      let ctx = translate_eq env ctx id inputs locals outputs i eq in
374
      ctx, i - 1)
375
    eqs (ctx, List.length eqs)
386
      ctx, i + 1)
387
    (ctx, 1) eqs
376 388
  |> fst
377 389

  
378 390

  
......
452 464
    tlocals = [];
453 465
    toutputs = [];
454 466
    tformula = True;
467
    tfootprint = ISet.empty
455 468
  }
456 469

  
457 470
let transition_toplevel nd i =
......
461 474
    tinputs = nd.node_inputs;
462 475
    tlocals = [];
463 476
    toutputs = nd.node_outputs;
464
    tformula = ExistsMem (Predicate (ResetCleared nd.node_id),
477
    tformula = ExistsMem (nd.node_id,
478
                          Predicate (ResetCleared nd.node_id),
465 479
                          mk_transition nd.node_id ~i
466 480
                            (vdecls_to_vals (nd.node_inputs))
467 481
                            []
468 482
                            (vdecls_to_vals nd.node_outputs));
483
    tfootprint = ISet.empty;
469 484
  }
470 485

  
471 486
let translate_decl nd sch =
......
519 534
        mpname = nd;
520 535
        mpindex = Some (i + 1);
521 536
        mpformula = red f
522
      }) ctx.mp
537
      }) (List.rev ctx.mp)
523 538
    @ [memory_pack_toplevel nd (List.length ctx.mp)]
524 539
  in
525 540
  let mtransitions =
526 541
    transition_0 nd
527
    :: List.mapi (fun i (tinputs, tlocals, toutputs, f) ->
542
    :: List.mapi (fun i (tinputs, tlocals, toutputs, tfootprint, f) ->
528 543
        {
529 544
          tname = nd;
530 545
          tindex = Some (i + 1);
......
532 547
          tlocals;
533 548
          toutputs;
534 549
          tformula = red f;
535
        }) ctx.t
550
          tfootprint
551
        }) (List.rev ctx.t)
536 552
    @ [transition_toplevel nd (List.length ctx.t)]
537 553
  in
538 554
  let clear_reset = mkinstr ~instr_spec:[
......
546 562
    mmemory = VSet.elements mems;
547 563
    mcalls = mmap;
548 564
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
549
    minit = ctx.si;
550
    mconst = ctx0_s;
565
    minit = List.rev ctx.si;
566
    mconst = List.rev ctx0_s;
551 567
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
552 568
    mstep = {
553 569
      step_inputs = nd.node_inputs;
......
562 578
                       common branches are not merged while they are in C or Java
563 579
                       backends. *)
564 580
                    (if !Backends.join_guards then
565
                       join_guards_list ctx.s
581
                       join_guards_list (List.rev ctx.s)
566 582
                     else
567
                       ctx.s);
583
                       List.rev ctx.s);
568 584
      step_asserts = List.map (translate_expr env) nd_node_asserts;
569 585
    };
570 586

  

Also available in: Unified diff