Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

src/backends/Ada/ada_backend.ml
92 92
      | Expr_appl call -> assert false
93 93
      *)
94 94
  in
95
  match m.mspec with
95
  match m.mspec.mnode_spec with
96 96
    | Some (NodeSpec ident) ->
97 97
      begin
98 98
        let machine_spec = find_submachine_from_ident ident machines in
99 99
        let guarantees =
100
          match machine_spec.mspec with
100
          match machine_spec.mspec.mnode_spec with
101 101
            | Some (Contract contract) ->
102 102
                assert (contract.consts=[]);
103 103
                assert (contract.locals=[]);
......
126 126
  let module Wrapper = Ada_backend_wrapper.Main in
127 127

  
128 128
  let is_real_machine m =
129
    match m.mspec with
129
    match m.mspec.mnode_spec with
130 130
      | Some (Contract _) -> false
131 131
      | _ -> true
132 132
  in
src/backends/EMF/EMF_backend.ml
454 454
  try
455 455
    fprintf fmt "@[<v 2>\"%a\": {@ "
456 456
      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
457
    (match m.mspec with Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ " | _ -> ());
457
    (match m.mspec.mnode_spec with
458
     | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
459
     | _ -> ());
458 460
    fprintf fmt "\"imported\": \"false\",@ ";
459 461
    fprintf fmt "\"kind\": %t,@ "
460 462
      (fun fmt -> if not ( snd (get_stateless_status m) )
......
471 473
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
472 474
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
473 475
      (pp_emf_instrs m) instrs;
474
    (match m.mspec with | None -> () 
475
                        | Some (Contract c) -> (
476
                          assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
477
                          fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
478
                        )
479
                        | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
476
    (match m.mspec.mnode_spec with
477
     | None -> ()
478
     | Some (Contract c) -> (
479
         assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
480
         fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
481
       )
482
     | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
480 483
    );
481 484
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
482 485
    fprintf fmt "@]@ }"
src/causality.ml
609 609

  
610 610
  
611 611
let pp_dep_graph fmt g =
612
  Format.fprintf fmt "@[<v 2>{ /* graph */%t@] }"
612
  Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]"
613 613
    (fun fmt ->
614
       IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@,%s -> %s" s t) g)
614
       IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@ %s -> %s" s t) g)
615 615

  
616 616
let pp_error fmt err =
617 617
  match err with
src/checks/liveness.ml
39 39
  end
40 40
 
41 41
let pp_fanin fmt fanin =
42
  begin
43
    Format.fprintf fmt "{ /* locals fanin: */@.";
44
    Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> %d@." s t) fanin;
45
    Format.fprintf fmt "}@."
46
  end
42
  Format.fprintf fmt "@[<v 0>@[<v 2>{ /* locals fanin: */";
43
  Hashtbl.iter (fun s t -> Format.fprintf fmt "@ %s -> %d" s t) fanin;
44
  Format.fprintf fmt "@]@ }@]"
47 45

  
48 46
(* computes the cone of influence of a given [var] wrt a dependency graph [g].
49 47
*)
src/clock_calculus.ml
600 600
      expr.expr_clock <- cres;
601 601
      cres
602 602
  in
603
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
603
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@ "
604
                          Printers.pp_expr expr Clocks.print_ck resulting_ck);
604 605
  resulting_ck
605 606

  
606 607
let clock_of_vlist vars =
......
686 687
  let ck_outs = clock_of_vlist nd.node_outputs in
687 688
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
688 689
  unify_imported_clock None ck_node loc;
689
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
690
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
690 691
  (* Local variables may contain first-order carrier variables that should be generalized.
691 692
     That's not the case for types. *)
692 693
  try_generalize ck_node loc;
......
698 699
  (*  if (is_main && is_polymorphic ck_node) then
699 700
      raise (Error (loc,(Cannot_be_polymorphic ck_node)));
700 701
  *)
701
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
702
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
702 703
  nd.node_clock <- ck_node;
703 704
  Env.add_value env nd.node_id ck_node
704 705

  
src/compiler_common.ml
72 72
    
73 73

  
74 74
let expand_automata decls =
75
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. expanding automata@ ");
75
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
76 76
  try
77 77
    Automata.expand_decls decls
78 78
  with (Error.Error (loc, err)) as exc ->
......
82 82
    raise exc
83 83

  
84 84
let check_stateless_decls decls =
85
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ ");
85
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. checking stateless/stateful status@ ");
86 86
  try
87 87
    Stateless.check_prog decls
88 88
  with (Stateless.Error (loc, err)) as exc ->
......
92 92
    raise exc
93 93

  
94 94
let force_stateful_decls decls =
95
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. forcing stateful status@ ");
95
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
96 96
  try
97 97
    Stateless.force_prog decls
98 98
  with (Stateless.Error (loc, err)) as exc ->
......
102 102
    raise exc
103 103

  
104 104
let type_decls env decls =  
105
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
105
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
106 106
  let new_env = 
107
    begin
108
      try
109
	Typing.type_prog env decls
110
      with (Types.Error (loc,err)) as exc ->
111
	eprintf "Typing error: %a%a@."
112
	  Types.pp_error err
113
	  Location.pp_loc loc;
114
	raise exc
115
    end 
107
    try
108
      Typing.type_prog env decls
109
    with Types.Error (loc,err) as exc ->
110
      eprintf "Typing error: %a%a@."
111
        Types.pp_error err
112
        Location.pp_loc loc;
113
      raise exc
116 114
  in
115
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
117 116
  if !Options.print_types || !Options.verbose_level > 2 then
118 117
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
119 118
  new_env
120 119
      
121 120
let clock_decls env decls = 
122
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
121
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
123 122
  let new_env =
124
    begin
125
      try
126
	Clock_calculus.clock_prog env decls
127
      with (Clocks.Error (loc,err)) as exc ->
128
	eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
129
	raise exc
130
    end
123
    try
124
      Clock_calculus.clock_prog env decls
125
    with (Clocks.Error (loc,err)) as exc ->
126
      eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
127
      raise exc
131 128
  in
129
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
132 130
  if !Options.print_clocks  || !Options.verbose_level > 2 then
133 131
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
134 132
  new_env
src/compiler_stages.ml
32 32
          not lusic.Lusic.from_lusi)
33 33
    then
34 34
      begin
35
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
35
        Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. generating compiled header file %s@,"
36
                                header_name);
36 37
        Lusic.write_lusic
37 38
          from_lusi (* is it a lusi file ? *)
38 39
          (if from_lusi then prog else Lusic.extract_header dirname basename prog)
......
42 43
      end
43 44
    else (* Lusic exists and is usable. Checking compatibility *)
44 45
      begin
45
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
46
        Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. loading compiled header file %s@,"
47
                                header_name);
46 48
        let lusic = Lusic.read_lusic destname lusic_ext in
47 49
        Lusic.check_obsolete lusic destname;
48 50
        let header = lusic.Lusic.contents in
......
61 63

  
62 64
  (* Removing automata *)
63 65
  let prog = expand_automata prog in
64
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
66
  Log.report ~level:4 (fun fmt ->
67
      fprintf fmt "@[<v 2>.. after automata expansion:@ %a@]@ "
68
        Printers.pp_prog prog
69
        (* Utils.Format.pp_print_nothing () *)
70
    );
65 71

  
66 72
  (* Importing source *)
67 73
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
......
78 84
  let prog = resolve_contracts prog in
79 85
  let prog = SortProg.sort prog in
80 86
  Log.report ~level:3 (fun fmt ->
81
      Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Printers.pp_prog prog);
87
      Format.fprintf fmt "@ @[<v 2>.. contracts resolved:@ %a@ @]@ " Printers.pp_prog prog);
82 88

  
83 89
  (* Consolidating main node *)
84 90
  let _ =
......
201 207
  (* Machine_types.load prog; *)
202 208

  
203 209
  (* Normalization phase *)
204
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
210
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. normalization@ ");
205 211
  let prog = Normalization.normalize_prog params prog in
206
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog_short prog);
207
  Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
212
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
213
                          Printers.pp_prog_short prog);
214
  Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
215
                           Printers.pp_prog prog);
208 216
  
209 217
  (* Compatibility with Lusi *)
210 218
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
......
217 225
    if !Options.mpfr
218 226
    then
219 227
      begin
220
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
228
	Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. targetting MPFR library@,");
221 229
	Mpfr.inject_prog prog
222 230
      end
223 231
    else
224 232
      begin
225
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
233
	Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. keeping floating-point numbers@,");
226 234
	prog
227 235
      end in
228 236
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
......
230 238
  (* Checking array accesses *)
231 239
  if !Options.check then
232 240
    begin
233
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
241
      Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. checking array accesses@,");
234 242
      Access.check_prog prog;
235 243
    end;
236 244

  
......
244 252
let stage2 params prog =
245 253
  (* Computation of node equation scheduling. It also breaks dependency cycles
246 254
     and warns about unused input or memory variables *)
247
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
255
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. scheduling@ ");
248 256
  let prog, node_schs =
249 257
    try
250 258
      Scheduling.schedule_prog prog
......
252 260
				 systemtic way in AlgebraicLoop module *)
253 261
      AlgebraicLoop.analyze prog
254 262
  in
255
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
256
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
257
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
258
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
259
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
260
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
263
  Scheduling.(
264
    Log.report ~level:1 (fun fmt -> pp_warning_unused fmt node_schs);
265
    Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" pp_schedule node_schs);
266
    Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" pp_fanin_table node_schs);
267
    Log.report ~level:5 (fun fmt -> fprintf fmt "@ %a" pp_dep_graph node_schs);
268
    Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" Printers.pp_prog prog);
269
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "));
261 270

  
262 271
  (* TODO Salsa optimize prog:
263 272
     - emits warning for programs with pre inside expressions
......
265 274
     - introduce fresh local variables for each real pure subexpression
266 275
  *)
267 276
  (* DFS with modular code generation *)
268
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
277
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. machines generation@ ");
269 278
  let machine_code = Machine_code.translate_prog prog node_schs in
279
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
270 280

  
271
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
281
  Log.report ~level:3 (fun fmt -> fprintf fmt "@ @[<v 2>.. generated machines (unoptimized):@ %a@]@ "
282
                          Machine_code_common.pp_machines machine_code);
272 283

  
273 284
  (* Optimize machine code *)
274 285
  Optimize_machine.optimize params prog node_schs machine_code
src/dune
21 21
   clocks
22 22
   delay
23 23
   machine_code_types
24
   spec_types
24 25
   scheduling_type
25 26
   log
26 27
   printers
src/log.ml
15 15
    ~level:level p =
16 16
if !verbose_level >= level then
17 17
  if modulename="" then
18
    Format.eprintf "%t@?" p
18
    Format.eprintf "%t" p
19 19
  else
20
    Format.eprintf "[%s] @[%t@]@?" modulename p
20
    Format.eprintf "[%s] @[%t@]" modulename p
21 21

  
22 22
(* Local Variables: *)
23 23
(* compile-command:"make -C .." *)
src/machine_code.ml
15 15
open Corelang
16 16
open Clocks
17 17
open Causality
18
  
18

  
19 19
exception NormalizationError
20 20

  
21 21
(* Questions:
22 22

  
23 23
   - where are used the mconst. They contain initialization of
24
   constant in nodes. But they do not seem to be used by c_backend *)
24
     constant in nodes. But they do not seem to be used by c_backend *)
25

  
25 26

  
26
       
27 27
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
28 28
(* the context contains  m : state aka memory variables  *)
29 29
(*                      si : initialization instructions *)
......
34 34
(* Machine processing requires knowledge about variables and local
35 35
   variables. Local could be memories while other could not.  *)
36 36
type machine_env = {
37
    is_local: string -> bool;
38
    get_var: string -> var_decl
39
  }
37
  is_local: string -> bool;
38
  get_var: string -> var_decl
39
}
40

  
40 41

  
41
                 
42 42
let build_env locals non_locals =
43 43
  let all = VSet.union locals non_locals in
