Compare commits
113 Commits
b4ae058bf6
...
master
Author | SHA1 | Date | |
---|---|---|---|
0349304632 | |||
|
66de13fff2 | ||
|
17e2f93629 | ||
b0545a2733 | |||
1297835bda | |||
|
a5f8c720f4 | ||
|
ad4f5e7962 | ||
|
2da1fac66f | ||
|
ad74146396 | ||
|
2f0b9a572e | ||
|
42cbc6ddaf | ||
|
23e234732f | ||
|
ad97c6b627 | ||
68d67bb53b | |||
|
b2aa8bc6d5 | ||
|
094f403f5f | ||
|
30f9c71294 | ||
|
fef64987de | ||
b168161b4f | |||
|
f8c673632e | ||
69e84f0a8e | |||
5cabb042fc | |||
|
ff9da14379 | ||
9d7588f103 | |||
|
8c3e3d1eac | ||
|
a673c447e3 | ||
|
03def2ce1a | ||
|
ffa8918330 | ||
|
24108925fd | ||
fd95446636 | |||
19524ea99c | |||
88c145a527 | |||
|
52092b1480 | ||
|
f121f55432 | ||
|
42536df81c | ||
|
c7edb27fb0 | ||
|
3ad133344a | ||
4303dcd0e4 | |||
|
f5daae824c | ||
9fbdb7000f | |||
e1de3e6829 | |||
657fe7e6fa | |||
|
91ff654fc9 | ||
025d25a146 | |||
10838d3f2d | |||
e63123d8f6 | |||
|
01d4a08e8a | ||
|
9483f7df5e | ||
9a0bfd468c | |||
609870755c | |||
|
906a3d948b | ||
|
249ac37934 | ||
|
1d39173e94 | ||
|
4ff193759b | ||
|
c52dce6c02 | ||
|
c344f125e5 | ||
|
aa7f7514d3 | ||
|
77c865e360 | ||
ade62ba678 | |||
02130cf57c | |||
273a868162 | |||
37dfcdda35 | |||
c3a64a2bae | |||
|
1491e279f7 | ||
|
ce686f6c9a | ||
|
1d4e1820e4 | ||
|
007c5b2862 | ||
|
243e8f245a | ||
|
791af71913 | ||
|
233b385608 | ||
|
7a32d474d4 | ||
|
cbc834b32a | ||
|
a877501cca | ||
|
3cbfaeb2a8 | ||
|
916c7f544b | ||
|
6291957be5 | ||
|
bb99a5882b | ||
|
0da0f58b22 | ||
|
fa052f70e2 | ||
0175749296 | |||
|
4054da7d47 | ||
|
fc0a12fa12 | ||
edfec42738 | |||
d06fccf36b | |||
b616bad07a | |||
7a0f54f291 | |||
dbf1583ffd | |||
9e96697991 | |||
|
aa84a07902 | ||
|
ed54fd0114 | ||
|
b69b6998ec | ||
73b753bec2 | |||
a0383dbf13 | |||
530f6ddf51 | |||
|
57dd9c1aa4 | ||
21414e6461 | |||
c37e819f1a | |||
ea94bb84dd | |||
|
3fa0f92233 | ||
|
3417d75620 | ||
f55cd56fde | |||
012131e035 | |||
b58b250532 | |||
78e096d2f4 | |||
621658e177 | |||
85ecea0b9e | |||
7c2c43fe24 | |||
|
c7a97f3305 | ||
|
8d6349dd3f | ||
|
d7f0f148e9 | ||
|
9987922e0f | ||
|
6af9ddf394 | ||
|
1b3af051b3 |
8
TODO
8
TODO
@@ -1,8 +0,0 @@
|
||||
# Parseur
|
||||
|
||||
- tests divers et variés
|
||||
- support pour un point-virgule optionel en fin de nœud
|
||||
- ajout des flottants (= réels)
|
||||
- ajout de pre, ->, fby, automates
|
||||
|
||||
# ...
|
@@ -1,4 +1,11 @@
|
||||
\documentclass{beamer}
|
||||
\usepackage{listings}
|
||||
\lstset{
|
||||
basicstyle=\ttfamily,
|
||||
columns=fullflexible,
|
||||
frame=single,
|
||||
breaklines=true,
|
||||
}
|
||||
\usepackage{tikz}
|
||||
|
||||
\usetikzlibrary{positioning}
|
||||
@@ -6,6 +13,13 @@
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Presentation of our Lustre-to-C compiler}
|
||||
\subtitle{github.com/Benjamin-Loison/Synchronous-reactive-systems}
|
||||
\date{16 December 2022}
|
||||
\author{Benjamin Loison, Arnaud Daby-Seesaram, Antoine Grimod}
|
||||
|
||||
\frame{\titlepage}
|
||||
|
||||
\section{Structure of the compiler}
|
||||
\begin{frame}{Main ideas}
|
||||
\begin{figure}
|
||||
@@ -96,36 +110,137 @@
|
||||
\end{frame}
|
||||
|
||||
\section{Passes}
|
||||
\begin{frame}{Passes}
|
||||
\begin{frame}{}
|
||||
\begin{block}{Classification}
|
||||
The passes of our compiler are functions of taking a program and either:
|
||||
\begin{itemize}
|
||||
\item returning a program if the pass succeeded
|
||||
\item returns nothing otherwise
|
||||
\item node-passes: for all nodes, do \texttt{P: t\_node -> t\_node
|
||||
option}
|
||||
\pause
|
||||
\item equation-passes: for all equations of all nodes, do
|
||||
\texttt{P: t\_equation -> t\_equation option}
|
||||
(the definition uses the node-passes constructor)
|
||||
\pause
|
||||
\item expression-passes: for all expression of all equations, do
|
||||
\texttt{P: t\_expression -> t\_expression option}
|
||||
(the definition uses the equation-passes constructor)
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
\begin{frame}{Implemented Passes}
|
||||
\begin{block}{Sanity checks}
|
||||
\begin{itemize}
|
||||
\item Check the well-typedness of a program
|
||||
\pause
|
||||
\item Check that there are no assignment conflicts in a programs
|
||||
(node-pass)
|
||||
\pause
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\begin{block}{AST modification}
|
||||
\begin{itemize}
|
||||
\item Rewrite automata into \texttt{if-then-else} constructs
|
||||
(node-pass)
|
||||
\pause
|
||||
\item Linearization of the equations:
|
||||
\begin{itemize}
|
||||
\item for all, \texttt{pre e} add a, intermediate variable
|
||||
\item \texttt{v1, v2, v3 = f(i), e3;} is rewritten into
|
||||
\texttt{v1, v2 = f(i); v3 = e3;}
|
||||
\end{itemize}
|
||||
(node-pass)
|
||||
\pause
|
||||
\item (no longer required) Push the \texttt{pre} to variables
|
||||
(expression-pass)
|
||||
\end{itemize}
|
||||
|
||||
We only have one language in our compiler: no intermediary language.
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\subsection{Check}
|
||||
\begin{frame}[fragile]{Translation of automaton}
|
||||
\only<1>{\lstinputlisting[language=ml, firstline=1, lastline=7]{code/example_automaton.lus}}
|
||||
\only<2>{\lstinputlisting[language=ml, firstline=9, lastline=14]{code/example_automaton.lus}}
|
||||
\end{frame}
|
||||
\begin{frame}{Restriction on automaton}
|
||||
The patterns that appears on the left of equations must be the
|
||||
same in all branches
|
||||
|
||||
\only<2>{\lstinputlisting[language=ml, firstline=16, lastline=22]{code/example_automaton.lus}}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Clock unification}
|
||||
|
||||
Derived from the rules provided in \emph{Clock-directed Modular Code Generation for Synchronous
|
||||
Data-flow Languages}
|
||||
\end{frame}
|
||||
|
||||
\section{Translation to C}
|
||||
\begin{frame}
|
||||
|
||||
\texttt{ast\_to\_c.ml} architecture similar to Arnaud's AST pretty-printer.
|
||||
|
||||
\pause
|
||||
|
||||
For instance, go from \texttt{counting.lus} to \texttt{counting.c}.
|
||||
|
||||
\pause
|
||||
|
||||
Use of three tricks, as our compiler only manages \texttt{bool}s, \texttt{int}s and \texttt{float}s:
|
||||
\begin{enumerate}
|
||||
\item \texttt{0} can be interpreted as a \texttt{bool}, an \texttt{int} and a \texttt{float}
|
||||
\pause
|
||||
\item A \texttt{float} correctly encode \texttt{bool}s (\texttt{true} and \texttt{false}) and \texttt{int}s (between $[-2^{24} + 1; 2^{24} + 1]$)
|
||||
\pause
|
||||
\item To run an assignment of \texttt{value} to \texttt{variable} within the condition of a \texttt{if} and also make the cases of the \texttt{if} depends on a condition \texttt{condition}, we can do \texttt{if(((variable = value) \&\& false) || condition)}\\
|
||||
\pause
|
||||
We can also use this trick to execute an assignment and \textit{return} a value \texttt{value\_to\_return} without using any \texttt{;}, by using \texttt{((variable = value) || true) ? value\_to\_return : 0} (thanks to the first trick)
|
||||
\end{enumerate}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}
|
||||
\begin{block}{Passes}
|
||||
The passes can be split into:
|
||||
\begin{itemize}
|
||||
\item those checking the program validity
|
||||
\item those modifying the AST of the program
|
||||
\item
|
||||
\begin{itemize}
|
||||
\item \texttt{pp\_varlist (Base | Arg | Dec)}
|
||||
\item \texttt{pp\_retvarlist}
|
||||
\item \texttt{pp\_prevarlist}
|
||||
\item \texttt{pp\_asnprevarlist}
|
||||
\end{itemize}
|
||||
\pause
|
||||
\item \texttt{when} implementation error: division by zero for instance, so used the first trick (\texttt{when\_merge.node})
|
||||
\pause
|
||||
\item \texttt{->}: use global variable \texttt{init\_\{NODE\_NAME\}}\\
|
||||
\texttt{1 -> 2 -> 3} returns \texttt{0} on first run and only \texttt{3} on the following ones, correct? (\texttt{arrow.node})
|
||||
\pause
|
||||
\item \texttt{pre}
|
||||
\pause
|
||||
\item \texttt{reset}% (\texttt{reset})
|
||||
\pause
|
||||
\item Functions returning tuples thanks to Arnaud's linearization only have to deal with \texttt{(a0, a1, ..., an) = return\_tuple\_a0\_a1\_dots\_an(0)} (\texttt{function\_returning\_tuple.node})
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\section{Tests}
|
||||
\begin{frame}{Tests}
|
||||
\begin{block}{testing methods}
|
||||
We thought of three testing methods:
|
||||
\begin{itemize}
|
||||
\item manual testing of our functionalities
|
||||
\item run the sanity-checks-passes after any AST-altering pass
|
||||
\item simulation of the nodes (aborted)
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Implemented passes}
|
||||
\begin{block}{\texttt{pre}-propagation to leaves}
|
||||
\end{block}
|
||||
\begin{block}{Check: unique initialization for variables}
|
||||
\end{block}
|
||||
\begin{block}{Linearization of the equations}
|
||||
\end{block}
|
||||
\section{Possible improvements}
|
||||
\begin{frame}{Improvements}
|
||||
\begin{itemize}
|
||||
\item Increase the expressivity of the accepted programs
|
||||
\item Improve the complexity of the different passes
|
||||
\begin{itemize}
|
||||
\item Group neighbour passes of the same type (node-, expression or
|
||||
equation-pass).
|
||||
\end{itemize}
|
||||
\item \dots{}
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\end{document}
|
||||
|
22
beamer/code/example_automaton.lus
Normal file
22
beamer/code/example_automaton.lus
Normal file
@@ -0,0 +1,22 @@
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
|
||||
| Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1);
|
||||
o, x = if _s = 1 then (0 fby o + 1, 2) else if _s = 2 then diagonal_int(0 fby 0) else (0, 0);
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
|
||||
| Decr -> do (x,o) = diagonal_int(0 fby o); until o > 3 then Incr
|
||||
tel
|
@@ -55,7 +55,7 @@ and t_equation = t_varlist * t_expression
|
||||
|
||||
and t_eqlist = t_equation list
|
||||
|
||||
and t_state = | State of ident * t_eqlist * t_expression * ident
|
||||
and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list)
|
||||
|
||||
and t_automaton = t_state * t_state list
|
||||
|
||||
@@ -73,3 +73,8 @@ and t_node =
|
||||
|
||||
type t_nodelist = t_node list
|
||||
|
||||
type t_ck = base_ck list
|
||||
and base_ck =
|
||||
| Base
|
||||
| On of base_ck * t_expression
|
||||
| Unknown
|
||||
|
536
src/ast_to_c.ml
536
src/ast_to_c.ml
@@ -1,246 +1,324 @@
|
||||
open Ast
|
||||
open Intermediate_ast
|
||||
open Intermediate_utils
|
||||
open Cprint
|
||||
open Cast
|
||||
open Utils
|
||||
open Ctranslation
|
||||
|
||||
let pp_loc fmt (start, stop) =
|
||||
Lexing.(
|
||||
Format.fprintf fmt "%s: <l: %d, c: %d> -- <l: %d, c: %d>"
|
||||
start.pos_fname
|
||||
start.pos_lnum start.pos_cnum
|
||||
stop.pos_lnum stop.pos_cnum)
|
||||
|
||||
type var_list_delim =
|
||||
| Base
|
||||
| Arg
|
||||
| Dec
|
||||
|
||||
let rec pp_varlist var_list_delim fmt : t_varlist -> unit = function
|
||||
| ([], []) -> ()
|
||||
| ([TInt] , IVar h :: []) -> Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s"
|
||||
| Arg -> "int %s"
|
||||
| Dec -> "int %s;") h
|
||||
| ([TReal], RVar h :: []) -> Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s"
|
||||
| Arg -> "float %s"
|
||||
| Dec -> "float %s;") h
|
||||
| ([TBool], BVar h :: []) -> Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s"
|
||||
| Arg -> "bool %s"
|
||||
| Dec -> "bool %s;") h
|
||||
| (TInt :: tl, IVar h :: h' :: l) ->
|
||||
Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s, %a"
|
||||
| Arg -> "int %s, %a"
|
||||
| Dec -> "int %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
|
||||
| (TBool :: tl, BVar h :: h' :: l) ->
|
||||
Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s, %a"
|
||||
| Arg -> "bool %s, %a"
|
||||
| Dec -> "bool %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
|
||||
| (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt (
|
||||
match var_list_delim with
|
||||
| Base -> "%s, %a"
|
||||
| Arg -> "float %s, %a"
|
||||
| Dec -> "float %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
|
||||
let rec pp_retvarlist fmt : t_varlist -> unit = function
|
||||
| ([], []) -> ()
|
||||
| ([TInt] , IVar h :: []) -> Format.fprintf fmt "int"
|
||||
| ([TReal], RVar h :: []) -> Format.fprintf fmt "float"
|
||||
| ([TBool], BVar h :: []) -> Format.fprintf fmt "bool"
|
||||
| (TInt :: tl, IVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "int, %a" pp_retvarlist (tl, h' :: l)
|
||||
| (TBool :: tl, BVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "float, %a" pp_retvarlist (tl, h' :: l)
|
||||
| (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "bool, %a" pp_retvarlist (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
|
||||
let rec pp_prevarlist node_name fmt : t_varlist -> unit = function
|
||||
| ([], []) -> ()
|
||||
| ([TInt] , IVar h :: []) -> Format.fprintf fmt "int pre_%s_%s;" node_name h
|
||||
| ([TReal], RVar h :: []) -> Format.fprintf fmt "float pre_%s_%s;" node_name h
|
||||
| ([TBool], BVar h :: []) -> Format.fprintf fmt "bool pre_%s_%s;" node_name h
|
||||
| (TInt :: tl, IVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "int pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
|
||||
| (TBool :: tl, BVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "float pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
|
||||
| (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "bool pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
|
||||
let rec pp_asnprevarlist node_name fmt : t_varlist -> unit = function
|
||||
| ([], []) -> ()
|
||||
| ([TInt] , IVar h :: []) | ([TReal], RVar h :: []) | ([TBool], BVar h :: []) -> Format.fprintf fmt "\tpre_%s_%s = %s;" node_name h h
|
||||
| (TInt :: tl, IVar h :: h' :: l) | (TBool :: tl, BVar h :: h' :: l) | (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "\tpre_%s_%s = %s;\n%a" node_name h h (pp_asnprevarlist node_name) (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
|
||||
let reset_expressions_counter = ref 0;;
|
||||
|
||||
let 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.")
|
||||
(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *)
|
||||
let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist =
|
||||
let c = ref 1 in
|
||||
let ast_to_intermediate_ast_varlist vl = snd vl in
|
||||
let rec ast_to_intermediate_ast_expr hloc = function
|
||||
| EVar (_, v) ->
|
||||
begin
|
||||
match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
|
||||
| None -> IEVar (CVInput (name_of_var v))
|
||||
| Some (s, i) -> IEVar (CVStored (s, i))
|
||||
end
|
||||
| EMonOp (_, MOp_pre, EVar (_, v)) ->
|
||||
let s, i = Hashtbl.find hloc (Utils.name_of_var v, true) in
|
||||
IEVar (CVStored (s, i))
|
||||
| EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e)
|
||||
| EBinOp (_, op, e, e') ->
|
||||
IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
|
||||
| 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
|
||||
match expression with
|
||||
| EWhen (_, e1, e2) ->
|
||||
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
|
||||
Format.fprintf fmt "%a ? %a : 0"
|
||||
pp_expression_aux e2
|
||||
pp_expression_aux e1
|
||||
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
|
||||
| EReset (_, e1, e2) ->
|
||||
begin
|
||||
incr reset_expressions_counter;
|
||||
(* Use following trick as we can't use `;`:
|
||||
if(((var = val) && false) || condition)
|
||||
is equivalent to an incorrect statement like
|
||||
if({var = val; condition})
|
||||
We also use this trick with the fact that `0` can be interpreted as a `bool`, an `int` and a `float` *)
|
||||
(* could use C macros to simplify the C code *)
|
||||
Format.fprintf fmt "(((tmp_reset[%i] = %a) && false) || init_%s) ? (((init[%i] = tmp_reset[%i]) || true) ? tmp_reset[%i] : 0) : (%a ? init[%i] : tmp_reset[%i])"
|
||||
(!reset_expressions_counter - 1)
|
||||
pp_expression_aux e1
|
||||
node_name
|
||||
(!reset_expressions_counter - 1)
|
||||
(!reset_expressions_counter - 1)
|
||||
(!reset_expressions_counter - 1)
|
||||
pp_expression_aux e2
|
||||
(!reset_expressions_counter - 1)
|
||||
(!reset_expressions_counter - 1)
|
||||
end
|
||||
| EConst (_, c) ->
|
||||
begin match c with
|
||||
| CBool b -> Format.fprintf fmt "%s" (Bool.to_string b)
|
||||
| CInt i -> Format.fprintf fmt "%i" i
|
||||
| CReal r -> Format.fprintf fmt "%f" r
|
||||
end
|
||||
| EVar (_, IVar v) | EVar (_, BVar v) | EVar (_, RVar v) -> Format.fprintf fmt "%s" v
|
||||
| EMonOp (_, mop, arg) ->
|
||||
begin match mop with
|
||||
| MOp_not ->
|
||||
Format.fprintf fmt "!%a"
|
||||
pp_expression_aux arg
|
||||
| MOp_minus ->
|
||||
Format.fprintf fmt "-%a"
|
||||
pp_expression_aux arg
|
||||
| MOp_pre ->
|
||||
Format.fprintf fmt "pre_%s_%a" node_name
|
||||
pp_expression_aux arg
|
||||
end
|
||||
| EBinOp (_, BOp_arrow, arg, arg') ->
|
||||
Format.fprintf fmt "init_%s ? %a : %a"
|
||||
node_name
|
||||
pp_expression_aux arg
|
||||
pp_expression_aux arg'
|
||||
| EBinOp (_, bop, arg, arg') ->
|
||||
begin
|
||||
let s = match bop with
|
||||
| BOp_add -> " + " | BOp_sub -> " - "
|
||||
| BOp_mul -> " * " | BOp_div -> " / " | BOp_mod -> " % "
|
||||
| BOp_and -> " && " | BOp_or -> " || " | _ -> "" (* `ocamlc` doesn't detect that `BOp_arrow` can't match here *) in
|
||||
Format.fprintf fmt "%a%s%a"
|
||||
pp_expression_aux arg
|
||||
s
|
||||
pp_expression_aux arg'
|
||||
end
|
||||
| EComp (_, cop, arg, arg') ->
|
||||
begin
|
||||
let s = match cop with
|
||||
| COp_eq -> " == "
|
||||
| COp_neq -> " != "
|
||||
| COp_le -> " <= " | COp_lt -> " < "
|
||||
| COp_ge -> " >= " | COp_gt -> " > " in
|
||||
Format.fprintf fmt "%a%s%a"
|
||||
pp_expression_aux arg
|
||||
s
|
||||
pp_expression_aux arg'
|
||||
end
|
||||
| ETriOp (_, top, arg, arg', arg'') ->
|
||||
begin
|
||||
Format.fprintf fmt "%a ? %a : %a"
|
||||
pp_expression_aux arg
|
||||
pp_expression_aux arg'
|
||||
pp_expression_aux arg''
|
||||
end
|
||||
| EApp (_, f, args) ->
|
||||
Format.fprintf fmt "%s(%a)"
|
||||
f.n_name
|
||||
pp_expression_list args
|
||||
| ETuple _ ->
|
||||
Format.fprintf fmt "%a"
|
||||
pp_expression_list expression;
|
||||
in
|
||||
pp_expression_aux
|
||||
nodes
|
||||
|
||||
let rec pp_equations node_name fmt: t_eqlist -> unit = function
|
||||
(** The following function defines the [node_states] for the nodes of a program,
|
||||
* and puts them in a hash table. *)
|
||||
let make_state_types nodes: node_states =
|
||||
(* Hash table to fill *)
|
||||
let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in
|
||||
|
||||
(** [one_node node pv ty] computes the number of variables of type [ty] in
|
||||
* [node] and a mapping from the variables of type ([ty] * bool) to int,
|
||||
* where [pv] is a list of variables used in the pre construct in the
|
||||
* program. *)
|
||||
let one_node node pv ty =
|
||||
(* variables of type [ty] among output and local variables *)
|
||||
let vars =
|
||||
List.filter (fun v -> type_var v = [ty])
|
||||
(snd (varlist_concat node.n_outputs node.n_local_vars)) in
|
||||
let 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
|
||||
* the node [n].
|
||||
* Note that the only occurrence of pre are of the form pre (var), due to
|
||||
* the linearization pass.
|
||||
*)
|
||||
let find_prevars node =
|
||||
let rec find_prevars_expr = function
|
||||
| EConst _ | EVar _ -> []
|
||||
| EMonOp (_, MOp_pre, EVar (_, v)) -> [v]
|
||||
| EMonOp (_, _, e) -> find_prevars_expr e
|
||||
| ETriOp (_, _, e, e', e'') ->
|
||||
(find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'')
|
||||
| EComp (_, _, e, e')
|
||||
| EBinOp (_, _, e, e')
|
||||
| EWhen (_, e, e')
|
||||
| EReset (_, e, e') -> (find_prevars_expr e) @ (find_prevars_expr e')
|
||||
| ETuple (_, l) -> List.flatten (List.map (find_prevars_expr) l)
|
||||
| EApp (_, _, e) -> find_prevars_expr e
|
||||
in
|
||||
list_remove_duplicates
|
||||
(List.fold_left
|
||||
(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
|
||||
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
|
||||
|
||||
(** 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
|
||||
in
|
||||
aux nodes
|
||||
|
||||
|
||||
|
||||
(** The following C-printer functions are in this file, as they need to work on
|
||||
* the AST and are not simple printers. *)
|
||||
|
||||
|
||||
|
||||
(** The following function prints the code to remember previous values of
|
||||
* variables used with the pre construct. *)
|
||||
let cp_prevars fmt (node, h) =
|
||||
let node_st = Hashtbl.find h node.in_name in
|
||||
match (Hashtbl.find h node.in_name).nt_prevars with
|
||||
| [] -> ()
|
||||
| (([], []), (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)
|
||||
| (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
|
||||
| l ->
|
||||
Format.fprintf fmt
|
||||
"\n\t/* Remember the values used in the [pre] construct */\n";
|
||||
List.iter
|
||||
(fun v -> (** Note that «dst_array = src_array» should hold. *)
|
||||
match Hashtbl.find_opt node_st.nt_map (v, false) with
|
||||
| Some (src_array, src_idx) ->
|
||||
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
|
||||
Format.fprintf fmt "\t_state->%s[%d] = _state->%s[%d];\n"
|
||||
dst_array dst_idx src_array src_idx
|
||||
| None ->
|
||||
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
|
||||
Format.fprintf fmt "\t_state->%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 *)
|
||||
Format.sprintf "float tmp_reset[%i], init[%i];" reset_expressions_counter reset_expressions_counter
|
||||
|
||||
(* TODO: manage general 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_MAIN}_{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%a %s(%a)\n{\n\t%a\n\n\t%a\n\n%a\n\tinit_%s = false;\n\n%a\n\n%a\n\n%a\n\n\treturn %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)
|
||||
pp_retvarlist node.n_outputs
|
||||
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_varlist Base) node.n_outputs
|
||||
|
||||
let rec pp_nodes fmt nodes =
|
||||
(** The following function defines the behaviour to have at the first
|
||||
* execution of a node, namely:
|
||||
* - initialize the states of auxiliary nodes
|
||||
*)
|
||||
let cp_init_aux_nodes fmt (node, h) =
|
||||
let rec aux fmt (node, nst, i) =
|
||||
match find_app_opt node.in_equations i with
|
||||
| None -> () (** All auxiliary nodes have been initialized *)
|
||||
| Some n ->
|
||||
begin
|
||||
Format.fprintf fmt "%a\t\tif(!_state->is_reset) {\n\
|
||||
\t\t\t_state->aux_states[%d] = calloc (1, sizeof (%s));\n\
|
||||
\t\t}\n\
|
||||
\t\t((%s*)(_state->aux_states[%d]))->is_init = true;\n\
|
||||
\t\t((%s*)(_state->aux_states[%d]))->is_reset = _state->is_reset;\n"
|
||||
aux (node, nst, i-1)
|
||||
(i-1) (Format.asprintf "t_state_%s" n.n_name)
|
||||
(Format.asprintf "t_state_%s" n.n_name) (i-1)
|
||||
(Format.asprintf "t_state_%s" n.n_name) (i-1)
|
||||
end
|
||||
in
|
||||
let nst = Hashtbl.find h node.in_name in
|
||||
if nst.nt_count_app = 0
|
||||
then ()
|
||||
else begin
|
||||
Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\
|
||||
\tif (_state->is_init) {\n%a\t}\n\n\n"
|
||||
aux (node, nst, nst.nt_count_app)
|
||||
end
|
||||
|
||||
|
||||
|
||||
(** [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\t_state->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
|
||||
| [] -> ()
|
||||
| node :: nodes ->
|
||||
Format.fprintf fmt "%a\n%a" pp_node node pp_nodes nodes
|
||||
Format.fprintf fmt "%a\n%a"
|
||||
cp_node (node, h)
|
||||
cp_nodes (nodes, h)
|
||||
|
||||
let ast_to_c fmt 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%a"
|
||||
pp_nodes prog
|
||||
|
||||
|
||||
(** [dump_var_locations] dumps the internal tables to map the program variable
|
||||
* (after all the passes) to their location in the final C program. *)
|
||||
let dump_var_locations fmt (st: node_states) =
|
||||
Format.fprintf fmt "Tables mapping the AST variables to the C variables:\n";
|
||||
Hashtbl.iter
|
||||
(fun n st ->
|
||||
Format.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#define BUFFER_SIZE 1024\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
Normal file
27
src/cast.ml
Normal file
@@ -0,0 +1,27 @@
|
||||
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
|
||||
|
@@ -3,3 +3,4 @@
|
||||
* variables. *)
|
||||
let maxvar = 100
|
||||
|
||||
let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"]
|
||||
|
454
src/cprint.ml
Normal file
454
src/cprint.ml
Normal file
@@ -0,0 +1,454 @@
|
||||
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_states[%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 "%s_state->%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 "%s_state->%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 _ -> "%hd"
|
||||
| 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[BUFFER_SIZE];\n\
|
||||
\tt_state_main _state;\n\
|
||||
\t_state.is_init = true;\n\
|
||||
\t_state.is_reset = false;\n\
|
||||
\twhile(true) {\n\
|
||||
\t\tprintf(\"input: \");\n\
|
||||
\t\tfor(unsigned short idx = 0; idx < BUFFER_SIZE; idx++) {\n\
|
||||
\t\t\tif(idx == (BUFFER_SIZE - 1) || (buffer[idx] = getchar()) == '\\n') {\n\
|
||||
\t\t\t\tbuffer[idx] = '\\0';\n\
|
||||
\t\t\t\tbreak;\n\
|
||||
\t\t\t}\n\
|
||||
\t\t}\n\
|
||||
\t\tif(!strcmp(buffer, \"exit\")) { break; }\n\
|
||||
\t\tsscanf(buffer, %a);\n%a\
|
||||
\t\tfn_main(&_state, %a);\n\
|
||||
\t\tprintf(\"output: \");\n\
|
||||
\t\tprintf(%a);\n\
|
||||
\t\tprintf(\"\\n\");\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
Normal file
120
src/ctranslation.ml
Normal file
@@ -0,0 +1,120 @@
|
||||
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
Normal file
75
src/intermediate_ast.ml
Normal file
@@ -0,0 +1,75 @@
|
||||
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
Normal file
50
src/intermediate_utils.ml
Normal file
@@ -0,0 +1,50 @@
|
||||
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
|
@@ -26,6 +26,7 @@
|
||||
("merge", TO_merge);
|
||||
("when", WHEN);
|
||||
("reset", RESET);
|
||||
("every", EVERY);
|
||||
("pre", MO_pre);
|
||||
("true", CONST_BOOL(true));
|
||||
("false", CONST_BOOL(false));
|
||||
|
@@ -37,7 +37,7 @@ let rec pp_varlist fmt : t_varlist -> unit = function
|
||||
Format.fprintf fmt "%s: bool, %a" h pp_varlist (tl, h' :: l)
|
||||
| (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
| _ -> raise (MyTypeError "(1) This exception should not have beed be raised.")
|
||||
|
||||
let pp_expression =
|
||||
let upd_prefix s = s ^ " | " in
|
||||
@@ -45,11 +45,14 @@ let pp_expression =
|
||||
let rec pp_expression_list prefix fmt exprs =
|
||||
match exprs with
|
||||
| ETuple([], []) -> ()
|
||||
| ETuple (_ :: tt, expr :: exprs) ->
|
||||
| ETuple (typs, expr :: exprs) ->
|
||||
let typ_h, typ_t =
|
||||
Utils.list_select (List.length (Utils.type_exp expr)) typs in
|
||||
Format.fprintf fmt "%a%a"
|
||||
(pp_expression_aux (prefix^" |> ")) expr
|
||||
(pp_expression_list prefix) (ETuple (tt, exprs))
|
||||
| _ -> raise (MyTypeError "This exception should not have been raised.")
|
||||
(pp_expression_list prefix) (ETuple (typ_t, exprs))
|
||||
| ETuple (_, []) -> failwith "An empty tuple has a type!"
|
||||
| _ -> failwith "This exception should never occur."
|
||||
in
|
||||
match expression with
|
||||
| EWhen (_, e1, e2) ->
|
||||
@@ -70,7 +73,7 @@ let pp_expression =
|
||||
begin match c with
|
||||
| CBool b -> Format.fprintf fmt "\t\t\t%s<%s : bool>\n" prefix (Bool.to_string b)
|
||||
| CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
|
||||
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r
|
||||
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: real>\n" prefix r
|
||||
end
|
||||
| EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v
|
||||
| EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v
|
||||
@@ -150,14 +153,22 @@ let rec pp_automata fmt: t_automaton list -> unit = function
|
||||
pp_translist trans
|
||||
pp_automata tail
|
||||
|
||||
and pp_nexts fmt: t_expression list * string list -> unit = function
|
||||
| [], [] -> ()
|
||||
| e::exprs, n::nexts ->
|
||||
Format.fprintf fmt "if %a then %s else %a"
|
||||
pp_expression e
|
||||
n
|
||||
pp_nexts (exprs, nexts)
|
||||
| _, _ -> () (*This should never happen*)
|
||||
|
||||
and pp_translist fmt: t_state list -> unit = function
|
||||
| [] -> ()
|
||||
| State(name, eqs, cond, next)::q ->
|
||||
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a"
|
||||
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a"
|
||||
name
|
||||
pp_equations eqs
|
||||
pp_expression cond
|
||||
next
|
||||
pp_nexts (cond, next)
|
||||
pp_translist q
|
||||
|
||||
let pp_node fmt node =
|
77
src/main.ml
77
src/main.ml
@@ -9,24 +9,44 @@ let print_debug d s =
|
||||
let print_verbose v s =
|
||||
if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else ()
|
||||
|
||||
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
|
||||
| [] -> f ast
|
||||
| (n, p) :: passes ->
|
||||
verbose (Format.asprintf "Executing pass %s:\n" n);
|
||||
match p verbose debug main_fn ast with
|
||||
match p verbose debug ast with
|
||||
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
|
||||
| Some ast -> (
|
||||
debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast);
|
||||
debug
|
||||
(Format.asprintf
|
||||
"Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
|
||||
aux ast passes)
|
||||
in
|
||||
aux ast passes
|
||||
|
||||
|
||||
|
||||
let _ =
|
||||
(** Usage and argument parsing. *)
|
||||
let default_passes = ["pre2vars"; "linearization"; "equations_ordering"] in
|
||||
let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
|
||||
let default_passes =
|
||||
["linearization_reset"; "automata_translation"; "remove_if";
|
||||
"linearization_merge"; "linearization_when";
|
||||
"linearization_pre"; "linearization_tuples"; "linearization_app";
|
||||
"ensure_assign_val";
|
||||
"equations_ordering";
|
||||
"clock_unification"] in
|
||||
let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
|
||||
let usage_msg =
|
||||
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
|
||||
[-o output_file] [-m main_function] source_file\n" in
|
||||
@@ -34,7 +54,6 @@ let _ =
|
||||
let debug = ref false in
|
||||
let ppast = ref false in
|
||||
let nopopt = ref false in
|
||||
let simopt = ref false in
|
||||
let passes = ref [] in
|
||||
let source_file = ref "" in
|
||||
let testopt = ref false in
|
||||
@@ -51,7 +70,6 @@ let _ =
|
||||
("-debug", Arg.Set debug, "Output a lot of debug information");
|
||||
("-p", Arg.String (fun s -> passes := s :: !passes),
|
||||
"Add a pass to the compilation process");
|
||||
("-sim", Arg.Set simopt, "Simulate the main node");
|
||||
("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])");
|
||||
] in
|
||||
Arg.parse speclist anon_fun usage_msg ;
|
||||
@@ -59,17 +77,25 @@ let _ =
|
||||
if !passes = [] then passes := default_passes;
|
||||
let print_verbose = print_verbose !verbose in
|
||||
let print_debug = print_debug !debug in
|
||||
let main_fn = "main" in
|
||||
|
||||
(** Definition of the passes table *)
|
||||
let passes_table = Hashtbl.create 100 in
|
||||
List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
|
||||
[
|
||||
("pre2vars", Passes.pre2vars);
|
||||
("chkvar_init_unicity", Passes.chkvar_init_unicity);
|
||||
("linearization", Passes.pass_linearization);
|
||||
("remove_if", Passes.pass_if_removal);
|
||||
("linearization_merge", Passes.pass_merge_lin);
|
||||
("linearization_when", Passes.pass_when_lin);
|
||||
("linearization_tuples", Passes.pass_linearization_tuples);
|
||||
("linearization_app", Passes.pass_linearization_app);
|
||||
("linearization_pre", Passes.pass_linearization_pre);
|
||||
("ensure_assign_val", Passes.pass_ensure_assignment_value);
|
||||
("linearization_reset", Passes.pass_linearization_reset);
|
||||
("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity);
|
||||
("automata_translation", Passes.automata_translation_pass);
|
||||
("automata_validity", Passes.check_automata_validity);
|
||||
("equations_ordering", Passes.pass_eq_reordering);
|
||||
("check_typing", Passes.pass_typing);
|
||||
("clock_unification", Passes.clock_unification_pass);
|
||||
];
|
||||
|
||||
(** Main functionality below *)
|
||||
@@ -90,7 +116,7 @@ let _ =
|
||||
begin
|
||||
close_in_noerr inchan;
|
||||
Format.printf "Syntax error at %a: %s\n\n"
|
||||
Pp.pp_loc (l, !source_file) s;
|
||||
Lustre_pp.pp_loc (l, !source_file) s;
|
||||
exit 0
|
||||
end
|
||||
| Parsing.Parse_error ->
|
||||
@@ -98,11 +124,16 @@ let _ =
|
||||
close_in_noerr inchan;
|
||||
Parsing.(
|
||||
Format.printf "Syntax error at %a\n\n"
|
||||
Pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
|
||||
Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
|
||||
exit 0
|
||||
end
|
||||
in
|
||||
|
||||
(** Computes the list of passes to execute. If the [-test] flag is set, all
|
||||
* sanity passes (ie. passes which do not modify the AST, but ensure its
|
||||
* validity) are re-run after any other pass.
|
||||
*
|
||||
* Note: the sanity passes are always executed before any other. *)
|
||||
let passes =
|
||||
List.map
|
||||
(fun (pass: string) -> (pass,
|
||||
@@ -118,19 +149,21 @@ let _ =
|
||||
in
|
||||
|
||||
print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
|
||||
Pp.pp_ast ast) ;
|
||||
exec_passes ast main_fn print_verbose print_debug passes
|
||||
begin
|
||||
if !simopt
|
||||
then Simulation.simulate main_fn
|
||||
else
|
||||
Lustre_pp.pp_ast ast) ;
|
||||
exec_passes ast print_verbose print_debug passes
|
||||
begin
|
||||
if !ppast
|
||||
then (Format.printf "%a" Pp.pp_ast)
|
||||
then (Format.printf "%a" Lustre_pp.pp_ast)
|
||||
else (
|
||||
if !nopopt
|
||||
then (fun _ -> ())
|
||||
else Format.printf "%a" Ast_to_c.ast_to_c)
|
||||
end
|
||||
else
|
||||
(
|
||||
let oc = open_out !output_file in
|
||||
let fmt = Format.make_formatter
|
||||
(Stdlib.output_substring oc)
|
||||
(fun () -> Stdlib.flush oc) in
|
||||
Ast_to_c.ast_to_c fmt print_verbose print_debug);
|
||||
)
|
||||
end
|
||||
|
||||
|
@@ -63,7 +63,7 @@
|
||||
|
||||
let make_binop_nonbool e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
(** e1 and e2 should be nunmbers here.*)
|
||||
(** e1 and e2 should be numbers here.*)
|
||||
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
|
||||
then
|
||||
begin
|
||||
@@ -88,7 +88,7 @@
|
||||
|
||||
let make_comp_nonbool e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
(** e1 and e2 should be nunmbers here.*)
|
||||
(** e1 and e2 should be numbers here.*)
|
||||
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
|
||||
then
|
||||
begin
|
||||
@@ -144,6 +144,7 @@
|
||||
|
||||
%token WHEN
|
||||
%token RESET
|
||||
%token EVERY
|
||||
|
||||
%token IF
|
||||
%token THEN
|
||||
@@ -215,8 +216,8 @@ node_content:
|
||||
if vars_distinct e_in e_out (snd $10)
|
||||
then (Hashtbl.add defined_nodes node_name n; n)
|
||||
else raise (MyParsingError
|
||||
("There is a conflict between the names of local, input \
|
||||
or output variables.",
|
||||
("There is a conflict between the names of local,\
|
||||
input or output variables.",
|
||||
current_location()))
|
||||
end};
|
||||
|
||||
@@ -276,6 +277,7 @@ equations:
|
||||
| /* empty */ { [] }
|
||||
| equation SEMICOL equations
|
||||
{ $1 :: $3 }
|
||||
| equation OPTIONAL_SEMICOL { [$1] }
|
||||
;
|
||||
|
||||
equation:
|
||||
@@ -311,33 +313,33 @@ expr:
|
||||
| MO_pre expr { EMonOp (type_exp $2, MOp_pre, $2) }
|
||||
| MINUS expr
|
||||
{ monop_neg_condition $2 [TBool]
|
||||
"You cannot take the opposite of a boolean expression."
|
||||
"You cannot take the opposite of an expression that is not a number."
|
||||
(EMonOp (type_exp $2, MOp_minus, $2)) }
|
||||
| PLUS expr
|
||||
{ monop_neg_condition $2 [TBool]
|
||||
"You cannot take the plus of a boolean expression." $2 }
|
||||
"(+) expects its argument to be a number." $2 }
|
||||
/* Binary operators */
|
||||
| expr PLUS expr
|
||||
{ make_binop_nonbool $1 $3 BOp_add
|
||||
"You should know better; addition hates booleans" }
|
||||
"Addition expects both arguments to be (the same kind of) numbers." }
|
||||
| expr MINUS expr
|
||||
{ make_binop_nonbool $1 $3 BOp_sub
|
||||
"You should know better; subtraction hates booleans" }
|
||||
"Substraction expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_mul expr
|
||||
{ make_binop_nonbool $1 $3 BOp_mul
|
||||
"You should know better; multiplication hates booleans" }
|
||||
"Multiplication expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_div expr
|
||||
{ make_binop_nonbool $1 $3 BOp_div
|
||||
"You should know better; division hates booleans" }
|
||||
"Division expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_mod expr
|
||||
{ make_binop_nonbool $1 $3 BOp_mod
|
||||
"You should know better; modulo hates booleans" }
|
||||
"Modulo expects both arguments to be numbers." }
|
||||
| expr BO_and expr
|
||||
{ make_binop_bool $1 $3 BOp_and
|
||||
"You should know better; conjunction hates numbers" }
|
||||
"Conjunction expects both arguments to be booleans." }
|
||||
| expr BO_or expr
|
||||
{ make_binop_bool $1 $3 BOp_or
|
||||
"You should know better; disjunction hates numbers" }
|
||||
"Disjunction expects both arguments to be booleans." }
|
||||
| expr BO_arrow expr
|
||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||
let e2 = $3 in let t2 = type_exp e2 in
|
||||
@@ -380,9 +382,9 @@ expr:
|
||||
then EWhen (t1, e1, e2)
|
||||
else raise (MyParsingError ("The when does not type-check!",
|
||||
current_location())) }
|
||||
| expr RESET expr
|
||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||
let e2 = $3 in let t2 = type_exp e2 in
|
||||
| RESET expr EVERY expr
|
||||
{ let e1 = $2 in let t1 = type_exp e1 in
|
||||
let e2 = $4 in let t2 = type_exp e2 in
|
||||
if t2 = [TBool]
|
||||
then EReset (t1, e1, e2)
|
||||
else raise (MyParsingError ("The reset does not type-check!",
|
||||
@@ -434,9 +436,10 @@ ident_comma_list:
|
||||
|
||||
transition:
|
||||
| CASE IDENT BO_arrow DO equations DONE {
|
||||
State($2, $5, EConst([TBool], CBool(true)), $2) }
|
||||
| CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
|
||||
State($2, $5, $7, $9)}
|
||||
State($2, $5, [EConst([TBool], CBool(true))], [$2]) }
|
||||
| CASE IDENT BO_arrow DO equations UNTIL next_list {
|
||||
let (exprs, outs) = $7 in
|
||||
State($2, $5, exprs, outs)}
|
||||
;
|
||||
|
||||
transition_list:
|
||||
@@ -444,3 +447,8 @@ transition_list:
|
||||
| transition transition_list { $1 :: $2 }
|
||||
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
|
||||
;
|
||||
|
||||
next_list:
|
||||
| expr THEN IDENT { [$1], [$3] }
|
||||
| next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs }
|
||||
;
|
||||
|
1225
src/passes.ml
1225
src/passes.ml
File diff suppressed because it is too large
Load Diff
@@ -33,6 +33,9 @@ let expression_pass f: t_nodelist -> t_nodelist option =
|
||||
exception PassExn of string
|
||||
|
||||
let counter = ref 0
|
||||
let create_automaton_name : unit -> string = fun () ->
|
||||
let create_automaton_id : unit -> int = fun () ->
|
||||
counter := !counter + 1;
|
||||
Format.asprintf "_s%d" (!counter)
|
||||
!counter
|
||||
|
||||
let create_automaton_name id =
|
||||
Format.asprintf "_s%d" (id)
|
||||
|
@@ -1,92 +0,0 @@
|
||||
open Ast
|
||||
|
||||
type sim_var =
|
||||
| SIVar of ident * (int option)
|
||||
| SBVar of ident * (bool option)
|
||||
| SRVar of ident * (real option)
|
||||
|
||||
type sim_node_st =
|
||||
{
|
||||
node_outputs: sim_var list;
|
||||
node_loc_vars: sim_var list;
|
||||
node_inner_nodes: sim_node list;
|
||||
}
|
||||
and sim_node_step_fn =
|
||||
sim_node_st -> sim_var list -> (sim_var list * sim_node_st)
|
||||
and sim_node = sim_node_st * sim_node_step_fn
|
||||
|
||||
let pp_sim fmt ((sn, _): sim_node) =
|
||||
let rec aux fmt vars =
|
||||
match vars with
|
||||
| [] -> ()
|
||||
| SIVar (s, None) :: t ->
|
||||
Format.fprintf fmt "\t<%s : int> uninitialized yet.\n%a" s aux t
|
||||
| SBVar (s, None) :: t ->
|
||||
Format.fprintf fmt "\t<%s : bool> uninitialized yet.\n%a" s aux t
|
||||
| SRVar (s, None) :: t ->
|
||||
Format.fprintf fmt "\t<%s : real> uninitialized yet.\n%a" s aux t
|
||||
| SIVar (s, Some i) :: t ->
|
||||
Format.fprintf fmt "\t<%s : int> = %d\n%a" s i aux t
|
||||
| SBVar (s, Some b) :: t ->
|
||||
Format.fprintf fmt "\t<%s : bool> = %s\n%a" s (Bool.to_string b) aux t
|
||||
| SRVar (s, Some r) :: t ->
|
||||
Format.fprintf fmt "\t<%s : real> = %f\n%a" s r aux t
|
||||
in
|
||||
if sn.node_loc_vars <> []
|
||||
then
|
||||
Format.fprintf fmt "State of the simulated node:\n\
|
||||
\tOutput variables:\n%a
|
||||
\tLocal variables:\n%a"
|
||||
aux sn.node_outputs
|
||||
aux sn.node_loc_vars
|
||||
else
|
||||
Format.fprintf fmt "State of the simulated node:\n\
|
||||
\tOutput variables:\n%a
|
||||
\tThere are no local variables:\n"
|
||||
aux sn.node_outputs
|
||||
|
||||
|
||||
exception MySimulationException of string
|
||||
|
||||
let fetch_node (p: t_nodelist) (s: ident) : t_node =
|
||||
match List.filter (fun n -> n.n_name = s) p with
|
||||
| [e] -> e
|
||||
| _ -> raise (MySimulationException (Format.asprintf "Node %s undefined." s))
|
||||
|
||||
let fetch_var (l: sim_var list) (s: ident) =
|
||||
match List.filter
|
||||
(function
|
||||
| SBVar (v, _) | SRVar (v, _) | SIVar (v, _) -> v = s) l with
|
||||
| [v] -> v
|
||||
| _ -> raise (MySimulationException
|
||||
(Format.asprintf "Variable %s undefined." s))
|
||||
|
||||
(** TODO! *)
|
||||
let make_sim (main_fn: ident) (p: t_nodelist): sim_node =
|
||||
let main_n = fetch_node p main_fn in
|
||||
let node_outputs =
|
||||
List.map
|
||||
(function
|
||||
| IVar s -> SIVar (s, None)
|
||||
| BVar s -> SBVar (s, None)
|
||||
| RVar s -> SRVar (s, None))
|
||||
(snd main_n.n_outputs) in
|
||||
let node_loc_vars: sim_var list =
|
||||
List.map
|
||||
(function
|
||||
| IVar s -> SIVar (s, None)
|
||||
| BVar s -> SBVar (s, None)
|
||||
| RVar s -> SRVar (s, None))
|
||||
(snd main_n.n_local_vars) in
|
||||
let node_inner_nodes = (* TODO! *) [] in
|
||||
({node_outputs = node_outputs;
|
||||
node_loc_vars = node_loc_vars;
|
||||
node_inner_nodes = node_inner_nodes; },
|
||||
(fun s l -> (s.node_outputs, s)))
|
||||
|
||||
|
||||
|
||||
let simulate main_fn ast =
|
||||
let sim_ast = make_sim main_fn ast in
|
||||
Format.printf "Initial state:\n%a" pp_sim sim_ast
|
||||
|
@@ -1,21 +1,25 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
var i: int;
|
||||
node id_int (i: int) returns (o: int);
|
||||
let
|
||||
(o1, o2) = (i, i);
|
||||
o = i -> i;
|
||||
tel
|
||||
|
||||
node undiag_test (i: int) returns (o : bool);
|
||||
var l1, l2: int; l3: int;
|
||||
node aux (i, j: int) returns (o: int);
|
||||
let
|
||||
l3 = (pre (1)) -> 0;
|
||||
(l1, l2) = diagonal_int(i);
|
||||
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
||||
o = id_int(i) + id_int(j);
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
node main (i: int) returns (a, b: int);
|
||||
var tmp: int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do o = (pre o) + 1; done
|
||||
| Decr -> do o = (pre o) - 1; done
|
||||
a = 1;
|
||||
b = aux (i, a);
|
||||
tmp = aux (a+b, i);
|
||||
tel
|
||||
|
||||
node test (u, v: int; c: bool) returns (o: int);
|
||||
var x, y: int; b: bool;
|
||||
let
|
||||
x = merge c u v;
|
||||
o = 2 * x;
|
||||
tel
|
||||
|
||||
|
@@ -1,7 +1,15 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
var y: int;
|
||||
node aux (i: int) returns (a, b: int);
|
||||
let
|
||||
o2 = y;
|
||||
y = i;
|
||||
o1 = i;
|
||||
a = 1 -> pre i;
|
||||
b = 2 * i -> (3 * pre i);
|
||||
tel
|
||||
|
||||
node n (i: int) returns (o1, o2: int);
|
||||
var u1, u2, t1, t2: int; c: bool;
|
||||
let
|
||||
c = true -> not pre c;
|
||||
(t1, t2) = aux (i) when c;
|
||||
(u1, u2) = aux (i) when (not c);
|
||||
o1 = merge c t1 u1;
|
||||
o2 = merge c t2 u2;
|
||||
tel
|
||||
|
13
src/utils.ml
13
src/utils.ml
@@ -9,6 +9,13 @@ let rec list_select n = function
|
||||
let p1, p2 = list_select (n-1) t in
|
||||
h :: p1, p2
|
||||
|
||||
let rec list_remove_duplicates l =
|
||||
match l with
|
||||
| [] -> []
|
||||
| h :: t ->
|
||||
let t = list_remove_duplicates t in
|
||||
if List.mem h t then t else h :: t
|
||||
|
||||
let rec list_map_option (f: 'a -> 'b option) (l: 'a list) : 'b list option =
|
||||
List.fold_right (fun elt acc ->
|
||||
match acc, f elt with
|
||||
@@ -97,3 +104,9 @@ let rec vars_of_expr (expr: t_expression) : ident list =
|
||||
let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist =
|
||||
(fst l1 @ fst l2, snd l1 @ snd l2)
|
||||
|
||||
let split_patt (patt: t_varlist) (e: t_expression): t_varlist * t_varlist =
|
||||
let pl, pr = list_select (List.length (type_exp e)) (snd patt) in
|
||||
let tl = List.flatten (List.map type_var pl) in
|
||||
let tr = List.flatten (List.map type_var pr) in
|
||||
(tl, pl), (tr, pr)
|
||||
|
||||
|
4
tests/arrow.node
Normal file
4
tests/arrow.node
Normal file
@@ -0,0 +1,4 @@
|
||||
node main (i: int) returns (o: int);
|
||||
let
|
||||
o = 1 -> 2 -> 3;
|
||||
tel
|
22
tests/automaton.node
Normal file
22
tests/automaton.node
Normal file
@@ -0,0 +1,22 @@
|
||||
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 main (i: int) returns (o : int);
|
||||
var x, y:int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
|
||||
| Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
|
||||
| Done -> do o = pre o; done
|
||||
tel
|
||||
|
16
tests/counting.node
Normal file
16
tests/counting.node
Normal file
@@ -0,0 +1,16 @@
|
||||
-- count the number of top between two tick
|
||||
node counting (tick:bool; top:bool)
|
||||
returns (o: int);
|
||||
var v, o1: int;
|
||||
let o = if tick then v else 0 -> (pre o) + v;
|
||||
v = if top then 1 else 0
|
||||
tel;
|
||||
|
||||
node main (i: int)
|
||||
returns (o: int);
|
||||
let
|
||||
-- 0 means no `tick` and no `top`
|
||||
-- 1 means `tick`
|
||||
-- 2 means `top`
|
||||
o = counting(i = 1, i = 2)
|
||||
tel;
|
@@ -1,4 +1,4 @@
|
||||
node n2 (i: int) returns (o: bool);
|
||||
node main (i: int) returns (o: bool);
|
||||
let
|
||||
o = pre (true and pre( i = pre(pre(i))));
|
||||
tel
|
15
tests/reset.node
Normal file
15
tests/reset.node
Normal file
@@ -0,0 +1,15 @@
|
||||
-- counter of `top`s until `reset` condition holds
|
||||
node counting (tick: bool) returns (o: int);
|
||||
var v: int;
|
||||
let
|
||||
o = v -> (pre o) + v;
|
||||
v = if tick then 1 else 0
|
||||
tel
|
||||
|
||||
node main (i: int) returns (o: int);
|
||||
let
|
||||
-- 0 means no `top` and no `reset`
|
||||
-- 1 means `top`
|
||||
-- 2 means `reset`
|
||||
o = reset counting(i = 1) every (i = 2);
|
||||
tel
|
11
tests/tuple.node
Normal file
11
tests/tuple.node
Normal file
@@ -0,0 +1,11 @@
|
||||
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
|
||||
|
13
tests/when_merge.node
Normal file
13
tests/when_merge.node
Normal file
@@ -0,0 +1,13 @@
|
||||
node test (i: real) returns (o: real);
|
||||
var x, y: real;
|
||||
let
|
||||
x = (1.0 / i) when (i <> 0.0);
|
||||
y = 0.0 when (not (i <> 0.0));
|
||||
o = merge (i <> 0.0) x y;
|
||||
tel
|
||||
|
||||
node main (i: real) returns (o: real);
|
||||
let
|
||||
-- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
|
||||
o = test(i);
|
||||
tel
|
Reference in New Issue
Block a user