Project

General

Profile

Revision b3b0dd56

View differences:

src/machine_code.ml
65 65
and pp_branch fmt (t, h) =
66 66
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
67 67

  
68
and pp_instrs fmt il =
69
  Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il
70

  
68 71
type step_t = {
69 72
  step_checks: (Location.t * value_t) list;
70 73
  step_inputs: var_decl list;
......
311 314
      are preserved in expression. While they are removed for C or Java
312 315
      backends. *)
313 316
   match !Options.output with
314
   | "horn"
317
   | "horn" ->
318
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
315 319
   | ("C" | "java") when ite ->
316 320
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
317 321
   | _ ->
318
     (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
322
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
319 323
 )
320 324
 | _                   -> raise NormalizationError
321 325

  
src/main_lustre_compiler.ml
211 211
    - eliminate trivial expressions
212 212
 *)
213 213
  let prog =
214
    if !Options.optimization >= 4 then
214
    if !Options.optimization >= 5 then
215 215
      begin
216 216
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. constants elimination@,");
217 217
	Optimize_prog.prog_unfold_consts prog
......
225 225

  
226 226
  (* Optimize machine code *)
227 227
  let machine_code =
228
    if !Options.optimization >= 4 && !Options.output <> "horn" then
229
      begin
230
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
231
	Optimize_machine.machines_cse machine_code
232
      end
233
    else
234
      machine_code
235
  in
236

  
237
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
238
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
239
  machine_code);
240

  
241
  (* Optimize machine code *)
242
  let machine_code =
228 243
    if !Options.optimization >= 2 && !Options.output <> "horn" then
229 244
      begin
230 245
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");
......
243 258
    else
244 259
      machine_code
245 260
  in
261

  
246 262
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
247 263
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
248 264
  machine_code);
src/optimize_machine.ml
41 41
    
42 42
and eliminate_expr elim expr =
43 43
  match expr with
44
  | StateVar v
44 45
  | LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr)
45 46
  | Fun (id, vl) -> Fun (id, List.map (eliminate_expr elim) vl)
46 47
  | Array(vl) -> Array(List.map (eliminate_expr elim) vl)
47 48
  | Access(v1, v2) -> Access(eliminate_expr elim v1, eliminate_expr elim v2)
48 49
  | Power(v1, v2) -> Power(eliminate_expr elim v1, eliminate_expr elim v2)
49
  | Cst _ | StateVar _ -> expr
50
  | Cst _ -> expr
50 51

  
51 52
let eliminate_dim elim dim =
52 53
  Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
......
59 60
  | Const_tag _   -> true
60 61
  | _             -> false
61 62

  
63
let basic_unfoldable_expr expr =
64
  match expr with
65
  | Cst c when is_scalar_const c -> true
66
  | LocalVar _
67
  | StateVar _                   -> true
68
  | _                            -> false
69

  
62 70
let unfoldable_assign fanin v expr =
63 71
  try
64 72
    let d = Hashtbl.find fanin v.var_id
65
    in match expr with
66
    | Cst c when is_scalar_const c -> true
67
    | Cst c when d < 2             -> true
68
    | LocalVar _
69
    | StateVar _                   -> true
73
    in basic_unfoldable_expr expr ||
74
    match expr with
75
    | Cst c when d < 2                                           -> true
70 76
    | Fun (id, _) when d < 2 && Basic_library.is_internal_fun id -> true
71 77
    | _                                                          -> false
72 78
  with Not_found -> false
......
165 171
      in machine_unfold fanin elim_consts m)
166 172
    machines
167 173

  
174
let get_assign_lhs instr =
175
  match instr with
176
  | MLocalAssign(v, _) -> LocalVar v
177
  | MStateAssign(v, _) -> StateVar v
178
  | _                  -> assert false
179

  
180
let get_assign_rhs instr =
181
  match instr with
182
  | MLocalAssign(_, e)
183
  | MStateAssign(_, e) -> e
184
  | _                  -> assert false
185

  
186
let is_assign instr =
187
  match instr with
188
  | MLocalAssign _
189
  | MStateAssign _ -> true
190
  | _              -> false
191

  
192
let mk_assign v e =
193
 match v with