44 44
  {
45 45
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
46
    get_var = (fun id -> try
47
                  VSet.get id all
48
                with Not_found -> (
49
                  (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
50
                   *   id
51
                   *   VSet.pp all; *)
52
                  raise Not_found
53
                )
54
              )  
46
    get_var = (fun id -> try VSet.get id all with Not_found ->
47
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
48
         *   id
49
         *   VSet.pp all; *)
50
        raise Not_found)
55 51
  }
56 52

  
57
  
53

  
58 54

  
59 55
(****************************************************************)
60 56
(* Basic functions to translate to machine values, instructions *) 
......
66 62
    let var_id = env.get_var id in
67 63
    mk_val (Var var_id) var_id.var_type
68 64
  with Not_found ->
69
    try (* id is a constant *)
70
      let vdecl = (Corelang.var_decl_of_const
71
                     (const_of_top (Hashtbl.find Corelang.consts_table id)))
72
      in
73
      mk_val (Var vdecl) vdecl.var_type
74
    with Not_found ->
75
      (* id is a tag, getting its type in the list of declared enums *)
76
      try
77
        let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
78
        mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
79
      with Not_found -> (Format.eprintf
80
                           "internal error: Machine_code.translate_ident %s@.@?"
81
                           id;
82
                         assert false)
65
  try (* id is a constant *)
66
    let vdecl = (Corelang.var_decl_of_const
67
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
68
    in
69
    mk_val (Var vdecl) vdecl.var_type
70
  with Not_found ->
71
  (* id is a tag, getting its type in the list of declared enums *)
72
  try
73
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
74
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
75
  with Not_found ->
76
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
77
    assert false
83 78

  
84 79
let rec control_on_clock env ck inst =
85
 match (Clocks.repr ck).cdesc with
86
 | Con    (ck1, cr, l) ->
87
   let id  = Clocks.const_of_carrier cr in
88
   control_on_clock env ck1
89
     (mkinstr
90
	(MBranch (translate_ident env id,
91
		  [l, [inst]] )))
92
 | _                   -> inst
80
  match (Clocks.repr ck).cdesc with
81
  | Con (ck1, cr, l) ->
82
    let id = Clocks.const_of_carrier cr in
83
    control_on_clock env ck1
84
      (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
85
  | _ -> inst
93 86

  
94 87

  
95 88
(* specialize predefined (polymorphic) operators wrt their instances,
96 89
   so that the C semantics is preserved *)
97 90
let specialize_to_c expr =
98
 match expr.expr_desc with
99
 | Expr_appl (id, e, r) ->
100
   if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
101
   then let id =
102
	  match id with
103
	  | "="  -> "equi"
104
	  | "!=" -> "xor"
105
	  | _    -> id in
106
	{ expr with expr_desc = Expr_appl (id, e, r) }
107
   else expr
108
 | _ -> expr
91
  match expr.expr_desc with
92
  | Expr_appl (id, e, r) ->
93
    if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
94
    then let id =
95
           match id with
96
           | "="  -> "equi"
97
           | "!=" -> "xor"
98
           | _    -> id in
99
      { expr with expr_desc = Expr_appl (id, e, r) }
100
    else expr
101
  | _ -> expr
109 102

  
110 103
let specialize_op expr =
111 104
  match !Options.output with
......
117 110
  let translate_expr = translate_expr env in
118 111
  let value_desc = 
119 112
    match expr.expr_desc with
120
    | Expr_const v                     -> Cst v
121
    | Expr_ident x                     -> (translate_ident env x).value_desc
122
    | Expr_array el                    -> Array (List.map translate_expr el)
123
    | Expr_access (t, i)               -> Access (translate_expr t,
124
                                                  translate_expr 
125
                                                    (expr_of_dimension i))
126
    | Expr_power  (e, n)               -> Power  (translate_expr e,
127
                                                  translate_expr
128
                                                    (expr_of_dimension n))
129
    | Expr_tuple _
130
      | Expr_arrow _ 
131
      | Expr_fby _
132
      | Expr_pre _                       -> (Printers.pp_expr
133
                                               Format.err_formatter expr;
134
                                             Format.pp_print_flush
135
                                               Format.err_formatter ();
136
                                             raise NormalizationError)
137
                                          
138
    | Expr_when    (e1, _, _)          -> (translate_expr e1).value_desc
139
    | Expr_merge   _                   -> raise NormalizationError
113
    | Expr_const v ->
114
      Cst v
115
    | Expr_ident x ->
116
      (translate_ident env x).value_desc
117
    | Expr_array el ->
118
      Array (List.map translate_expr el)
119
    | Expr_access (t, i) ->
120
      Access (translate_expr t, translate_expr (expr_of_dimension i))
121
    | Expr_power  (e, n) ->
122
      Power (translate_expr e, translate_expr (expr_of_dimension n))
123
    | Expr_when (e1, _, _) ->
124
      (translate_expr e1).value_desc
140 125
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
141
       let nd = node_from_name id in
142
       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
143
    | Expr_ite (g,t,e) -> (
126
      let nd = node_from_name id in
127
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
128
    | Expr_ite (g,t,e) when Backends.is_functional () ->
144 129
      (* special treatment depending on the active backend. For
145 130
         functional ones, like horn backend, ite are preserved in
146 131
         expression. While they are removed for C or Java backends. *)
147
      if Backends.is_functional () then
148
	Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
149
      else 
150
	(Format.eprintf "Normalization error for backend %s: %a@."
151
	   !Options.output
152
	   Printers.pp_expr expr;
153
	 raise NormalizationError)
154
    )
155
    | _                   -> raise NormalizationError
132
      Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
133
    | _ ->
134
      Format.eprintf "Normalization error for backend %s: %a@."
135
        !Options.output
136
        Printers.pp_expr expr;
137
      raise NormalizationError
156 138
  in
157 139
  mk_val value_desc expr.expr_type
158 140

  
159 141
let translate_guard env expr =
160 142
  match expr.expr_desc with
161
  | Expr_ident x  -> translate_ident env x
162
  | _ -> (Format.eprintf "internal error: translate_guard %a@."
163
            Printers.pp_expr expr;
164
          assert false)
143
  | Expr_ident x -> translate_ident env x
144
  | _ ->
145
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
146
    assert false
165 147

  
166 148
let rec translate_act env (y, expr) =
167 149
  let translate_act = translate_act env in
168 150
  let translate_guard = translate_guard env in
169 151
  let translate_ident = translate_ident env in
170 152
  let translate_expr = translate_expr env in
171
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
153
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
172 154
  match expr.expr_desc with
173
  | Expr_ite   (c, t, e) -> let g = translate_guard c in
174
			    mk_conditional ?lustre_eq:(Some eq) g
175
                              [translate_act (y, t)]
176
                              [translate_act (y, e)]
177
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq)
178
                              (MBranch (translate_ident x,
179
                                        List.map (fun (t,  h) ->
180
                                            t, [translate_act (y, h)])
181
                                          hl))
182
  | _                    -> mkinstr ?lustre_eq:(Some eq)
183
                              (MLocalAssign (y, translate_expr expr))
155
  | Expr_ite (c, t, e) ->
156
    mk_conditional ~lustre_eq
157
      (translate_guard c)
158
      [translate_act (y, t)]
159
      [translate_act (y, e)]
160
  | Expr_merge (x, hl) ->
161
    mkinstr ~lustre_eq
162
      (MBranch (translate_ident x,
163
                List.map (fun (t,  h) -> t, [translate_act (y, h)]) hl))
164
  | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
184 165

  
185 166
let reset_instance env i r c =
186 167
  match r with
187
  | None        -> []
188
  | Some r      -> let g = translate_guard env r in
189
                   [control_on_clock
190
                      env
191
                      c
192
                      (mk_conditional
193
                         g
194
                         [mkinstr (MReset i)]
195
                         [mkinstr (MNoReset i)])
196
                   ]
168
  | Some r ->
169
    [control_on_clock env c
170
       (mk_conditional
171
          (translate_guard env r)
172
          [mkinstr (MReset i)]
173
          [mkinstr (MNoReset i)])]
174
  | None -> []
197 175

  
198 176

  
199 177
(* Datastructure updated while visiting equations *)
200 178
type machine_ctx = {
201
    m: VSet.t; (* Memories *)
202
    si: instr_t list;
203
    j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
204
    s: instr_t list;
205
  }
179
  m: VSet.t; (* Memories *)
180
  si: instr_t list;
181
  j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
182
  s: instr_t list;
183
}
206 184

  
207 185
let ctx_init = { m = VSet.empty; (* memories *)
208 186
                 si = []; (* init instr *)
209 187
                 j = Utils.IMap.empty;
210 188
                 s = [] }
