Project

General

Profile

Revision cf9cc6f9

View differences:

src/backends/C/c_backend_src.ml
300 300

  
301 301
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
302 302
  match instr with 
303
  | MNoReset _ -> ()
303 304
  | MReset i ->
304 305
    pp_machine_reset m self fmt i
305 306
  | MLocalAssign (i,v) ->
src/backends/Horn/horn_backend_printers.ml
78 78
   - [value]: assigned value
79 79
   - [pp_var]: printer for variables
80 80
*)
81
let pp_assign m self pp_var fmt var_type var_name value =
81
let pp_assign m pp_var fmt var_type var_name value =
82
  let self = m.mname.node_id in
82 83
  fprintf fmt "(= %a %a)" 
83 84
    (pp_horn_val ~is_lhs:true self pp_var) var_name
84 85
    (pp_value_suffix self pp_var) value
85 86
    
86 87

  
87 88
(* In case of no reset call, we define mid_mem = current_mem *)
88
let pp_no_reset machines m target_machine i fmt =
89
let pp_no_reset machines m fmt i =
90
  let (n,_) = List.assoc i m.minstances in
91
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
92

  
89 93
  let m_list = 
90 94
    rename_machine_list
91 95
      (concat m.mname.node_id i)
......
114 118
    fprintf fmt ")@]@ @]"
115 119
  )
116 120

  
117
let pp_instance_reset machines m self fmt i =
121
let pp_instance_reset machines m fmt i =
118 122
  let (n,_) = List.assoc i m.minstances in
119 123
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
120 124
  
......
133 137
	)
134 138
    )
135 139

  
136
let pp_instance_call machines reset_instances m self fmt i inputs outputs =
140
let pp_instance_call machines reset_instances m fmt i inputs outputs =
141
  let self = m.mname.node_id in
137 142
  try (* stateful node instance *)
138 143
    begin
139 144
      let (n,_) = List.assoc i m.minstances in
......
141 146
      (* Checking whether this specific instances has been reset yet *)
142 147
      if not (List.mem i reset_instances) then
143 148
	(* If not, declare mem_m = mem_c *)
144
	pp_no_reset machines m target_machine i fmt;
149
	pp_no_reset machines m fmt i;
145 150
      
146 151
      let mems = full_memory_vars machines target_machine in
147 152
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
......
208 213
(*     pp_print_newline fmt; *)
209 214
    
210 215
    
211

  
212
let rec pp_machine_instr machines reset_instances (m: machine_t) self fmt instr =
216
(* Print the instruction and update the set of reset instances *)
217
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
213 218
  match instr with
219
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
220
    pp_no_reset machines m fmt i;
221
    i::reset_instances
214 222
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
215
    pp_instance_reset machines m self fmt i;
223
    pp_instance_reset machines m fmt i;
216 224
    i::reset_instances
217 225
  | MLocalAssign (i,v) ->
218 226
    pp_assign
219
      m self (pp_horn_var m) fmt
227
      m (pp_horn_var m) fmt
220 228
      i.var_type (LocalVar i) v;
221 229
    reset_instances
222 230
  | MStateAssign (i,v) ->
223 231
    pp_assign
224
      m self (pp_horn_var m) fmt
232
      m (pp_horn_var m) fmt
225 233
      i.var_type (StateVar i) v;
226 234
    reset_instances
227 235
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
228 236
    assert false (* This should not happen anymore *)
229 237
  | MStep (il, i, vl) ->
230
      (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
231
	 mem_c and print the call to mem_m *)
232
    pp_instance_call machines reset_instances m self fmt i vl il;
238
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
239
       mem_c and print the call to mem_m *)
240
    pp_instance_call machines reset_instances m fmt i vl il;
