Project

General

Profile

« Previous | Next » 

Revision 58272238

Added by Teme Kahsai almost 10 years ago

modifed / to div in horn backend

View differences:

src/machine_code.ml
21 21

  
22 22
module ISet = Set.Make(OrdVarDecl)
23 23

  
24
type value_t = 
24
type value_t =
25 25
  | Cst of constant
26 26
  | LocalVar of var_decl
27 27
  | StateVar of var_decl
28
  | Fun of ident * value_t list 
28
  | Fun of ident * value_t list
29 29
  | Array of value_t list
30 30
  | Access of value_t * value_t
31 31
  | Power of value_t * value_t
......
36 36
  | MReset of ident
37 37
  | MStep of var_decl list * ident * value_t list
38 38
  | MBranch of value_t * (label * instr_t list) list
39
 
39

  
40 40
let rec pp_val fmt v =
41 41
  match v with
42
    | Cst c         -> Printers.pp_const fmt c 
42
    | Cst c         -> Printers.pp_const fmt c
43 43
    | LocalVar v    -> Format.pp_print_string fmt v.var_id
44 44
    | StateVar v    -> Format.pp_print_string fmt v.var_id
45 45
    | Array vl      -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
......
48 48
    | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
49 49

  
50 50
let rec pp_instr fmt i =
51
  match i with 
51
  match i with
52 52
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
53 53
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
54 54
    | MReset i           -> Format.fprintf fmt "reset %s" i
55 55
    | MStep (il, i, vl)  ->
56 56
      Format.fprintf fmt "%a = %s (%a)"
57 57
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
58
	i      
58
	i
59 59
	(Utils.fprintf_list ~sep:", " pp_val) vl
60 60
    | MBranch (g,hl)     ->
61 61
      Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
......
104 104
   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
105 105

  
106 106
let pp_machine fmt m =
107
  Format.fprintf fmt 
107
  Format.fprintf fmt
108 108
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
109 109
    m.mname.node_id
110 110
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
......
264 264
 List.fold_right join_guards insts []
265 265

  
266 266
(* specialize predefined (polymorphic) operators
267
   wrt their instances, so that the C semantics 
267
   wrt their instances, so that the C semantics
268 268
   is preserved *)
269 269
let specialize_to_c expr =
270 270
 match expr.expr_desc with
......
293 293
 | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
294 294
 | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
295 295
 | Expr_tuple _
296
 | Expr_arrow _ 
296
 | Expr_arrow _
297 297
 | Expr_fby _
298 298
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
299 299
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
......
305 305
   (* special treatment depending on the active backend. For horn backend, ite
306 306
      are preserved in expression. While they are removed for C or Java
307 307
      backends. *)
308
   match !Options.output with | "horn" -> 
308
   match !Options.output with | "horn" ->
309 309
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
310
   | "C" | "java" | _ -> 
310
   | "C" | "java" | _ ->
311 311
     (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
312 312
 )
313 313
 | _                   -> raise NormalizationError
......
323 323
			    conditional g [translate_act node args (y, t)]
324 324
                              [translate_act node args (y, e)]
325 325
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
326
  | _                    -> 
326
  | _                    ->
327 327
    MLocalAssign (y, translate_expr node args expr)
328 328

  
329 329
let reset_instance node args i r c =
......
367 367
    let node_f = node_from_name f in
368 368
    let call_f =
369 369
      node_f,
370
      NodeDep.filter_static_inputs (node_inputs node_f) el in 
370
      NodeDep.filter_static_inputs (node_inputs node_f) el in
371 371
    let o = new_instance node node_f eq.eq_rhs.expr_tag in
372 372
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
373 373
    let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
......
386 386
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
387 387
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
388 388
      backends. *)
389
  | [x], Expr_ite   (c, t, e) 
389
  | [x], Expr_ite   (c, t, e)
390 390
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
391
      -> 
391
      ->
392 392
    let var_x = get_node_var x node in
393
    (m, 
394
     si, 
395
     j, 
396
     d, 
397
     (control_on_clock node args eq.eq_rhs.expr_clock 
393
    (m,
394
     si,
395
     j,
396
     d,
397
     (control_on_clock node args eq.eq_rhs.expr_clock
398 398
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
399 399
    )
400
      
400

  
401 401
  | [x], _                                       -> (
402 402
    let var_x = get_node_var x node in
403
    (m, si, j, d, 
404
     control_on_clock 
403
    (m, si, j, d,
404
     control_on_clock
405 405
       node
406 406
       args
407 407
       eq.eq_rhs.expr_clock
......
424 424
	      Printers.pp_node_eqs eqs;
425 425
	    assert false
426 426
	  end
427
	| hd::tl -> 
427
	| hd::tl ->
428 428
	  if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
429 429
    in
430 430
    aux [] eqs
431 431

  
432
(* Sort the set of equations of node [nd] according 
432
(* Sort the set of equations of node [nd] according
433 433
   to the computed schedule [sch]
434 434
*)
435 435
let sort_equations_from_schedule nd sch =
......
438 438
		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
439 439
  let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
440 440
  let eqs_rev, remainder =
441
    List.fold_left 
442
      (fun (accu, node_eqs_remainder) vl -> 
441
    List.fold_left
442
      (fun (accu, node_eqs_remainder) vl ->
443 443
       if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu
444 444
       then
445 445
	 (accu, node_eqs_remainder)
446 446
       else
447 447
	 let eq_v, remainder = find_eq vl node_eqs_remainder in
448 448
	 eq_v::accu, remainder
449
      ) 
450
      ([], split_eqs) 
451
      sch 
449
      )
450
      ([], split_eqs)
451
      sch
452 452
  in
453 453
  begin
454 454
    if List.length remainder > 0 then (
......
491 491
	| "horn" -> s
492 492
	| "C" | "java" | _ -> join_guards_list s
493 493
      );
494
      step_asserts = 
494
      step_asserts =
495 495
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
496 496
	List.map (translate_expr nd init_args) exprl
497 497
	;
......
502 502

  
503 503
(** takes the global delcarations and the scheduling associated to each node *)
504 504
let translate_prog decls node_schs =
505
  let nodes = get_nodes decls in 
506
  List.map 
507
    (fun decl -> 
505
  let nodes = get_nodes decls in
506
  List.map
507
    (fun decl ->
508 508
     let node = node_of_top decl in
509 509
      let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in
510
      translate_decl node sch 
510
      translate_decl node sch
511 511
    ) nodes
512 512

  
513
let get_machine_opt name machines =  
514
  List.fold_left 
515
    (fun res m -> 
516
      match res with 
517
      | Some _ -> res 
513
let get_machine_opt name machines =
514
  List.fold_left
515
    (fun res m ->
516
      match res with
517
      | Some _ -> res
518 518
      | None -> if m.mname.node_id = name then Some m else None)
519 519
    None machines
520
    
520

  
521 521

  
522 522
(* Local Variables: *)
523 523
(* compile-command:"make -C .." *)

Also available in: Unified diff