211
             
189

  
212 190
(****************************************************************)
213 191
(* Main function to translate equations into this machine context we
214 192
   are building *) 
215 193
(****************************************************************)
216 194

  
217
                   
195

  
218 196

  
219 197
let translate_eq env ctx eq =
220 198
  let translate_expr = translate_expr env in
221 199
  let translate_act = translate_act env in
222 200
  let control_on_clock = control_on_clock env in
223 201
  let reset_instance = reset_instance env in
202
  let mkinstr' = mkinstr ~lustre_eq:eq in
203
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
204
    control_on_clock ck (mkinstr' instr) in
224 205

  
225 206
  (* Format.eprintf "translate_eq %a with clock %a@." 
226 207
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
227 208
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
228 209
  | [x], Expr_arrow (e1, e2)                     ->
229
     let var_x = env.get_var x in
230
     let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
231
     let c1 = translate_expr e1 in
232
     let c2 = translate_expr e2 in
233
     { ctx with
234
       si = mkinstr (MReset o) :: ctx.si;
235
       j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
236
       s = (control_on_clock
237
              eq.eq_rhs.expr_clock
238
              (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
239
           ) :: ctx.s
240
     }
210
    let var_x = env.get_var x in
211
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
212
    let c1 = translate_expr e1 in
213
    let c2 = translate_expr e2 in
214
    { ctx with
215
      si = mkinstr (MReset o) :: ctx.si;
216
      j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
217
      s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
218
    }
241 219
  | [x], Expr_pre e1 when env.is_local x    ->
242
     let var_x = env.get_var x in
243
     
244
      { ctx with
245
        m = VSet.add var_x ctx.m;
246
        s = control_on_clock
247
              eq.eq_rhs.expr_clock
248
              (mkinstr ?lustre_eq:(Some eq)
249
                 (MStateAssign (var_x, translate_expr e1)))
250
            :: ctx.s
251
      }
220
    let var_x = env.get_var x in
221
    { ctx with
222
      m = VSet.add var_x ctx.m;
223
      s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
224
    }
252 225
  | [x], Expr_fby (e1, e2) when env.is_local x ->
253
     let var_x = env.get_var x in
254
     { ctx with
255
       m = VSet.add var_x ctx.m;
256
       si = mkinstr ?lustre_eq:(Some eq)
257
              (MStateAssign (var_x, translate_expr e1))
258
            :: ctx.si;
259
       s = control_on_clock
260
             eq.eq_rhs.expr_clock
261
             (mkinstr ?lustre_eq:(Some eq)
262
                (MStateAssign (var_x, translate_expr e2)))
263
           :: ctx.s
264
     }
265

  
266
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
267
     let var_p = List.map (fun v -> env.get_var v) p in
268
     let el = expr_list_of_expr arg in
269
     let vl = List.map translate_expr el in
270
     let node_f = node_from_name f in
271
     let call_f =
272
       node_f,
273
       NodeDep.filter_static_inputs (node_inputs node_f) el in
274
     let o = new_instance node_f eq.eq_rhs.expr_tag in
275
     let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
276
     let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
277
     (*Clocks.new_var true in
278
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
279
       Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
280
     { ctx with
281
       si = 
282
         (if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si);
226
    let var_x = env.get_var x in
227
    { ctx with
228
      m = VSet.add var_x ctx.m;
229
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
230
      s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
231
    }
232
  | p, Expr_appl (f, arg, r)
233
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
234
    let var_p = List.map (fun v -> env.get_var v) p in
235
    let el = expr_list_of_expr arg in
236
    let vl = List.map translate_expr el in
237
    let node_f = node_from_name f in
238
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
239
    let o = new_instance node_f eq.eq_rhs.expr_tag in
240
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
241
        el [eq.eq_rhs.expr_clock] in
242
    let call_ck = Clock_calculus.compute_root_clock
243
        (Clock_predef.ck_tuple env_cks) in
244
    (*Clocks.new_var true in
245
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
246
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
247
    { ctx with
248
      si = if Stateless.check_node node_f
249
        then ctx.si else mkinstr (MReset o) :: ctx.si;
283 250
      j = Utils.IMap.add o call_f ctx.j;
284 251
      s = (if Stateless.check_node node_f
285
           then []
286
           else reset_instance o r call_ck) @
287
	    (control_on_clock call_ck
288
               (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl))))
289
            :: ctx.s
290
     }
291

  
292
  | [x], _                                       -> (
252
           then [] else reset_instance o r call_ck)
253
          @ ctl ~ck:call_ck (MStep (var_p, o, vl))
254
          :: ctx.s
255
    }
256
  | [x], _ ->
293 257
    let var_x = env.get_var x in
294 258
    { ctx with
295
      s = 
296
     control_on_clock 
297
       eq.eq_rhs.expr_clock
298
       (translate_act (var_x, eq.eq_rhs)) :: ctx.s
299
    }
300
  )
301
  | _                                            ->
302
     begin
303
       Format.eprintf "internal error: Machine_code.translate_eq %a@?"
304
         Printers.pp_node_eq eq;
305
       assert false
306
     end
307

  
308

  
259
      s = control_on_clock eq.eq_rhs.expr_clock
260
          (translate_act (var_x, eq.eq_rhs))
261
          :: ctx.s
262
      }
263
  | _ ->
264
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
265
      Printers.pp_node_eq eq;
266
    assert false
309 267

  
310 268
let constant_equations locals =
311
 VSet.fold (fun vdecl eqs ->
312
   if vdecl.var_dec_const
313
   then
314
     { eq_lhs = [vdecl.var_id];
315
       eq_rhs = Utils.desome vdecl.var_dec_value;
316
       eq_loc = vdecl.var_loc
317
     } :: eqs
318
   else eqs)
319
   locals []
269
  VSet.fold (fun vdecl eqs ->
270
      if vdecl.var_dec_const
271
      then
272
        { eq_lhs = [vdecl.var_id];
273
          eq_rhs = Utils.desome vdecl.var_dec_value;
274
          eq_loc = vdecl.var_loc
275
        } :: eqs
276
      else eqs)
277
    locals []
320 278

  
321 279
let translate_eqs env ctx eqs =
322
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx;;
280
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
323 281

  
324 282

  
325 283
(****************************************************************)
......
327 285
(****************************************************************)
328 286

  
329 287
let process_asserts nd =
330
  
331
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
332
    if Backends.is_functional () then
333
      [], [], exprl  
334
    else (* Each assert(e) is associated to a fresh variable v and declared as
335
	    v=e; assert (v); *)
336
      let _, vars, eql, assertl =
337
	List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
338
	  let loc = expr.expr_loc in
339
	  let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
340
	  let assert_var =
341
	    mkvar_decl
342
	      loc
343
	      ~orig:false (* fresh var *)
344
	      (var_id,
345
	       mktyp loc Tydec_bool,
346
	       mkclock loc Ckdec_any,
347
	       false, (* not a constant *)
348
	       None, (* no default value *)
349
	       Some nd.node_id
350
	      )
351
	  in
352
	  assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
353
	  let eq = mkeq loc ([var_id], expr) in
288

  
289
  let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
290
  if Backends.is_functional () then
291
    [], [], exprl
292
  else (* Each assert(e) is associated to a fresh variable v and declared as
293
          v=e; assert (v); *)
294
    let _, vars, eql, assertl =
295
      List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
296
          let loc = expr.expr_loc in
297
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
298
          let assert_var =
299
            mkvar_decl
300
              loc
301
              ~orig:false (* fresh var *)
302
              (var_id,
303
               mktyp loc Tydec_bool,
304
               mkclock loc Ckdec_any,
305
               false, (* not a constant *)
306
               None, (* no default value *)
307
               Some nd.node_id
308
              )
309
          in
310
          assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
311
          let eq = mkeq loc ([var_id], expr) in
354 312
          (i+1,
355 313
           assert_var::vars,
356 314
           eq::eqlist,
357 315
           {expr with expr_desc = Expr_ident var_id}::assertlist)
358
	) (1, [], [], []) exprl
