Project

General

Profile

Revision d4807c3d

View differences:

src/causality.ml
113 113
let node_memory_variables nd =
114 114
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
115 115

  
116
let node_non_input_variables nd =
117
  let outputs = List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs in
118
  List.fold_left (fun non_inputs v -> ISet.add v.var_id non_inputs) outputs nd.node_locals
119

  
116 120
(* computes the equivalence relation relating variables 
117 121
   in the same equation lhs, under the form of a table 
118 122
   of class representatives *)
......
132 136
 | Types.Ttuple tl -> duplicate v (List.length tl)
133 137
 | _         -> [v]
134 138

  
139

  
135 140
(* Add dependencies from lhs to rhs in [g, g'], *)
136 141
(* no-mem/no-mem and mem/no-mem in g            *)
137 142
(* mem/mem in g'                                *)
138 143
(* excluding all/[inputs]                       *)
139
let add_eq_dependencies mems inputs eq (g, g') =
140
  let rec add_dep lhs_is_mem lhs rhs g =
141
    let add_var x (g, g') =
142
      if ISet.mem x inputs then (g, g') else
144
let add_eq_dependencies mems non_inputs eq (g, g') =
145
  let add_var lhs_is_mem lhs x (g, g') =
146
    if ISet.mem x non_inputs then
143 147
      match (lhs_is_mem, ISet.mem x mems) with
144 148
      | (false, true ) -> (add_edges [x] lhs g, g'                  )
145 149
      | (false, false) -> (add_edges lhs [x] g, g'                  )
146 150
      | (true , false) -> (add_edges lhs [x] g, g'                  )
147
      | (true , true ) -> (g                  , add_edges [x] lhs g') in
151
      | (true , true ) -> (g                  , add_edges [x] lhs g')
152
    else (g, g') in
153
(* Add dependencies from [lhs] to rhs clock [ck]. *)
154
  let rec add_clock lhs_is_mem lhs ck g =
155
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
156
    match (Clocks.repr ck).Clocks.cdesc with
157
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
158
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
159
    | _                         -> g in
160
  let rec add_dep lhs_is_mem lhs rhs g =
148 161
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
149 162
(* i.e every input is connected to every output, through a ghost var *)
150 163
    let mashup_appl_dependencies f e g =
151 164
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
152 165
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
153
	(expr_list_of_expr e) (add_var f_var g) in
166
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) in
154 167
    match rhs.expr_desc with
155 168
    | Expr_const _    -> g
156 169
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
157 170
    | Expr_pre e      -> add_dep true lhs e g
158
    | Expr_ident x -> add_var x g
171
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
159 172
    | Expr_access (e1, _)
160 173
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
161 174
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
162 175
    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
163
    | Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
176
    | Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
164 177
    | Expr_ite   (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
165 178
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
166
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var c g)
179
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
167 180
    | Expr_appl (f, e, None) ->
168 181
      if Basic_library.is_internal_fun f
169 182
    (* tuple component-wise dependency for internal operators *)
......
173 186
      else
174 187
	mashup_appl_dependencies f e g
175 188
    | Expr_appl (f, e, Some (r, _)) ->
176
      mashup_appl_dependencies f e (add_var r g)
189
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
177 190
    | Expr_uclock  (e, _)
178 191
    | Expr_dclock  (e, _)
179 192
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
......
182 195
  
183 196

  
184 197
(* Returns the dependence graph for node [n] *)
185
let dependence_graph mems n =
198
let dependence_graph mems non_inputs n =
186 199
  eq_var_cpt := 0;
187 200
  instance_var_cpt := 0;
188 201
  let g = new_graph (), new_graph () in
189
  let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in
190 202
  (* Basic dependencies *)
191
  let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in
203
  let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in
192 204
  g
193 205

  
194 206
end
......
385 397

  
386 398
let global_dependency node =
387 399
  let mems = ExprDep.node_memory_variables node in
388
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in
400
  let non_inputs = ExprDep.node_non_input_variables node in
401
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in
389 402
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
390 403
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
391 404
  CycleDetection.check_cycles g_non_mems;
src/clock_calculus.ml
522 522
(* ck1 is a subtype of ck2 *)
523 523
let rec sub_unify sub ck1 ck2 =
524 524
  match (repr ck1).cdesc, (repr ck2).cdesc with
525
  | Ctuple [c1]        , Ctuple [c2]        -> sub_unify sub c1 c2
526 525
  | Ctuple cl1         , Ctuple cl2         ->
527 526
    if List.length cl1 <> List.length cl2
528 527
    then raise (Unify (ck1, ck2))
......
792 791
  (* let is_main = nd.node_id = !Options.main_node in *)
793 792
  let new_env = clock_var_decl_list env false nd.node_inputs in
794 793
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
795
  let new_env = clock_var_decl_list new_env false nd.node_locals in
794
  let new_env = clock_var_decl_list new_env true nd.node_locals in
796 795
  List.iter (clock_eq new_env) nd.node_eqs;
797 796
  let ck_ins = clock_of_vlist nd.node_inputs in
798 797
  let ck_outs = clock_of_vlist nd.node_outputs in
......
803 802
     That's not the case for types. *)
804 803
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
805 804
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;
806
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;
805
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
807 806
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
808 807
(*  if (is_main && is_polymorphic ck_node) then
809 808
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
src/clocks.ml
573 573
      print_ck ck_node
574 574
      print_ck ck
575 575

  
576
let const_of_carrier cr =
577
 match (carrier_repr cr).carrier_desc with
578
 | Carry_const id -> id
579
 | Carry_name
580
 | Carry_var
581
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
582
 
576 583
let uneval const cr =
577 584
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
578 585
  let cr = carrier_repr cr in
579 586
  match cr.carrier_desc with
580 587
  | Carry_var -> cr.carrier_desc <- Carry_const const
588
  | Carry_name -> cr.carrier_desc <- Carry_const const
581 589
  | _         -> assert false
582 590

  
583 591
(* Local Variables: *)
src/machine_code.ml
215 215
      o
216 216
    end
217 217

  
218
let const_of_carrier cr =
219
 match (carrier_repr cr).carrier_desc with
220
 | Carry_const id -> id
221
 | Carry_name
222
 | Carry_var
223
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
224

  
225 218
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
226 219
(* the context contains  m : state aka memory variables  *)
227 220
(*                      si : initialization instructions *)
......
240 233
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
241 234
 match (Clocks.repr ck).cdesc with
242 235
 | Con    (ck1, cr, l) ->
243
   let id  = const_of_carrier cr in
236
   let id  = Clocks.const_of_carrier cr in
244 237
   control_on_clock node args ck1 (MBranch (translate_ident node args id,
245 238
					    [l, [inst]] ))
246 239
 | _                   -> inst
......
313 306
let translate_guard node args expr =
314 307
  match expr.expr_desc with
315 308
  | Expr_ident x  -> translate_ident node args x
316
  | _ -> assert false
309
  | _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
317 310

  
318 311
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
319 312
  match expr.expr_desc with
......
367 360
      node_f,
368 361
      NodeDep.filter_static_inputs (node_inputs node_f) el in 
369 362
    let o = new_instance node node_f eq.eq_rhs.expr_tag in
363
    let call_ck = Clocks.new_var true in
364
    Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock;
370 365
    (m,
371 366
     (if Stateless.check_node node_f then si else MReset o :: si),
372 367
     (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),
373 368
     d,
374 369
     reset_instance node args o r eq.eq_rhs.expr_clock @
375
       (control_on_clock node args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s)
370
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
376 371

  
377 372
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
378 373
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
src/normalization.ml
142 142
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
143 143
    in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
144 144

  
145
(* Create an alias for [expr], if [opt] *)
145
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
146
   and [opt] is true *)
146 147
let mk_expr_alias_opt opt node defvars expr =
147
 if opt
148
 then
149
   mk_expr_alias node defvars expr
150
 else
151
   defvars, expr
148
  match expr.expr_desc with
149
  | Expr_ident alias ->
150
    defvars, expr
151
  | _                -> 
152
    if opt
153
    then
154
      mk_expr_alias node defvars expr
155
    else
156
      defvars, expr
152 157

  
153 158
(* Create a (normalized) expression from [ref_e], 
154 159
   replacing description with [norm_d],
......
286 291
  | _ -> normalize_expr ~alias:alias node offsets defvars expr
287 292

  
288 293
and normalize_guard node defvars expr =
289
  match expr.expr_desc with
290
  | Expr_ident _ -> defvars, expr
291
  | _ ->
292
    let defvars, norm_expr = normalize_expr node [] defvars expr in
293
    mk_expr_alias_opt true node defvars norm_expr
294
  let defvars, norm_expr = normalize_expr node [] defvars expr in
295
  mk_expr_alias_opt true node defvars norm_expr
294 296

  
295 297
(* outputs cannot be memories as well. If so, introduce new local variable.
296 298
*)
src/printers.ml
59 59
  match expr.expr_desc with
60 60
    | Expr_const c -> pp_const fmt c
61 61
    | Expr_ident id -> Format.fprintf fmt "%s" id
62
(*    | Expr_cst_array (c, e) -> fprintf fmt "%a^%a" pp_expr e pp_const c *)
63 62
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
64 63
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
65 64
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
src/scheduling.ml
98 98
    !sorted
99 99
  end
100 100

  
101
(* Removes global constants from [node] schedule [sch] *)
102
let remove_consts node sch =
103
  let filter v = 
104
       List.exists (fun vdecl -> vdecl.var_id = v) node.node_locals
105
    || List.exists (fun vdecl -> vdecl.var_id = v) node.node_outputs in
106
  List.filter filter sch
107

  
108 101
let schedule_node n =
109 102
  try
110 103
    let eq_equiv = ExprDep.node_eq_equiv n in
......
115 108
    let n', g = global_dependency n in
116 109
    Log.report ~level:5 (fun fmt -> Format.eprintf "dependency graph for node %s: %a" n'.node_id pp_dep_graph g);
117 110
    let gg = IdentDepGraph.copy g in
118
    let sort = remove_consts n (topological_sort eq_equiv g) in
111
    let sort = topological_sort eq_equiv g in
119 112

  
120 113
    let death = Liveness.death_table n gg sort in
121 114
    Log.report ~level:5 (fun fmt -> Format.eprintf "death table for node %s: %a" n'.node_id Liveness.pp_death_table death);
src/typing.ml
293 293
(* ty1 is a subtype of ty2 *)
294 294
let rec sub_unify sub ty1 ty2 =
295 295
  match (repr ty1).tdesc, (repr ty2).tdesc with
296
  | Ttuple [t1]        , Ttuple [t2]        -> sub_unify sub t1 t2
297 296
  | Ttuple tl1         , Ttuple tl2         ->
298 297
    if List.length tl1 <> List.length tl2
299 298
    then raise (Unify (ty1, ty2))

Also available in: Unified diff