From e75d525a6dd5ddded277fec344681300541e2e9f Mon Sep 17 00:00:00 2001 From: dsac Date: Thu, 15 Dec 2022 09:13:28 +0100 Subject: [PATCH] =?UTF-8?q?[passes]=20linearisation=20des=20=C3=A9quations?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/main.ml | 34 +++++++++++++------ src/parser.mly | 6 ++++ src/passes.ml | 83 ++++++++++++++++++++++----------------------- src/passes_utils.ml | 33 ++++++++++++++++++ src/test2.node | 4 +++ src/utils.ml | 21 ++++++++++++ 6 files changed, 127 insertions(+), 54 deletions(-) create mode 100644 src/passes_utils.ml create mode 100644 src/test2.node diff --git a/src/main.ml b/src/main.ml index 447e598..6edbada 100644 --- a/src/main.ml +++ b/src/main.ml @@ -9,12 +9,12 @@ let print_debug d s = let print_verbose v s = if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else () -let exec_passes ast verbose debug passes f = +let exec_passes ast main_fn verbose debug passes f = let rec aux ast = function | [] -> f ast | (n, p) :: passes -> verbose (Format.asprintf "Executing pass %s:\n" n); - match p verbose debug ast with + match p verbose debug main_fn ast with | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0) | Some ast -> ( debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast); @@ -25,15 +25,17 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["chkvar_init_unicity"; "pre2vars"] in + let default_passes = ["chkvar_init_unicity"; "pre2vars"; "linearization"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ - [-o output_file] source_file\n" in + [-o output_file] [-m main_function] source_file\n" in let verbose = ref false in let debug = ref false in let ppast = ref false in let nopopt = ref false in + let simopt = ref false in let passes = ref [] in + let main_fn = ref "main" in let source_file = ref "" in let output_file = ref "out.c" in let anon_fun filename = source_file := filename in @@ -45,6 +47,9 @@ let _ = ("-debug", Arg.Set debug, "Output a lot of debug information"); ("-p", Arg.String (fun s -> passes := s :: !passes), "Add a pass to the compilation process"); + ("-sim", Arg.Set simopt, "Simulate the main node"); + ("-m", Arg.String (fun s -> main_fn := s), + "Defines what the main function is (defaults to main)."); ("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])"); ] in Arg.parse speclist anon_fun usage_msg ; @@ -52,6 +57,7 @@ let _ = if !passes = [] then passes := default_passes; let print_verbose = print_verbose !verbose in let print_debug = print_debug !debug in + let main_fn = !main_fn in (** Definition of the passes table *) let passes_table = Hashtbl.create 100 in @@ -59,6 +65,7 @@ let _ = [ ("pre2vars", Passes.pre2vars); ("chkvar_init_unicity", Passes.chkvar_init_unicity); + ("linearization", Passes.pass_linearization); ]; (** Main functionality below *) @@ -101,13 +108,18 @@ let _ = print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" Pp.pp_ast ast) ; - exec_passes ast print_verbose print_debug passes + exec_passes ast main_fn print_verbose print_debug passes begin - if !ppast - then (Format.printf "%a" Pp.pp_ast) - else ( - if !nopopt - then (fun _ -> ()) - else Format.printf "%a" Ast_to_c.ast_to_c) + if !simopt + then Simulation.simulate main_fn + else + begin + if !ppast + then (Format.printf "%a" Pp.pp_ast) + else ( + if !nopopt + then (fun _ -> ()) + else Format.printf "%a" Ast_to_c.ast_to_c) + end end diff --git a/src/parser.mly b/src/parser.mly index 2c72e62..3d39a12 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -161,6 +161,12 @@ %token CONST_BOOL %token CONST_REAL +%left MO_not +%left MO_pre +%left PLUS +%left MINUS +%left BO_and BO_or BO_mul BO_div BO_mod BO_arrow BO_fby TO_merge + /* The Entry Point */ %start main %type main diff --git a/src/passes.ml b/src/passes.ml index a6d9c66..bbb7b19 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -1,40 +1,9 @@ (** This file contains simplification passes for our Lustre-like AST *) open Ast +open Passes_utils -(** [node_pass] is an auxiliary function used to write passes: it will iterate - * the function passed as argument on all the nodes of the program *) -let node_pass f ast: t_nodelist option = - Utils.list_map_option f ast - -(** [equation_pass] is an auxiliary function used to write passes: it will - * iterate the function passed as argument on all the equations of the - * program *) -let equation_pass f ast: t_nodelist option = - let aux (node: t_node): t_node option = - match Utils.list_map_option f node.n_equations with - | None -> None - | Some eqs -> Some {n_name = node.n_name; - n_inputs = node.n_inputs; - n_outputs = node.n_outputs; - 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 - -let expression_pass f: t_nodelist -> t_nodelist option = - let aux (patt, expr) = - match f expr with - | None -> None - | Some expr -> Some (patt, expr) - in - equation_pass aux - -let pre2vars verbose debug = +let pre2vars verbose debug main_fn = let rec all_pre expr = match expr with | EMonOp (ty, MOp_pre, expr) -> all_pre expr @@ -115,7 +84,7 @@ let pre2vars verbose debug = in expression_pass (Utils.somify aux) -let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = +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 @@ -129,9 +98,7 @@ let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = | [] -> () | 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 @@ -146,7 +113,6 @@ let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = ) 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 -> @@ -161,9 +127,6 @@ let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = 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 @@ -176,8 +139,6 @@ let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = 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 @@ -190,7 +151,43 @@ let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = 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) -> + 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; + } + in + node_pass node_lin diff --git a/src/passes_utils.ml b/src/passes_utils.ml new file mode 100644 index 0000000..5848189 --- /dev/null +++ b/src/passes_utils.ml @@ -0,0 +1,33 @@ +open Ast + +(** [node_pass] is an auxiliary function used to write passes: it will iterate + * the function passed as argument on all the nodes of the program *) +let node_pass f ast: t_nodelist option = + Utils.list_map_option f ast + +(** [equation_pass] is an auxiliary function used to write passes: it will + * iterate the function passed as argument on all the equations of the + * program *) +let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option = + let aux (node: t_node): t_node option = + match Utils.list_map_option f node.n_equations with + | None -> None + | Some eqs -> Some {n_name = node.n_name; + n_inputs = node.n_inputs; + n_outputs = node.n_outputs; + 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 + +let expression_pass f: t_nodelist -> t_nodelist option = + let aux (patt, expr) = + match f expr with + | None -> None + | Some expr -> Some (patt, expr) + in + equation_pass aux diff --git a/src/test2.node b/src/test2.node new file mode 100644 index 0000000..58ac619 --- /dev/null +++ b/src/test2.node @@ -0,0 +1,4 @@ +node diagonal_int (i: int) returns (o1, o2 : int); +let + (o1, o2) = (i, i); +tel diff --git a/src/utils.ml b/src/utils.ml index f019946..afadb9f 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -1,5 +1,14 @@ open Ast +let rec list_select n = function + | [] -> [], [] + | h :: t -> + if n = 0 + then ([], h :: t) + else + let p1, p2 = list_select (n-1) t in + h :: p1, p2 + let rec list_map_option (f: 'a -> 'b option) (l: 'a list) : 'b list option = List.fold_right (fun elt acc -> match acc, f elt with @@ -39,3 +48,15 @@ let name_of_var: t_var -> ident = function | IVar s -> s | BVar s -> s | RVar s -> s + +let rec fresh_var_name (l: t_varlist) n : ident = + let rec aux acc n = + let r = Random.int 26 in + Format.asprintf "%c%s" + (char_of_int (r + (if Random.bool () then 65 else 97))) + (if n = 0 then acc else aux acc (n-1)) + in + let name = aux "" n in + if List.filter (fun v -> name_of_var v = name) (snd l) = [] + then name + else fresh_var_name l n