Benjamin_Loison/Synchronous_reactive_systems
1
0
Fork 0
Code Issues 7 Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: Benjamin_Loison:9d7588f10388b198ecadeba251eadab3ebbe7d55
Branches Tags
Benjamin_Loison:master
Benjamin_Loison:ast2C_proposition
..
compare: Benjamin_Loison:ade62ba678686581eaff8f5ed7f3d99943415042
Branches Tags
Benjamin_Loison:master
Benjamin_Loison:ast2C_proposition

No commits in common. "9d7588f10388b198ecadeba251eadab3ebbe7d55" and "ade62ba678686581eaff8f5ed7f3d99943415042" have entirely different histories.
9d7588f103 ... ade62ba678

19 changed files with 613 additions and 1701 deletions
Show Stats Expand all files Collapse all files

550
src/ast_to_c.ml
View File

@ -1,324 +1,280 @@
open Ast open Ast
open Intermediate_ast
open Intermediate_utils
open Cprint
open Cast
open Utils
open Ctranslation
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.")
(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *) let rec pp_retvarlist fmt : t_varlist -> unit = function
let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist = | ([], []) -> ()
let c = ref 1 in | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int"
let ast_to_intermediate_ast_varlist vl = snd vl in | ([TReal], RVar h :: []) -> Format.fprintf fmt "float"
let rec ast_to_intermediate_ast_expr hloc = function | ([TBool], BVar h :: []) -> Format.fprintf fmt "bool"
| EVar (_, v) -> | (TInt :: tl, IVar h :: h' :: l) ->
begin Format.fprintf fmt "int, %a" pp_retvarlist (tl, h' :: l)
match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with | (TBool :: tl, BVar h :: h' :: l) ->
| None -> IEVar (CVInput (name_of_var v)) Format.fprintf fmt "float, %a" pp_retvarlist (tl, h' :: l)
| Some (s, i) -> IEVar (CVStored (s, i)) | (TReal :: tl, RVar h :: h' :: l) ->
end Format.fprintf fmt "bool, %a" pp_retvarlist (tl, h' :: l)
| EMonOp (_, MOp_pre, EVar (_, v)) -> | _ -> raise (MyTypeError "This exception should not have beed be raised.")
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')
| ETriOp (_, op, e, e', 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') ->
IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
| EWhen (_, e, e') ->
IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
| EReset (_, e, e') ->
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_intermediate_ast_expr hloc e in
let res = IEApp (!c, n, e) in
let () = incr c in
res
end
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 ->
let () = c := 1 in
let hloc = (Hashtbl.find h node.n_name).nt_map in
{
in_name = node.n_name;
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
(** The following function defines the [node_states] for the nodes of a program, let rec pp_prevarlist node_name fmt : t_varlist -> unit = function
* and puts them in a hash table. *) | ([], []) -> ()
let make_state_types nodes: node_states = | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int pre_%s_%s;" node_name h
(* Hash table to fill *) | ([TReal], RVar h :: []) -> Format.fprintf fmt "float pre_%s_%s;" node_name h
let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in | ([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 let rec pp_asnprevarlist node_name fmt : t_varlist -> unit = function
* [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 | ([TInt] , IVar h :: []) | ([TReal], RVar h :: []) | ([TBool], BVar h :: []) -> Format.fprintf fmt "\tpre_%s_%s = %s;" node_name h h
* program. *) | (TInt :: tl, IVar h :: h' :: l) | (TBool :: tl, BVar h :: h' :: l) | (TReal :: tl, RVar h :: h' :: l) ->
let one_node node pv ty = Format.fprintf fmt "\tpre_%s_%s = %s;\n%a" node_name h h (pp_asnprevarlist node_name) (tl, h' :: l)
(* variables of type [ty] among output and local variables *) | _ -> raise (MyTypeError "This exception should not have beed be raised.")
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) 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: (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
let _ =
List.fold_left
(fun i v -> let () = Hashtbl.add tyh (v, true) i in i + 1) i pre_vars in
(nb, tyh)
in
(** [find_prevars n] returns the list of variables appearing after a pre in let reset_expressions_counter = ref 0;;
* the node [n].
* Note that the only occurrence of pre are of the form pre (var), due to let outputs = ref [];;
* the linearization pass.
*) let pp_expression node_name =
let find_prevars node = let rec pp_expression_aux fmt expression =
let rec find_prevars_expr = function let rec pp_expression_list fmt exprs =
| EConst _ | EVar _ -> [] match exprs with
| EMonOp (_, MOp_pre, EVar (_, v)) -> [v] | ETuple([], []) -> ()
| EMonOp (_, _, e) -> find_prevars_expr e | ETuple (_ :: tt, expr :: exprs) ->
| ETriOp (_, _, e, e', e'') -> Format.fprintf fmt "%a%s%a"
(find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'') pp_expression_aux expr
| EComp (_, _, e, e') (if (List.length tt > 0) then ", " else "")
| EBinOp (_, _, e, e') pp_expression_list (ETuple (tt, exprs))
| EWhen (_, e, e') | _ -> raise (MyTypeError "This exception should not have been raised.")
| 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 in
list_remove_duplicates match expression with
(List.fold_left | EWhen (_, e1, e2) ->
(fun acc (_, expr) -> (find_prevars_expr expr) @ acc)
[] 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 =
match nodes with
| [] -> h
| node :: nodes ->
begin begin
let h = aux nodes in Format.fprintf fmt "%a ? %a : 0"
let node_name = node.n_name in pp_expression_aux e2
let pv = find_prevars node in pp_expression_aux e1
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
(fun n (v: t_var) ->
match v with
| IVar s ->
let i = Hashtbl.find h_int (s, false) in
Hashtbl.add h_out n ("ivars", i)
| BVar s ->
let i = Hashtbl.find h_bool (s, false) in
Hashtbl.add h_out n ("bvars", i)
| 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
{
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 = h_map;
nt_output_map = h_out;
nt_prevars = pv;
nt_count_app = count_app node;
} in
h
end 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 in
aux nodes pp_expression_aux
(* deterministic *)
let nodes_outputs = Hashtbl.create Config.maxvar;;
let prepend_output_aux node_name name =
"output_" ^ node_name ^ "_" ^ name
(** The following C-printer functions are in this file, as they need to work on let prepend_output output node_name =
* the AST and are not simple printers. *) 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
(** 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.in_name in
match (Hashtbl.find h node.in_name).nt_prevars with
| [] -> () | [] -> ()
| l -> | ((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)
Format.fprintf fmt | (([], []), (ETuple ([], []))) :: eqs -> Format.fprintf fmt "%a" (pp_equations node_name) eqs
"\n\t/* Remember the values used in the [pre] construct */\n"; | ((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)
List.iter | (([], []), expr) :: eqs ->
(fun v -> (** Note that «dst_array = src_array» should hold. *) Format.fprintf fmt "\t%a;\n%a"
match Hashtbl.find_opt node_st.nt_map (v, false) with (pp_expression node_name) expr
| Some (src_array, src_idx) -> (pp_equations node_name) eqs
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in | (patt, expr) :: eqs ->
Format.fprintf fmt "\tstate->%s[%d] = state->%s[%d];\n" Format.fprintf fmt "\t%a = %a;\n%a"
dst_array dst_idx src_array src_idx (pp_varlist Base) patt
| None -> (pp_expression node_name) expr
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in (pp_equations node_name) eqs
Format.fprintf fmt "\tstate->%s[%d] = %s;\n"
dst_array dst_idx v
)
(List.map Utils.name_of_var l)
(* 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)))
(** The following function defines the behaviour to have at the first let pp_node fmt node =
* execution of a node, namely: (* undefined behavior if the initial code uses a variable with name:
* - initialize the states of auxiliary nodes - `init_{NODE_NAME}`
*) - `tmp_reset_{int}`
let cp_init_aux_nodes fmt (node, h) = - `init_{int}`
let rec aux fmt (node, nst, i) = - `pre_{NODE_NAME}_{VARIABLE}`
match find_app_opt node.in_equations i with - `output_{NODE_NAME}_{VARIABLE}` *)
| None -> () (** All auxiliary nodes have been initialized *) reset_expressions_counter := 0;
| Some n -> let _ = (pp_equations node.n_name) Format.str_formatter node.n_equations in
begin reset_expressions_counter := 0;
Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\ 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"
\t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\ node.n_name
\t\t}\n\ (* could avoid declaring unused variables *)
\t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\ (pp_prevarlist node.n_name) node.n_inputs
\t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n" (pp_prevarlist node.n_name) node.n_local_vars
aux (node, nst, i-1) (pp_prevarlist node.n_name) node.n_outputs
(i-1) (Format.asprintf "t_state_%s" n.n_name) (pp_resvars !reset_expressions_counter)
(Format.asprintf "t_state_%s" n.n_name) (i-1) (if node.n_name = "main" then "int" else "void")
(Format.asprintf "t_state_%s" n.n_name) (i-1) node.n_name
end (* could avoid newlines if they aren't used to seperate statements *)
in (pp_varlist Arg) node.n_inputs
let nst = Hashtbl.find h node.in_name in (pp_varlist Dec) node.n_local_vars
if nst.nt_count_app = 0 (pp_varlist Dec) node.n_outputs
then () (pp_equations node.n_name) node.n_equations
else begin node.n_name
Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\ (pp_asnprevarlist node.n_name) node.n_inputs
\tif (state->is_init) {\n%a\t}\n\n\n" (pp_asnprevarlist node.n_name) node.n_local_vars
aux (node, nst, nst.nt_count_app) (pp_asnprevarlist node.n_name) node.n_outputs
end (pp_return node.n_name) node.n_outputs
let rec pp_nodes fmt nodes =
(** [cp_equations] prints the node equations. *)
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) =
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, h)
cp_prevars (node, h)
(** [cp_nodes] recursively prints all the nodes of a program. *)
let rec cp_nodes fmt (nodes, h) =
match nodes with match nodes with
| [] -> () | [] -> ()
| node :: nodes -> | node :: nodes ->
Format.fprintf fmt "%a\n%a" Format.fprintf fmt "%a\n%a" pp_node node pp_nodes nodes
cp_node (node, h)
cp_nodes (nodes, h)
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
(** [dump_var_locations] dumps the internal tables to map the program variable let ast_to_c fmt prog =
* (after all the passes) to their location in the final C program. *) load_outputs_from_nodes prog;
let dump_var_locations fmt (st: node_states) = Format.fprintf fmt
Format.fprintf fmt "Tables mapping the AST variables to the C variables:\n"; (* could verify that uses, possibly indirectly (cf `->` implementation), a boolean in the ast before including `<stdbool.h>` *)
Hashtbl.iter "#include <stdbool.h>\n\n%s\n\n%a"
(fun n st -> ("float " ^ (String.concat ", " (List.map (fun output -> "output_" ^ output) !outputs)) ^ ";") pp_nodes prog
Format.fprintf fmt " ∗ NODE: %s\n" n;
Hashtbl.iter
(fun (s, (ispre: bool)) ((arr: string), (idx: int)) ->
match ispre with
| 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
(** main function that prints a C-code from a term of type [t_nodelist]. *)
let ast_to_c fmt 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 iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
Format.fprintf fmt "%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)

27
src/cast.ml
View File

@ -1,27 +0,0 @@
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 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, ... *)
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

1
src/config.ml
View File

@ -3,4 +3,3 @@
* variables. *) * variables. *)
let maxvar = 100 let maxvar = 100
let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"]

446
src/cprint.ml
View File

@ -1,446 +0,0 @@
open Intermediate_utils
open Intermediate_ast
open Ast
open Cast
(** This file contains extremely simple functions printing C code. *)
let rec cp_includes fmt = function
| [] -> ()
| h :: t ->
Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t
let cp_node_state fmt (st: node_state) =
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
in
if st.nt_count_app = 0
then
Format.fprintf fmt "typedef struct {%a%a%a\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")
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, 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")
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 =
Hashtbl.iter (fun n nst ->
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((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 ->
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
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
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 print_if_any fmt = function
| [] -> ()
| _ :: _ -> Format.fprintf fmt ", "
in
match vl with
| [] -> ()
| v :: vl ->
Format.fprintf fmt "%a%a%a"
cp_var' v
print_if_any vl
cp_varlist' vl
let rec cp_varlist fmt vl =
let print_if_any fmt = function
| [] -> ()
| _ :: _ -> Format.fprintf fmt ", "
in
match vl with
| [] -> ()
| v :: vl ->
Format.fprintf fmt "%a%a%a"
cp_var v
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!"
| Some nst ->
begin
Format.fprintf fmt "void fn_%s (%s *state, %a)"
node.in_name
nst.nt_name
cp_varlist node.in_inputs
end
let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) =
match nodes with
| [] -> ()
| node :: nodes ->
Format.fprintf fmt "%a;\n%a"
cp_prototype (node, h)
cp_prototypes (nodes, h)
(** [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 -> "+"
| BOp_sub -> "-"
| BOp_mul -> "*"
| BOp_div -> "/"
| BOp_mod -> "%"
| BOp_and -> "&&"
| BOp_or -> "||"
| BOp_arrow -> failwith "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
| CConst (CInt i) -> Format.fprintf fmt "%d" i
| 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)
| CMonOp (MOp_pre, (CVariable v)) ->
let varname = (match v with
| CVStored (arr, idx) ->
begin
match find_varname hloc (arr, idx) with
| None -> failwith "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 "state->%s[%d]" arr idx
| 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)
| 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 "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_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
match expr with
| CAssign (CVStored (arr, idx), value) ->
begin
Format.fprintf fmt "%sstate->%s[%d] = %a;\n"
prefix arr idx cp_value (value, hloc)
end
| CAssign (CVInput _, _) -> failwith "never assign an input."
| CSeq (e, e') ->
Format.fprintf fmt "%a%a"
cp_expression (e, hloc)
cp_expression (e', hloc)
| 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(%s, %a);\n"
prefix fn
(Format.asprintf "state->aux_states[%d]" (nb-1))
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 "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\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, []) ->
let p = prefix in
prefix_ := prefix^"\t";
Format.fprintf fmt "%sif (%a) {\n%a%s}\n"
p
cp_value (v, hloc)
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"
p
cp_value (v, hloc)
cp_block (b1, hloc)
p
cp_block (b2, hloc)
p;
prefix_ := p
(** [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) =
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 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 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"
| 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 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"
| 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\\n\"%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
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(&state);\n"
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;\n\
\tstate.is_init = true;\n\
\tstate.is_reset = false;\n\
\twhile(true) {\n\
\t\tscanf(\"%%s\", _buffer);\n\
\t\tif(!strcmp(_buffer, \"exit\")) { break; }\n\
\t\tsscanf(_buffer, %a);\n%a\
\t\tfn_main(&state, %a);\n\
\t\tprintf(%a);\n\
\t}\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 ()

120
src/ctranslation.ml
View File

@ -1,120 +0,0 @@
open Ast
open Intermediate_ast
open Cast
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 "Should not happened."
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
| [v] ->
begin
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
| _ -> failwith "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) ->
CAssign (fetch_unique_var (),
CMonOp (op, iexpression_to_cvalue e))
| IEBinOp (op, e, e') ->
CAssign (fetch_unique_var (),
CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e'))
| 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 "should not happened due to the linearization pass."
) l
| _ -> failwith "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)
| IETuple _ -> failwith "linearization should have \
transformed the tuples of the right members."
| IEWhen (expr, cond) ->
begin
CIf (iexpression_to_cvalue cond,
[equation_to_expression (node_st, node_sts, (vl, expr))],
[])
end
| IETriOp (TOp_if, _, _, _) ->
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 (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"
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 ->
begin
if c = c' then
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',
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,
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 ->
stmt :: merge_neighbour_ifs (stmt' :: b)

75
src/intermediate_ast.ml
View File

@ -1,75 +0,0 @@
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 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_<node name>;
*)
type node_state =
{
nt_name: string;
nt_nb_int : int;
nt_nb_real: int;
nt_nb_bool: int;
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;
}
type c_var =
| CVStored of string * int
| CVInput of ident
type i_expression =
| 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 *)
| IEApp of int * t_node * i_expression
and i_varlist = t_var list
and i_equation = i_varlist * i_expression
and i_eqlist = i_equation list
and i_node =
{
in_name : ident;
in_inputs: i_varlist;
in_outputs: i_varlist;
in_local_vars: i_varlist;
in_equations: i_eqlist;
}
type i_nodelist = i_node list
type node_states = (ident, node_state) Hashtbl.t

50
src/intermediate_utils.ml
View File

@ -1,50 +0,0 @@
open Intermediate_ast
let rec find_app_opt eqs i =
let rec find_app_expr_opt i = function
| 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
| IETriOp (_, 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
| 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
(** [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
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
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

1
src/lexer.mll
View File

@ -26,7 +26,6 @@
("merge", TO_merge); ("merge", TO_merge);
("when", WHEN); ("when", WHEN);
("reset", RESET); ("reset", RESET);
("every", EVERY);
("pre", MO_pre); ("pre", MO_pre);
("true", CONST_BOOL(true)); ("true", CONST_BOOL(true));
("false", CONST_BOOL(false)); ("false", CONST_BOOL(false));

99
src/main.ml
View File

@ -9,46 +9,24 @@ let print_debug d s =
let print_verbose v s = let print_verbose v s =
if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else () 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 =
(** [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 let rec aux ast = function
| [] -> f ast | [] -> f ast
| (n, p) :: passes -> | (n, p) :: passes ->
verbose (Format.asprintf "Executing pass %s:\n" n); verbose (Format.asprintf "Executing pass %s:\n" n);
try match p verbose debug main_fn ast with
begin | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
match p verbose debug ast with | Some ast -> (
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0) debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast);
| Some ast -> ( aux ast passes)
debug
(Format.asprintf
"Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
aux ast passes)
end with
| _ -> failwith ("The pass "^n^" should have caught me!")
in in
aux ast passes aux ast passes
let _ = let _ =
(** Usage and argument parsing. *) (** Usage and argument parsing. *)
let default_passes = let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in
["linearization_reset"; "remove_if"; let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
"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 = let usage_msg =
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
[-o output_file] [-m main_function] source_file\n" in [-o output_file] [-m main_function] source_file\n" in
@ -56,6 +34,7 @@ let _ =
let debug = ref false in let debug = ref false in
let ppast = ref false in let ppast = ref false in
let nopopt = ref false in let nopopt = ref false in
let simopt = ref false in
let passes = ref [] in let passes = ref [] in
let source_file = ref "" in let source_file = ref "" in
let testopt = ref false in let testopt = ref false in
@ -72,6 +51,7 @@ let _ =
("-debug", Arg.Set debug, "Output a lot of debug information"); ("-debug", Arg.Set debug, "Output a lot of debug information");
("-p", Arg.String (fun s -> passes := s :: !passes), ("-p", Arg.String (fun s -> passes := s :: !passes),
"Add a pass to the compilation process"); "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])"); ("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])");
] in ] in
Arg.parse speclist anon_fun usage_msg ; Arg.parse speclist anon_fun usage_msg ;
@ -79,20 +59,17 @@ let _ =
if !passes = [] then passes := default_passes; if !passes = [] then passes := default_passes;
let print_verbose = print_verbose !verbose in let print_verbose = print_verbose !verbose in
let print_debug = print_debug !debug in let print_debug = print_debug !debug in
let main_fn = "main" in
(** Definition of the passes table *) (** Definition of the passes table *)
let passes_table = Hashtbl.create 100 in let passes_table = Hashtbl.create 100 in
List.iter (fun (s, k) -> Hashtbl.add passes_table s k) List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
[ [
("remove_if", Passes.pass_if_removal); ("pre2vars", Passes.pre2vars);
("linearization_tuples", Passes.pass_linearization_tuples); ("chkvar_init_unicity", Passes.chkvar_init_unicity);
("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_translation", Passes.automata_translation_pass);
("automata_validity", Passes.check_automata_validity); ("automata_validity", Passes.check_automata_validity);
("linearization", Passes.pass_linearization);
("equations_ordering", Passes.pass_eq_reordering); ("equations_ordering", Passes.pass_eq_reordering);
("check_typing", Passes.pass_typing); ("check_typing", Passes.pass_typing);
("clock_unification", Passes.clock_unification_pass); ("clock_unification", Passes.clock_unification_pass);
@ -116,7 +93,7 @@ let _ =
begin begin
close_in_noerr inchan; close_in_noerr inchan;
Format.printf "Syntax error at %a: %s\n\n" Format.printf "Syntax error at %a: %s\n\n"
Lustre_pp.pp_loc (l, !source_file) s; Pp.pp_loc (l, !source_file) s;
exit 0 exit 0
end end
| Parsing.Parse_error -> | Parsing.Parse_error ->
@ -124,16 +101,11 @@ let _ =
close_in_noerr inchan; close_in_noerr inchan;
Parsing.( Parsing.(
Format.printf "Syntax error at %a\n\n" Format.printf "Syntax error at %a\n\n"
Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file)); Pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
exit 0 exit 0
end end
in 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 = let passes =
List.map List.map
(fun (pass: string) -> (pass, (fun (pass: string) -> (pass,
@ -149,21 +121,26 @@ let _ =
in in
print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
Lustre_pp.pp_ast ast) ; Pp.pp_ast ast) ;
exec_passes ast print_verbose print_debug passes exec_passes ast main_fn print_verbose print_debug passes
begin begin
if !ppast if !simopt
then (Format.printf "%a" Lustre_pp.pp_ast) then Simulation.simulate main_fn
else ( else
if !nopopt begin
then (fun _ -> ()) if !ppast
else then (Format.printf "%a" Pp.pp_ast)
( else (
let oc = open_out !output_file in if !nopopt
let fmt = Format.make_formatter then (fun _ -> ())
(Stdlib.output_substring oc) else
(fun () -> Stdlib.flush oc) in (
Ast_to_c.ast_to_c fmt print_verbose print_debug); let oc = open_out !output_file in
) let fmt = Format.make_formatter
end (Stdlib.output_substring oc)
(fun () -> Stdlib.flush oc) in
Format.fprintf fmt "%a" Ast_to_c.ast_to_c);
)
end
end

33
src/parser.mly
View File

@ -63,7 +63,7 @@
let make_binop_nonbool e1 e2 op error_msg = let make_binop_nonbool e1 e2 op error_msg =
let t1 = type_exp e1 in let t2 = type_exp e2 in let t1 = type_exp e1 in let t2 = type_exp e2 in
(** e1 and e2 should be numbers here.*) (** e1 and e2 should be nunmbers here.*)
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]] if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
then then
begin begin
@ -88,7 +88,7 @@
let make_comp_nonbool e1 e2 op error_msg = let make_comp_nonbool e1 e2 op error_msg =
let t1 = type_exp e1 in let t2 = type_exp e2 in let t1 = type_exp e1 in let t2 = type_exp e2 in
(** e1 and e2 should be numbers here.*) (** e1 and e2 should be nunmbers here.*)
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]] if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
then then
begin begin
@ -144,7 +144,6 @@
%token WHEN %token WHEN
%token RESET %token RESET
%token EVERY
%token IF %token IF
%token THEN %token THEN
@ -216,8 +215,8 @@ node_content:
if vars_distinct e_in e_out (snd $10) if vars_distinct e_in e_out (snd $10)
then (Hashtbl.add defined_nodes node_name n; n) then (Hashtbl.add defined_nodes node_name n; n)
else raise (MyParsingError else raise (MyParsingError
("There is a conflict between the names of local,\ ("There is a conflict between the names of local, input \
input or output variables.", or output variables.",
current_location())) current_location()))
end}; end};
@ -313,33 +312,33 @@ expr:
| MO_pre expr { EMonOp (type_exp $2, MOp_pre, $2) } | MO_pre expr { EMonOp (type_exp $2, MOp_pre, $2) }
| MINUS expr | MINUS expr
{ monop_neg_condition $2 [TBool] { monop_neg_condition $2 [TBool]
"You cannot take the opposite of an expression that is not a number." "You cannot take the opposite of a boolean expression."
(EMonOp (type_exp $2, MOp_minus, $2)) } (EMonOp (type_exp $2, MOp_minus, $2)) }
| PLUS expr | PLUS expr
{ monop_neg_condition $2 [TBool] { monop_neg_condition $2 [TBool]
"(+) expects its argument to be a number." $2 } "You cannot take the plus of a boolean expression." $2 }
/* Binary operators */ /* Binary operators */
| expr PLUS expr | expr PLUS expr
{ make_binop_nonbool $1 $3 BOp_add { make_binop_nonbool $1 $3 BOp_add
"Addition expects both arguments to be (the same kind of) numbers." } "You should know better; addition hates booleans" }
| expr MINUS expr | expr MINUS expr
{ make_binop_nonbool $1 $3 BOp_sub { make_binop_nonbool $1 $3 BOp_sub
"Substraction expects both arguments to be (the same kind of) numbers." } "You should know better; subtraction hates booleans" }
| expr BO_mul expr | expr BO_mul expr
{ make_binop_nonbool $1 $3 BOp_mul { make_binop_nonbool $1 $3 BOp_mul
"Multiplication expects both arguments to be (the same kind of) numbers." } "You should know better; multiplication hates booleans" }
| expr BO_div expr | expr BO_div expr
{ make_binop_nonbool $1 $3 BOp_div { make_binop_nonbool $1 $3 BOp_div
"Division expects both arguments to be (the same kind of) numbers." } "You should know better; division hates booleans" }
| expr BO_mod expr | expr BO_mod expr
{ make_binop_nonbool $1 $3 BOp_mod { make_binop_nonbool $1 $3 BOp_mod
"Modulo expects both arguments to be numbers." } "You should know better; modulo hates booleans" }
| expr BO_and expr | expr BO_and expr
{ make_binop_bool $1 $3 BOp_and { make_binop_bool $1 $3 BOp_and
"Conjunction expects both arguments to be booleans." } "You should know better; conjunction hates numbers" }
| expr BO_or expr | expr BO_or expr
{ make_binop_bool $1 $3 BOp_or { make_binop_bool $1 $3 BOp_or
"Disjunction expects both arguments to be booleans." } "You should know better; disjunction hates numbers" }
| expr BO_arrow expr | expr BO_arrow expr
{ let e1 = $1 in let t1 = type_exp e1 in { let e1 = $1 in let t1 = type_exp e1 in
let e2 = $3 in let t2 = type_exp e2 in let e2 = $3 in let t2 = type_exp e2 in
@ -382,9 +381,9 @@ expr:
then EWhen (t1, e1, e2) then EWhen (t1, e1, e2)
else raise (MyParsingError ("The when does not type-check!", else raise (MyParsingError ("The when does not type-check!",
current_location())) } current_location())) }
| RESET expr EVERY expr | expr RESET expr
{ let e1 = $2 in let t1 = type_exp e1 in { let e1 = $1 in let t1 = type_exp e1 in
let e2 = $4 in let t2 = type_exp e2 in let e2 = $3 in let t2 = type_exp e2 in
if t2 = [TBool] if t2 = [TBool]
then EReset (t1, e1, e2) then EReset (t1, e1, e2)
else raise (MyParsingError ("The reset does not type-check!", else raise (MyParsingError ("The reset does not type-check!",

723
src/passes.ml
View File

@ -4,544 +4,92 @@ open Ast
open Passes_utils open Passes_utils
open Utils open Utils
let pre2vars verbose debug main_fn =
let rec all_pre expr =
(** [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 (** new variables are called «_ifrem[varcount]» *)
(** 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 ->
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
(** 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 match expr with
| EConst _ | EVar _ -> [], vars, eq | EMonOp (ty, MOp_pre, expr) -> all_pre expr
| EMonOp (t, op, e) -> | EMonOp _ -> false
let eqs, vars, (patt, e) = aux_eq vars (patt, e) in | EVar _ -> true
eqs, vars, (patt, EMonOp (t, op, e)) | _ -> false
| 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 in
(** For each node, apply the previous function to all equations. *) let rec pre_push expr : t_expression =
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
(** [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.
* 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] 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
* - 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) (patt, expr) ->
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:
* 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 match expr with
| ETuple (_, expr_h :: expr_t) -> | EVar _ -> EMonOp (type_exp expr, MOp_pre, expr)
| EConst _ -> expr (** pre(c) = c for any constant c *)
| EMonOp (ty, mop, expr) ->
begin begin
let t_l = type_exp expr_h in match mop with
let patt_l, patt_r = list_select (List.length t_l) (snd patt) in | MOp_pre ->
let t_r = List.flatten (List.map type_var patt_r) in if all_pre expr
((t_l, patt_l), expr_h) :: then EMonOp (ty, mop, EMonOp (ty, mop, expr))
split_tuple ((t_r, patt_r), ETuple (t_r, expr_t)) else pre_push (pre_push expr)
| _ -> EMonOp (ty, mop, pre_push expr)
end end
| ETuple (_, []) -> [] | EBinOp (ty, bop, expr, expr') ->
| _ -> [eq] 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 in
(** For each node, apply the previous function to all equations. let rec aux (expr: t_expression) =
* 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
(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)))
| 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
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 (* 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 match expr with
| EConst _ | EVar _ -> [], vars, expr | EVar _ -> expr
| EMonOp (t, op, expr) -> | EMonOp (ty, mop, expr) ->
let eqs, vars, expr = aux_expr vars expr in begin
eqs, vars, EMonOp (t, op, expr) match mop with
| EBinOp (t, op, e, e') -> | MOp_pre -> pre_push expr
let eqs, vars, e = aux_expr vars e in | _ -> let expr = aux expr in EMonOp (ty, mop, expr)
let eqs', vars, e' = aux_expr vars e' in end
eqs @ eqs', vars, EBinOp (t, op, e, e') | EBinOp (ty, bop, expr, expr') ->
| ETriOp (t, op, e, e', e'') -> let expr = aux expr in let expr' = aux expr' in
let eqs, vars, e = aux_expr vars e in EBinOp (ty, bop, expr, expr')
let eqs', vars, e' = aux_expr vars e' in | ETriOp (ty, top, expr, expr', expr'') ->
let eqs'', vars, e'' = aux_expr vars e'' in let expr = aux expr in let expr' = aux expr' in
eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') let expr'' = aux expr'' in
| EComp (t, op, e, e') -> ETriOp (ty, top, expr, expr', expr'')
let eqs, vars, e = aux_expr vars e in | EComp (ty, cop, expr, expr') ->
let eqs', vars, e' = aux_expr vars e' in let expr = aux expr in let expr' = aux expr' in
eqs @ eqs', vars, EComp (t, op, e, e') EComp (ty, cop, expr, expr')
| EWhen (t, e, e') -> | EWhen (ty, expr, expr') ->
let eqs, vars, e = aux_expr vars e in let expr = aux expr in let expr' = aux expr' in
let eqs', vars, e' = aux_expr vars e' in EWhen (ty, expr, expr')
eqs @ eqs', vars, EWhen (t, e, e') | EReset (ty, expr, expr') ->
| EReset (t, e, e') -> let expr = aux expr in let expr' = aux expr' in
let eqs, vars, e = aux_expr vars e in EReset (ty, expr, expr')
let eqs', vars, e' = aux_expr vars e' in | EConst (ty, c) -> EConst (ty, c)
eqs @ eqs', vars, EReset (t, e, e') | ETuple (ty, elist) ->
| ETuple (t, l) -> let elist =
let eqs, vars, l = List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in
List.fold_right ETuple (ty, elist)
(fun e (eqs, vars, l) -> | EApp (ty, node, arg) ->
let eqs', vars, e = aux_expr vars e in let arg = aux arg in
eqs' @ eqs, vars, (e :: l)) EApp (ty, node, arg)
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 "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 "Should not happened (parser)"
in in
(** [aux_linearization_app] applies the previous function to every equation *) expression_pass (somify aux)
let aux_linearization_app node =
let new_equations, new_locvars =
List.fold_left
(fun (eqs, vars) eq ->
let eqs', vars, expr = aux_expr vars (snd eq) in
(fst eq, 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 aux_linearization_app
let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option =
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).
*
* 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 aux (node: t_node) : t_node option =
let incr_aux h n = let incr_aux h n =
match Hashtbl.find_opt h n with match Hashtbl.find_opt h n with
| None -> raise (PassExn "should not happened.") | None -> raise (PassExn "todo, should not happened.")
| Some num -> Hashtbl.replace h n (num + 1) | Some num -> Hashtbl.replace h n (num + 1)
in in
let incr_eq h (((_, patt), _): t_equation) = let incr_eq h (((_, patt), _): t_equation) =
@ -623,7 +171,114 @@ let rec tpl debug ((pat, exp): t_equation) =
| ETuple (_, []) -> [] | ETuple (_, []) -> []
| _ -> [(pat, exp)] | _ -> [(pat, exp)]
let pass_eq_reordering verbose debug ast = let pass_linearization verbose debug main_fn =
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 with
| 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'') ->
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 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
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 main_fn ast =
let rec pick_equations init_vars eqs remaining_equations = let rec pick_equations init_vars eqs remaining_equations =
match remaining_equations with match remaining_equations with
| [] -> Some eqs | [] -> Some eqs
@ -657,7 +312,7 @@ let pass_eq_reordering verbose debug ast =
in in
node_pass node_eq_reorganising ast node_pass node_eq_reorganising ast
let pass_typing verbose debug ast = let pass_typing verbose debug main_fn ast =
let htbl = Hashtbl.create (List.length ast) in let htbl = Hashtbl.create (List.length ast) in
let () = debug "[typing verification]" in let () = debug "[typing verification]" in
let () = List.iter let () = List.iter
@ -727,7 +382,7 @@ let pass_typing verbose debug ast =
else None else None
in aux ast in aux ast
let check_automata_validity verbos debug = let check_automata_validity verbos debug main_fn =
let check_automaton_branch_vars automaton = let check_automaton_branch_vars automaton =
let (init, states) = automaton in let (init, states) = automaton in
let left_side = Hashtbl.create 10 in let left_side = Hashtbl.create 10 in
@ -838,7 +493,7 @@ let automaton_translation debug automaton =
in in
let rec translate_var s v explist ty = match explist with let rec translate_var s v explist ty = match explist with
| [] -> default_constant ty | [] -> default_constant ty (* TODO *)
| (state, exp)::q -> | (state, exp)::q ->
ETriOp(Utils.type_exp exp, TOp_if, ETriOp(Utils.type_exp exp, TOp_if,
EComp([TBool], COp_eq, EComp([TBool], COp_eq,
@ -884,10 +539,10 @@ let automata_trans_pass debug (node:t_node) : t_node option=
n_automata = []; (* not needed anymore *) n_automata = []; (* not needed anymore *)
} }
let automata_translation_pass verbose debug = let automata_translation_pass verbose debug main_fn =
node_pass (automata_trans_pass debug) node_pass (automata_trans_pass debug)
let clock_unification_pass verbose debug ast = let clock_unification_pass verbose debug main_fn ast =
let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
@ -946,8 +601,8 @@ let clock_unification_pass verbose debug ast =
| _ -> failure ("Merge format") | _ -> failure ("Merge format")
end end
| ETriOp(_, TOp_if, e1, e2, e3) -> | ETriOp(_, TOp_if, e1, e2, e3) ->
let (* Unused: c1 = compute_clock_exp e1 let 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"

13
src/lustre_pp.ml → src/pp.ml
View File

@ -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) Format.fprintf fmt "%s: bool, %a" h pp_varlist (tl, h' :: l)
| (TReal :: tl, RVar h :: h' :: l) -> | (TReal :: tl, RVar h :: h' :: l) ->
Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l) Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l)
| _ -> raise (MyTypeError "(1) This exception should not have beed be raised.") | _ -> raise (MyTypeError "This exception should not have beed be raised.")
let pp_expression = let pp_expression =
let upd_prefix s = s ^ " | " in let upd_prefix s = s ^ " | " in
@ -45,14 +45,11 @@ let pp_expression =
let rec pp_expression_list prefix fmt exprs = let rec pp_expression_list prefix fmt exprs =
match exprs with match exprs with
| ETuple([], []) -> () | ETuple([], []) -> ()
| ETuple (typs, expr :: exprs) -> | ETuple (_ :: tt, expr :: exprs) ->
let typ_h, typ_t =
Utils.list_select (List.length (Utils.type_exp expr)) typs in
Format.fprintf fmt "%a%a" Format.fprintf fmt "%a%a"
(pp_expression_aux (prefix^" |> ")) expr (pp_expression_aux (prefix^" |> ")) expr
(pp_expression_list prefix) (ETuple (typ_t, exprs)) (pp_expression_list prefix) (ETuple (tt, exprs))
| ETuple (_, []) -> failwith "An empty tuple has a type!" | _ -> raise (MyTypeError "This exception should not have been raised.")
| _ -> failwith "This exception should never occur."
in in
match expression with match expression with
| EWhen (_, e1, e2) -> | EWhen (_, e1, e2) ->
@ -73,7 +70,7 @@ let pp_expression =
begin match c with begin match c with
| CBool b -> Format.fprintf fmt "\t\t\t%s<%s : bool>\n" prefix (Bool.to_string b) | 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 | CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: real>\n" prefix r | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r
end end
| EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v | EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v
| EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v | EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v

92
src/simulation.ml Normal file
View File

@ -0,0 +1,92 @@
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

21
src/test.node
View File

@ -1,18 +1,21 @@
node id_int (i: int) returns (o: int); node diagonal_int (i: int) returns (o1, o2 : int);
let let
o = i -> i; (o1, o2) = (i, i);
tel tel
node aux (i, j: int) returns (o: int); node undiag_test (i: int) returns (o : bool);
var l1, l2: int; l3: int;
let let
o = id_int(i) + id_int(j); l3 = (pre (1)) -> 0;
(l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel tel
node main (i: int) returns (a, b: int); node auto (i: int) returns (o : int);
var tmp: int; var x, y:int;
let let
a = 1; automaton
b = aux (i, a); | Incr -> do (o,x) = (0 fby o + 1, 2); done
tmp = aux (a+b, i); | Decr -> do (o,x) = diagonal_int(0 fby o); done
tel tel

18
src/test2.node
View File

@ -1,15 +1,13 @@
node aux (i: int) returns (a, b: int); node main (i: int) returns (o1: int);
let let
a = 1 -> pre i; o1 = 10 -> pre (20 -> 30);
b = 2 * i -> (3 * pre i);
tel tel
node n (i: int) returns (o1, o2: int); node flipflop(i: int) returns (z: int);
var u1, u2, t1, t2: int; c: bool; var x, y: int; c: bool;
let let
c = true -> not pre c; c = true fby (not c);
(t1, t2) = aux (i) when c; x = 1 on c;
(u1, u2) = aux (i) when (not c); y = 2 on (not c);
o1 = merge c t1 u1; z = merge c x y;
o2 = merge c t2 u2;
tel tel

0
tests/test_pre.node → src/test_pre.node
View File

13
src/utils.ml
View File

@ -9,13 +9,6 @@ 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
@ -104,9 +97,3 @@ let rec vars_of_expr (expr: t_expression) : ident list =
let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist = let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist =
(fst l1 @ fst l2, snd l1 @ snd l2) (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)

21
tests/test.node
View File

@ -1,21 +0,0 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let
(o1, o2) = (i, i);
tel
node undiag_test (i: int) returns (o : bool);
var l1, l2: int; l3: int;
let
l3 = (pre (1)) -> 0;
(l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel
node auto (i: int) returns (o : int);
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); done
| Decr -> do (o,x) = diagonal_int(0 fby o); done
tel

11
tests/test2.node
View File

@ -1,11 +0,0 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let
(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