Project

General

Profile

« Previous | Next » 

Revision d0f26f04

Added by LĂ©lio Brun 7 months ago

corrections for stateless nodes

View differences:

dune-project
1 1
(lang dune 2.8)
2

  
2 3
(name lustrec)
3 4
(version 1.7)
4 5

  
src/backends/C/c_backend.ml
41 41
    ( print_alloc_header,
42 42
      print_lib_c,
43 43
      print_main_c,
44
      print_makefile,
45
      preprocess
44
      print_makefile
46 45
    (* , print_cmake *) ) basename prog machines dependencies =
47 46
  let destname = !Options.dest_dir ^ "/" ^ basename in
48 47

  
49
  let machines, spec = preprocess machines in
50

  
51 48
  (* Generating H alloc file *)
52 49
  let alloc_header_file = destname ^ "_alloc.h" in
53 50
  (* Could be changed *)
54 51
  with_out_file alloc_header_file (fun header_fmt ->
55
      print_alloc_header header_fmt basename prog machines dependencies spec);
52
      print_alloc_header header_fmt basename machines dependencies);
56 53

  
57 54
  (* Generating Lib C file *)
58 55
  let source_lib_file = c_or_cpp destname in
......
124 121
      Header.print_header_from_header header_fmt basename lusic.contents)
125 122

  
126 123
let translate_to_c generate_c_header basename prog machines dependencies =
127
  let header_m, source_m, source_main_m, makefile_m, preprocess =
124
  let header_m, source_m, source_main_m, makefile_m =
128 125
    match !Options.spec with
129 126
    | "no" ->
130 127
      ( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
131 128
        C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
132 129
        C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
133
        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)),
134
        fun m -> m, [] )
130
        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)) )
135 131
    | "acsl" ->
136 132
      let open C_backend_spec in
137 133
      ( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
138 134
        C_backend_src.((module SrcMod : MODIFIERS_SRC)),
139 135
        C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
140
        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)),
141
        preprocess_acsl )
136
        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)) )
142 137
    | "c" ->
143 138
      assert false (* not implemented yet *)
144 139
    | _ ->
......
153 148
    ( Header.print_alloc_header,
154 149
      Source.print_lib_c,
155 150
      SourceMain.print_main_c,
156
      Makefile.print_makefile,
157
      preprocess )
151
      Makefile.print_makefile )
158 152
    (* CMakefile.print_makefile *)
159 153
  in
160 154
  if generate_c_header then print_c_header basename;
src/backends/C/c_backend_common.ml
720 720
end
721 721

  
722 722
module EmptyGhostProto : MODIFIERS_GHOST_PROTO = struct
723
  let pp_ghost_parameters ?cut _ _ = ()
723
  let pp_ghost_parameters ?cut _ _ = ignore cut
724 724
end
725 725

  
726 726
module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
src/backends/C/c_backend_header.ml
302 302
    (* MAIN Header Printing functions *)
303 303
    (********************************************************************************************)
304 304

  
305
    let print_alloc_header header_fmt basename _prog machines dependencies spec
306
        =
305
    let print_alloc_header header_fmt basename machines dependencies =
307 306
      (* Include once: start *)
308 307
      let baseNAME = file_to_module_name basename in
309 308
      fprintf header_fmt
src/backends/C/c_backend_spec.ml
22 22

  
23 23
(**************************************************************************)
24 24

  
25
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
26
   preamble *)
27
let preprocess_acsl machines = machines, []
28

  
29 25
let pp_acsl_basic_type_desc t_desc =
30 26
  if Types.is_bool_type t_desc then
31 27
    (* if !Options.cpp then "bool" else "_Bool" *)
......
187 183

  
188 184
let pp_not pp fmt = fprintf fmt "!%a" pp
189 185

  
190
let pp_valid pp =
191
  pp_and_l
192
    (* pp_print_list *)
193
    (* ~pp_sep:pp_print_cut *)
194
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
186
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
195 187

  
196 188
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
197 189

  
src/backends/C/c_backend_src.ml
228 228
        | MSetReset inst ->
229 229
          pp_machine_set_reset m self mem fmt inst
