Tools.tex

\section{Tools} \label{sec:tools}

Copilot comes with a variety of tools, including a pretty-printer, an
interpreter, a compiler targeting C, and a verifier front-end. In the following
section, we will demonstrate some of these tools and their usage. All the tools
are shown in the Figure~\ref{fig:new-toolchain}.

\begin{figure}[ht!]
	\centering
\begin{tikzpicture}[->, node distance=3cm, auto, shorten >=1pt, bend angle=45,
thick]
\tikzstyle{every state}=[rectangle, rounded corners]
		
		
\node[state] (Int) {Interpreter};
\node[state] (Lang) [above right of=Int] {%
		\begin{tabular}[b]{l}
		Copilot Libraries\\ \hline Copilot Language
		\end{tabular}};
	
	\node[state] (M4) [left=3cm of Lang] {M4};
	\node[state] (Core) [below right of=Lang] {Copilot Core};
	\node[state] (PP) [right of=Core] {Pretty Printer};
	
	
	
	\node[state] (ACSL) [below of=PP] {\begin{tabular}[b]{l}
		ACSL\\ generator
		\end{tabular}};
	\node[state] (DOTc) [right of=ACSL] {\begin{tabular}[b]{l}
		DOT\\ generator
		\end{tabular}};
	\node[state] (SBV) [below of=Core] {SBV Back-End};
	
	\node[state] (SMT) [below left=1.6cm and 1.2cm of Int] {SMT Lib};
	\node[state] (C99S) [below of=SBV] {\begin{tabular}[b]{l}
		DOT\\ \hline ACSL\\ \hline C99
		\end{tabular}};
	\node[state] (DOT) [below right of=C99S] {DOT/graphviz};
	\node[state] (CCOMP) [below left=0.3cm and 0.3cm of C99S] {CompCert};
	\node[state] (ASM) [below=1cm of CCOMP] {Assembly code};
	
	
	\tikzstyle{every node}=[]
	
	
	\path %% (Libs) edge node {0,1,L} (Lang);
	%% edge node {1,1,R} (C)
	(Lang) edge [bend left, anchor=west, text width=2.5cm] node {Reification and DSL-specific type-checking} (Core)
	%% edge node {0,1,L} (C)
	(M4) edge [text width=2.5cm] node {Preprocessing} (Lang)
	(Core) edge [anchor=east] node {Translation} (SBV)
	edge node {} (PP)
	edge node [swap] {Evaluation} (Int)
	(ACSL) edge [bend left, anchor=west] node {Integration} (C99S)
	(DOTc) edge [bend left, anchor=east] node {} (C99S)
	(Int) edge [<->,red, bend right, anchor=east] node {QuickCheck} (SBV)
	(PP) edge [->, anchor=east, text width=2cm] node {ACSL generation} (ACSL)
	(PP) edge [->, anchor=west] node {DOT generation} (DOTc)
	(C99S) edge [->, anchor=north west] node {make} (CCOMP)
	(Core) edge [->, anchor=south east, text width=3cm] node {proof generation} (SMT)
	(CCOMP) edge [->, anchor=east] node {Cross-compilation} (ASM)
	(C99S) edge [loop left, ->, anchor=east] node {Verification with frama-c WP plugin} (C99S)
	(C99S) edge [->, anchor=west] node {Extraction and graph generation} (DOT)
	(SBV) edge [->,anchor=east] node {Compilation} (C99S);
	%% edge [bend left] node {Translation} (SBV)
	%% (Atom) edge [loop below] node {1,1,R} (D)
	%% edge node {0,1,R} (Libs)
	%% (SBV) edge [bend left] node {1,0,R} ();
	\end{tikzpicture}
	\caption{The new Copilot toolchain. The red arrows are the one to implement in the future.}
	\label{fig:new-toolchain}
	\end{figure}

\subsection{Pretty-Printing} \label{sec:pretty-printing}
Pretty-printing is straightforward. For some specification {\tt spec},
%
\begin{code}
prettyPrint spec
\end{code}
%
\noindent
returns the specification after static macro expansion. Pretty-printing can
provide some indication about the complexity of the specification to be
evaluated. Specifications that are built by recursive Haskell programs (e.g.,
the majority voting example in Section~\ref{subsec:boyer_moore}) can generate
expressions that are large. Large expressions can take significant
time to interpret or compile. 

\subsubsection{Dot Pretty-Printing} 

In order to use the Dot Pretty-Printter, you have to generate C source code. When generating C source code with SBV, each C source file (except driver.c), will have a dot source code output inside, which summaries what the file is. If the generation is on proof mode (using the function \texttt{proofACSL}), then Copilot will generate one more file named "main.gv", which contains the code for the whole AST of your program.