Revision 58272238
Added by Teme Kahsai almost 10 years ago
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
modifed / to div in horn backend