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{ |
---|
16 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
17 | (ICT)\\ |
---|
18 | PROGRAMME\\ |
---|
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{ |
---|
63 | Report n. D6.6\\ |
---|
64 | Packages for Linux distributions and Live CD } |
---|
65 | \end{LARGE} |
---|
66 | \end{center} |
---|
67 | |
---|
68 | \vspace*{2cm} |
---|
69 | \begin{center} |
---|
70 | \begin{large} |
---|
71 | Version 1.0 |
---|
72 | \end{large} |
---|
73 | \end{center} |
---|
74 | |
---|
75 | \vspace*{0.5cm} |
---|
76 | \begin{center} |
---|
77 | \begin{large} |
---|
78 | Main Authors:\\ |
---|
79 | Claudio Sacerdoti Coen |
---|
80 | \end{large} |
---|
81 | \end{center} |
---|
82 | |
---|
83 | \vspace*{\fill} |
---|
84 | |
---|
85 | \noindent |
---|
86 | Project Acronym: \cerco{}\\ |
---|
87 | Project full title: Certified Complexity\\ |
---|
88 | Proposal/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} |
---|
98 | We provide Debian packages for all the software developed in CerCo and for all |
---|
99 | its software dependencies. The Debian packages are for the forthcoming stable |
---|
100 | Debian distribution. Moreover, we provide a Live CD, also based on Debian, that |
---|
101 | contains a pre-installed version of all the packages and a copy of the |
---|
102 | formalization. |
---|
103 | \newpage |
---|
104 | |
---|
105 | \tableofcontents |
---|
106 | |
---|
107 | \newpage |
---|
108 | |
---|
109 | \section{Task} |
---|
110 | \label{sect.task} |
---|
111 | |
---|
112 | The Grant Agreement describes deliverable D6.6 as follows: |
---|
113 | \begin{quotation} |
---|
114 | \textbf{Packages for Linux distributions and Live CD}: |
---|
115 | In order |
---|
116 | to foster adoption of the CerCo compiler in a wider community, we will provide packages for selected Linux |
---|
117 | distributions and a Live CD with the software developed in the project. We will also consider and discuss the |
---|
118 | integration of our software in an extensible platform dedicated to source-code analysis of C software, like |
---|
119 | Frama-C. However, at the moment it is unclear how these rapidly changing platforms will evolve in the next |
---|
120 | two years, if integration would provide an added value and if it would be possible to practically achieve the |
---|
121 | integration in the project timeframe without an actual involvement of the platform developers (that would need to |
---|
122 | contribute man-power to the task). |
---|
123 | \end{quotation} |
---|
124 | |
---|
125 | Integration with Frama-C has been done in D5.1-D5.3. |
---|
126 | This report overviews the packages that have been provided and the contents |
---|
127 | of the Live CD. |
---|
128 | |
---|
129 | \section{Debian packages} |
---|
130 | We show here the description of every Debian package made for the |
---|
131 | software developed in CerCo, as reported by \texttt{apt-cache show}. |
---|
132 | Only 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 | |
---|
176 | The following additional Debian packages are required by the CerCo's Frama-C |
---|
177 | Cost Plugin. They do not install software developed in CerCo, but their Debian |
---|
178 | packages themselves have been made by CerCo. Among all the theorem provers |
---|
179 | that can be used in combination with Why3 (and the CerCo Cost Plugin), we |
---|
180 | have decided to package cvc3 because its licence allows free redistribution |
---|
181 | and because it is powerful enough to close most proof obligations generated |
---|
182 | by CerCo on common examples. The user can still manually install and try other |
---|
183 | provers 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 | |
---|
217 | Finally, we have released and packaged a new version of Matita that contains |
---|
218 | several 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 | |
---|
227 | All 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} |
---|
229 | release of Debian, soon to be freezed and become the forthcoming \emph{stable} |
---|
230 | release. The source code to recompile the Debian packages from scratch is part |
---|
231 | of the CerCo repository and can be also downloaded from the website. |
---|
232 | |
---|
233 | \section{Live CD} |
---|
234 | |
---|
235 | We also provide a Live CD to easily test all the software implemented in CerCo |
---|
236 | without having to recompile the software by hand or install a Debian |
---|
237 | distribution. 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 |
---|
239 | burnt on a physical disk used to boot a real machine, or it can be used to |
---|
240 | bootstrap a virtual machine using any virtualizer like \texttt{virtualbox, qemu} |
---|
241 | or similar ones. |
---|
242 | |
---|
243 | The Live CD contains an xserver and a standard gnome environment and it |
---|
244 | connects automatically to any available network. The virtualbox guest tools |
---|
245 | have also been installed to facilitate communication between the host and |
---|
246 | the virtual machine, e.g. for file transfer. |
---|
247 | |
---|
248 | The Live CD also has pre-installed all the Debian packages described in the |
---|
249 | previous 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 |
---|
251 | format for the 8051. The executable also computes the cost model for the |
---|
252 | source program, its cost invariants and tries to certify them using the |
---|
253 | cvc3 theorem prover. In case of failure, the flag \texttt{-ide} can be used |
---|
254 | to open an interactive why3 session to experiment with different theorem |
---|
255 | prover flags (e.g. increasing the prover timeout). |
---|
256 | |
---|
257 | Further informations on the \texttt{cerco} executable can be found in |
---|
258 | Deliverable D5.2. |
---|
259 | |
---|
260 | Finally, the Live CD also has a preinstalled copy of the interactive theorem |
---|
261 | prover Matita and a snapshot of the compiler certification. The snapshot can |
---|
262 | be found in the user's home directory, under \texttt{cerco/src}. Matita |
---|
263 | files can be opened running \texttt{matita}. The other |
---|
264 | directory \texttt{cerco/driver} contains the extracted code together with |
---|
265 | the untrusted code that forms the CerCo Trusted Compiler. |
---|
266 | |
---|
267 | \end{document} |
---|