diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index bca0ea2..3e3bbe8 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -288,29 +288,28 @@ let rec cp_nodes fmt (nodes, h) = -let dump_var_locations (st: node_states) = +(** [dump_var_locations] dumps the internal tables to map the program variable + * (after all the passes) to their location in the final C program. *) +let dump_var_locations fmt (st: node_states) = + Format.fprintf fmt "Tables mapping the AST Variables to the C variables:\n"; Hashtbl.iter (fun n st -> - Format.printf "\n\n\tNODE: %s\n" n; + Format.fprintf fmt " ∗ NODE: %s\n" n; Hashtbl.iter (fun (s, (ispre: bool)) ((arr: string), (idx: int)) -> match ispre with - | true -> Format.printf "PRE Variable %s stored as %s[%d]\n" s arr idx - | false -> Format.printf " Variable %s stored as %s[%d]\n" s arr idx) + | true -> Format.fprintf fmt " PRE Variable %s stored as %s[%d]\n" s arr idx + | false -> Format.fprintf fmt " Variable %s stored as %s[%d]\n" s arr idx) st.nt_map) - st; - Format.printf "\n\n" + st (** main function that prints a C-code from a term of type [t_nodelist]. *) -let ast_to_c (debug: bool) prog = +let ast_to_c verbose debug prog = + verbose "Computation of the node_states"; let prog_st_types = make_state_types prog in - let () = - if debug - then dump_var_locations prog_st_types - else () - in + debug (Format.asprintf "%a" dump_var_locations prog_st_types); let prog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in Format.printf "%a\n\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) diff --git a/src/main.ml b/src/main.ml index 83d407f..3711c06 100644 --- a/src/main.ml +++ b/src/main.ml @@ -9,24 +9,44 @@ 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 () + + +(** [exec_passes] executes the passes on the parsed typed-AST. + * A pass should return [Some program] in case of a success, and [None] + * otherwise. + * + * The function [exec_passes] returns the optionnal program returned by the + * last pass. + * + * A pass should never be interrupted by an exception. Nevertheless, we make + * sure that no pass raise one. *) let exec_passes ast 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 - | 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 Lustre_pp.pp_ast ast); - aux ast passes) + try + begin + match p verbose debug 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 Lustre_pp.pp_ast ast); + aux ast passes) + end with + | _ -> failwith ("[main.ml] The pass "^n^" should have catched me!") in aux ast passes + let _ = (** Usage and argument parsing. *) - let default_passes = ["remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; - "equations_ordering"] in + let default_passes = + ["remove_if"; + "linearization_pre"; "linearization_tuples"; "linearization_app"; + "equations_ordering"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -106,6 +126,11 @@ let _ = end in + (** Computes the list of passes to execute. If the [-test] flag is set, all + * sanity passes (ie. passes which do not modify the AST, but ensure its + * validity) are re-run after any other pass. + * + * Note: the sanity passes are always executed before any other. *) let passes = List.map (fun (pass: string) -> (pass, @@ -129,6 +154,6 @@ let _ = else ( if !nopopt then (fun _ -> ()) - else Ast_to_c.ast_to_c !debug) + else Ast_to_c.ast_to_c print_verbose print_debug) end diff --git a/src/passes.ml b/src/passes.ml index 352bb65..0566934 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -4,6 +4,8 @@ open Ast open Passes_utils open Utils + + (** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones. * * [x1, ..., xn = if c then e_l else e_r;] @@ -18,7 +20,8 @@ open Utils * order to have the expressions active at each step. *) let pass_if_removal verbose debug = - let varcount = ref 0 in + let varcount = ref 0 in (** new variables are called «_ifrem[varcount]» *) + (** Males a pattern (t_varlist) of fresh variables matching the type t *) let make_patt t: t_varlist = (t, List.fold_right (fun ty acc -> @@ -33,11 +36,14 @@ let pass_if_removal verbose debug = nvar :: acc) t []) in + (** If a tuple contains a single element, it should not be. *) let simplify_tuple t = match t with | ETuple (t, [elt]) -> elt | _ -> t in + (** For each equation, build a list of equations and a new list of local + * variables as well as an updated version of the original equation. *) let rec aux_eq vars eq: t_eqlist * t_varlist * t_equation = let patt, expr = eq in match expr with @@ -127,6 +133,7 @@ let pass_if_removal verbose debug = let eqs, vars, (_, e) = aux_eq vars (patt, e) in eqs, vars, (patt, EApp (t, n, e)) in + (** For each node, apply the previous function to all equations. *) let aux_if_removal node = let new_equations, new_locvars = List.fold_left @@ -139,7 +146,23 @@ let pass_if_removal verbose debug = in node_pass aux_if_removal + + +(** [pass_linearization_tuples] transforms expressions of the form + * (x1, ..., xn) = (e1, ..., em); + * into: + * p1 = e1; + * ... + * pm = em; + * where flatten (p1, ..., pm) = x1, ..., xn + * + * Idem for tuples hidden behind merges and when: + * patt = (...) when c; + * patt = merge c (...) (...); + *) let pass_linearization_tuples verbose debug ast = + (** [split_tuple] takes an equation and produces an equation list + * corresponding to the [pi = ei;] above. *) let rec split_tuple (eq: t_equation): t_eqlist = let patt, expr = eq in match expr with @@ -154,6 +177,9 @@ let pass_linearization_tuples verbose debug ast = | ETuple (_, []) -> [] | _ -> [eq] in + (** For each node, apply the previous function to all equations. + * It builds fake equations in order to take care of tuples behind + * merge/when. *) let aux_linearization_tuples node = let new_equations = List.flatten (List.map @@ -186,8 +212,15 @@ let pass_linearization_tuples verbose debug ast = try node_pass aux_linearization_tuples ast with | PassExn err -> (debug err; None) + + +(** [pass_linearization_app] makes sure that any argument to a function is + * either a variable, or of the form [pre _] (which will be translated as a + * variable in the final C code. *) let pass_linearization_app verbose debug = - let applin_count = ref 0 in + let applin_count = ref 0 in (* new variables are called «_applin[varcount]» *) + (** [aux_expr] recursively explores the AST in order to find applications, and + * adds the requires variables and equations. *) let rec aux_expr vars expr: t_eqlist * t_varlist * t_expression = match expr with | EConst _ | EVar _ -> [], vars, expr @@ -253,16 +286,13 @@ let pass_linearization_app verbose debug = eqs, vars, EApp (tout, n, ETuple (tin, l)) | EApp _ -> failwith "[passes.ml] Should not happened (parser)" in - let aux vars eq = - let eqs, vars, expr = aux_expr vars (snd eq) in - (fst eq, expr) :: eqs, vars - in + (** [aux_linearization_app] applies the previous function to every equation *) let aux_linearization_app node = let new_equations, new_locvars = List.fold_left (fun (eqs, vars) eq -> - let es, vs = aux vars eq in - es @ eqs, vs) + let eqs', vars, expr = aux_expr vars (snd eq) in + (fst eq, expr) :: eqs' @ eqs, vars) ([], node.n_local_vars) node.n_equations in @@ -270,6 +300,8 @@ let pass_linearization_app verbose debug = in node_pass aux_linearization_app + + let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = let aux (node: t_node) : t_node option = let incr_aux h n = @@ -363,8 +395,11 @@ let pass_linearization_pre verbose debug = | EVar _ -> [], vars, expr | EMonOp (t, op, e) -> begin - match op with - | MOp_pre -> + match op, e with + | MOp_pre, EVar _ -> + let eqs, vars, e = pre_aux_expression vars e in + eqs, vars, EMonOp (t, op, e) + | MOp_pre, _ -> let eqs, vars, e = pre_aux_expression vars e in let nvar: string = fresh_var_name vars 6 in let nvar = match t with @@ -376,7 +411,7 @@ let pass_linearization_pre verbose debug = let neq_expr: t_expression = e in let vars = varlist_concat (t, [nvar]) vars in (neq_patt, neq_expr) :: eqs, vars, EMonOp (t, MOp_pre, EVar (t, nvar)) - | _ -> + | _, _ -> let eqs, vars, e = pre_aux_expression vars e in eqs, vars, EMonOp (t, op, e) end diff --git a/src/test.node b/src/test.node index 6dd535f..d6f531d 100644 --- a/src/test.node +++ b/src/test.node @@ -1,10 +1,15 @@ +node id (a: bool) returns (o: bool); +let + o = a; +tel + node test_merge_tuples (a, b: bool) returns (o: bool); var t: bool; let (o, t) = if a and b then (true, false) else (false, true); tel ---node my_and (a, b: bool) returns (o: bool); ---let --- o = if a then b else false; ---tel +node my_and (a, b: bool) returns (o: bool); +let + o = if a then b else id(false -> a); +tel