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