Project

General

Profile

Revision 29f59e36

View differences:

src/corelang.ml
475 475
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
476 476

  
477 477
let get_var id var_list =
478
 List.find (fun v -> v.var_id = id) var_list
478
    List.find (fun v -> v.var_id = id) var_list
479 479

  
480 480
let get_node_var id node =
481 481
  get_var id (get_node_vars node)
src/machine_code.ml
285 285
  | _   -> expr
286 286

  
287 287
let rec translate_expr node ((m, si, j, d, s) as args) expr =
288
 let expr = specialize_op expr in
288
  let expr = specialize_op expr in
289 289
 match expr.expr_desc with
290 290
 | Expr_const v                     -> Cst v
291 291
 | Expr_ident x                     -> translate_ident node args x
......
323 323
			    conditional g [translate_act node args (y, t)]
324 324
                              [translate_act node args (y, e)]
325 325
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
326
  | _                    -> MLocalAssign (y, translate_expr node args expr)
326
  | _                    -> 
327
    MLocalAssign (y, translate_expr node args expr)
327 328

  
328 329
let reset_instance node args i r c =
329 330
  match r with
......
332 333
                   [control_on_clock node args c (conditional g [MReset i] [])]
333 334

  
334 335
let translate_eq node ((m, si, j, d, s) as args) eq =
335
  (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)
336
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
336 337
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
337 338
  | [x], Expr_arrow (e1, e2)                     ->
338 339
    let var_x = get_node_var x node in
src/main_lustre_compiler.ml
174 174
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
175 175
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
176 176

  
177
  if !Options.scopes_mode then (
178
    if !Options.main_node = "" then failwith "Main node is required for scopes option";
179
    Scopes.compute_all_scopes prog;
180
    (* Printing scopes *)
181
    if !Options.show_scopes then (
182
      Format.printf "Possible scopes are:@.%a@."
183
	Scopes.print_all_scopes ();
184
      exit 0;
185
    );
186
  );
187

  
177 188
  (* Normalization phase *)
178 189
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
179 190
  (* Special treatment of arrows in lustre backend. We want to keep them *)
......
181 192
    Normalization.unfold_arrow_active := false;
182 193
  let prog = Normalization.normalize_prog prog in
183 194
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
184

  
185 195
  (* Checking array accesses *)
186 196
  if !Options.check then
187 197
    begin
......
191 201

  
192 202
  (* Computation of node equation scheduling. It also breaks dependency cycles
193 203
     and warns about unused input or memory variables *)
194
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
204
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,@?");
195 205
  let prog, node_schs = Scheduling.schedule_prog prog in
196 206
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
197 207
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
......
208 218
    else
209 219
      prog
210 220
  in
211

  
212 221
  (* DFS with modular code generation *)
213 222
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
214 223
  let machine_code = Machine_code.translate_prog prog node_schs in
......
237 246
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
238 247
  machine_code);
239 248

  
249
  if !Options.scopes_mode then (
250
    Scopes.check_scopes prog machine_code  
251
  );
252

  
240 253
  (* Printing code *)
241 254
  let basename    =  Filename.basename basename in
242 255
  let destname = !Options.dest_dir ^ "/" ^ basename in
src/normalization.ml
358 358
      let assert_expr = assert_.assert_expr in
359 359
      let (defs, vars'), expr = 
360 360
	normalize_expr 
361
	  ~alias:false 
361
	  ~alias:true 
362 362
	  node 
363 363
	  [] (* empty offset for arrays *)
364 364
	  ([], vars) (* defvar only contains vars *)
365 365
	  assert_expr
366 366
      in
367
      (* Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars'; *)
367 368
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
368 369
    ) (vars, [], []) node.node_asserts in
369 370
  let new_locals = List.filter is_local vars in
371
  (* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *)
372

  
370 373
  (* Compute traceability info: 
371 374
     - gather newly bound variables
372 375
     - compute the associated expression without aliases     
......
393 396
    node_asserts = asserts;
394 397
    node_annot = norm_traceability::node.node_annot;
395 398
  }
396
  in ((*Printers.pp_node Format.err_formatter node;*) node)
399
  in ((*Printers.pp_node Format.err_formatter node;*) 
400
    node
401
)
402

  
397 403

  
398 404
let normalize_decl decl =
399 405
  match decl.top_decl_desc with
400 406
  | Node nd ->
401
    {decl with top_decl_desc = Node (normalize_node nd)}
407
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
408
    Hashtbl.replace Corelang.node_table nd.node_id decl';
409
    decl'
402 410
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
403 411
  
404 412
let normalize_prog decls = 
src/options.ml
38 38
let horn_cex = ref false
39 39
let horn_queries = ref false
40 40

  
41
let scopes_mode = ref false
42
let show_scopes = ref false
43
let scopes : string list list ref = ref []
44
let inputs = ref []
45

  
46
let register_scopes s = 
47
  scopes_mode:= true;
48
  let scope_list = Str.split (Str.regexp ", *") s in
49
  let scope_list = List.map (fun scope -> Str.split (Str.regexp "\\.") scope) scope_list in
50
  scopes := scope_list
51

  
52
let register_inputs s = 
53
  scopes_mode:= true;
54
  let input_list = Str.split (Str.regexp "[;]") s in
55
  let input_list = List.map (fun s -> match Str.split (Str.regexp "=") s with | [v;e] -> v, e | _ -> raise (Invalid_argument ("Input list error: " ^ s))) input_list in
56
  let input_list = List.map (fun (v, e) -> v, Str.split (Str.regexp "[;]") e) input_list in
57
  inputs := input_list
58

  
59

  
60

  
41 61

  
42 62
let options =
43 63
  [ "-d", Arg.Set_string dest_dir,
......
64 84
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
65 85
    "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
66 86
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
67
    "-version", Arg.Unit print_version, " displays the version";]
87
    "-version", Arg.Unit print_version, " displays the version";]@