230 230
        | MClearReset ->
231
          fprintf fmt "%t@,%a"
232
            (pp_machine_clear_reset m self mem)
233
            pp_label reset_label
231
          if not (fst (get_stateless_status m)) then
232
            fprintf fmt "%t@,%a"
233
              (pp_machine_clear_reset m self mem)
234
              pp_label reset_label
234 235
        | MResetAssign b ->
235 236
          pp_reset_assign self fmt b
236 237
        | MLocalAssign (i, v) ->
src/backends/Horn/horn_backend_traces.ml
27 27

  
28 28
(* Compute memories associated to each machine *)
29 29
let compute_mems machines m =
30
  let rec aux fst prefix m =
30
  let rec aux prefix m =
31 31
    List.map (fun mem -> prefix, mem) m.mmemory
32 32
    @ List.fold_left
33 33
        (fun accu (id, (n, _)) ->
......
35 35
          if name = "_arrow" then accu
36 36
          else
37 37
            let machine_n = get_machine machines name in
38
            aux false ((id, machine_n) :: prefix) machine_n @ accu)
38
            aux ((id, machine_n) :: prefix) machine_n @ accu)
39 39
        [] m.minstances
40 40
  in
41
  aux true [] m
41
  aux [] m
42 42

  
43 43
(* We extract the annotation dealing with traceability *)
44 44
let machines_traces machines =
src/clock_calculus.ml
480 480

  
481 481
and clock_call env f args clock_reset loc =
482 482
  (* Format.eprintf "Clocking call %s@." f; *)
483
  let cfun = clock_ident false env f loc in
483
  let cfun = clock_ident env f loc in
484 484
  let cins, couts = split_arrow cfun in
485 485
  let cins = clock_list_of_clock cins in
486 486
  List.iter2 (clock_subtyping_arg env) args cins;
487 487
  unify_imported_clock (Some clock_reset) cfun loc;
488 488
  couts
489 489

  
490
and clock_ident nocarrier env id loc =
491
  clock_expr ~nocarrier env (expr_of_ident id loc)
490
and clock_ident env id loc = clock_expr env (expr_of_ident id loc)
492 491

  
493 492
and clock_carrier env c loc ce =
494 493
  let expr_c = expr_of_ident c loc in
495
  let ck = clock_expr ~nocarrier:false env expr_c in
494
  let ck = clock_expr env expr_c in
496 495
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
497 496
  let ckb = new_var true in
498 497
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
......
502 501

  
503 502
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
504 503
    environment [env] *)
505
and clock_expr ?(nocarrier = true) env expr =
504
and clock_expr env expr =
506 505
  let resulting_ck =
507 506
    match expr.expr_desc with
508 507
    | Expr_const _ ->
src/lustre_live.ml
15 15
open ISet
16 16
module Live = Map.Make (Int)
17 17

  
18
let pp_live fmt l = Live.bindings
19

  
20 18
let assigned s eq = union s (of_list eq.eq_lhs)
21 19

  
22 20
let rec occur_dim_expr s d =
src/machine_code.ml
236 236
  | None ->
237 237
    None, []
238 238

  
239
let translate_eq env ctx id inputs locals outputs i eq =
239
let translate_eq env ctx nd inputs locals outputs i eq =
240
  let id = nd.node_id in
240 241
  let translate_expr = translate_expr env in
241 242
  let translate_act = translate_act env in
242 243
  let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
