Project

General

Profile

Revision 3ca27bc7

View differences:

src/backends/C/c_backend_src.ml
327 327
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) el
328 328

  
329 329
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
330
  match instr with 
330
  match get_instr_desc instr with 
331 331
  | MNoReset _ -> ()
332 332
  | MReset i ->
333 333
    pp_machine_reset m self fmt i
......
341 341
      i.var_type (mk_val (StateVar i) i.var_type) v
342 342
  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
343 343
    pp_machine_instr dependencies m self fmt 
344
      (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))
344
      (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
345 345
  | MStep ([i0], i, vl) when has_c_prototype i dependencies -> 
346 346
    fprintf fmt "%a = %s(%a);" 
347 347
      (pp_c_val self (pp_c_var_read m)) (mk_val (LocalVar i0) i0.var_type)
......
437 437
    (Utils.fprintf_list ~sep:"" print_dealloc_instance) m.minstances
438 438

  
439 439
let print_stateless_init_code dependencies fmt m self =
440
  let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
440
  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
441 441
  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
442 442
  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
443 443
    (print_init_prototype self) (m.mname.node_id, m.mstatic)
......
452 452
    (Utils.pp_newline_if_non_empty m.minit)
453 453

  
454 454
let print_stateless_clear_code dependencies fmt m self =
455
  let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
455
  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
456 456
  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
457 457
  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
458 458
    (print_clear_prototype self) (m.mname.node_id, m.mstatic)
......
522 522
    (Utils.pp_newline_if_non_empty m.minit)
523 523

  
524 524
let print_init_code dependencies fmt m self =
525
  let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
525
  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
526 526
  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
527 527
  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
528 528
    (print_init_prototype self) (m.mname.node_id, m.mstatic)
......
537 537
    (Utils.pp_newline_if_non_empty m.minit)
538 538

  
539 539
let print_clear_code dependencies fmt m self =
540
  let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
540
  let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
541 541
  let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
542 542
  fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
543 543
    (print_clear_prototype self) (m.mname.node_id, m.mstatic)
src/backends/EMF/EMF_backend.ml
1
(* EMF backend *)
2
(* This backup is initially motivated by the need to express Spacer computed
3
   invariants as Matlab Simulink executable evidences.
4

  
5
   Therefore the input language is more restricted. We do not expect fancy
6
   datastructure, complex function calls, etc.
7

  
8
   In case of error, use -node foo -inline to eliminate function calls that are
9
   not seriously handled yet.
10
   
11

  
12
   In terms of algorithm, the process was initially based on printing normalized
13
   code. We now rely on machine code printing. The old code is preserved for
14
   reference.
15
*)
16

  
1 17
open LustreSpec
2 18
open Machine_code
3 19
open Format
4 20
open Utils
5 21

  
6 22
exception Unhandled of string
7
  
23
    
24

  
25
(* Basic printing functions *)
26
    
8 27
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
9 28
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
10

  
11 29
let pp_node_args = fprintf_list ~sep:", " pp_var_name
12 30

  
13
(* simple function to extract the element id in the list. Starts from 1. *)
31
    
32
(* Matlab starting counting from 1.
33
   simple function to extract the element id in the list. Starts from 1. *)
14 34
let rec get_idx x l =
15 35
  match l with
16 36
  | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
17 37
  | [] -> assert false
18
     
38

  
39
(**********************************************)
40
(* Old stuff: printing normalized code as EMF *)     
41
(**********************************************)
42

  
43
(*
19 44
let pp_expr vars fmt expr =
20 45
  let rec pp_expr fmt expr =
21 46
    match expr.expr_desc with
......
107 132
  | Const _
108 133
  | Open _
109 134
  | TypeDef _ -> eprintf "should not happen in EMF backend"
135
*)
136

  
137

  
138
(**********************************************)
139
(*   Printing machine code as EMF             *)
140
(**********************************************)
110 141

  
111 142
let rec pp_val vars fmt v =
112 143
  match v.value_desc with
......
142 173
    | "not", [v] -> fprintf fmt "(~%a)" (pp_val vars) v
143 174
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_val vars)) vl 
144 175

  
176
     
145 177

  
146 178
     
147 179
let rec pp_instr m vars fmt i =
148
  match i with
