RemovedTools.tex

\subsection{Interpreting Copilot}
To use Copilot's interpreter, one must first invoke the GHC Interpreter via
the Cabal sandbox. Invoking the interpreter with the \texttt{cabal
repl} command starts a session that looks like: 

%
\begin{lstlisting}[language = Copilot]
cabal repl
Preprocessing library copilot-2.1.2...
GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Language.Copilot ( src/Language/Copilot.hs, interpreted )
Ok, modules loaded: Language.Copilot.
*Language.Copilot> 
\end{lstlisting}
%

A copilot file \texttt{file} is loaded as follows:
%
\begin{lstlisting}[language = Copilot]
Language.Copilot> :l file
\end{lstlisting}

Notice that \texttt{file} has to be located
in the directory \emph{Copilot}.

The copilot interpreter is invoked as follows:
%
\begin{lstlisting}[language = Copilot]
Language.Copilot> interpret 10 propTempRiseShutOff
\end{lstlisting}
%
The first argument to the function \emph{interpret} is the number of iterations
that we want to evaluate. The third argument is the specification (of type {\tt
Spec}) that we wish to interpret.

The interpreter outputs the values of the arguments passed to the trigger, if
its guard is true, and {\tt --} otherwise. For example, consider the following
Copilot program:
%
\begin{lstlisting}[language = Copilot]
spec = do
  trigger "trigger1" (even nats) [arg nats, arg $ odd nats]
  trigger "trigger2" (odd nats) [arg nats]
\end{lstlisting}
% $
where {\tt nats} is the stream of natural numbers, and {\tt even} and {\tt odd}
are functions that take a stream and return whether the point-wise values are
even or odd, respectively. The output of
%
\begin{lstlisting}[language = Copilot]
interpret 10 spec
\end{lstlisting}
%
is as follows:
%
\begin{code}
trigger:   trigger2:
(0,false)  --
--         (1)
(2,false)  --
--         (3)
(4,false)  --
--         (5)
(6,false)  --
--         (7)
(8,false)  --
--         (9)
\end{code}
%

Sometimes it is convenient to observe the behavior of a stream without defining
a trigger. We can do so declaring an \emph{observer}. For example:
%
\begin{lstlisting}[language = Copilot]
spec :: Spec
spec = observer "obs" nats
\end{lstlisting}
%
can be interpreted using
%
\begin{lstlisting}[language = Copilot]
interpret 5 spec
\end{lstlisting}
%
as usual. Observers can be combined in larger Copilot programs. For example,
consider the following:
%
\begin{lstlisting}[language = Copilot]
spec :: Spec
spec = do
  let x = externW8 "x" (Just [0..])
  trigger "trigger" true [arg $ x < 3]
  observer "debug_x" x
\end{lstlisting}
% $
Interpreting {\tt spec} as follows
%
\begin{lstlisting}[language = Copilot]
interpret 10 spec
\end{lstlisting}
%
yields
%
\begin{code}
trigger:  debug_x:
(true)    0
(true)    1
(true)    2
(false)   3
(false)   4
(false)   5
(false)   6
(false)   7
(false)   8
(false)   9
\end{code}

\subsection{Compiling Copilot} \label{sec:compiling}