359
      in
360
      vars, eql, assertl
316
        ) (1, [], [], []) exprl
317
    in
318
    vars, eql, assertl
361 319

  
362 320
let translate_core sorted_eqs locals other_vars =
363 321
  let constant_eqs = constant_equations locals in
364
  
322

  
365 323
  let env = build_env locals other_vars  in
366
  
324

  
367 325
  (* Compute constants' instructions  *)
368 326
  let ctx0 = translate_eqs env ctx_init constant_eqs in
369 327
  assert (VSet.is_empty ctx0.m);
370 328
  assert (ctx0.si = []);
371 329
  assert (Utils.IMap.is_empty ctx0.j);
372
  
330

  
373 331
  (* Compute ctx for all eqs *)
374 332
  let ctx = translate_eqs env ctx_init sorted_eqs in
375
  
333

  
376 334
  ctx, ctx0.s
377 335

  
378
 
336

  
379 337
let translate_decl nd sch =
380 338
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
381 339
  (* Extracting eqs, variables ..  *)
382 340
  let eqs, auts = get_node_eqs nd in
383 341
  assert (auts = []); (* Automata should be expanded by now *)
384
  
342

  
385 343
  (* In case of non functional backend (eg. C), additional local variables have
386 344
     to be declared for each assert *)
387 345
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
......
393 351
  let env = build_env locals inout_vars  in 
394 352

  
395 353
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
396
  
354

  
397 355
  (* Computing main content *)
398 356
  (* Format.eprintf "ok1@.@?"; *)
399 357
  let schedule = sch.Scheduling_type.schedule in
......
403 361
   *   VSet.pp locals
404 362
   *   VSet.pp inout_vars
405 363
   * ; *)
