1c26e288c8
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| Simpl | ||
| doc | ||
| recursive_records | ||
| standalone-parser | ||
| testfiles | ||
| tools | ||
| umm_heap | ||
| .gitignore | ||
| Absyn-CType.ML | ||
| Absyn-Expr.ML | ||
| Absyn-Serial.ML | ||
| Absyn-StmtDecl.ML | ||
| Absyn.ML | ||
| Binaryset.ML | ||
| CLanguage.thy | ||
| CProof.thy | ||
| CTranslation.thy | ||
| Feedback.ML | ||
| FunctionalRecordUpdate.ML | ||
| General.ML | ||
| HPInter.ML | ||
| INSTALL.md | ||
| IndirectCalls.thy | ||
| LemmaBucket_C.thy | ||
| MANIFEST | ||
| MString.ML | ||
| Makefile | ||
| MemoryModelExtras-sig.ML | ||
| MemoryModelExtras.ML | ||
| ModifiesProofs.thy | ||
| PackedTypes.thy | ||
| PrettyProgs.thy | ||
| README.md | ||
| RELEASES.md | ||
| ROOT | ||
| Region.ML | ||
| RegionExtras.ML | ||
| SourceFile.ML | ||
| SourcePos.ML | ||
| StaticFun.thy | ||
| StrictC.grm | ||
| StrictC.lex | ||
| StrictCParser.ML | ||
| Target-generic32.ML | ||
| TargetNumbers-sig.ML | ||
| TypHeapLib.thy | ||
| UMM_Proofs.ML | ||
| UMM_termstypes.ML | ||
| basics.ML | ||
| calculate_state.ML | ||
| complit.ML | ||
| expression_translation.ML | ||
| expression_typing.ML | ||
| globalmakevars | ||
| heapstatetype.ML | ||
| hp_termstypes.ML | ||
| isa_termstypes.ML | ||
| isar_install.ML | ||
| mkrelease | ||
| modifies_proofs.ML | ||
| name_generation.ML | ||
| openUnsynch.ML | ||
| program_analysis.ML | ||
| shorten_names.ML | ||
| static-fun.ML | ||
| stmt_translation.ML | ||
| syntax_transforms.ML | ||
| termstypes-sig.ML | ||
| termstypes.ML | ||
| topo_sort.ML | ||
| use.ML | ||
README.md
The StrictC translation tool
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.
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 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.
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 (
...) staticlocal variables- limited support for function pointers
Releases
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)
License
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