source: Deliverables/D6.6/report.tex

Last change on this file was 3244, checked in by sacerdot, 6 years ago

Final version.

File size: 11.7 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../style/cerco}
4
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage{amssymb} 
8\usepackage[english]{babel}
9\usepackage{graphicx}
10\usepackage[utf8x]{inputenc}
11\usepackage{listings}
12\usepackage{stmaryrd}
13\usepackage{url}
14
15\title{
16INFORMATION AND COMMUNICATION TECHNOLOGIES\\
17(ICT)\\
18PROGRAMME\\
19\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
20
21\lstdefinelanguage{matita-ocaml}
22  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
23   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
24   morekeywords={[3]type,of},
25   mathescape=true,
26  }
27
28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        keywordstyle=[3]\color{blue}\bfseries,
32        commentstyle=\color{green},
33        stringstyle=\color{blue},
34        showspaces=false,showstringspaces=false}
35
36\lstset{extendedchars=false}
37\lstset{inputencoding=utf8x}
38\DeclareUnicodeCharacter{8797}{:=}
39\DeclareUnicodeCharacter{10746}{++}
40\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
41\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
42
43\date{}
44\author{}
45
46\begin{document}
47
48\thispagestyle{empty}
49
50\vspace*{-1cm}
51\begin{center}
52\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
53\end{center}
54
55\begin{minipage}{\textwidth}
56\maketitle
57\end{minipage}
58
59\vspace*{0.5cm}
60\begin{center}
61\begin{LARGE}
62\textbf{
63Report n. D6.6\\
64Packages for Linux distributions and Live CD }
65\end{LARGE} 
66\end{center}
67
68\vspace*{2cm}
69\begin{center}
70\begin{large}
71Version 1.0
72\end{large}
73\end{center}
74
75\vspace*{0.5cm}
76\begin{center}
77\begin{large}
78Main Authors:\\
79Claudio Sacerdoti Coen
80\end{large}
81\end{center}
82
83\vspace*{\fill}
84
85\noindent
86Project Acronym: \cerco{}\\
87Project full title: Certified Complexity\\
88Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
89
90\clearpage
91\pagestyle{myheadings}
92\markright{\cerco{}, FP7-ICT-2009-C-243881}
93
94\newpage
95
96\vspace*{7cm}
97\paragraph{Abstract}
98We provide Debian packages for all the software developed in CerCo and for all
99its software dependencies. The Debian packages are for the forthcoming stable
100Debian distribution. Moreover, we provide a Live CD, also based on Debian, that
101contains a pre-installed version of all the packages and a copy of the
102formalization.
103\newpage
104
105\tableofcontents
106
107\newpage
108
109\section{Task}
110\label{sect.task}
111
112The Grant Agreement describes deliverable D6.6 as follows:
113\begin{quotation}
114\textbf{Packages for Linux distributions and Live CD}:
115In order
116to foster adoption of the CerCo compiler in a wider community, we will provide packages for selected Linux
117distributions and a Live CD with the software developed in the project. We will also consider and discuss the
118integration of our software in an extensible platform dedicated to source-code analysis of C software, like
119Frama-C. However, at the moment it is unclear how these rapidly changing platforms will evolve in the next
120two years, if integration would provide an added value and if it would be possible to practically achieve the
121integration in the project timeframe without an actual involvement of the platform developers (that would need to
122contribute man-power to the task).
123\end{quotation}
124
125Integration with Frama-C has been done in D5.1-D5.3.
126This report overviews the packages that have been provided and the contents
127of the Live CD.
128
129\section{Debian packages}
130We show here the description of every Debian package made for the
131software developed in CerCo, as reported by \texttt{apt-cache show}.
132Only the relevant fields are shown.
133\begin{enumerate}
134 \item Package name: \texttt{acc}, Version: 0.2-1\\
135   \textbf{CerCo's Annotating C Compiler}\\
136 CerCo's Annotating C Compiler is a C compiler for the 8051 microprocessor.
137 It produces both an Intel HEX code memory representation and an instrumented
138 version of the source code. The instrumented source code is a copy of the
139 original source code augmented with additional instructions to keep track of
140 the exact number of clock cycles spent by the microprocessor to execute the
141 program basic blocks. Combined with CerCo's Frama-C Cost Plugin it allows to
142 certify exact parametric time and stack bounds for the source code.
143 Limitations: the source code must all be in one .c file and it must not
144 contain external calls.
145 \item Package name: \texttt{acc-trusted}, Version: 0.2-1\\
146   \textbf{CerCo's Trusted Annotating C Compiler}\\
147 CerCo's Annotating C Compiler is a C compiler for the 8051 microprocessor.
148 It produces both an Intel HEX code memory representation and an instrumented
149 version of the source code. The instrumented source code is a copy of the
150 original source code augmented with additional instructions to keep track of
151 the exact number of clock cycles spent by the microprocessor to execute the
152 program basic blocks. Combined with CerCo's Frama-C Cost Plugin it allows to
153 certify exact parametric time and stack bounds for the source code.
154 Limitations: the source code must all be in one .c file and it must not
155 contain external calls.
156 This version of the compiler has been certified for preservation of the
157 inferred costs using the interactive theorem prover Matita.
158 \item Package name: \texttt{frama-c-cost-plugin}, Version: 0.2-1\\
159   Depends: \texttt{acc | acc-trusted},
160   Recommends: \texttt{why, why3, cvc3}\\
161   \textbf{CerCo's Frama-C Cost Plugin}\\
162 The CerCo's Frama-C Cost Plugin has been developed by the CerCo project\\
163 http://cerco.cs.unibo.it.
164 It compiles a C source file to an 8051 Intel HEX using either the acc
165 or the acc-trusted compilers. The compilation also produces an instrumented
166 copy of the source code obtained inserting instructions to keep track of the
167 number of clock cycles spent by the program on the real hardware. The plugin
168 implements an invariant generator that computes parametric bounds for the
169 total program execution time and stack usage. Moreover, the plugin can invoke
170 the Jessie condition generators to generate proof obligations to certify the
171 produced bound. The proof generators may be automatically closed using the
172 why3 tool that invokes automated theorem provers. The cvc3 prover works
173 particularly well with the proof obligations generated from the cost plugin.
174\end{enumerate}
175
176The following additional Debian packages are required by the CerCo's Frama-C
177Cost Plugin. They do not install software developed in CerCo, but their Debian
178packages themselves have been made by CerCo. Among all the theorem provers
179that can be used in combination with Why3 (and the CerCo Cost Plugin), we
180have decided to package cvc3 because its licence allows free redistribution
181and because it is powerful enough to close most proof obligations generated
182by CerCo on common examples. The user can still manually install and try other
183provers that will be automatically recognized by why3 just by running
184\texttt{why3config}. We do not provide any Debian packages for them.
185
186\begin{enumerate}
187 \item Package name: \texttt{why}, Version: 2.31+cerco-1\\
188   \textbf{Software verification tool}\\
189 Why aims at being a verification conditions generator (VCG) back-end
190 for other verification tools. It provides a powerful input language
191 including higher-order functions, polymorphism, references, arrays and
192 exceptions. It generates proof obligations for many systems: the proof
193 assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
194 decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
195 \item Package name: \texttt{why3}, Version: 0.73+cerco-1\\
196   \textbf{Software verification tool}\\
197 Why aims at being a verification conditions generator (VCG) back-end
198 for other verification tools. It provides a powerful input language
199 including higher-order functions, polymorphism, references, arrays and
200 exceptions. It generates proof obligations for many systems: the proof
201 assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
202 decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
203 \item Package name: \texttt{cvc3}, Version: 2.4.1-1\\
204   \textbf{CVC3 is an automatic theorem prover for Satisfiability Module Theories}\\
205  CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
206 CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.
207 CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:
208 * several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
209 * support for quantifiers;
210 * an interactive text-based interface;
211 * a rich C and C++ API for embedding in other systems;
212 * proof and model generation abilities;
213 * predicate subtyping;
214 * essentially no limit on its use for research or commercial purposes (see license).
215\end{enumerate}
216
217Finally, we have released and packaged a new version of Matita that contains
218several improvements driven by CerCo, like code extraction.
219
220\begin{enumerate}
221 \item Package name: \texttt{matita}, Version: 0.99.2-1\\
222   \textbf{Interactive theorem prover}\\
223 Matita is a graphical interactive theorem prover based on the Calculus of
224 (Co)Inductive Constructions.
225\end{enumerate}
226
227All Debian packages mentioned above can be downloaded from the CerCo's website
228\texttt{http://cerco.cs.unibo.it} and are compatible with the \emph{testing}
229release of Debian, soon to be freezed and become the forthcoming \emph{stable}
230release. The source code to recompile the Debian packages from scratch is part
231of the CerCo repository and can be also downloaded from the website.
232
233\section{Live CD}
234
235We also provide a Live CD to easily test all the software implemented in CerCo
236without having to recompile the software by hand or install a Debian
237distribution. The Live CD can be downloaded from the CerCo's website
238\texttt{http://cerco.cs.unibo.it}. It is a Live Debian CD that can be either
239burnt on a physical disk used to boot a real machine, or it can be used to
240bootstrap a virtual machine using any virtualizer like \texttt{virtualbox, qemu}
241or similar ones.
242
243The Live CD contains an xserver and a standard gnome environment and it
244connects automatically to any available network. The virtualbox guest tools
245have also been installed to facilitate communication between the host and
246the virtual machine, e.g. for file transfer.
247
248The Live CD also has pre-installed all the Debian packages described in the
249previous section. The user can simply boot the system and invoke the
250\texttt{cerco} executable to compile any compatible C file to the Intel HEX
251format for the 8051. The executable also computes the cost model for the
252source program, its cost invariants and tries to certify them using the
253cvc3 theorem prover. In case of failure, the flag \texttt{-ide} can be used
254to open an interactive why3 session to experiment with different theorem
255prover flags (e.g. increasing the prover timeout).
256
257Further informations on the \texttt{cerco} executable can be found in
258Deliverable D5.2.
259
260Finally, the Live CD also has a preinstalled copy of the interactive theorem
261prover Matita and a snapshot of the compiler certification. The snapshot can
262be found in the user's home directory, under \texttt{cerco/src}. Matita
263files can be opened running \texttt{matita}. The other
264directory \texttt{cerco/driver} contains the extracted code together with
265the untrusted code that forms the CerCo Trusted Compiler.
266
267\end{document}
Note: See TracBrowser for help on using the repository browser.