Project

General

Profile

« Previous | Next » 

Revision 58272238

Added by Teme Kahsai almost 10 years ago

modifed / to div in horn backend

View differences:

src/basic_library.ml
23 23
  type_static (mkdim_var ()) ty
24 24

  
25 25
let type_env =
26
  List.fold_left 
26
  List.fold_left
27 27
    (fun env (op, op_type) -> TE.add_value env op op_type)
28 28
    TE.initial
29 29
    [
30 30
      "true", (static_op type_bool);
31 31
      "false", (static_op type_bool);
32 32
      "+", (static_op type_bin_poly_op);
33
      "uminus", (static_op type_unary_poly_op); 
34
      "-", (static_op type_bin_poly_op); 
33
      "uminus", (static_op type_unary_poly_op);
34
      "-", (static_op type_bin_poly_op);
35 35
      "*", (static_op type_bin_poly_op);
36 36
      "/", (static_op type_bin_poly_op);
37 37
      "mod", (static_op type_bin_int_op);
......
48 48
      "=", (static_op type_bin_comp_op);
49 49
      "not", (static_op type_unary_bool_op)
50 50
]
51
 
51

  
52 52
module CE = Env
53 53

  
54 54
let clock_env =
......
56 56
  let env' =
57 57
    List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ)
58 58
      ["true"; "false"] init_env in
59
  let env' = 
59
  let env' =
60 60
    List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
61 61
      ["uminus"; "not"] env' in
62
  let env' = 
62
  let env' =
63 63
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
64 64
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
65 65
  env'
......
74 74
  let env' =
75 75
    List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
76 76
      ["uminus"; "not"] env' in
77
  let env' = 
77
  let env' =
78 78
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
79 79
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
80
  let env' = 
80
  let env' =
81 81
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
82 82
      [] env' in
83 83
  env'
......
85 85
module VE = Env
86 86

  
87 87
let eval_env =
88
  let defs = [ 
88
  let defs = [
89 89
    "uminus", (function [Dint a] -> Dint (-a)           | _ -> assert false);
90 90
    "not", (function [Dbool b] -> Dbool (not b)         | _ -> assert false);
91 91
    "+", (function [Dint a; Dint b] -> Dint (a+b)       | _ -> assert false);
......
106 106
    "=", (function [a; b] -> Dbool (a=b)                | _ -> assert false);
107 107
  ]
108 108
  in
109
  List.fold_left 
109
  List.fold_left
110 110
    (fun env (op, op_eval) -> VE.add_value env op op_eval)
111 111
    VE.initial
112 112
    defs
......
120 120
  match i, vl with
121 121
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
122 122
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
123
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
124
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
125
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
123
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
124
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
125
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
126 126
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
127 127
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
128 128
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
129
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
129
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
130 130
    | _ -> failwith i
131 131

  
132 132
let pp_java i pp_val fmt vl =
133 133
  match i, vl with
134 134
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
135 135
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
136
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
137
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
138
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
136
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
137
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
138
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
139 139
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
140 140
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
141 141
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
142
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
142
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
143 143
    | _ -> assert false
144 144

  
145
let pp_horn i pp_val fmt vl = 
145
let pp_horn i pp_val fmt vl =
146 146
  match i, vl with
147
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 
147
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
148

  
148 149
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
149
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v 
150
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
151
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
152
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
153
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
150
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
151
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
152
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
153
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
154
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
154 155
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
155 156
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
156 157
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
157
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
158
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
158
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
159
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
160
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
159 161
  | _ -> assert false
160
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
161
  
162
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
163

  
162 164
*)
163 165

  
164 166
(* Local Variables: *)
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