180
  match Corelang.get_instr_desc i with
149 181
  | MLocalAssign (var,v) 
150 182
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
151 183
  | MStep ([var], i, vl)  -> (
......
177 209
and pp_instrs m vars fmt il =
178 210
  fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m vars)) il
179 211

  
212

  
180 213
let rec get_instr_var i =
181
  match i with
214
  match Corelang.get_instr_desc i with
182 215
  | MLocalAssign (var,_) 
183 216
  | MStateAssign (var,_) 
184 217
  | MStep ([var], _, _)  -> var 
......
194 227
  | i::_ -> get_instr_var i (* looking for the first instr *)
195 228
  | _ -> assert false
196 229

  
230
  
197 231
let rec  get_val_vars v =
198 232
  match v.value_desc with
199 233
  | Cst c -> Utils.ISet.empty
......
201 235
  | StateVar v -> Utils.ISet.singleton v.var_id
202 236
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
203 237
  | _ -> assert false (* not available in EMF backend *)
204
  
238

  
205 239
let rec get_instr_vars i =
206
  match i with
240
  match Corelang.get_instr_desc i with
207 241
  | MLocalAssign (_,v)  
208 242
  | MStateAssign (_,v) -> get_val_vars v
209 243
  | MStep ([_], _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
......
219 253
  | MBranch _ (* EMF backend only accept true/false ite *)
220 254
  | MReset _           
221 255
  | MNoReset _
222
  | MComment _ -> assert false (* not  available for EMF output *)
256
  | MComment _ -> failwith "Error in compiling some constructs into EMF. Have you considered -node foo -inline options ?" (* not  available for EMF output *)
223 257
and get_instrs_vars il =
224 258
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
225 259
    Utils.ISet.empty
......
229 263
  (* first, we extract the expression and associated variables *)
230 264
  let var = get_instr_var i in
231 265
  let vars = Utils.ISet.elements (get_instr_vars i) in	
232
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
266
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%t]@]}"
233 267
    var.var_id
234 268
    (pp_instr m vars) i
235 269
    (fprintf_list ~sep:", " pp_var_string) vars
236
    
270
    (fun fmt -> ()
271
      (*xxxx
272
      if is expr than print associated lustre eq else empty string
273
	xxx todo
274
      *)
275
    ) 
237 276
     
238 277
let pp_machine fmt m =
239 278
  try
......
250 289
    eprintf "%s@ " msg;
251 290
    eprintf "node skipped - no output generated@ @]@."
252 291
  )
292

  
293
(****************************************************)
294
(* Main function: iterates over node and print them *)
295
(****************************************************)
296
let pp_meta fmt basename =
297
  fprintf fmt "\"meta\": @[<v 0>{@ ";
298
  Utils.fprintf_list ~sep:",@ "
299
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
300
    fmt
301
    ["compiler-name", (Filename.basename Sys.executable_name);
302
     "compiler-version", Version.number;
303
     "command", (String.concat " " (Array.to_list Sys.argv));
304
     "source_file", basename
305
    ]
306
  ;
307
  fprintf fmt "@ @]},@ "
253 308
    
254
let translate fmt prog machines =
309
let translate fmt basename prog machines =
255 310
  fprintf fmt "@[<v 0>{@ ";
311
  pp_meta fmt basename;
