Benjamin_Loison/Synchronous_reactive_systems
1
0
Fork 0
Code Issues 7 Pull Requests Packages Projects Releases Wiki Activity

[passes] pass to check the typing tags of the program / expressions

Browse Source
This commit is contained in:
Arnaud DABY-SEESARAM 2022-12-15 18:33:04 +01:00
parent db5c584435
commit 8582337774
8 changed files with 286 additions and 205 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/ast.ml
View File

@ -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

3
src/main.ml
View File

@ -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 *)

8
src/parser.mly
View File

@ -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()))
}

460
src/passes.ml
View File

@ -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

4
src/passes_utils.ml
View File

@ -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

1
src/test.node
View File

@ -1,4 +1,5 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let i: int;
let
(o1, o2) = (i, i);
tel

5
src/test2.node
View File

@ -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

8
src/utils.ml
View File

@ -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)