Project

General

Profile

Revision 15003796

View differences:

src/annotations.ml
20 20
let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
21 21

  
22 22
let get_expr_annotations key = Hashtbl.find_all expr_annotations key
23
let get_node_annotations key = Hashtbl.find_all node_annotations key
24

  
25

  
26
(* Local Variables: *)
27
(* compile-command:"make -C .." *)
28
(* End: *)
src/corelang.ml
856 856

  
857 857
(* Replace any occurence of a var in vars_to_replace by its associated
858 858
   expression in defs until e does not contain any such variables *)
859
let rec substitute_expr vars_to_replace defs e =
860
  let se = substitute_expr vars_to_replace defs in
861
  { e with expr_desc = 
859
let substitute_expr ?(open_pre=true) vars_to_replace defs e =
860
  Format.eprintf "substitution in %a@." Printers.pp_expr e;
861
  let normalized = ref [] in
862
  let rec se vars_to_replace defs e =
863
    let se = se vars_to_replace defs in
864
    { e with expr_desc = 
862 865
      let ed = e.expr_desc in
863 866
      match ed with
864 867
      | Expr_const _ -> ed
......
869 872
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
870 873
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
871 874
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
872
      | Expr_pre e' -> Expr_pre (se e')
875
      | Expr_pre e' -> if open_pre then Expr_pre (se e') else ed
873 876
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
874 877
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
875 878
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
876 879
      | Expr_ident i -> 
877
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
880
	if List.exists (fun vid -> vid = i) vars_to_replace then (
881
	  Format.eprintf "computation substitution in %a@." Printers.pp_expr e;
878 882
	  let eq_i eq = eq.eq_lhs = [i] in
879
	  if List.exists eq_i defs then
883
	  if List.mem_assoc i !normalized then (
884
	      Format.eprintf "substitution of variable  %a already computed. getting it: %a@." Printers.pp_expr e Printers.pp_expr (List.assoc i !normalized);
885
	    (List.assoc i !normalized).expr_desc
886
	  )
887
	  else if List.exists eq_i defs then (
888
	    Format.eprintf "substitution of variable  %a not computed.@." Printers.pp_expr e;
880 889
	    let sub = List.find eq_i defs in
890
	    Format.eprintf "definition is %a@." Printers.pp_expr (sub.eq_rhs);
881 891
	    let sub' = se sub.eq_rhs in
892
	    Format.eprintf "substitution of variable  %a just computed.@." Printers.pp_expr e;
893
	    normalized := (i, sub')::!normalized;
882 894
	    sub'.expr_desc
895
	  )
883 896
	  else 
884 897
	    assert false
885 898
	)
......
887 900
	  ed
888 901

  
889 902
  }
903
  in
904
  se vars_to_replace defs e
