Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by Lélio Brun 7 months ago

it works

View differences:

dune
21 21
   include/arrow.c
22 22
   include/arrow.h
23 23
   include/arrow_spec.h
24
   include/arrow_spec.c
24 25
   include/arrow.cpp
25 26
   include/arrow.hpp
26 27
   include/io_frontend.c
include/arrow_spec.h
44 44
                             : (mem_out._reg._first == mem_in._reg._first));
45 45
*/
46 46

  
47
/*@ predicate _arrow_ghost(struct _arrow_mem_ghost mem,
48
                           struct _arrow_mem *self) =
47
/*@ predicate _arrow_pack(struct _arrow_mem_ghost mem,
48
                          struct _arrow_mem *self) =
49 49
      mem._reg._first == self->_reg._first;
50 50
*/
51 51

  
52 52
/*@
53 53
  requires \separated(mem, self);
54
  requires _arrow_ghost(*mem, self);
55
  ensures  _arrow_ghost(*mem, self);
54
  requires _arrow_pack(*mem, self);
55
  ensures  _arrow_pack(*mem, self);
56 56
  ensures \result == \old(self->_reg._first);
57 57
  ensures self->_reg._first == 0;
58 58
  ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);
src/backends/C/c_backend_common.ml
299 299
  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
300 300

  
301 301
let reset_flag_name = "_reset"
302
let pp_reset_flag ?(indirect=true) fmt self =
303
  fprintf fmt "%s%s%s" self (if indirect then "->" else ".") reset_flag_name
302
let pp_reset_flag ?(indirect=true) pp_stru fmt stru =
303
  fprintf fmt "%a%s%s"
304
    pp_stru stru
305
    (if indirect then "->" else ".")
306
    reset_flag_name
307
let pp_reset_flag' ?indirect fmt =
308
  pp_reset_flag ?indirect pp_print_string fmt
304 309

  
305 310
let pp_reset_assign self fmt b =
306 311
  fprintf fmt "%a = %i;"
307
    (pp_reset_flag ~indirect:true) self (if b then 1 else 0)
312
    (pp_reset_flag' ~indirect:true) self (if b then 1 else 0)
308 313

  
309 314
(* Prints a value expression [v], with internal function calls only.
310 315
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
......
337 342
  | Fun (n, vl) ->
338 343
    pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
339 344
  | ResetFlag ->
340
    pp_reset_flag fmt self
345
    pp_reset_flag' fmt self
341 346

  
342 347

  
343 348
(* Access to the value of a variable:
......
346 351
     despite its scalar Lustre type)
347 352
   - moreover, dereference memory array variables.
348 353
*)
349
let pp_c_var_read m fmt id =
354
let pp_c_var_read ?(test_output=true) m fmt id =
350 355
  (* mpfr_t is a static array, not treated as general arrays *)
351 356
  if Types.is_address_type id.var_type
352 357
  then
......
355 360
    then fprintf fmt "(*%s)" id.var_id
356 361
    else fprintf fmt "%s" id.var_id
357 362
  else
358
    if Machine_code_common.is_output m id
363
    if test_output && Machine_code_common.is_output m id
359 364
    then fprintf fmt "*%s" id.var_id
360 365
    else fprintf fmt "%s" id.var_id
361 366

  
......
616 621
  | _, Cst cst ->
617 622
    pp_c_const_suffix var_type fmt cst
618 623
  | _, ResetFlag ->
619
    pp_reset_flag fmt self
624
    pp_reset_flag' fmt self
620 625
  | _, _ ->
621 626
    eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
622 627
      Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
src/backends/C/c_backend_header.ml
24 24
module type MODIFIERS_HDR = sig
25 25
  module GhostProto: MODIFIERS_GHOST_PROTO
26 26
  val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
27
  val pp_import_standard_spec: formatter -> unit -> unit
27
  val pp_import_arrow: formatter -> unit -> unit
28 28
end
29 29

  
30 30
module EmptyMod = struct
31 31
  module GhostProto = EmptyGhostProto
32 32
  let print_machine_decl_prefix = fun _ _ -> ()
33
  let pp_import_standard_spec _ _ = ()
33
  let pp_import_arrow fmt () =
34
    fprintf fmt "#include \"%s/arrow.h%s\""
35
      (Arrow.arrow_top_decl ()).top_decl_owner
36
      (if !Options.cpp then "pp" else "")
34 37
end
35 38

  
36 39
module Main = functor (Mod: MODIFIERS_HDR) -> struct
......
42 45
    fprintf fmt
43 46
      "#include <stdint.h>@,\
44 47
       %a\
45
       #include \"%s/arrow.h%s\"\
46 48
       %a"
47 49
      (if !Options.mpfr then
48 50
         pp_print_endcut "#include <mpfr.h>"
49 51
       else pp_print_nothing) ()
50
      (Arrow.arrow_top_decl ()).top_decl_owner
51
      (if !Options.cpp then "pp" else "")
52
      Mod.pp_import_standard_spec ()
52
      Mod.pp_import_arrow ()
53 53

  
54 54
  let rec print_static_val pp_var fmt v =
55 55
    match v.value_desc with
src/backends/C/c_backend_spec.ml
16 16
open C_backend_common
17 17
open Corelang
18 18
open Spec_types
19
open Spec_common
20 19
open Machine_code_common
21 20

  
22 21
(**************************************************************************)
......
34 33
    "_Bool"
35 34
  else if Types.is_int_type t_desc then
36 35
    (* !Options.int_type *)
37
    "integer"
36
    if t_desc.tid = -1 then "int" else "integer"
38 37
  else if Types.is_real_type t_desc then
39 38
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
40 39
  else
......
91 90

  
92 91
let pp_access' = pp_access pp_print_string pp_print_string
93 92

  
94
let pp_inst self fmt (name, _) =
95
  pp_indirect' fmt (self, name)
96

  
97 93
let pp_var_decl fmt v =
98 94
  pp_print_string fmt v.var_id
99 95

  
......
251 247

  
252 248
let pp_initialization' = pp_initialization pp_print_string
253 249

  
250
let pp_local m =
251
  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m
252

  
254 253
let pp_locals m =
255 254
  pp_comma_list
256
    ~pp_open_box:pp_open_hbox
257
    (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
255
    ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0)
256
    (pp_local m)
258 257

  
259 258
let pp_ptr_decl fmt v =
260 259
  pp_ptr fmt v.var_id
......
272 271
  let depth = expansion_depth value in
273 272
  let loop_vars = mk_loop_variables m var_type depth in
274 273
  let reordered_loop_vars = reorder_loop_variables loop_vars in
275
  let rec aux typ fmt vars =
274
  let aux typ fmt vars =
276 275
    match vars with
277 276
    | [] ->
278 277
      pp_basic_assign_spec
......
298 297
    aux var_type fmt reordered_loop_vars;
299 298
  end
300 299

  
301
let pp_c_var_read m fmt id =
302
  (* mpfr_t is a static array, not treated as general arrays *)
303
  if Types.is_address_type id.var_type
304
  then
305
    if is_memory m id
306
    && not (Types.is_real_type id.var_type && !Options.mpfr)
307
    then fprintf fmt "(*%s)" id.var_id
308
    else fprintf fmt "%s" id.var_id
309
  else
310
    fprintf fmt "%s" id.var_id
311

  
312 300
let pp_nothing fmt () =
313 301
  pp_print_string fmt "\\nothing"
314 302

  
......
334 322
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
335 323
    name
336 324
    (pp_print_option pp_print_int) i
337
    (fun fmt -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in)
338
    (pp_comma_list pp_input) inputs
325
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
326
    (pp_comma_list
327
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
328
       pp_input) inputs
339 329
    (pp_print_option (fun fmt _ ->
340 330
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
341 331
    i
......
364 354

  
365 355
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
366 356

  
357
let pp_functional_update mems fmt mem =
358
  let rec aux fmt mems =
359
    match mems with
360
    | [] -> pp_print_string fmt mem
361
    | x :: mems ->
362
      fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
363
  in
364
  aux fmt
365
  (* if Utils.ISet.is_empty mems then
366
   *   pp_print_string fmt mem
367
   *     else
368
   *   fprintf fmt "{ %s @[<hov>\\with %a@] }"
369
   *     mem
370
   *     (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
371
   *        (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
372
      (Utils.ISet.elements mems)
373

  
367 374
module PrintSpec = struct
368 375

  
369
  let pp_reg pp_mem fmt = function
376
  type mode =
377
    | MemoryPackMode
378
    | TransitionMode
379
    | TransitionFootprintMode
380
    | ResetIn
381
    | ResetOut
382
    | InstrMode of ident
383

  
384
  let pp_reg mem fmt = function
370 385
    | ResetFlag ->
371
      fprintf fmt "%t%s" pp_mem reset_flag_name
386
      fprintf fmt "%s.%s" mem reset_flag_name
372 387
    | StateVar x ->
373
      fprintf fmt "%t%a" pp_mem pp_var_decl x
388
      fprintf fmt "%s.%a" mem pp_var_decl x
374 389

  
375 390
  let pp_expr:
376
    type a. machine_t -> (formatter -> unit) -> formatter -> (value_t, a) expression_t -> unit =
377
    fun m pp_mem fmt -> function
378
    | Val v -> pp_val m fmt v
391
    type a. ?output:bool -> machine_t -> ident -> formatter
392
    -> (value_t, a) expression_t -> unit =
393
    fun ?(output=false) m mem fmt -> function
394
    | Val v -> pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
379 395
    | Tag t -> pp_print_string fmt t
380 396
    | Var v -> pp_var_decl fmt v
381
    | Memory r -> pp_reg pp_mem fmt r
397
    | Memory r -> pp_reg mem fmt r
382 398

  
383
  let pp_predicate m mem_in mem_in' mem_out mem_out' fmt p =
384
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
385
      fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
399
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
400
    let output, mem_update = match mode with
401
      | InstrMode _ -> true, false
402
      | TransitionFootprintMode -> false, true
403
      | _ -> false, false
404
    in
405
    let pp_expr:
406
      type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
407
      fun ?output fmt e -> pp_expr ?output m mem_out fmt e
386 408
    in
387 409
    match p with
388
    | Transition (f, inst, i, inputs, locals, outputs) ->
410
    | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
389 411
      let pp_mem_in, pp_mem_out = match inst with
390 412
        | None ->
391
          pp_print_string, pp_print_string
413
          pp_print_string,
414
          if mem_update then pp_functional_update mems else pp_print_string
392 415
        | Some inst ->
393
          (fun fmt mem_in -> pp_access' fmt (mem_in, inst)),
416
          (fun fmt mem_in ->
417
             if r then pp_print_string fmt mem_in
418
             else pp_access' fmt (mem_in, inst)),
394 419
          (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
395 420
      in
396
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr pp_expr fmt
421
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output)
422
        fmt
397 423
        (f, inputs, locals, outputs, mem_in', mem_out')
424
    | Reset (_f, inst, r) ->
425
      pp_ite
426
        (pp_c_val m mem_in (pp_c_var_read m))
427
        (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
428
        (pp_equal pp_print_string pp_access')
429
        fmt
430
        (r, (mem_out, 1), (mem_out, (mem_in, inst)))
398 431
    | MemoryPack (f, inst, i) ->
399 432
      let pp_mem, pp_self = match inst with
400 433
        | None ->
......
418 451
    | Memory (StateVar v) -> vdecl_to_val v
419 452
    | Memory ResetFlag -> vdecl_to_val reset_flag
420 453

  
421
  type mode =
422
    | MemoryPackMode
423
    | TransitionMode
424
    | ResetIn
425
    | ResetOut
426
    | InstrMode of ident
427

  
428 454
  let find_arrow m =
429 455
    try
430 456
      List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
431 457
      |> fst
432 458
    with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
433 459

  
434
  let pp_spec mode m =
460
  let pp_spec mode m fmt f =
435 461
    let rec pp_spec mode fmt f =
436 462
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
437 463
        let self = mk_self m in
......
444 470
          self, self, true, mem, mem, false
445 471
        | TransitionMode ->
446 472
          mem_in, mem_in, false, mem_out, mem_out, false
473
        | TransitionFootprintMode ->
474
          mem_in, mem_in, false, mem_out, mem_out, false
447 475
        | ResetIn ->
448
          mem_in, mem_in, false, mem_reset, mem_reset, false
449
        | ResetOut ->
450 476
          mem_reset, mem_reset, false, mem_out, mem_out, false
477
        | ResetOut ->
478
          mem_in, mem_in, false, mem_reset, mem_reset, false
451 479
        | InstrMode self ->
452 480
          let mem = "*" ^ mem in
453 481
          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
......
455 483
          mem, mem, false
456 484
      in
457 485
      let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
458
        fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
486
        fun fmt e -> pp_expr m mem_out fmt e
459 487
      in
460 488
      let pp_spec' = pp_spec mode in
461 489
      match f with
......
465 493
        pp_false fmt ()
466 494
      | Equal (a, b) ->
467 495
        pp_assign_spec m
468
          mem_out (pp_c_var_read m) indirect_l
469
          mem_in (pp_c_var_read m) indirect_r
496
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
497
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
470 498
          fmt
471 499
          (type_of_l_value a, val_of_expr a, val_of_expr b)
472 500
      | And fs ->
......
482 510
      | Ternary (e, a, b) ->
483 511
        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
484 512
      | Predicate p ->
485
        pp_predicate m mem_in mem_in' mem_out mem_out' fmt p
513
        pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
486 514
      | StateVarPack ResetFlag ->
487 515
        let r = vdecl_to_val reset_flag in
488 516
        pp_assign_spec m
489
          mem_out (pp_c_var_read m) indirect_l
490
          mem_in (pp_c_var_read m) indirect_r
517
          mem_out (pp_c_var_read ~test_output:false m) indirect_l
518
          mem_in (pp_c_var_read ~test_output:false m) indirect_r
491 519
          fmt
492 520
          (Type_predef.type_bool, r, r)
493 521
      | StateVarPack (StateVar v) ->
......
496 524
        pp_par (pp_implies
497 525
                  (pp_not (pp_initialization pp_access'))
498 526
                  (pp_assign_spec m
499
                     mem_out (pp_c_var_read m) indirect_l
500
                     mem_in (pp_c_var_read m) indirect_r))
527
                     mem_out (pp_c_var_read ~test_output:false m) indirect_l
528
                     mem_in (pp_c_var_read ~test_output:false m) indirect_r))
501 529
          fmt
502 530
          ((Arrow.arrow_id, (mem_out, inst)),
503 531
           (v.var_type, v', v'))
504
      | ExistsMem (rc, tr) ->
532
      | ExistsMem (f, rc, tr) ->
505 533
        pp_exists
506 534
          (pp_machine_decl' ~ghost:true)
507
          (pp_and (pp_spec ResetIn) (pp_spec ResetOut))
535
          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))
508 536
          fmt
509
          ((m.mname.node_id, mk_mem_reset m),
537
          ((f, mk_mem_reset m),
510 538
           (rc, tr))
511
          (* fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec f *)
512 539
    in
513
    pp_spec mode
540
    match mode with
541
    | TransitionFootprintMode ->
542
      let mem_in = mk_mem_in m in
543
      let mem_out = mk_mem_out m in
544
      pp_forall
545
        (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
546
        (pp_spec mode)
547
        fmt ((m.mname.node_id, [mem_in; mem_out]), f)
548
    | _ ->
549
      pp_spec mode fmt f
514 550

  
515 551
end
516 552

  
......
519 555
    pp_l l
520 556
    pp_r r
521 557

  
522
let print_machine_valid_predicate fmt m =
558
let pp_lemma pp_l pp_r fmt (l, r) =
559
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]"
560
    pp_l l
561
    pp_r r
562

  
563
let pp_mem_valid_def fmt m =
523 564
  if not (fst (get_stateless_status m)) then
524 565
    let name = m.mname.node_id in
525 566
    let self = mk_self m in
......
527 568
      (pp_predicate
528 569
         (pp_mem_valid (pp_machine_decl pp_ptr))
529 570
         (pp_and
530
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
531
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
571
            (pp_and_l (fun fmt (inst, (td, _)) ->
572
                 if Arrow.td_is_arrow td then
573
                   pp_valid pp_indirect' fmt [self, inst]
574
                 else
575
                   pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))
532 576
            (pp_valid pp_print_string)))
533 577
      fmt
534 578
      ((name, (name, self)),
535 579
       (m.minstances, [self]))
536 580

  
537

  
538 581
let pp_memory_pack_def m fmt mp =
539 582
  let name = mp.mpname.node_id in
540 583
  let self = mk_self m in
......
567 610
    (pp_predicate
568 611
       (pp_transition m
569 612
          (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
570
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
571
          (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
613
          (pp_local m)
614
          (pp_local m))
572 615
       (PrintSpec.pp_spec TransitionMode m))
573 616
    fmt
574 617
    ((t, (name, mem_in), (name, mem_out)),
575 618
     t.tformula)
576 619

  
577
(* let print_trans_simulation dependencies m fmt (i, instr) =
578
 *   let mem_in = mk_mem_in m in
579
 *   let mem_out = mk_mem_out m in
580
 *   let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
581
 *                    (live_i m (i+1))) in
582
 *   (\* XXX *\)
583
 *   (\* printf "%d : %a\n%d : %a\nocc: %a\n\n"
584
 *    *   i
585
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
586
 *    *   (i+1)
587
 *    *   (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
588
 *    *   (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *\)
589
 *   let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
590
 *   let pred pp v =
591
 *     let vars = VDSet.(union (of_list m.mstep.step_locals)
592
 *                         (of_list m.mstep.step_outputs)) in
593
 *     let locals = VDSet.(inter vars d |> elements) in
594
 *     if locals = []
595
 *     then pp_and prev_trans pp fmt ((), v)
596
 *     else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
597
 *   in
598
 *   let rec aux fmt instr = match instr.instr_desc with
599
 *     | MLocalAssign (x, v)
600
 *     | MStateAssign (x, v) ->
601
 *       pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
602
 *         (x.var_type, mk_val (Var x) x.var_type, v)
603
 *     | MStep ([i0], i, vl)
604
 *       when Basic_library.is_value_internal_fun
605
 *           (mk_val (Fun (i, vl)) i0.var_type)  ->
606
 *       pp_true fmt ()
607
 *     | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
608
 *       pp_true fmt ()
609
 *     | MStep ([_], i, _) when has_c_prototype i dependencies ->
610
 *       pp_true fmt ()
611
 *     | MStep (xs, i, ys) ->
612
 *       begin try
613
 *           let n, _ = List.assoc i m.minstances in
614
 *           pp_mem_trans_aux
615
 *             (fst (get_stateless_status_top_decl n))
616
 *             pp_access' pp_access'
617
 *             (pp_c_val m mem_in (pp_c_var_read m))
618
 *             pp_var_decl
619
 *             fmt
620
 *             (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
621
 *         with Not_found -> pp_true fmt ()
622
 *       end
623
 *     | MReset i ->
624
 *       begin try
625
 *           let n, _ = List.assoc i m.minstances in
626
 *           pp_mem_init' fmt (node_name n, mem_out)
627
 *         with Not_found -> pp_true fmt ()
628
 *       end
629
 *     | MBranch (v, brs) ->
630
 *       if let t = fst (List.hd brs) in t = tag_true || t = tag_false
631
 *       then (\* boolean case *\)
632
 *         pp_ite (pp_c_val m mem_in (pp_c_var_read m))
633
 *           (fun fmt () ->
634
 *              match List.assoc tag_true brs with
635
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
636
 *              | []
637
 *              | exception Not_found -> pp_true fmt ())
638
 *           (fun fmt () ->
639
 *              match List.assoc tag_false brs with
640
 *              | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
641
 *              | []
642
 *              | exception Not_found -> pp_true fmt ())
643
 *           fmt (v, (), ())
644
 *       else (\* enum type case *\)
645
 *       pp_and_l (fun fmt (l, instrs) ->
646
 *             let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
647
 *             pp_paren (pp_implies
648
 *                         (pp_equal pp_val pp_c_tag)
649
 *                         (pp_and_l aux))
650
 *               fmt
651
 *               ((v, l), instrs))
652
 *         fmt brs
653
 *     | _ -> pp_true fmt ()
654
 *   in
655
 *   pred aux instr *)
656

  
657
(* let print_machine_trans_simulation dependencies m fmt i instr =
658
 *   print_machine_trans_simulation_aux m
659
 *     (print_trans_simulation dependencies m)
660
 *     ~i:(i+1)
661
 *     fmt (i, instr) *)
662

  
663 620
let pp_transition_defs fmt m =
664
  (* set_live_of m; *)
665
  (* let i = List.length m.mstep.step_instrs in *)
666
  (* let mem_in = mk_mem_in m in
667
   * let mem_out = mk_mem_out m in *)
668
  (* let last_trans fmt () =
669
   *   let locals = VDSet.(inter
670
   *                         (of_list m.mstep.step_locals)
671
   *                         (live_i m i)
672
   *                       |> elements) in
673
   *   if locals = []
674
   *   then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
675
   *   else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
676
   *       (locals, (m, mem_in, mem_out))
677
   * in *)
678
  fprintf fmt "%a"
679
    (pp_print_list
680
       ~pp_epilogue:pp_print_cut
681
       ~pp_open_box:pp_open_vbox0
682
       (pp_transition_def m)) m.mspec.mtransitions
683

  
684
let print_machine_init_predicate fmt m =
621
  pp_print_list
622
    ~pp_epilogue:pp_print_cut
623
    ~pp_open_box:pp_open_vbox0
624
    (pp_transition_def m) fmt m.mspec.mtransitions
625

  
626
let pp_transition_footprint fmt t =
627
  fprintf fmt "%s_transition%a_footprint"
628
    t.tname.node_id
629
    (pp_print_option pp_print_int) t.tindex
630

  
631
let pp_transition_footprint_lemma m fmt t =
632
  let open Utils.ISet in
633
  let name = t.tname.node_id in
634
  let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in
635
  let memories = List.map (fun v ->
636
      { v with var_type = { v.var_type with tid = -1 }})
637
      (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
638
  in
639
  if not (is_empty mems) then
640
    pp_acsl
641
      (pp_lemma
642
         pp_transition_footprint
643
         (PrintSpec.pp_spec TransitionFootprintMode m))
644
      fmt
645
      (t,
646
       Forall (
647
         memories @ t.tinputs @ t.tlocals @ t.toutputs,
648
         Imply (Spec_common.mk_transition ?i:t.tindex name
649
                  (vdecls_to_vals t.tinputs)
650
                  (vdecls_to_vals t.tlocals)
651
                  (vdecls_to_vals t.toutputs),
652
                Spec_common.mk_transition ~mems ?i:t.tindex name
653
                  (vdecls_to_vals t.tinputs)
654
                  (vdecls_to_vals t.tlocals)
655
                  (vdecls_to_vals t.toutputs))))
656

  
657
let pp_transition_footprint_lemmas fmt m =
658
  pp_print_list
659
    ~pp_epilogue:pp_print_cut
660
    ~pp_open_box:pp_open_vbox0
661
    (pp_transition_footprint_lemma m) fmt
662
    (List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
663
         m.mspec.mtransitions)
664

  
665
let pp_initialization_def fmt m =
685 666
  if not (fst (get_stateless_status m)) then
686 667
    let name = m.mname.node_id in
687 668
    let mem_in = mk_mem_in m in
......
689 670
      (pp_predicate
690 671
         (pp_initialization (pp_machine_decl' ~ghost:true))
691 672
         (pp_and_l (fun fmt (i, (td, _)) ->
692
              pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
673
              if Arrow.td_is_arrow td then
674
                pp_initialization pp_access' fmt (node_name td, (mem_in, i))
675
              else
676
                pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int
677
                  fmt
678
                  ((mem_in, i), 1))))
693 679
      fmt
694 680
      ((name, (name, mem_in)), m.minstances)
695 681

  
682
let pp_reset_cleared_def fmt m =
683
  if not (fst (get_stateless_status m)) then
684
    let name = m.mname.node_id in
685
    let mem_in = mk_mem_in m in
686
    let mem_out = mk_mem_out m in
687
    pp_acsl
688
      (pp_predicate
689
         (pp_reset_cleared
690
            (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true))
691
         (pp_ite
692
            (pp_reset_flag' ~indirect:false)
693
            (pp_and
694
               (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
695
               pp_initialization')
696
            (pp_equal pp_print_string pp_print_string)))
697
      fmt
698
      ((name, (name, mem_in), (name, mem_out)),
699
       (mem_in,
700
        ((mem_out, 0), (name, mem_out)),
701
        (mem_out, mem_in)))
702

  
696 703
let pp_at pp_p fmt (p, l) =
697 704
  fprintf fmt "\\at(%a, %s)" pp_p p l
698 705

  
......
712 719
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
713 720
  pp_print_list
714 721
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
715
    ~pp_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
722
    ~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "")
716 723
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
717 724
    (fun fmt (i, _) -> pp_print_string fmt i)
718 725
    fmt mems
......
736 743

  
737 744
  let print_machine_decl_prefix = fun _ _ -> ()
738 745

  
739
  let pp_import_standard_spec fmt () =
740
    fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
746
  let pp_import_arrow fmt () =
747
    fprintf fmt "#include \"%s/arrow_spec.h%s\""
741 748
      (Arrow.arrow_top_decl ()).top_decl_owner
742 749
      (if !Options.cpp then "pp" else "")
743 750

  
......
748 755
  module GhostProto = GhostProto
749 756

  
750 757
  let pp_predicates (* dependencies *) fmt machines =
758
    let pp_preds comment pp =
759
      pp_print_list
760
        ~pp_open_box:pp_open_vbox0
761
        ~pp_prologue:(pp_print_endcut comment)
762
        pp
763
        ~pp_epilogue:pp_print_cutcut in
751 764
    fprintf fmt
752
      "%a%a%a%a"
753
      (pp_print_list
754
         ~pp_open_box:pp_open_vbox0
755
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
756
         print_machine_valid_predicate
757
         ~pp_epilogue:pp_print_cutcut) machines
758
      (pp_print_list
759
         ~pp_open_box:pp_open_vbox0
760
         ~pp_sep:pp_print_cutcut
761
         ~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
762
         pp_memory_pack_defs
763
         ~pp_epilogue:pp_print_cutcut) machines
764
      (pp_print_list
765
         ~pp_open_box:pp_open_vbox0
766
         ~pp_sep:pp_print_cutcut
767
         ~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
768
         print_machine_init_predicate
769
         ~pp_epilogue:pp_print_cutcut) machines
770
      (pp_print_list
771
         ~pp_open_box:pp_open_vbox0
772
         ~pp_sep:pp_print_cutcut
773
         ~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
774
         pp_transition_defs
775
         ~pp_epilogue:pp_print_cutcut) machines
765
      "%a%a%a%a%a%a"
766
      (pp_preds "/* ACSL `valid` predicates */"
