Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/checks/access.ml | ||
---|---|---|
9 | 9 |
(* *) |
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 |
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *) |
|
12 |
(** Access checking module. Done after typing. Generates dimension constraints |
|
13 |
stored in nodes *) |
|
13 | 14 |
|
14 |
let debug _fmt _args = () (* Format.eprintf "%a" *) |
|
15 |
(* Though it shares similarities with the clock calculus module, no code |
|
16 |
is shared. Simple environments, very limited identifier scoping, no |
|
17 |
identifier redefinition allowed. *) |
|
15 |
let debug _fmt _args = () |
|
16 |
|
|
17 |
(* Format.eprintf "%a" *) |
|
18 |
(* Though it shares similarities with the clock calculus module, no code is |
|
19 |
shared. Simple environments, very limited identifier scoping, no identifier |
|
20 |
redefinition allowed. *) |
|
18 | 21 |
|
19 | 22 |
open Utils |
20 |
(* Yes, opening both modules is dirty as some type names will be |
|
21 |
overwritten, yet this makes notations far lighter.*) |
|
23 |
|
|
24 |
(* Yes, opening both modules is dirty as some type names will be overwritten, |
|
25 |
yet this makes notations far lighter.*) |
|
22 | 26 |
open Lustre_types |
23 | 27 |
open Corelang |
24 | 28 |
|
25 |
module ConstraintModule = |
|
26 |
struct (* bool dimension module *)
|
|
29 |
module ConstraintModule = struct
|
|
30 |
(* bool dimension module *)
|
|
27 | 31 |
type t = Dimension.dim_expr |
32 |
|
|
28 | 33 |
let equal d1 d2 = Dimension.is_eq_dimension d1 d2 |
29 |
let compare d1 d2 = if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id |
|
34 |
|
|
35 |
let compare d1 d2 = |
|
36 |
if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id |
|
37 |
|
|
30 | 38 |
let hash n = Hashtbl.hash n |
31 | 39 |
end |
32 | 40 |
|
33 |
module CSet = Set.Make(ConstraintModule) |
|
41 |
module CSet = Set.Make (ConstraintModule)
|
|
34 | 42 |
|
35 |
(** [check_expr env expr] checks expression [expr] and gathers constraints |
|
36 |
in set [checks]. *)
|
|
43 |
(** [check_expr env expr] checks expression [expr] and gathers constraints in
|
|
44 |
set [checks]. *) |
|
37 | 45 |
let rec check_expr checks expr = |
38 |
(*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr Types.print_ty expr.expr_type;*) |
|
39 |
let res = |
|
40 |
match expr.expr_desc with |
|
41 |
| Expr_const _ |
|
42 |
| Expr_ident _ -> checks |
|
43 |
| Expr_array elist -> List.fold_left check_expr checks elist |
|
44 |
| Expr_access (e1, d) -> check_expr (CSet.add (Dimension.check_access expr.expr_loc (Types.array_type_dimension e1.expr_type) d) checks) e1 |
|
46 |
(*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr |
|
47 |
Types.print_ty expr.expr_type;*) |
|
48 |
let res = |
|
49 |
match expr.expr_desc with |
|
50 |
| Expr_const _ | Expr_ident _ -> |
|
51 |
checks |
|
52 |
| Expr_array elist -> |
|
53 |
List.fold_left check_expr checks elist |
|
54 |
| Expr_access (e1, d) -> |
|
55 |
check_expr |
|
56 |
(CSet.add |
|
57 |
(Dimension.check_access expr.expr_loc |
|
58 |
(Types.array_type_dimension e1.expr_type) |
|
59 |
d) |
|
60 |
checks) |
|
61 |
e1 |
|
45 | 62 |
(* TODO: check dimensions *) |
46 |
|
|
47 |
| Expr_power (e1, _) -> check_expr checks e1 |
|
48 |
|
|
49 |
| Expr_tuple elist -> List.fold_left check_expr checks elist |
|
50 |
|
|
51 |
| Expr_ite (c, t, e) -> List.fold_left check_expr checks [c; t; e] |
|
52 |
|
|
53 |
| Expr_appl (_, args, _) -> check_expr checks args |
|
54 |
|
|
55 |
| Expr_fby (e1,e2) |
|
56 |
| Expr_arrow (e1,e2) -> check_expr (check_expr checks e1) e2 |
|
57 |
| Expr_pre e1 |
|
58 |
| Expr_when (e1,_,_) -> check_expr checks e1 |
|
59 |
|
|
60 |
| Expr_merge (_,hl) -> List.fold_left (fun checks (_, h) -> check_expr checks h) checks hl |
|
61 |
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res |
|
63 |
| Expr_power (e1, _) -> |
|
64 |
check_expr checks e1 |
|
65 |
| Expr_tuple elist -> |
|
66 |
List.fold_left check_expr checks elist |
|
67 |
| Expr_ite (c, t, e) -> |
|
68 |
List.fold_left check_expr checks [ c; t; e ] |
|
69 |
| Expr_appl (_, args, _) -> |
|
70 |
check_expr checks args |
|
71 |
| Expr_fby (e1, e2) | Expr_arrow (e1, e2) -> |
|
72 |
check_expr (check_expr checks e1) e2 |
|
73 |
| Expr_pre e1 | Expr_when (e1, _, _) -> |
|
74 |
check_expr checks e1 |
|
75 |
| Expr_merge (_, hl) -> |
|
76 |
List.fold_left (fun checks (_, h) -> check_expr checks h) checks hl |
|
77 |
in |
|
78 |
(*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr |
|
79 |
Location.pp_loc expr.expr_loc Types.print_ty res;*) |
|
80 |
res |
|
62 | 81 |
|
63 | 82 |
let rec check_var_decl_type loc checks ty = |
64 |
if Types.is_array_type ty |
|
65 |
then |
|
83 |
if Types.is_array_type ty then |
|
66 | 84 |
check_var_decl_type loc |
67 |
(CSet.add (Dimension.check_bound loc (Types.array_type_dimension ty)) checks) |
|
68 |
(Types.array_element_type ty) |
|
85 |
(CSet.add |
|
86 |
(Dimension.check_bound loc (Types.array_type_dimension ty)) |
|
87 |
checks) |
|
88 |
(Types.array_element_type ty) |
|
69 | 89 |
else checks |
70 | 90 |
|
71 | 91 |
let check_var_decl checks vdecl = |
72 | 92 |
check_var_decl_type vdecl.var_loc checks vdecl.var_type |
73 | 93 |
|
74 |
(** [check_node nd] checks node [nd]. |
|
75 |
The resulting constraints are stored in nodes. *)
|
|
94 |
(** [check_node nd] checks node [nd]. The resulting constraints are stored in
|
|
95 |
nodes. *) |
|
76 | 96 |
let check_node nd = |
77 | 97 |
let checks = CSet.empty in |
78 |
let checks = |
|
79 |
List.fold_left check_var_decl checks (get_node_vars nd) in |
|
98 |
let checks = List.fold_left check_var_decl checks (get_node_vars nd) in |
|
80 | 99 |
let checks = |
81 | 100 |
let eqs, auts = get_node_eqs nd in |
82 |
assert (auts = []); (* Not checking automata yet . *) |
|
83 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks eqs in |
|
101 |
assert (auts = []); |
|
102 |
(* Not checking automata yet . *) |
|
103 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks eqs |
|
104 |
in |
|
84 | 105 |
nd.node_checks <- CSet.elements checks |
85 | 106 |
|
86 | 107 |
let check_top_decl decl = |
87 |
match decl.top_decl_desc with |
|
88 |
| Node nd -> check_node nd |
|
89 |
| _ -> () |
|
90 |
|
|
91 |
let check_prog decls = |
|
92 |
List.iter check_top_decl decls |
|
108 |
match decl.top_decl_desc with Node nd -> check_node nd | _ -> () |
|
93 | 109 |
|
110 |
let check_prog decls = List.iter check_top_decl decls |
|
94 | 111 |
|
95 | 112 |
(* Local Variables: *) |
96 | 113 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
reformatting