312
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
256 313
  (* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
257 314
  fprintf_list ~sep:",@ " pp_machine fmt machines;
315
  fprintf fmt "@ @]}";
258 316
  fprintf fmt "@ @]}"
317

  
318
(* Local Variables: *)
319
(* compile-command: "make -C ../.." *)
320
(* End: *)
src/backends/Horn/horn_backend_printers.ml
288 288
    
289 289
(* Print the instruction and update the set of reset instances *)
290 290
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
291
  match instr with
291
  match get_instr_desc instr with
292 292
  | MComment _ -> reset_instances
293 293
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
294 294
    pp_no_reset machines m fmt i;
src/corelang.ml
181 181
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
182 182

  
183 183

  
184
let mkinstr (* TODO ?(lustre_expr=None) ?(lustre_eq=None) *) i =
185
  {
186
    instr_desc = i;
187

  
188
  }
189

  
190
let get_instr_desc i = i.instr_desc
191
let update_instr_desc i id = { i with instr_desc = id }
192

  
184 193
(***********************************************************)
185 194
(* Fast access to nodes, by name *)
186 195
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
src/corelang.mli
31 31
val mk_new_node_name: node_desc -> ident -> ident
32 32
val mktop: top_decl_desc -> top_decl
33 33

  
34

  
34
(* constructor for machine types *)
35
val mkinstr: (* TODO ?lustre_expr:expr -> ?lustre_eq: eq option -> *) instr_t_desc -> instr_t
36
val get_instr_desc: instr_t -> instr_t_desc
37
val update_instr_desc: instr_t -> instr_t_desc -> instr_t
38
  
35 39
val node_table : (ident, top_decl) Hashtbl.t
36 40
val print_node_table:  Format.formatter -> unit -> unit
37 41
val node_name: top_decl -> ident
src/lustreSpec.ml
236 236
  | Power of value_t * value_t
237 237

  
238 238
type instr_t =
239
  {
240
    instr_desc: instr_t_desc;
241
  }
242
and instr_t_desc =
239 243
  | MLocalAssign of var_decl * value_t
240 244
  | MStateAssign of var_decl * value_t
241 245
  | MReset of ident
src/machine_code.ml
43 43
    | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
44 44

  
45 45
let rec pp_instr fmt i =
46
  match i with
46
  match i.instr_desc with
47 47
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
48 48
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
49 49
    | MReset i           -> Format.fprintf fmt "reset %s" i
......
149 149
let is_memory m id =
150 150
  List.exists (fun o -> o.var_id = id.var_id) m.mmemory
151 151

  
152
let conditional c t e =
153
  MBranch(c, [ (tag_true, t); (tag_false, e) ])
152
let conditional (* TODO ?(lustre_expr:expr option=None) *) c t e =
153
  mkinstr (* TODO ?lustre_expr *) (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
154 154

  
155 155
let dummy_var_decl name typ =
156 156
  {
......
211 211
    mmemory = [var_state];
212 212
    mcalls = [];
213 213
    minstances = [];
214
    minit = [MStateAssign(var_state, cst true)];
214
    minit = [mkinstr (MStateAssign(var_state, cst true))];
215 215
    mstatic = [];
216 216
    mconst = [];
217 217
    mstep = {
......
220 220
      step_locals = [];
221 221
      step_checks = [];
222 222
      step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)
223
			         [MStateAssign(var_state, cst false);
224
                                  MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]
225
                                 [MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ];
223
			(List.map mkinstr
224
			[MStateAssign(var_state, cst false);
225
			 MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)])
226
                        (List.map mkinstr
227
			[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ];
226 228
      step_asserts = [];
227 229
    };
228 230
    mspec = None;
......
314 316
 match (Clocks.repr ck).cdesc with
315 317
 | Con    (ck1, cr, l) ->
316 318
   let id  = Clocks.const_of_carrier cr in
317
   control_on_clock node args ck1 (MBranch (translate_ident node args id,
318
					    [l, [inst]] ))
319
   control_on_clock node args ck1 (mkinstr
320
				     (* TODO il faudrait prendre le lustre
321
					associé à instr et rajouter print_ck_suffix
322
					ck) de clocks.ml *)
323
				     (MBranch (translate_ident node args id,
324
					       [l, [inst]] )))
319 325
 | _                   -> inst
320 326

  
321 327
let rec join_branches hl1 hl2 =
......
328 334
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
329 335

  
330 336
and join_guards inst1 insts2 =
331
 match inst1, insts2 with
337
 match get_instr_desc inst1, List.map get_instr_desc insts2 with
332 338
 | _                   , []                               ->
333 339
   [inst1]
334 340
 | MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 ->
335
   MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))
336
   :: q
341
    mkinstr
342
      (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
343
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
344
   :: (List.tl insts2)
337 345
 | _ -> inst1 :: insts2
338 346

  
339 347
let join_guards_list insts =
......
403 411
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
404 412
  match expr.expr_desc with
405 413
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
406
			    conditional g
414
			    conditional (* TODO ?lustre_expr:(Some expr) *) g
407 415
                              [translate_act node args (y, t)]
408 416
                              [translate_act node args (y, e)]
409
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x,
410
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
411
  | _                    -> MLocalAssign (y, translate_expr node args expr)
417
  | Expr_merge (x, hl)   -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MBranch (translate_ident node args x,
418
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl))
419
  | _                    -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MLocalAssign (y, translate_expr node args expr))
412 420

  
413 421
let reset_instance node args i r c =
414 422
  match r with
415 423
  | None        -> []
416 424
  | Some r      -> let g = translate_guard node args r in
417
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
425
                   [control_on_clock node args c (conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]
418 426

  
419 427
let translate_eq node ((m, si, j, d, s) as args) eq =
420 428
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
......
425 433
     let c1 = translate_expr node args e1 in
426 434
     let c2 = translate_expr node args e2 in
427 435
     (m,
428
      MReset o :: si,
436
      mkinstr (MReset o) :: si,
429 437
      Utils.IMap.add o (arrow_top_decl, []) j,
430 438
      d,
431
      (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
439
      (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:eq *) (MStep ([var_x], o, [c1;c2])))) :: s)
432 440
  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->
433 441
     let var_x = get_node_var x node in
434 442
     (ISet.add var_x m,
435 443
      si,
436 444
      j,
437 445
      d,
438
      control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
446
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1))) :: s)
439 447
  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
440 448
     let var_x = get_node_var x node in
441 449
     (ISet.add var_x m,
442
      MStateAssign (var_x, translate_expr node args e1) :: si,
450
      mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1)) :: si,
443 451
      j,
444 452
      d,
445
      control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
453
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e2))) :: s)
446 454

  
447 455
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
448 456
     let var_p = List.map (fun v -> get_node_var v node) p in
......
459 467
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
460 468
       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;*)
461 469
     (m,
462
      (if Stateless.check_node node_f then si else MReset o :: si),
470
      (if Stateless.check_node node_f then si else mkinstr (MReset o) :: si),
463 471
      Utils.IMap.add o call_f j,
464 472
      d,
465 473
      (if Stateless.check_node node_f
466 474
       then []
467 475
       else reset_instance node args o r call_ck) @
468
	(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
476
	(control_on_clock node args call_ck (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStep (var_p, o, vl)))) :: s)
469 477
  (*
470 478
    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
471 479
    are preserved. While they are replaced as if g then x = t else x = e in  C or Java
......
656 664

  
657 665
let get_const_assign m id =
658 666
  try
659
    match (List.find (fun instr -> match instr with MLocalAssign (v, _) -> v == id | _ -> false) m.mconst) with
667
    match get_instr_desc (List.find
668
	     (fun instr -> match get_instr_desc instr with
669
	     | MLocalAssign (v, _) -> v == id
670
	     | _ -> false)
671
	     m.mconst
672
    ) with
660 673
    | MLocalAssign (_, e) -> e
661 674
    | _                   -> assert false
662 675
  with Not_found -> assert false
src/main_lustre_compiler.ml
389 389
       let source_file = destname ^ ".emf" in (* Could be changed *)
390 390
       let source_out = open_out source_file in
391 391
       let fmt = formatter_of_out_channel source_out in
392
       EMF_backend.translate fmt prog machine_code;
392
       EMF_backend.translate fmt basename prog machine_code;
393 393
       ()
394 394
     end
395 395

  
src/optimize_machine.ml
26 26

  
27 27
let rec eliminate elim instr =
28 28
  let e_expr = eliminate_expr elim in
29
  match instr with
29
  match get_instr_desc instr with
30 30
  | MComment _         -> instr
31
  | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
32
  | MStateAssign (i,v) -> MStateAssign (i, e_expr v)
31
  | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
32
  | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
33 33
  | MReset i           -> instr
34 34
  | MNoReset i         -> instr
35
  | MStep (il, i, vl)  -> MStep(il, i, List.map e_expr vl)
35
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
36 36
  | MBranch (g,hl)     -> 
37
    MBranch
38
      (e_expr g, 
39
       (List.map 
40
	  (fun (l, il) -> l, List.map (eliminate elim) il) 
41
	  hl
42
       )
43
      )
37
     update_instr_desc instr (
38
       MBranch
39
	 (e_expr g, 
40
	  (List.map 
41
	     (fun (l, il) -> l, List.map (eliminate elim) il) 
42
	     hl
43
	  )
44
	 )
45
     )
44 46
    
45 47
and eliminate_expr elim expr =
46 48
  match expr.value_desc with
......
106 108
  in simplify [] expr
107 109

  
108 110
let rec simplify_instr_offset m instr =
109
  match instr with
110
  | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
111
  | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
111
  match get_instr_desc instr with
112
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
113
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
112 114
  | MReset id              -> instr
113 115
  | MNoReset id            -> instr
114
  | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
116
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
115 117
  | MBranch (cond, brl)
116
    -> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
118
    -> update_instr_desc instr (
119
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
120
    )
117 121
  | MComment _             -> instr
118 122

  
119 123
and simplify_instrs_offset m instrs =
......
197 201

  
198 202
and instr_unfold fanin instrs elim instr =
199 203
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
200
  match instr with
204
  match get_instr_desc instr with
201 205
  (* Simple cases*)
202 206
  | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
203
    -> instr_unfold fanin instrs elim (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))
207
    -> instr_unfold fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
204 208
  | MLocalAssign(v, expr) when unfoldable_assign fanin v expr
205 209
    -> (IMap.add v.var_id expr elim, instrs)
206 210
  | MBranch(g, hl) when false
......
209 213
	 List.fold_right
210 214
	   (fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches))
211 215
	   elim_branches (elim, [])
212
       in elim, (MBranch (g, branches) :: instrs)
216
       in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs)
213 217
  | _
214 218
    -> (elim, instr :: instrs)
215 219
    (* default case, we keep the instruction and do not modify elim *)
......
259 263
  let const = const_of_top top_const in
260 264
  let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in
261 265
  let vdecl = { vdecl with var_type = const.const_type }
262
  in MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)
266
  in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
263 267

  
264 268
let machines_unfold consts node_schs machines =
265 269
  List.fold_right (fun m (machines, removed) ->
......
272 276
    ([], IMap.empty)
273 277

  
274 278
let get_assign_lhs instr =
275
  match instr with
279
  match get_instr_desc instr with
276 280
  | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type
277 281
  | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type
278 282
  | _                  -> assert false
279 283

  
280 284
let get_assign_rhs instr =
281
  match instr with
285
  match get_instr_desc instr with
282 286
  | MLocalAssign(_, e)
283 287
  | MStateAssign(_, e) -> e
284 288
  | _                  -> assert false
285 289

  
286 290
let is_assign instr =
287
  match instr with
291
  match get_instr_desc instr with
288 292
  | MLocalAssign _
289 293
  | MStateAssign _ -> true
290 294
  | _              -> false
......
296 300
 | _          -> assert false
297 301

  
298 302
let rec assigns_instr instr assign =
299
  match instr with  
303
  match get_instr_desc instr with  
300 304
  | MLocalAssign (i,_)
301 305
  | MStateAssign (i,_) -> ISet.add i assign
302 306
  | MStep (ol, _, _)   -> List.fold_right ISet.add ol assign
......
359 363
       let lhs = get_assign_lhs instr' in
360 364
      (match lhs.value_desc with
361 365
      | LocalVar v' ->
362
        let instr = eliminate subst (mk_assign v lhs) in
366
        let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in
363 367
	subst, instr :: instrs
364 368
      | StateVar stv' ->
365 369
	let subst_v' = IMap.add stv'.var_id v IMap.empty in
......
377 381
   - [instr] : current instruction, normalized by [subst]
378 382
*)
379 383
let rec instr_cse (subst, instrs) instr =
380
  match instr with
384
  match get_instr_desc instr with
381 385
  (* Simple cases*)
382 386
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
383
      -> instr_cse (subst, instrs) (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))
387
      -> instr_cse (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
384 388
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
385 389
      -> (IMap.add v.var_id expr subst, instr :: instrs)
386 390
  | _ when is_assign instr
......
421 425

  
422 426
(* checks whether an [instr] is skip and can be removed from program *)
423 427
let rec instr_is_skip instr =
424
  match instr with
428
  match get_instr_desc instr with
425 429
  | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true
426 430
  | MStateAssign (i, { value_desc = StateVar v; _}) when i = v -> true
427 431
  | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
......
433 437
 if instr_is_skip instr then cont else instr::cont
434 438

  
435 439
let rec instr_remove_skip instr cont =
436
  match instr with
440
  match get_instr_desc instr with
437 441
  | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont
438 442
  | MStateAssign (i, { value_desc = StateVar v; _ }) when i = v -> cont
439
  | MBranch (g, hl) -> MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl) :: cont
443
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
440 444
  | _               -> instr::cont
441 445

  
442 446
and instrs_remove_skip instrs cont =
......
453 457
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
454 458

  
455 459
let rec instr_replace_var fvar instr cont =
456
  match instr with
460
  match get_instr_desc instr with
457 461
  | MComment _          -> instr_cons instr cont
458
  | MLocalAssign (i, v) -> instr_cons (MLocalAssign (fvar i, value_replace_var fvar v)) cont
459
  | MStateAssign (i, v) -> instr_cons (MStateAssign (i, value_replace_var fvar v)) cont
462
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
463
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
460 464
  | MReset i            -> instr_cons instr cont
461 465
  | MNoReset i          -> instr_cons instr cont
462
  | MStep (il, i, vl)   -> instr_cons (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)) cont
463
  | MBranch (g, hl)     -> instr_cons (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl)) cont
466
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
467
  | MBranch (g, hl)     -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont
464 468

  
465 469
and instrs_replace_var fvar instrs cont =
466 470
  List.fold_right (instr_replace_var fvar) instrs cont
......
504 508
    ) prog
505 509

  
506 510
let rec instr_assign res instr =
507
  match instr with
511
  match get_instr_desc instr with
508 512
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
509 513
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
510 514
  | MBranch (g, hl)     -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl
......
515 519
  List.fold_left instr_assign res instrs
516 520

  
517 521
let rec instr_constant_assign var instr =
518
  match instr with
522
  match get_instr_desc instr with
519 523
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
520 524
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
521 525
  | MBranch (g, hl)                     -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
......
525 529
  List.fold_left (fun res i -> if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs
526 530

  
527 531
let rec instr_reduce branches instr1 cont =
528
  match instr1 with
532
  match get_instr_desc instr1 with
529 533
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
530 534
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
531
  | MBranch (g, hl)                     -> MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl) :: cont
535
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
532 536
  | _                                   -> instr1 :: cont
533 537

  
534 538
and instrs_reduce branches instrs cont =
......
538 542
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
539 543

  
540 544
let rec instrs_fusion instrs =
541
  match instrs with
542
  | []
543
  | [_]                                                               ->
545
  match instrs, List.map get_instr_desc instrs with
546
  | [], []
547
  | [_], [_]                                                               ->
544 548
    instrs
545
  | i1::(MBranch ({ value_desc = LocalVar v; _}, hl))::q when instr_constant_assign v i1 ->
549
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = LocalVar v; _}, hl))::q_desc when instr_constant_assign v i1 ->
546 550
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
547
  | i1::(MBranch ({ value_desc = StateVar v; _}, hl))::q when instr_constant_assign v i1 ->
551
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = StateVar v; _}, hl))::q_desc when instr_constant_assign v i1 ->
548 552
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) 
549
  | i1::i2::q                                                         ->
553
  | i1::i2::q, _                                                         ->
550 554
    i1 :: instrs_fusion (i2::q)
551

  
555
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
556
     
