Project

General

Profile

Revision 7c95dcab src/machine_code.ml

View differences:

src/machine_code.ml
292 292
  | "C" -> specialize_to_c expr
293 293
  | _   -> expr
294 294

  
295
let rec merge_to_ite g hl =
296
  let loc = Location.dummy_loc in
297
  let mkcst x = mkexpr loc (Expr_const (Const_tag x)) in
298
  let g_expr = mkcst g in
299
  match hl with
300
  | [] -> assert false
301
  | [_, e] -> e
302
  | (l_c,l_e)::tl -> 
303
    let cond_expr = 
304
      mkpredef_call loc "=" [g_expr; mkcst l_c]
305
    in
306
    mkexpr loc (Expr_ite (cond_expr, l_e, merge_to_ite g tl))
307
      
295 308
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
296 309
  let expr = specialize_op expr in
297 310
 match expr.expr_desc with
......
305 318
 | Expr_fby _
306 319
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
307 320
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
308
 | Expr_merge   (x, _)              -> raise NormalizationError
321
 | 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
   | _ ->
327
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
328

  
329
 )
330
  
309 331
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
310 332
   let nd = node_from_name id in
311 333
   Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
......
397 419
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
398 420
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
399 421
      backends. *)
400
  | [x], Expr_ite   (c, t, e)
422
  | [x], Expr_ite   _
423
  (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
424
  | [x], Expr_merge _ 
401 425
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
426

  
427
      (* Remark for Ocaml: the when is shared among the two patterns *)
402 428
      ->
403 429
    let var_x = get_node_var x node in
404 430
    (m,
......
409 435
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
410 436
    )
411 437

  
438
 
412 439
  | [x], _                                       -> (
413 440
    let var_x = get_node_var x node in
414 441
    (m, si, j, d,

Also available in: Unified diff