767
         pp_mem_valid_def) machines
768
      (pp_preds "/* ACSL `memory pack` simulations */"
769
         pp_memory_pack_defs) machines
770
      (pp_preds "/* ACSL initialization annotations */"
771
         pp_initialization_def) machines
772
      (pp_preds "/* ACSL reset cleared annotations */"
773
         pp_reset_cleared_def) machines
774
      (pp_preds "/* ACSL transition annotations */"
775
         pp_transition_defs) machines
776
      (pp_preds "/* ACSL transition memory footprints lemmas */"
777
         pp_transition_footprint_lemmas) machines
776 778

  
777 779
  let pp_clear_reset_spec fmt self mem m =
778 780
    let name = m.mname.node_id in
......
796 798
                         ~i:(List.length m.mspec.mmemory_packs - 2)
797 799
                         pp_ptr pp_print_string))
798 800
          (name, mem, self)
799
          (pp_assigns pp_reset_flag) [self]
801
          (pp_assigns pp_reset_flag') [self]
800 802
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
801 803
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
802
          (pp_assigns pp_reset_flag) [mem]
804
          (pp_assigns pp_reset_flag') [mem]
803 805
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
804 806
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
805
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
807
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
806 808
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
807
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
809
          (pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0)
808 810
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
809 811
      )
810 812
      fmt ()
......
815 817
        fprintf fmt
816 818
          "%a@,%a@,%a"
817 819
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
818
          (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
819
          (pp_assigns pp_reset_flag) [self; mem])
820
          (pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1)
821
          (pp_assigns pp_reset_flag') [self; mem])
820 822
      fmt ()
821 823

  
822 824
  let pp_step_spec fmt machines self mem m =
......
839 841
            (name, inputs, [], outputs, "", "")
840 842
        else
841 843
          fprintf fmt
842
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
844
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
843 845
            (pp_requires (pp_valid pp_var_decl)) outputs
844 846
            (pp_requires pp_mem_valid') (name, self)
845 847
            (pp_requires (pp_separated self mem)) (insts', outputs)
846 848
            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
847 849
            (name, mem, self)
850
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
851
            (name, mem, self)
852
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
853
                           pp_ptr pp_var_decl pp_ptr_decl))
854
            (name, inputs, [], outputs, mem, mem)
848 855
            (pp_assigns pp_ptr_decl) outputs
849 856
            (pp_assigns (pp_reg self)) m.mmemory
857
            (pp_assigns pp_reset_flag') [self]
850 858
            (pp_assigns (pp_memory self)) (memories insts')
851 859
            (pp_assigns (pp_register_chain self)) insts
852 860
            (pp_assigns (pp_reset_flag_chain self)) insts''
853 861
            (pp_assigns (pp_reg mem)) m.mmemory
862
            (pp_assigns pp_reset_flag') [mem]
854 863
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
855 864
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
856 865
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
857
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
858
                           pp_ptr pp_var_decl pp_ptr_decl))
859
            (name, inputs, [], outputs, mem, mem)
860 866
      )
861 867
      fmt ()
862 868

  
......
876 882
    | MSetReset inst ->
877 883
      let td, _ = List.assoc inst m.minstances in
878 884
      if Arrow.td_is_arrow td then
879
         fprintf fmt "@,%a"
885
         fprintf fmt "@,%a;"
880 886
           (pp_acsl_line
881 887
              (pp_ghost
882 888
                 (pp_arrow_reset_ghost self)))
src/backends/EMF/EMF_backend.ml
248 248
  | MNoReset ni ->
249 249
    let write = ISet.singleton (reset_name ni) in
250 250
    write, write, VSet.empty
251
  (* TODO: handle clear_reset *)
252
  | MClearReset -> ISet.empty, ISet.empty, VSet.empty
251
  (* TODO: handle clear_reset and reset flag *)
252
  | MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty
253 253
  | MSpec _ | MComment _ -> assert false (* not  available for EMF output *)
254 254
     
255 255
(* A kind of super join_guards: all MBranch are postponed and sorted by
......
274 274
let rec pp_emf_instr m fmt i =
275 275
  let pp_content fmt i =
276 276
    match Corelang.get_instr_desc i with
277
    | MLocalAssign(lhs, expr)
278
      -> (
279
	(match expr.value_desc with
280
	| Fun (fun_id, vl) -> (
281
	  (* Thanks to normalization, vl shall only contain constant or
282
	     local/state vars but not calls to other functions *)
283
	  fprintf fmt "\"kind\": \"operator\",@ ";
284
	  fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
285
	  fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
286
	    fun_id
287
	    (pp_emf_cst_or_var_list m) vl
288
	)	 
289
	| Array _ | Access _ | Power _ 
290
	| Cst _ 
291
	| Var _ -> (
292
	  fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
293
	    pp_var_name lhs
294
	    (pp_emf_cst_or_var m) expr
295
	))    )
277
    | MLocalAssign(lhs, expr) ->
278
      begin match expr.value_desc with
279
        | Fun (fun_id, vl) ->
280
          (* Thanks to normalization, vl shall only contain constant or
281
             local/state vars but not calls to other functions *)
282
          fprintf fmt "\"kind\": \"operator\",@ ";
283
          fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
284
          fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
285
            fun_id
286
            (pp_emf_cst_or_var_list m) vl
287
        | Array _ | Access _ | Power _
288
        | Cst _
289
        | Var _ ->
290
          fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
291
            pp_var_name lhs
292
            (pp_emf_cst_or_var m) expr
293
        | ResetFlag ->
294
          (* TODO: handle reset flag *)
295
          assert false
296
      end
296 297

  
297 298
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
298
				 variable or a constant, no function anymore! *)
299
                                 variable or a constant, no function anymore! *)
299 300
      -> (
300
	fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
301
	  pp_var_name lhs
302
	  (pp_emf_cst_or_var m) expr
303
      )
304
       
301
          fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
302
            pp_var_name lhs
303
            (pp_emf_cst_or_var m) expr
304
        )