406
  
364

  
407 365
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
408
  
366

  
409 367
  (* Format.eprintf "ok4@.@?"; *)
410 368

  
411 369
  (* Removing computed memories from locals. We also removed unused variables. *)
......
423 381
    mconst = ctx0_s;
424 382
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
425 383
    mstep = {
426
        step_inputs = nd.node_inputs;
427
        step_outputs = nd.node_outputs;
428
        step_locals = updated_locals;
429
        step_checks = List.map (fun d -> d.Dimension.dim_loc,
430
                                         translate_expr env 
431
                                           (expr_of_dimension d))
432
                        nd.node_checks;
433
        step_instrs = (
434
	  (* special treatment depending on the active backend. For horn backend,
435
	   common branches are not merged while they are in C or Java
436
	   backends. *)
437
	  if !Backends.join_guards then
438
	    join_guards_list ctx.s
439
	  else
440
	    ctx.s
441
        );
442
        step_asserts = List.map (translate_expr env) nd_node_asserts;
443
      };
384
      step_inputs = nd.node_inputs;
385
      step_outputs = nd.node_outputs;
386
      step_locals = updated_locals;
387
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
388
                                       translate_expr env
389
                                         (expr_of_dimension d))
390
          nd.node_checks;
391
      step_instrs = (
392
        (* special treatment depending on the active backend. For horn backend,
393
           common branches are not merged while they are in C or Java
394
           backends. *)
395
        if !Backends.join_guards then
396
          join_guards_list ctx.s
397
        else
398
          ctx.s
399
      );
400
      step_asserts = List.map (translate_expr env) nd_node_asserts;
401
    };
444 402

  
445 403
    (* Processing spec: there is no processing performed here. Contract
446
     have been processed already. Either one of the other machine is a
447
     cocospec node, or the current one is a cocospec node. Contract do
448
     not contain any statement or import. *)
449
 
450
    mspec = nd.node_spec;
404
       have been processed already. Either one of the other machine is a
405
       cocospec node, or the current one is a cocospec node. Contract do
406
       not contain any statement or import. *)
407

  
408
    mspec = { mnode_spec = nd.node_spec; mtransitions = [] };
451 409
    mannot = nd.node_annot;
452 410
    msch = Some sch;
453 411
  }
......
457 415
  let nodes = get_nodes decls in
458 416
  let machines =
459 417
    List.map
460
    (fun decl ->
461
     let node = node_of_top decl in
462
      let sch = Utils.IMap.find node.node_id node_schs in
463
      translate_decl node sch
464
    ) nodes
418
      (fun decl ->
419
         let node = node_of_top decl in
420
         let sch = Utils.IMap.find node.node_id node_schs in
421
         translate_decl node sch
422
      ) nodes
465 423
  in
466 424
  machines
467 425

  
468
    (* Local Variables: *)
469
    (* compile-command:"make -C .." *)
470
    (* End: *)
426
(* Local Variables: *)
427
(* compile-command:"make -C .." *)
428
(* End: *)
src/machine_code_common.ml
99 99

  
100 100
let pp_machine fmt m =
101 101
  Format.fprintf fmt
102
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
102
    "@[<v 2>machine %s@ \
103
     mem      : %a@ \
104
     instances: %a@ \
105
     init     : %a@ \
106
     const    : %a@ \
107
     step     :@   \
108
     @[<v 2>%a@]@ \
109
     spec     : @[%t@]@ \
110
     annot    : @[%a@]@]@ "
103 111
    m.mname.node_id
104 112
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
105 113
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
106 114
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
107 115
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
108 116
    (pp_step m) m.mstep
109
    (fun fmt -> match m.mspec with | None -> ()
110
                                   | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
111
                                   | Some (Contract spec) -> Printers.pp_spec fmt spec)
117
    (fun fmt -> match m.mspec.mnode_spec with
118
       | None -> ()
119
       | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
120
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
112 121
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
113 122

  
114 123
let pp_machines fmt ml =
......
185 194
			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
186 195
      step_asserts = [];
187 196
    };
188
    mspec = None;
197
    mspec = { mnode_spec = None; mtransitions = [] };
189 198
    mannot = [];
190 199
    msch = None
191 200
  }
......
226 235
      step_instrs = [];
227 236
      step_asserts = [];
228 237
    };
229
    mspec = None;
238
    mspec = { mnode_spec = None; mtransitions = [] };
230 239
    mannot = [];
231 240
    msch = None
232 241
  }
src/machine_code_types.ml
1 1
(************ Machine code types *************)
2 2
open Lustre_types
3
open Spec_types
3 4
  
4 5
type value_t =
5 6
  {
......
42 43

  
43 44
type static_call = top_decl * (Dimension.dim_expr list)
44 45

  
46
type machine_spec = {
47
  mnode_spec: node_spec_t option;
48
  mtransitions: transition_t list
49
}
45 50
  
46 51
type machine_t = {
47 52
  mname: node_desc;
......
52 57
  mstatic: var_decl list; (* static inputs only *)
53 58
  mconst: instr_t list; (* assignments of node constant locals *)
54 59
  mstep: step_t;
55
  mspec: node_spec_t option;
60
  mspec: machine_spec;
56 61
  mannot: expr_annot list;
57 62
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
58 63
}
src/main_lustre_compiler.ml
77 77
        assert false
78 78
    )
79 79
  in
80
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
81
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
80
  Log.report ~level:3 (fun fmt -> fprintf fmt "@ @[<v 2>.. Normalized program:@ %a@]"
81
                          Printers.pp_prog prog);
82 82

  
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ @ @[<v 2>.. Phase 2 : Machines generation@,");
84 84

  
85 85
  let prog, machine_code = 
86 86
    Compiler_stages.stage2 params prog 
87 87
  in
88 88

  
89
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " Machine_code_common.pp_machines machine_code);
89
  Log.report ~level:3 (fun fmt -> fprintf fmt "@ @[<v 2>.. Generated machines:@ %a@]"
90
                          Machine_code_common.pp_machines machine_code);
90 91

  
91 92
  if Scopes.Plugin.show_scopes () then
92 93
    begin
......
103 104
  
104 105
  Compiler_stages.stage3 prog machine_code dependencies basename extension;
105 106
  begin
106
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
107
    Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. done !@]@.");
