diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-07 16:13:31 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-07 16:13:31 +0200 |
| commit | 73fa920959d22c084265fe847f4788564bf49700 (patch) | |
| tree | 9e99d91203b475ebe74fa0b484a86ada05caacf1 /doc/enonce.html | |
| parent | bcde99fbe99174a094f38fdda70ad69d65a423f4 (diff) | |
| download | SemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.tar.gz SemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.zip | |
Achieve nothing.
Diffstat (limited to 'doc/enonce.html')
| -rw-r--r-- | doc/enonce.html | 170 |
1 files changed, 170 insertions, 0 deletions
diff --git a/doc/enonce.html b/doc/enonce.html new file mode 100644 index 0000000..f9948e6 --- /dev/null +++ b/doc/enonce.html @@ -0,0 +1,170 @@ +<!-- -*- ispell-local-dictionary: "english" -*- --> +<html><head> +<title>Semantics and application to program verification, École normale supérieure, 2013-2014</title> +<meta name="author" content="Antoine Mine"> +<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> +<link rel="Stylesheet" title="Stylesheet" type="text/css" href="enonce_files/preferred.css"> +<script src="enonce_files/main.js" type="text/javascript"></script> +</head> +<body> + +<h1>Semantics and application to program verification</h1> + +<div id="main"> + +<h2>Project</h2> + +<p> +The goal of the project is to write a simple static analyzer by abstract + interpretation in OCaml to discover automatically numeric invariants +about the variables of programs written in a simple programming +language. + +</p><p> +The project is due on the day of the exam, on <b>May the 28th</b>. +The project should be sent by email to the teachers. + +</p><h3>Result</h3> + +<p> +For the project, you should deliver an archive that contains the following items: +</p><ul> +<li> the source code of the static analyzer, well-commented and complete with a Makefile; +</li><li> a report of 4 pages or more that describes the language +features supported, the choices in semantics and implementation (if +any), the usage of the analyzer; it must also discuss the result of a +few analysis tests (we provide some <a href="#testing">tests</a> that you can use). +</li></ul> + + +<h3><a name="features">Required features</a></h3> + +<h4>Input language</h4> + +<p> +The input language can be based on the language used in the lab session, + or you can design your own language with similar features. +To get started, you can download the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a> package (see the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/denotational.html#syntax">first practical session</a> for an explanation of the syntax of the language). + +</p><p> +More precisely, the language must feature at least: +</p><ul> +<li> blocks (nested sequences of instructions); +</li><li> declarations of variables of integer type, with proper scoping with respect to blocks <span class="com">(to simplify, you can assume that all variable names are distinct)</span>; +</li><li> assignments of integer expressions, with the standard arithmetic operators: <tt>+</tt>, <tt>-</tt>, <tt>*</tt> <span class="com">(and optionally division <tt>/</tt> and modulo <tt>%</tt>)</span>; +</li><li> if-then-else instructions, using boolean expressions containing integer comparisons (<tt>==</tt>, <tt>!=</tt>, <tt><</tt>, <tt>></tt>, <tt><=</tt>, <tt>>=</tt>) and boolean operators (<tt>&&</tt>, <tt>||</tt>, <tt>!</tt>) <span class="com">(support for boolean variables is not required)</span>; +</li><li> while loops; +</li><li> a non-deterministic operation, such as <tt>rand(l,h)</tt> in integer expressions; +</li><li> an <tt>assert</tt> instruction, that checks the validity of a boolean expression; +</li><li> a <tt>print</tt> instruction, that takes as argument a list of variables and prints their value. +</li></ul> + +<p> +<span class="com">(You are free to reject programs using other language +constructions, such as functions, non-integer variable declarations, +gotos, etc.)</span> + +</p><h4>Analysis</h4> + +<p> +The analyzer should contain an iterator that analyzes the program +forwards, by induction on the abstract syntax tree. +Loops can be unrolled a fixed number of times (e.g., 3 times), but you +should ultimately use iterations with widening in order to always +terminate for domains with infinite increasing chains. +To increase the precision, the first few (e.g., 3) applications of the +widening may be replaced with a join. + +</p><p> +The analysis should be parametric in the choice of a numeric abstract domain. +At least the <b>three</b> following domains must be provided: +</p><ul> +<li> the <b>constant domain</b>, that you should implement yourself; +</li><li> the <b>interval domain</b>, that you should also implement yourself; +</li><li> the <b>polyhedra domain</b>, which calls the <a href="http://apron.cri.ensmp.fr/library/0.9.10/mlapronidl">Apron library</a> to perform the abstract operations <span class="com">(you are not asked to implement the polyhedra operators yourself)</span>. +</li></ul> + +<p> +Depending on the domain, at least the following kinds of expressions should be handled precisely: +</p><ul> +<li> in assignments: all arithmetic expressions for the constant and interval domains; affine expressions for polyhedra; +</li><li> in the conditions of if-then-else and while instructions: for +polyhedra, boolean formulas whose atoms are affine constraints; for +constants and intervals, boolean formulas whose atoms are simple +comparisons between two variables or between a variable and a constant. +</li></ul> + +<p> +All the expressions allowed in the program syntax must be handled (no +"not implemented" exception); however, any expression not belonging to +the above categories may be handled in a coarse way (e.g., considering +assignments as non-deterministic and ignoring conditions). + +</p><h4>Output</h4> + +<p> +The analysis should at least output a textual file containing: +</p><ul> +<li> a list of the assertions that cannot be proved to hold, and their location; +</li><li> for each <tt>print</tt> instruction, the invariant found for the specified variables at the location of the instruction. +</li></ul> + +<p> +For debugging, it can be useful to implement a <i>trace mode</i> that outputs the abstract element computed at each step of the analysis. + +</p><h4><a name="testing">Tests</a></h4> + +<p> +To help you test your analyzer, we provide a <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/tests.tgz">set of small test programs</a>, + written in the small language used in the practical sessions. +We also provide the output of their analysis using our reference +analyzer, so that you can easily check the correctness and the precision + of your analyzer. + +</p><h3><a name="extensions">Extensions</a></h3> + +<p> +In addition to the mandatory features described above, you may implement one or several extensions, such as for instance: +</p><ul> +<li> functions and function calls <span class="com">(without recursion)</span>; +</li><li> checks for arithmetic overflows and divisions by zero errors in expressions; +</li><li> other numeric abstract domains <span class="com">(such as non-relational integer congruences, or linear equalities)</span>; +</li><li> several types of numeric variables <span class="com">(such as rationals or floating-point numbers, which are supported directly by Apron)</span>; +</li><li> boolean variables <span class="com">(you can handle them as integer variables that can only take two values: 0 for false, and 1 for true)</span>; +</li><li> arrays <span class="com">(each array can be abstracted by a single variable, and assignments result in weak updates); +</span></li><li> non-local control-flow instructions, such as <tt>break</tt> and <tt>continue</tt> in loops, forward <tt>goto</tt>, or even arbitrary <tt>goto</tt>; +</li><li> a backward analysis <span class="com">(find necessary conditions on the start of the program so that all assertions are satisfied)</span>; +</li><li> a nicer presentation for the output of the analysis, such as a graphical visualisation of numeric invariants <span class="com">(particularly useful for polyhedra in 2D or 3D)</span>; +</li><li> any extension of your choice. +</li></ul> + +<h3><a name="doc">Resources</a></h3> + +<h4>Files</h4> +<ul> +<li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>: language parser; +</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/tests.tgz">tests.tgz</a>: some programs to test your analyzer. +</li></ul> + +<h4>Documentation</h4> +<ul> +<li> <a href="http://caml.inria.fr/pub/docs/manual-ocaml"><b>OCaml</b></a> programming language; +</li><li> <a href="http://gallium.inria.fr/%7Efpottier/menhir"><b>Menhir</b></a> parser generator; +</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/doc-zarith"><b>ZArith</b></a> arbitrary precision number library; +</li><li> <a href="http://apron.cri.ensmp.fr/library/0.9.10/mlapronidl"><b>Apron</b></a> abstract domain library; +</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/doc-mapext/index.html"><b>Mapext</b></a> maps with some additional useful functions (the source code is included in the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a> bundle). +</li></ul> + +<p> +</p><hr> +<br> +<p> +Author: <a href="http://www.di.ens.fr/%7Emine">Antoine Miné</a> +<br><br> + +</p></div> + + + + +</body></html>
\ No newline at end of file |