194
 | LocalVar v -> MLocalAssign(v, e)
195
 | StateVar v -> MStateAssign(v, e)
196
 | _          -> assert false
197

  
198
let rec assigns_instr instr assign =
199
  match instr with  
200
  | MLocalAssign (i,_)
201
  | MStateAssign (i,_) -> ISet.add i assign
202
  | MStep (ol, _, _)   -> List.fold_right ISet.add ol assign
203
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
204
  | _                  -> assign
205

  
206
and assigns_instrs instrs assign =
207
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
208

  
209
(*    
210
and substitute_expr subst expr =
211
  match expr with
212
  | StateVar v
213
  | LocalVar v -> (try IMap.find expr subst with Not_found -> expr)
214
  | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
215
  | Array(vl) -> Array(List.map (substitute_expr subst) vl)
216
  | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
217
  | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2)
218
  | Cst _  -> expr
219
*)
220
(** Finds a substitute for [instr] in [instrs], 
221
   i.e. another instr' with the same rhs expression.
222
   Then substitute this expression with the first assigned var
223
*)
224
let subst_instr subst instrs instr =
225
  (*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*)
226
  let instr = eliminate subst instr in
227
  let v = get_assign_lhs instr in
228
  let e = get_assign_rhs instr in
229
  try
230
    let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
231
    match v with
232
    | LocalVar v ->
233
      IMap.add v.var_id (get_assign_lhs instr') subst, instrs
234
    | StateVar v ->
235
      (match get_assign_lhs instr' with
236
      | LocalVar v' ->
237
	let instr = eliminate subst (mk_assign (StateVar v) (LocalVar v')) in
238
	subst, instr :: instrs
239
      | StateVar v' ->
240
	let subst_v' = IMap.add v'.var_id (StateVar v) IMap.empty in
241
	let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
242
	IMap.add v'.var_id (StateVar v) subst, instr :: instrs'
243
      | _           -> assert false)
244
    | _          -> assert false
245
  with Not_found -> subst, instr :: instrs
246
 
247
(** Common sub-expression elimination for machine instructions *)
248
(* - [subst] : hashtable from ident to (simple) definition
249
               it is an equivalence table
250
   - [elim]   : set of eliminated variables
251
   - [instrs] : previous instructions, which [instr] is compared against
252
   - [instr] : current instruction, normalized by [subst]
253
*)
254
let rec instr_cse (subst, instrs) instr =
255
  match instr with
256
  (* Simple cases*)
257
  | MStep([v], id, vl) when Basic_library.is_internal_fun id
258
      -> instr_cse (subst, instrs) (MLocalAssign (v, Fun (id, vl)))
259
  | MLocalAssign(v, expr) when basic_unfoldable_expr expr
260
      -> (IMap.add v.var_id expr subst, instr :: instrs)
261
  | _ when is_assign instr
262
      -> subst_instr subst instrs instr
263
  | _ -> (subst, instr :: instrs)
264

  
265
(** Apply common sub-expression elimination to a sequence of instrs
266
*)
267
let rec instrs_cse subst instrs =
268
  let subst, rev_instrs = 
269
    List.fold_left instr_cse (subst, []) instrs
270
  in subst, List.rev rev_instrs
271

  
272
(** Apply common sub-expression elimination to a machine
273
    - iterate through step instructions and remove simple local assigns
274
*)
275
let machine_cse subst machine =
276
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
277
  let subst, instrs = instrs_cse subst machine.mstep.step_instrs in
278
  let assigned = assigns_instrs instrs ISet.empty
279
  in
280
  {
281
    machine with
282
      mmemory = List.filter (fun vdecl -> ISet.mem vdecl assigned) machine.mmemory;
283
      mstep = { 
284
	machine.mstep with 
285
	  step_locals = List.filter (fun vdecl -> ISet.mem vdecl assigned) machine.mstep.step_locals;
286
	  step_instrs = instrs
287
      }
288
  }
289

  
290
let machines_cse machines =
291
  List.map
292
    (machine_cse IMap.empty)
293
    machines
294

  
168 295
(* variable substitution for optimizing purposes *)
169 296

  
170 297
(* checks whether an [instr] is skip and can be removed from program *)

Also available in: Unified diff