e3c2e878b9
wp rules for most operators such as return, get, gets are named return_wp, get_wp, etc. Then when, whenE, unless, unlessE operators had an additional hoare_.. prefix that this commit removes for more consistency. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
---|---|---|
.. | ||
doc/quickstart | ||
experiments/alloc-proof | ||
test-seL4 | ||
tests | ||
tools | ||
AbstractArrays.thy | ||
AutoCorres.thy | ||
AutoCorresSimpset.thy | ||
Auto_Separation_Algebra.thy | ||
CCorresE.thy | ||
CorresXF.thy | ||
DataStructures.thy | ||
ExceptionRewrite.thy | ||
ExecConcrete.thy | ||
HeapLift.thy | ||
L1Defs.thy | ||
L1Peephole.thy | ||
L1Valid.thy | ||
L2Defs.thy | ||
L2Opt.thy | ||
L2Peephole.thy | ||
LocalVarExtract.thy | ||
Makefile | ||
MonadMono.thy | ||
NatBitwise.thy | ||
NonDetMonadEx.thy | ||
Polish.thy | ||
README.md | ||
ROOT | ||
SimplBucket.thy | ||
SimplConv.thy | ||
TypHeapSimple.thy | ||
TypeStrengthen.thy | ||
WordAbstract.thy | ||
WordPolish.thy | ||
autocorres.ML | ||
autocorres_data.ML | ||
autocorres_trace.ML | ||
autocorres_util.ML | ||
exception_rewrite.ML | ||
function_info.ML | ||
heap_lift.ML | ||
heap_lift_base.ML | ||
l2_opt.ML | ||
local_var_extract.ML | ||
monad_convert.ML | ||
monad_types.ML | ||
pretty_bound_var_names.ML | ||
prog.ML | ||
program_info.ML | ||
record_utils.ML | ||
simpl_conv.ML | ||
simple_lazy.ML | ||
trace_antiquote.ML | ||
type_strengthen.ML | ||
utils.ML | ||
word_abstract.ML |
README.md
Note to maintainer: sync with tools/release_files/README
AutoCorres
AutoCorres is a tool that assists reasoning about C programs in Isabelle/HOL. In particular, it uses Norrish's C-to-Isabelle parser to parse C into Isabelle, and then abstracts the result to produce a result that is (hopefully) more pleasant to reason about.
Contents of this README
- Installation
- Quickstart
- Development and reporting bugs
- Options
- Examples
- Publications
Installation
AutoCorres is packaged as a theory for Isabelle2021:
https://isabelle.in.tum.de
AutoCorres currently supports three platforms: ARM, X64, and RISCV64. The platform determines the sizes of C integral and pointer types.
For ARM, the sizes are:
- 64 bits: long long
- 32 bits: pointers, long, int
- 16 bits: short
For X64:
- 64 bits: pointers, long long, long
- 32 bits: int
- 16 bits: short
For RISCV64:
- 64 bits: pointers, long long, long
- 32 bits: int
- 16 bits: short
To build or use AutoCorres, you must set the L4V_ARCH environment variable according to your choice of platform.
To build AutoCorres for ARM, run the following in the L4.verified directory:
L4V_ARCH=ARM misc/regression/run_tests.py AutoCorres
This builds the C parser and AutoCorres itself.
To build AutoCorres for X64:
L4V_ARCH=X64 misc/regression/run_tests.py AutoCorres
There is also a test suite, which can be run using:
L4V_ARCH=ARM misc/regression/run_tests.py AutoCorresTest
L4V_ARCH=X64 misc/regression/run_tests.py AutoCorresTest
Quickstart
A brief tutorial can be found in doc/quickstart.
Run make AutoCorresDoc
to generate a readable PDF document of
the tutorial.
Development and reporting bugs
AutoCorres is currently maintained by the seL4 Foundation.
Additionally, the latest development version is available on GitHub as part of the L4.verified project:
https://github.com/seL4/l4v (in tools/autocorres)
Please use the tracker on the GitHub address above for reporting issues with the tool.
Options
AutoCorres supports a variety of options, which are used as follows:
autocorres [option, key=val, list=a b c d] "path/to/file.c"
path/to/file.c
is the same path given to install_C_file
, and
AutoCorres will define the translated functions in the C-parser's
generated locale (named file
).
The options are:
-
no_heap_abs = FUNC_NAMES
: Disable heap abstraction on the given list of functions. -
force_heap_abs = FUNC_NAMES
: Attempt heap abstraction on the given list of functions, even if AutoCorres' heuristics believes that they cannot be lifted. -
heap_abs_syntax
: Enable experimental heap abstraction syntactic sugar. -
skip_heap_abs
: Completely disable heap abstraction. -
unsigned_word_abs = FUNC_NAMES
: Use word abstraction on unsigned integers in the given functions. -
no_signed_word_abs = FUNC_NAMES
: Disable signed word abstraction on the given list of functions. -
skip_word_abs
: Completely disable word abstraction. -
ts_rules = RULES
: Enable type strengthening to the following types. Possible types includepure
(pure functional),option
(option monad without state),gets
(option monad with state) andnondet
(non-deterministic state monad). -
ts_force RULE_NAME = FUNC_NAMES
: Force the given functions to be type-strengthened to the given type, even if a "better" type could otherwise be used. Seetests/examples/type_strengthen_tricks.thy
. -
scope = FUNC_NAMES
: Only translate the given functions and their callees, up to depthscope_depth
. AutoCorres can be invoked multiple times to translate parts of a program. Seetests/examples/Incremental.thy
. -
scope_depth = N
: Call depth forscope
.
Name compatibility options (see tests/examples/AC_Rename.thy
):
-
lifted_globals_field_prefix="foo"
,lifted_globals_field_suffix="foo"
: Override generated names for global variables during heap abstraction. The default isf
->f_''
(i.e. prefix="", suffix="_''"). -
function_name_prefix="foo"
,function_name_suffix="foo"
: Override generated names for abstracted functions. The default isf
->f'
(i.e. prefix="", suffix="'").
Less common options (mainly for debugging):
-
keep_going
: Attempt to ignore certain non-critical errors. -
trace_heap_lift = FUNC_NAMES
: Trace the heap abstraction process for each of the given functions. The traces are stored in the Isabelle theory and can be quite large. Seetests/examples/TraceDemo.thy
. -
trace_word_abs = FUNC_NAMES
: As above, but traces word abstraction. -
trace_opt
: As above, but traces internal simplification phases (for all functions). -
no_opt
: Disable some optimisation passes that simplify the AutoCorres output. -
gen_word_heaps
: Force heap abstraction to create abstract heaps for standardword
types (word8
,word16
,word32
,word64
) even if they are not needed.
The following options are for interfacing with the seL4 proofs.
-
c_locale = NAME
: Run in this locale, rather than the default locale created by the C-parser. This locale must behave like the C-parser one except that the function bodies may be different. -
no_c_termination
: Generate SIMPL wrappers and correspondence proofs that do not require program termination for the SIMPL source.
An example of invoking AutoCorres with all of the options is as follows:
autocorres [
no_heap_abs = a b,
force_heap_abs = c d,
gen_word_heaps,
skip_heap_abs, (* mutually exclusive with previous options *)
heap_abs_syntax,
unsigned_word_abs = f g h,
no_signed_word_abs = i j k,
skip_word_abs, (* mutually exclusive with previous options *)
ts_rules = pure nondet,
ts_force nondet = l m n,
scope = o p q,
scope_depth = 5,
keep_going,
c_locale = "my_locale",
no_c_termination,
trace_heap_lift = c d,
trace_word_abs = f h i,
no_opt,
lifted_globals_field_prefix="my_global_",
lifted_globals_field_suffix="",
function_name_prefix="my_func_",
function_name_suffix=""
] "filename.c"
Examples
Some examples are in the tests/examples
directory.
Many of these examples are quick-and-dirty proofs, and should not necessary be considered the best style.
None-the-less, some of the examples available are, in approximate increasing level of difficulty:
-
Simple.thy
: Proofs of some simple functions, includingmax
andgcd
. -
Swap.thy
: Proof of a simpleswap
function. -
MultByAdd.thy
: Proof of a function that carries out multiplication using addition. -
Factorial.thy
: Proof of a factorial function, using several different methods. -
FibProof.thy
: Proof of the Fibonacci function, using several different methods. -
ListRev.thy
: Proof of a function that carries out an in-place linked list reversal. -
CList.thy
: Another list reversal, based on a proof by Mehta and Nipkow. See [the paper][3]. -
IsPrime.thy
: Proof of a function that determines if the input number is prime. -
Memset.thy
: Proof of a Cmemset
implementation. -
Quicksort.thy
: Proof of a simple quicksort implementation on an array ofint
s. -
BinarySearch.thy
: Proof of a function that determines if a sorted input array ofunsigned int
contains the givenunsigned int
. -
SchorrWaite.thy
: Proof a C implementation of the Schorr-Waite algorithm, using Mehta and Nipkow's high-level proof. See [the paper][3]. -
Memcpy.thy
: Proof of a Cmemcpy
implementation. The proof connects the C parser's byte-level heap with AutoCorres's type-safe heap representation.
There are also some examples that aren't about program proofs, but demonstrate AutoCorres features:
-
AC_Rename.thy
: how to change AutoCorres-generated names. -
TraceDemo.thy
: how to use the (experimental) tracing. -
type_strengthen_tricks.thy
: configuring type-strengthening. -
Incremental.thy
: (experimental) support for incremental translation.
Publications
L1 (SimplConv), L2 (LocalVarExtract) and TS (TypeStrengthen) were described in
"Bridging the gap: Automatic verified abstraction of C"
David Greenaway, June Andronick, Gerwin Klein
Proceedings of the Third International
Conference on Interactive Theorem Proving (ITP), August 2012.
https://trustworthy.systems/publications/nicta_full_text/5662.pdf
HL (heap abstraction) and WA (word abstraction) were described in
[3]: "Don’t sweat the small stuff --- Formal verification of C code without the pain" David Greenaway, Japheth Lim, June Andronick, Gerwin Klein Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, June 2014. https://trustworthy.systems/publications/nicta_full_text/7629.pdf
A more comprehensive source is
"Automated proof-producing abstraction of C code"
David Greenaway
PhD thesis, March 2015.
https://trustworthy.systems/publications/nicta_full_text/8758.pdf