107 108
    (* We stop the process here *)
108 109
    exit 0
109 110
  end
src/optimize_machine.ml
20 20

  
21 21

  
22 22
let pp_elim m fmt elim =
23
  begin
24
    Format.fprintf fmt "@[{ /* elim table: */@ ";
25
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v (pp_val m) expr) elim;
26
    Format.fprintf fmt "}@ @]";
27
  end
23
  pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
24
  (* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
25
   * IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
26
   * Format.fprintf fmt "@]@ }@]" *)
28 27

  
29 28
let rec eliminate m elim instr =
30 29
  let e_expr = eliminate_expr m elim in
......
246 245
    
247 246
*)
248 247
let machine_unfold fanin elim machine =
249
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@." machine.mname.node_id (pp_elim machine) (IMap.map fst elim)); 
248
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@ "
249
                          machine.mname.node_id (pp_elim machine) (IMap.map fst elim));
250 250
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
251 251
  let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
252 252
  let instrs = simplify_instrs_offset machine instrs in
......
291 291
   contracts. *)
292 292
let machines_unfold consts node_schs machines =
293 293
  List.fold_right (fun m (machines, removed) ->
294
      let is_contract = match m.mspec with Some (Contract _) -> true | _ -> false in
294
      let is_contract = match m.mspec.mnode_spec with
295
        | Some (Contract _) -> true
296
        | _ -> false in
295 297
      if is_contract then
296
        m::machines, removed
298
        m :: machines, removed
297 299
      else 
298 300
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
299 301
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
......
688 690
*)
689 691
let optimize params prog node_schs machine_code =
690 692
  let machine_code =
691
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
692
      begin
693
	Log.report ~level:1 
694
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
695
	let machine_code = machines_cse machine_code in
696
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code);
697
	machine_code
698
      end
699
    else
693
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then begin
694
      Log.report ~level:1
695
        (fun fmt -> Format.fprintf fmt "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
696
      let machine_code = machines_cse machine_code in
697
      Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ "
698
                              pp_machines machine_code);
699
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
700
      machine_code
701
    end else
700 702
      machine_code
701 703
  in
702 704
  (* Optimize machine code *)
703 705
  let prog, machine_code, removed_table = 
704 706
    if !Options.optimization >= 2
705
       && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
706
    then
707
      begin
708
	Log.report ~level:1
709
          (fun fmt ->
710
            Format.fprintf fmt 
711
	      ".. machines optimization: const. inlining (partial eval. with const)@,");
712
	let machine_code, removed_table =
713
          machines_unfold (Corelang.get_consts prog) node_schs machine_code in
714
  Log.report ~level:3
715
          (fun fmt ->
716
            Format.fprintf fmt "\t@[Eliminated flows: @[%a@]@]@ "
717
	      (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m))) removed_table); 
718
	Log.report ~level:3
719
          (fun fmt ->
720
            Format.fprintf fmt
721
              ".. generated machines (const inlining):@ %a@ "
722
              pp_machines machine_code);
723
        (* If variables were eliminated, relaunch the
724
           normalization/machine generation *)
707
    && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
708
    then begin
709
      Log.report ~level:1
710
        (fun fmt ->
711
           Format.fprintf fmt
712
             "@ @[<v 2>.. machines optimization: const. inlining (partial eval. with const)@ ");
713
      let machine_code, removed_table =
714
        machines_unfold (Corelang.get_consts prog) node_schs machine_code in
715
      Log.report ~level:3
716
        (fun fmt ->
717
           Format.fprintf fmt "@ Eliminated flows: %a@ "
718
             (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m))) removed_table);
719
      Log.report ~level:3
720
        (fun fmt ->
721
           Format.fprintf fmt
722
             "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
723
             pp_machines machine_code);
724
      (* If variables were eliminated, relaunch the
725
         normalization/machine generation *)
726
      let prog, machine_code, removed_table =
725 727
        if IMap.is_empty removed_table then
726
	  (* stopping here, no need to reupdate the prog *)
728
          (* stopping here, no need to reupdate the prog *)
727 729
          prog, machine_code, removed_table
728 730
        else (
729 731
          let prog = elim_prog_variables prog removed_table in
......
734 736
             alg. loop since this should have been handled before *)
735 737
          let prog, node_schs = Scheduling.schedule_prog prog in
736 738
          let machine_code = Machine_code.translate_prog prog node_schs in
737
	  (* Mini stage2 machine optimiation *)
739
          (* Mini stage2 machine optimiation *)
738 740
          let machine_code, removed_table =
739 741
            machines_unfold (Corelang.get_consts prog) node_schs machine_code in
740
	  prog, machine_code, removed_table
742
          prog, machine_code, removed_table
741 743
        )
744
        in
745
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
746
        prog, machine_code, removed_table
742 747

  
743
      end
744
    else
748
    end else
745 749
      prog, machine_code, IMap.empty
746 750
  in  
747 751
  (* Optimize machine code *)
748 752
  let machine_code =
749 753
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
750 754
      begin
751
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
752
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
753
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
754
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
755
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
756
        let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
757
        let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
758
        machines_fusion (machines_reuse_variables machine_code reuse_tables)
755 759
      end
756 760
    else
757 761
      machine_code
758 762
  in
759
  
763

  
760 764

  
761 765
  prog, List.rev machine_code  
762
          
766

  
763 767
          
764 768
                 (* Local Variables: *)
765 769
                 (* compile-command:"make -C .." *)
src/printers.ml
10 10
(********************************************************************)
11 11

  
12 12
open Lustre_types
13
open Format
14 13
open Utils
14
open Format
15 15

  
16 16
let kind2_language_cst =
17 17
  [ "initial" ]
......
348 348
  | Eq eq -> pp_node_eq fmt eq
349 349
  | Aut aut -> pp_node_aut fmt aut
