From 0da0f58b2293dadef2c74b4654b85497db722db4 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 16:01:48 +0100 Subject: [PATCH] [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