Project

General

Profile

Revision 25320f03

View differences:

src/machine_code.ml
398 398
  (* Format.eprintf "ok1@.@?"; *)
399 399
  let schedule = sch.Scheduling_type.schedule in
400 400
  (* Format.eprintf "ok2@.@?"; *)
401
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
401
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
402 402
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
403 403
   *   VSet.pp locals
404 404
   *   VSet.pp inout_vars
......
407 407
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
408 408
  
409 409
  (* Format.eprintf "ok4@.@?"; *)
410
  
411
 
410

  
411
  (* Removing computed memories from locals. We also removed unused variables. *)
412
  let updated_locals =
413
    let l = VSet.elements (VSet.diff locals ctx.m) in
414
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
415
  in
412 416
  let mmap = Utils.IMap.elements ctx.j in
413 417
  {
414 418
    mname = nd;
......
421 425
    mstep = {
422 426
        step_inputs = nd.node_inputs;
423 427
        step_outputs = nd.node_outputs;
424
        step_locals = (* Removing computed memories from locals *)
425
          VSet.elements (VSet.diff locals ctx.m);
428
        step_locals = updated_locals;
426 429
        step_checks = List.map (fun d -> d.Dimension.dim_loc,
427 430
                                         translate_expr env 
428 431
                                           (expr_of_dimension d))
src/scheduling.ml
250 250
   node_schs
251 251

  
252 252

  
253
   (* Sort eqs according to schedule *)
253
(* Sort eqs according to schedule *)
254 254
(* Sort the set of equations of node [nd] according
255 255
   to the computed schedule [sch]
256 256
*)
......
273 273
      sch
274 274
  in
275 275
  begin
276
    if List.length remainder > 0 then (
277
      Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
278
		     Printers.pp_node_eqs remainder
279
      		     Printers.pp_node_eqs eqs;
280
      assert false);
281
    List.rev eqs_rev
276
    let eqs = List.rev eqs_rev in 
277
    let unused =
278
      if List.length remainder > 0 then (
279
        Log.report ~level:3 (fun fmt -> Format.fprintf fmt
280
                                       "[Warning] Equations not used are@ %a@ Full equation set is:@ %a@ "
281
		                       Printers.pp_node_eqs remainder
282
      		                     Printers.pp_node_eqs eqs
283
          );
284
        let vars = List.fold_left (fun accu eq -> eq.eq_lhs @ accu) [] remainder in
285
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt
286
                                      "[Warning] Unused variables: %a@ "
287
                                      (fprintf_list ~sep:", " Format.pp_print_string)
288
                                  vars
289
          );
290
        vars
291
      )
292
      else
293
        []
294
    in
295
    eqs, unused
282 296
  end
283 297

  
284 298
(* Local Variables: *)
src/tools/seal/seal_extract.ml
841 841
  let schedule = nd_report.Scheduling_type.schedule in
842 842
  let eqs, auts = Corelang.get_node_eqs nd in
843 843
  assert (auts = []); (* Automata should be expanded by now *)
844
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
844
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
845 845
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
846 846
  let add_def = add_def defs in
847 847

  
848 848
  let vars = Corelang.get_node_vars nd in
849
  (* Filtering out unused vars *)
850
  let vars = List.filter (fun v -> not (List.mem v.var_id unused)) vars in
849 851
  (* Registering all locals variables as Z3 predicates. Will be use to
850 852
     simplify the expansion *) 
851 853
  let _ =
src/tools/seal/seal_slice.ml
130 130
  (* Split tuples while sorting eqs *)
131 131
  let eqs, auts = Corelang.get_node_eqs nd in
132 132
  assert (auts = []); (* Automata should be expanded by now *)
133
  let sorted_eqs = Scheduling.sort_equations_from_schedule
133
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule
134 134
                     eqs
135
                     msch.Scheduling_type.schedule in
136

  
135
                     msch.Scheduling_type.schedule 
136
  in
137
  let locals = List.filter (fun v -> not (List.mem v.var_id unused)) locals in
137 138
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduled node@.");
138 139

  
139 140
  let stmts =
src/tools/seal/seal_verifier.ml
61 61
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
62 62
  let msch = Utils.desome m.msch in
63 63
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
64
  let sliced_nd = slice_node mems msch nd in
64
  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in
65 65
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
66 66
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
67 67

  

Also available in: Unified diff