Revision d4807c3d
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