......
268 269
        {
269 270
          inst with
270 271
          instr_spec =
271
            [
272
              mk_memory_pack ~i id;
273
              mk_transition ~i id (vdecls_to_vals inputs)
274
                (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
275
            ];
272
            (if fst (get_stateless_status_node nd) then []
273
            else [ mk_memory_pack ~i id ])
274
            @ [
275
                mk_transition ~i id (vdecls_to_vals inputs)
276
                  (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
277
              ];
276 278
        }
277 279
        :: ctx.s;
278 280
      mp = pred_mp ctx spec_mp;
......
388 390
      else eqs)
389 391
    [] locals
390 392

  
391
let translate_eqs env ctx id inputs locals outputs eqs =
393
let translate_eqs env ctx nd inputs locals outputs eqs =
392 394
  List.fold_left
393 395
    (fun (ctx, i) eq ->
394
      let ctx = translate_eq env ctx id inputs locals outputs i eq in
396
      let ctx = translate_eq env ctx nd inputs locals outputs i eq in
395 397
      ctx, i + 1)
396 398
    (ctx, 1) eqs
397 399
  |> fst
......
434 436
    in
435 437
    vars, eql, assertl
436 438

  
437
let translate_core env nid sorted_eqs inputs locals outputs =
439
let translate_core env nd sorted_eqs inputs locals outputs =
438 440
  let constant_eqs = constant_equations locals in
439 441

  
440 442
  (* Compute constants' instructions *)
441
  let ctx0 =
442
    translate_eqs env ctx_init nid inputs locals outputs constant_eqs
443
  in
443
  let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in
444 444
  assert (ctx0.si = []);
445 445
  assert (IMap.is_empty ctx0.j);
446 446

  
447 447
  (* Compute ctx for all eqs *)
448
  let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
448
  let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in
449 449

  
450 450
  ctx, ctx0.s
451 451

  
......
480 480
  }
481 481

  
482 482
let transition_toplevel nd i =
483
  let tr =
484
    mk_transition nd.node_id ~i
485
      (vdecls_to_vals nd.node_inputs)
486
      []
487
      (vdecls_to_vals nd.node_outputs)
488
  in
483 489
  {
484 490
    tname = nd;
485 491
    tindex = None;
......
487 493
    tlocals = [];
488 494
    toutputs = nd.node_outputs;
489 495
    tformula =
490
      ExistsMem
491
        ( nd.node_id,
492
          Predicate (ResetCleared nd.node_id),
493
          mk_transition nd.node_id ~i
494
            (vdecls_to_vals nd.node_inputs)
495
            []
496
            (vdecls_to_vals nd.node_outputs) );
496
      (if fst (get_stateless_status_node nd) then tr
497
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
497 498
    tfootprint = ISet.empty;
498 499
  }
499 500

  
......
542 543

  
543 544
  (* Translate equations *)
544 545
  let ctx, ctx0_s =
545
    translate_core env nd.node_id equations nd.node_inputs locals
546
      nd.node_outputs
546
    translate_core env nd equations nd.node_inputs locals nd.node_outputs
547 547
  in
548 548

  
549 549
  (* Format.eprintf "ok4@.@?"; *)
......
578 578
  let clear_reset =
579 579
    mkinstr
580 580
      ~instr_spec:
581
        [
582
          mk_memory_pack ~i:0 nd.node_id;
583
          mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
584
        ]
581
        ((if fst (get_stateless_status_node nd) then []
582
         else [ mk_memory_pack ~i:0 nd.node_id ])
583
        @ [
584
            mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
585
          ])
585 586
      MClearReset
586 587
  in
587 588
  {
src/machine_code_common.mli
17 17
  Lustre_types.var_decl ->
18 18
  Machine_code_types.value_t
19 19

  
20
val get_stateless_status_node : Lustre_types.node_desc -> bool * bool
21

  
20 22
val get_stateless_status : Machine_code_types.machine_t -> bool * bool
21 23

  
22 24
val get_stateless_status_top_decl : Lustre_types.top_decl -> bool * bool
src/main_lustre_testgen.ml
192 192

  
193 193
    Arg.parse options anonymous usage
194 194
  with
195
  | Parse.Error _
195
  | Parse.Error
196 196
  | Types.Error (_, _)
197 197
  | Clocks.Error (_, _)
198 198
  | Error.Error _
src/typing.ml
332 332
  (* Expected type ty1, got type ty2 *)
333 333
  let try_unify ?(sub = false) ?(semi = false) ty1 ty2 loc =
334 334
    try unify ~sub ~semi ty1 ty2 with
335
    | Unify (t1', t2') ->
335
    | Unify _ ->
336 336
      raise (Error (loc, Type_clash (ty1, ty2)))
337 337
    | Dimension.Unify _ ->
338 338
      raise (Error (loc, Type_clash (ty1, ty2)))

Also available in: Unified diff