350 350

  
351
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
351
and pp_node_stmts fmt stmts =
352
  pp_print_list
353
    ~pp_open_box:pp_open_vbox0
354
    ~pp_sep:pp_print_cut
355
    pp_node_stmt fmt stmts
352 356

  
353 357
and pp_node_aut fmt aut =
354 358
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
......
475 479
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
476 480
  
477 481
let pp_node fmt nd =
478
  fprintf fmt "@[<v 0>";
479 482
  (* Prototype *)
480 483
  fprintf fmt  "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
481 484
    pp_node_vs_function nd
......
484 487
    pp_node_args nd.node_outputs;
485 488
  (* Contracts *)
486 489
  fprintf fmt "%a"
487
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
490
    (fun fmt s -> match s with
491
       | Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
492
       | _ -> ()) nd.node_spec
488 493
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
489 494
  (* Locals *)
490 495
  fprintf fmt "%a" (fun fmt locals ->
491
      match locals with [] -> () | _ ->
492
                                    fprintf fmt "@[<v 4>var %a@]@ " 
493
                                      (fprintf_list ~sep:"@ " 
494
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
495
                                      locals
496
      match locals with
497
      | [] -> ()
498
      | _ ->
499
        fprintf fmt "@[<v 4>var %a@]@ "
500
          (fprintf_list ~sep:"@ "
501
	           (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
502
          locals
496 503
    ) nd.node_locals;
497 504
  (* Checks *)
498 505
  fprintf fmt "%a"
499 506
    (fun fmt checks ->
500
      match checks with [] -> () | _ ->
501
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
502
                                      (fprintf_list ~sep:"@ " 
503
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
504
                                      checks
507
       match checks with
508
       | [] -> ()
509
       | _ ->
510
         fprintf fmt "@[<v 4>check@ %a@]@ "
511
           (fprintf_list ~sep:"@ "
512
	            (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
513
           checks
505 514
    ) nd.node_checks;
506 515
  (* Body *)
507
  fprintf fmt "let@[<h 2>   @ @[<v>";
516
  fprintf fmt "@[<v 2>let@ ";
508 517
  (* Annotations *)
509
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
518
  fprintf fmt "%a" (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
510 519
  (* Statements *)
511
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
520
  fprintf fmt "%a" pp_node_stmts nd.node_stmts;
512 521
  (* Asserts *)    
513 522
  fprintf fmt "%a" pp_asserts nd.node_asserts;
514 523
  (* closing boxes body (2)  and node (1) *) 
515
  fprintf fmt "@]@]@ tel@]@ "
524
  fprintf fmt "@]@ tel"
516 525

  
517 526

  
518 527
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
......
520 529
let pp_node fmt nd =
521 530
  match nd.node_spec, nd.node_iscontract with
522 531
  | None, false
523
    | Some (NodeSpec _), false 
524
    -> pp_node fmt nd
525
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
526
  | Some (Contract _), true -> pp_contract fmt nd 
532
  | Some (NodeSpec _), false ->
533
    pp_node fmt nd
534
  | Some (Contract _), false ->
535
    pp_node fmt nd (* may happen early in the compil process *)
536
  | Some (Contract _), true ->
537
    pp_contract fmt nd
527 538
  | _ -> assert false
528 539
     
529 540
let pp_imported_node fmt ind = 
......
547 558
let pp_const_decl_list fmt clist = 
548 559
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
549 560

  
550

  
551 561
  
552 562
let pp_decl fmt decl =
553 563
  match decl.top_decl_desc with
554
  | Node nd -> fprintf fmt "%a" pp_node nd
564
  | Node nd ->
565
    fprintf fmt "%a" pp_node nd
555 566
  | ImportedNode ind -> (* We do not print imported nodes *)
556 567
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
557
  | Const c -> fprintf fmt "const %a" pp_const_decl c
558
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
559
  | Include s -> fprintf fmt "include \"%s\"" s
560
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
568
  | Const c ->
569
    fprintf fmt "const %a" pp_const_decl c
570
  | Open (local, s) ->
571
    if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
572
  | Include s ->
573
    fprintf fmt "include \"%s\"" s
574
  | TypeDef tdef ->
575
    fprintf fmt "%a" pp_typedef tdef
561 576
  
562 577
let pp_prog pp_decl fmt prog =
563 578
  (* we first print types: the function SortProg.sort could do the job but ut
564 579
     introduces a cyclic dependance *)
565 580

  
566 581
  let open_decl, prog =
567
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
582
    List.partition (fun decl -> match decl.top_decl_desc with
583
          Open _ -> true | _ -> false) prog
568 584
  in
569 585
  let type_decl, prog =
570
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
586
    List.partition (fun decl -> match decl.top_decl_desc with
587
          TypeDef _ -> true | _ -> false) prog
571 588
  in
572
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
589
  pp_print_list
590
    ~pp_open_box:pp_open_vbox0
591
    ~pp_sep:pp_print_cutcut
592
    pp_decl
593
    fmt
594
    (open_decl @ type_decl @ prog)
573 595

  
574 596
(* Gives a short overview of model content. Do not print all node content *)
575 597
let pp_short_decl fmt decl =
src/scheduling.ml
120 120

  
121 121
let schedule_node n =
122 122
  (* let node_vars = get_node_vars n in *)
123
  Log.report ~level:5 (fun fmt -> Format.fprintf fmt "scheduling node %s@," n.node_id);
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 126
  let n', g = global_dependency n in
......
177 177
    fun top_decl (accu_prog, sch_map)  ->
178 178
      match top_decl.top_decl_desc with
179 179
      | Node nd ->
180
	let report = schedule_node nd in
181
	{top_decl with top_decl_desc = Node report.node}::accu_prog, 
182
	IMap.add nd.node_id report sch_map
183
	| _ -> top_decl::accu_prog, sch_map
184
    ) 
180
        let report = schedule_node nd in
181
        {top_decl with top_decl_desc = Node report.node}::accu_prog,
182
        IMap.add nd.node_id report sch_map
183
      | _ -> top_decl::accu_prog, sch_map
184
  )
185 185
    prog
186 186
    ([],IMap.empty)
187
  
187

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff