Project

General

Profile

Revision 01d48bb0 src/machine_code.ml

View differences:

src/machine_code.ml
83 83
  minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
84 84
  minit: instr_t list;
85 85
  mstatic: var_decl list; (* static inputs only *)
86
  mconst: instr_t list; (* assignments of node constant locals *)
86 87
  mstep: step_t;
87 88
  mspec: node_annot option;
88 89
  mannot: expr_annot list;
......
105 106

  
106 107
let pp_machine fmt m =
107 108
  Format.fprintf fmt
108
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
109
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
109 110
    m.mname.node_id
110 111
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
111 112
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
112 113
    (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
114
    (Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst
113 115
    pp_step m.mstep
114 116
    (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
115 117
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
......
137 139
    var_dec_type = dummy_type_dec;
138 140
    var_dec_clock = dummy_clock_dec;
139 141
    var_dec_const = false;
142
    var_dec_value = None;
140 143
    var_type =  typ;
141 144
    var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
142 145
    var_loc = Location.dummy_loc
......
183 186
    mcalls = [];
184 187
    minstances = [];
185 188
    minit = [MStateAssign(var_state, Cst (const_of_bool true))];
189
    mconst = [];
186 190
    mstatic = [];
187 191
    mstep = {
188 192
      step_inputs = arrow_desc.node_inputs;
......
215 219
      o
216 220
    end
217 221

  
222

  
218 223
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
219 224
(* the context contains  m : state aka memory variables  *)
220 225
(*                      si : initialization instructions *)
......
284 289
  | "C" -> specialize_to_c expr
285 290
  | _   -> expr
286 291

  
287
let rec translate_expr node ((m, si, j, d, s) as args) expr =
292
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
288 293
  let expr = specialize_op expr in
289 294
 match expr.expr_desc with
290 295
 | Expr_const v                     -> Cst v
......
305 310
   (* special treatment depending on the active backend. For horn backend, ite
306 311
      are preserved in expression. While they are removed for C or Java
307 312
      backends. *)
308
   match !Options.output with | "horn" ->
313
   match !Options.output with
314
   | "horn"
315
   | ("C" | "java") when ite ->
309 316
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
310
   | "C" | "java" | _ ->
317
   | _ ->
311 318
     (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
312 319
 )
313 320
 | _                   -> raise NormalizationError
......
433 440
   to the computed schedule [sch]
434 441
*)
435 442
let sort_equations_from_schedule nd sch =
436
(*  Format.eprintf "%s schedule: %a@."
443
(*Format.eprintf "%s schedule: %a@."
437 444
		 nd.node_id
438 445
		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
439 446
  let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
......
459 466
    List.rev eqs_rev
460 467
  end
461 468

  
469
let constant_equations nd =
470
 List.fold_right (fun vdecl eqs ->
471
   if vdecl.var_dec_const
472
   then
473
     { eq_lhs = [vdecl.var_id];
474
       eq_rhs = Utils.desome vdecl.var_dec_value;
475
       eq_loc = vdecl.var_loc
476
     } :: eqs
477
   else eqs)
478
   nd.node_locals []
479

  
462 480
let translate_eqs node args eqs =
463 481
  List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
464 482

  
......
466 484
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
467 485

  
468 486
  let sorted_eqs = sort_equations_from_schedule nd sch in
469

  
487
  let constant_eqs = constant_equations nd in
488
  
470 489
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
471 490
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
472
  let m, init, j, locals, s = translate_eqs nd init_args sorted_eqs in
491
  let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in
492
  assert (ISet.is_empty m0);
493
  assert (init0 = []);
494
  assert (Utils.IMap.is_empty j0);
495
  let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, s0) sorted_eqs in
473 496
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
474 497
  {
475 498
    mname = nd;
......
477 500
    mcalls = mmap;
478 501
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
479 502
    minit = init;
503
    mconst = s0;
480 504
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
481 505
    mstep = {
482 506
      step_inputs = nd.node_inputs;
......
500 524
    mannot = nd.node_annot;
501 525
  }
502 526

  
503
(** takes the global delcarations and the scheduling associated to each node *)
527
(** takes the global declarations and the scheduling associated to each node *)
504 528
let translate_prog decls node_schs =
505 529
  let nodes = get_nodes decls in
506 530
  List.map
......
518 542
      | None -> if m.mname.node_id = name then Some m else None)
519 543
    None machines
520 544

  
545
let get_const_assign m id =
546
  try
547
    match (List.find (fun instr -> match instr with MLocalAssign (v, _) -> v == id | _ -> false) m.mconst) with
548
    | MLocalAssign (_, e) -> e
549
    | _                   -> assert false
550
  with Not_found -> assert false
551

  
552

  
553
let value_of_ident m id =
554
  (* is is a state var *)
555
  try
556
    StateVar (List.find (fun v -> v.var_id = id) m.mmemory)
557
  with Not_found ->
558
  try (* id is a node var *)
559
    LocalVar (get_node_var id m.mname)
560
  with Not_found ->
561
    try (* id is a constant *)
562
      LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
563
    with Not_found ->
564
      (* id is a tag *)
565
      Cst (Const_tag id)
566

  
567
let rec value_of_dimension m dim =
568
  match dim.Dimension.dim_desc with
569
  | Dimension.Dbool b         -> Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))
570
  | Dimension.Dint i          -> Cst (Const_int i)
571
  | Dimension.Dident v        -> value_of_ident m v
572
  | Dimension.Dappl (f, args) -> Fun (f, List.map (value_of_dimension m) args)
573
  | Dimension.Dite (i, t, e)  -> Fun ("ite", List.map (value_of_dimension m) [i; t; e])
574
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
575
  | _                         -> assert false
576

  
577
let rec dimension_of_value value =
578
  match value with
579
  | Cst (Const_tag t) when t = Corelang.tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
580
  | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
581
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
582
  | LocalVar v                                    -> Dimension.mkdim_ident Location.dummy_loc v.var_id
583
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
584
  | _                                             -> assert false
521 585

  
522 586
(* Local Variables: *)
523 587
(* compile-command:"make -C .." *)

Also available in: Unified diff