From a71f90a3ea8061b9c645a5d7a6605e06fb38a711 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Tue, 16 Jan 2024 11:32:36 +1100
Subject: [PATCH] c-parser: turn README into main C-parser website

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 tools/c-parser/README.md | 123 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 109 insertions(+), 14 deletions(-)

diff --git a/tools/c-parser/README.md b/tools/c-parser/README.md
index ca00754bde..f765baeea4 100644
--- a/tools/c-parser/README.md
+++ b/tools/c-parser/README.md
@@ -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.
-
-See also the examples in the testfiles directory.  For example,
-`breakcontinue.thy` is a fairly involved demonstration of doing things
-the hard way.
-
-----------------------------------------------------------------------
-The translation tool builds on various open source projects by others.
+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.
+
+[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/
+
+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>