From 858233777421c119c2ef2a87aced19066a25bb0a Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Thu, 15 Dec 2022 18:33:04 +0100 Subject: [PATCH] [passes] pass to check the typing tags of the program / expressions --- src/ast.ml | 2 - src/main.ml | 3 +- src/parser.mly | 8 +- src/passes.ml | 460 +++++++++++++++++++++++++------------------- src/passes_utils.ml | 4 +- src/test.node | 1 + src/test2.node | 5 +- src/utils.ml | 8 + 8 files changed, 286 insertions(+), 205 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index ffa3ef1..fe087cf 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -69,8 +69,6 @@ and t_node = n_local_vars: t_varlist; n_equations: t_eqlist; n_automata: t_autolist; - n_inputs_type : full_ty; - n_outputs_type : full_ty; } type t_nodelist = t_node list diff --git a/src/main.ml b/src/main.ml index 2df8c12..c1334ea 100644 --- a/src/main.ml +++ b/src/main.ml @@ -26,7 +26,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) let default_passes = ["pre2vars"; "linearization"; "equations_ordering"] in - let sanity_passes = ["chkvar_init_unicity"] in + let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ [-o output_file] [-m main_function] source_file\n" in @@ -72,6 +72,7 @@ let _ = ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("linearization", Passes.pass_linearization); ("equations_ordering", Passes.pass_eq_reordering); + ("check_typing", Passes.pass_typing); ]; (** Main functionality below *) diff --git a/src/parser.mly b/src/parser.mly index 3d39a12..4722140 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -198,9 +198,7 @@ node_content: n_outputs = (t_out, e_out); n_local_vars = $10; n_equations = eqs; - n_automata = aut; - n_inputs_type = t_in; - n_outputs_type = t_out; } in + n_automata = aut; } in if Hashtbl.find_opt defined_nodes node_name <> None then raise (MyParsingError (Format.asprintf "The node %s is already defined." @@ -386,8 +384,8 @@ expr: { let name = $1 in let node = fetch_node name in let args = $3 in - if type_exp args = node.n_inputs_type - then EApp (node.n_outputs_type, fetch_node name, args) + if type_exp args = fst node.n_inputs + then EApp (fst node.n_outputs, fetch_node name, args) else raise (MyParsingError ("The application does not type check!", current_location())) } diff --git a/src/passes.ml b/src/passes.ml index 34363ff..52f3bbf 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -2,6 +2,7 @@ open Ast open Passes_utils +open Utils let pre2vars verbose debug main_fn = let rec all_pre expr = @@ -13,212 +14,285 @@ let pre2vars verbose debug main_fn = in let rec pre_push expr : t_expression = match expr with - | EVar _ -> EMonOp (Utils.type_exp expr, MOp_pre, expr) + | EVar _ -> EMonOp (type_exp expr, MOp_pre, expr) | EConst _ -> expr (** pre(c) = c for any constant c *) | EMonOp (ty, mop, expr) -> begin match mop with - | MOp_pre -> - if all_pre expr - then EMonOp (ty, mop, EMonOp (ty, mop, expr)) - else pre_push (pre_push expr) - | _ -> EMonOp (ty, mop, pre_push expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = pre_push expr in let expr' = pre_push expr' in - let expr'' = pre_push expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EReset (ty, expr, expr') - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = pre_push arg in - EApp (ty, node, arg) - in - let rec aux (expr: t_expression) = - match expr with - | EVar _ -> expr - | EMonOp (ty, mop, expr) -> - begin - match mop with - | MOp_pre -> pre_push expr - | _ -> let expr = aux expr in EMonOp (ty, mop, expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = aux expr in let expr' = aux expr' in - let expr'' = aux expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EReset (ty, expr, expr') - | EConst (ty, c) -> EConst (ty, c) - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = aux arg in - EApp (ty, node, arg) - in - expression_pass (Utils.somify aux) + | MOp_pre -> + if all_pre expr + then EMonOp (ty, mop, EMonOp (ty, mop, expr)) + else pre_push (pre_push expr) + | _ -> EMonOp (ty, mop, pre_push expr) + end + | EBinOp (ty, bop, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EBinOp (ty, bop, expr, expr') + | ETriOp (ty, top, expr, expr', expr'') -> + let expr = pre_push expr in let expr' = pre_push expr' in + let expr'' = pre_push expr'' in + ETriOp (ty, top, expr, expr', expr'') + | EComp (ty, cop, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EComp (ty, cop, expr, expr') + | EWhen (ty, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EWhen (ty, expr, expr') + | EReset (ty, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EReset (ty, expr, expr') + | ETuple (ty, elist) -> + let elist = + List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in + ETuple (ty, elist) + | EApp (ty, node, arg) -> + let arg = pre_push arg in + EApp (ty, node, arg) +in +let rec aux (expr: t_expression) = + match expr with + | EVar _ -> expr + | EMonOp (ty, mop, expr) -> + begin + match mop with + | MOp_pre -> pre_push expr + | _ -> let expr = aux expr in EMonOp (ty, mop, expr) + end + | EBinOp (ty, bop, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EBinOp (ty, bop, expr, expr') + | ETriOp (ty, top, expr, expr', expr'') -> + let expr = aux expr in let expr' = aux expr' in + let expr'' = aux expr'' in + ETriOp (ty, top, expr, expr', expr'') + | EComp (ty, cop, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EComp (ty, cop, expr, expr') + | EWhen (ty, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EWhen (ty, expr, expr') + | EReset (ty, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EReset (ty, expr, expr') + | EConst (ty, c) -> EConst (ty, c) + | ETuple (ty, elist) -> + let elist = + List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in + ETuple (ty, elist) + | EApp (ty, node, arg) -> + let arg = aux arg in + EApp (ty, node, arg) +in +expression_pass (somify aux) let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option = - let aux (node: t_node) : t_node option = - let incr_aux h n = - match Hashtbl.find_opt h n with - | None -> failwith "todo, should not happend." - | Some num -> Hashtbl.replace h n (num + 1) - in - let incr_eq h (((_, patt), _): t_equation) = - List.iter (fun v -> incr_aux h (Utils.name_of_var v)) patt - in - let rec incr_eqlist h = function - | [] -> () - | eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs) - in - let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in - let incr_automata h ((_, states): t_automaton) = - let acc = Hashtbl.copy h in - List.iter - (fun st -> - let h_st = Hashtbl.copy h in - incr_branch h_st st; - Hashtbl.iter - (fun varname num' -> - match Hashtbl.find_opt acc varname with - | None -> failwith "non!" - | Some num -> Hashtbl.replace acc varname (Int.max num num') - ) h_st) states; - Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc - in - let check_now h : bool= - Hashtbl.fold - (fun varname num old_res -> - if num > 1 - then (verbose (Format.asprintf "%s initialized twice!" varname); false) - else old_res) h true - in - (*let purge_initialized h = - Hashtbl.iter - (fun varname num -> - if num > 0 - then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname) - else ()) h - in*) - let h = Hashtbl.create Config.maxvar in - let add_var n v = - match v with - | IVar s -> Hashtbl.add h s n - | BVar s -> Hashtbl.add h s n - | RVar s -> Hashtbl.add h s n +let aux (node: t_node) : t_node option = + let incr_aux h n = + match Hashtbl.find_opt h n with + | None -> failwith "todo, should not happend." + | Some num -> Hashtbl.replace h n (num + 1) in - let add_var_in = add_var 1 in - let add_var_loc = add_var 0 in - List.iter add_var_in (snd node.n_inputs); - List.iter add_var_loc (snd node.n_outputs); - List.iter add_var_loc (snd node.n_local_vars); - (** Usual Equations *) - incr_eqlist h node.n_equations; - if check_now h = false - then None - else - begin - List.iter (* 0. *) (incr_automata h) node.n_automata; - if check_now h - then Some node - else None - end - (** never purge -> failwith never executed! purge_initialized h; *) + let incr_eq h (((_, patt), _): t_equation) = + List.iter (fun v -> incr_aux h (name_of_var v)) patt + in + let rec incr_eqlist h = function + | [] -> () + | eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs) + in + let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in + let incr_automata h ((_, states): t_automaton) = + let acc = Hashtbl.copy h in + List.iter + (fun st -> + let h_st = Hashtbl.copy h in + incr_branch h_st st; + Hashtbl.iter + (fun varname num' -> + match Hashtbl.find_opt acc varname with + | None -> failwith "non!" + | Some num -> Hashtbl.replace acc varname (Int.max num num') + ) h_st) states; + Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc + in + let check_now h : bool= + Hashtbl.fold + (fun varname num old_res -> + if num > 1 + then (verbose (Format.asprintf "%s initialized twice!" varname); false) + else old_res) h true + in + (*let purge_initialized h = + Hashtbl.iter + (fun varname num -> + if num > 0 + then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname) + else ()) h + in*) + let h = Hashtbl.create Config.maxvar in + let add_var n v = + match v with + | IVar s -> Hashtbl.add h s n + | BVar s -> Hashtbl.add h s n + | RVar s -> Hashtbl.add h s n in - node_pass aux + let add_var_in = add_var 1 in + let add_var_loc = add_var 0 in + List.iter add_var_in (snd node.n_inputs); + List.iter add_var_loc (snd node.n_outputs); + List.iter add_var_loc (snd node.n_local_vars); + (** Usual Equations *) + incr_eqlist h node.n_equations; + if check_now h = false + then None + else + begin + List.iter (* 0. *) (incr_automata h) node.n_automata; + if check_now h + then Some node + else None + end + (** never purge -> failwith never executed! purge_initialized h; *) +in +node_pass aux let pass_linearization verbose debug main_fn = - let node_lin (node: t_node): t_node option = - let rec tpl ((pat, exp): t_equation) = - match exp with - | ETuple (_, hexps :: texps) -> - debug "An ETuple has been recognized, inlining..."; - let p1, p2 = - Utils.list_select - (List.length (Utils.type_exp hexps)) - (snd pat) in - let t1 = List.flatten (List.map Utils.type_var p1) in - let t2 = List.flatten (List.map Utils.type_var p2) in - ((t1, p1), hexps) - :: (tpl ((t2, p2), - ETuple (List.flatten (List.map Utils.type_exp texps), texps))) - | ETuple (_, []) -> [] - | _ -> [(pat, exp)] - in - let new_locvars = node.n_local_vars in - let new_equations = List.flatten - begin - List.map - tpl - node.n_equations - end in - Some - { - n_name = node.n_name; - n_inputs = node.n_inputs; - n_outputs = node.n_outputs; - n_local_vars = new_locvars; - n_equations = new_equations; - n_automata = node.n_automata; - n_inputs_type = node.n_inputs_type; - n_outputs_type = node.n_outputs_type; - } +let node_lin (node: t_node): t_node option = + let rec tpl ((pat, exp): t_equation) = + match exp with + | ETuple (_, hexps :: texps) -> + debug "An ETuple has been recognized, inlining..."; + let p1, p2 = + list_select + (List.length (type_exp hexps)) + (snd pat) in + let t1 = List.flatten (List.map type_var p1) in + let t2 = List.flatten (List.map type_var p2) in + ((t1, p1), hexps) + :: (tpl ((t2, p2), + ETuple (List.flatten (List.map type_exp texps), texps))) + | ETuple (_, []) -> [] + | _ -> [(pat, exp)] in - node_pass node_lin + let new_locvars = node.n_local_vars in + let new_equations = List.flatten + begin + List.map + tpl + node.n_equations + end in + Some + { + n_name = node.n_name; + n_inputs = node.n_inputs; + n_outputs = node.n_outputs; + n_local_vars = new_locvars; + n_equations = new_equations; + n_automata = node.n_automata; + } +in +node_pass node_lin let pass_eq_reordering verbose debug main_fn ast = - let rec pick_equations init_vars eqs remaining_equations = - match remaining_equations with - | [] -> Some eqs - | _ -> - begin - match List.filter - (fun (patt, expr) -> - List.for_all - (fun v -> List.mem v init_vars) - (Utils.vars_of_expr expr)) - remaining_equations with - | [] -> raise EquationOrderingIssue - | h :: t -> - let init_vars = - List.fold_left - (fun acc vs -> - acc @ (Utils.vars_of_patt (fst vs))) init_vars (h :: t) in - pick_equations init_vars (eqs@(h :: t)) - (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations) - end - in - let node_eq_reorganising (node: t_node): t_node option = - let init_vars = List.map Utils.name_of_var (snd node.n_inputs) in +let rec pick_equations init_vars eqs remaining_equations = + match remaining_equations with + | [] -> Some eqs + | _ -> + begin + match List.filter + (fun (patt, expr) -> + List.for_all + (fun v -> List.mem v init_vars) + (vars_of_expr expr)) + remaining_equations with + | [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.") + | h :: t -> + let init_vars = + List.fold_left + (fun acc vs -> + acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in + pick_equations init_vars (eqs@(h :: t)) + (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations) + end + in +let node_eq_reorganising (node: t_node): t_node option = + let init_vars = List.map name_of_var (snd node.n_inputs) in + try + begin match pick_equations init_vars [] node.n_equations with | None -> None | Some eqs -> Some { node with n_equations = eqs } - in - node_pass node_eq_reorganising ast + end + with PassExn err -> (verbose err; None) +in +node_pass node_eq_reorganising ast + +let pass_typing verbose debug main_fn ast = + let htbl = Hashtbl.create (List.length ast) in + let () = debug "[typing verification]" in + let () = List.iter + (fun n -> Hashtbl.add htbl n.n_name (fst n.n_inputs, fst n.n_outputs)) + ast in + let rec check_varlist vl = + let t = fst vl in + let l = snd vl in + match t, l with + | [], [] -> true + | TInt :: t, IVar _ :: l -> check_varlist (t, l) + | TBool :: t, BVar _ :: l -> check_varlist (t, l) + | TReal :: t, RVar _ :: l -> check_varlist (t, l) + | _, _ -> false + in + let rec check_expr vl = function + | EVar (t, v) -> t = type_var v + | EMonOp (t, _, e) -> check_expr vl e && type_exp e = t + | EBinOp (t, _, e, e') -> check_expr vl e && check_expr vl e' + && t = type_exp e && t = type_exp e' + | ETriOp (t, _, c, e, e') -> + check_expr vl e && check_expr vl e' && check_expr vl c + && type_exp c = [TBool] && type_exp e = t && type_exp e' = t + | EComp (t, _, e, e') -> + check_expr vl e && check_expr vl e' && t = [TBool] + | EWhen (t, e, e') -> + check_expr vl e && check_expr vl e' + && t = type_exp e && [TBool] = type_exp e' + | EReset (t, e, e') -> + check_expr vl e && check_expr vl e' && t = type_exp e && type_exp e' = [TBool] + | EConst (t, c) -> type_const c = t + | ETuple (t, l) -> + List.for_all (check_expr vl) l + && t = List.flatten (List.map type_exp l) + | EApp (t, n, e) -> + check_expr vl e && t = (fst n.n_outputs) && type_exp e = (fst n.n_inputs) + in + let check_equation vl ((peq, eeq): t_equation) = + if check_varlist peq + then + if check_expr vl eeq + then fst peq = type_exp eeq + else false + else false + in + let rec check_equations vl = function + | [] -> true + | eq :: eqs -> + if check_equation vl eq + then check_equations vl eqs + else false + in + let check_one_node node = + check_varlist (node.n_inputs) + && check_varlist (node.n_outputs) + && check_varlist (node.n_local_vars) + && check_equations + (varlist_concat node.n_inputs + (varlist_concat node.n_outputs node.n_local_vars)) + node.n_equations + in + let rec aux = function + | [] -> Some ast + | n :: nodes -> + if check_one_node n + then aux nodes + else None + in aux ast + diff --git a/src/passes_utils.ml b/src/passes_utils.ml index f1a6426..0e159d9 100644 --- a/src/passes_utils.ml +++ b/src/passes_utils.ml @@ -18,8 +18,6 @@ let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option = n_local_vars = node.n_local_vars; n_equations = eqs; n_automata = node.n_automata; - n_inputs_type = node.n_inputs_type; - n_outputs_type = node.n_outputs_type; } in node_pass aux ast @@ -32,4 +30,4 @@ let expression_pass f: t_nodelist -> t_nodelist option = in equation_pass aux -exception EquationOrderingIssue +exception PassExn of string diff --git a/src/test.node b/src/test.node index 5b65c18..9200b38 100644 --- a/src/test.node +++ b/src/test.node @@ -1,4 +1,5 @@ node diagonal_int (i: int) returns (o1, o2 : int); +let i: int; let (o1, o2) = (i, i); tel diff --git a/src/test2.node b/src/test2.node index 58ac619..36209a1 100644 --- a/src/test2.node +++ b/src/test2.node @@ -1,4 +1,7 @@ node diagonal_int (i: int) returns (o1, o2 : int); +var y: int; let - (o1, o2) = (i, i); + o2 = y; + y = i; + o1 = i; tel diff --git a/src/utils.ml b/src/utils.ml index 58e09f3..fa769a1 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -24,6 +24,11 @@ let rec list_chk v = function exception MyParsingError of (string * location) +let type_const = function + | CReal _ -> [TReal] + | CInt _ -> [TInt ] + | CBool _ -> [TBool] + let type_var (v: t_var) = match v with | IVar _ -> [TInt] @@ -77,3 +82,6 @@ let rec vars_of_expr (expr: t_expression) : ident list = (vars_of_expr e) @ (vars_of_expr e') @ (vars_of_expr e'') | ETuple (_, l) -> List.flatten (List.map vars_of_expr l) +let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist = + (fst l1 @ fst l2, snd l1 @ snd l2) +