552 557
let step_fusion step =
553 558
  { step with
554 559
    step_instrs = instrs_fusion step.step_instrs;
src/pluginList.ml
1
let plugins =
2
  [
3
    (module Scopes.Plugin : PluginType.PluginType);
4
    (module Salsa_plugin.Plugin : PluginType.PluginType);
5
  ]
src/plugins/salsa/machine_salsa_opt.ml
48 48
    [] -> Vars.empty
49 49
  | i::tl -> (
50 50
    let vars_tl = get_read_vars tl in 
51
    match i with
51
    match Corelang.get_instr_desc i with
52 52
    | LT.MLocalAssign(_,e) 
53 53
    | LT.MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl
54 54
    | LT.MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el
......
66 66
    [] -> Vars.empty
67 67
  | i::tl -> (
68 68
    let vars_tl = get_written_vars tl in 
69
    match i with
69
    match Corelang.get_instr_desc i with
70 70
    | LT.MLocalAssign(v,_) 
71 71
    | LT.MStateAssign(v,_) -> Vars.add v vars_tl 
72 72
    | LT.MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
......
224 224
	(* Obtaining unfold expression of v in formalEnv *)
225 225
	let v_def = FormalEnv.get_def formalEnv v  in
226 226
	let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in
227
	let instr = 
227
	let instr_desc = 
228 228
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
229 229
	    LT.MLocalAssign(v, e)
230 230
	  else
231 231
	    LT.MStateAssign(v, e)
232 232
	in
233
	instr::accu_instr, 
233
	(Corelang.mkinstr instr_desc)::accu_instr, 
234 234
	(match r with 
235 235
	| None -> ranges 
236 236
	| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r)
......
267 267
       formalEnv, possibly ranges and vars_to_print *)
268 268
     begin
269 269
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
270
	 match hd_instr with 
270
	 match Corelang.get_instr_desc hd_instr with 
271 271
	 | LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
272 272
	    (* LocalAssign are injected into formalEnv *)
273 273
	    if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr;
......
319 319
	      assign_vars printed_vars ranges formalEnv required_vars in
320 320
	    let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
321 321
	    let new_instr = 
322
	      match hd_instr with
323
	      | LT.MLocalAssign _ -> LT.MLocalAssign(vd,vt')
324
	      | _ -> LT.MStateAssign(vd,vt')
322
	      match Corelang.get_instr_desc hd_instr with
323
	      | LT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt'))
324
	      | _ -> Corelang.update_instr_desc hd_instr (LT.MStateAssign(vd,vt'))
325 325
	    in
326 326
	    let written_vars = Vars.add vd required_vars in
327 327
	    prefix_instr@[new_instr],
......
382 382
									 variables *)
383 383
	      let written_vars = Vars.union required_vars (Vars.of_list vdl) in
384 384
	      let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in
385
	      instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *)
385
	      instrs' @ [Corelang.update_instr_desc hd_instr (LT.MStep(vdl,id,vtl'))], (* New instrs *)
386 386
	      RangesInt.add_call ranges' vdl id vtl_ranges,   (* add information bounding each vdl var *) 
387 387
	      formalEnv,
388 388
	      Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
......
430 430
									     
431 431
							   ) branches ([], required_vars, ranges) in
432 432
	    if debug then Format.eprintf "dealing with branches done@ @]@ ";	  
433
	    prefix_instr@[LT.MBranch(vt', branches')],
433
	    prefix_instr@[Corelang.update_instr_desc hd_instr (LT.MBranch(vt', branches'))],
434 434
	    merged_ranges, (* Only step functions call within branches
435 435
			    may have produced new ranges. We merge this data by
436 436
			    computing the join per variable *)
src/plugins/scopes/scopes.ml
105 105
      let find_var = (fun v -> v.var_id = varid) in
106 106
      let instance = 
107 107
	List.find 
108
	  (fun i -> match i with 
108
	  (fun i -> match get_instr_desc i with 
109 109
	  | MStep(p, o, _) -> List.exists find_var p 
110 110
	  | _ -> false
111 111
	  ) 
......
113 113
      in
114 114
      try
115 115
	let variable, instance_node, instance_id = 
116
	  match instance with 
116
	  match get_instr_desc instance with 
117 117
	  | MStep(p, o, _) -> 
118 118
	    (* Format.eprintf "Looking for machine %s@.@?" o; *)
119 119
	    let o_fun, _ = List.assoc o e_machine.mcalls in
......
219 219

  
220 220
let update_machine machine =
221 221
  let stateassign vdecl =
222
    MStateAssign (vdecl, mk_val (LocalVar vdecl) vdecl.var_type)
222
    mkinstr 
223
    (MStateAssign (vdecl, mk_val (LocalVar vdecl) vdecl.var_type))
223 224
  in
224 225
  let local_decls = machine.mstep.step_inputs
225 226
    (* @ machine.mstep.step_outputs   *)
......
230 231
    mstep = { 
231 232
      machine.mstep with 
232 233
        step_instrs = machine.mstep.step_instrs
233
        @ (MComment "Registering all flows")::(List.map stateassign local_decls)
234
        @ (mkinstr (MComment "Registering all flows"))::(List.map stateassign local_decls)
234 235
          
235 236
    }
236 237
  }

Also available in: Unified diff