1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
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>
|
