Project

General

Profile

Revision ca88e660 src/machine_code.ml

View differences:

src/machine_code.ml
20 20
  struct type t = var_decl;; let compare = compare end
21 21

  
22 22

  
23
<<<<<<< HEAD
24
type value_t =
25
  | Cst of constant
26
  | LocalVar of var_decl
27
  | StateVar of var_decl
28
  | Fun of ident * value_t list
29
  | Array of value_t list
30
  | Access of value_t * value_t
31
  | Power of value_t * value_t
32

  
33
type instr_t =
34
  | MLocalAssign of var_decl * value_t
35
  | MStateAssign of var_decl * value_t
36
  | MReset of ident
37
  | MNoReset of ident (* used to symmetrize the reset function *)
38
  | MStep of var_decl list * ident * value_t list
39
  | MBranch of value_t * (label * instr_t list) list
40
=======
41 23
module ISet = Set.Make(OrdVarDecl)
42
>>>>>>> salsa
43 24

  
44 25
 
45 26
let rec pp_val fmt v =
......
315 296
  | "C" -> specialize_to_c expr
316 297
  | _   -> expr
317 298

  
318
<<<<<<< HEAD
319
let rec merge_to_ite g hl =
320
  let loc = Location.dummy_loc in
321
  let mkcst x = mkexpr loc (Expr_const (Const_tag x)) in
322
  let g_expr = mkcst g in
323
  match hl with
324
  | [] -> assert false
325
  | [_, e] -> e
326
  | (l_c,l_e)::tl -> 
327
    let cond_expr = 
328
      mkpredef_call loc "=" [g_expr; mkcst l_c]
329
    in
330
    mkexpr loc (Expr_ite (cond_expr, l_e, merge_to_ite g tl))
331
      
332
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
333
  let expr = specialize_op expr in
334
 match expr.expr_desc with
335
 | Expr_const v                     -> Cst v
336
 | Expr_ident x                     -> translate_ident node args x
337
 | Expr_array el                    -> Array (List.map (translate_expr node args) el)
338
 | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
339
 | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
340
 | Expr_tuple _
341
 | Expr_arrow _
342
 | Expr_fby _
343
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
344
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
345
 | Expr_merge   (g, hl)              -> (
346
   (* (\* Special treatment for functional backends. Is transformed into Ite *\) *)
347
   (* match !Options.output with *)
348
   (* | "horn" -> translate_expr node  args (merge_to_ite g hl) *)
349
   (* | ("C" | "java")          -> raise NormalizationError (\* should have been replaced by MBranch *\) *)
350
   (* | _ -> *)
351
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
352

  
353
 )
354
  
355
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
356
   let nd = node_from_name id in
357
   Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
358
 | Expr_ite (g,t,e) -> (
359
   (* special treatment depending on the active backend. For horn backend, ite
360
      are preserved in expression. While they are removed for C or Java
361
      backends. *)
362
   match !Options.output with
363
   | "horn" ->
364
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
365
   | ("C" | "java") when ite ->
366
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
367
   | _ ->
368
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
369
 )
370
 | _                   -> raise NormalizationError
371
=======
372 299
let rec translate_expr node ((m, si, j, d, s) as args) expr =
373 300
  let expr = specialize_op expr in
374 301
  let value_desc = 
......
399 326
    | _                   -> raise NormalizationError
400 327
  in
401 328
  mk_val value_desc expr.expr_type
402
>>>>>>> salsa
403 329

  
404 330
let translate_guard node args expr =
405 331
  match expr.expr_desc with
......
470 396
      then []
471 397
      else reset_instance node args o r call_ck) @
472 398
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
473
(*
474
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
475
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
476
      backends. *)
477
<<<<<<< HEAD
478
  | [x], Expr_ite   _
479
  (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
480
  | [x], Expr_merge _ 
481
    when (match !Options.output with | "horn" -> false (* TODO 16/12 was true *) | "C" | "java" | _ -> false)
482

  
483
      (* Remark for Ocaml: the when is shared among the two patterns *)
484
      ->
485
=======
486
  | [x], Expr_ite   (c, t, e) 
487
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
488
      -> 
489
>>>>>>> salsa
490
    let var_x = get_node_var x node in
491
    (m, 
492
     si, 
493
     j, 
494
     d, 
495
     (control_on_clock node args eq.eq_rhs.expr_clock 
496
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
497
    )
498
<<<<<<< HEAD
499 399

  
500
*)
501
=======
502
      
503
>>>>>>> salsa
504 400
  | [x], _                                       -> (
505 401
    let var_x = get_node_var x node in
506 402
    (m, si, j, d, 

Also available in: Unified diff