305

  
305 306
    | MSetReset id
306 307
      -> (
307
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
308
	  (reset_name id)
309
      )
308
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
309
            (reset_name id)
310
        )
310 311
    | MNoReset id           
311 312
      -> (
312
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
313
	  (reset_name id)
314
      )
315
  (* TODO: handle clear_reset *)
316
  | MClearReset -> ()
317
       
318
    | MBranch (g, hl) -> (
319
      let all_outputs, outputs, inputs = branch_instr_vars m i in
320
      (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
321
      (* 	Machine_code.pp_instr i *)
322
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
323
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
324
      (* 	pp_emf_vars_decl *)
325
      (* 	(VSet.elements inputs) *)
313
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
314
            (reset_name id)
315
        )
316
    (* TODO: handle clear_reset and reset flag *)
317
    | MClearReset | MResetAssign _ -> ()
326 318

  
327
      (* ; *)
328
      let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
319
    | MBranch (g, hl) -> (
320
        let all_outputs, outputs, inputs = branch_instr_vars m i in
321
        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
322
        (* 	Machine_code.pp_instr i *)
323
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
324
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
325
        (* 	pp_emf_vars_decl *)
326
        (* 	(VSet.elements inputs) *)
327

  
328
        (* ; *)
329
        let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
329 330
      (* Format.eprintf "Filtering in: %a@.@." *)
330 331
      (* 	pp_emf_vars_decl *)
331 332
      (* 	(VSet.elements inputs) *)
src/clock_calculus.ml
517 517
and clock_expr ?(nocarrier=true) env expr =
518 518
  let resulting_ck = 
519 519
    match expr.expr_desc with
520
      | Expr_const _ ->
520
    | Expr_const _ ->
521 521
      let ck = new_var true in
522 522
      expr.expr_clock <- ck;
523 523
      ck
524
  | Expr_ident v ->
524
    | Expr_ident v ->
525 525
      let ckv =
526 526
        try
527 527
          Env.lookup_value env v
528 528
        with Not_found -> 
529
	  failwith ("Internal error, variable \""^v^"\" not found")
529
          failwith ("Internal error, variable \""^v^"\" not found")
530 530
      in
531 531
      let ck = instantiate (ref []) (ref []) ckv in
532 532
      expr.expr_clock <- ck;
533 533
      ck
534
  | Expr_array elist ->
535
    let ck = clock_standard_args env elist in
536
    expr.expr_clock <- ck;
537
    ck
538
  | Expr_access (e1, _) ->
539
    (* dimension, being a static value, doesn't need to be clocked *)
540
    let ck = clock_standard_args env [e1] in
541
    expr.expr_clock <- ck;
542
    ck
543
  | Expr_power (e1, _) ->
544
    (* dimension, being a static value, doesn't need to be clocked *)
545
    let ck = clock_standard_args env [e1] in
546
    expr.expr_clock <- ck;
547
    ck
548
  | Expr_tuple elist ->
549
    let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
550
    expr.expr_clock <- ck;
551
    ck
552
  | Expr_ite (c, t, e) ->
553
    let ck_c = clock_standard_args env [c] in
554
    let ck = clock_standard_args env [t; e] in
555
    (* Here, the branches may exhibit a tuple clock, not the condition *)
556
    unify_tuple_clock (Some ck_c) ck expr.expr_loc;
557
    expr.expr_clock <- ck;
558
    ck
559
  | Expr_appl (id, args, r) ->
560
    (try
561
(* for a modular compilation scheme, all inputs/outputs must share the same clock !
562
   this is also the reset clock !
563
*)
564
    let cr =
565
      match r with
566
      | None        -> new_var true
567
      | Some c      -> clock_standard_args env [c] in
568
    let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
569
    expr.expr_clock <- couts;
570
    couts
571
    with exn -> (
572
      Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
573
      raise exn
574
    ))
575
  | Expr_fby (e1,e2)
576
  | Expr_arrow (e1,e2) ->
577
    let ck = clock_standard_args env [e1; e2] in
578
    unify_tuple_clock None ck expr.expr_loc;
579
    expr.expr_clock <- ck;
580
    ck
581
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
534
    | Expr_array elist ->
535
      let ck = clock_standard_args env elist in
536
      expr.expr_clock <- ck;
537
      ck
538
    | Expr_access (e1, _) ->
539
      (* dimension, being a static value, doesn't need to be clocked *)
540
      let ck = clock_standard_args env [e1] in
541
      expr.expr_clock <- ck;
542
      ck
543
    | Expr_power (e1, _) ->
544
      (* dimension, being a static value, doesn't need to be clocked *)
545
      let ck = clock_standard_args env [e1] in
546
      expr.expr_clock <- ck;
547
      ck
548
    | Expr_tuple elist ->
549
      let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
550
      expr.expr_clock <- ck;
551
      ck
552
    | Expr_ite (c, t, e) ->
553
      let ck_c = clock_standard_args env [c] in
554
      let ck = clock_standard_args env [t; e] in
555
      (* Here, the branches may exhibit a tuple clock, not the condition *)
556
      unify_tuple_clock (Some ck_c) ck expr.expr_loc;
557
      expr.expr_clock <- ck;
558
      ck
559
    | Expr_appl (id, args, r) ->
560
      (try
561
         (* for a modular compilation scheme, all inputs/outputs must share the same clock !
562
            this is also the reset clock !
563
         *)
564
         let cr =
565
           match r with
566
           | None        -> new_var true
567
           | Some c      -> clock_standard_args env [c] in
568
         let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
569
         expr.expr_clock <- couts;
570
         couts
571
       with exn -> (
572
           Format.eprintf "Current expr: %a@." Printers.pp_expr expr;
573
           raise exn
574
         ))
575
    | Expr_fby (e1,e2)
576
    | Expr_arrow (e1,e2) ->
577
      let ck = clock_standard_args env [e1; e2] in
578
      unify_tuple_clock None ck expr.expr_loc;
579
      expr.expr_clock <- ck;
580
      ck
581
    | Expr_pre e -> (* todo : deal with phases as in tail ? *)
582 582
      let ck = clock_standard_args env [e] in
583 583
      expr.expr_clock <- ck;
584 584
      ck
585
  | Expr_when (e,c,l) ->
585
    | Expr_when (e,c,l) ->
586 586
      let ce = clock_standard_args env [e] in
587 587
      let c_loc = loc_of_cond expr.expr_loc c in
588 588
      let cr = clock_carrier env c c_loc ce in
......
591 591
      let ck' = clock_on ce cr' l in
592 592
      expr.expr_clock <- ck';
593 593
      ck
594
  | Expr_merge (c,hl) ->
594
    | Expr_merge (c,hl) ->
595 595
      let cvar = new_var true in
596 596
      let crvar = new_carrier Carry_name true in
597
      List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
597
      List.iter (fun (t, h) ->
598
          let ckh = clock_uncarry (clock_expr env h) in
599
          unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
598 600
      let cr = clock_carrier env c expr.expr_loc cvar in
599 601
      try_unify_carrier cr crvar expr.expr_loc;
600 602
      let cres = clock_current ((snd (List.hd hl)).expr_clock) in
src/lustre_live.ml
80 80
      let asg = inter (assigned asg eq) vars in
81 81
      let noc = no_occur_after i in
82 82
      let liv = diff asg noc in
83
      Format.printf "asg %i: %a@." (i+1) pp_iset asg;
84
      Format.printf "noc %i: %a@." (i+1) pp_iset noc;
85
      Format.printf "liv %i: %a@." (i+1) pp_iset liv;
86 83
      Live.add (i + 1) liv l, asg, i + 1)
87 84
      (Live.add 0 empty Live.empty, empty, 0) sorted_eqs in
88
  Format.(printf "@;%a@." (pp_print_list ~pp_open_box:pp_open_vbox0
89
                           (fun fmt (i, l) -> fprintf fmt "%i : %a" i pp_iset l))
90
                           (Live.bindings l));
85
  Log.report ~level:6 (fun fmt ->
86
      Format.(fprintf fmt "Live variables of %s: %a@;@;" nid
87
                (pp_print_list ~pp_open_box:pp_open_vbox0
88
                   (fun fmt (i, l) -> fprintf fmt "%i: %a" i pp_iset l))
89
                (Live.bindings l)));
91 90
  Hashtbl.add live nid l
92 91

  
93 92
let live_i nid i =
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

  
src/machine_code_common.ml
54 54
      fun fmt e -> pp_expr m fmt e
55 55
    in
56 56
    match p with
57
    | Transition (f, inst, i, inputs, locals, outputs) ->
57
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
58 58
      fprintf fmt "Transition_%a<%a>%a%a"
59 59
        pp_print_string f
60 60
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
61 61
           pp_print_string) inst
62 62
        (pp_print_option pp_print_int) i
63 63
        (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
64
    | Reset (f, inst, r) ->
65
      fprintf fmt "Reset_%a<%a> on %a"
66
        pp_print_string f
67
        pp_print_string inst
68
        (pp_val m) r
64 69
    | MemoryPack (f, inst, i) ->
65 70
      fprintf fmt "MemoryPack_%a<%a>%a"
66 71
        pp_print_string f
......
102 107
        pp_predicate m fmt p
103 108
      | StateVarPack r ->
104 109
        fprintf fmt "StateVarPack<%a>" pp_reg r
105
      | ExistsMem (rc, tr) ->
106
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [rc; tr])
110
      | ExistsMem (_f, a, b) ->
111
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [a; b])
107 112
    in
108 113
    pp_spec
109 114

  
src/scheduling.ml
123 123
  Log.report ~level:5 (fun fmt -> Format.fprintf fmt "scheduling node %s@ " n.node_id);
124 124
  let eq_equiv = eq_equiv (ExprDep.node_eq_equiv n) in
125 125

  
126
  let n', g = global_dependency n in
126
  let node, g = global_dependency n in
127 127
  
128 128
  (* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs
129 129
     compute: coi predecessors of outputs
......
131 131
     DONE !
132 132
  *)
133 133

  
134
  let gg = IdentDepGraph.copy g in
135
  let sort = topological_sort eq_equiv g in
136
  let unused = Liveness.compute_unused_variables n gg in
137
  let fanin = Liveness.compute_fanin n gg in
138
  { node = n'; schedule = sort; unused_vars = unused; fanin_table = fanin; dep_graph = gg; }
134
  let dep_graph = IdentDepGraph.copy g in
135
  let schedule = topological_sort eq_equiv g in
136
  let unused_vars = Liveness.compute_unused_variables n dep_graph in
137
  let fanin_table = Liveness.compute_fanin n dep_graph in
138
  { node; schedule; unused_vars; fanin_table; dep_graph }
139 139

  
140 140
(* let schedule_eqs eqs =
141 141
 *   let eq_equiv = eq_equiv (ExprDep.eqs_eq_equiv eqs) in
src/spec_common.ml
1
open Lustre_types
2 1
open Spec_types
3 2

  
4 3
(* a small reduction engine *)
......
85 84
(* let mk_clocked_on id =
86 85
 *   mk_pred_call (Clocked_on id) *)
87 86

  
88
let mk_transition ?i ?inst id inputs locals outputs =
89
  mk_pred_call
90
    (Transition (id, inst, i, vals inputs, vals locals, vals outputs))
87
let mk_transition ?(mems=Utils.ISet.empty) ?r ?i ?inst id inputs locals outputs =
88
  let tr =
89
    mk_pred_call
90
      (Transition (id, inst, i, vals inputs, vals locals, vals outputs,
91
                  (match r with Some _ -> true | None -> false), mems)) in
92
    (match r, inst with
93
     | Some r, Some inst ->
94
       ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
95
     | _ ->
96
       tr)
91 97

  
92 98
let mk_memory_pack ?i ?inst id =
93 99
  mk_pred_call (MemoryPack (id, inst, i))
src/spec_types.ml
23 23
type ('a, 'b) expressions_t = ('a, 'b) expression_t list
24 24

  
25 25
type 'a predicate_t =
26
  | Transition: ident * ident option * int option
27
                * ('a, 'b) expressions_t
28
                * ('a, 'b) expressions_t
29
                * ('a, 'b) expressions_t -> 'a predicate_t
26
  | Transition: ident                        (* node name *)
27
                * ident option               (* instance *)
28
                * int option                 (* transition index *)
29
                * ('a, 'b) expressions_t       (* inputs *)
30
                * ('a, 'b) expressions_t       (* locals *)
31
                * ('a, 'b) expressions_t       (* outputs *)
32
                * bool                       (* reset *)
33
                * Utils.ISet.t               (* memory footprint *)
34
      -> 'a predicate_t
35
  | Reset of ident * ident * 'a
30 36
  | MemoryPack of ident * ident option * int option
31 37
  | Initialization
32 38
  | ResetCleared of ident
......
43 49
  | Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t -> 'a formula_t
44 50
  | Predicate: 'a predicate_t -> 'a formula_t
45 51
  | StateVarPack of register_t
46
  | ExistsMem of 'a formula_t * 'a formula_t
52
  | ExistsMem of ident * 'a formula_t * 'a formula_t
47 53

  
48 54
(* type 'a simulation_t = {
49 55
 *   sname: node_desc;
......
64 70
  tlocals: var_decl list;
65 71
  toutputs: var_decl list;
66 72
  tformula: 'a formula_t;
73
  tfootprint: Utils.ISet.t;
67 74
}
68 75

  

Also available in: Unified diff