Revision ca7ff3f7
Added by Lélio Brun 7 months 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