88
[
89
  "-scopes", Arg.String register_scopes, "specifies which variables to log";
90
  "-input", Arg.String register_inputs, "specifies the simulation input";
91
  "-show-possible-scopes", Arg.Unit (fun () -> show_scopes:= true; scopes_mode := true), "list possible variables to log";
92
] 
68 93

  
69 94
let get_witness_dir filename =
70 95
  (* Make sure the directory exists *)
src/scopes.ml
1
open LustreSpec 
2
open Corelang 
3
open Machine_code
4

  
5

  
6

  
7
let rec compute_scopes ?(is_first=true) prog main_node : var_decl list list =
8
  try
9
    let node = node_of_top (node_from_name main_node) in
10
    let full_local_vars = get_node_vars node in
11
    let local_vars =if is_first then full_local_vars else node.node_inputs @node.node_locals in
12
    let local_scopes = List.map (fun x -> [x]) local_vars in
13
    let sub_scopes =
14
      let sub_nodes =
15
	List.fold_left 
16
	  (fun res eq -> 
17
	    match eq.eq_rhs.expr_desc with 
18
	      | Expr_appl (id, _, _) -> (* Obtaining the var_del associated to the first var of eq_lhs *)
19
		let vid = List.find (fun v -> v.var_id = List.hd eq.eq_lhs) full_local_vars in
20
		(id, vid)::res 
21
	    | _ -> res
22
	  ) [] (get_node_eqs node)
23
      in
24
      List.map (fun (id, vid) ->
25
      let scopes = compute_scopes ~is_first:false prog id in
26
      List.map (fun s -> vid :: s) scopes
27
      ) sub_nodes
28
    in
29
    local_scopes @ (List.flatten sub_scopes) 
30
  with Not_found -> []
31

  
32

  
33
let print_scopes =
34
  Utils.fprintf_list ~sep:"@." 
35
    (fun fmt vl -> 
36
      Format.fprintf fmt "%a: %a"
37
	(Utils.fprintf_list ~sep:"." (fun fmt v -> Format.fprintf fmt "%s" v.var_id)) vl
38
	Types.print_ty ((List.hd (List.rev vl)).var_type)
39
    ) 
40

  
41
let print_path fmt p = 
42
  Utils.fprintf_list ~sep:"." (fun fmt (id, _) -> Format.pp_print_string fmt id) fmt p
43

  
44
let scope_path main_node_name prog machines all_scopes sl : (string * node_desc) list * var_decl =
45
  let rec get_path node id_list (accu: (string * node_desc) list) =
46
    match id_list with
47
      | [id] -> 
48
	let last_node = snd (List.hd accu) in
49
	let id_vdecl = get_node_var id last_node in
50
	List.rev accu, id_vdecl
51
      | id::id_list_tl ->
52
	let e_machine = Utils.desome (get_machine_opt node.node_id machines) in 
53
	Format.eprintf "Machine %a@." Machine_code.pp_machine e_machine;
54
	let instance = 
55
	  List.find 
56
	    (fun i -> match i with | MStep(p, o, _) -> List.exists (fun x -> x.var_id = id) p | _ -> false) 
57
	    e_machine.mstep.step_instrs 
58
	in
59
	let instance_id, instance_node_id = 
60
	  match instance with 
61
	  | MStep(_, o, _) -> o , (
62
	    let n, _ = List.assoc o e_machine.minstances in
63
	    (* node_name *) (node_name n:string)
64
	  )
65
	    | _ -> assert false
66
	in
67
	
68
	let next_node: node_desc = node_of_top (node_from_name (instance_node_id)) in
69
	let accu = (instance_id, next_node)::accu in
70
	get_path next_node id_list_tl accu
71
      | [] -> assert false
72
  in
73
  let all_scopes_as_strings = List.map (List.map (fun v -> v.var_id)) all_scopes in
74
  if not (List.mem sl all_scopes_as_strings) then (
75
    Format.eprintf "%s is an invalid scope.@." (String.concat "." sl);
76
    exit 1
77
  )
78
  else (
79
    Format.eprintf "@.@.Required path: %s@." (String.concat "." sl); 
80
    let main_node = node_from_name main_node_name in
81
    let path, flow = (* Special treatment of first level flow *)
82
      match sl with 
83
	| [flow] -> let flow_var = get_node_var flow (node_of_top main_node) in
84
		    [], flow_var 
85
	| _ -> get_path (node_of_top main_node) sl [] in
86
    Format.eprintf "computed path: %a.%s@." print_path path flow.var_id;
87
    path, flow
88
  )
89

  
90
let all_scopes = ref []
91

  
92
let compute_all_scopes prog = 
93
  all_scopes := compute_scopes prog !Options.main_node 
94
  
95
let print_all_scopes fmt () =
96
  print_scopes fmt !all_scopes
97

  
98
let checked_scopes = ref []
99

  
100
let check_scopes prog machines =
101
 let scopes = !Options.scopes in
102
 let main_node_name = !Options.main_node in
103
 checked_scopes :=
104
   List.map
105
    (fun sl ->
106
      sl, scope_path main_node_name prog machines !all_scopes sl 
107
    ) scopes
108
    
109
(* Local Variables: *)
110
(* compile-command:"make -C .." *)
111
(* End: *)

Also available in: Unified diff