Revision ca88e660 src/machine_code.ml
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