233 241
    reset_instances (* Since this instance call will only happen once, we
234 242
		       don't have to update reset_instances *)
235
  | MBranch (g,hl) -> (* should not be produced yet. Later, we will have to
243

  
244
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
245
			 should not be produced yet. Later, we will have to
236 246
			 compare the reset_instances of each branch and
237 247
			 introduced the mem_m = mem_c for branches to do not
238 248
			 address it while other did. Am I clear ? *)
239
    assert false
240
      
241
  (* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
242
  (* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
243
  (*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
244
  (*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
245
  (*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
246
  (*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
247
  (* else (\* enum type case *\) *)
248

  
249
  (*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
249
    (* For each branch we obtain the logical encoding, and the information
250
       whether a sub node has been reset or not. If a node has been reset in one
251
       of the branch, then all others have to have the mem_m = mem_c
252
       statement. *)
253
    let self = m.mname.node_id in
254
    let pp_branch fmt (tag, instrs) =
255
      fprintf fmt "@[<v 3>(=> (= %a %s)@ "
256
	(pp_horn_val self (pp_horn_var m)) g
257
	tag;
258
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
259
      fprintf fmt "@])";
260
      () (* rs *)
261
    in
262
    pp_conj pp_branch fmt hl;
263
    reset_instances (* TODO: le code est faux en ce qui concerne les resets. Il
264
		       faut calculer ce qui se passe sur chaque branche et rajouter les instructions
265
		       adequates *)
266
	     
267
(* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
268
(* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
269
(*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
270
(*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
271
(*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
272
(*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
273
(* else (\* enum type case *\) *)
274

  
275
(*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
250 276
and pp_machine_instrs machines reset_instances m fmt instrs = 
251
  let ppi rs fmt i = pp_machine_instr machines rs m m.mname.node_id fmt i in
277
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
252 278
  match instrs with
253
  | [] -> assert false
254 279
  | [x] -> ppi reset_instances fmt x 
255 280
  | _::_ ->
256 281
    fprintf fmt "(and @[<v 0>";
......
261 286
    )
262 287
      reset_instances instrs 
263 288
    in
264
    fprintf fmt "@]@ )";
289
    fprintf fmt "@])";
265 290
    rs
266 291

  
292
  | [] -> fprintf fmt "true"; reset_instances
293

  
267 294
let pp_machine_reset machines fmt m =
268 295
  let locals = local_memory_vars machines m in
269 296
  fprintf fmt "@[<v 5>(and @ ";
src/machine_code.ml
34 34
  | MLocalAssign of var_decl * value_t
35 35
  | MStateAssign of var_decl * value_t
36 36
  | MReset of ident
37
  | MNoReset of ident (* used to symmetrize the reset function *)
37 38
  | MStep of var_decl list * ident * value_t list
38 39
  | MBranch of value_t * (label * instr_t list) list
39 40

  
......
52 53
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
53 54
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
54 55
    | MReset i           -> Format.fprintf fmt "reset %s" i
56
    | MNoReset i         -> ()
55 57
    | MStep (il, i, vl)  ->
56 58
      Format.fprintf fmt "%a = %s (%a)"
57 59
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
......
319 321
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
320 322
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
321 323
 | Expr_merge   (g, hl)              -> (
322
   (* Special treatment for functional backends. Is transformed into Ite *)
323
   match !Options.output with
324
   | "horn" -> translate_expr node  args (merge_to_ite g hl)
325
   | ("C" | "java")          -> raise NormalizationError (* should have been replaced by MBranch *)
326
   | _ ->
324
   (* (\* Special treatment for functional backends. Is transformed into Ite *\) *)
325
   (* match !Options.output with *)
326
   (* | "horn" -> translate_expr node  args (merge_to_ite g hl) *)
327
   (* | ("C" | "java")          -> raise NormalizationError (\* should have been replaced by MBranch *\) *)
328
   (* | _ -> *)
327 329
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
328 330

  
329 331
 )
......
363 365
  match r with
364 366
  | None        -> []
365 367
  | Some r      -> let g = translate_guard node args r in
366
                   [control_on_clock node args c (conditional g [MReset i] [])]
368
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
367 369

  
368 370
let translate_eq node ((m, si, j, d, s) as args) eq =
369 371
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
......
415 417
      then []
416 418
      else reset_instance node args o r call_ck) @
417 419
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
418

  
420
(*
419 421
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
420 422
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
421 423
      backends. *)
422 424
  | [x], Expr_ite   _
423 425
  (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
424 426
  | [x], Expr_merge _ 
425
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
427
    when (match !Options.output with | "horn" -> false (* TODO 16/12 was true *) | "C" | "java" | _ -> false)
426 428

  
427 429
      (* Remark for Ocaml: the when is shared among the two patterns *)
428 430
      ->
......
435 437
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
436 438
    )
437 439

  
438
 
440
*)
439 441
  | [x], _                                       -> (
440 442
    let var_x = get_node_var x node in
441 443
    (m, si, j, d,
......
543 545
	   common branches are not merged while they are in C or Java
544 546
	   backends. *)
545 547
	match !Options.output with
546
	| "horn" -> s
548
	(* | "horn" -> s TODO 16/12 *)
547 549
	| "C" | "java" | _ -> join_guards_list s
548 550
      );
549 551
      step_asserts =
src/main_lustre_compiler.ml
86 86
  end
87 87

  
88 88

  
89
let functional_backend () = 
90
  match !Options.output with
91
  | "horn" | "lustre" | "acsl" -> true
92
  | _ -> false
89 93

  
90 94
(* compile a .lus source file *)
91 95
let rec compile_source dirname basename extension =
......
236 240

  
237 241
  (* Optimize machine code *)
238 242
  let machine_code =
239
    if !Options.optimization >= 4 && !Options.output <> "horn" then
243
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
240 244
      begin
241
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
245
	Log.report ~level:1 
246
	  (fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,");
242 247
	Optimize_machine.machines_cse machine_code
243 248
      end
244 249
    else
......
247 252

  
248 253
  (* Optimize machine code *)
249 254
  let machine_code =
250
    if !Options.optimization >= 2 && !Options.output <> "horn" then
255
    if !Options.optimization >= 2 (* && !Options.output <> "horn" *) then
251 256
      begin
252
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");
257
	Log.report ~level:1 
258
	  (fun fmt -> fprintf fmt 
259
	    ".. machines optimization: const. inlining (partial eval. with const)@,");
253 260
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
254 261
      end
255 262
    else
256 263
      machine_code
257 264
  in
258 265
  (* Optimize machine code *)
259
  let machine_code =
260
    if !Options.optimization >= 3 && !Options.output <> "horn" then
266
  let machine_code = (* TODO reactivate. I disabled it because output variables were removed *)
267
    if false && !Options.optimization >= 3 && not (functional_backend ()) then
261 268
      begin
262
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,");
263
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code node_schs)
269
	Log.report ~level:1 
270
	  (fun fmt -> fprintf fmt ".. machines optimization: minimize heap alloc by reusing vars@,");
271
	Optimize_machine.machines_fusion 
272
	  (Optimize_machine.machines_reuse_variables machine_code node_schs)
264 273
      end
265 274
    else
266 275
      machine_code
src/optimize_machine.ml
30 30
  | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
31 31
  | MStateAssign (i,v) -> MStateAssign (i, e_expr v)
32 32
  | MReset i           -> instr
33
  | MNoReset i         -> instr
33 34
  | MStep (il, i, vl)  -> MStep(il, i, List.map e_expr vl)
34 35
  | MBranch (g,hl)     -> 
35 36
    MBranch
......
51 52
  | Cst _ -> expr
52 53

  
53 54
let eliminate_dim elim dim =
54
  Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
55
  Dimension.expr_replace_expr 
56
    (fun v -> try
57
		dimension_of_value (IMap.find v elim) 
58
      with Not_found -> mkdim_ident dim.dim_loc v) 
59
    dim
55 60

  
56 61
let unfold_expr_offset m offset expr =
57
  List.fold_left (fun res -> (function Index i -> Access(res, value_of_dimension m i) | Field f -> failwith "not yet implemented")) expr offset
62
  List.fold_left 
63
    (fun res -> 
64
      (function Index i -> 
65
       Access(res, value_of_dimension m i) 
66
      | Field f -> failwith "not yet implemented"))
67
    expr offset
58 68

  
59 69
let rec simplify_cst_expr m offset cst =
60 70
    match offset, cst with
......
84 94
    | Index i :: q, Array vl when Dimension.is_dimension_const i
85 95
                                     -> simplify q (List.nth vl (Dimension.size_const_dimension i))
86 96
    | Index i :: q, Array vl         -> unfold_expr_offset m [Index i] (Array (List.map (simplify q) vl))
87
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_expr_offset %a@." pp_val expr; assert false)
97
(*    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_expr_offset %a@." pp_val expr; assert false) *)
88 98
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
89 99
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
90 100
  in simplify [] expr
91 101

  
92
let rec simplify_instr_offset m instr =
102
let rec simplify_instr_offset m accu instr =
93 103
  match instr with
94
  | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
95
  | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
96
  | MReset id              -> instr
97
  | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
104
  | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr) :: accu
105
  | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr) :: accu
106
  | MReset id              -> instr :: accu
107
  | MNoReset id              -> instr :: accu
108
  | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs) :: accu
98 109
  | MBranch (cond, brl)
99
    -> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
100

  
110
    -> (
111
    let cond' = simplify_expr_offset m cond in
112
    match cond' with
113
    | Cst (Const_tag l) -> 
114
      let il = List.assoc l brl in
115
      List.fold_left (simplify_instr_offset m) accu il
116
    |  _ -> MBranch(cond', List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl) :: accu
117
    )
101 118
and simplify_instrs_offset m instrs =
102
  List.map (simplify_instr_offset m) instrs
119
  let rev_l = List.fold_left (simplify_instr_offset m) [] instrs in
120
  List.rev rev_l
103 121

  
104 122
let is_scalar_const c =
105 123
  match c with
......
219 237

  
220 238
(** Perform optimization on machine code:
221 239
    - iterate through step instructions and remove simple local assigns
222
    
240
    - constant switch cases are simplified
223 241
*)
224 242
let machine_unfold fanin elim machine =
225 243
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*)
......
419 437
  | MLocalAssign (i, v) -> instr_cons (MLocalAssign (fvar i, value_replace_var fvar v)) cont
420 438
  | MStateAssign (i, v) -> instr_cons (MStateAssign (i, value_replace_var fvar v)) cont
421 439
  | MReset i            -> instr_cons instr cont
440
  | MNoReset i            -> instr_cons instr cont
422 441
  | MStep (il, i, vl)   -> instr_cons (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)) cont
423 442
  | MBranch (g, hl)     -> instr_cons (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl)) cont
424 443

  

Also available in: Unified diff