Project

General

Profile

Revision e24b2e9b

View differences:

src/automata.ml
24 24
      actual_s : var_decl
25 25
    }
26 26

  
27
let cpvar_decl var_decl =
28
 mkvar_decl var_decl.var_loc ~orig:var_decl.var_orig (var_decl.var_id, var_decl.var_dec_type, var_decl.var_dec_clock, var_decl.var_dec_const, var_decl.var_dec_value)
29

  
30 27
let as_clock var_decl =
31 28
  let tydec = var_decl.var_dec_type in
32 29
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
......
37 34
let mkident loc id =
38 35
 mkexpr loc (Expr_ident id)
39 36

  
37
let mkconst loc id =
38
 mkexpr loc (Expr_const (Const_tag id))
39

  
40 40
let mkfby loc e1 e2 =
41 41
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
42 42

  
43
let mkpair loc e1 e2 =
44
 mkexpr loc (Expr_tuple [e1; e2])
45

  
43 46
let mkidentpair loc restart state =
44 47
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
45 48

  
......
126 129
    node_id = node_id;
127 130
    node_type = Types.new_var ();
128 131
    node_clock = Clocks.new_var true;
129
    node_inputs = List.map cpvar_decl var_inputs;
130
    node_outputs = List.map cpvar_decl var_outputs;
132
    node_inputs = List.map copy_var_decl var_inputs;
133
    node_outputs = List.map copy_var_decl var_outputs;
131 134
    node_locals = [];
132 135
    node_gencalls = [];
133 136
    node_checks = [];
......
176 179
    node_id = node_id;
177 180
    node_type = Types.new_var ();
178 181
    node_clock = Clocks.new_var true;
179
    node_inputs = List.map cpvar_decl var_inputs;
180
    node_outputs = List.map cpvar_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
181
    node_locals = List.map cpvar_decl (new_var_locals @ handler.hand_locals);
182
    node_inputs = List.map copy_var_decl var_inputs;
183
    node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
184
    node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
182 185
    node_gencalls = [];
183 186
    node_checks = [];
184 187
    node_asserts = handler.hand_asserts; 
......
209 212
  let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
210 213
  let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
211 214
  let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
212
  let fby_incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
215
  let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
213 216
  let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
214 217
  let locals' = vars_of_aut_state aut_state in
215 218
  let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in
src/liveness.ml
121 121
    | None           -> []
122 122
    | Some (_, args) -> List.fold_right (fun e r -> match e.expr_desc with Expr_ident id -> id::r | _ -> r) args [] in
123 123
  fun v -> is_aliasable v && List.mem v.var_id inputs_var
124

  
124
(*
125
    let res =
126
is_aliasable v && List.mem v.var_id inputs_var
127
    in (Format.eprintf "aliasable %s by %s = %B@." var v.var_id res; res)
128
*)
125 129
(* replace variable [v] by [v'] in graph [g].
126 130
   [v'] is a dead variable
127 131
*)
......
171 175
  end
172 176

  
173 177
(* tests whether a variable [v] may be (re)used instead of [var]. The conditions are:
178
   - [v] has been really used ([v] is its own representative)
174 179
   - same type
175 180
   - [v] is not an aliasable input of the equation defining [var]
176 181
   - [v] is not one of the current heads (which contain [var])
177
   - the representative of [v] is not currently in use
182
   - [v] is not currently in use
178 183
 *)
179 184
let eligible node ctx heads var v =
180
     Typing.eq_ground var.var_type v.var_type
185
     Hashtbl.find ctx.policy v.var_id == v
186
  && Typing.eq_ground (Types.unclock_type var.var_type) (Types.unclock_type v.var_type)
181 187
  && not (is_aliasable_input node var.var_id v)
182 188
  && not (List.exists (fun h -> h.var_id = v.var_id) heads)
183
  && let repr_v = Hashtbl.find ctx.policy v.var_id
184
     in not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id repr_v.var_id) ctx.evaluated)
189
  && (*let repr_v = Hashtbl.find ctx.policy v.var_id*)
190
     not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id) ctx.evaluated)
185 191

  
186 192
let compute_reuse node ctx heads var =
187 193
  let disjoint = Hashtbl.find ctx.disjoint var.var_id in
188 194
  let locally_reusable v =
189 195
    IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in
190 196
  let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in
197
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles);
191 198
  let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in
199
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);
192 200
  try
193 201
    let disjoint_live = Disjunction.CISet.inter disjoint live in
202
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);
194 203
    let reuse = Disjunction.CISet.max_elt disjoint_live in
195
    let reuse' = Hashtbl.find ctx.policy reuse.var_id in
204
    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
196 205
    begin
197 206
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
198
      if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;
199
      Hashtbl.add ctx.policy var.var_id reuse';
207
      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
208
      Hashtbl.add ctx.policy var.var_id reuse;
200 209
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
201 210
      (*Format.eprintf "%s reused by live@." var.var_id;*)
202 211
    end
203 212
  with Not_found ->
204 213
  try
205 214
    let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
215
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);
206 216
    let reuse = Disjunction.CISet.choose dead in
207
    let reuse' = Hashtbl.find ctx.policy reuse.var_id in
217
    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
208 218
    begin
209 219
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
210
      if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;
211
      Hashtbl.add ctx.policy var.var_id reuse';
220
      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
221
      Hashtbl.add ctx.policy var.var_id reuse;
212 222
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
213 223
      (*Format.eprintf "%s reused by dead %a@." var.var_id Disjunction.pp_ciset dead;*)
214 224
    end
......
229 239
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);
230 240
    let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in
231 241
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:");
232
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s " head.var_id)) heads;
242
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads;
233 243
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@.");
234 244
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@.");
235 245
    compute_dependencies heads ctx;
src/main_lustre_compiler.ml
164 164
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
165 165
    begin
166 166
      let orig = Corelang.copy_prog orig in
167
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file !@,");
167
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
168 168
      check_stateless_decls orig;
169 169
      let _ = Typing.type_prog type_env orig in
170 170
      let _ = Clock_calculus.clock_prog clock_env orig in
......
173 173
      Inliner.witness 
174 174
	basename
175 175
	!Options.main_node
176
	orig prog type_env clock_env;
177
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@,");
176
	orig prog type_env clock_env
178 177
    end;
179 178

  
180 179
(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
src/types.ml
214 214
 | Tclock ty -> Some ty
215 215
 | _         -> None
216 216

  
217
let unclock_type ty =
218
  let ty = repr ty in
219
  match ty.tdesc with
220
  | Tclock ty' -> ty'
221
  | _          -> ty
222

  
217 223
let rec is_dimension_type ty =
218 224
 match (repr ty).tdesc with
219 225
 | Tint

Also available in: Unified diff