c-parser: turn README into main C-parser website
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
parent
f9359ead94
commit
c84bb14362
|
|
@ -1,4 +1,5 @@
|
|||
<!--
|
||||
Copyright 2024, Proofcraft Pty Ltd
|
||||
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||
|
||||
SPDX-License-Identifier: CC-BY-SA-4.0
|
||||
|
|
@ -7,29 +8,123 @@
|
|||
The StrictC translation tool
|
||||
============================
|
||||
|
||||
To install, see the file INSTALL in the `src/c-parser` directory.
|
||||
The StrictC translation tool, also called the Isabelle C parser, translates a
|
||||
large subset of C99 code into the imperative language [Simpl] embedded in the
|
||||
theorem prover [Isabelle/HOL]. The Simpl language provides a verified
|
||||
verification condition generator and further tools for software verification.
|
||||
The tool is aimed at Isabelle/HOL experts with knowledge in program
|
||||
verification, reasoning in [Isabelle/HOL], Hoare logic, and C semantics.
|
||||
|
||||
The semantics the parser produces contains a C memory model that can be used to
|
||||
reason about the behaviour of low-level C programs. The memory model admits more
|
||||
behaviours than the C standard -- in particular, it does not require that memory
|
||||
be allocated via `alloc`, because this library function does typically not yet
|
||||
exist in low-level code such as OS kernel implementation.
|
||||
|
||||
To install, we recommend using one of the [releases] provided below and see the
|
||||
file INSTALL in the `src/c-parser` directory. You will need Isabelle and the
|
||||
[MLton compiler] for Standard ML.
|
||||
|
||||
To use:
|
||||
|
||||
1. Use the heap CParser that is created by installation
|
||||
2. Import the theory CTranslation
|
||||
1. Use the Isabelle session heap `CParser` that is created by installation
|
||||
2. Import the theory `CTranslation`
|
||||
3. Load ('install') C files into your theories with the Isar command
|
||||
`install_C_file`.
|
||||
|
||||
See `docs/ctranslation.pdf` for more information about the options
|
||||
and C language semantics that this tool provides.
|
||||
The [AutoCorres] tool can abstract and simplify most Simpl C code generated by
|
||||
the parser and is aimed at easing C verification. See the [AutoCorres] web page
|
||||
for more information.
|
||||
|
||||
See also the examples in the testfiles directory. For example,
|
||||
`breakcontinue.thy` is a fairly involved demonstration of doing things
|
||||
the hard way.
|
||||
[Isabelle/HOL]: https://isabelle.in.tum.de
|
||||
[Simpl]: https://isa-afp.org/entries/Simpl.html
|
||||
[releases]: #releases
|
||||
[testfiles]: testfiles/
|
||||
[breakcontinue]: testfiles/breakcontinue.thy
|
||||
[MLton compiler]: http://mlton.org
|
||||
[AutoCorres]: https://trustworthy.systems/projects/OLD/autocorres/
|
||||
|
||||
----------------------------------------------------------------------
|
||||
The translation tool builds on various open source projects by others.
|
||||
Documentation
|
||||
-------------
|
||||
|
||||
The [releases] contain the file `docs/ctranslation.pdf` which provides more
|
||||
information about the options and C language semantics that this tool provides.
|
||||
|
||||
See also the examples in the [testfiles] directory. For example,
|
||||
[`breakcontinue.thy`][breakcontinue] is a fairly involved demonstration of doing
|
||||
things the hard way.
|
||||
|
||||
|
||||
The following academic publications describe the C parser, C subset, and memory
|
||||
model:
|
||||
|
||||
- Harvey Tuch, Gerwin Klein, Micheal Norrish. [Types, bytes, and separation logic][1].
|
||||
POPL'07, pages 97-108, ACM, 2007.
|
||||
DOI [10.1145/1190215.1190234](https://doi.org/10.1145/1190215.1190234).
|
||||
- Harvey Tuch. [Formal memory models for verifying C systems code][2]. PhD thesis,
|
||||
University of New South Wales, 2008.
|
||||
DOI [10.26190/unsworks/17927](https://doi.org/10.26190/unsworks/17927).
|
||||
|
||||
[1]: https://trustworthy.systems/publications/papers/Tuch_KN_07.abstract
|
||||
[2]: https://trustworthy.systems/publications/papers/Tuch:phd.abstract
|
||||
|
||||
Supported C Subset
|
||||
------------------
|
||||
|
||||
The C parser supports a large subset of C99. The following C features are not
|
||||
supported:
|
||||
|
||||
- taking the address of local variables
|
||||
- floating point types
|
||||
- side effects in expressions, pre-increment and pre-decrement operators
|
||||
- `goto`
|
||||
- switch fall-through cases
|
||||
- variadic argument lists (`...`)
|
||||
- `static` local variables
|
||||
- limited support for function pointers
|
||||
|
||||
Releases
|
||||
--------
|
||||
|
||||
Current release:
|
||||
|
||||
- [c-parser-1.20.tar.gz][1.20] (Released 2023-11-03, Isabelle 2023)
|
||||
|
||||
Older releases:
|
||||
|
||||
- [c-parser-1.19.tar.gz][1.19] (Released 2022-10-31, Isabelle 2021-1)
|
||||
- [c-parser-1.18.tar.gz][1.18] (Released 2021-10-31, Isabelle 2021)
|
||||
- [c-parser-1.17.tar.gz][1.17] (Released 2020-11-02, Isabelle 2020)
|
||||
- [c-parser-1.16.1.tar.gz][1.16.1] (Released 2019-10-03, Isabelle 2019)
|
||||
- [c-parser-1.16.0.tar.gz][1.16.0] (Released 2019-09-05, Isabelle 2019)
|
||||
- [c-parser-1.15.0.tar.gz][1.15] (Released 2018-09-05, Isabelle 2018)
|
||||
- [c-parser-1.14.0.tar.gz][1.14] (Released 2018-03-02, Isabelle 2017)
|
||||
- [c-parser-1.13.0.tar.gz][1.13] (Released 2013-05-06, Isabelle 2013)
|
||||
- [c-parser-1.12.0.tar.gz][1.12] (Released 2012-12-05, Isabelle 2012)
|
||||
- [c-parser-1.0.tar.gz][1.0] (Released 2012-09-24, Isabelle 2011-1)
|
||||
|
||||
[1.20]: https://github.com/seL4/l4v/releases/download/autocorres-1.10/c-parser-1.20.tar.gz
|
||||
[1.19]: https://github.com/seL4/l4v/releases/download/autocorres-1.9/c-parser-1.19.tar.gz
|
||||
[1.18]: https://github.com/seL4/l4v/releases/download/autocorres-1.8/c-parser-1.18.tar.gz
|
||||
[1.17]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.17.tar.gz
|
||||
[1.16.1]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.16.1.tar.gz
|
||||
[1.16.0]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.16.0.tar.gz
|
||||
[1.15]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.15.0.tar.gz
|
||||
[1.14]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.14.0.tar.gz
|
||||
[1.13]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.13.0.tar.gz
|
||||
[1.12]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.12.0.tar.gz
|
||||
[1.0]: https://c-parser.s3.us-east-2.amazonaws.com/c-parser-1.0.tar.gz
|
||||
|
||||
License
|
||||
-------
|
||||
|
||||
The StrictC translation tool itself is available under the BSD 2-Clause license.
|
||||
It builds on the following open source projects by others.
|
||||
|
||||
1. Norbert Schirmer's Simpl language and associated VCG tool.
|
||||
|
||||
Sources for this are found in the Simpl/ directory. The
|
||||
code is covered by an LGPL licence.
|
||||
Sources for this are found in the [Simpl/](Simpl/) directory. The
|
||||
code is covered by the LGPL licence.
|
||||
|
||||
See <https://isa-afp.org/entries/Simpl.html>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue