From 0da0f58b2293dadef2c74b4654b85497db722db4 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 16:01:48 +0100 Subject: [PATCH 01/50] [ast2C] proposition initiale --- src/ast_to_c.ml | 363 +++++++++++++----------------------------------- src/c_utils.ml | 34 +++++ src/config.ml | 1 + src/cprint.ml | 57 ++++++++ src/main.ml | 2 +- src/passes.ml | 4 +- src/utils.ml | 7 + 7 files changed, 202 insertions(+), 266 deletions(-) create mode 100644 src/c_utils.ml create mode 100644 src/cprint.ml diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 53c6324..014007e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -1,280 +1,117 @@ open Ast +open C_utils +open Cprint +open Utils -type var_list_delim = - | Base - | Arg - | Dec -let rec pp_varlist var_list_delim fmt : t_varlist -> unit = function - | ([], []) -> () - | ([TInt] , IVar h :: []) -> Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s" - | Arg -> "int %s" - | Dec -> "int %s;") h - | ([TReal], RVar h :: []) -> Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s" - | Arg -> "float %s" - | Dec -> "float %s;") h - | ([TBool], BVar h :: []) -> Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s" - | Arg -> "bool %s" - | Dec -> "bool %s;") h - | (TInt :: tl, IVar h :: h' :: l) -> - Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s, %a" - | Arg -> "int %s, %a" - | Dec -> "int %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l) - | (TBool :: tl, BVar h :: h' :: l) -> - Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s, %a" - | Arg -> "bool %s, %a" - | Dec -> "bool %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l) - | (TReal :: tl, RVar h :: h' :: l) -> - Format.fprintf fmt ( - match var_list_delim with - | Base -> "%s, %a" - | Arg -> "float %s, %a" - | Dec -> "float %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l) - | _ -> raise (MyTypeError "This exception should not have beed be raised.") -let rec pp_retvarlist fmt : t_varlist -> unit = function - | ([], []) -> () - | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int" - | ([TReal], RVar h :: []) -> Format.fprintf fmt "float" - | ([TBool], BVar h :: []) -> Format.fprintf fmt "bool" - | (TInt :: tl, IVar h :: h' :: l) -> - Format.fprintf fmt "int, %a" pp_retvarlist (tl, h' :: l) - | (TBool :: tl, BVar h :: h' :: l) -> - Format.fprintf fmt "float, %a" pp_retvarlist (tl, h' :: l) - | (TReal :: tl, RVar h :: h' :: l) -> - Format.fprintf fmt "bool, %a" pp_retvarlist (tl, h' :: l) - | _ -> raise (MyTypeError "This exception should not have beed be raised.") +(** The following function defines the [node_states] for the nodes of a program, + * and puts them in a hash table. *) +let make_state_types nodes: (ident, node_state) Hashtbl.t = + (* Hash table to fill *) + let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in -let rec pp_prevarlist node_name fmt : t_varlist -> unit = function - | ([], []) -> () - | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int pre_%s_%s;" node_name h - | ([TReal], RVar h :: []) -> Format.fprintf fmt "float pre_%s_%s;" node_name h - | ([TBool], BVar h :: []) -> Format.fprintf fmt "bool pre_%s_%s;" node_name h - | (TInt :: tl, IVar h :: h' :: l) -> - Format.fprintf fmt "int pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) - | (TBool :: tl, BVar h :: h' :: l) -> - Format.fprintf fmt "float pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) - | (TReal :: tl, RVar h :: h' :: l) -> - Format.fprintf fmt "bool pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) - | _ -> raise (MyTypeError "This exception should not have beed be raised.") + (** [one_node node pv ty] computes the number of variables of type [ty] in + * [node] and a mapping from the variables of type ([ty] * bool) to int, + * where [pv] is a list of variables used in the pre construct in the + * programm. *) + let one_node node pv ty = + (* variables of type [ty] among output and local variables *) + let vars = + List.filter (fun v -> type_var v = [ty]) + (snd (varlist_concat node.n_outputs node.n_local_vars)) in + let pre_vars = + List.filter (fun v -> List.mem v pv) vars in + let nb = (List.length vars) + (List.length pre_vars) in + let tyh = Hashtbl.create nb in + let i = + List.fold_left + (fun i v -> let () = Hashtbl.add tyh (v, false) i in i + 1) 0 vars in + let _ = + List.fold_left + (fun i v -> let () = Hashtbl.add tyh (v, true) i in i + 1) i pre_vars in + (nb, tyh) + in -let rec pp_asnprevarlist node_name fmt : t_varlist -> unit = function - | ([], []) -> () - | ([TInt] , IVar h :: []) | ([TReal], RVar h :: []) | ([TBool], BVar h :: []) -> Format.fprintf fmt "\tpre_%s_%s = %s;" node_name h h - | (TInt :: tl, IVar h :: h' :: l) | (TBool :: tl, BVar h :: h' :: l) | (TReal :: tl, RVar h :: h' :: l) -> - Format.fprintf fmt "\tpre_%s_%s = %s;\n%a" node_name h h (pp_asnprevarlist node_name) (tl, h' :: l) - | _ -> raise (MyTypeError "This exception should not have beed be raised.") - -let reset_expressions_counter = ref 0;; - -let outputs = ref [];; - -let pp_expression node_name = - let rec pp_expression_aux fmt expression = - let rec pp_expression_list fmt exprs = - match exprs with - | ETuple([], []) -> () - | ETuple (_ :: tt, expr :: exprs) -> - Format.fprintf fmt "%a%s%a" - pp_expression_aux expr - (if (List.length tt > 0) then ", " else "") - pp_expression_list (ETuple (tt, exprs)) - | _ -> raise (MyTypeError "This exception should not have been raised.") + (** [find_prevars n] returns the list of variables appearing after a pre in + * the node [n]. + * Note that the only occurence of pre are of the form pre (var), due to the + * linearization pass. + *) + let find_prevars node = + let rec find_prevars_expr = function + | EConst _ | EVar _ -> [] + | EMonOp (_, MOp_pre, EVar (_, v)) -> [v] + | EMonOp (_, _, e) -> find_prevars_expr e + | ETriOp (_, _, e, e', e'') -> + (find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'') + | EComp (_, _, e, e') + | EBinOp (_, _, e, e') + | EWhen (_, e, e') + | EReset (_, e, e') -> (find_prevars_expr e) @ (find_prevars_expr e') + | ETuple (_, l) -> List.flatten (List.map (find_prevars_expr) l) + | EApp (_, _, e) -> find_prevars_expr e in - match expression with - | EWhen (_, e1, e2) -> + list_remove_duplicates + (List.fold_left + (fun acc (_, expr) -> (find_prevars_expr expr) @ acc) + [] node.n_equations) + in + + (** [aux] iterates over all nodes of the program to build the required hash + * table *) + let rec aux nodes = + match nodes with + | [] -> h + | node :: nodes -> begin - Format.fprintf fmt "%a ? %a : 0" - pp_expression_aux e2 - pp_expression_aux e1 + let h = aux nodes in + let node_name = node.n_name in + let pv = find_prevars node in + let nb_int_vars, h_int = one_node node pv TInt in + let nb_bool_vars, h_bool = one_node node pv TBool in + let nb_real_vars, h_real = one_node node pv TReal in + let node_out_vars = snd node.n_outputs in + let h_out = Hashtbl.create (List.length node_out_vars) in + let () = List.iteri + (fun n v -> + match v with + | IVar _ -> + let i = Hashtbl.find h_int (v, false) in + Hashtbl.add h_out n ("ivars", i) + | BVar _ -> + let i = Hashtbl.find h_bool (v, false) in + Hashtbl.add h_out n ("bvars", i) + | RVar _ -> + let i = Hashtbl.find h_real (v, false) in + Hashtbl.add h_out n ("rvars", i)) + (snd node.n_outputs) in + let () = Hashtbl.add h node_name + { + nt_name = Format.asprintf "t_state_%s" node.n_name; + nt_nb_int = nb_int_vars; + nt_nb_bool = nb_bool_vars; + nt_nb_real = nb_real_vars; + nt_map_int = h_int; + nt_map_bool = h_bool; + nt_map_real = h_real; + nt_output_map = h_out; + } in + h end - | EReset (_, e1, e2) -> - begin - incr reset_expressions_counter; - (* Use following trick as we can't use `;`: - if(((var = val) && false) || condition) - is equivalent to an incorrect statement like - if({var = val; condition}) - We also use this trick with the fact that `0` can be interpreted as a `bool`, an `int` and a `float` *) - (* could use C macros to simplify the C code *) - Format.fprintf fmt "(((tmp_reset[%i] = %a) && false) || init_%s) ? (((init[%i] = tmp_reset[%i]) || true) ? tmp_reset[%i] : 0) : (%a ? init[%i] : tmp_reset[%i])" - (!reset_expressions_counter - 1) - pp_expression_aux e1 - node_name - (!reset_expressions_counter - 1) - (!reset_expressions_counter - 1) - (!reset_expressions_counter - 1) - pp_expression_aux e2 - (!reset_expressions_counter - 1) - (!reset_expressions_counter - 1) - end - | EConst (_, c) -> - begin match c with - | CBool b -> Format.fprintf fmt "%s" (Bool.to_string b) - | CInt i -> Format.fprintf fmt "%i" i - | CReal r -> Format.fprintf fmt "%f" r - end - | EVar (_, IVar v) | EVar (_, BVar v) | EVar (_, RVar v) -> Format.fprintf fmt "%s" v - | EMonOp (_, mop, arg) -> - begin match mop with - | MOp_not -> - Format.fprintf fmt "!%a" - pp_expression_aux arg - | MOp_minus -> - Format.fprintf fmt "-%a" - pp_expression_aux arg - | MOp_pre -> - Format.fprintf fmt "pre_%s_%a" node_name - pp_expression_aux arg - end - | EBinOp (_, BOp_arrow, arg, arg') -> - Format.fprintf fmt "init_%s ? %a : %a" - node_name - pp_expression_aux arg - pp_expression_aux arg' - | EBinOp (_, bop, arg, arg') -> - begin - let s = match bop with - | BOp_add -> " + " | BOp_sub -> " - " - | BOp_mul -> " * " | BOp_div -> " / " | BOp_mod -> " % " - | BOp_and -> " && " | BOp_or -> " || " | _ -> "" (* `ocamlc` doesn't detect that `BOp_arrow` can't match here *) in - Format.fprintf fmt "%a%s%a" - pp_expression_aux arg - s - pp_expression_aux arg' - end - | EComp (_, cop, arg, arg') -> - begin - let s = match cop with - | COp_eq -> " == " - | COp_neq -> " != " - | COp_le -> " <= " | COp_lt -> " < " - | COp_ge -> " >= " | COp_gt -> " > " in - Format.fprintf fmt "%a%s%a" - pp_expression_aux arg - s - pp_expression_aux arg' - end - | ETriOp (_, top, arg, arg', arg'') -> - begin - Format.fprintf fmt "%a ? %a : %a" - pp_expression_aux arg - pp_expression_aux arg' - pp_expression_aux arg'' - end - | EApp (_, f, args) -> - Format.fprintf fmt "%s(%a)" - f.n_name - pp_expression_list args - | ETuple _ -> - Format.fprintf fmt "%a" - pp_expression_list expression; in - pp_expression_aux + aux nodes -(* deterministic *) -let nodes_outputs = Hashtbl.create Config.maxvar;; -let prepend_output_aux node_name name = - "output_" ^ node_name ^ "_" ^ name -let prepend_output output node_name = - match output with - | BVar name -> BVar (prepend_output_aux node_name name) - | IVar name -> IVar (prepend_output_aux node_name name) - | RVar name -> RVar (prepend_output_aux node_name name) +(*let ast_to_c*) -let rec pp_equations node_name fmt: t_eqlist -> unit = function - | [] -> () - | ((l_types, vars), (EApp (r_types, node, exprs))) :: eqs when l_types <> [] -> Format.fprintf fmt "%a" (pp_equations node_name) ((([], []), (EApp (r_types, node, exprs))) :: ((l_types, vars), (ETuple (fst node.n_outputs, List.map (fun output -> EVar (fst node.n_outputs, prepend_output output node.n_name)) (snd node.n_outputs)))) :: eqs) - | (([], []), (ETuple ([], []))) :: eqs -> Format.fprintf fmt "%a" (pp_equations node_name) eqs - | ((l_type :: l_types, var :: vars), (ETuple (r_type :: r_types, expr :: exprs))) :: eqs -> Format.fprintf fmt "%a" (pp_equations node_name) ((([l_type], [var]), expr) :: ((l_types, vars), (ETuple (r_types, exprs))) :: eqs) - | (([], []), expr) :: eqs -> - Format.fprintf fmt "\t%a;\n%a" - (pp_expression node_name) expr - (pp_equations node_name) eqs - | (patt, expr) :: eqs -> - Format.fprintf fmt "\t%a = %a;\n%a" - (pp_varlist Base) patt - (pp_expression node_name) expr - (pp_equations node_name) eqs -(* By prepending to the `Format.formatter` `fmt` we could just declare these arrays once with a size of the maximum `reset_expressions_counter` *) -let pp_resvars reset_expressions_counter = - (* use the fact that any boolean and any integer can be encoded as a float, concerning integers [-2^(23+1) + 1; 2^(23+1) + 1] are correctly encoded (cf https://stackoverflow.com/a/53254438) *) - Format.sprintf "float tmp_reset[%i], init[%i];" reset_expressions_counter reset_expressions_counter -let pp_return node_name fmt outputs = - if node_name = "main" then - (Format.fprintf fmt "return %a;" - (pp_varlist Base) outputs) - else - Format.fprintf fmt "%s" (String.concat "\n\t" (List.map (fun output -> match output with | BVar name | IVar name | RVar name -> "output_" ^ node_name ^ "_" ^ name ^ " = " ^ name ^ ";") (snd outputs))) - -let pp_node fmt node = - (* undefined behavior if the initial code uses a variable with name: - - `init_{NODE_NAME}` - - `tmp_reset_{int}` - - `init_{int}` - - `pre_{NODE_NAME}_{VARIABLE}` - - `output_{NODE_NAME}_{VARIABLE}` *) - reset_expressions_counter := 0; - let _ = (pp_equations node.n_name) Format.str_formatter node.n_equations in - reset_expressions_counter := 0; - Format.fprintf fmt "bool init_%s = true;\n\n%a\n\n%a\n\n%a\n\n%s\n\n%s %s(%a)\n{\n\t%a\n\n\t%a\n\n%a\n\n\tinit_%s = false;\n\n%a\n\n%a\n\n%a\n\n\t%a\n}\n" - node.n_name - (* could avoid declaring unused variables *) - (pp_prevarlist node.n_name) node.n_inputs - (pp_prevarlist node.n_name) node.n_local_vars - (pp_prevarlist node.n_name) node.n_outputs - (pp_resvars !reset_expressions_counter) - (if node.n_name = "main" then "int" else "void") - node.n_name - (* could avoid newlines if they aren't used to seperate statements *) - (pp_varlist Arg) node.n_inputs - (pp_varlist Dec) node.n_local_vars - (pp_varlist Dec) node.n_outputs - (pp_equations node.n_name) node.n_equations - node.n_name - (pp_asnprevarlist node.n_name) node.n_inputs - (pp_asnprevarlist node.n_name) node.n_local_vars - (pp_asnprevarlist node.n_name) node.n_outputs - (pp_return node.n_name) node.n_outputs - -let rec pp_nodes fmt nodes = - match nodes with - | [] -> () - | node :: nodes -> - Format.fprintf fmt "%a\n%a" pp_node node pp_nodes nodes - -let rec load_outputs_from_vars node_name n_outputs = - match n_outputs with - | [] -> () - | BVar n_output :: n_outputs - | IVar n_output :: n_outputs - | RVar n_output :: n_outputs -> - (if (not (List.mem n_output !outputs)) then outputs := (node_name ^ "_" ^ n_output) :: !outputs;); load_outputs_from_vars node_name n_outputs - -let rec load_outputs_from_nodes nodes = - match nodes with - | [] -> () - | node :: nodes -> - (if node.n_name <> "main" then (load_outputs_from_vars node.n_name (snd node.n_outputs)); Hashtbl.add nodes_outputs node.n_name (snd node.n_outputs)); load_outputs_from_nodes nodes - -let ast_to_c fmt prog = - load_outputs_from_nodes prog; - Format.fprintf fmt - (* could verify that uses, possibly indirectly (cf `->` implementation), a boolean in the ast before including `` *) - "#include \n\n%s\n\n%a" - ("float " ^ (String.concat ", " (List.map (fun output -> "output_" ^ output) !outputs)) ^ ";") pp_nodes prog +let ast_to_c prog = + let prog_st_types = make_state_types prog in + Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a" + Config.c_includes + cp_state_types prog_st_types + cp_prototypes (prog, prog_st_types) diff --git a/src/c_utils.ml b/src/c_utils.ml new file mode 100644 index 0000000..fe33c09 --- /dev/null +++ b/src/c_utils.ml @@ -0,0 +1,34 @@ +open Ast + +(** A node state is translated into a struct. This struct has: + * 1. A name (t_state_) + * 2. A number of local and output variables of each type (int, real, bool) + * 3-5. mappings that maps + * [(variable, is_pre)] to an index of the corresponding array (see below) + * where [variable] is of type [t_var], and [is_pre] indicated whether we + * deal with pre (x) or x. + * 6. A mapping mapping the output number i to its location (name of the + * table that contains it and index. + * + * Important Note: if a variable x appears behind a pre, it will count as two + * variables in the point 2. above.. + * + * It should be translated as follow in C: + typedef struct { + int ivars[nt_nb_int]; (or nothing if nt_nb_int = 0) + int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0) + int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0) + } t_state_; + *) +type node_state = + { + nt_name: string; + nt_nb_int : int; + nt_nb_real: int; + nt_nb_bool: int; + nt_map_int: (t_var * bool, int) Hashtbl.t; + nt_map_bool: (t_var * bool, int) Hashtbl.t; + nt_map_real: (t_var * bool, int) Hashtbl.t; + nt_output_map: (int, string * int) Hashtbl.t; + } + diff --git a/src/config.ml b/src/config.ml index 3255356..7761b61 100644 --- a/src/config.ml +++ b/src/config.ml @@ -3,3 +3,4 @@ * variables. *) let maxvar = 100 +let c_includes = "#include " diff --git a/src/cprint.ml b/src/cprint.ml new file mode 100644 index 0000000..3881257 --- /dev/null +++ b/src/cprint.ml @@ -0,0 +1,57 @@ +open C_utils +open Ast + +let cp_node_state fmt (st: node_state) = + let maybeprint fmt (ty, nb, name): unit = + if nb = 0 + then () + else Format.fprintf fmt "\n\t%s %s[%d]" ty name nb + in + Format.fprintf fmt "typedef struct {%a%a%a\n} %s;\n\n" + maybeprint ("int", st.nt_nb_int, "ivars") + maybeprint ("bool", st.nt_nb_bool, "bvars") + maybeprint ("double", st.nt_nb_real, "rvars") + st.nt_name + +let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = + Hashtbl.iter (fun n nst -> + Format.fprintf fmt "/* Struct holding states of the node %s: */\n%a" n + cp_node_state nst) h + +let cp_var fmt = function + | IVar s -> Format.fprintf fmt "int %s" s + | BVar s -> Format.fprintf fmt "bool %s" s + | RVar s -> Format.fprintf fmt "double %s" s + +let rec cp_varlist fmt vl = + let maybeprint fmt = function + | [] -> () + | _ :: _ -> Format.fprintf fmt ", " + in + match vl with + | [] -> () + | v :: vl -> + Format.fprintf fmt "%a%a%a" + cp_var v + maybeprint vl + cp_varlist vl + +let cp_prototype fmt (node, h): unit = + match Hashtbl.find_opt h node.n_name with + | None -> failwith "This should not happend!" + | Some nst -> + begin + Format.fprintf fmt "void %s (%s *state, %a);\n" + node.n_name + nst.nt_name + cp_varlist (snd node.n_inputs) + end + +let rec cp_prototypes fmt (nodes, h) = + match nodes with + | [] -> Format.fprintf fmt "\n\n" + | node :: nodes -> + Format.fprintf fmt "%a%a" + cp_prototype (node, h) + cp_prototypes (nodes, h) + diff --git a/src/main.ml b/src/main.ml index e4e38b8..7acfc16 100644 --- a/src/main.ml +++ b/src/main.ml @@ -133,7 +133,7 @@ let _ = else ( if !nopopt then (fun _ -> ()) - else Format.printf "%a" Ast_to_c.ast_to_c) + else Ast_to_c.ast_to_c) end end diff --git a/src/passes.ml b/src/passes.ml index 02b1501..179242f 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -601,8 +601,8 @@ let clock_unification_pass verbose debug main_fn ast = | _ -> failure ("Merge format") end | ETriOp(_, TOp_if, e1, e2, e3) -> - let c1 = compute_clock_exp e1 - and c2 = compute_clock_exp e2 + let (* Unused: c1 = compute_clock_exp e1 + and*) c2 = compute_clock_exp e2 and c3 = compute_clock_exp e3 in if c2 <> c3 then failure "If clocks" diff --git a/src/utils.ml b/src/utils.ml index ae46399..01312ef 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -9,6 +9,13 @@ let rec list_select n = function let p1, p2 = list_select (n-1) t in h :: p1, p2 +let rec list_remove_duplicates l = + match l with + | [] -> [] + | h :: t -> + let t = list_remove_duplicates t in + if List.mem h t then t else h :: t + 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 From bb99a5882b4fd9f1499d47eedb53f691829e19d1 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 16:30:10 +0100 Subject: [PATCH 02/50] [ast2C] store old values of variables used in the pre construct --- src/ast_to_c.ml | 16 +++++++++++++++- src/c_utils.ml | 6 +++++- src/cprint.ml | 30 +++++++++++++++++++++++++++--- 3 files changed, 47 insertions(+), 5 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 014007e..4bfdd9b 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -71,6 +71,17 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = let nb_int_vars, h_int = one_node node pv TInt in let nb_bool_vars, h_bool = one_node node pv TBool in let nb_real_vars, h_real = one_node node pv TReal in + + (** h_map gathers information from h_* maps above *) + let h_map = + Hashtbl.create (nb_int_vars + nb_bool_vars + nb_real_vars) in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("ivars", v)) h_int in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("bvars", v)) h_bool in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("rvars", v)) h_real in + let node_out_vars = snd node.n_outputs in let h_out = Hashtbl.create (List.length node_out_vars) in let () = List.iteri @@ -95,7 +106,9 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = nt_map_int = h_int; nt_map_bool = h_bool; nt_map_real = h_real; + nt_map = h_map; nt_output_map = h_out; + nt_prevars = pv; } in h end @@ -110,8 +123,9 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = let ast_to_c prog = let prog_st_types = make_state_types prog in - Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a" + Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" Config.c_includes cp_state_types prog_st_types cp_prototypes (prog, prog_st_types) + cp_nodes (prog, prog_st_types) diff --git a/src/c_utils.ml b/src/c_utils.ml index fe33c09..83a354a 100644 --- a/src/c_utils.ml +++ b/src/c_utils.ml @@ -7,7 +7,9 @@ open Ast * [(variable, is_pre)] to an index of the corresponding array (see below) * where [variable] is of type [t_var], and [is_pre] indicated whether we * deal with pre (x) or x. - * 6. A mapping mapping the output number i to its location (name of the + * 6. A mapping mapping any variable to the name of the C table containing it + * and the index at which it is stored (= union of the tables [nt_map_*]) + * 7. A mapping mapping the output number i to its location (name of the * table that contains it and index. * * Important Note: if a variable x appears behind a pre, it will count as two @@ -29,6 +31,8 @@ type node_state = nt_map_int: (t_var * bool, int) Hashtbl.t; nt_map_bool: (t_var * bool, int) Hashtbl.t; nt_map_real: (t_var * bool, int) Hashtbl.t; + nt_map: (t_var * bool, string * int) Hashtbl.t; nt_output_map: (int, string * int) Hashtbl.t; + nt_prevars: t_var list } diff --git a/src/cprint.ml b/src/cprint.ml index 3881257..ab2db08 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -41,7 +41,7 @@ let cp_prototype fmt (node, h): unit = | None -> failwith "This should not happend!" | Some nst -> begin - Format.fprintf fmt "void %s (%s *state, %a);\n" + Format.fprintf fmt "void %s (%s *state, %a)" node.n_name nst.nt_name cp_varlist (snd node.n_inputs) @@ -49,9 +49,33 @@ let cp_prototype fmt (node, h): unit = let rec cp_prototypes fmt (nodes, h) = match nodes with - | [] -> Format.fprintf fmt "\n\n" + | [] -> () | node :: nodes -> - Format.fprintf fmt "%a%a" + Format.fprintf fmt "%a;\n%a" cp_prototype (node, h) cp_prototypes (nodes, h) +(** The ollowing function prints the code to remember previous values of + * variables used with the pre construct. *) +let cp_prevars fmt (node, h) = + let node_st = Hashtbl.find h node.n_name in + List.iter + (fun v -> (** Note that «dst_array = src_array» should hold. *) + let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx) + node_st.nt_prevars + +let rec cp_node fmt (node, h) = + Format.fprintf fmt "%a\n{\nTODO...\n%a}\n" + cp_prototype (node, h) + cp_prevars (node, h) + +let rec cp_nodes fmt (nodes, h) = + match nodes with + | [] -> () + | node :: nodes -> + Format.fprintf fmt "%a\n%a" + cp_node (node, h) + cp_nodes (nodes, h) From 6291957be5b3044d1112a7284e059f30032ad178 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 16:35:49 +0100 Subject: [PATCH 03/50] [ast2C] init or not init (field added to the state of the node) --- src/c_utils.ml | 1 + src/cprint.ml | 8 +++++--- src/test2.node | 8 -------- 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/c_utils.ml b/src/c_utils.ml index 83a354a..26ba5e1 100644 --- a/src/c_utils.ml +++ b/src/c_utils.ml @@ -20,6 +20,7 @@ open Ast int ivars[nt_nb_int]; (or nothing if nt_nb_int = 0) int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0) int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0) + bool is_init; } t_state_; *) type node_state = diff --git a/src/cprint.ml b/src/cprint.ml index ab2db08..bbfc952 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -5,9 +5,9 @@ let cp_node_state fmt (st: node_state) = let maybeprint fmt (ty, nb, name): unit = if nb = 0 then () - else Format.fprintf fmt "\n\t%s %s[%d]" ty name nb + else Format.fprintf fmt "\n\t%s %s[%d];" ty name nb in - Format.fprintf fmt "typedef struct {%a%a%a\n} %s;\n\n" + Format.fprintf fmt "typedef struct {%a%a%a\n\tbool is_init;\n} %s;\n\n" maybeprint ("int", st.nt_nb_int, "ivars") maybeprint ("bool", st.nt_nb_bool, "bvars") maybeprint ("double", st.nt_nb_real, "rvars") @@ -58,6 +58,8 @@ let rec cp_prototypes fmt (nodes, h) = (** The ollowing function prints the code to remember previous values of * variables used with the pre construct. *) let cp_prevars fmt (node, h) = + Format.fprintf fmt + "\n\t/* Remember the values of variables used in the [pre] construct */\n"; let node_st = Hashtbl.find h node.n_name in List.iter (fun v -> (** Note that «dst_array = src_array» should hold. *) @@ -68,7 +70,7 @@ let cp_prevars fmt (node, h) = node_st.nt_prevars let rec cp_node fmt (node, h) = - Format.fprintf fmt "%a\n{\nTODO...\n%a}\n" + Format.fprintf fmt "%a\n{\n\t\tTODO...\n\n\tstate->is_init = false;\n%a}\n" cp_prototype (node, h) cp_prevars (node, h) diff --git a/src/test2.node b/src/test2.node index 3598f37..2c60962 100644 --- a/src/test2.node +++ b/src/test2.node @@ -3,11 +3,3 @@ let o1 = 10 -> pre (20 -> 30); tel -node flipflop(i: int) returns (z: int); -var x, y: int; c: bool; -let - c = true fby (not c); - x = 1 on c; - y = 2 on (not c); - z = merge c x y; -tel From 916c7f544b5cd3433986ab9afdd5908e0cb95a69 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 18:34:11 +0100 Subject: [PATCH 04/50] [ast2C] initialize states of auxiliary nodes. --- src/ast_to_c.ml | 145 +++++++++++++++++++++++++++++++++++++++++++++--- src/c_utils.ml | 79 +++++++++++++------------- src/cast.ml | 78 ++++++++++++++++++++++++++ src/config.ml | 2 +- src/cprint.ml | 67 +++++++++++----------- src/test2.node | 10 +++- 6 files changed, 297 insertions(+), 84 deletions(-) create mode 100644 src/cast.ml diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 4bfdd9b..0789b76 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -1,20 +1,72 @@ open Ast +open Cast open C_utils open Cprint open Utils +(** [ast_to_cast] translates a [t_nodelist] into a [c_nodelist] *) +let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = + let c = ref 1 in + let ast_to_cast_varlist vl = snd vl in + let rec ast_to_cast_expr hloc = function + | EVar (_, v) -> + begin + match Hashtbl.find_opt hloc (v, false) with + | None -> CVar (CVInput (name_of_var v)) + | Some (s, i) -> CVar (CVStored (s, i)) + end + | EMonOp (_, op, e) -> CMonOp (op, ast_to_cast_expr hloc e) + | EBinOp (_, op, e, e') -> + CBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | ETriOp (_, op, e, e', e'') -> + CTriOp + (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'') + | EComp (_, op, e, e') -> + CComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | EWhen (_, e, e') -> + CWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | EReset (_, e, e') -> + CReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | EConst (_, c) -> CConst c + | ETuple (_, l) -> CTuple (List.map (ast_to_cast_expr hloc) l) + | EApp (_, n, e) -> + begin + let e = ast_to_cast_expr hloc e in + let res = CApp (!c, n, e) in + let () = incr c in + res + end + in + let ast_to_cast_eq hloc (patt, expr) : c_equation = + (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in + List.map + begin + fun node -> + let () = c := 1 in + let hloc = (Hashtbl.find h node.n_name).nt_map in + { + cn_name = node.n_name; + cn_inputs = ast_to_cast_varlist node.n_inputs; + cn_outputs = ast_to_cast_varlist node.n_outputs; + cn_local_vars = ast_to_cast_varlist node.n_local_vars; + cn_equations = List.map (ast_to_cast_eq hloc) node.n_equations; + } + end + nodes + + (** The following function defines the [node_states] for the nodes of a program, * and puts them in a hash table. *) -let make_state_types nodes: (ident, node_state) Hashtbl.t = +let make_state_types nodes: node_states = (* Hash table to fill *) let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in (** [one_node node pv ty] computes the number of variables of type [ty] in * [node] and a mapping from the variables of type ([ty] * bool) to int, * where [pv] is a list of variables used in the pre construct in the - * programm. *) + * program. *) let one_node node pv ty = (* variables of type [ty] among output and local variables *) let vars = @@ -35,8 +87,8 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = (** [find_prevars n] returns the list of variables appearing after a pre in * the node [n]. - * Note that the only occurence of pre are of the form pre (var), due to the - * linearization pass. + * Note that the only occurrence of pre are of the form pre (var), due to + * the linearization pass. *) let find_prevars node = let rec find_prevars_expr = function @@ -58,6 +110,26 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = [] node.n_equations) in + (** [count_app n] count the number of auxiliary nodes calls in [n] *) + let count_app n = + let rec count_app_expr = function + | EConst _ | EVar _ -> 0 + | EMonOp (_, _, e) -> count_app_expr e + | ETriOp (_, _, e, e', e'') -> + (count_app_expr e) + (count_app_expr e') + (count_app_expr e'') + | EComp (_, _, e, e') + | EBinOp (_, _, e, e') + | EWhen (_, e, e') + | EReset (_, e, e') -> (count_app_expr e) + (count_app_expr e') + | ETuple (_, l) -> + List.fold_left (fun acc e -> acc + count_app_expr e) 0 l + | EApp (_, _, e) -> 1 + count_app_expr e + in + List.fold_left + (fun i (_, expr) -> i + count_app_expr expr) + 0 n.n_equations + in + (** [aux] iterates over all nodes of the program to build the required hash * table *) let rec aux nodes = @@ -109,6 +181,7 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = nt_map = h_map; nt_output_map = h_out; nt_prevars = pv; + nt_count_app = count_app node; } in h end @@ -117,14 +190,72 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = -(*let ast_to_c*) +(** The following C-printer functions are in this file, as they need to work on + * the AST and are not simple printers. *) + + + +(** The following function prints the code to remember previous values of + * variables used with the pre construct. *) +let cp_prevars fmt (node, h) = + Format.fprintf fmt + "\n\t/* Remember the values of variables used in the [pre] construct */\n"; + let node_st = Hashtbl.find h node.cn_name in + List.iter + (fun v -> (** Note that «dst_array = src_array» should hold. *) + let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx) + node_st.nt_prevars + +(** The following function defines the behaviour to have at the first + * execution of a node, namely: + * - initialize the states of auxiliary nodes + * *) +let cp_init_aux_nodes fmt (node, h) = + let rec aux fmt (node, nst, i) = + match find_app_opt node.cn_equations i with + | None -> () (** All auxiliary nodes have been initialized *) + | Some n -> + begin + Format.fprintf fmt "%a\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ + \t\t(%s*)(state->aux_states[%d])->is_init = true;\n" + aux (node, nst, i-1) + (i-1) (Format.asprintf "t_state_%s" n.n_name) + (Format.asprintf "t_state_%s" n.n_name) (i-1) + end + in + let nst = Hashtbl.find h node.cn_name in + if nst.nt_count_app = 0 + then () + else begin + Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\ + \tif (state->is_init) {\n%a\t}\n" + aux (node, nst, nst.nt_count_app) + end + +let rec cp_node fmt (node, h) = + Format.fprintf fmt "%a\n{\n%a\t\tTODO...\n\n\tstate->is_init = false;\n%a}\n" + cp_prototype (node, h) + cp_init_aux_nodes (node, h) + cp_prevars (node, h) + +let rec cp_nodes fmt (nodes, h) = + match nodes with + | [] -> () + | node :: nodes -> + Format.fprintf fmt "%a\n%a" + cp_node (node, h) + cp_nodes (nodes, h) let ast_to_c prog = let prog_st_types = make_state_types prog in - Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" - Config.c_includes + let prog: c_nodelist = ast_to_cast prog prog_st_types in + Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" + cp_includes (Config.c_includes) cp_state_types prog_st_types cp_prototypes (prog, prog_st_types) cp_nodes (prog, prog_st_types) diff --git a/src/c_utils.ml b/src/c_utils.ml index 26ba5e1..717b4a5 100644 --- a/src/c_utils.ml +++ b/src/c_utils.ml @@ -1,39 +1,42 @@ -open Ast - -(** A node state is translated into a struct. This struct has: - * 1. A name (t_state_) - * 2. A number of local and output variables of each type (int, real, bool) - * 3-5. mappings that maps - * [(variable, is_pre)] to an index of the corresponding array (see below) - * where [variable] is of type [t_var], and [is_pre] indicated whether we - * deal with pre (x) or x. - * 6. A mapping mapping any variable to the name of the C table containing it - * and the index at which it is stored (= union of the tables [nt_map_*]) - * 7. A mapping mapping the output number i to its location (name of the - * table that contains it and index. - * - * Important Note: if a variable x appears behind a pre, it will count as two - * variables in the point 2. above.. - * - * It should be translated as follow in C: - typedef struct { - int ivars[nt_nb_int]; (or nothing if nt_nb_int = 0) - int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0) - int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0) - bool is_init; - } t_state_; - *) -type node_state = - { - nt_name: string; - nt_nb_int : int; - nt_nb_real: int; - nt_nb_bool: int; - nt_map_int: (t_var * bool, int) Hashtbl.t; - nt_map_bool: (t_var * bool, int) Hashtbl.t; - nt_map_real: (t_var * bool, int) Hashtbl.t; - nt_map: (t_var * bool, string * int) Hashtbl.t; - nt_output_map: (int, string * int) Hashtbl.t; - nt_prevars: t_var list - } +open Cast +let rec find_app_opt eqs i = + let rec find_app_expr_opt i = function + | CVar _ | CConst _ -> None + | CMonOp (_, e) -> find_app_expr_opt i e + | CReset (e, e') | CWhen (e, e') | CComp (_, e, e') | CBinOp (_, e, e') -> + begin + match find_app_expr_opt i e with + | None -> find_app_expr_opt i e' + | Some n -> Some n + end + | CTriOp (_, e, e', e'') -> + begin + match find_app_expr_opt i e with + | None -> + begin + match find_app_expr_opt i e' with + | None -> find_app_expr_opt i e'' + | Some n -> Some n + end + | Some n -> Some n + end + | CTuple l -> + List.fold_left + (fun acc e -> + match acc, find_app_expr_opt i e with + | Some n, _ -> Some n + | None, v -> v) + None l + (** [CApp] below represents the n-th call to an aux node *) + | CApp (j, n, e) -> + if i = j + then Some n + else find_app_expr_opt i e + in + match eqs with + | [] -> None + | (_, expr) :: eqs -> + match find_app_expr_opt i expr with + | None -> find_app_opt eqs i + | Some n -> Some n diff --git a/src/cast.ml b/src/cast.ml new file mode 100644 index 0000000..31a4dc7 --- /dev/null +++ b/src/cast.ml @@ -0,0 +1,78 @@ +open Ast + +(** A node state is translated into a struct. This struct has: + * 1. A name (t_state_) + * 2. A number of local and output variables of each type (int, real, bool) + * 3-5. mappings that maps + * [(variable, is_pre)] to an index of the corresponding array (see below) + * where [variable] is of type [t_var], and [is_pre] indicated whether we + * deal with pre (x) or x. + * 6. A mapping mapping any variable to the name of the C table containing it + * and the index at which it is stored (= union of the tables [nt_map_*]) + * 7. A mapping mapping the output number i to its location (name of the + * table that contains it and index. + * + * Important Note: if a variable x appears behind a pre, it will count as two + * variables in the point 2. above.. + * + * It should be translated as follow in C: + typedef struct { + int ivars[nt_nb_int]; (or nothing if nt_nb_int = 0) + int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0) + int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0) + bool is_init; + } t_state_; + *) +type node_state = + { + nt_name: string; + nt_nb_int : int; + nt_nb_real: int; + nt_nb_bool: int; + nt_map_int: (t_var * bool, int) Hashtbl.t; + nt_map_bool: (t_var * bool, int) Hashtbl.t; + nt_map_real: (t_var * bool, int) Hashtbl.t; + nt_map: (t_var * bool, string * int) Hashtbl.t; + nt_output_map: (int, string * int) Hashtbl.t; + nt_prevars: t_var list; + nt_count_app: int; + } + + + +type c_var = + | CVStored of string * int + | CVInput of ident + +type c_expression = + | CVar of c_var + | CMonOp of monop * c_expression + | CBinOp of binop * c_expression * c_expression + | CTriOp of triop * c_expression * c_expression * c_expression + | CComp of compop * c_expression * c_expression + | CWhen of c_expression * c_expression + | CReset of c_expression * c_expression + | CConst of const + | CTuple of (c_expression list) + (** [CApp] below represents the n-th call to an aux node *) + | CApp of int * t_node * c_expression + +and c_varlist = t_var list + +and c_equation = c_varlist * c_expression + +and c_eqlist = c_equation list + +and c_node = + { + cn_name : ident; + cn_inputs: c_varlist; + cn_outputs: c_varlist; + cn_local_vars: c_varlist; + cn_equations: c_eqlist; + } + +type c_nodelist = c_node list + +type node_states = (ident, node_state) Hashtbl.t + diff --git a/src/config.ml b/src/config.ml index 7761b61..1ad7133 100644 --- a/src/config.ml +++ b/src/config.ml @@ -3,4 +3,4 @@ * variables. *) let maxvar = 100 -let c_includes = "#include " +let c_includes = ["stdbool"; "stdlib"] diff --git a/src/cprint.ml b/src/cprint.ml index bbfc952..a64e8fa 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -1,17 +1,38 @@ open C_utils +open Cast open Ast +(** This file contains extrimely simple functions printing C code. *) + +let rec cp_includes fmt = function + | [] -> () + | h :: t -> + Format.fprintf fmt "#include <%s>\n%a" h cp_includes t + let cp_node_state fmt (st: node_state) = let maybeprint fmt (ty, nb, name): unit = if nb = 0 then () else Format.fprintf fmt "\n\t%s %s[%d];" ty name nb in - Format.fprintf fmt "typedef struct {%a%a%a\n\tbool is_init;\n} %s;\n\n" - maybeprint ("int", st.nt_nb_int, "ivars") - maybeprint ("bool", st.nt_nb_bool, "bvars") - maybeprint ("double", st.nt_nb_real, "rvars") - st.nt_name + if st.nt_count_app = 0 + then + Format.fprintf fmt "typedef struct {%a%a%a\n\ + \tbool is_init;\n\ + } %s;\n\n" + maybeprint ("int", st.nt_nb_int, "ivars") + maybeprint ("bool", st.nt_nb_bool, "bvars") + maybeprint ("double", st.nt_nb_real, "rvars") + st.nt_name + else + Format.fprintf fmt "typedef struct {%a%a%a\n\ + \tbool is_init;\n\ + \tvoid* aux_states[%d]; /* stores the states of auxiliary nodes */\n\ + } %s;\n\n" + maybeprint ("int", st.nt_nb_int, "ivars") + maybeprint ("bool", st.nt_nb_bool, "bvars") + maybeprint ("double", st.nt_nb_real, "rvars") + st.nt_count_app st.nt_name let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = Hashtbl.iter (fun n nst -> @@ -37,17 +58,17 @@ let rec cp_varlist fmt vl = cp_varlist vl let cp_prototype fmt (node, h): unit = - match Hashtbl.find_opt h node.n_name with + match Hashtbl.find_opt h node.cn_name with | None -> failwith "This should not happend!" | Some nst -> begin - Format.fprintf fmt "void %s (%s *state, %a)" - node.n_name + Format.fprintf fmt "void fn_%s (%s *state, %a)" + node.cn_name nst.nt_name - cp_varlist (snd node.n_inputs) + cp_varlist node.cn_inputs end -let rec cp_prototypes fmt (nodes, h) = +let rec cp_prototypes fmt ((nodes, h): c_nodelist * node_states) = match nodes with | [] -> () | node :: nodes -> @@ -55,29 +76,3 @@ let rec cp_prototypes fmt (nodes, h) = cp_prototype (node, h) cp_prototypes (nodes, h) -(** The ollowing function prints the code to remember previous values of - * variables used with the pre construct. *) -let cp_prevars fmt (node, h) = - Format.fprintf fmt - "\n\t/* Remember the values of variables used in the [pre] construct */\n"; - let node_st = Hashtbl.find h node.n_name in - List.iter - (fun v -> (** Note that «dst_array = src_array» should hold. *) - let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in - let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s[%d];\n" - dst_array dst_idx src_array src_idx) - node_st.nt_prevars - -let rec cp_node fmt (node, h) = - Format.fprintf fmt "%a\n{\n\t\tTODO...\n\n\tstate->is_init = false;\n%a}\n" - cp_prototype (node, h) - cp_prevars (node, h) - -let rec cp_nodes fmt (nodes, h) = - match nodes with - | [] -> () - | node :: nodes -> - Format.fprintf fmt "%a\n%a" - cp_node (node, h) - cp_nodes (nodes, h) diff --git a/src/test2.node b/src/test2.node index 2c60962..2a4f0b3 100644 --- a/src/test2.node +++ b/src/test2.node @@ -1,5 +1,11 @@ -node main (i: int) returns (o1: int); +node diagonal_int (i: int) returns (o1, o2 : int); let - o1 = 10 -> pre (20 -> 30); + (o1, o2) = (i, i); +tel + +node main (i: int) returns (o1, o2, o3, o4: int); +let + (o1, o2) = diagonal_int(i); + (o3, o4) = diagonal_int(o1); tel From 3cbfaeb2a8acb449cf72cef82bc11b707cd7d790 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 21:26:32 +0100 Subject: [PATCH 05/50] [general] renaming (pp -> lustre_pp ; c_* -> intermediate_*) --- src/ast_to_c.ml | 58 ++++++++++---- src/cprint.ml | 4 +- src/{cast.ml => intermediate_ast.ml} | 0 src/{c_utils.ml => intermediate_utils.ml} | 2 +- src/{pp.ml => lustre_pp.ml} | 0 src/main.ml | 31 +++----- src/simulation.ml | 92 ----------------------- {src => tests}/test.node | 0 {src => tests}/test2.node | 0 {src => tests}/test_pre.node | 0 10 files changed, 57 insertions(+), 130 deletions(-) rename src/{cast.ml => intermediate_ast.ml} (100%) rename src/{c_utils.ml => intermediate_utils.ml} (98%) rename src/{pp.ml => lustre_pp.ml} (100%) delete mode 100644 src/simulation.ml rename {src => tests}/test.node (100%) rename {src => tests}/test2.node (100%) rename {src => tests}/test_pre.node (100%) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 0789b76..f98ffa3 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -1,6 +1,6 @@ open Ast -open Cast -open C_utils +open Intermediate_ast +open Intermediate_utils open Cprint open Utils @@ -56,7 +56,6 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = end nodes - (** The following function defines the [node_states] for the nodes of a program, * and puts them in a hash table. *) let make_state_types nodes: node_states = @@ -198,21 +197,26 @@ let make_state_types nodes: node_states = (** The following function prints the code to remember previous values of * variables used with the pre construct. *) let cp_prevars fmt (node, h) = - Format.fprintf fmt - "\n\t/* Remember the values of variables used in the [pre] construct */\n"; let node_st = Hashtbl.find h node.cn_name in - List.iter - (fun v -> (** Note that «dst_array = src_array» should hold. *) - let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in - let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s[%d];\n" - dst_array dst_idx src_array src_idx) - node_st.nt_prevars + match (Hashtbl.find h node.cn_name).nt_prevars with + | [] -> () + | l -> + Format.fprintf fmt + "\n\t/* Remember the values used in the [pre] construct */\n"; + List.iter + (fun v -> (** Note that «dst_array = src_array» should hold. *) + let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx) + l + + (** The following function defines the behaviour to have at the first * execution of a node, namely: * - initialize the states of auxiliary nodes - * *) + *) let cp_init_aux_nodes fmt (node, h) = let rec aux fmt (node, nst, i) = match find_app_opt node.cn_equations i with @@ -220,7 +224,7 @@ let cp_init_aux_nodes fmt (node, h) = | Some n -> begin Format.fprintf fmt "%a\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ - \t\t(%s*)(state->aux_states[%d])->is_init = true;\n" + \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n" aux (node, nst, i-1) (i-1) (Format.asprintf "t_state_%s" n.n_name) (Format.asprintf "t_state_%s" n.n_name) (i-1) @@ -235,12 +239,33 @@ let cp_init_aux_nodes fmt (node, h) = aux (node, nst, nst.nt_count_app) end -let rec cp_node fmt (node, h) = - Format.fprintf fmt "%a\n{\n%a\t\tTODO...\n\n\tstate->is_init = false;\n%a}\n" + + +(** The following function prints one equation of the program into a set of + * instruction ending in assignments. *) +let cp_equation fmt (eq, hloc) = + Format.fprintf fmt "\t\t/* TODO! */\n" + + + +(** [cp_equations] prints the node equations. *) +let rec cp_equations fmt (eqs, hloc) = + match eqs with + | [] -> () + | eq :: eqs -> + Format.fprintf fmt "%a%a" + cp_equation (eq, hloc) + cp_equations (eqs, hloc) + +(** [cp_node] prints a single node *) +let cp_node fmt (node, h) = + Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n" cp_prototype (node, h) cp_init_aux_nodes (node, h) + cp_equations (node.cn_equations, Hashtbl.find h node.cn_name) cp_prevars (node, h) +(** [cp_nodes] recursively prints all the nodes of a program. *) let rec cp_nodes fmt (nodes, h) = match nodes with | [] -> () @@ -251,6 +276,7 @@ let rec cp_nodes fmt (nodes, h) = +(** main function that prints a C-code from a term of type [t_nodelist]. *) let ast_to_c prog = let prog_st_types = make_state_types prog in let prog: c_nodelist = ast_to_cast prog prog_st_types in diff --git a/src/cprint.ml b/src/cprint.ml index a64e8fa..5f191ae 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -1,5 +1,5 @@ -open C_utils -open Cast +open Intermediate_utils +open Intermediate_ast open Ast (** This file contains extrimely simple functions printing C code. *) diff --git a/src/cast.ml b/src/intermediate_ast.ml similarity index 100% rename from src/cast.ml rename to src/intermediate_ast.ml diff --git a/src/c_utils.ml b/src/intermediate_utils.ml similarity index 98% rename from src/c_utils.ml rename to src/intermediate_utils.ml index 717b4a5..c964e50 100644 --- a/src/c_utils.ml +++ b/src/intermediate_utils.ml @@ -1,4 +1,4 @@ -open Cast +open Intermediate_ast let rec find_app_opt eqs i = let rec find_app_expr_opt i = function diff --git a/src/pp.ml b/src/lustre_pp.ml similarity index 100% rename from src/pp.ml rename to src/lustre_pp.ml diff --git a/src/main.ml b/src/main.ml index 7acfc16..80c3678 100644 --- a/src/main.ml +++ b/src/main.ml @@ -17,7 +17,7 @@ let exec_passes ast main_fn verbose debug passes f = 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); + debug (Format.asprintf "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast); aux ast passes) in aux ast passes @@ -34,7 +34,6 @@ let _ = 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 source_file = ref "" in let testopt = ref false in @@ -51,7 +50,6 @@ 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"); ("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])"); ] in Arg.parse speclist anon_fun usage_msg ; @@ -93,7 +91,7 @@ let _ = begin close_in_noerr inchan; Format.printf "Syntax error at %a: %s\n\n" - Pp.pp_loc (l, !source_file) s; + Lustre_pp.pp_loc (l, !source_file) s; exit 0 end | Parsing.Parse_error -> @@ -101,7 +99,7 @@ let _ = close_in_noerr inchan; Parsing.( Format.printf "Syntax error at %a\n\n" - Pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file)); + Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file)); exit 0 end in @@ -121,19 +119,14 @@ let _ = in print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" - Pp.pp_ast ast) ; + Lustre_pp.pp_ast ast) ; exec_passes ast main_fn print_verbose print_debug passes - begin - if !simopt - then Simulation.simulate main_fn - else - begin - if !ppast - then (Format.printf "%a" Pp.pp_ast) - else ( - if !nopopt - then (fun _ -> ()) - else Ast_to_c.ast_to_c) - end - end + begin + if !ppast + then (Format.printf "%a" Lustre_pp.pp_ast) + else ( + if !nopopt + then (fun _ -> ()) + else Ast_to_c.ast_to_c) + end diff --git a/src/simulation.ml b/src/simulation.ml deleted file mode 100644 index e7ba3db..0000000 --- a/src/simulation.ml +++ /dev/null @@ -1,92 +0,0 @@ -open Ast - -type sim_var = - | SIVar of ident * (int option) - | SBVar of ident * (bool option) - | SRVar of ident * (real option) - -type sim_node_st = - { - node_outputs: sim_var list; - node_loc_vars: sim_var list; - node_inner_nodes: sim_node list; - } -and sim_node_step_fn = - sim_node_st -> sim_var list -> (sim_var list * sim_node_st) -and sim_node = sim_node_st * sim_node_step_fn - -let pp_sim fmt ((sn, _): sim_node) = - let rec aux fmt vars = - match vars with - | [] -> () - | SIVar (s, None) :: t -> - Format.fprintf fmt "\t<%s : int> uninitialized yet.\n%a" s aux t - | SBVar (s, None) :: t -> - Format.fprintf fmt "\t<%s : bool> uninitialized yet.\n%a" s aux t - | SRVar (s, None) :: t -> - Format.fprintf fmt "\t<%s : real> uninitialized yet.\n%a" s aux t - | SIVar (s, Some i) :: t -> - Format.fprintf fmt "\t<%s : int> = %d\n%a" s i aux t - | SBVar (s, Some b) :: t -> - Format.fprintf fmt "\t<%s : bool> = %s\n%a" s (Bool.to_string b) aux t - | SRVar (s, Some r) :: t -> - Format.fprintf fmt "\t<%s : real> = %f\n%a" s r aux t - in - if sn.node_loc_vars <> [] - then - Format.fprintf fmt "State of the simulated node:\n\ - \tOutput variables:\n%a - \tLocal variables:\n%a" - aux sn.node_outputs - aux sn.node_loc_vars - else - Format.fprintf fmt "State of the simulated node:\n\ - \tOutput variables:\n%a - \tThere are no local variables:\n" - aux sn.node_outputs - - -exception MySimulationException of string - -let fetch_node (p: t_nodelist) (s: ident) : t_node = - match List.filter (fun n -> n.n_name = s) p with - | [e] -> e - | _ -> raise (MySimulationException (Format.asprintf "Node %s undefined." s)) - -let fetch_var (l: sim_var list) (s: ident) = - match List.filter - (function - | SBVar (v, _) | SRVar (v, _) | SIVar (v, _) -> v = s) l with - | [v] -> v - | _ -> raise (MySimulationException - (Format.asprintf "Variable %s undefined." s)) - -(** TODO! *) -let make_sim (main_fn: ident) (p: t_nodelist): sim_node = - let main_n = fetch_node p main_fn in - let node_outputs = - List.map - (function - | IVar s -> SIVar (s, None) - | BVar s -> SBVar (s, None) - | RVar s -> SRVar (s, None)) - (snd main_n.n_outputs) in - let node_loc_vars: sim_var list = - List.map - (function - | IVar s -> SIVar (s, None) - | BVar s -> SBVar (s, None) - | RVar s -> SRVar (s, None)) - (snd main_n.n_local_vars) in - let node_inner_nodes = (* TODO! *) [] in - ({node_outputs = node_outputs; - node_loc_vars = node_loc_vars; - node_inner_nodes = node_inner_nodes; }, - (fun s l -> (s.node_outputs, s))) - - - -let simulate main_fn ast = - let sim_ast = make_sim main_fn ast in - Format.printf "Initial state:\n%a" pp_sim sim_ast - diff --git a/src/test.node b/tests/test.node similarity index 100% rename from src/test.node rename to tests/test.node diff --git a/src/test2.node b/tests/test2.node similarity index 100% rename from src/test2.node rename to tests/test2.node diff --git a/src/test_pre.node b/tests/test_pre.node similarity index 100% rename from src/test_pre.node rename to tests/test_pre.node From a877501cca02b853983e62400a6ccc2f55f0f3a3 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 21:37:37 +0100 Subject: [PATCH 06/50] [general] renaming: done. --- src/ast_to_c.ml | 52 +++++++++++++++++++-------------------- src/cprint.ml | 10 ++++---- src/intermediate_ast.ml | 42 +++++++++++++++---------------- src/intermediate_utils.ml | 14 +++++------ 4 files changed, 59 insertions(+), 59 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index f98ffa3..618cb11 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -6,40 +6,40 @@ open Utils -(** [ast_to_cast] translates a [t_nodelist] into a [c_nodelist] *) -let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = +(** [ast_to_cast] translates a [t_nodelist] into a [i_nodelist] *) +let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = let c = ref 1 in let ast_to_cast_varlist vl = snd vl in let rec ast_to_cast_expr hloc = function | EVar (_, v) -> begin match Hashtbl.find_opt hloc (v, false) with - | None -> CVar (CVInput (name_of_var v)) - | Some (s, i) -> CVar (CVStored (s, i)) + | None -> IVar (CVInput (name_of_var v)) + | Some (s, i) -> IVar (CVStored (s, i)) end - | EMonOp (_, op, e) -> CMonOp (op, ast_to_cast_expr hloc e) + | EMonOp (_, op, e) -> IMonOp (op, ast_to_cast_expr hloc e) | EBinOp (_, op, e, e') -> - CBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | ETriOp (_, op, e, e', e'') -> - CTriOp + ITriOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'') | EComp (_, op, e, e') -> - CComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | EWhen (_, e, e') -> - CWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | EReset (_, e, e') -> - CReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') - | EConst (_, c) -> CConst c - | ETuple (_, l) -> CTuple (List.map (ast_to_cast_expr hloc) l) + IReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | EConst (_, c) -> IConst c + | ETuple (_, l) -> ITuple (List.map (ast_to_cast_expr hloc) l) | EApp (_, n, e) -> begin let e = ast_to_cast_expr hloc e in - let res = CApp (!c, n, e) in + let res = IApp (!c, n, e) in let () = incr c in res end in - let ast_to_cast_eq hloc (patt, expr) : c_equation = + let ast_to_cast_eq hloc (patt, expr) : i_equation = (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in List.map begin @@ -47,11 +47,11 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = let () = c := 1 in let hloc = (Hashtbl.find h node.n_name).nt_map in { - cn_name = node.n_name; - cn_inputs = ast_to_cast_varlist node.n_inputs; - cn_outputs = ast_to_cast_varlist node.n_outputs; - cn_local_vars = ast_to_cast_varlist node.n_local_vars; - cn_equations = List.map (ast_to_cast_eq hloc) node.n_equations; + in_name = node.n_name; + in_inputs = ast_to_cast_varlist node.n_inputs; + in_outputs = ast_to_cast_varlist node.n_outputs; + in_local_vars = ast_to_cast_varlist node.n_local_vars; + in_equations = List.map (ast_to_cast_eq hloc) node.n_equations; } end nodes @@ -156,7 +156,7 @@ let make_state_types nodes: node_states = let node_out_vars = snd node.n_outputs in let h_out = Hashtbl.create (List.length node_out_vars) in let () = List.iteri - (fun n v -> + (fun n (v: t_var) -> match v with | IVar _ -> let i = Hashtbl.find h_int (v, false) in @@ -197,8 +197,8 @@ let make_state_types nodes: node_states = (** The following function prints the code to remember previous values of * variables used with the pre construct. *) let cp_prevars fmt (node, h) = - let node_st = Hashtbl.find h node.cn_name in - match (Hashtbl.find h node.cn_name).nt_prevars with + let node_st = Hashtbl.find h node.in_name in + match (Hashtbl.find h node.in_name).nt_prevars with | [] -> () | l -> Format.fprintf fmt @@ -219,7 +219,7 @@ let cp_prevars fmt (node, h) = *) let cp_init_aux_nodes fmt (node, h) = let rec aux fmt (node, nst, i) = - match find_app_opt node.cn_equations i with + match find_app_opt node.in_equations i with | None -> () (** All auxiliary nodes have been initialized *) | Some n -> begin @@ -230,7 +230,7 @@ let cp_init_aux_nodes fmt (node, h) = (Format.asprintf "t_state_%s" n.n_name) (i-1) end in - let nst = Hashtbl.find h node.cn_name in + let nst = Hashtbl.find h node.in_name in if nst.nt_count_app = 0 then () else begin @@ -262,7 +262,7 @@ let cp_node fmt (node, h) = Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n" cp_prototype (node, h) cp_init_aux_nodes (node, h) - cp_equations (node.cn_equations, Hashtbl.find h node.cn_name) + cp_equations (node.in_equations, Hashtbl.find h node.in_name) cp_prevars (node, h) (** [cp_nodes] recursively prints all the nodes of a program. *) @@ -279,7 +279,7 @@ let rec cp_nodes fmt (nodes, h) = (** main function that prints a C-code from a term of type [t_nodelist]. *) let ast_to_c prog = let prog_st_types = make_state_types prog in - let prog: c_nodelist = ast_to_cast prog prog_st_types in + let prog: i_nodelist = ast_to_cast prog prog_st_types in Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) cp_state_types prog_st_types diff --git a/src/cprint.ml b/src/cprint.ml index 5f191ae..39da179 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -7,7 +7,7 @@ open Ast let rec cp_includes fmt = function | [] -> () | h :: t -> - Format.fprintf fmt "#include <%s>\n%a" h cp_includes t + Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t let cp_node_state fmt (st: node_state) = let maybeprint fmt (ty, nb, name): unit = @@ -58,17 +58,17 @@ let rec cp_varlist fmt vl = cp_varlist vl let cp_prototype fmt (node, h): unit = - match Hashtbl.find_opt h node.cn_name with + match Hashtbl.find_opt h node.in_name with | None -> failwith "This should not happend!" | Some nst -> begin Format.fprintf fmt "void fn_%s (%s *state, %a)" - node.cn_name + node.in_name nst.nt_name - cp_varlist node.cn_inputs + cp_varlist node.in_inputs end -let rec cp_prototypes fmt ((nodes, h): c_nodelist * node_states) = +let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = match nodes with | [] -> () | node :: nodes -> diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index 31a4dc7..3cc296b 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -44,35 +44,35 @@ type c_var = | CVStored of string * int | CVInput of ident -type c_expression = - | CVar of c_var - | CMonOp of monop * c_expression - | CBinOp of binop * c_expression * c_expression - | CTriOp of triop * c_expression * c_expression * c_expression - | CComp of compop * c_expression * c_expression - | CWhen of c_expression * c_expression - | CReset of c_expression * c_expression - | CConst of const - | CTuple of (c_expression list) +type i_expression = + | IVar of c_var + | IMonOp of monop * i_expression + | IBinOp of binop * i_expression * i_expression + | ITriOp of triop * i_expression * i_expression * i_expression + | IComp of compop * i_expression * i_expression + | IWhen of i_expression * i_expression + | IReset of i_expression * i_expression + | IConst of const + | ITuple of (i_expression list) (** [CApp] below represents the n-th call to an aux node *) - | CApp of int * t_node * c_expression + | IApp of int * t_node * i_expression -and c_varlist = t_var list +and i_varlist = t_var list -and c_equation = c_varlist * c_expression +and i_equation = i_varlist * i_expression -and c_eqlist = c_equation list +and i_eqlist = i_equation list -and c_node = +and i_node = { - cn_name : ident; - cn_inputs: c_varlist; - cn_outputs: c_varlist; - cn_local_vars: c_varlist; - cn_equations: c_eqlist; + in_name : ident; + in_inputs: i_varlist; + in_outputs: i_varlist; + in_local_vars: i_varlist; + in_equations: i_eqlist; } -type c_nodelist = c_node list +type i_nodelist = i_node list type node_states = (ident, node_state) Hashtbl.t diff --git a/src/intermediate_utils.ml b/src/intermediate_utils.ml index c964e50..34414d1 100644 --- a/src/intermediate_utils.ml +++ b/src/intermediate_utils.ml @@ -2,15 +2,15 @@ open Intermediate_ast let rec find_app_opt eqs i = let rec find_app_expr_opt i = function - | CVar _ | CConst _ -> None - | CMonOp (_, e) -> find_app_expr_opt i e - | CReset (e, e') | CWhen (e, e') | CComp (_, e, e') | CBinOp (_, e, e') -> + | IVar _ | IConst _ -> None + | IMonOp (_, e) -> find_app_expr_opt i e + | IReset (e, e') | IWhen (e, e') | IComp (_, e, e') | IBinOp (_, e, e') -> begin match find_app_expr_opt i e with | None -> find_app_expr_opt i e' | Some n -> Some n end - | CTriOp (_, e, e', e'') -> + | ITriOp (_, e, e', e'') -> begin match find_app_expr_opt i e with | None -> @@ -21,15 +21,15 @@ let rec find_app_opt eqs i = end | Some n -> Some n end - | CTuple l -> + | ITuple l -> List.fold_left (fun acc e -> match acc, find_app_expr_opt i e with | Some n, _ -> Some n | None, v -> v) None l - (** [CApp] below represents the n-th call to an aux node *) - | CApp (j, n, e) -> + (** [IApp] below represents the n-th call to an aux node *) + | IApp (j, n, e) -> if i = j then Some n else find_app_expr_opt i e From cbc834b32abcc27993201c015da6cc1d1cd15528 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 22:36:42 +0100 Subject: [PATCH 07/50] [ast2C] constants, simple assignations, variables (+ one fix about pre storage) --- src/ast_to_c.ml | 109 +++++++++++++++++++++++++------------- src/cast.ml | 26 +++++++++ src/cprint.ml | 35 ++++++++++++ src/ctranslation.ml | 40 ++++++++++++++ src/intermediate_ast.ml | 20 +++---- src/intermediate_utils.ml | 14 ++--- src/main.ml | 4 +- 7 files changed, 191 insertions(+), 57 deletions(-) create mode 100644 src/cast.ml create mode 100644 src/ctranslation.ml diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 618cb11..5756bdb 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -3,44 +3,45 @@ open Intermediate_ast open Intermediate_utils open Cprint open Utils +open Ctranslation -(** [ast_to_cast] translates a [t_nodelist] into a [i_nodelist] *) -let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = +(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *) +let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist = let c = ref 1 in - let ast_to_cast_varlist vl = snd vl in - let rec ast_to_cast_expr hloc = function + let ast_to_intermediate_ast_varlist vl = snd vl in + let rec ast_to_intermediate_ast_expr hloc = function | EVar (_, v) -> begin match Hashtbl.find_opt hloc (v, false) with - | None -> IVar (CVInput (name_of_var v)) - | Some (s, i) -> IVar (CVStored (s, i)) + | None -> IEVar (CVInput (name_of_var v)) + | Some (s, i) -> IEVar (CVStored (s, i)) end - | EMonOp (_, op, e) -> IMonOp (op, ast_to_cast_expr hloc e) + | EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e) | EBinOp (_, op, e, e') -> - IBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | ETriOp (_, op, e, e', e'') -> - ITriOp - (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'') + IETriOp + (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e', ast_to_intermediate_ast_expr hloc e'') | EComp (_, op, e, e') -> - IComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | EWhen (_, e, e') -> - IWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | EReset (_, e, e') -> - IReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') - | EConst (_, c) -> IConst c - | ETuple (_, l) -> ITuple (List.map (ast_to_cast_expr hloc) l) + IEReset (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') + | EConst (_, c) -> IEConst c + | ETuple (_, l) -> IETuple (List.map (ast_to_intermediate_ast_expr hloc) l) | EApp (_, n, e) -> begin - let e = ast_to_cast_expr hloc e in - let res = IApp (!c, n, e) in + let e = ast_to_intermediate_ast_expr hloc e in + let res = IEApp (!c, n, e) in let () = incr c in res end in - let ast_to_cast_eq hloc (patt, expr) : i_equation = - (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in + let ast_to_intermediate_ast_eq hloc (patt, expr) : i_equation = + (ast_to_intermediate_ast_varlist patt, ast_to_intermediate_ast_expr hloc expr) in List.map begin fun node -> @@ -48,10 +49,10 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = let hloc = (Hashtbl.find h node.n_name).nt_map in { in_name = node.n_name; - in_inputs = ast_to_cast_varlist node.n_inputs; - in_outputs = ast_to_cast_varlist node.n_outputs; - in_local_vars = ast_to_cast_varlist node.n_local_vars; - in_equations = List.map (ast_to_cast_eq hloc) node.n_equations; + in_inputs = ast_to_intermediate_ast_varlist node.n_inputs; + in_outputs = ast_to_intermediate_ast_varlist node.n_outputs; + in_local_vars = ast_to_intermediate_ast_varlist node.n_local_vars; + in_equations = List.map (ast_to_intermediate_ast_eq hloc) node.n_equations; } end nodes @@ -71,8 +72,11 @@ let make_state_types nodes: node_states = let vars = List.filter (fun v -> type_var v = [ty]) (snd (varlist_concat node.n_outputs node.n_local_vars)) in + let all_vars = + List.filter (fun v -> type_var v = [ty]) + (snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in let pre_vars = - List.filter (fun v -> List.mem v pv) vars in + List.filter (fun v -> List.mem v pv) all_vars in let nb = (List.length vars) + (List.length pre_vars) in let tyh = Hashtbl.create nb in let i = @@ -205,10 +209,16 @@ let cp_prevars fmt (node, h) = "\n\t/* Remember the values used in the [pre] construct */\n"; List.iter (fun v -> (** Note that «dst_array = src_array» should hold. *) - let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in - let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s[%d];\n" - dst_array dst_idx src_array src_idx) + match Hashtbl.find_opt node_st.nt_map (v, false) with + | Some (src_array, src_idx) -> + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx + | None -> + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s;\n" + dst_array dst_idx (Utils.name_of_var v) + ) l @@ -241,20 +251,13 @@ let cp_init_aux_nodes fmt (node, h) = -(** The following function prints one equation of the program into a set of - * instruction ending in assignments. *) -let cp_equation fmt (eq, hloc) = - Format.fprintf fmt "\t\t/* TODO! */\n" - - - (** [cp_equations] prints the node equations. *) let rec cp_equations fmt (eqs, hloc) = match eqs with | [] -> () | eq :: eqs -> Format.fprintf fmt "%a%a" - cp_equation (eq, hloc) + cp_expression (equation_to_expression (hloc.nt_map, eq), hloc) cp_equations (eqs, hloc) (** [cp_node] prints a single node *) @@ -276,10 +279,40 @@ let rec cp_nodes fmt (nodes, h) = +let dump_var_locations (st: node_states) = + Hashtbl.iter + (fun n st -> + Format.printf "\n\n\tNODE: %s\n" n; + Hashtbl.iter + (fun ((v: t_var), (ispre: bool)) ((arr: string), (idx: int)) -> + match v, ispre with + | IVar s, true -> Format.printf "PRE Variable (int) %s stored as %s[%d]\n" + s arr idx + | BVar s, true -> Format.printf "PRE Variable (bool) %s stored as %s[%d]\n" + s arr idx + | RVar s, true -> Format.printf "PRE Variable (real) %s stored as %s[%d]\n" + s arr idx + | IVar s, false -> Format.printf "Variable (int) %s stored as %s[%d]\n" + s arr idx + | BVar s, false -> Format.printf "Variable (bool) %s stored as %s[%d]\n" + s arr idx + | RVar s, false -> Format.printf "Variable (real) %s stored as %s[%d]\n" + s arr idx) + st.nt_map) + st; + Format.printf "\n\n" + + + (** main function that prints a C-code from a term of type [t_nodelist]. *) -let ast_to_c prog = +let ast_to_c (debug: bool) prog = let prog_st_types = make_state_types prog in - let prog: i_nodelist = ast_to_cast prog prog_st_types in + let () = + if debug + then dump_var_locations prog_st_types + else () + in + let prog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) cp_state_types prog_st_types diff --git a/src/cast.ml b/src/cast.ml new file mode 100644 index 0000000..4bc3282 --- /dev/null +++ b/src/cast.ml @@ -0,0 +1,26 @@ +open Intermediate_ast +open Ast + +(** This file contains a small subset of the syntax of C required for the + * translation. *) + +(** A [c_block] represents a block in C. *) +type c_block = c_expression list + +(** A [c_expresion] represents a C expression, which can need sequences and + * function calls. *) +and c_expression = + | CAssign of c_var * c_value + | CSeq of c_expression * c_expression + | CIf of c_value * c_block * c_block + | CApplication of c_var list * c_expression + +(** A value here is anything that can be inlined into a single C expression + * containing no function call, condition, ... *) +and c_value = + | CVariable of c_var + | CMonOp of monop * c_value + | CBinOp of binop * c_value * c_value + | CComp of compop * c_value * c_value + | CConst of const + diff --git a/src/cprint.ml b/src/cprint.ml index 39da179..b3e8742 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -1,6 +1,7 @@ open Intermediate_utils open Intermediate_ast open Ast +open Cast (** This file contains extrimely simple functions printing C code. *) @@ -76,3 +77,37 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = cp_prototype (node, h) cp_prototypes (nodes, h) + + +let cp_value fmt value = + match value with + | CVariable (CVInput s) -> Format.fprintf fmt "%s" s + | CVariable (CVStored (arr, idx)) -> + Format.fprintf fmt "%s[%d]" arr idx + | CConst (CInt i) -> Format.fprintf fmt "%d" i + | CConst (CBool true) -> Format.fprintf fmt "true" + | CConst (CBool false) -> Format.fprintf fmt "false" + | CConst (CReal r) -> Format.fprintf fmt "%f" r + (**| CMonOp of monop * c_value + | CBinOp of binop * c_value * c_value + | CComp of compop * c_value * c_value*) + | _ -> failwith "[cprint.ml] TODO!" + + + + +(** The following function prints one transformed equation of the program into a + * set of instruction ending in assignments. *) +let cp_expression fmt (expr, hloc) = + let prefix = "\t" in + match expr with + | CAssign (CVStored (arr, idx), value) -> + begin + Format.fprintf fmt "%s%s[%d] = %a;\n" + prefix arr idx cp_value value + end + | CAssign (CVInput _, _) -> failwith "should not happend." + (*| CSeq of c_expression * c_expression + | CIf of c_value * c_block * c_block + | CApplication of c_var list * c_expression*) + | _ -> failwith "[cprint.ml] TODO!" diff --git a/src/ctranslation.ml b/src/ctranslation.ml new file mode 100644 index 0000000..aab6548 --- /dev/null +++ b/src/ctranslation.ml @@ -0,0 +1,40 @@ +open Ast +open Intermediate_ast +open Cast + +let iexpression_to_cvalue e = () + +let equation_to_expression (hloc, ((vl, expr): i_equation)) : c_expression = + let fetch_unique_var () = + match vl with + | [v] -> + begin + match Hashtbl.find_opt hloc (v, false) with + | None -> CVInput (Utils.name_of_var v) + | Some (arr, idx) -> CVStored (arr, idx) + end + | _ -> failwith "[ctranslation.ml] This should not happened." + in + match expr with + | IEVar vsrc -> + CAssign (fetch_unique_var (), CVariable vsrc) + | IEMonOp (MOp_pre, IEVar v) -> + CAssign (fetch_unique_var (), CVariable v) + | IEConst c -> + CAssign (fetch_unique_var (), CConst c) + (*| IEMonOp (op, e) -> + CMonOp (op, iexpression_to_cvalue e) + | IEBinOp (op, e, e') -> + CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEComp (op, e, e') -> + CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEConst c -> CConst c + TODO! + | IETriOp of triop * i_expression * i_expression * i_expression + | IEWhen of i_expression * i_expression + | IEReset of i_expression * i_expression + | IETuple of (i_expression list) + (** [CApp] below represents the n-th call to an aux node *) + | IEApp of int * t_node * i_expression*) + | _ -> failwith "[ctranslation.ml] TODO!" + diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index 3cc296b..4c520bf 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -45,17 +45,17 @@ type c_var = | CVInput of ident type i_expression = - | IVar of c_var - | IMonOp of monop * i_expression - | IBinOp of binop * i_expression * i_expression - | ITriOp of triop * i_expression * i_expression * i_expression - | IComp of compop * i_expression * i_expression - | IWhen of i_expression * i_expression - | IReset of i_expression * i_expression - | IConst of const - | ITuple of (i_expression list) + | IEVar of c_var + | IEMonOp of monop * i_expression + | IEBinOp of binop * i_expression * i_expression + | IETriOp of triop * i_expression * i_expression * i_expression + | IEComp of compop * i_expression * i_expression + | IEWhen of i_expression * i_expression + | IEReset of i_expression * i_expression + | IEConst of const + | IETuple of (i_expression list) (** [CApp] below represents the n-th call to an aux node *) - | IApp of int * t_node * i_expression + | IEApp of int * t_node * i_expression and i_varlist = t_var list diff --git a/src/intermediate_utils.ml b/src/intermediate_utils.ml index 34414d1..26804f8 100644 --- a/src/intermediate_utils.ml +++ b/src/intermediate_utils.ml @@ -2,15 +2,15 @@ open Intermediate_ast let rec find_app_opt eqs i = let rec find_app_expr_opt i = function - | IVar _ | IConst _ -> None - | IMonOp (_, e) -> find_app_expr_opt i e - | IReset (e, e') | IWhen (e, e') | IComp (_, e, e') | IBinOp (_, e, e') -> + | IEVar _ | IEConst _ -> None + | IEMonOp (_, e) -> find_app_expr_opt i e + | IEReset (e, e') | IEWhen (e, e') | IEComp (_, e, e') | IEBinOp (_, e, e') -> begin match find_app_expr_opt i e with | None -> find_app_expr_opt i e' | Some n -> Some n end - | ITriOp (_, e, e', e'') -> + | IETriOp (_, e, e', e'') -> begin match find_app_expr_opt i e with | None -> @@ -21,15 +21,15 @@ let rec find_app_opt eqs i = end | Some n -> Some n end - | ITuple l -> + | IETuple l -> List.fold_left (fun acc e -> match acc, find_app_expr_opt i e with | Some n, _ -> Some n | None, v -> v) None l - (** [IApp] below represents the n-th call to an aux node *) - | IApp (j, n, e) -> + (** [IEApp] below represents the n-th call to an aux node *) + | IEApp (j, n, e) -> if i = j then Some n else find_app_expr_opt i e diff --git a/src/main.ml b/src/main.ml index 80c3678..78e1dc1 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in + let default_passes = [] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -127,6 +127,6 @@ let _ = else ( if !nopopt then (fun _ -> ()) - else Ast_to_c.ast_to_c) + else Ast_to_c.ast_to_c !debug) end From 7a32d474d459c44594f17460768c3ab26c78efb1 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 23:36:07 +0100 Subject: [PATCH 08/50] [ast2C] support for some basic operations (exemple in test.node) --- src/ast_to_c.ml | 42 ++++++++++++++++----------------------- src/cprint.ml | 28 ++++++++++++++++++-------- src/ctranslation.ml | 29 ++++++++++++++++++++------- src/intermediate_ast.ml | 8 ++++---- src/intermediate_utils.ml | 8 ++++++++ src/test.node | 7 +++++++ 6 files changed, 78 insertions(+), 44 deletions(-) create mode 100644 src/test.node diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 5756bdb..be8b01b 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -14,7 +14,7 @@ let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist = let rec ast_to_intermediate_ast_expr hloc = function | EVar (_, v) -> begin - match Hashtbl.find_opt hloc (v, false) with + match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with | None -> IEVar (CVInput (name_of_var v)) | Some (s, i) -> IEVar (CVStored (s, i)) end @@ -77,8 +77,10 @@ let make_state_types nodes: node_states = (snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in let pre_vars = List.filter (fun v -> List.mem v pv) all_vars in + let vars = List.map Utils.name_of_var vars in + let pre_vars = List.map Utils.name_of_var pre_vars in let nb = (List.length vars) + (List.length pre_vars) in - let tyh = Hashtbl.create nb in + let tyh: (ident * bool, int) Hashtbl.t = Hashtbl.create nb in let i = List.fold_left (fun i v -> let () = Hashtbl.add tyh (v, false) i in i + 1) 0 vars in @@ -162,14 +164,14 @@ let make_state_types nodes: node_states = let () = List.iteri (fun n (v: t_var) -> match v with - | IVar _ -> - let i = Hashtbl.find h_int (v, false) in + | IVar s -> + let i = Hashtbl.find h_int (s, false) in Hashtbl.add h_out n ("ivars", i) - | BVar _ -> - let i = Hashtbl.find h_bool (v, false) in + | BVar s -> + let i = Hashtbl.find h_bool (s, false) in Hashtbl.add h_out n ("bvars", i) - | RVar _ -> - let i = Hashtbl.find h_real (v, false) in + | RVar s -> + let i = Hashtbl.find h_real (s, false) in Hashtbl.add h_out n ("rvars", i)) (snd node.n_outputs) in let () = Hashtbl.add h node_name @@ -217,9 +219,9 @@ let cp_prevars fmt (node, h) = | None -> let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in Format.fprintf fmt "\t%s[%d] = %s;\n" - dst_array dst_idx (Utils.name_of_var v) + dst_array dst_idx v ) - l + (List.map Utils.name_of_var l) @@ -257,7 +259,7 @@ let rec cp_equations fmt (eqs, hloc) = | [] -> () | eq :: eqs -> Format.fprintf fmt "%a%a" - cp_expression (equation_to_expression (hloc.nt_map, eq), hloc) + cp_expression (equation_to_expression (hloc.nt_map, eq), hloc.nt_map) cp_equations (eqs, hloc) (** [cp_node] prints a single node *) @@ -284,20 +286,10 @@ let dump_var_locations (st: node_states) = (fun n st -> Format.printf "\n\n\tNODE: %s\n" n; Hashtbl.iter - (fun ((v: t_var), (ispre: bool)) ((arr: string), (idx: int)) -> - match v, ispre with - | IVar s, true -> Format.printf "PRE Variable (int) %s stored as %s[%d]\n" - s arr idx - | BVar s, true -> Format.printf "PRE Variable (bool) %s stored as %s[%d]\n" - s arr idx - | RVar s, true -> Format.printf "PRE Variable (real) %s stored as %s[%d]\n" - s arr idx - | IVar s, false -> Format.printf "Variable (int) %s stored as %s[%d]\n" - s arr idx - | BVar s, false -> Format.printf "Variable (bool) %s stored as %s[%d]\n" - s arr idx - | RVar s, false -> Format.printf "Variable (real) %s stored as %s[%d]\n" - s arr idx) + (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) st.nt_map) st; Format.printf "\n\n" diff --git a/src/cprint.ml b/src/cprint.ml index b3e8742..40f02e7 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -79,23 +79,35 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = -let cp_value fmt value = +let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = match value with | CVariable (CVInput s) -> Format.fprintf fmt "%s" s - | CVariable (CVStored (arr, idx)) -> - Format.fprintf fmt "%s[%d]" arr idx + | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "%s[%d]" arr idx | CConst (CInt i) -> Format.fprintf fmt "%d" i | CConst (CBool true) -> Format.fprintf fmt "true" | CConst (CBool false) -> Format.fprintf fmt "false" | CConst (CReal r) -> Format.fprintf fmt "%f" r - (**| CMonOp of monop * c_value - | CBinOp of binop * c_value * c_value - | CComp of compop * c_value * c_value*) + | CMonOp (MOp_not, v) -> Format.fprintf fmt "! (%a)" cp_value (v, hloc) + | CMonOp (MOp_minus, v) -> Format.fprintf fmt "- (%a)" cp_value (v, hloc) + | CMonOp (MOp_pre, (CVariable v)) -> + let varname = (match v with + | CVStored (arr, idx) -> + begin + match find_varname hloc (arr, idx) with + | None -> failwith "[cprint.ml] This varname should be defined." + | Some (n, _) -> n + end + | CVInput n -> n) in + let (arr, idx) = Hashtbl.find hloc (varname, true) in + Format.fprintf fmt "%s[%d]" arr idx + | CBinOp (BOp_add, v, v') -> + Format.fprintf fmt "(%a) + (%a)" + cp_value (v, hloc) cp_value (v', hloc) + (**| CComp of compop * c_value * c_value*) | _ -> failwith "[cprint.ml] TODO!" - (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) let cp_expression fmt (expr, hloc) = @@ -104,7 +116,7 @@ let cp_expression fmt (expr, hloc) = | CAssign (CVStored (arr, idx), value) -> begin Format.fprintf fmt "%s%s[%d] = %a;\n" - prefix arr idx cp_value value + prefix arr idx cp_value (value, hloc) end | CAssign (CVInput _, _) -> failwith "should not happend." (*| CSeq of c_expression * c_expression diff --git a/src/ctranslation.ml b/src/ctranslation.ml index aab6548..c0de7ff 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -2,14 +2,27 @@ open Ast open Intermediate_ast open Cast -let iexpression_to_cvalue e = () +let rec iexpression_to_cvalue e = + match e with + | IEVar v -> CVariable v + | IEMonOp (op, e) -> CMonOp (op, iexpression_to_cvalue e) + | IEBinOp (op, e, e') -> + CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEComp (op, e, e') -> + CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEConst c -> CConst c + | IEWhen _ + | IEReset _ + | IETuple _ + | IEApp _ + | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." -let equation_to_expression (hloc, ((vl, expr): i_equation)) : c_expression = +let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, expr): i_equation)) : c_expression = let fetch_unique_var () = match vl with | [v] -> begin - match Hashtbl.find_opt hloc (v, false) with + match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with | None -> CVInput (Utils.name_of_var v) | Some (arr, idx) -> CVStored (arr, idx) end @@ -22,11 +35,13 @@ let equation_to_expression (hloc, ((vl, expr): i_equation)) : c_expression = CAssign (fetch_unique_var (), CVariable v) | IEConst c -> CAssign (fetch_unique_var (), CConst c) - (*| IEMonOp (op, e) -> - CMonOp (op, iexpression_to_cvalue e) + | IEMonOp (op, e) -> + CAssign (fetch_unique_var (), + CMonOp (op, iexpression_to_cvalue e)) | IEBinOp (op, e, e') -> - CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') - | IEComp (op, e, e') -> + CAssign (fetch_unique_var (), + CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')) + (*| IEComp (op, e, e') -> CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') | IEConst c -> CConst c TODO! diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index 4c520bf..e259596 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -29,10 +29,10 @@ type node_state = nt_nb_int : int; nt_nb_real: int; nt_nb_bool: int; - nt_map_int: (t_var * bool, int) Hashtbl.t; - nt_map_bool: (t_var * bool, int) Hashtbl.t; - nt_map_real: (t_var * bool, int) Hashtbl.t; - nt_map: (t_var * bool, string * int) Hashtbl.t; + nt_map_int: (ident * bool, int) Hashtbl.t; + nt_map_bool: (ident * bool, int) Hashtbl.t; + nt_map_real: (ident * bool, int) Hashtbl.t; + nt_map: (ident * bool, string * int) Hashtbl.t; nt_output_map: (int, string * int) Hashtbl.t; nt_prevars: t_var list; nt_count_app: int; diff --git a/src/intermediate_utils.ml b/src/intermediate_utils.ml index 26804f8..e136508 100644 --- a/src/intermediate_utils.ml +++ b/src/intermediate_utils.ml @@ -40,3 +40,11 @@ let rec find_app_opt eqs i = match find_app_expr_opt i expr with | None -> find_app_opt eqs i | Some n -> Some n + +let find_varname h v = + Hashtbl.fold + (fun s e acc -> + match acc with + | None -> if e = v then Some s else None + | Some _ -> acc) + h None diff --git a/src/test.node b/src/test.node new file mode 100644 index 0000000..4e3d799 --- /dev/null +++ b/src/test.node @@ -0,0 +1,7 @@ +node n (i: int) returns (o: int); +var v, t: int; +let + o = 1; + v = pre o; + t = o + pre i; +tel From 233b385608e09696b19495e39b54d35897899479 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 23:46:39 +0100 Subject: [PATCH 09/50] missing 'state->' added + print +,-,*,... --- src/ast_to_c.ml | 4 ++-- src/cprint.ml | 23 +++++++++++++++++------ src/test.node | 4 +++- 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index be8b01b..71be88e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -214,11 +214,11 @@ let cp_prevars fmt (node, h) = match Hashtbl.find_opt node_st.nt_map (v, false) with | Some (src_array, src_idx) -> let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + Format.fprintf fmt "\tstate->%s[%d] = state->%s[%d];\n" dst_array dst_idx src_array src_idx | None -> let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s;\n" + Format.fprintf fmt "\tstate->%s[%d] = %s;\n" dst_array dst_idx v ) (List.map Utils.name_of_var l) diff --git a/src/cprint.ml b/src/cprint.ml index 40f02e7..afd619c 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -80,9 +80,19 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = + let string_of_binop = function + | BOp_add -> "+" + | BOp_sub -> "-" + | BOp_mul -> "*" + | BOp_div -> "/" + | BOp_mod -> "%" + | BOp_and -> "&&" + | BOp_or -> "||" + | BOp_arrow -> failwith "[cprint.ml] string_of_binop undefined on (->)" + in match value with | CVariable (CVInput s) -> Format.fprintf fmt "%s" s - | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "%s[%d]" arr idx + | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx | CConst (CInt i) -> Format.fprintf fmt "%d" i | CConst (CBool true) -> Format.fprintf fmt "true" | CConst (CBool false) -> Format.fprintf fmt "false" @@ -99,10 +109,11 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = end | CVInput n -> n) in let (arr, idx) = Hashtbl.find hloc (varname, true) in - Format.fprintf fmt "%s[%d]" arr idx - | CBinOp (BOp_add, v, v') -> - Format.fprintf fmt "(%a) + (%a)" - cp_value (v, hloc) cp_value (v', hloc) + Format.fprintf fmt "state->%s[%d]" arr idx + | CBinOp (BOp_arrow, v, v') -> failwith "[cprint.ml] (->) TODO!" + | CBinOp (op, v, v') -> + Format.fprintf fmt "(%a) %s (%a)" + cp_value (v, hloc) (string_of_binop op) cp_value (v', hloc) (**| CComp of compop * c_value * c_value*) | _ -> failwith "[cprint.ml] TODO!" @@ -115,7 +126,7 @@ let cp_expression fmt (expr, hloc) = match expr with | CAssign (CVStored (arr, idx), value) -> begin - Format.fprintf fmt "%s%s[%d] = %a;\n" + Format.fprintf fmt "%sstate->%s[%d] = %a;\n" prefix arr idx cp_value (value, hloc) end | CAssign (CVInput _, _) -> failwith "should not happend." diff --git a/src/test.node b/src/test.node index 4e3d799..324533a 100644 --- a/src/test.node +++ b/src/test.node @@ -1,6 +1,8 @@ node n (i: int) returns (o: int); -var v, t: int; +var v, t: int; a, b: bool; let + a = true; + b = a and not (pre a); o = 1; v = pre o; t = o + pre i; From 791af719138acc52722d1cc1523623b050b18ae1 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 23:58:45 +0100 Subject: [PATCH 10/50] [ast2C] print all basic operators --- src/cprint.ml | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index afd619c..0ad269a 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -90,6 +90,14 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | BOp_or -> "||" | BOp_arrow -> failwith "[cprint.ml] string_of_binop undefined on (->)" in + let string_of_compop = function + | COp_eq -> "==" + | COp_neq -> "!=" + | COp_le -> "<=" + | COp_lt -> "<" + | COp_ge -> ">=" + | COp_gt -> ">" + in match value with | CVariable (CVInput s) -> Format.fprintf fmt "%s" s | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx @@ -114,14 +122,16 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CBinOp (op, v, v') -> Format.fprintf fmt "(%a) %s (%a)" cp_value (v, hloc) (string_of_binop op) cp_value (v', hloc) - (**| CComp of compop * c_value * c_value*) - | _ -> failwith "[cprint.ml] TODO!" - + | CComp (op, v, v') -> + Format.fprintf fmt "(%a) %s (%a)" + cp_value (v, hloc) (string_of_compop op) cp_value (v', hloc) + | CMonOp (MOp_pre, _) -> + failwith "[cprint.ml] The linearization should have removed this case." (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) -let cp_expression fmt (expr, hloc) = +let rec cp_expression fmt (expr, hloc) = let prefix = "\t" in match expr with | CAssign (CVStored (arr, idx), value) -> @@ -130,7 +140,11 @@ let cp_expression fmt (expr, hloc) = prefix arr idx cp_value (value, hloc) end | CAssign (CVInput _, _) -> failwith "should not happend." - (*| CSeq of c_expression * c_expression - | CIf of c_value * c_block * c_block + | CSeq (e, e') -> + Format.fprintf fmt "%a%a" + cp_expression (e, hloc) + cp_expression (e', hloc) + (**| CIf of c_value * c_block * c_block | CApplication of c_var list * c_expression*) | _ -> failwith "[cprint.ml] TODO!" + From 243e8f245aa45c77eb6f825952f7a1e8da32346e Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 00:11:02 +0100 Subject: [PATCH 11/50] [ast2C] adding the (->) construct --- src/cprint.ml | 4 +++- src/ctranslation.ml | 8 ++++---- src/test.node | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index 0ad269a..81cb1fc 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -118,7 +118,9 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CVInput n -> n) in let (arr, idx) = Hashtbl.find hloc (varname, true) in Format.fprintf fmt "state->%s[%d]" arr idx - | CBinOp (BOp_arrow, v, v') -> failwith "[cprint.ml] (->) TODO!" + | CBinOp (BOp_arrow, v, v') -> + Format.fprintf fmt "(state->is_init ? (%a) : (%a))" + cp_value (v, hloc) cp_value (v', hloc) | CBinOp (op, v, v') -> Format.fprintf fmt "(%a) %s (%a)" cp_value (v, hloc) (string_of_binop op) cp_value (v', hloc) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index c0de7ff..78979a4 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -41,10 +41,10 @@ let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, | IEBinOp (op, e, e') -> CAssign (fetch_unique_var (), CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')) - (*| IEComp (op, e, e') -> - CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') - | IEConst c -> CConst c - TODO! + | IEComp (op, e, e') -> + CAssign (fetch_unique_var (), + CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')) + (*TODO! | IETriOp of triop * i_expression * i_expression * i_expression | IEWhen of i_expression * i_expression | IEReset of i_expression * i_expression diff --git a/src/test.node b/src/test.node index 324533a..f6054ee 100644 --- a/src/test.node +++ b/src/test.node @@ -1,7 +1,7 @@ node n (i: int) returns (o: int); var v, t: int; a, b: bool; let - a = true; + a = true -> false; b = a and not (pre a); o = 1; v = pre o; From 007c5b2862a19b3dc293b91102d297f279539dd9 Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 00:26:51 +0100 Subject: [PATCH 12/50] [c printer] Ok. --- src/cast.ml | 2 +- src/cprint.ml | 35 +++++++++++++++++++++++++++++++---- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/src/cast.ml b/src/cast.ml index 4bc3282..f000b2a 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -13,7 +13,7 @@ and c_expression = | CAssign of c_var * c_value | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block - | CApplication of c_var list * c_expression + | CApplication of ident * c_var list (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 81cb1fc..572ab06 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -40,11 +40,28 @@ let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = Format.fprintf fmt "/* Struct holding states of the node %s: */\n%a" n cp_node_state nst) h +let cp_var' fmt = function + | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx + | CVInput s -> Format.fprintf fmt "s" + let cp_var fmt = function | IVar s -> Format.fprintf fmt "int %s" s | BVar s -> Format.fprintf fmt "bool %s" s | RVar s -> Format.fprintf fmt "double %s" s +let rec cp_varlist' fmt vl = + let maybeprint fmt = function + | [] -> () + | _ :: _ -> Format.fprintf fmt ", " + in + match vl with + | [] -> () + | v :: vl -> + Format.fprintf fmt "%a%a%a" + cp_var' v + maybeprint vl + cp_varlist' vl + let rec cp_varlist fmt vl = let maybeprint fmt = function | [] -> () @@ -130,11 +147,14 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CMonOp (MOp_pre, _) -> failwith "[cprint.ml] The linearization should have removed this case." - (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) let rec cp_expression fmt (expr, hloc) = let prefix = "\t" in + let rec cp_block fmt = function + | [] -> () + | e :: b -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block b + in match expr with | CAssign (CVStored (arr, idx), value) -> begin @@ -146,7 +166,14 @@ let rec cp_expression fmt (expr, hloc) = Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_expression (e', hloc) - (**| CIf of c_value * c_block * c_block - | CApplication of c_var list * c_expression*) - | _ -> failwith "[cprint.ml] TODO!" + | CApplication (fn, l) -> + (Format.fprintf fmt "%s(%a);" + fn + cp_varlist' l; + failwith "TODO: use nt_output_map to fetch the output!") + | CIf (v, b1, b2) -> + Format.fprintf fmt "if (%a) {\n%a\t\t} else {\n%a\t\t}\n" + cp_value (v, hloc) + cp_block b1 + cp_block b2 From 1d4e1820e465cc70d2eb27b1bc68042ce39db011 Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 09:41:22 +0100 Subject: [PATCH 13/50] [ast2C] Applications to values --- src/ast_to_c.ml | 8 ++++---- src/cast.ml | 2 +- src/cprint.ml | 25 ++++++++++++++++++++----- src/ctranslation.ml | 29 +++++++++++++++++++++++++---- src/test2.node | 10 ++++++++++ 5 files changed, 60 insertions(+), 14 deletions(-) create mode 100644 src/test2.node diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 71be88e..e812ff5 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -254,20 +254,20 @@ let cp_init_aux_nodes fmt (node, h) = (** [cp_equations] prints the node equations. *) -let rec cp_equations fmt (eqs, hloc) = +let rec cp_equations fmt (eqs, hloc, h) = match eqs with | [] -> () | eq :: eqs -> Format.fprintf fmt "%a%a" - cp_expression (equation_to_expression (hloc.nt_map, eq), hloc.nt_map) - cp_equations (eqs, hloc) + cp_expression (equation_to_expression (hloc, h, eq), hloc.nt_map) + cp_equations (eqs, hloc, h) (** [cp_node] prints a single node *) let cp_node fmt (node, h) = Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n" cp_prototype (node, h) cp_init_aux_nodes (node, h) - cp_equations (node.in_equations, Hashtbl.find h node.in_name) + cp_equations (node.in_equations, Hashtbl.find h node.in_name, h) cp_prevars (node, h) (** [cp_nodes] recursively prints all the nodes of a program. *) diff --git a/src/cast.ml b/src/cast.ml index f000b2a..81b0672 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -13,7 +13,7 @@ and c_expression = | CAssign of c_var * c_value | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block - | CApplication of ident * c_var list + | CApplication of ident * int * c_var list * c_var list * node_states (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 572ab06..714ae48 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -166,11 +166,26 @@ let rec cp_expression fmt (expr, hloc) = Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_expression (e', hloc) - | CApplication (fn, l) -> - (Format.fprintf fmt "%s(%a);" - fn - cp_varlist' l; - failwith "TODO: use nt_output_map to fetch the output!") + | CApplication (fn, nb, argl, destl, h) -> + begin + let aux_node_st = Hashtbl.find h fn in + let h_out = aux_node_st.nt_output_map in + Format.fprintf fmt "%sfn_%s(%a);\n" + prefix fn + cp_varlist' argl; + let _ = List.fold_left + (fun i var -> + match var with + | CVStored (arr, idx) -> + let (arr', idx') = Hashtbl.find h_out i in + Format.fprintf fmt "%sstate->%s[%d] = ((%s*)(state->aux_states[%d]))->%s[%d];\n" + prefix arr idx + aux_node_st.nt_name (nb-1) + arr' idx'; + i+1 + | CVInput _ -> failwith "[cprint.ml] Impossible!") + 0 destl in () + end | CIf (v, b1, b2) -> Format.fprintf fmt "if (%a) {\n%a\t\t} else {\n%a\t\t}\n" cp_value (v, hloc) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 78979a4..0e593f3 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -17,7 +17,8 @@ let rec iexpression_to_cvalue e = | IEApp _ | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." -let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, expr): i_equation)) : c_expression = +let equation_to_expression (node_st, node_sts, (vl, expr)) = + let hloc = node_st.nt_map in let fetch_unique_var () = match vl with | [v] -> @@ -44,12 +45,32 @@ let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, | IEComp (op, e, e') -> CAssign (fetch_unique_var (), CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')) + (** [CApp] below represents the i-th call to an aux node *) + | IEApp (i, node, e) -> + (** e is a tuple of variables due to the linearization pass *) + let al: c_var list = + match e with + | IETuple l -> + List.map + (function + | IEVar v -> v + | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + ) l + | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + in + let vl = + List.map + (fun v -> + match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with + | Some (arr, idx) -> CVStored (arr, idx) + | None -> CVInput (Utils.name_of_var v)) + vl + in + CApplication (node.n_name,i , al, vl, node_sts) (*TODO! | IETriOp of triop * i_expression * i_expression * i_expression | IEWhen of i_expression * i_expression | IEReset of i_expression * i_expression - | IETuple of (i_expression list) - (** [CApp] below represents the n-th call to an aux node *) - | IEApp of int * t_node * i_expression*) + | IETuple of (i_expression list)*) | _ -> failwith "[ctranslation.ml] TODO!" diff --git a/src/test2.node b/src/test2.node new file mode 100644 index 0000000..5dcbf29 --- /dev/null +++ b/src/test2.node @@ -0,0 +1,10 @@ +node aux (i: int) returns (a, b: int); +let + a = 1 -> pre i; + b = 2 * i -> (3 * pre i); +tel + +node n (i: int) returns (o1, o2: int); +let + (o1, o2) = aux (i); +tel From ce686f6c9a1051e89ae592e14d7a6e00b63e459f Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 10:41:36 +0100 Subject: [PATCH 14/50] [ast2C] merge ok (needs linearization) --- src/ast_to_c.ml | 2 +- src/cprint.ml | 25 ++++++++++++++++++++----- src/ctranslation.ml | 13 +++++++++---- src/test2.node | 3 +++ 4 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index e812ff5..37f8f4e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -247,7 +247,7 @@ let cp_init_aux_nodes fmt (node, h) = then () else begin Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\ - \tif (state->is_init) {\n%a\t}\n" + \tif (state->is_init) {\n%a\t}\n\n\n" aux (node, nst, nst.nt_count_app) end diff --git a/src/cprint.ml b/src/cprint.ml index 714ae48..43767da 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -42,7 +42,7 @@ let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = let cp_var' fmt = function | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx - | CVInput s -> Format.fprintf fmt "s" + | CVInput s -> Format.fprintf fmt "%s" s let cp_var fmt = function | IVar s -> Format.fprintf fmt "int %s" s @@ -147,10 +147,12 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CMonOp (MOp_pre, _) -> failwith "[cprint.ml] The linearization should have removed this case." +let prefix_ = ref "\t" + (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) let rec cp_expression fmt (expr, hloc) = - let prefix = "\t" in + let prefix = !prefix_ in let rec cp_block fmt = function | [] -> () | e :: b -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block b @@ -170,8 +172,9 @@ let rec cp_expression fmt (expr, hloc) = begin let aux_node_st = Hashtbl.find h fn in let h_out = aux_node_st.nt_output_map in - Format.fprintf fmt "%sfn_%s(%a);\n" + Format.fprintf fmt "%sfn_%s(%s, %a);\n" prefix fn + (Format.asprintf "state->aux_states[%d]" (nb-1)) cp_varlist' argl; let _ = List.fold_left (fun i var -> @@ -186,9 +189,21 @@ let rec cp_expression fmt (expr, hloc) = | CVInput _ -> failwith "[cprint.ml] Impossible!") 0 destl in () end - | CIf (v, b1, b2) -> - Format.fprintf fmt "if (%a) {\n%a\t\t} else {\n%a\t\t}\n" + | CIf (v, b1, []) -> + let p = prefix in + prefix_ := prefix^"\t"; + Format.fprintf fmt "%sif (%a) {\n%a%s}\n" + p cp_value (v, hloc) cp_block b1 + p; + prefix_ := p + | CIf (v, b1, b2) -> + Format.fprintf fmt "%sif (%a) {\n%a%s} else {\n%a%s}\n" + prefix + cp_value (v, hloc) + cp_block b1 + prefix cp_block b2 + prefix diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 0e593f3..5433596 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -17,7 +17,7 @@ let rec iexpression_to_cvalue e = | IEApp _ | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." -let equation_to_expression (node_st, node_sts, (vl, expr)) = +let rec equation_to_expression (node_st, node_sts, (vl, expr)) = let hloc = node_st.nt_map in let fetch_unique_var () = match vl with @@ -67,10 +67,15 @@ let equation_to_expression (node_st, node_sts, (vl, expr)) = vl in CApplication (node.n_name,i , al, vl, node_sts) + | IETuple _ -> failwith "[ctranslation.ml] linearisatiosn should have transformed you." + | IEWhen (expr, cond) -> + begin + CIf (iexpression_to_cvalue cond, + [equation_to_expression (node_st, node_sts, (vl, expr))], + []) + end (*TODO! | IETriOp of triop * i_expression * i_expression * i_expression - | IEWhen of i_expression * i_expression - | IEReset of i_expression * i_expression - | IETuple of (i_expression list)*) + | IEReset of i_expression * i_expression*) | _ -> failwith "[ctranslation.ml] TODO!" diff --git a/src/test2.node b/src/test2.node index 5dcbf29..a88c1e6 100644 --- a/src/test2.node +++ b/src/test2.node @@ -5,6 +5,9 @@ let tel node n (i: int) returns (o1, o2: int); +var t1, t2: int; c: bool; let + c = true -> not pre c; + (t1, t2) = aux (i) when c; (o1, o2) = aux (i); tel From 1491e279f7a5a8bcac284e2abebdc5d838e5da0e Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 13:38:40 +0100 Subject: [PATCH 15/50] [ast2C] printer: ok. --- src/ast_to_c.ml | 21 ++++++++++++++------- src/cprint.ml | 26 +++++++++++++++----------- src/ctranslation.ml | 29 +++++++++++++++++++++++++---- src/test2.node | 6 ++++-- 4 files changed, 58 insertions(+), 24 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 37f8f4e..12c7f1e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -2,6 +2,7 @@ open Ast open Intermediate_ast open Intermediate_utils open Cprint +open Cast open Utils open Ctranslation @@ -254,13 +255,19 @@ let cp_init_aux_nodes fmt (node, h) = (** [cp_equations] prints the node equations. *) -let rec cp_equations fmt (eqs, hloc, h) = - match eqs with - | [] -> () - | eq :: eqs -> - Format.fprintf fmt "%a%a" - cp_expression (equation_to_expression (hloc, h, eq), hloc.nt_map) - cp_equations (eqs, hloc, h) +let cp_equations fmt (eqs, hloc, h) = + (** [main_block] is modified through some optimization passes, eg: + * - merge two CIf blocks using the same condition + * - replace [if (! c) { b1 } else {b2 }] by [if(c) { b2 } else { b1 }] + * + * These passes are defined in [ctranslation.ml] + *) + let main_block: c_block = + List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in + let main_block = remove_ifnot main_block in + let main_block = merge_neighbour_ifs main_block in + Format.fprintf fmt "\t/*Main code :*/\n%a" + cp_block (main_block, hloc.nt_map) (** [cp_node] prints a single node *) let cp_node fmt (node, h) = diff --git a/src/cprint.ml b/src/cprint.ml index 43767da..eab8edb 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -151,12 +151,13 @@ let prefix_ = ref "\t" (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) -let rec cp_expression fmt (expr, hloc) = +let rec cp_block fmt (b, hloc) = + match b with + | [] -> () + | e :: b -> + Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block (b, hloc) +and cp_expression fmt (expr, hloc) = let prefix = !prefix_ in - let rec cp_block fmt = function - | [] -> () - | e :: b -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block b - in match expr with | CAssign (CVStored (arr, idx), value) -> begin @@ -195,15 +196,18 @@ let rec cp_expression fmt (expr, hloc) = Format.fprintf fmt "%sif (%a) {\n%a%s}\n" p cp_value (v, hloc) - cp_block b1 + cp_block (b1, hloc) p; prefix_ := p | CIf (v, b1, b2) -> + let p = prefix in + prefix_ := prefix^"\t"; Format.fprintf fmt "%sif (%a) {\n%a%s} else {\n%a%s}\n" - prefix + p cp_value (v, hloc) - cp_block b1 - prefix - cp_block b2 - prefix + cp_block (b1, hloc) + p + cp_block (b2, hloc) + p; + prefix_ := p diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 5433596..bc8959b 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -74,8 +74,29 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = [equation_to_expression (node_st, node_sts, (vl, expr))], []) end - (*TODO! - | IETriOp of triop * i_expression * i_expression * i_expression - | IEReset of i_expression * i_expression*) - | _ -> failwith "[ctranslation.ml] TODO!" + | IETriOp (TOp_if, _, _, _) -> + failwith "[ctranslation.ml] A pass should have turned conditionnals into merges." + | IETriOp (TOp_merge, c, e, e') -> + CIf (iexpression_to_cvalue c, + [equation_to_expression (node_st, node_sts, (vl, e))], + [equation_to_expression (node_st, node_sts, (vl, e'))]) + | IEReset _ -> failwith "[ctranslation.ml] A pass should have removed resets." + + +let rec remove_ifnot = function + | [] -> [] + | CIf (CMonOp (MOp_not, c), bh :: bt, b'h :: b't) :: block -> + (CIf (c, b'h :: b't, bh :: bt)) :: (remove_ifnot block ) + | stmt :: block -> + stmt :: (remove_ifnot block) + +let rec merge_neighbour_ifs = function + | [] -> [] + | [stmt] -> [stmt] + | CIf (c, e1, e2) :: CIf (c', e'1, e'2) :: b -> + if c = c' + then merge_neighbour_ifs (CIf (c, e1 @ e'1, e2 @ e'2) :: b) + else (CIf (c, e1, e2)) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b) + | stmt :: stmt' :: b -> + stmt :: merge_neighbour_ifs (stmt' :: b) diff --git a/src/test2.node b/src/test2.node index a88c1e6..ac054f7 100644 --- a/src/test2.node +++ b/src/test2.node @@ -5,9 +5,11 @@ let tel node n (i: int) returns (o1, o2: int); -var t1, t2: int; c: bool; +var u1, u2, t1, t2: int; c: bool; let c = true -> not pre c; (t1, t2) = aux (i) when c; - (o1, o2) = aux (i); + (u1, u2) = aux (i) when (not c); + o1 = merge c t1 u1; + o2 = merge c t2 u2; tel From c3a64a2baef8b36691540faab3d38dff05a11a2b Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Sun, 18 Dec 2022 14:31:56 +0100 Subject: [PATCH 16/50] Correct some typos --- src/ast_to_c.ml | 2 +- src/cprint.ml | 6 +++--- src/ctranslation.ml | 2 +- src/lustre_pp.ml | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 12c7f1e..ef77938 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -258,7 +258,7 @@ let cp_init_aux_nodes fmt (node, h) = let cp_equations fmt (eqs, hloc, h) = (** [main_block] is modified through some optimization passes, eg: * - merge two CIf blocks using the same condition - * - replace [if (! c) { b1 } else {b2 }] by [if(c) { b2 } else { b1 }] + * - replace [if (! c) { b1 } else { b2 }] by [if(c) { b2 } else { b1 }] * * These passes are defined in [ctranslation.ml] *) diff --git a/src/cprint.ml b/src/cprint.ml index eab8edb..d5a1662 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -3,7 +3,7 @@ open Intermediate_ast open Ast open Cast -(** This file contains extrimely simple functions printing C code. *) +(** This file contains extremely simple functions printing C code. *) let rec cp_includes fmt = function | [] -> () @@ -77,7 +77,7 @@ let rec cp_varlist fmt vl = let cp_prototype fmt (node, h): unit = match Hashtbl.find_opt h node.in_name with - | None -> failwith "This should not happend!" + | None -> failwith "This should not happened!" | Some nst -> begin Format.fprintf fmt "void fn_%s (%s *state, %a)" @@ -164,7 +164,7 @@ and cp_expression fmt (expr, hloc) = Format.fprintf fmt "%sstate->%s[%d] = %a;\n" prefix arr idx cp_value (value, hloc) end - | CAssign (CVInput _, _) -> failwith "should not happend." + | CAssign (CVInput _, _) -> failwith "should not happened." | CSeq (e, e') -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index bc8959b..48af417 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -67,7 +67,7 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = vl in CApplication (node.n_name,i , al, vl, node_sts) - | IETuple _ -> failwith "[ctranslation.ml] linearisatiosn should have transformed you." + | IETuple _ -> failwith "[ctranslation.ml] linearization should have transformed you." | IEWhen (expr, cond) -> begin CIf (iexpression_to_cvalue cond, diff --git a/src/lustre_pp.ml b/src/lustre_pp.ml index 11aa484..11335b4 100644 --- a/src/lustre_pp.ml +++ b/src/lustre_pp.ml @@ -70,7 +70,7 @@ let pp_expression = begin match c with | CBool b -> Format.fprintf fmt "\t\t\t%s<%s : bool>\n" prefix (Bool.to_string b) | CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i - | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r + | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: real>\n" prefix r end | EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v | EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v From 37dfcdda35b7ce780af40b0c97a30ee5aafd5c73 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Sun, 18 Dec 2022 14:42:26 +0100 Subject: [PATCH 17/50] Remove unneeded node prototypes, as Lustre only allows to call already defined nodes --- src/ast_to_c.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index ef77938..746e2a8 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -312,9 +312,8 @@ let ast_to_c (debug: bool) prog = else () in let prog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in - Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" + Format.printf "%a\n\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) cp_state_types prog_st_types - cp_prototypes (prog, prog_st_types) cp_nodes (prog, prog_st_types) From 273a86816238b156938fda9e432f2f6644895c3b Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Sun, 18 Dec 2022 14:45:23 +0100 Subject: [PATCH 18/50] Simplify `cp_value` for boolean constants in `src/cprint.ml` --- src/cprint.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index d5a1662..a36ca3e 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -119,8 +119,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CVariable (CVInput s) -> Format.fprintf fmt "%s" s | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx | CConst (CInt i) -> Format.fprintf fmt "%d" i - | CConst (CBool true) -> Format.fprintf fmt "true" - | CConst (CBool false) -> Format.fprintf fmt "false" + | CConst (CBool b) -> Format.fprintf fmt "%s" (Bool.to_string b) | CConst (CReal r) -> Format.fprintf fmt "%f" r | CMonOp (MOp_not, v) -> Format.fprintf fmt "! (%a)" cp_value (v, hloc) | CMonOp (MOp_minus, v) -> Format.fprintf fmt "- (%a)" cp_value (v, hloc) From 02130cf57cd2bf3763096b1139921ee5d7e0ab3d Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Sun, 18 Dec 2022 14:50:55 +0100 Subject: [PATCH 19/50] Rename `maybeprint` to `print_if_any` to precise the purpose of this function --- src/cprint.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index a36ca3e..d030c24 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -11,7 +11,7 @@ let rec cp_includes fmt = function Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t let cp_node_state fmt (st: node_state) = - let maybeprint fmt (ty, nb, name): unit = + let print_if_any fmt (ty, nb, name): unit = if nb = 0 then () else Format.fprintf fmt "\n\t%s %s[%d];" ty name nb @@ -21,18 +21,18 @@ let cp_node_state fmt (st: node_state) = Format.fprintf fmt "typedef struct {%a%a%a\n\ \tbool is_init;\n\ } %s;\n\n" - maybeprint ("int", st.nt_nb_int, "ivars") - maybeprint ("bool", st.nt_nb_bool, "bvars") - maybeprint ("double", st.nt_nb_real, "rvars") + print_if_any ("int", st.nt_nb_int, "ivars") + print_if_any ("bool", st.nt_nb_bool, "bvars") + print_if_any ("double", st.nt_nb_real, "rvars") st.nt_name else Format.fprintf fmt "typedef struct {%a%a%a\n\ \tbool is_init;\n\ \tvoid* aux_states[%d]; /* stores the states of auxiliary nodes */\n\ } %s;\n\n" - maybeprint ("int", st.nt_nb_int, "ivars") - maybeprint ("bool", st.nt_nb_bool, "bvars") - maybeprint ("double", st.nt_nb_real, "rvars") + print_if_any ("int", st.nt_nb_int, "ivars") + print_if_any ("bool", st.nt_nb_bool, "bvars") + print_if_any ("double", st.nt_nb_real, "rvars") st.nt_count_app st.nt_name let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = @@ -50,7 +50,7 @@ let cp_var fmt = function | RVar s -> Format.fprintf fmt "double %s" s let rec cp_varlist' fmt vl = - let maybeprint fmt = function + let print_if_any fmt = function | [] -> () | _ :: _ -> Format.fprintf fmt ", " in @@ -59,11 +59,11 @@ let rec cp_varlist' fmt vl = | v :: vl -> Format.fprintf fmt "%a%a%a" cp_var' v - maybeprint vl + print_if_any vl cp_varlist' vl let rec cp_varlist fmt vl = - let maybeprint fmt = function + let print_if_any fmt = function | [] -> () | _ :: _ -> Format.fprintf fmt ", " in @@ -72,7 +72,7 @@ let rec cp_varlist fmt vl = | v :: vl -> Format.fprintf fmt "%a%a%a" cp_var v - maybeprint vl + print_if_any vl cp_varlist vl let cp_prototype fmt (node, h): unit = From 77c865e36084672c2421e007e7c4b821e9f549c8 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Sun, 18 Dec 2022 17:25:34 +0100 Subject: [PATCH 20/50] [intermediate_ast] remove unused fields of i_nodes --- src/ast_to_c.ml | 3 --- src/intermediate_ast.ml | 3 --- 2 files changed, 6 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 746e2a8..9edace9 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -181,9 +181,6 @@ let make_state_types nodes: node_states = nt_nb_int = nb_int_vars; nt_nb_bool = nb_bool_vars; nt_nb_real = nb_real_vars; - nt_map_int = h_int; - nt_map_bool = h_bool; - nt_map_real = h_real; nt_map = h_map; nt_output_map = h_out; nt_prevars = pv; diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index e259596..33aefdc 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -29,9 +29,6 @@ type node_state = nt_nb_int : int; nt_nb_real: int; nt_nb_bool: int; - nt_map_int: (ident * bool, int) Hashtbl.t; - nt_map_bool: (ident * bool, int) Hashtbl.t; - nt_map_real: (ident * bool, int) Hashtbl.t; nt_map: (ident * bool, string * int) Hashtbl.t; nt_output_map: (int, string * int) Hashtbl.t; nt_prevars: t_var list; From aa7f7514d35a8195226ce30ccb3ea90c71cb7b85 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Sun, 18 Dec 2022 17:36:10 +0100 Subject: [PATCH 21/50] [Lustre -> intermediate] fix for the [pre] construct --- src/ast_to_c.ml | 7 +++++-- src/test.node | 5 +---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 9edace9..bca0ea2 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -14,11 +14,14 @@ let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist = let ast_to_intermediate_ast_varlist vl = snd vl in let rec ast_to_intermediate_ast_expr hloc = function | EVar (_, v) -> - begin + begin match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with | None -> IEVar (CVInput (name_of_var v)) | Some (s, i) -> IEVar (CVStored (s, i)) - end + end + | EMonOp (_, MOp_pre, EVar (_, v)) -> + let s, i = Hashtbl.find hloc (Utils.name_of_var v, true) in + IEVar (CVStored (s, i)) | EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e) | EBinOp (_, op, e, e') -> IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') diff --git a/src/test.node b/src/test.node index f6054ee..5fb4a8f 100644 --- a/src/test.node +++ b/src/test.node @@ -1,9 +1,6 @@ node n (i: int) returns (o: int); -var v, t: int; a, b: bool; +var v: int; let - a = true -> false; - b = a and not (pre a); o = 1; v = pre o; - t = o + pre i; tel From c344f125e55384d9f9f78c572d14f2c107046437 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Sun, 18 Dec 2022 19:00:24 +0100 Subject: [PATCH 22/50] [passes] linearization of tuple-equations + deletion of unused pass --- src/main.ml | 11 ++-- src/passes.ml | 138 +++++++++++--------------------------------------- src/test.node | 12 +++-- 3 files changed, 42 insertions(+), 119 deletions(-) diff --git a/src/main.ml b/src/main.ml index 78e1dc1..8c0fc97 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 main_fn verbose debug passes f = +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 main_fn ast with + 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); @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = [] in + let default_passes = ["linearization_tuples"; "linearization"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -57,13 +57,12 @@ 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" in (** Definition of the passes table *) let passes_table = Hashtbl.create 100 in List.iter (fun (s, k) -> Hashtbl.add passes_table s k) [ - ("pre2vars", Passes.pre2vars); + ("linearization_tuples", Passes.pass_linearization_tuples); ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); @@ -120,7 +119,7 @@ let _ = print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" Lustre_pp.pp_ast ast) ; - exec_passes ast main_fn print_verbose print_debug passes + exec_passes ast print_verbose print_debug passes begin if !ppast then (Format.printf "%a" Lustre_pp.pp_ast) diff --git a/src/passes.ml b/src/passes.ml index 179242f..4cc32fe 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -4,88 +4,29 @@ open Ast open Passes_utils open Utils -let pre2vars verbose debug main_fn = - let rec all_pre expr = - match expr with - | EMonOp (ty, MOp_pre, expr) -> all_pre expr - | EMonOp _ -> false - | EVar _ -> true - | _ -> false - in - let rec pre_push expr : t_expression = - match expr with - | 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 (somify aux) +let rec split_tuple (eq: t_equation): t_eqlist = + let patt, expr = eq in + match expr with + | ETuple (_, expr_h :: expr_t) -> + begin + let t_l = type_exp expr_h in + let patt_l, patt_r = list_select (List.length t_l) (snd patt) in + let t_r = List.flatten (List.map type_var patt_r) in + ((t_l, patt_l), expr_h) :: + split_tuple ((t_r, patt_r), ETuple (t_r, expr_t)) + end + | ETuple (_, []) -> [] + | _ -> [eq] -let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option = + +let pass_linearization_tuples verbose debug = + let aux_linearization_tuples node = + let new_equations = List.flatten (List.map split_tuple node.n_equations) in + Some { node with n_equations = new_equations } + in + node_pass aux_linearization_tuples + +let chkvar_init_unicity verbose debug : 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 @@ -171,7 +112,7 @@ let rec tpl debug ((pat, exp): t_equation) = | ETuple (_, []) -> [] | _ -> [(pat, exp)] -let pass_linearization verbose debug main_fn = +let pass_linearization verbose debug = let node_lin (node: t_node): t_node option = let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = match expr with @@ -237,34 +178,13 @@ let pass_linearization verbose debug main_fn = let eqs, vars, expr = pre_aux_expression vars expr in (patt, expr)::eqs, vars in - 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 - let new_equations = List.flatten - (List.map - tpl - node.n_equations) - in let new_equations, new_locvars = List.fold_left (fun (eqs, vars) eq -> let es, vs = pre_aux_equation vars eq in es @ eqs, vs) ([], node.n_local_vars) - new_equations + node.n_equations in Some { @@ -278,7 +198,7 @@ let pass_linearization verbose debug main_fn = in node_pass node_lin -let pass_eq_reordering verbose debug main_fn ast = +let pass_eq_reordering verbose debug ast = let rec pick_equations init_vars eqs remaining_equations = match remaining_equations with | [] -> Some eqs @@ -312,7 +232,7 @@ let pass_eq_reordering verbose debug main_fn ast = in node_pass node_eq_reorganising ast -let pass_typing verbose debug main_fn ast = +let pass_typing verbose debug ast = let htbl = Hashtbl.create (List.length ast) in let () = debug "[typing verification]" in let () = List.iter @@ -382,7 +302,7 @@ let pass_typing verbose debug main_fn ast = else None in aux ast -let check_automata_validity verbos debug main_fn = +let check_automata_validity verbos debug = let check_automaton_branch_vars automaton = let (init, states) = automaton in let left_side = Hashtbl.create 10 in @@ -539,10 +459,10 @@ let automata_trans_pass debug (node:t_node) : t_node option= n_automata = []; (* not needed anymore *) } -let automata_translation_pass verbose debug main_fn = +let automata_translation_pass verbose debug = node_pass (automata_trans_pass debug) -let clock_unification_pass verbose debug main_fn ast = +let clock_unification_pass verbose debug ast = let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in diff --git a/src/test.node b/src/test.node index 5fb4a8f..faa8355 100644 --- a/src/test.node +++ b/src/test.node @@ -1,6 +1,10 @@ -node n (i: int) returns (o: int); -var v: int; +node my_and (a, b: bool) returns (o: bool); let - o = 1; - v = pre o; + o = a and b; +tel + +node n (i: int) returns (o: int); +var v: bool; +let + (o, v) = (1, my_and (pre o = 8, pre v)); tel From c52dce6c025ae92ebb9a779ee642c4cdb32a727d Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Sun, 18 Dec 2022 22:34:07 +0100 Subject: [PATCH 23/50] [passes] linearization: done for app, tuples (lvl 1 behind when) and pre --- src/main.ml | 6 ++- src/passes.ml | 101 ++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 101 insertions(+), 6 deletions(-) diff --git a/src/main.ml b/src/main.ml index 8c0fc97..4a46502 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,8 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["linearization_tuples"; "linearization"] in + let default_passes = ["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] \ @@ -63,10 +64,11 @@ let _ = List.iter (fun (s, k) -> Hashtbl.add passes_table s k) [ ("linearization_tuples", Passes.pass_linearization_tuples); + ("linearization_app", Passes.pass_linearization_app); + ("linearization_pre", Passes.pass_linearization_pre); ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); - ("linearization", Passes.pass_linearization); ("equations_ordering", Passes.pass_eq_reordering); ("check_typing", Passes.pass_typing); ("clock_unification", Passes.clock_unification_pass); diff --git a/src/passes.ml b/src/passes.ml index 4cc32fe..4a47113 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -18,14 +18,107 @@ let rec split_tuple (eq: t_equation): t_eqlist = | ETuple (_, []) -> [] | _ -> [eq] - let pass_linearization_tuples verbose debug = let aux_linearization_tuples node = - let new_equations = List.flatten (List.map split_tuple node.n_equations) in + let new_equations = List.flatten + (List.map + (fun eq -> + match snd eq with + | ETuple _ -> split_tuple eq + | EWhen (t, ETuple (_, l), e') -> + List.map + (fun (patt, expr) -> (patt, EWhen (type_exp expr, expr, e'))) + (split_tuple (fst eq, ETuple (t, l))) + | _ -> [eq]) + node.n_equations) in Some { node with n_equations = new_equations } in node_pass aux_linearization_tuples +let pass_linearization_app verbose debug = + let applin_count = ref 0 in + let rec aux_expr vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EConst _ | EVar _ -> [], vars, expr + | EMonOp (t, op, expr) -> + let eqs, vars, expr = aux_expr vars expr in + eqs, vars, EMonOp (t, op, expr) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = aux_expr vars e in + let eqs', vars, e' = aux_expr vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = aux_expr vars e in + let eqs', vars, e' = aux_expr vars e' in + let eqs'', vars, e'' = aux_expr vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = aux_expr vars e in + let eqs', vars, e' = aux_expr vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = aux_expr vars e in + let eqs', vars, e' = aux_expr vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = aux_expr vars e in + let eqs', vars, e' = aux_expr vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | ETuple (t, l) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (tout, n, ETuple (tin, l)) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr vars e in + match e with + | EVar _ | EMonOp (_, MOp_pre, _) -> (** No need for a new var. *) + eqs' @ eqs, vars, (e :: l) + | _ -> (** Need for a new var. *) + let ty = match type_exp e with + | [ty] -> ty + | _ -> failwith "[passes.ml] One should not provide + tuples as arguments to an auxiliary node." + in + let nvar: string = Format.sprintf "_applin%d" !applin_count in + incr applin_count; + let nvar: t_var = + match ty with + | TBool -> BVar nvar + | TInt -> IVar nvar + | TReal -> RVar nvar + in + let neq_patt: t_varlist = ([ty], [nvar]) in + let neq_expr: t_expression = e in + let vars = varlist_concat neq_patt vars in + (neq_patt, neq_expr)::eqs'@eqs, vars, EVar([ty], nvar) :: l) + l ([], vars, []) in + 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 + 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) + ([], node.n_local_vars) + node.n_equations + in + Some { node with n_local_vars = new_locvars; n_equations = new_equations } + 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 = @@ -112,7 +205,7 @@ let rec tpl debug ((pat, exp): t_equation) = | ETuple (_, []) -> [] | _ -> [(pat, exp)] -let pass_linearization verbose debug = +let pass_linearization_pre verbose debug = let node_lin (node: t_node): t_node option = let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = match expr with @@ -140,7 +233,7 @@ let pass_linearization verbose debug = let eqs, vars, e = pre_aux_expression vars e in let eqs', vars, e' = pre_aux_expression vars e' in eqs @ eqs', vars, EBinOp (t, op, e, e') - | ETriOp (t, op, e, e', e'') -> + | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here ? *) let eqs, vars, e = pre_aux_expression vars e in let nvar: string = fresh_var_name vars 6 in let nvar: t_var = BVar nvar in From 4ff193759bd8651161205dfdcad3c3736524a1e4 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 11:22:16 +0100 Subject: [PATCH 24/50] [passes] removal of constructs: seems ok --- src/cprint.ml | 2 +- src/ctranslation.ml | 3 +- src/main.ml | 3 +- src/passes.ml | 181 ++++++++++++++++++++++++++++++++++++++++---- src/test.node | 14 ++-- src/utils.ml | 6 ++ 6 files changed, 184 insertions(+), 25 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index d030c24..e1e25c6 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -163,7 +163,7 @@ and cp_expression fmt (expr, hloc) = Format.fprintf fmt "%sstate->%s[%d] = %a;\n" prefix arr idx cp_value (value, hloc) end - | CAssign (CVInput _, _) -> failwith "should not happened." + | CAssign (CVInput _, _) -> failwith "[cprint.ml] never assign an input." | CSeq (e, e') -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 48af417..b9a7997 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -67,7 +67,8 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = vl in CApplication (node.n_name,i , al, vl, node_sts) - | IETuple _ -> failwith "[ctranslation.ml] linearization should have transformed you." + | IETuple _ -> failwith "[ctranslation.ml] linearization should have \ + transformed the tuples of the right members." | IEWhen (expr, cond) -> begin CIf (iexpression_to_cvalue cond, diff --git a/src/main.ml b/src/main.ml index 4a46502..83d407f 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,7 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["linearization_pre"; "linearization_tuples"; "linearization_app"; + 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 = @@ -63,6 +63,7 @@ let _ = let passes_table = Hashtbl.create 100 in List.iter (fun (s, k) -> Hashtbl.add passes_table s k) [ + ("remove_if", Passes.pass_if_removal); ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); diff --git a/src/passes.ml b/src/passes.ml index 4a47113..352bb65 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -4,21 +4,156 @@ open Ast open Passes_utils open Utils -let rec split_tuple (eq: t_equation): t_eqlist = - let patt, expr = eq in - match expr with - | ETuple (_, expr_h :: expr_t) -> - begin - let t_l = type_exp expr_h in - let patt_l, patt_r = list_select (List.length t_l) (snd patt) in - let t_r = List.flatten (List.map type_var patt_r) in - ((t_l, patt_l), expr_h) :: - split_tuple ((t_r, patt_r), ETuple (t_r, expr_t)) - end - | ETuple (_, []) -> [] - | _ -> [eq] +(** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones. + * + * [x1, ..., xn = if c then e_l else e_r;] + * is replaced by: + * (t1, ..., tn) = e_l; + * (u1, ..., un) = e_r; + * (v1, ..., vn) = (t1, ..., tn) when c; + * (w1, ..., wn) = (u1, ..., un) when (not c); + * (x1, ..., xn) = merge c (v1, ..., vn) (w1, ..., wn); + * + * Note that the first two equations (before the use of when) is required in + * order to have the expressions active at each step. + *) +let pass_if_removal verbose debug = + let varcount = ref 0 in + let make_patt t: t_varlist = + (t, List.fold_right + (fun ty acc -> + let nvar: ident = Format.sprintf "_ifrem%d" !varcount in + let nvar = + match ty with + | TInt -> IVar nvar + | TReal -> RVar nvar + | TBool -> BVar nvar + in + incr varcount; + nvar :: acc) + t []) + in + let simplify_tuple t = + match t with + | ETuple (t, [elt]) -> elt + | _ -> t + in + let rec aux_eq vars eq: t_eqlist * t_varlist * t_equation = + let patt, expr = eq in + match expr with + | EConst _ | EVar _ -> [], vars, eq + | EMonOp (t, op, e) -> + let eqs, vars, (patt, e) = aux_eq vars (patt, e) in + eqs, vars, (patt, EMonOp (t, op, e)) + | EBinOp (t, op, e, e') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + eqs @ eqs', vars, (patt, EBinOp (t, op, e, e')) + | ETriOp (t, TOp_if, e, e', e'') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + let eqs'', vars, (_, e'') = aux_eq vars (patt, e'') in + let patt_l: t_varlist = make_patt t in + let patt_r: t_varlist = make_patt t in + let patt_l_when: t_varlist = make_patt t in + let patt_r_when: t_varlist = make_patt t in + let expr_l: t_expression = + simplify_tuple + (ETuple + (fst patt_l, List.map (fun v -> EVar (type_var v, v)) (snd patt_l))) + in + let expr_r: t_expression = + simplify_tuple + (ETuple + (fst patt_r, List.map (fun v -> EVar (type_var v, v)) (snd patt_r))) + in + let expr_l_when: t_expression = + simplify_tuple + (ETuple + (fst patt_l_when, List.map (fun v -> EVar (type_var v, v)) + (snd patt_l_when))) + in + let expr_r_when: t_expression = + simplify_tuple + (ETuple + (fst patt_r_when, List.map (fun v -> EVar (type_var v, v)) + (snd patt_r_when))) + in + let equations: t_eqlist = + [(patt_l, e'); + (patt_r, e''); + (patt_l_when, + EWhen (t, expr_l, e)); + (patt_r_when, + EWhen (t, + expr_r, + (EMonOp (type_exp e, MOp_not, e))))] + @ eqs @ eqs' @eqs'' in + let vars: t_varlist = + varlist_concat + vars + (varlist_concat patt_l_when (varlist_concat patt_r_when + (varlist_concat patt_r patt_l))) in + let expr = + ETriOp (t, TOp_merge, e, expr_l_when, expr_r_when) in + equations, vars, (patt, expr) + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + let eqs'', vars, (_, e'') = aux_eq vars (patt, e'') in + eqs @ eqs' @ eqs'', vars, (patt, ETriOp (t, op, e, e', e'')) + | EComp (t, op, e, e') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + eqs @ eqs', vars, (patt, EComp (t, op, e, e')) + | EWhen (t, e, e') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + eqs @ eqs', vars, (patt, EWhen (t, e, e')) + | EReset (t, e, e') -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + let eqs', vars, (_, e') = aux_eq vars (patt, e') in + eqs @ eqs', vars, (patt, EReset (t, e, e')) + | ETuple (t, l) -> + let eqs, vars, l, _ = + List.fold_right + (fun e (eqs, vars, l, remaining_patt) -> + let patt_l, patt_r = split_patt remaining_patt e in + let eqs', vars, (_, e) = aux_eq vars (patt_l, e) in + eqs' @ eqs, vars, (e :: l), patt_r) + l ([], vars, [], patt) in + eqs, vars, (patt, ETuple (t, l)) + | EApp (t, n, e) -> + let eqs, vars, (_, e) = aux_eq vars (patt, e) in + eqs, vars, (patt, EApp (t, n, e)) + in + let aux_if_removal node = + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, eq = aux_eq vars eq in + eq :: eqs' @ eqs, vars) + ([], node.n_local_vars) node.n_equations + in + Some { node with n_equations = new_equations; n_local_vars = new_locvars } + in + node_pass aux_if_removal -let pass_linearization_tuples verbose debug = +let pass_linearization_tuples verbose debug ast = + let rec split_tuple (eq: t_equation): t_eqlist = + let patt, expr = eq in + match expr with + | ETuple (_, expr_h :: expr_t) -> + begin + let t_l = type_exp expr_h in + let patt_l, patt_r = list_select (List.length t_l) (snd patt) in + let t_r = List.flatten (List.map type_var patt_r) in + ((t_l, patt_l), expr_h) :: + split_tuple ((t_r, patt_r), ETuple (t_r, expr_t)) + end + | ETuple (_, []) -> [] + | _ -> [eq] + in let aux_linearization_tuples node = let new_equations = List.flatten (List.map @@ -29,11 +164,27 @@ let pass_linearization_tuples verbose debug = List.map (fun (patt, expr) -> (patt, EWhen (type_exp expr, expr, e'))) (split_tuple (fst eq, ETuple (t, l))) + | ETriOp (t, TOp_merge, c, ETuple (_, l), ETuple (_, l')) -> + begin + if List.length l <> List.length l' + || List.length t <> List.length (snd (fst eq)) + then raise (PassExn "Error while merging tuples.") + else + fst + (List.fold_left2 + (fun (eqs, remaining_patt) el er -> + let patt, remaining_patt = split_patt remaining_patt el in + let t = type_exp el in + (patt, ETriOp (t, TOp_merge, c, el, er)) + :: eqs, remaining_patt) + ([], fst eq) l l') + end | _ -> [eq]) node.n_equations) in Some { node with n_equations = new_equations } in - node_pass aux_linearization_tuples + try node_pass aux_linearization_tuples ast with + | PassExn err -> (debug err; None) let pass_linearization_app verbose debug = let applin_count = ref 0 in diff --git a/src/test.node b/src/test.node index faa8355..6dd535f 100644 --- a/src/test.node +++ b/src/test.node @@ -1,10 +1,10 @@ -node my_and (a, b: bool) returns (o: bool); +node test_merge_tuples (a, b: bool) returns (o: bool); +var t: bool; let - o = a and b; + (o, t) = if a and b then (true, false) else (false, true); tel -node n (i: int) returns (o: int); -var v: bool; -let - (o, v) = (1, my_and (pre o = 8, pre v)); -tel +--node my_and (a, b: bool) returns (o: bool); +--let +-- o = if a then b else false; +--tel diff --git a/src/utils.ml b/src/utils.ml index 01312ef..8005e46 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -104,3 +104,9 @@ let rec vars_of_expr (expr: t_expression) : ident list = let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist = (fst l1 @ fst l2, snd l1 @ snd l2) +let split_patt (patt: t_varlist) (e: t_expression): t_varlist * t_varlist = + let pl, pr = list_select (List.length (type_exp e)) (snd patt) in + let tl = List.flatten (List.map type_var pl) in + let tr = List.flatten (List.map type_var pr) in + (tl, pl), (tr, pr) + From 1d39173e94067f9bb852c68dc56ef27542d39507 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 12:07:43 +0100 Subject: [PATCH 25/50] [general] useless fn removed in pass_linearization_app + comments + print_debug in ast_to_c --- src/ast_to_c.ml | 23 ++++++++++---------- src/main.ml | 41 ++++++++++++++++++++++++++++------- src/passes.ml | 57 +++++++++++++++++++++++++++++++++++++++---------- src/test.node | 13 +++++++---- 4 files changed, 99 insertions(+), 35 deletions(-) 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 From 249ac379342a53db8af39014ff5b289d432e9a49 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 12:18:21 +0100 Subject: [PATCH 26/50] [general] renaming, comments and removal of unused function in [pass_linearization_pre] --- src/main.ml | 4 +- src/passes.ml | 188 ++++++++++++++++++++++++++------------------------ 2 files changed, 99 insertions(+), 93 deletions(-) diff --git a/src/main.ml b/src/main.ml index 3711c06..db2008f 100644 --- a/src/main.ml +++ b/src/main.ml @@ -47,7 +47,7 @@ let _ = ["remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; "equations_ordering"] in - let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in + let sanity_passes = ["sanity_pass_assignment_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 @@ -87,7 +87,7 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); - ("chkvar_init_unicity", Passes.chkvar_init_unicity); + ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); ("equations_ordering", Passes.pass_eq_reordering); diff --git a/src/passes.ml b/src/passes.ml index 0566934..23749f6 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -148,6 +148,95 @@ let pass_if_removal verbose debug = +(** [pass_linearization_pre] makes sure that all pre constructs in the program + * are applied to variables. + * This is required, since the pre construct is translated into a variable in + * the final C code. *) +let pass_linearization_pre verbose debug = + (** [node_lin] linearises a single node. *) + let node_lin (node: t_node): t_node option = + (** [pre_aux_expression] takes an expression and returns: + * - a list of additional equations + * - the new list of local variables + * - an updated version of the original expression *) + let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + begin + 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 + | [TInt] -> IVar nvar + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | _ -> failwith "Should not happened." in + let neq_patt: t_varlist = (t, [nvar]) in + 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 + | EBinOp (t, op, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here ? *) + let eqs, vars, e = pre_aux_expression vars e in + let nvar: string = fresh_var_name vars 6 in + let nvar: t_var = BVar nvar in + let neq_patt: t_varlist = ([TBool], [nvar]) in + let neq_expr: t_expression = e in + let vars = varlist_concat vars (neq_patt) in + let eqs', vars, e' = pre_aux_expression vars e' in + let eqs'', vars, e'' = pre_aux_expression vars e'' in + (neq_patt, neq_expr) :: eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | EConst _ -> [], vars, expr + | ETuple (t, l) -> + let eqs, vars, l = List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = pre_aux_expression vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = pre_aux_expression vars e in + eqs, vars, EApp (t, n, e) + in + (** Applies the previous function to the expressions of every equation. *) + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, expr = pre_aux_expression vars expr in + (patt, expr)::eqs' @ eqs, vars) + ([], node.n_local_vars) + node.n_equations + in + Some { node with n_local_vars = new_locvars; n_equations = new_equations } + in + node_pass node_lin + + + (** [pass_linearization_tuples] transforms expressions of the form * (x1, ..., xn) = (e1, ..., em); * into: @@ -302,11 +391,17 @@ let pass_linearization_app verbose debug = -let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option = +(** [sanity_pass_assignment_unicity] makes sure that there is at most one + * equation defining each variable (and that no equation tries to redefine an + * input). + * + * This is required, since the equations are not ordered in Lustre. *) +let sanity_pass_assignment_unicity verbose debug : t_nodelist -> t_nodelist option = + (** For each node, test the node. *) let aux (node: t_node) : t_node option = let incr_aux h n = match Hashtbl.find_opt h n with - | None -> raise (PassExn "todo, should not happened.") + | None -> raise (PassExn "should not happened.") | Some num -> Hashtbl.replace h n (num + 1) in let incr_eq h (((_, patt), _): t_equation) = @@ -388,95 +483,6 @@ let rec tpl debug ((pat, exp): t_equation) = | ETuple (_, []) -> [] | _ -> [(pat, exp)] -let pass_linearization_pre verbose debug = - let node_lin (node: t_node): t_node option = - let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = - match expr with - | EVar _ -> [], vars, expr - | EMonOp (t, op, e) -> - begin - 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 - | [TInt] -> IVar nvar - | [TBool] -> BVar nvar - | [TReal] -> RVar nvar - | _ -> failwith "Should not happened." in - let neq_patt: t_varlist = (t, [nvar]) in - 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 - | EBinOp (t, op, e, e') -> - let eqs, vars, e = pre_aux_expression vars e in - let eqs', vars, e' = pre_aux_expression vars e' in - eqs @ eqs', vars, EBinOp (t, op, e, e') - | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here ? *) - let eqs, vars, e = pre_aux_expression vars e in - let nvar: string = fresh_var_name vars 6 in - let nvar: t_var = BVar nvar in - let neq_patt: t_varlist = ([TBool], [nvar]) in - let neq_expr: t_expression = e in - let vars = varlist_concat vars (neq_patt) in - let eqs', vars, e' = pre_aux_expression vars e' in - let eqs'', vars, e'' = pre_aux_expression vars e'' in - (neq_patt, neq_expr) :: eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') - | EComp (t, op, e, e') -> - let eqs, vars, e = pre_aux_expression vars e in - let eqs', vars, e' = pre_aux_expression vars e' in - eqs @ eqs', vars, EComp (t, op, e, e') - | EWhen (t, e, e') -> - let eqs, vars, e = pre_aux_expression vars e in - let eqs', vars, e' = pre_aux_expression vars e' in - eqs @ eqs', vars, EWhen (t, e, e') - | EReset (t, e, e') -> - let eqs, vars, e = pre_aux_expression vars e in - let eqs', vars, e' = pre_aux_expression vars e' in - eqs @ eqs', vars, EReset (t, e, e') - | EConst _ -> [], vars, expr - | ETuple (t, l) -> - let eqs, vars, l = List.fold_right - (fun e (eqs, vars, l) -> - let eqs', vars, e = pre_aux_expression vars e in - eqs' @ eqs, vars, (e :: l)) - l ([], vars, []) in - eqs, vars, ETuple (t, l) - | EApp (t, n, e) -> - let eqs, vars, e = pre_aux_expression vars e in - eqs, vars, EApp (t, n, e) - in - let rec pre_aux_equation (vars: t_varlist) ((patt, expr): t_equation) = - let eqs, vars, expr = pre_aux_expression vars expr in - (patt, expr)::eqs, vars - in - let new_equations, new_locvars = - List.fold_left - (fun (eqs, vars) eq -> - let es, vs = pre_aux_equation vars eq in - es @ eqs, vs) - ([], node.n_local_vars) - node.n_equations - 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 ast = let rec pick_equations init_vars eqs remaining_equations = match remaining_equations with From 906a3d948b334172e02381ea7af4cbd40aa84abc Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 12:20:03 +0100 Subject: [PATCH 27/50] [oups] forgot a pattern matching --- src/passes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/passes.ml b/src/passes.ml index 23749f6..43d0e94 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -225,7 +225,7 @@ let pass_linearization_pre verbose debug = (** Applies the previous function to the expressions of every equation. *) let new_equations, new_locvars = List.fold_left - (fun (eqs, vars) eq -> + (fun (eqs, vars) (patt, expr) -> let eqs', vars, expr = pre_aux_expression vars expr in (patt, expr)::eqs' @ eqs, vars) ([], node.n_local_vars) From 609870755c62f99f2f145a1c9a93aa1faaf09d58 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Mon, 19 Dec 2022 13:56:48 +0100 Subject: [PATCH 28/50] Remove debugging symbols in `failwith` As running `OCAMLRUNPARAM=b ./_build/main.native ...` provides in case of `failwith` a better stacktrace. This enables moving `failwith`s from a file to the other without adapting them. --- src/cprint.ml | 10 +++++----- src/ctranslation.ml | 14 +++++++------- src/main.ml | 2 +- src/passes.ml | 4 ++-- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index e1e25c6..484f2ca 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -105,7 +105,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | BOp_mod -> "%" | BOp_and -> "&&" | BOp_or -> "||" - | BOp_arrow -> failwith "[cprint.ml] string_of_binop undefined on (->)" + | BOp_arrow -> failwith "string_of_binop undefined on (->)" in let string_of_compop = function | COp_eq -> "==" @@ -128,7 +128,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CVStored (arr, idx) -> begin match find_varname hloc (arr, idx) with - | None -> failwith "[cprint.ml] This varname should be defined." + | None -> failwith "This varname should be defined." | Some (n, _) -> n end | CVInput n -> n) in @@ -144,7 +144,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = Format.fprintf fmt "(%a) %s (%a)" cp_value (v, hloc) (string_of_compop op) cp_value (v', hloc) | CMonOp (MOp_pre, _) -> - failwith "[cprint.ml] The linearization should have removed this case." + failwith "The linearization should have removed this case." let prefix_ = ref "\t" @@ -163,7 +163,7 @@ and cp_expression fmt (expr, hloc) = Format.fprintf fmt "%sstate->%s[%d] = %a;\n" prefix arr idx cp_value (value, hloc) end - | CAssign (CVInput _, _) -> failwith "[cprint.ml] never assign an input." + | CAssign (CVInput _, _) -> failwith "never assign an input." | CSeq (e, e') -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) @@ -186,7 +186,7 @@ and cp_expression fmt (expr, hloc) = aux_node_st.nt_name (nb-1) arr' idx'; i+1 - | CVInput _ -> failwith "[cprint.ml] Impossible!") + | CVInput _ -> failwith "Impossible!") 0 destl in () end | CIf (v, b1, []) -> diff --git a/src/ctranslation.ml b/src/ctranslation.ml index b9a7997..41a3f55 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -15,7 +15,7 @@ let rec iexpression_to_cvalue e = | IEReset _ | IETuple _ | IEApp _ - | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." + | IETriOp _ -> failwith "Should not happened." let rec equation_to_expression (node_st, node_sts, (vl, expr)) = let hloc = node_st.nt_map in @@ -27,7 +27,7 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = | None -> CVInput (Utils.name_of_var v) | Some (arr, idx) -> CVStored (arr, idx) end - | _ -> failwith "[ctranslation.ml] This should not happened." + | _ -> failwith "This should not happened." in match expr with | IEVar vsrc -> @@ -54,9 +54,9 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = List.map (function | IEVar v -> v - | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + | _ -> failwith "should not happened due to the linearization pass." ) l - | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + | _ -> failwith "should not happened due to the linearization pass." in let vl = List.map @@ -67,7 +67,7 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = vl in CApplication (node.n_name,i , al, vl, node_sts) - | IETuple _ -> failwith "[ctranslation.ml] linearization should have \ + | IETuple _ -> failwith "linearization should have \ transformed the tuples of the right members." | IEWhen (expr, cond) -> begin @@ -76,12 +76,12 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = []) end | IETriOp (TOp_if, _, _, _) -> - failwith "[ctranslation.ml] A pass should have turned conditionnals into merges." + failwith "A pass should have turned conditionnals into merges." | IETriOp (TOp_merge, c, e, e') -> CIf (iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, e))], [equation_to_expression (node_st, node_sts, (vl, e'))]) - | IEReset _ -> failwith "[ctranslation.ml] A pass should have removed resets." + | IEReset _ -> failwith "A pass should have removed resets." diff --git a/src/main.ml b/src/main.ml index db2008f..f7fe8c8 100644 --- a/src/main.ml +++ b/src/main.ml @@ -35,7 +35,7 @@ let exec_passes ast verbose debug passes f = "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!") + | _ -> failwith ("The pass "^n^" should have catched me!") in aux ast passes diff --git a/src/passes.ml b/src/passes.ml index 43d0e94..c303cc0 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -356,7 +356,7 @@ let pass_linearization_app verbose debug = | _ -> (** Need for a new var. *) let ty = match type_exp e with | [ty] -> ty - | _ -> failwith "[passes.ml] One should not provide + | _ -> failwith "One should not provide tuples as arguments to an auxiliary node." in let nvar: string = Format.sprintf "_applin%d" !applin_count in @@ -373,7 +373,7 @@ let pass_linearization_app verbose debug = (neq_patt, neq_expr)::eqs'@eqs, vars, EVar([ty], nvar) :: l) l ([], vars, []) in eqs, vars, EApp (tout, n, ETuple (tin, l)) - | EApp _ -> failwith "[passes.ml] Should not happened (parser)" + | EApp _ -> failwith "Should not happened (parser)" in (** [aux_linearization_app] applies the previous function to every equation *) let aux_linearization_app node = From 9a0bfd468cf143e137d613049e895a4660c87220 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Mon, 19 Dec 2022 14:06:18 +0100 Subject: [PATCH 29/50] Correct some typos --- src/ast_to_c.ml | 2 +- src/main.ml | 2 +- src/passes.ml | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 3e3bbe8..dbdbd5e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -291,7 +291,7 @@ let rec cp_nodes fmt (nodes, h) = (** [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"; + Format.fprintf fmt "Tables mapping the AST variables to the C variables:\n"; Hashtbl.iter (fun n st -> Format.fprintf fmt " ∗ NODE: %s\n" n; diff --git a/src/main.ml b/src/main.ml index f7fe8c8..da6fed1 100644 --- a/src/main.ml +++ b/src/main.ml @@ -35,7 +35,7 @@ let exec_passes ast verbose debug passes f = "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast); aux ast passes) end with - | _ -> failwith ("The pass "^n^" should have catched me!") + | _ -> failwith ("The pass "^n^" should have caught me!") in aux ast passes diff --git a/src/passes.ml b/src/passes.ml index c303cc0..4768751 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -21,7 +21,7 @@ open Utils *) let pass_if_removal verbose debug = let varcount = ref 0 in (** new variables are called «_ifrem[varcount]» *) - (** Males a pattern (t_varlist) of fresh variables matching the type t *) + (** Makes a pattern (t_varlist) of fresh variables matching the type t *) let make_patt t: t_varlist = (t, List.fold_right (fun ty acc -> @@ -153,7 +153,7 @@ let pass_if_removal verbose debug = * This is required, since the pre construct is translated into a variable in * the final C code. *) let pass_linearization_pre verbose debug = - (** [node_lin] linearises a single node. *) + (** [node_lin] linearizes a single node. *) let node_lin (node: t_node): t_node option = (** [pre_aux_expression] takes an expression and returns: * - a list of additional equations @@ -188,7 +188,7 @@ let pass_linearization_pre verbose debug = let eqs, vars, e = pre_aux_expression vars e in let eqs', vars, e' = pre_aux_expression vars e' in eqs @ eqs', vars, EBinOp (t, op, e, e') - | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here ? *) + | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here? *) let eqs, vars, e = pre_aux_expression vars e in let nvar: string = fresh_var_name vars 6 in let nvar: t_var = BVar nvar in From 9483f7df5e022587aa682fb6a2eea386eee0fd53 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 14:22:19 +0100 Subject: [PATCH 30/50] [c pass] merge neighbour conditionals (improved) --- src/ctranslation.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 41a3f55..2470737 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -96,8 +96,15 @@ let rec merge_neighbour_ifs = function | [] -> [] | [stmt] -> [stmt] | CIf (c, e1, e2) :: CIf (c', e'1, e'2) :: b -> - if c = c' - then merge_neighbour_ifs (CIf (c, e1 @ e'1, e2 @ e'2) :: b) - else (CIf (c, e1, e2)) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b) + begin + if c = c' then + merge_neighbour_ifs (CIf (c, e1 @ e'1, e2 @ e'2) :: b) + else if c = CMonOp (MOp_not, c') then + merge_neighbour_ifs (CIf (c, e1 @ e'2, e2 @ e'1) :: b) + else if c' = CMonOp (MOp_not, c) then + merge_neighbour_ifs (CIf (c, e1 @ e'2, e2 @ e'1) :: b) + else CIf (c, e1, e2) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b) + end | stmt :: stmt' :: b -> stmt :: merge_neighbour_ifs (stmt' :: b) + From 01d4a08e8aa3b974a36ce2d906be5931efdebb00 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 14:30:39 +0100 Subject: [PATCH 31/50] [c pass] idem --- src/ctranslation.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 2470737..9113c5b 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -98,11 +98,20 @@ let rec merge_neighbour_ifs = function | CIf (c, e1, e2) :: CIf (c', e'1, e'2) :: b -> begin if c = c' then - merge_neighbour_ifs (CIf (c, e1 @ e'1, e2 @ e'2) :: b) + merge_neighbour_ifs + (CIf (c, + merge_neighbour_ifs (e1 @ e'1), + merge_neighbour_ifs (e2 @ e'2)) :: b) else if c = CMonOp (MOp_not, c') then - merge_neighbour_ifs (CIf (c, e1 @ e'2, e2 @ e'1) :: b) + merge_neighbour_ifs + (CIf (c', + merge_neighbour_ifs (e2 @ e'1), + merge_neighbour_ifs (e1 @ e'2)) :: b) else if c' = CMonOp (MOp_not, c) then - merge_neighbour_ifs (CIf (c, e1 @ e'2, e2 @ e'1) :: b) + merge_neighbour_ifs + (CIf (c, + merge_neighbour_ifs (e1 @ e'2), + merge_neighbour_ifs (e2 @ e'1)) :: b) else CIf (c, e1, e2) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b) end | stmt :: stmt' :: b -> From e63123d8f6ed2372c8a5f8f132083c09b22104f6 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Mon, 19 Dec 2022 16:28:03 +0100 Subject: [PATCH 32/50] Move from the `x reset y` syntax to `reset x every y` one As described on https://www.di.ens.fr/~pouzet/cours/mpri/cours7/coiteration.pdf#page=4 --- src/lexer.mll | 1 + src/parser.mly | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lexer.mll b/src/lexer.mll index b11ee74..27bf17a 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -26,6 +26,7 @@ ("merge", TO_merge); ("when", WHEN); ("reset", RESET); + ("every", EVERY); ("pre", MO_pre); ("true", CONST_BOOL(true)); ("false", CONST_BOOL(false)); diff --git a/src/parser.mly b/src/parser.mly index f5b92d5..71bbc0b 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -144,6 +144,7 @@ %token WHEN %token RESET +%token EVERY %token IF %token THEN @@ -381,9 +382,9 @@ expr: then EWhen (t1, e1, e2) else raise (MyParsingError ("The when does not type-check!", current_location())) } - | expr RESET expr - { let e1 = $1 in let t1 = type_exp e1 in - let e2 = $3 in let t2 = type_exp e2 in + | RESET expr EVERY expr + { let e1 = $2 in let t1 = type_exp e1 in + let e2 = $4 in let t2 = type_exp e2 in if t2 = [TBool] then EReset (t1, e1, e2) else raise (MyParsingError ("The reset does not type-check!", From 10838d3f2d9f23427ce715997679e65c7b846477 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Mon, 19 Dec 2022 17:45:33 +0100 Subject: [PATCH 33/50] Remove `TODO` in `src/passes.ml:automaton_translation` As Antoine Grimod said that it was already done. --- src/passes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/passes.ml b/src/passes.ml index 4768751..c409846 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -698,7 +698,7 @@ let automaton_translation debug automaton = in let rec translate_var s v explist ty = match explist with - | [] -> default_constant ty (* TODO *) + | [] -> default_constant ty | (state, exp)::q -> ETriOp(Utils.type_exp exp, TOp_if, EComp([TBool], COp_eq, From 025d25a146fbce66d7c1d8ffb1bcf1e2516f1b84 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Mon, 19 Dec 2022 19:48:21 +0100 Subject: [PATCH 34/50] Replace `nunmbers` to `numbers` in two comments of `src/parser.mly` --- src/parser.mly | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index 71bbc0b..ef3504e 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -63,7 +63,7 @@ let make_binop_nonbool e1 e2 op error_msg = let t1 = type_exp e1 in let t2 = type_exp e2 in - (** e1 and e2 should be nunmbers here.*) + (** e1 and e2 should be numbers here.*) if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]] then begin @@ -88,7 +88,7 @@ let make_comp_nonbool e1 e2 op error_msg = let t1 = type_exp e1 in let t2 = type_exp e2 in - (** e1 and e2 should be nunmbers here.*) + (** e1 and e2 should be numbers here.*) if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]] then begin From 91ff654fc9cdab2dbb031a43befdba403101bbc7 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Mon, 19 Dec 2022 23:21:11 +0100 Subject: [PATCH 35/50] [passes] ensure that apps don't mix with operators --- src/main.ml | 2 ++ src/passes.ml | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+) diff --git a/src/main.ml b/src/main.ml index da6fed1..b9c677e 100644 --- a/src/main.ml +++ b/src/main.ml @@ -46,6 +46,7 @@ let _ = let default_passes = ["remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; + "ensure_assign_val"; "equations_ordering"] in let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in let usage_msg = @@ -87,6 +88,7 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); + ("ensure_assign_val", Passes.pass_ensure_assignment_value); ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); diff --git a/src/passes.ml b/src/passes.ml index c409846..ac498da 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -391,6 +391,79 @@ let pass_linearization_app verbose debug = +let pass_ensure_assignment_value verbose debug = + let varcount = ref 0 in + let rec aux_expr should_be_value vars expr = + match expr with + | EConst _ | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = aux_expr true vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + let eqs'', vars, e'' = aux_expr should_be_value vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | ETuple (t, l) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr true vars e in + eqs' @ eqs, vars, e :: l) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = aux_expr true vars e in + if should_be_value + then + let nvar = Format.sprintf "_assignval%d" !varcount in + incr varcount; + let nvar: t_var = + match t with + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | [TInt] -> IVar nvar + | _ -> + failwith "An application occurring here should return a single element." + in + let neq_patt: t_varlist = (t, [nvar]) in + let neq_expr: t_expression = EApp (t, n, e) in + let vars = varlist_concat neq_patt vars in + (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar) + else + eqs, vars, EApp (t, n, e) + in + let aux_ensure_assign_val node = + let new_equations, vars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, expr = aux_expr false vars (snd eq) in + (fst eq, expr) :: eqs' @ eqs, vars + ) + ([], node.n_local_vars) node.n_equations + in + Some { node with n_equations = new_equations; n_local_vars = vars } + in + node_pass aux_ensure_assign_val + + + (** [sanity_pass_assignment_unicity] makes sure that there is at most one * equation defining each variable (and that no equation tries to redefine an * input). From 657fe7e6fae3af61899547b55b262e5dcc3cf3b7 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 03:48:37 +0100 Subject: [PATCH 36/50] Add support for `reset`s --- src/cast.ml | 1 + src/cprint.ml | 8 +++ src/ctranslation.ml | 3 +- src/main.ml | 5 +- src/passes.ml | 140 ++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 155 insertions(+), 2 deletions(-) diff --git a/src/cast.ml b/src/cast.ml index 81b0672..d2ead4f 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -14,6 +14,7 @@ and c_expression = | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block | CApplication of ident * int * c_var list * c_var list * node_states + | CReset of ident * int * c_value * c_block (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 484f2ca..759c1c2 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -189,6 +189,14 @@ and cp_expression fmt (expr, hloc) = | CVInput _ -> failwith "Impossible!") 0 destl in () end + | CReset (node_name, i, v, b) -> + begin + Format.fprintf fmt "\tif (%a) {\n\t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\t}\n%a\n" + cp_value (v, hloc) + node_name + (i - 1) + cp_block (b, hloc) + end | CIf (v, b1, []) -> let p = prefix in prefix_ := prefix^"\t"; diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 9113c5b..6a2e3d5 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -81,7 +81,8 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = CIf (iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, e))], [equation_to_expression (node_st, node_sts, (vl, e'))]) - | IEReset _ -> failwith "A pass should have removed resets." + | IEReset (IEApp (i, node, b), c) -> CReset (node.n_name, i, iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, IEApp (i, node, b)))]) + | IEReset _ -> failwith "A pass should have turned not function resets into function resets" diff --git a/src/main.ml b/src/main.ml index da6fed1..7699020 100644 --- a/src/main.ml +++ b/src/main.ml @@ -44,8 +44,9 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) let default_passes = - ["remove_if"; + ["linearization_reset"; "remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; + "ensure_assign_val"; "equations_ordering"] in let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in let usage_msg = @@ -87,6 +88,8 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); + ("ensure_assign_val", Passes.pass_ensure_assignment_value); + ("linearization_reset", Passes.pass_linearization_reset); ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); diff --git a/src/passes.ml b/src/passes.ml index c409846..669c0ac 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -147,6 +147,73 @@ let pass_if_removal verbose debug = node_pass aux_if_removal +(** [pass_linearization_reset] makes sure that all reset constructs in the program + * are applied to functions. + * This is required, since the reset construct is translated into resetting the + * function state in the final C code. *) +let pass_linearization_reset verbose debug = + (** [node_lin] linearizes a single node. *) + let node_lin (node: t_node): t_node option = + (** [reset_aux_expression] takes an expression and returns: + * - a list of additional equations + * - the new list of local variables + * - an updated version of the original expression *) + let rec reset_aux_expression vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + let eqs'', vars, e'' = reset_aux_expression vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + ( + match e with + | EApp (t_app, n_app, e_app) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EReset (t, e, e') + | e -> reset_aux_expression vars e + ) + | EConst _ -> [], vars, expr + | ETuple (t, l) -> + let eqs, vars, l = List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = reset_aux_expression vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EApp (t, n, e) + in + (** Applies the previous function to the expressions of every equation. *) + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) (patt, expr) -> + let eqs', vars, expr = reset_aux_expression vars expr in + (patt, expr)::eqs' @ eqs, vars) + ([], node.n_local_vars) + node.n_equations + in + Some { node with n_local_vars = new_locvars; n_equations = new_equations } + in + node_pass node_lin + (** [pass_linearization_pre] makes sure that all pre constructs in the program * are applied to variables. @@ -391,6 +458,79 @@ let pass_linearization_app verbose debug = +let pass_ensure_assignment_value verbose debug = + let varcount = ref 0 in + let rec aux_expr should_be_value vars expr = + match expr with + | EConst _ | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = aux_expr true vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + let eqs'', vars, e'' = aux_expr should_be_value vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | ETuple (t, l) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr true vars e in + eqs' @ eqs, vars, e :: l) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = aux_expr true vars e in + if should_be_value + then + let nvar = Format.sprintf "_assignval%d" !varcount in + incr varcount; + let nvar: t_var = + match t with + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | [TInt] -> IVar nvar + | _ -> + failwith "An application occurring here should return a single element." + in + let neq_patt: t_varlist = (t, [nvar]) in + let neq_expr: t_expression = EApp (t, n, e) in + let vars = varlist_concat neq_patt vars in + (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar) + else + eqs, vars, EApp (t, n, e) + in + let aux_ensure_assign_val node = + let new_equations, vars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, expr = aux_expr false vars (snd eq) in + (fst eq, expr) :: eqs' @ eqs, vars + ) + ([], node.n_local_vars) node.n_equations + in + Some { node with n_equations = new_equations; n_local_vars = vars } + in + node_pass aux_ensure_assign_val + + + (** [sanity_pass_assignment_unicity] makes sure that there is at most one * equation defining each variable (and that no equation tries to redefine an * input). From e1de3e68297279d0b21f6d5584b002be1d143752 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 03:51:28 +0100 Subject: [PATCH 37/50] Add support for `reset`s --- src/cast.ml | 1 + src/cprint.ml | 8 +++ src/ctranslation.ml | 3 +- src/main.ml | 5 +- src/passes.ml | 140 ++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 155 insertions(+), 2 deletions(-) diff --git a/src/cast.ml b/src/cast.ml index 81b0672..d2ead4f 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -14,6 +14,7 @@ and c_expression = | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block | CApplication of ident * int * c_var list * c_var list * node_states + | CReset of ident * int * c_value * c_block (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 484f2ca..759c1c2 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -189,6 +189,14 @@ and cp_expression fmt (expr, hloc) = | CVInput _ -> failwith "Impossible!") 0 destl in () end + | CReset (node_name, i, v, b) -> + begin + Format.fprintf fmt "\tif (%a) {\n\t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\t}\n%a\n" + cp_value (v, hloc) + node_name + (i - 1) + cp_block (b, hloc) + end | CIf (v, b1, []) -> let p = prefix in prefix_ := prefix^"\t"; diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 9113c5b..6a2e3d5 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -81,7 +81,8 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = CIf (iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, e))], [equation_to_expression (node_st, node_sts, (vl, e'))]) - | IEReset _ -> failwith "A pass should have removed resets." + | IEReset (IEApp (i, node, b), c) -> CReset (node.n_name, i, iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, IEApp (i, node, b)))]) + | IEReset _ -> failwith "A pass should have turned not function resets into function resets" diff --git a/src/main.ml b/src/main.ml index da6fed1..7699020 100644 --- a/src/main.ml +++ b/src/main.ml @@ -44,8 +44,9 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) let default_passes = - ["remove_if"; + ["linearization_reset"; "remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; + "ensure_assign_val"; "equations_ordering"] in let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in let usage_msg = @@ -87,6 +88,8 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); + ("ensure_assign_val", Passes.pass_ensure_assignment_value); + ("linearization_reset", Passes.pass_linearization_reset); ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); diff --git a/src/passes.ml b/src/passes.ml index c409846..669c0ac 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -147,6 +147,73 @@ let pass_if_removal verbose debug = node_pass aux_if_removal +(** [pass_linearization_reset] makes sure that all reset constructs in the program + * are applied to functions. + * This is required, since the reset construct is translated into resetting the + * function state in the final C code. *) +let pass_linearization_reset verbose debug = + (** [node_lin] linearizes a single node. *) + let node_lin (node: t_node): t_node option = + (** [reset_aux_expression] takes an expression and returns: + * - a list of additional equations + * - the new list of local variables + * - an updated version of the original expression *) + let rec reset_aux_expression vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + let eqs'', vars, e'' = reset_aux_expression vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + ( + match e with + | EApp (t_app, n_app, e_app) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EReset (t, e, e') + | e -> reset_aux_expression vars e + ) + | EConst _ -> [], vars, expr + | ETuple (t, l) -> + let eqs, vars, l = List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = reset_aux_expression vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EApp (t, n, e) + in + (** Applies the previous function to the expressions of every equation. *) + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) (patt, expr) -> + let eqs', vars, expr = reset_aux_expression vars expr in + (patt, expr)::eqs' @ eqs, vars) + ([], node.n_local_vars) + node.n_equations + in + Some { node with n_local_vars = new_locvars; n_equations = new_equations } + in + node_pass node_lin + (** [pass_linearization_pre] makes sure that all pre constructs in the program * are applied to variables. @@ -391,6 +458,79 @@ let pass_linearization_app verbose debug = +let pass_ensure_assignment_value verbose debug = + let varcount = ref 0 in + let rec aux_expr should_be_value vars expr = + match expr with + | EConst _ | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = aux_expr true vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + let eqs'', vars, e'' = aux_expr should_be_value vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | ETuple (t, l) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr true vars e in + eqs' @ eqs, vars, e :: l) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = aux_expr true vars e in + if should_be_value + then + let nvar = Format.sprintf "_assignval%d" !varcount in + incr varcount; + let nvar: t_var = + match t with + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | [TInt] -> IVar nvar + | _ -> + failwith "An application occurring here should return a single element." + in + let neq_patt: t_varlist = (t, [nvar]) in + let neq_expr: t_expression = EApp (t, n, e) in + let vars = varlist_concat neq_patt vars in + (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar) + else + eqs, vars, EApp (t, n, e) + in + let aux_ensure_assign_val node = + let new_equations, vars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, expr = aux_expr false vars (snd eq) in + (fst eq, expr) :: eqs' @ eqs, vars + ) + ([], node.n_local_vars) node.n_equations + in + Some { node with n_equations = new_equations; n_local_vars = vars } + in + node_pass aux_ensure_assign_val + + + (** [sanity_pass_assignment_unicity] makes sure that there is at most one * equation defining each variable (and that no equation tries to redefine an * input). From 4303dcd0e4e9e70be63a4baeacb7e193d3f76e63 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 13:09:09 +0100 Subject: [PATCH 38/50] Correct a typo in `src/main.ml` disabling the compilation --- src/main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.ml b/src/main.ml index 319f215..7699020 100644 --- a/src/main.ml +++ b/src/main.ml @@ -88,7 +88,7 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); - ("ensure_assign_val", Passes.pass_ensure_assignment_valuh); + ("ensure_assign_val", Passes.pass_ensure_assignment_value); ("linearization_reset", Passes.pass_linearization_reset); ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); From 3ad133344a67a8ca1eadb694c4f2803928e00286 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 14:02:00 +0100 Subject: [PATCH 39/50] [lustre_pp] precise error messages --- src/lustre_pp.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/lustre_pp.ml b/src/lustre_pp.ml index 11335b4..c515449 100644 --- a/src/lustre_pp.ml +++ b/src/lustre_pp.ml @@ -37,7 +37,7 @@ let rec pp_varlist fmt : t_varlist -> unit = function Format.fprintf fmt "%s: bool, %a" h pp_varlist (tl, h' :: l) | (TReal :: tl, RVar h :: h' :: l) -> Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l) - | _ -> raise (MyTypeError "This exception should not have beed be raised.") + | _ -> raise (MyTypeError "(1) This exception should not have beed be raised.") let pp_expression = let upd_prefix s = s ^ " | " in @@ -49,7 +49,9 @@ let pp_expression = Format.fprintf fmt "%a%a" (pp_expression_aux (prefix^" |> ")) expr (pp_expression_list prefix) (ETuple (tt, exprs)) - | _ -> raise (MyTypeError "This exception should not have been raised.") + | ETuple ([], _) -> failwith "A non-empty tuple has no type!" + | ETuple (_, []) -> failwith "An empty tuple has a type!" + | _ -> failwith "This exception should never occur." in match expression with | EWhen (_, e1, e2) -> From c7edb27fb0eeb8be2b6cd11d7a35eb83d966f94a Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 14:04:50 +0100 Subject: [PATCH 40/50] [lustre_pp] fix a typing error --- src/lustre_pp.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/lustre_pp.ml b/src/lustre_pp.ml index c515449..01d5b0c 100644 --- a/src/lustre_pp.ml +++ b/src/lustre_pp.ml @@ -45,11 +45,12 @@ let pp_expression = let rec pp_expression_list prefix fmt exprs = match exprs with | ETuple([], []) -> () - | ETuple (_ :: tt, expr :: exprs) -> + | ETuple (typs, expr :: exprs) -> + let typ_h, typ_t = + Utils.list_select (List.length (Utils.type_exp expr)) typs in Format.fprintf fmt "%a%a" (pp_expression_aux (prefix^" |> ")) expr - (pp_expression_list prefix) (ETuple (tt, exprs)) - | ETuple ([], _) -> failwith "A non-empty tuple has no type!" + (pp_expression_list prefix) (ETuple (typ_t, exprs)) | ETuple (_, []) -> failwith "An empty tuple has a type!" | _ -> failwith "This exception should never occur." in From 42536df81c012e93eacd15638b8b4b7ee6fb464a Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 14:10:34 +0100 Subject: [PATCH 41/50] [parser] update of some error messages --- src/parser.mly | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/parser.mly b/src/parser.mly index ef3504e..f15de24 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -313,15 +313,15 @@ expr: | MO_pre expr { EMonOp (type_exp $2, MOp_pre, $2) } | MINUS expr { monop_neg_condition $2 [TBool] - "You cannot take the opposite of a boolean expression." + "You cannot take the opposite of an expression that is not a number." (EMonOp (type_exp $2, MOp_minus, $2)) } | PLUS expr { monop_neg_condition $2 [TBool] - "You cannot take the plus of a boolean expression." $2 } + "(+) expects its argument to be a number." $2 } /* Binary operators */ | expr PLUS expr { make_binop_nonbool $1 $3 BOp_add - "You should know better; addition hates booleans" } + "Addition expects both arguments to be (the same kind of) numbers." } | expr MINUS expr { make_binop_nonbool $1 $3 BOp_sub "You should know better; subtraction hates booleans" } From f121f55432ee3be849f2eca2ca36015a970069ca Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 15:11:12 +0100 Subject: [PATCH 42/50] [cprint] add a main function --- src/ast_to_c.ml | 7 +-- src/config.ml | 2 +- src/cprint.ml | 126 ++++++++++++++++++++++++++++++++++++++++++++++++ src/test.node | 14 +----- 4 files changed, 133 insertions(+), 16 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index dbdbd5e..0f1e4af 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -310,9 +310,10 @@ let ast_to_c verbose debug prog = verbose "Computation of the node_states"; let prog_st_types = make_state_types prog 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" + let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in + Format.printf "%a\n\n%a\n\n/* Nodes: */\n%a%a\n" cp_includes (Config.c_includes) cp_state_types prog_st_types - cp_nodes (prog, prog_st_types) + cp_nodes (iprog, prog_st_types) + cp_main_fn (prog, prog_st_types) diff --git a/src/config.ml b/src/config.ml index 1ad7133..c89bff4 100644 --- a/src/config.ml +++ b/src/config.ml @@ -3,4 +3,4 @@ * variables. *) let maxvar = 100 -let c_includes = ["stdbool"; "stdlib"] +let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"] diff --git a/src/cprint.ml b/src/cprint.ml index 759c1c2..3df57af 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -218,3 +218,129 @@ and cp_expression fmt (expr, hloc) = p; prefix_ := p + + +(** [cp_main] tries to print a main function to the C code. + * If there is a function [main] in the lustre program, it will generate a main + * function in the C code, otherwise it does not do anything. + *) +let cp_main_fn fmt (prog, sts) = + let rec cp_array fmt (vl: t_var list): unit = + match vl with + | [] -> () + | v :: vl -> + let typ, name = + match v with + | IVar s -> ("int", s) + | RVar s -> ("double", s) + | BVar s -> + Format.fprintf fmt "\tchar _char_of_%s;\n" s; + ("bool", s) + in + Format.fprintf fmt "\t%s %s;\n%a" typ name + cp_array vl + in + let rec cp_inputs fmt (f, l) = + match f, l with + | _, [] -> () + | true, h :: t -> + Format.fprintf fmt ", %s%a" + (Utils.name_of_var h) + cp_inputs (true, t) + | false, h :: t -> + Format.fprintf fmt "%s%a" + (Utils.name_of_var h) + cp_inputs (true, t) + in + let cp_scanf fmt vl = + let rec cp_scanf_str fmt (b, vl) = + match b, vl with + | _, [] -> () + | true, h :: t -> + Format.fprintf fmt " %s%a" + (match h with + | IVar _ -> "%d" + | BVar _ -> "%c" + | RVar _ -> "%lf") + cp_scanf_str (true, t) + | false, h :: t -> + Format.fprintf fmt "%s%a" + (match h with + | IVar _ -> "%d" + | BVar _ -> "%c" + | RVar _ -> "%lf") + cp_scanf_str (true, t) + in + let rec cp_scanf_args fmt vl = + match vl with + | [] -> () + | RVar s :: vl | IVar s :: vl -> + Format.fprintf fmt ", &%s%a" s cp_scanf_args vl + | BVar s :: vl -> + Format.fprintf fmt ", &%s%a" (Format.sprintf "_char_of_%s" s) + cp_scanf_args vl + in + Format.fprintf fmt "\"%a\"%a" + cp_scanf_str (false, vl) + cp_scanf_args vl + in + let cp_printf fmt vl = + let rec cp_printf_str fmt (b, vl) = + match b, vl with + | _, [] -> () + | true, h :: t -> + Format.fprintf fmt " %s%a" + (match h with + | IVar _ -> "%d" + | BVar _ -> "%c" + | RVar _ -> "%f") + cp_printf_str (true, t) + | false, h :: t -> + Format.fprintf fmt "%s%a" + (match h with + | IVar _ -> "%d" + | BVar _ -> "%c" + | RVar _ -> "%f") + cp_printf_str (true, t) + in + let rec cp_printf_arg fmt (h, i) = + match Hashtbl.find_opt h i with + | None -> () + | Some (s, i) -> + Format.fprintf fmt ", state.%s[%d]%a" + s i cp_printf_arg (h, i+1) + in + Format.fprintf fmt "\"%a\"%a" + cp_printf_str (false, vl) + cp_printf_arg ((Hashtbl.find sts "main").nt_output_map, 0) + in + let rec cp_char_to_bool fmt vl = + match vl with + | [] -> () + | RVar _ :: vl | IVar _ :: vl -> Format.fprintf fmt "%a" cp_char_to_bool vl + | BVar s :: vl -> + Format.fprintf fmt "\t\t%s = (%s == 't') ? true : false;\n%a" + s (Format.sprintf "_char_of_%s" s) + cp_char_to_bool vl + in + match List.find_opt (fun n -> n.n_name = "main") prog with + | None -> () + | Some node -> + Format.fprintf fmt "int main (int argc, char **argv)\n\ + {\n%a\n\ + \tchar _buffer[1024];\n\ + \tt_state_main state; state.is_init = true;\n\ + \twhile(true) {\n\ + \t\tscanf(\"%%s\", _buffer);\n\ + \t\tif(!strcmp(_buffer, \"exit\")) { exit (EXIT_SUCCESS); }\n\ + \t\tsscanf(_buffer, %a);\n%a\ + \t\tfn_main(&state, %a);\n\ + \t\tprintf(%a);\n\ + \t}\n\ + \treturn EXIT_SUCCESS;\n\ + }\n" + cp_array (snd node.n_inputs) + cp_scanf (snd node.n_inputs) + cp_char_to_bool (snd node.n_inputs) + cp_inputs (false, snd node.n_inputs) + cp_printf (snd node.n_outputs) diff --git a/src/test.node b/src/test.node index d6f531d..3c3e9a8 100644 --- a/src/test.node +++ b/src/test.node @@ -1,15 +1,5 @@ -node id (a: bool) returns (o: bool); +node main (i: int) returns (a, b: int); let - o = a; + (a, b) = (i, i); 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 id(false -> a); -tel From 52092b1480f10f9ea2c72fe3b4d847088851c893 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 15:24:55 +0100 Subject: [PATCH 43/50] [cprint] code reduction --- src/cprint.ml | 48 ++++++++++++++++++------------------------------ 1 file changed, 18 insertions(+), 30 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index 3df57af..fb56053 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -241,30 +241,23 @@ let cp_main_fn fmt (prog, sts) = cp_array vl in let rec cp_inputs fmt (f, l) = - match f, l with - | _, [] -> () - | true, h :: t -> - Format.fprintf fmt ", %s%a" - (Utils.name_of_var h) - cp_inputs (true, t) - | false, h :: t -> - Format.fprintf fmt "%s%a" + match l with + | [] -> () + | h :: t -> + (if f + then Format.fprintf fmt ", %s%a" + else Format.fprintf fmt "%s%a") (Utils.name_of_var h) cp_inputs (true, t) in let cp_scanf fmt vl = let rec cp_scanf_str fmt (b, vl) = - match b, vl with - | _, [] -> () - | true, h :: t -> - Format.fprintf fmt " %s%a" - (match h with - | IVar _ -> "%d" - | BVar _ -> "%c" - | RVar _ -> "%lf") - cp_scanf_str (true, t) - | false, h :: t -> - Format.fprintf fmt "%s%a" + match vl with + | [] -> () + | h :: t -> + (if b + then Format.fprintf fmt " %s%a" + else Format.fprintf fmt "%s%a") (match h with | IVar _ -> "%d" | BVar _ -> "%c" @@ -286,17 +279,12 @@ let cp_main_fn fmt (prog, sts) = in let cp_printf fmt vl = let rec cp_printf_str fmt (b, vl) = - match b, vl with - | _, [] -> () - | true, h :: t -> - Format.fprintf fmt " %s%a" - (match h with - | IVar _ -> "%d" - | BVar _ -> "%c" - | RVar _ -> "%f") - cp_printf_str (true, t) - | false, h :: t -> - Format.fprintf fmt "%s%a" + match vl with + | [] -> () + | h :: t -> + (if b + then Format.fprintf fmt " %s%a" + else Format.fprintf fmt "%s%a") (match h with | IVar _ -> "%d" | BVar _ -> "%c" From 88c145a52713cc8eda6326124d77a5b0b02b41b6 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 15:39:33 +0100 Subject: [PATCH 44/50] Disable `malloc`s when `reset`ing --- src/ast_to_c.ml | 8 ++++++-- src/cprint.ml | 12 +++++++++--- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index dbdbd5e..15db7fb 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -236,11 +236,15 @@ let cp_init_aux_nodes fmt (node, h) = | None -> () (** All auxiliary nodes have been initialized *) | Some n -> begin - Format.fprintf fmt "%a\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ - \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n" + Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\ + \t\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ + \t\t}\n\ + \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\ + \t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n" aux (node, nst, i-1) (i-1) (Format.asprintf "t_state_%s" n.n_name) (Format.asprintf "t_state_%s" n.n_name) (i-1) + (Format.asprintf "t_state_%s" n.n_name) (i-1) end in let nst = Hashtbl.find h node.in_name in diff --git a/src/cprint.ml b/src/cprint.ml index 759c1c2..3837d2c 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -19,7 +19,7 @@ let cp_node_state fmt (st: node_state) = if st.nt_count_app = 0 then Format.fprintf fmt "typedef struct {%a%a%a\n\ - \tbool is_init;\n\ + \tbool is_init, is_reset;\n\ } %s;\n\n" print_if_any ("int", st.nt_nb_int, "ivars") print_if_any ("bool", st.nt_nb_bool, "bvars") @@ -27,7 +27,7 @@ let cp_node_state fmt (st: node_state) = st.nt_name else Format.fprintf fmt "typedef struct {%a%a%a\n\ - \tbool is_init;\n\ + \tbool is_init, is_reset;\n\ \tvoid* aux_states[%d]; /* stores the states of auxiliary nodes */\n\ } %s;\n\n" print_if_any ("int", st.nt_nb_int, "ivars") @@ -191,10 +191,16 @@ and cp_expression fmt (expr, hloc) = end | CReset (node_name, i, v, b) -> begin - Format.fprintf fmt "\tif (%a) {\n\t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\t}\n%a\n" + Format.fprintf fmt "\tif (%a) {\n\ + \t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\ + \t\t((t_state_%s*)(state->aux_states[%d]))->is_reset = true;\n\ + \t}\n\ + %a\n" cp_value (v, hloc) node_name (i - 1) + node_name + (i - 1) cp_block (b, hloc) end | CIf (v, b1, []) -> From fd9544663694ebee0268c37fd98aa2edbaa06c48 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 15:46:31 +0100 Subject: [PATCH 45/50] Modify C `main` to initialize correctly the state with `is_reset = false` --- src/cprint.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cprint.ml b/src/cprint.ml index 9585e6f..20a96a5 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -323,7 +323,9 @@ let cp_main_fn fmt (prog, sts) = Format.fprintf fmt "int main (int argc, char **argv)\n\ {\n%a\n\ \tchar _buffer[1024];\n\ - \tt_state_main state; state.is_init = true;\n\ + \tt_state_main state;\n\ + \tstate.is_init = true;\n\ + \tstate.is_reset = false;\n\ \twhile(true) {\n\ \t\tscanf(\"%%s\", _buffer);\n\ \t\tif(!strcmp(_buffer, \"exit\")) { exit (EXIT_SUCCESS); }\n\ From 24108925fd09fbcdc7620a81d96db3917ce27ab6 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 16:29:26 +0100 Subject: [PATCH 46/50] [cprint] free the allocated memory (states). --- src/ast_to_c.ml | 3 +- src/cprint.ml | 96 ++++++++++++++++++++++++++++++++++++++++++++++++- src/test.node | 17 +++++++-- 3 files changed, 112 insertions(+), 4 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index b8f3715..3bd4c28 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -315,9 +315,10 @@ let ast_to_c verbose debug prog = let prog_st_types = make_state_types prog in debug (Format.asprintf "%a" dump_var_locations prog_st_types); let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in - Format.printf "%a\n\n%a\n\n/* Nodes: */\n%a%a\n" + Format.printf "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n" cp_includes (Config.c_includes) cp_state_types prog_st_types + cp_state_frees (iprog, prog_st_types) cp_nodes (iprog, prog_st_types) cp_main_fn (prog, prog_st_types) diff --git a/src/cprint.ml b/src/cprint.ml index 20a96a5..a4d8064 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -40,6 +40,79 @@ let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = Format.fprintf fmt "/* Struct holding states of the node %s: */\n%a" n cp_node_state nst) h + + +(** [cp_state_frees] prints the required code to recursively free the node + * states. *) +let cp_state_frees fmt (iprog, sts) = + let rec find_callee (i: int) (f: i_node) = + let rec aux_expr = function + | IETuple [] | IEVar _ | IEConst _ -> None + | IEMonOp (_, e) -> aux_expr e + | IEWhen (e, e') + | IEReset (e, e') + | IEComp (_, e, e') + | IEBinOp (_, e, e') -> + begin + match aux_expr e with + | None -> aux_expr e' + | Some res -> Some res + end + | IETriOp (_, e, e', e'') -> + begin + match aux_expr e with + | None -> + (match aux_expr e' with + | None -> aux_expr e'' + | Some res -> Some res) + | Some res -> Some res + end + | IETuple (h :: t) -> + begin + match aux_expr h with + | None -> aux_expr (IETuple t) + | Some res -> Some res + end + | IEApp (j, n, e) -> + if i = j + then Some n.n_name + else aux_expr e + in + List.fold_right + (fun (_, expr) acc -> + match acc with + | Some _ -> acc + | None -> aux_expr expr) + f.in_equations None + in + let rec cp_free_aux fmt (i, caller_name) = + let idx = i - 1 in + match find_callee i (List.find (fun n -> n.in_name = caller_name) iprog)with + | None -> () + | Some callee_name -> + let callee_st = Hashtbl.find sts callee_name in + if callee_st.nt_count_app > 0 then + Format.fprintf fmt "\tif (st->aux_states[%d])\n\ + \t\tfree_state_%s(st->aux_states + %d);\n" + idx callee_name idx; + Format.fprintf fmt "\tif (st->aux_states[%d])\n\ + \t\tfree(st->aux_states[%d]);\n%a" + idx idx cp_free_aux (i+1, caller_name) + in + Hashtbl.iter + (fun node_name node_st -> + if node_st.nt_count_app = 0 + then () (** Nothing to free for the node [node_name]. *) + else + Format.fprintf fmt "void free_state_%s(t_state_%s *st)\n\ + {\n\ + %a\ + }\n" + node_name node_name + cp_free_aux (1, node_name)) sts + + + let cp_var' fmt = function | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx | CVInput s -> Format.fprintf fmt "%s" s @@ -75,6 +148,13 @@ let rec cp_varlist fmt vl = print_if_any vl cp_varlist vl + + +(** [cp_prototype] prints functions prototypes (without the «;»). It is only + * used to write the beginning of functions right now. If we later allow to + * use auxiliary nodes before their definition, it might be useful to declare + * all the prototypes at the beginning of the file (Cf. [cp_prototypes] below. + *) let cp_prototype fmt (node, h): unit = match Hashtbl.find_opt h node.in_name with | None -> failwith "This should not happened!" @@ -96,6 +176,10 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = +(** [cp_value] prints values, that is unary or binary operations which can be + * inlined in the final code without requiring many manipulations. + * It uses a lot of parenthesis at the moment. An improvement would be to + * remove useless ones at some point. *) let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = let string_of_binop = function | BOp_add -> "+" @@ -146,6 +230,8 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CMonOp (MOp_pre, _) -> failwith "The linearization should have removed this case." + + let prefix_ = ref "\t" (** The following function prints one transformed equation of the program into a @@ -317,6 +403,12 @@ let cp_main_fn fmt (prog, sts) = s (Format.sprintf "_char_of_%s" s) cp_char_to_bool vl in + let cp_free fmt () = + let main_st = Hashtbl.find sts "main" in + if main_st.nt_count_app = 0 + then () + else Format.fprintf fmt "\tfree_state_main(&st)\n" + in match List.find_opt (fun n -> n.n_name = "main") prog with | None -> () | Some node -> @@ -333,10 +425,12 @@ let cp_main_fn fmt (prog, sts) = \t\tfn_main(&state, %a);\n\ \t\tprintf(%a);\n\ \t}\n\ - \treturn EXIT_SUCCESS;\n\ + %a\treturn EXIT_SUCCESS;\n\ }\n" cp_array (snd node.n_inputs) cp_scanf (snd node.n_inputs) cp_char_to_bool (snd node.n_inputs) cp_inputs (false, snd node.n_inputs) cp_printf (snd node.n_outputs) + cp_free () + diff --git a/src/test.node b/src/test.node index 3c3e9a8..6f83475 100644 --- a/src/test.node +++ b/src/test.node @@ -1,5 +1,18 @@ -node main (i: int) returns (a, b: int); +node id_int (i: int) returns (o: int); let - (a, b) = (i, i); + o = i -> i; +tel + +node aux (i, j: int) returns (o: int); +let + o = id_int(i) + id_int(j); +tel + +node main (i: int) returns (a, b: int); +var tmp: int; +let + a = 1; + b = aux (i, a); + tmp = aux (a+b, i); tel From ffa8918330a437f0ad0543d93e0dc1c1aebd194f Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 16:34:31 +0100 Subject: [PATCH 47/50] [C] a few fixes --- src/cprint.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index a4d8064..061cd70 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -93,12 +93,19 @@ let cp_state_frees fmt (iprog, sts) = let callee_st = Hashtbl.find sts callee_name in if callee_st.nt_count_app > 0 then Format.fprintf fmt "\tif (st->aux_states[%d])\n\ - \t\tfree_state_%s(st->aux_states + %d);\n" - idx callee_name idx; + \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n" + idx callee_name callee_name idx; Format.fprintf fmt "\tif (st->aux_states[%d])\n\ \t\tfree(st->aux_states[%d]);\n%a" idx idx cp_free_aux (i+1, caller_name) in + Hashtbl.iter + (fun node_name node_st -> + if node_st.nt_count_app = 0 + then () (** Nothing to free for the node [node_name]. *) + else + Format.fprintf fmt "void free_state_%s(t_state_%s *);\n" + node_name node_name) sts; Hashtbl.iter (fun node_name node_st -> if node_st.nt_count_app = 0 @@ -407,7 +414,7 @@ let cp_main_fn fmt (prog, sts) = let main_st = Hashtbl.find sts "main" in if main_st.nt_count_app = 0 then () - else Format.fprintf fmt "\tfree_state_main(&st)\n" + else Format.fprintf fmt "\tfree_state_main(&state);\n" in match List.find_opt (fun n -> n.n_name = "main") prog with | None -> () @@ -420,7 +427,7 @@ let cp_main_fn fmt (prog, sts) = \tstate.is_reset = false;\n\ \twhile(true) {\n\ \t\tscanf(\"%%s\", _buffer);\n\ - \t\tif(!strcmp(_buffer, \"exit\")) { exit (EXIT_SUCCESS); }\n\ + \t\tif(!strcmp(_buffer, \"exit\")) { break; }\n\ \t\tsscanf(_buffer, %a);\n%a\ \t\tfn_main(&state, %a);\n\ \t\tprintf(%a);\n\ From 03def2ce1a34e08798569246781547b9fdf6f62d Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 16:38:29 +0100 Subject: [PATCH 48/50] [C] new lines in then output after each step --- src/cprint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cprint.ml b/src/cprint.ml index 061cd70..c9faf22 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -397,7 +397,7 @@ let cp_main_fn fmt (prog, sts) = Format.fprintf fmt ", state.%s[%d]%a" s i cp_printf_arg (h, i+1) in - Format.fprintf fmt "\"%a\"%a" + Format.fprintf fmt "\"%a\\n\"%a" cp_printf_str (false, vl) cp_printf_arg ((Hashtbl.find sts "main").nt_output_map, 0) in From a673c447e3d45dc04203f9ffa4d358f19f64205a Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 16:41:21 +0100 Subject: [PATCH 49/50] [messages] better comment and errors --- src/cprint.ml | 4 ++-- src/parser.mly | 16 ++++++++-------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/cprint.ml b/src/cprint.ml index c9faf22..a47edcd 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -319,8 +319,8 @@ and cp_expression fmt (expr, hloc) = -(** [cp_main] tries to print a main function to the C code. - * If there is a function [main] in the lustre program, it will generate a main +(** [cp_main] prints a main function to the C code if necessary: + * if there is a function [main] in the lustre program, it will generate a main * function in the C code, otherwise it does not do anything. *) let cp_main_fn fmt (prog, sts) = diff --git a/src/parser.mly b/src/parser.mly index f15de24..e2e0853 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -216,8 +216,8 @@ node_content: if vars_distinct e_in e_out (snd $10) then (Hashtbl.add defined_nodes node_name n; n) else raise (MyParsingError - ("There is a conflict between the names of local, input \ - or output variables.", + ("There is a conflict between the names of local,\ + input or output variables.", current_location())) end}; @@ -324,22 +324,22 @@ expr: "Addition expects both arguments to be (the same kind of) numbers." } | expr MINUS expr { make_binop_nonbool $1 $3 BOp_sub - "You should know better; subtraction hates booleans" } + "Substraction expects both arguments to be (the same kind of) numbers." } | expr BO_mul expr { make_binop_nonbool $1 $3 BOp_mul - "You should know better; multiplication hates booleans" } + "Multiplication expects both arguments to be (the same kind of) numbers." } | expr BO_div expr { make_binop_nonbool $1 $3 BOp_div - "You should know better; division hates booleans" } + "Division expects both arguments to be (the same kind of) numbers." } | expr BO_mod expr { make_binop_nonbool $1 $3 BOp_mod - "You should know better; modulo hates booleans" } + "Modulo expects both arguments to be numbers." } | expr BO_and expr { make_binop_bool $1 $3 BOp_and - "You should know better; conjunction hates numbers" } + "Conjunction expects both arguments to be booleans." } | expr BO_or expr { make_binop_bool $1 $3 BOp_or - "You should know better; disjunction hates numbers" } + "Disjunction expects both arguments to be booleans." } | expr BO_arrow expr { let e1 = $1 in let t1 = type_exp e1 in let e2 = $3 in let t2 = type_exp e2 in From 8c3e3d1eac0676fc1598a4ea843bcc3374e2ae03 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Tue, 20 Dec 2022 16:52:59 +0100 Subject: [PATCH 50/50] [C] malloc->calloc + conditions merged in free_state_* --- src/ast_to_c.ml | 2 +- src/cprint.ml | 17 ++++++++++------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 3bd4c28..cca059f 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -237,7 +237,7 @@ let cp_init_aux_nodes fmt (node, h) = | Some n -> begin Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\ - \t\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ + \t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\ \t\t}\n\ \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\ \t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n" diff --git a/src/cprint.ml b/src/cprint.ml index a47edcd..07013db 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -91,13 +91,16 @@ let cp_state_frees fmt (iprog, sts) = | None -> () | Some callee_name -> let callee_st = Hashtbl.find sts callee_name in - if callee_st.nt_count_app > 0 then - Format.fprintf fmt "\tif (st->aux_states[%d])\n\ - \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n" - idx callee_name callee_name idx; - Format.fprintf fmt "\tif (st->aux_states[%d])\n\ - \t\tfree(st->aux_states[%d]);\n%a" - idx idx cp_free_aux (i+1, caller_name) + if callee_st.nt_count_app > 0 + then + Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\ + \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\ + \t\tfree (st->aux_state[%d]);\n\t}\n%a" + idx callee_name callee_name idx + idx cp_free_aux (i+1, caller_name) + else Format.fprintf fmt "\tif (st->aux_states[%d])\n\ + \t\tfree(st->aux_states[%d]);\n%a" + idx idx cp_free_aux (i+1, caller_name) in Hashtbl.iter (fun node_name node_st ->