890 905
(* FAUT IL RETIRER ?
891 906
  
892 907
 let rec expr_to_eexpr  expr =
src/corelang.mli
122 122

  
123 123
(** rename_prog f_node f_var f_const prog *)
124 124
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
125
val substitute_expr: var_decl list -> eq list -> expr -> expr
125
val substitute_expr: ?open_pre:bool -> ident list -> eq list -> expr -> expr
126 126

  
127 127
val copy_var_decl: var_decl -> var_decl
128 128
val copy_const: const_desc -> const_desc
src/linearize.ml
1
open LustreSpec
2

  
3
let check_input nd value =
4
      Format.eprintf "lin check input@.";
5
  if not (value.eexpr_quantifiers = []) then (
6
    Log.report ~level:1 
7
      (fun fmt -> Format.fprintf fmt "Invalid linearization command for node %s. No quantifiers allowed!@." nd.node_id );
8
    false
9
 
10
  ) else 
11
    let value_type = 
12
      match (Types.repr value.eexpr_type).Types.tdesc with
13
      | Types.Ttuple tl -> Types.Ttuple (List.map Types.dynamic_type tl)
14
      | t -> t
15
    in 
16
    let vardecl_types = Types.Ttuple(List.map (fun v -> Types.repr v.var_type) nd.node_inputs) in
17
    if not (value_type = vardecl_types) then (
18
    Log.report ~level:1 
19
      (fun fmt -> Format.fprintf fmt "Invalid linearization command for node %s: expecting type %a, got type %a@." nd.node_id
20
	Types.print_ty (Types.new_ty vardecl_types)
21
	Types.print_ty (Types.repr value.eexpr_type)
22
 );
23
    false
24
  )
25
  else 
26
    true
27
  
28
(* Eliminate variables. It will change the order of the statements. Do not touch automaton *)
29

  
30
  
31
let rec elim_vars vars stmts =
32
  Format.eprintf "lin elim var@.";
33
  
34
  (* Removing memories (lhs = Pre _ or Fby _) *)
35
  let memory_vars, non_memory_vars = List.partition (fun vid -> 
36
    let v_def = List.find (fun stm -> match stm with Eq e -> e.eq_lhs = [vid] | _ -> false) stmts in
37
    match v_def with
38
      Eq eq -> (match eq.eq_rhs.expr_desc with 
39
      Expr_pre _ | Expr_fby _ -> true
40
    | _ -> false
41
      )
42
    | _ -> false
43
  ) vars 
44
  in
45
  
46
  (* we partition this level stmts. Local Automata are left untouched and
47
     are addressed separately *)
48
  let local_defs, mem_defs, aut_defs = List.fold_left 
49
    (fun (ll,el,al) def -> (
50
      match def with
51
      | Aut a -> (ll, el, a::al) (* we do not handle automaton now. Will be down later *)
52
      | Eq eq -> (
53
	match eq.eq_lhs with 
54
	| [v] -> if List.mem v non_memory_vars then
55
	    eq::ll, el, al
56
	  else
57
	    ll, eq::el, al
58
	| _ -> raise (Failure "elim eq failed, unnormalized equation"))
59
     )) ([], [], []) stmts
60
  in
61
      Format.eprintf "lin local ok@.";
62
    let mem_defs' = 
63
      (* let local_defs, _ = (\* local defs have to be normalized to avoid loops (fixpoints) in unrolling *\) *)
64
      (* 	List.fold_left (fun (accu, vl) def ->  *)
65
      (* 	  (\* we clean def wrt accu *\) *)
66
      (* 	  Format.eprintf "lin cleaning local %a@." Printers.pp_node_eq def; *)
67
      (* 	  let def_e = Corelang.substitute_expr vl accu def.eq_rhs in *)
68
      (* 	  Format.eprintf "lin obtaining %a@." Printers.pp_expr def_e; *)
69
      (* 	  {def with eq_rhs = def_e}::accu, def.eq_lhs @ vl *)
70
      (* 	  ) ([],[]) local_defs *)
71
      (* in *)
72
      List.map (fun e -> 
73
	Format.eprintf "lin cleaning %a@." Printers.pp_expr e.eq_rhs; 
74
	let res = {e with eq_rhs = Corelang.substitute_expr ~open_pre:true non_memory_vars local_defs e.eq_rhs } in
75
	Format.eprintf "lin cleaned %a@." Printers.pp_expr res.eq_rhs; 
76
	Eq res
77
      ) mem_defs in
78
      Format.eprintf "lin main def ok@.";
79
    let aut_defs' = List.map (fun a -> Aut {a with aut_handlers = List.map elim_handler a.aut_handlers}) aut_defs in   
80
    Format.eprintf "lin aut def ok@.";
81
    mem_defs'@aut_defs', memory_vars
82

  
83
and elim_handler h = 
84
  Format.eprintf "lin elim handler@.";
85
  let stmts, mem_vid = elim_vars (List.map (fun v -> v.var_id) h.hand_locals) h.hand_stmts in
86
  { h with
87
    hand_locals = (List.filter (fun v -> List.mem v.var_id mem_vid) h.hand_locals); 
88
    hand_stmts = stmts }
89

  
90

  
91
    
92
  
93

  
94
(* This function returns a modified node. 
95
   TODO make sure there is no function call in the node (or nothing with a lhs of length > 1 
96
 *)
97
    let node nd value = 
98
      (* We check that value is a tuple compatible with the input arguments of the node *)
99
      Format.eprintf "lin node@.";
100
      if not (check_input nd value) then
101
	nd (* not applicable *)
102
      else (
103
	Log.report ~level:1 
104
	  (fun fmt -> Format.fprintf fmt "Linearizing node %s around point %a@." 
105
	    nd.node_id 
106
	    Printers.pp_eexpr value
107
	  );
108
	(* Node is simplified. No more local non memory variables *)
109
	let unrolled_stmts, mem_vid = 
110
	  elim_vars (List.map (fun v -> v.var_id) nd.node_locals) nd.node_stmts 
111
	in
112
	(* Each expression is expressed as (expr -> Pre expr) ie. normalized wrt pre *)
113
	let stmts = unrolled_stmts in
114
	{ nd with
115
	  node_locals = (List.filter (fun v -> List.mem v.var_id mem_vid) nd.node_locals); 
116
	  node_stmts = stmts
117
	}
118
      )
119

  
120
(* Local Variables: *)
121
(* compile-command:"make -C .." *)
122
(* End: *)
123

  
src/machine_code.ml
425 425
      assert false
426 426
    end
427 427

  
428
let find_eq xl eqs =
429
  let rec aux accu eqs =
430
      match eqs with
431
	| [] ->
432
	  begin
433
	    Format.eprintf "Looking for variables %a in the following equations@.%a@."
434
	      (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
435
	      Printers.pp_node_eqs eqs;
436
	    assert false
437
	  end
438
	| hd::tl ->
439
	  if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
440
    in
441
    aux [] eqs
442

  
443
(* Sort the set of equations of node [nd] according
444
   to the computed schedule [sch]
445
*)
446
let sort_equations_from_schedule nd sch =
447
(*Format.eprintf "%s schedule: %a@."
448
		 nd.node_id
449
		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
450
  let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
451
  let eqs_rev, remainder =
452
    List.fold_left
453
      (fun (accu, node_eqs_remainder) vl ->
454
       if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu
455
       then
456
	 (accu, node_eqs_remainder)
457
       else
458
	 let eq_v, remainder = find_eq vl node_eqs_remainder in
459
	 eq_v::accu, remainder
460
      )
461
      ([], split_eqs)
462
      sch
463
  in
464
  begin
465
    if List.length remainder > 0 then (
466
      Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
467
		     Printers.pp_node_eqs remainder
468
      		     Printers.pp_node_eqs (get_node_eqs nd);
469
      assert false);
470
    List.rev eqs_rev
471
  end
428

  
472 429

  
473 430
let constant_equations nd =
474 431
 List.fold_right (fun vdecl eqs ->
......
487 444
let translate_decl nd sch =
488 445
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
489 446

  
490
  let sorted_eqs = sort_equations_from_schedule nd sch in
447
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd sch in
491 448
  let constant_eqs = constant_equations nd in
492 449
  
493 450
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
src/main_lustre_compiler.ml
204 204
      Access.check_prog prog;
205 205
    end;
206 206

  
207
  (* Computation of node equation scheduling. It also breaks dependency cycles
208
     and warns about unused input or memory variables *)
209
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
210
  let prog, node_schs = Scheduling.schedule_prog prog in
211
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
212
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
213
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
214
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
207
  (* Apply transformation according to annotations: for the moment, linearization only *)
208
  let prog = 
209
    List.map (
210
      fun top -> 
211
	match top.top_decl_desc with
212
	| Node nd -> 
213
	  let nd = 
214
	    List.fold_left ( 
215
     	      fun nd annots ->
216
		List.fold_left (
217
		  fun nd (keyl, value) ->
218
		    match keyl, value with
219
	  	    | ["linearize"], _ ->  (* This option is activated only for lustre output *)
220
		      if !Options.output = "lustre" then
221
			Linearize.node nd value
222
		      else 
223
			nd
224
	  	    | _ -> nd (* do nothing *)
225
		) nd annots.annots
226
	    ) nd nd.node_annot
227
	  in
228
	  { top with top_decl_desc = Node nd }
229
	| _ -> top
230
    ) prog
231
  in
232

  
215 233

  
216 234
 (* Optimization of prog:
217 235
    - Unfold consts
......
226 244
    else
227 245
      prog
228 246
  in
247

  
248

  
249
  let machine_code =
250
    if !Options.output = "lustre" then 
251
      None
252
    else begin
253

  
254
  (* Computation of node equation scheduling. It also breaks dependency cycles
255
     and warns about unused input or memory variables *)
256
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
257
  let prog, node_schs = Scheduling.schedule_prog prog in
258
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
259
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
260
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
261
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
262
      
229 263
  (* DFS with modular code generation *)
230 264
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
231 265
  let machine_code = Machine_code.translate_prog prog node_schs in
......
271 305
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
272 306
  machine_code);
273 307

  
308
  Some machine_code 
309
    end
310
  in
311
  
274 312
  (* Printing code *)
275 313
  let basename    =  Filename.basename basename in
276 314
  let destname = !Options.dest_dir ^ "/" ^ basename in
277
  let _ = match !Options.output with
278
    | "C" ->
315
  let _ = match !Options.output, machine_code with
316
    | "C", Some machine_code ->
279 317
      begin
280 318
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
281 319
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
......
286 324
	    alloc_header_file source_lib_file source_main_file makefile_file
287 325
	    basename prog machine_code dependencies
288 326
	end
289
    | "java" ->
327
    | "java", Some machine_code ->
290 328
      begin
291 329
	failwith "Sorry, but not yet supported !"
292 330
    (*let source_file = basename ^ ".java" in
......
296 334
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
297 335
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
298 336
      end
299
    | "horn" ->
337
    | "horn", Some machine_code ->
300 338
       begin
301 339
	let source_file = destname ^ ".smt2" in (* Could be changed *)
302 340
	let source_out = open_out source_file in
......
312 350
	Horn_backend.traces_file fmt basename prog machine_code;
313 351
	)
314 352
      end
315
    | "lustre" ->
353
    | "lustre", None ->
316 354
      begin
317 355
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
318 356
	let source_out = open_out source_file in
src/normalization.ml
374 374
	   - gather newly bound variables
375 375
	   - compute the associated expression without aliases
376 376
	*)
377
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
377
	let diff_vars = List.fold_left (fun accu v -> if not (List.mem v node.node_locals) then v.var_id :: accu else accu ) [] new_locals in
378 378
	let norm_traceability = {
379
	  annots = List.map (fun v ->
379
	  annots = List.map (fun vid ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
382
		List.find (fun eq -> eq.eq_lhs = [vid]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." vid; assert false) in
384
	    let expr = substitute_expr ~open_pre:true diff_vars (defs@assert_defs) eq.eq_rhs in
385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident vid expr.expr_loc; expr])) in
386 386
	    (["traceability"], pair)
387 387
	  ) diff_vars;
388 388
	  annot_loc = Location.dummy_loc
src/scheduling.ml
205 205
    prog
206 206
    ([],IMap.empty)
207 207

  
208

  
209
(* Sort the set of equations of node [nd] according
210
   to the computed schedule [sch]
211
*)
212
let sort_equations_from_schedule nd sch =
213
  let find_eq xl eqs =
214
    let rec aux accu eqs =
215
      match eqs with
216
      | [] ->
217
	begin
218
	  Format.eprintf "Looking for variables %a in the following equations@.%a@."
219
	    (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
220
	    Printers.pp_node_eqs eqs;
221
	  assert false
222
	end
223
      | hd::tl ->
224
	if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
225
    in
226
    aux [] eqs
227
  in
228
  (*Format.eprintf "%s schedule: %a@."
229
    nd.node_id
230
    (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
231
  let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
232
  let eqs_rev, remainder =
233
    List.fold_left
234
      (fun (accu, node_eqs_remainder) vl ->
235
       if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu
236
       then
237
	 (accu, node_eqs_remainder)
238
       else
239
	 let eq_v, remainder = find_eq vl node_eqs_remainder in
240
	 eq_v::accu, remainder
241
      )
242
      ([], split_eqs)
243
      sch
244
  in
245
  begin
246
    if List.length remainder > 0 then (
247
      Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
248
		     Printers.pp_node_eqs remainder
249
      		     Printers.pp_node_eqs (get_node_eqs nd);
250
      assert false);
251
    List.rev eqs_rev
252
  end
253

  
254

  
208 255
let pp_eq_schedule fmt vl =
209 256
  match vl with
210 257
  | []  -> assert false
src/typing.ml
390 390
(** [type_expr env in_main expr] types expression [expr] in environment
391 391
    [env], expecting it to be [const] or not. *)
392 392
and type_expr env in_main const expr =
393
  (* typing also the possible annotations *)
394
  let _ = (
395
    match expr.expr_annot with
396
      None -> () 
397
    | Some anns -> type_expr_annot env in_main const anns
398
  ) in
393 399
  let resulting_ty = 
394
  match expr.expr_desc with
400
    match expr.expr_desc with
395 401
  | Expr_const c ->
396 402
    let ty = type_const expr.expr_loc c in
397 403
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
......
509 515
  with Unify (t1, t2) ->
510 516
    raise (Error (loc, Type_clash (t1,t2)))
511 517

  
518

  
519
and type_eexpr env in_main const ee =
520
  let ty = type_expr env in_main const ee.eexpr_qfexpr in
521
  ee.eexpr_type <- ty;
522
  ty
523

  
524
and type_expr_annot env in_main const anns =
525
  List.iter (fun (_, ee) ->
526
    ignore (type_eexpr env in_main const ee)
527
  ) anns.annots
528
    
529

  
512 530
(** [type_eq env eq] types equation [eq] in environment [env] *)
513 531
let type_eq env in_main undefined_vars eq =
514 532
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
......
633 651
    let assert_expr =  assert_.assert_expr in
634 652
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
635 653
  )  nd.node_asserts;
654

  
655
  (* Typing node annotations *)
656
  List.iter (fun expr_annot ->
657
    type_expr_annot (new_env, vd_env) is_main false expr_annot
658
  )  nd.node_annot;
636 659
  
637 660
  (* check that table is empty *)
638 661
  let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in

Also available in: Unified diff