[ast2C] proposition initiale

This commit is contained in:
dsac 2022-12-17 16:01:48 +01:00
parent fa052f70e2
commit 0da0f58b22
7 changed files with 202 additions and 266 deletions

View File

@ -1,280 +1,117 @@
open Ast 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 (** The following function defines the [node_states] for the nodes of a program,
| ([], []) -> () * and puts them in a hash table. *)
| ([TInt] , IVar h :: []) -> Format.fprintf fmt "int" let make_state_types nodes: (ident, node_state) Hashtbl.t =
| ([TReal], RVar h :: []) -> Format.fprintf fmt "float" (* Hash table to fill *)
| ([TBool], BVar h :: []) -> Format.fprintf fmt "bool" let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in
| (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.")
let rec pp_prevarlist node_name fmt : t_varlist -> unit = function (** [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,
| ([TInt] , IVar h :: []) -> Format.fprintf fmt "int pre_%s_%s;" node_name h * where [pv] is a list of variables used in the pre construct in the
| ([TReal], RVar h :: []) -> Format.fprintf fmt "float pre_%s_%s;" node_name h * programm. *)
| ([TBool], BVar h :: []) -> Format.fprintf fmt "bool pre_%s_%s;" node_name h let one_node node pv ty =
| (TInt :: tl, IVar h :: h' :: l) -> (* variables of type [ty] among output and local variables *)
Format.fprintf fmt "int pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) let vars =
| (TBool :: tl, BVar h :: h' :: l) -> List.filter (fun v -> type_var v = [ty])
Format.fprintf fmt "float pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) (snd (varlist_concat node.n_outputs node.n_local_vars)) in
| (TReal :: tl, RVar h :: h' :: l) -> let pre_vars =
Format.fprintf fmt "bool pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l) List.filter (fun v -> List.mem v pv) vars in
| _ -> raise (MyTypeError "This exception should not have beed be raised.") let nb = (List.length vars) + (List.length pre_vars) in
let tyh = Hashtbl.create nb in
let rec pp_asnprevarlist node_name fmt : t_varlist -> unit = function let i =
| ([], []) -> () List.fold_left
| ([TInt] , IVar h :: []) | ([TReal], RVar h :: []) | ([TBool], BVar h :: []) -> Format.fprintf fmt "\tpre_%s_%s = %s;" node_name h h (fun i v -> let () = Hashtbl.add tyh (v, false) i in i + 1) 0 vars in
| (TInt :: tl, IVar h :: h' :: l) | (TBool :: tl, BVar h :: h' :: l) | (TReal :: tl, RVar h :: h' :: l) -> let _ =
Format.fprintf fmt "\tpre_%s_%s = %s;\n%a" node_name h h (pp_asnprevarlist node_name) (tl, h' :: l) List.fold_left
| _ -> raise (MyTypeError "This exception should not have beed be raised.") (fun i v -> let () = Hashtbl.add tyh (v, true) i in i + 1) i pre_vars in
(nb, tyh)
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.")
in in
match expression with
| EWhen (_, e1, e2) -> (** [find_prevars n] returns the list of variables appearing after a pre in
begin * the node [n].
Format.fprintf fmt "%a ? %a : 0" * Note that the only occurence of pre are of the form pre (var), due to the
pp_expression_aux e2 * linearization pass.
pp_expression_aux e1 *)
end let find_prevars node =
| EReset (_, e1, e2) -> let rec find_prevars_expr = function
begin | EConst _ | EVar _ -> []
incr reset_expressions_counter; | EMonOp (_, MOp_pre, EVar (_, v)) -> [v]
(* Use following trick as we can't use `;`: | EMonOp (_, _, e) -> find_prevars_expr e
if(((var = val) && false) || condition) | ETriOp (_, _, e, e', e'') ->
is equivalent to an incorrect statement like (find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'')
if({var = val; condition}) | EComp (_, _, e, e')
We also use this trick with the fact that `0` can be interpreted as a `bool`, an `int` and a `float` *) | EBinOp (_, _, e, e')
(* could use C macros to simplify the C code *) | EWhen (_, e, e')
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])" | EReset (_, e, e') -> (find_prevars_expr e) @ (find_prevars_expr e')
(!reset_expressions_counter - 1) | ETuple (_, l) -> List.flatten (List.map (find_prevars_expr) l)
pp_expression_aux e1 | EApp (_, _, e) -> find_prevars_expr e
node_name in
(!reset_expressions_counter - 1) list_remove_duplicates
(!reset_expressions_counter - 1) (List.fold_left
(!reset_expressions_counter - 1) (fun acc (_, expr) -> (find_prevars_expr expr) @ acc)
pp_expression_aux e2 [] node.n_equations)
(!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 in
pp_expression_aux
(* deterministic *) (** [aux] iterates over all nodes of the program to build the required hash
let nodes_outputs = Hashtbl.create Config.maxvar;; * table *)
let rec aux nodes =
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 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 match nodes with
| [] -> () | [] -> h
| node :: nodes -> | node :: nodes ->
Format.fprintf fmt "%a\n%a" pp_node node pp_nodes nodes begin
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
in
aux 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 = (*let ast_to_c*)
load_outputs_from_nodes prog;
Format.fprintf fmt
(* could verify that uses, possibly indirectly (cf `->` implementation), a boolean in the ast before including `<stdbool.h>` *)
"#include <stdbool.h>\n\n%s\n\n%a" let ast_to_c prog =
("float " ^ (String.concat ", " (List.map (fun output -> "output_" ^ output) !outputs)) ^ ";") pp_nodes 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)

34
src/c_utils.ml Normal file
View File

@ -0,0 +1,34 @@
open Ast
(** A node state is translated into a struct. This struct has:
* 1. A name (t_state_<name of the node>)
* 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_<node name>;
*)
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;
}

View File

@ -3,3 +3,4 @@
* variables. *) * variables. *)
let maxvar = 100 let maxvar = 100
let c_includes = "#include <stdbool.h>"

57
src/cprint.ml Normal file
View File

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

View File

@ -133,7 +133,7 @@ let _ =
else ( else (
if !nopopt if !nopopt
then (fun _ -> ()) then (fun _ -> ())
else Format.printf "%a" Ast_to_c.ast_to_c) else Ast_to_c.ast_to_c)
end end
end end

View File

@ -601,8 +601,8 @@ let clock_unification_pass verbose debug main_fn ast =
| _ -> failure ("Merge format") | _ -> failure ("Merge format")
end end
| ETriOp(_, TOp_if, e1, e2, e3) -> | ETriOp(_, TOp_if, e1, e2, e3) ->
let c1 = compute_clock_exp e1 let (* Unused: c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2 and*) c2 = compute_clock_exp e2
and c3 = compute_clock_exp e3 in and c3 = compute_clock_exp e3 in
if c2 <> c3 then if c2 <> c3 then
failure "If clocks" failure "If clocks"

View File

@ -9,6 +9,13 @@ let rec list_select n = function
let p1, p2 = list_select (n-1) t in let p1, p2 = list_select (n-1) t in
h :: p1, p2 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 = let rec list_map_option (f: 'a -> 'b option) (l: 'a list) : 'b list option =
List.fold_right (fun elt acc -> List.fold_right (fun elt acc ->
match acc, f elt with match acc, f elt with