1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7Note to maintainer: sync with tools/release_files/README
8
9AutoCorres
10==========
11
12AutoCorres is a tool that assists reasoning about C programs
13in [Isabelle/HOL][1]. In particular, it uses Norrish's
14[C-to-Isabelle parser][2] to parse C into Isabelle, and then
15abstracts the result to produce a result that is (hopefully)
16more pleasant to reason about.
17
18  [1]: https://www.cl.cam.ac.uk/research/hvg/Isabelle/
19  [2]: https://ts.data61.csiro.au/software/TS/c-parser/
20
21
22
23Contents of this README
24-----------------------
25
26  * Installation
27  * Quickstart
28  * Development and reporting bugs
29  * Options
30  * Examples
31  * Publications
32
33
34
35Installation
36------------
37
38AutoCorres is packaged as a theory for Isabelle2020:
39
40    https://isabelle.in.tum.de
41
42AutoCorres currently supports three platforms: ARM, X64, and RISCV64.
43The platform determines the sizes of C integral and pointer types.
44
45For ARM, the sizes are:
46  - 64 bits: long long
47  - 32 bits: pointers, long, int
48  - 16 bits: short
49
50For X64:
51  - 64 bits: pointers, long long, long
52  - 32 bits: int
53  - 16 bits: short
54
55For RISCV64:
56  - 64 bits: pointers, long long, long
57  - 32 bits: int
58  - 16 bits: short
59
60To build or use AutoCorres, you must set the L4V_ARCH environment variable
61according to your choice of platform.
62
63To build AutoCorres for ARM, run the following in the L4.verified directory:
64
65    L4V_ARCH=ARM misc/regression/run_tests.py AutoCorres
66
67This builds the C parser and AutoCorres itself.
68
69To build AutoCorres for X64:
70
71    L4V_ARCH=X64 misc/regression/run_tests.py AutoCorres
72
73There is also a test suite, which can be run using:
74
75    L4V_ARCH=ARM misc/regression/run_tests.py AutoCorresTest
76    L4V_ARCH=X64 misc/regression/run_tests.py AutoCorresTest
77
78
79
80Quickstart
81----------
82
83A brief tutorial can be found in doc/quickstart.
84Run `make AutoCorresDoc` to generate a readable PDF document of
85the tutorial.
86
87
88
89Development and reporting bugs
90------------------------------
91
92AutoCorres is currently maintained by
93Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>.
94
95Additionally, the latest development version is available on GitHub
96as part of the L4.verified project:
97
98    https://github.com/seL4/l4v (in tools/autocorres)
99
100
101
102Options
103-------
104
105AutoCorres supports a variety of options, which are used as follows:
106
107    autocorres [option, key=val, list=a b c d] "path/to/file.c"
108
109`path/to/file.c` is the same path given to `install_C_file`, and
110AutoCorres will define the translated functions in the C-parser's
111generated locale (named `file`).
112
113The options are:
114
115  * `no_heap_abs = FUNC_NAMES`: Disable _heap abstraction_
116    on the given list of functions.
117
118  * `force_heap_abs = FUNC_NAMES`: Attempt _heap abstraction_
119    on the given list of functions, even if AutoCorres' heuristics
120    believes that they cannot be lifted.
121
122  * `heap_abs_syntax`: Enable experimental heap abstraction
123    syntactic sugar.
124
125  * `skip_heap_abs`: Completely disable _heap abstraction_.
126
127  * `unsigned_word_abs = FUNC_NAMES`: Use _word abstraction_
128    on unsigned integers in the given functions.
129
130  * `no_signed_word_abs = FUNC_NAMES`: Disable signed
131    _word abstraction_ on the given list of functions.
132
133  * `skip_word_abs`: Completely disable _word abstraction_.
134
135  * `ts_rules = RULES`: Enable _type strengthening_ to the
136    following types. Possible types include `pure` (pure
137    functional), `option` (option monad without state), `gets` (option
138    monad with state) and `nondet` (non-deterministic state monad).
139
140  * `ts_force RULE_NAME = FUNC_NAMES`: Force the given
141    functions to be type-strengthened to the given type,
142    even if a "better" type could otherwise be used.
143    See `tests/examples/type_strengthen_tricks.thy`.
144
145  * `scope = FUNC_NAMES`: Only translate the given functions
146    and their callees, up to depth `scope_depth`.
147    AutoCorres can be invoked multiple times to translate
148    parts of a program. See `tests/examples/Incremental.thy`.
149
150  * `scope_depth = N`: Call depth for `scope`.
151
152Name compatibility options (see `tests/examples/AC_Rename.thy`):
153
154  * `lifted_globals_field_prefix="foo"`, `lifted_globals_field_suffix="foo"`:
155    Override generated names for global variables during heap abstraction.
156    The default is `f` -> `f_''` (i.e. prefix="", suffix="_''").
157
158  * `function_name_prefix="foo"`, `function_name_suffix="foo"`:
159    Override generated names for abstracted functions.
160    The default is `f` -> `f'` (i.e. prefix="", suffix="'").
161
162Less common options (mainly for debugging):
163
164  * `keep_going`: Attempt to ignore certain non-critical
165    errors.
166
167  * `trace_heap_lift = FUNC_NAMES`: Trace the _heap abstraction_
168    process for each of the given functions. The traces
169    are stored in the Isabelle theory and can be quite large.
170    See `tests/examples/TraceDemo.thy`.
171
172  * `trace_word_abs = FUNC_NAMES`: As above, but traces
173    _word abstraction_.
174
175  * `trace_opt`: As above, but traces internal simplification
176    phases (for all functions).
177
178  * `no_opt`: Disable some optimisation passes that simplify
179    the AutoCorres output.
180
181  * `gen_word_heaps`: Force _heap abstraction_ to create
182    abstract heaps for standard `word` types
183    (`word8`, `word16`, `word32`, `word64`) even if they
184    are not needed.
185
186The following options are for interfacing with the seL4 proofs.
187
188  * `c_locale = NAME`: Run in this locale, rather than the default locale
189    created by the C-parser. This locale must behave like the C-parser
190    one except that the function bodies may be different.
191
192  * `no_c_termination`: Generate SIMPL wrappers and correspondence
193    proofs that do not require program termination for the SIMPL source.
194
195An example of invoking AutoCorres with _all_ of the options
196is as follows:
197
198    autocorres [
199        no_heap_abs = a b,
200        force_heap_abs = c d,
201        gen_word_heaps,
202        skip_heap_abs,  (* mutually exclusive with previous options *)
203        heap_abs_syntax,
204
205        unsigned_word_abs = f g h,
206        no_signed_word_abs = i j k,
207        skip_word_abs,  (* mutually exclusive with previous options *)
208
209        ts_rules = pure nondet,
210        ts_force nondet = l m n,
211
212        scope = o p q,
213        scope_depth = 5,
214        keep_going,
215        c_locale = "my_locale",
216        no_c_termination,
217        trace_heap_lift = c d,
218        trace_word_abs = f h i,
219        no_opt,
220
221        lifted_globals_field_prefix="my_global_",
222        lifted_globals_field_suffix="",
223        function_name_prefix="my_func_",
224        function_name_suffix=""
225        ] "filename.c"
226
227
228
229Examples
230--------
231
232Some examples are in the `tests/examples` directory.
233
234Many of these examples are quick-and-dirty proofs, and should not
235necessary be considered the best style.
236
237None-the-less, some of the examples available are, in approximate
238increasing level of difficulty:
239
240  * `Simple.thy`: Proofs of some simple functions, including
241    `max` and `gcd`.
242
243  * `Swap.thy`: Proof of a simple `swap` function.
244
245  * `MultByAdd.thy`: Proof of a function that carries out
246    multiplication using addition.
247
248  * `Factorial.thy`: Proof of a factorial function, using
249    several different methods.
250
251  * `FibProof.thy`: Proof of the Fibonacci function, using
252    several different methods.
253
254  * `ListRev.thy`: Proof of a function that carries out an
255    in-place linked list reversal.
256
257  * `CList.thy`: Another list reversal, based on a proof by
258    Mehta and Nipkow. See [the paper][3].
259
260  * `IsPrime.thy`: Proof of a function that determines if
261    the input number is prime.
262
263  * `Memset.thy`: Proof of a C `memset` implementation.
264
265  * `Quicksort.thy`: Proof of a simple quicksort
266    implementation on an array of `int`s.
267
268  * `BinarySearch.thy`: Proof of a function that determines
269    if a sorted input array of `unsigned int` contains the
270    given `unsigned int`.
271
272  * `SchorrWaite.thy`: Proof a C implementation of the
273    Schorr-Waite algorithm, using Mehta and Nipkow's
274    high-level proof. See [the paper][3].
275
276  * `Memcpy.thy`: Proof of a C `memcpy` implementation.
277    The proof connects the C parser's byte-level heap
278    with AutoCorres's type-safe heap representation.
279
280There are also some examples that aren't about program proofs,
281but demonstrate AutoCorres features:
282
283  * `AC_Rename.thy`: how to change AutoCorres-generated names.
284
285  * `TraceDemo.thy`: how to use the (experimental) tracing.
286
287  * `type_strengthen_tricks.thy`: configuring type-strengthening.
288
289  * `Incremental.thy`: (experimental) support for incremental translation.
290
291
292
293Publications
294------------
295
296L1 (SimplConv), L2 (LocalVarExtract) and TS (TypeStrengthen) were described in
297
298    "Bridging the gap: Automatic verified abstraction of C"
299    David Greenaway, June Andronick, Gerwin Klein
300    Proceedings of the Third International
301            Conference on Interactive Theorem Proving (ITP), August 2012.
302    https://ts.data61.csiro.au/publications/nicta_full_text/5662.pdf
303
304HL (heap abstraction) and WA (word abstraction) were described in
305
306  [3]:
307    "Don���t sweat the small stuff --- Formal verification of C code without the pain"
308    David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
309    Proceedings of the 35th ACM SIGPLAN Conference on
310            Programming Language Design and Implementation. ACM, June 2014.
311    https://ts.data61.csiro.au/publications/nicta_full_text/7629.pdf
312
313A more comprehensive source is
314
315    "Automated proof-producing abstraction of C code"
316    David Greenaway
317    PhD thesis, March 2015.
318    https://ts.data61.csiro.au/publications/nicta_full_text/8758.pdf
319