Project

General

Profile

Revision b3f91fdb

View differences:

src/clocks.ml
72 72
exception Scope_clock of clock_expr
73 73
exception Error of Location.t * error
74 74

  
75
let print_ckset fmt s =
76
  match s with
77
  | CSet_all -> ()
78
  | CSet_pck (k,q) ->
79
      let (a,b) = simplify_rat q in
80
      if k = 1 && a = 0 then
81
        fprintf fmt "<:P"
82
      else
83
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
84

  
85
let rec print_carrier fmt cr =
86
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
87
  match cr.carrier_desc with
88
  | Carry_const id -> fprintf fmt "%s" id
89
  | Carry_name ->
90
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
91
  | Carry_var ->
92
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
93
  | Carry_link cr' ->
94
    print_carrier fmt cr'
95

  
96
(* Simple pretty-printing, performs no simplifications. Linear
97
   complexity. For debug mainly. *)
98
let rec print_ck_long fmt ck =
99
  match ck.cdesc with
100
  | Carrow (ck1,ck2) ->
101
      fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
102
  | Ctuple cklist ->
103
    fprintf fmt "(%a)"
104
      (fprintf_list ~sep:" * " print_ck_long) cklist
105
  | Con (ck,c,l) ->
106
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
107
  | Pck_up (ck,k) ->
108
    fprintf fmt "%a*^%i" print_ck_long ck k
109
  | Pck_down (ck,k) ->
110
    fprintf fmt "%a/^%i" print_ck_long ck k
111
  | Pck_phase (ck,q) ->
112
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
113
  | Pck_const (n,p) ->
114
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
115
  | Cvar cset ->
116
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
117
  | Cunivar cset ->
118
    fprintf fmt "'%i%a" ck.cid print_ckset cset
119
  | Clink ck' ->
120
    fprintf fmt "link %a" print_ck_long ck'
