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:
- Use the Isabelle session heap
CParserthat is created by installation - Import the theory
CTranslation - Load ('install') C files into your theories with the Isar command
install_C_file.
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.
The C parser provides a command install_C_file that parses and translates
a single .c file, potentially with include files, into Isabelle.
The syntax is as follows
install_C_file <main options> "file-path" [<param options>]where <main options> are zero or more of the following, separated by space.
They have to be provided in the order listed below.
memsafe: automatically attempt to prove memory safety for separation logic frame rulesc_types: only define the types in the C code, leave out function definitionsc_defs: only provide C definitions, leave out type definitionsno_modifies: do not generate "modifies" proofs (frame theorems that indicate the global variables each function can change).
If neither of c_types and c_defs are supplied, both will be produced.
Following the file name an optional comma-separated list <param-options>
enclosed in square brackets can be provided. These are:
machinety=<type_name>: define an additional state fieldphantom_machine_stateof typetype_nameas part of the state record. This is intended to be used for variable read/write state that is not visible to standard C semantics, and can be read/written inAUXUPDannotations, modifies clauses, andSPECannotations.ghostty=<type_name>: define an additional state fieldghost'stateof typetype_nameas part of the global state record. This state is intended to be ghost state. It can only be written to from the program viaGHOSTUPDannotations, but not read by normal C code. It is accessible and useful in Hoare logic assertions.roots=[fun_name_1, fun_name_2, ...]: only translate functionsfun_name_1,fun_name_2, etc, including all functions called by them, but ignoring the rest of the functions in the provided file. This is useful for verifying specific functions in a larger C context that is not entirely in the StrictC subset.
An example that uses all options:
install_C_file memsafe c_types c_defs no_modifies "file.c"
[machinety=int, ghostty=nat, roots=[f, g, h]]Definitions will be deposited into a locale with the same name as the base name
of the C file without extension, i.e. the locale file in the example above.
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 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. POPL'07, pages 97-108, ACM, 2007. DOI 10.1145/1190215.1190234.
- Harvey Tuch. Formal memory models for verifying C systems code. PhD thesis, University of New South Wales, 2008. DOI 10.26190/unsworks/17927.
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 (
...) staticlocal variables- limited support for function pointers
Current release:
- c-parser-1.21.tar.gz (Released 2024-10-11, Isabelle 2024)
Older releases:
- c-parser-1.20.tar.gz (Released 2023-11-03, Isabelle 2023)
- c-parser-1.19.tar.gz (Released 2022-10-31, Isabelle 2021-1)
- c-parser-1.18.tar.gz (Released 2021-10-31, Isabelle 2021)
- c-parser-1.17.tar.gz (Released 2020-11-02, Isabelle 2020)
- c-parser-1.16.1.tar.gz (Released 2019-10-03, Isabelle 2019)
- c-parser-1.16.0.tar.gz (Released 2019-09-05, Isabelle 2019)
- c-parser-1.15.0.tar.gz (Released 2018-09-05, Isabelle 2018)
- c-parser-1.14.0.tar.gz (Released 2018-03-02, Isabelle 2017)
- c-parser-1.13.0.tar.gz (Released 2013-05-06, Isabelle 2013)
- c-parser-1.12.0.tar.gz (Released 2012-12-05, Isabelle 2012)
- c-parser-1.0.tar.gz (Released 2012-09-24, Isabelle 2011-1)
The StrictC translation tool itself is available under the BSD 2-Clause license. It builds on the following open source projects by others.
-
Norbert Schirmer's Simpl language and associated VCG tool.
Sources for this are found in the Simpl/ directory. The code is covered by the LGPL licence.
-
Code from SML/NJ:
- an implementation of binary sets (Binaryset.ML)
- the mllex and mlyacc tools (tools/{mllex,mlyacc})
- command-line option parsing (standalone-parser/GetOpt)
This code is covered by SML/NJ's BSD-ish licence.
-
Code from the mlton compiler:
- regions during lexing and parsing (Region.ML, SourceFile.ML and SourcePos.ML)
This code is governed by a BSD licence.
See http://mlton.org