Compiling the engine controller from Example~\ref{exm:engine} is
straightforward. First, we pick a back-end to compile to. Currently, two
back-ends are implemented, both of which generate constant-time and
constant-space C code. One back-end is called \emph{copilot-c99} and targets
the Atom language,\footnote{\url{http://hackage.haskell.org/package/atom}}
originally developed by Tom Hawkins at Eaton Corp.\ for developing control
systems (in the process of depreciation). The second back-end is called \emph{copilot-sbv} and targets the SBV
language,\footnote{\url{http://hackage.haskell.org/package/sbv}} originally
developed by Levent Erk\"{o}k. SBV is primarily used as an interface to SMT
solvers~\cite{smt} and also contains a C-code generator. Both languages are
open-source.

The two back-ends are installed with Copilot, and they can be imported,
respectively, as

\begin{lstlisting}[language = Copilot]
import Copilot.Compile.C99
\end{lstlisting}
\noindent
and
\begin{lstlisting}[language = Copilot]
import Copilot.Compile.SBV
\end{lstlisting}

After importing a back-end, the interface for compiling is as
follows:
%
\footnote{Two explanations are in order: (1) {\tt reify} allows sharing in the
expressions to be compiled~\cite{DSLExtract}, and {\tt >>=} is a higher-order
operator that takes the result of reification and ``feeds'' it to the compile
function.}
%
\begin{lstlisting}[language = Copilot]
reify spec >>= compile defaultParams
\end{lstlisting}
%
\noindent
(The compile function takes a parameter to rename the generated C files; {\tt
defaultParams} is the default, in which there is no renaming.)

The compiler now generates several files in a separate-subfolder, some of which are called:

\begin{itemize}
\item ``driver.c'' ---
\item ``copilot.h'' ---
\end{itemize}

The file named ``copilot.h'' contains prototypes for all external variables,
functions, and arrays, and contains a prototype for the ``step''-function,
which evaluates a single iteration.

\begin{code}
/* Generated by Copilot Core v. 0.1 */

#include <stdint.h>
#include <stdbool.h>

/* Triggers (must be defined by user): */

void over_temp_rise();

/* External variables (must be defined by user): */

extern float temp;
extern bool running;

/* Step function: */

void step();
\end{code}

Using the prototypes in ``copilot.h'' we can build a controller as follows:

\begin{code}
/* main.c */
#include <stdio.h>
#include "copilot.h"

bool running = true;
float temp = 1.1;

void over_temp_rise()
{
  printf("The trigger has been evoked!\n");
}

int main (int argc, char const *argv[])
{
  int i;

  for (i = 0; i < 10; i++)
  {
    printf("iteration: %d\n", i);
    temp = temp * 1.3;
    step();
  }

  return 0;
}
\end{code}

Running {\tt gcc *.c -o prop} gives a program {\tt prop}, which,
when executed, yields the following output:
%
\begin{code}
iteration: 0
iteration: 1
iteration: 2
iteration: 3
iteration: 4
iteration: 5
iteration: 6
iteration: 7
The trigger has been evoked!
iteration: 8
The trigger has been evoked!
iteration: 9
The trigger has been evoked!
\end{code}
%

\subsection{Correctness of the generated code}~\label{sec:correctness}

\subsubsection{Frama-c}~\label{subsec:frama-c}
For this, make sure the following is installed:

\begin{itemize}
	\item GNU parallel
	\item frama-c (version at least sodium)
	\item why3
	\item cvc4 prover
\end{itemize}

It is possible to generate C code optimized for frama-c by using the \texttt{proofACSL}
function from SBV.Compile (instead of \texttt{compile} as shown
in~\ref{sec:compiling}). It will then generate the C source code (which should be in
the \texttt{copilot-sbv-codegen} folder). Go into that folder and just run
\texttt{make fwp} to use frama-c with the WP plugin. This should generate two
log files: a first exhaustive one called \texttt{logfwp}, and another which
summaries the former which is called \texttt{logfwpcompact}. The command make
fwp is detailed in Figure~\ref{fig:fwp}.

\begin{figure*}[!htb]
	\begin{lstlisting}[frame=none, language=bash]
parallel frama-c -wp -wp-out . -wp-timeout 20 -wp-prover CVC4 -wp-split {} ::: *.c | tee >logfwp >(grep 'Proved\|Unknown\|Timeout\|Failed\|Qed:\s\|CVC4:\s\|Parsing .*\.c' > logfwpcompact) >(grep 'Proved\|Qed:\s\|CVC4:\s\|Unknown\|Timeout\|Failed\|Parsing .*\.c')

	\end{lstlisting}
	\caption{The bash command.}
	\label{fig:fwp}
\end{figure*}

It is also possible to run frama-c with the value analysis plugin by running
\texttt{make fval}. Be careful, the value analysis plugin requires to preload
all the C sources files together, which requires a lot of RAM memory for big
projects.

It is recommended to refactor your code before trying to use frama-c on it, by for example splitting non-trivial expressions using magic labels, deleting all
local variables (use functions) and bitwise operators. If this step is
neglected, it may happen that frama-c would start swapping all your memory
resulting in a system crash.

\subsubsection{Splint}~\label{subsec:splint}

If you have splint installed on your computer, you can also try running splint on the C source code generated (with the command \texttt{make splint}), which will be a good starting point for manual code optimization or refactoring. The same problem as for frama-c may occur if you are working on a very big project (system crash).

\textbf{This tools does not guarantee that the generated C source code is compliant to ISO 9899:1999.} 

\subsubsection{Dot}~\label{subsec:dot}

It is also possible to generate dot graphs for each C source file generated, in
order to make the files more understandable. For this, you should check that
you have dot installed. Extract the dot code from a C source file, and then
just run \texttt{dot -Tps code.gv -o code.ps}
%
\footnote{A script doing that automatically is provided here
\url{https://raw.githubusercontent.com/Copilot-Language/examplesForACSL/master/WCV/scriptdot.cpp}}.

\subsection{Cross compiling}~\label{sec:cross}

If you go in the \texttt{copilot-sbv-codegen} folder, and run {\tt make all}
inside it, it should generate an archive file named \texttt{internal.a}, using
the compiler defined in the file \texttt{copilot.mk} (default is compcert, you
have to install it with its standard library). This can create some problems
during the linking process if you change the compiler for the final compilation
(typically \texttt{gcc -m32 -lm main.c internal.a} where \texttt{main.c} is
where your controller code is). For this purpose, we recommend installing first
the cross compiler (example \texttt{arm-none-eabi-gcc}), and compile the
\emph{whole} project using that very same compiler using the command \texttt{arm-none-eabi-gcc -m32 -lm [options] *.c}.