121
  | Ccarrying (cr,ck') ->
122
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
123

  
75 124
let new_id = ref (-1)
76 125

  
77 126
let new_ck desc scoped =
......
117 166
 | Ccarrying (cr, _) -> Some cr
118 167
 | _                 -> None
119 168

  
169
let rename_carrier_static rename cr =
170
  match (carrier_repr cr).carrier_desc with
171
  | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
172
  | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
173

  
174
let rec rename_static rename ck =
175
 match (repr ck).cdesc with
176
 | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
177
 | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
178
 | _                   -> ck
179

  
120 180
let uncarrier ck =
121 181
 match ck.cdesc with
122 182
 | Ccarrying (_, ck') -> ck'
......
257 317
  in
258 318
  aux [] ck
259 319

  
260
let print_ckset fmt s =
261
  match s with
262
  | CSet_all -> ()
263
  | CSet_pck (k,q) ->
264
      let (a,b) = simplify_rat q in
265
      if k = 1 && a = 0 then
266
        fprintf fmt "<:P"
267
      else
268
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
269

  
270
let rec print_carrier fmt cr =
271
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
272
  match cr.carrier_desc with
273
  | Carry_const id -> fprintf fmt "%s" id
274
  | Carry_name ->
275
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
276
  | Carry_var ->
277
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
278
  | Carry_link cr' ->
279
    print_carrier fmt cr'
280

  
281
(* Simple pretty-printing, performs no simplifications. Linear
282
   complexity. For debug mainly. *)
283
let rec print_ck_long fmt ck =
284
  match ck.cdesc with
285
  | Carrow (ck1,ck2) ->
286
      fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
287
  | Ctuple cklist ->
288
    fprintf fmt "(%a)"
289
      (fprintf_list ~sep:" * " print_ck_long) cklist
290
  | Con (ck,c,l) ->
291
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
292
  | Pck_up (ck,k) ->
293
    fprintf fmt "%a*^%i" print_ck_long ck k
294
  | Pck_down (ck,k) ->
295
    fprintf fmt "%a/^%i" print_ck_long ck k
296
  | Pck_phase (ck,q) ->
297
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
298
  | Pck_const (n,p) ->
299
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
300
  | Cvar cset ->
301
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
302
  | Cunivar cset ->
303
    fprintf fmt "'%i%a" ck.cid print_ckset cset
304
  | Clink ck' ->
305
    fprintf fmt "link %a" print_ck_long ck'
306
  | Ccarrying (cr,ck') ->
307
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
308

  
309 320
(** [period ck] returns the period of [ck]. Expects a constant pclock
310 321
    expression belonging to the correct clock set. *)
311 322
let rec period ck =
src/corelang.ml
376 376
 | Expr_ident id -> id
377 377
 | _             -> assert false
378 378

  
379
(* Generate a new ident expression from a declared variable *)
380
let expr_of_vdecl v =
381
  { expr_tag = Utils.new_tag ();
382
    expr_desc = Expr_ident v.var_id;
383
    expr_type = v.var_type;
384
    expr_clock = v.var_clock;
385
    expr_delay = Delay.new_var ();
386
    expr_annot = None;
387
    expr_loc = v.var_loc }
388

  
379 389
(* Caution, returns an untyped and unclocked expression *)
380 390
let expr_of_ident id loc =
381 391
  {expr_tag = Utils.new_tag ();
......
429 439
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
430 440
 | Dlink dim'       -> expr_of_dimension dim'
431 441
 | Dvar
432
 | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
442
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
433 443
			assert false)
434 444

  
435 445
let dimension_of_const loc const =
......
478 488
let get_node_vars nd =
479 489
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
480 490

  
491
let mk_new_node_name nd id =
492
  let used_vars = get_node_vars nd in
493
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
494
  mk_new_name used id
495

  
481 496
let get_var id var_list =
482 497
    List.find (fun v -> v.var_id = id) var_list
483 498

  
src/corelang.mli
27 27
val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
28 28
val mkpredef_call: Location.t -> ident -> expr list -> expr
29 29
val mk_new_name: (ident -> bool) -> ident -> ident
30

  
30
val mk_new_node_name: node_desc -> ident -> ident
31 31

  
32 32
val node_table : (ident, top_decl) Hashtbl.t
33 33
val print_node_table:  Format.formatter -> unit -> unit
......
81 81
(* Caution, returns an untyped, unclocked, etc, expression *)
82 82
val is_tuple_expr : expr -> bool
83 83
val ident_of_expr : expr -> ident
84
val expr_of_vdecl : var_decl -> expr
84 85
val expr_of_ident : ident -> Location.t -> expr
85 86
val expr_list_of_expr : expr -> expr list
86 87
val expr_of_expr_list : Location.t -> expr list -> expr
src/dimension.ml
339 339
  in unif dim1 dim2
340 340

  
341 341
let rec expr_replace_var fvar e = 
342
 { e with dim_desc = expr_replace_desc fvar e.dim_desc }
343
and expr_replace_desc fvar e =
342
 { e with dim_desc = expr_replace_var_desc fvar e.dim_desc }
343
and expr_replace_var_desc fvar e =
344 344
  let re = expr_replace_var fvar in
345 345
  match e with
346 346
  | Dvar
......
351 351
  | Dappl (id, el) -> Dappl (id, List.map re el)
352 352
  | Dite (g,t,e) -> Dite (re g, re t, re e)
353 353
  | Dlink e -> Dlink (re e)
354

  
355
let rec expr_replace_expr fvar e = 
356
 { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
357
and expr_replace_expr_desc fvar e =
358
  let re = expr_replace_expr fvar in
359
  match e with
360
  | Dvar
361
  | Dunivar
362
  | Dbool _
363
  | Dint _ -> e
364
  | Dident v -> (fvar v).dim_desc
365
  | Dappl (id, el) -> Dappl (id, List.map re el)
366
  | Dite (g,t,e) -> Dite (re g, re t, re e)
367
  | Dlink e -> Dlink (re e)
src/inliner.ml
27 27
  | Node nd -> nd.node_id = id 
28 28
  | _ -> false) 
29 29

  
30
let get_static_inputs node args =
31
  List.fold_right2 (fun vdecl arg static ->
32
    if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
33
    node.node_inputs
34
    (Corelang.expr_list_of_expr args)
35
    []
36

  
37
let get_carrier_inputs node args =
38
  List.fold_right2 (fun vdecl arg carrier ->
39
    if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
40
    node.node_inputs
41
    (Corelang.expr_list_of_expr args)
42
    []
43

  
44
let is_node_var node v =
45
 try
46
   ignore (Corelang.get_node_var v node); true
47
 with Not_found -> false
30 48

  
31 49
let rename_expr rename expr = expr_replace_var rename expr
50

  
32 51
let rename_eq rename eq = 
33 52
  { eq with
34 53
    eq_lhs = List.map rename eq.eq_lhs; 
......
36 55
  }
37 56

  
38 57
(* 
39
    expr, locals', eqs = inline_call id args' reset locals nodes
58
    expr, locals', eqs = inline_call id args' reset locals node nodes
40 59

  
41 60
We select the called node equations and variables.
42 61
   renamed_inputs = args
......
47 66
TODO: convert the specification/annotation/assert and inject them
48 67
TODO: deal with reset
49 68
*)
50
let inline_call orig_expr args reset locals node =
69
let inline_call node orig_expr args reset locals caller =
51 70
  let loc = orig_expr.expr_loc in
52 71
  let uid = orig_expr.expr_tag in
53 72
  let rename v =
54
    if v = tag_true || v = tag_false then v else
55
    (Format.fprintf Format.str_formatter "%s_%i_%s" 
56
      node.node_id uid v;
57
    Format.flush_str_formatter ())
73
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
74
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
58 75
  in
59 76
  let eqs' = List.map (rename_eq rename) (get_node_eqs node)
60 77
  in
61
  let rename_var v = { v with var_id = rename v.var_id } in
78
  let static_inputs = get_static_inputs node args in
79
  let carrier_inputs = get_carrier_inputs node args in
80
  let rename_static v =
81
    try
82
      List.assoc v static_inputs
83
    with Not_found -> Dimension.mkdim_ident loc v
84
    (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
85
  in
86
  let rename_carrier v =
87
    try
88
      List.assoc v carrier_inputs
89
    with Not_found -> v in
90
  let rename_var v =
91
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
92
    { v with
93
      var_id = rename v.var_id;
94
      var_type = Types.rename_static rename_static v.var_type;
95
      var_clock = Clocks.rename_static rename_carrier v.var_clock;
96
    } in
62 97
  let inputs' = List.map rename_var node.node_inputs in
63 98
  let outputs' = List.map rename_var node.node_outputs in
64 99
  let locals' = List.map rename_var node.node_locals in
65

  
66 100
  (* checking we are at the appropriate (early) step: node_checks and
67 101
     node_gencalls should be empty (not yet assigned) *)
68 102
  assert (node.node_checks = []);
......
72 106
  assert (reset = None);
73 107

  
74 108
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
75
  let expr = expr_of_expr_list 
76
    loc 
77
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
109
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
78 110
  in
79 111
  let asserts' = (* We rename variables in assert expressions *)
80 112
    List.map 
......
92 124

  
93 125

  
94 126

  
127
let inline_table = Hashtbl.create 23
95 128

  
96 129
(* 
97
   new_expr, new_locals, new_eqs = inline_expr expr locals nodes
130
   new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
98 131
   
99 132
   Each occurence of a node in nodes in the expr should be replaced by fresh
100 133
   variables and the code of called node instance added to new_eqs
101 134

  
102 135
*)
103
let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
136
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
104 137
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
105 138
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
106 139
  let inline_tuple el = 
107 140
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
108
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
141
      let e', locals', eqs', asserts' = inline_expr e locals node nodes in
109 142
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
110 143
    ) el ([], locals, [], [])
111 144
  in
......
124 157
  
125 158
  match expr.expr_desc with
126 159
  | Expr_appl (id, args, reset) ->
127
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
160
    let args', locals', eqs', asserts' = inline_expr args locals node nodes in 
128 161
    if List.exists (check_node_name id) nodes && (* the current node call is provided
129 162
						    as arguments nodes *)
130 163
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
131 164
							      it is explicitely inlined here *)
132 165
    then 
133 166
      (* The node should be inlined *)
134
       let _ =     Format.eprintf "Inlining call to %s@." id in 
135
      let node = try List.find (check_node_name id) nodes 
167
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
168
      let called = try List.find (check_node_name id) nodes 
136 169
	with Not_found -> (assert false) in
137
      let node = node_of_top node in
138
      let node = inline_node node nodes in
170
      let called = node_of_top called in
171
      let called' = inline_node called nodes in
139 172
      let expr, locals', eqs'', asserts'' = 
140
	inline_call expr args' reset locals' node in
173
	inline_call called' expr args' reset locals' node in
141 174
      expr, locals', eqs'@eqs'', asserts'@asserts''
142 175
    else 
143 176
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
......
165 198
    let el', l', eqs', asserts' = inline_tuple el in
166 199
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
167 200
  | Expr_access (e, dim) ->
168
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
201
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
169 202
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
170 203
  | Expr_power (e, dim) ->
171
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
204
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
172 205
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
173 206
  | Expr_pre e ->
174
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
207
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
175 208
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
176 209
  | Expr_when (e, id, label) ->
177
    let e', l', eqs', asserts' = inline_expr e locals nodes in 
210
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
178 211
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
179 212
  | Expr_merge (id, branches) ->
180 213
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
181 214
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
182 215
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
183
and inline_node ?(selection_on_annotation=false) nd nodes = 
216

  
217
and inline_node ?(selection_on_annotation=false) node nodes =
218
  try Hashtbl.find inline_table node.node_id
219
  with Not_found ->
184 220
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
185 221
  let new_locals, eqs, asserts = 
186 222
    List.fold_left (fun (locals, eqs, asserts) eq ->
187 223
      let eq_rhs', locals', new_eqs', asserts' = 
188
	inline_expr eq.eq_rhs locals nodes 
224
	inline_expr eq.eq_rhs locals node nodes 
189 225
      in
190 226
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
191
    ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
227
    ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
192 228
  in
193
  { nd with
229
  let inlined = 
230
  { node with
194 231
    node_locals = new_locals;
195 232
    node_stmts = List.map (fun eq -> Eq eq) eqs;
196 233
    node_asserts = asserts;
197 234
  }
235
  in
236
  begin
237
    (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
238
    Hashtbl.add inline_table node.node_id inlined;
239
    inlined
240
  end
198 241

  
199 242
let inline_all_calls node nodes =
200 243
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
......
299 342
  in
300 343
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
301 344
  let new_prog = others@nodes_origs@nodes_inlined@main in
345

  
302 346
  let _ = Typing.type_prog type_env new_prog in
303 347
  let _ = Clock_calculus.clock_prog clock_env new_prog in
304 348

  
src/main_lustre_compiler.ml
123 123
      exit 0
124 124
    end;
125 125

  
126
  (* Perform global inlining *)
127
  let prog =
128
    if !Options.global_inline &&
129
      (match !Options.main_node with | "" -> false | _ -> true) then
130
      Inliner.global_inline basename prog type_env clock_env
131
    else (* if !Option.has_local_inline *)
132
      Inliner.local_inline basename prog type_env clock_env
133
  in
134

  
135 126
  (* Delay calculus *)
136 127
  (* TO BE DONE LATER (Xavier)
137 128
    if(!Options.delay_calculus)
......
159 150
  Typing.uneval_prog_generics prog;
160 151
  Clock_calculus.uneval_prog_generics prog;
161 152

  
153
  (* Perform global inlining *)
154
  let prog =
155
    if !Options.global_inline &&
156
      (match !Options.main_node with | "" -> false | _ -> true) then
157
      Inliner.global_inline basename prog type_env clock_env
158
    else (* if !Option.has_local_inline *)
159
      Inliner.local_inline basename prog type_env clock_env
160
  in
161
(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
162 162
  (* Computes and stores generic calls for each node,
163 163
     only useful for ANSI C90 compliant generic node compilation *)
164 164
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
......
170 170
  if !Options.output = "lustre" then
171 171
    Normalization.unfold_arrow_active := false;
172 172
  let prog = Normalization.normalize_prog prog in
173

  
173 174
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
174 175
  (* Checking array accesses *)
175 176
  if !Options.check then
src/normalization.ml
75 75
  }
76 76
  in aux ()
77 77

  
78
(* Generate a new ident expression from a declared variable *)
79
let mk_ident_expr v =
80
  { expr_tag = new_tag ();
81
    expr_desc = Expr_ident v.var_id;
82
    expr_type = v.var_type;
83
    expr_clock = v.var_clock;
84
    expr_delay = Delay.new_var ();
85
    expr_annot = None;
86
    expr_loc = v.var_loc }
87

  
88 78
(* Get the equation in [defs] with [expr] as rhs, if any *)
89 79
let get_expr_alias defs expr =
90 80
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
......
100 90
   expr_desc = Expr_ident v.var_id }
101 91
 | _   -> { expr with
102 92
   expr_tag = Utils.new_tag ();
103
   expr_desc = Expr_tuple (List.map mk_ident_expr locals) }
93
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
104 94

  
105 95
let unfold_offsets e offsets =
106 96
  let add_offset e d =
107
(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*)
97
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
98
    let res = *)
108 99
    { e with
109 100
      expr_tag = Utils.new_tag ();
110 101
      expr_loc = d.Dimension.dim_loc;
111 102
      expr_type = Types.array_element_type e.expr_type;
112
      expr_desc = Expr_access (e, d) } in
103
      expr_desc = Expr_access (e, d) }
104
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
105
  in
113 106
 List.fold_left add_offset e offsets
114 107

  
115 108
(* Create an alias for [expr], if none exists yet *)
......
128 121
    let new_def =
129 122
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
130 123
    in
131
    (* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
124
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
132 125
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
133 126

  
134 127
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
......
149 142
   taking propagated [offsets] into account 
150 143
   in order to change expression type *)
151 144
let mk_norm_expr offsets ref_e norm_d =
145
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
152 146
  let drop_array_type ty =
153 147
    Types.map_tuple_type Types.array_element_type ty in
154 148
  { ref_e with
......
301 295
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
302 296
			    then
303 297
			      let newvar = mk_fresh_var node eq.eq_loc t c in
304
			      let neweq  = mkeq eq.eq_loc ([v], mk_ident_expr newvar) in
298
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
305 299
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
306 300
			    else
307 301
			      (defs_q, vars_q), v::lhs_q
src/types.ml
193 193
  | Tstatic (d, _) -> Some d
194 194
  | _              -> None
195 195

  
196
let rec rename_static rename ty =
197
 match (repr ty).tdesc with
198
 | Tstatic (d, ty') -> { ty with tdesc = Tstatic (Dimension.expr_replace_expr rename d, rename_static rename ty') }
199
 | Tarray  (d, ty') -> { ty with tdesc = Tarray  (Dimension.expr_replace_expr rename d, rename_static rename ty') }
200
 | _                -> ty
201
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
202

  
196 203
let get_field_type ty label =
197 204
  match (repr ty).tdesc with
198 205
  | Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
......
254 261
let array_type_dimension ty =
255 262
  match (dynamic_type ty).tdesc with
256 263
  | Tarray (d, _) -> d
257
  | _             -> assert false
264
  | _             -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)
258 265

  
259 266
let rec array_type_multi_dimension ty =
260 267
  match (dynamic_type ty).tdesc with
......
264 271
let array_element_type ty =
265 272
  match (dynamic_type ty).tdesc with
266 273
  | Tarray (_, ty') -> ty'
267
  | _               -> assert false
274
  | _               -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)
268 275

  
269 276
let rec array_base_type ty =
270 277
  let ty = repr ty in
src/typing.ml
566 566
 | _                   -> ()
567 567

  
568 568
let type_var_decl vd_env env vdecl =
569
(*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)
569 570
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
570 571
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
571 572
  let type_dim d =
......
581 582
  let new_env = Env.add_value env vdecl.var_id ty_status in
582 583
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
583 584
  vdecl.var_type <- ty_status;
585
(*Format.eprintf "END@.";*)
584 586
  new_env
585 587

  
586 588
let type_var_decl_list vd_env env l =
test/test-compile.sh
14 14
mkdir -p build
15 15
build=`pwd`"/build"
16 16

  
17
gcc_compile() {
18
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
19
    if [ $? -ne 0 ]; then
20
	rgcc="INVALID";
21
    else
22
	rgcc="VALID"
23
    fi
24
}
25

  
26
lustrec_compile() {
27
    $LUSTREC "$@";
28
    if [ $? -ne 0 ]; then
29
        rlustrec="INVALID";
30
    else
31
        rlustrec="VALID"
32
    fi
33
}
17 34

  
18 35
base_compile() {
19 36
    while IFS=, read -r file main opts
......
26 43
	fi
27 44
        dir=${SRC_PREFIX}/`dirname "$file"`
28 45
	pushd $dir > /dev/null
29
    if [ "$main" != "" ]; then
30
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
31
        if [ $? -ne 0 ]; then
32
            rlustrec1="INVALID";
33
        else
34
            rlustrec1="VALID"
35
	fi
36
	pushd $build > /dev/null
37
	if [ $ext = ".lus" ]; then
38
            gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
39
            if [ $? -ne 0 ]; then
40
		rgcc1="INVALID";
41
            else
42
		rgcc1="VALID"
43
	    fi
46

  
47
	if [ "$main" != "" ]; then
48
	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
44 49
	else
45
	    rgcc1="NONE"
50
	    lustrec_compile -d $build -verbose 0 $opts $name$ext
46 51
	fi
47
	popd > /dev/null
48
    else
49
	$LUSTREC -d $build -verbose 0 $opts "$name""$ext";
50
        if [ $? -ne 0 ]; then
51
            rlustrec1="INVALID";
52
        else
53
            rlustrec1="VALID"
54
        fi
55 52
	pushd $build > /dev/null
53

  
56 54
	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
57
            gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
58
            if [ $? -ne 0 ]; then
59
		rgcc1="INVALID";
60
            else
61
		rgcc1="VALID"
62
            fi
55
            gcc_compile "$name";
63 56
	else
64
	    rgcc1="NONE"
57
	    rgcc="NONE"
65 58
	fi
66 59
	popd > /dev/null
67
    fi
68
    popd > /dev/null
69
    if [ $verbose -gt 0 ]; then
70
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
71
    else
72
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
73
    fi;
60
	popd > /dev/null
61

  
62
	if [ $verbose -gt 0 ]; then
63
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
64
	else
65
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
66
	fi;
74 67
    done < $file_list
75 68
}
76 69

  
......
78 71
    while IFS=, read -r file main opts
79 72
    do
80 73
	name=`basename "$file" .lus`
74
	ext=".lus"
81 75
	if [ `dirname "$file"`/"$name" = "$file" ]; then
82
	    return 0
76
	    name=`basename "$file" .lusi`
77
	    ext=".lusi"
83 78
	fi
84 79
	dir=${SRC_PREFIX}/`dirname "$file"`
85

  
86 80
	pushd $dir > /dev/null
87 81

  
88
# Checking inlining
89
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
90
    if [ $? -ne 0 ]; then
91
        rlustrec2="INVALID";
92
    else
93
        rlustrec2="VALID"
94
    fi
95
    pushd $build > /dev/null
96
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
97
    if [ $? -ne 0 ]; then
98
        rgcc2="INVALID";
99
    else
100
        rgcc2="VALID"
101
    fi
102
    popd > /dev/null
103
    if [ $verbose -gt 0 ]; then
104
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
105
    else
106
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
107
    fi;
108
    popd > /dev/null
109
done < $file_list
82
	if [ "$main" != "" ]; then
83
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
84
	else
85
	    if [ "$ext" = ".lusi" ]; then
86
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
87
	    else
88
		rlustrec="NONE"
89
		rgcc="NONE"
90
	    fi
91
	fi
92
	pushd $build > /dev/null
93

  
94
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
95
	    gcc_compile "$name";
96
	else
97
	    rgcc="NONE"
98
	fi
99
	popd > /dev/null
100
	popd > /dev/null
101

  
102
	if [ $verbose -gt 0 ]; then
103
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
104
	else
105
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
106
	fi;
107
    done < $file_list
110 108
}
111 109

  
112 110
inline_compile_with_check () {
......
119 117
	fi
120 118
	dir=${SRC_PREFIX}/`dirname "$file"`
121 119
	pushd $dir > /dev/null
122
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
123
    if [ $? -ne 0 ]; then
124
        rlustrec2="INVALID";
125
    else
126
        rlustrec2="VALID"
127
    fi
120
    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
121

  
128 122
    pushd $build > /dev/null
129
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
130
    if [ $? -ne 0 ]; then
131
        rgcc2="INVALID";
132
    else
133
        rgcc2="VALID"
134
    fi	
123
    gcc_compile "$name"
124
	
135 125
    popd > /dev/null
136 126
	# Cheching witness
137 127
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
128
    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
139 129
    popd > /dev/null
140 130
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 131
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
148 138
	rinlining="INVALID/TIMEOUT"
149 139
    fi  
150 140
    if [ $verbose -gt 0 ]; then
151
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
141
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
152 142
    else
153
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
143
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
154 144
    fi
155 145
    popd > /dev/null
156 146
done < $file_list
......
169 159
	
170 160
    # Checking horn backend
171 161
    if [ "$main" != "" ]; then
172
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
162
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
173 163
    else
174
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
175
    fi
176
    if [ $? -ne 0 ]; then
177
        rlustrec="INVALID";
178
    else
179
        rlustrec="VALID"
164
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
180 165
    fi
166

  
181 167
    # echo "z3 $build/$name".smt2 
182 168
    # TODO: This part of the script has to be optimized
183 169
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
......
231 217
    exit 1
232 218
fi
233 219

  
220
# cleaning directory $build
221

  
222
rm -f "$build"/* 2> /dev/null
223

  
224
# executing tests
225

  
234 226
[ ! -z "$c" ] && base_compile
235 227
[ ! -z "$i" ] && inline_compile
236 228
[ ! -z "$w" ] && inline_compile_with_check
test/tests_ok.list
904 904
./tests/arrays_arnaud/generic1.lusi
905 905
./tests/arrays_arnaud/generic1.lus
906 906
./tests/arrays_arnaud/generic2.lus
907
./tests/arrays_arnaud/generic3.lus,top,-dynamic -check-access
908 907
./tests/clocks/clocks1.lus,,-lusi
909 908
./tests/clocks/clocks1.lusi
910 909
./tests/clocks/clocks1.lus

Also available in: Unified diff