2 \page cprover-architecture-overview CProver Architecture Overview
4 \author Martin Brain, Peter Schrammel
6 \section overview-dirs Overview of CPROVER Directories
10 The source code is divided into a number of sub-directories, each
11 containing the code for a different part of the system.
24 * \ref pointer-analysis
31 * Language API: \ref langapi
34 * Java: \ref java_bytecode
35 * JavaScript: \ref jsil
42 * \ref goto-instrument
57 In the top level of `src` there are only a few files:
59 * `config.inc`: The user-editable configuration parameters for the
60 build process. The main use of this file is setting the paths for the
61 various external SAT solvers that are used. As such, anyone building
62 from source will likely need to edit this.
64 * `Makefile`: The main systems Make file. Parallel builds are
65 supported and encouraged; please don’t break them!
67 * `common`: System specific magic required to get the system to build.
68 This should only need to be edited if porting CBMC to a new platform /
71 * `doxygen.cfg`: The config file for doxygen.cfg
75 Contains the CBMC man page. Doxygen HTML pages are generated
76 into the `doc/html` directory when running `doxygen` from `src`.
80 The `regression/` directory contains the test suites.
81 They are grouped into directories for each of the tools/modules.
82 Each of these contains a directory per test case, containing a C or C++
83 file that triggers the bug and a `.desc` file that describes
84 the tests, expected output and so on. There is a Perl script,
85 `test.pl` that is used to invoke the tests as:
87 ../test.pl -c PATH_TO_CBMC
89 The `–help` option gives instructions for use and the
90 format of the description files.
93 \section general-info General Information
95 First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
96 how to get, build and use CBMC. This document covers the
97 internals of the system and how to get started on development.
101 Apart from the (user-orientated) CBMC user manual and this document, most
102 of the rest of the documentation is inline in the code as `doxygen` and
103 some comments. A man page for CBMC, goto-cc and goto-instrument is
104 contained in the `doc/` directory and gives some options for these
105 tools. All of these could be improved and patches are very welcome. In
106 some cases the algorithms used are described in the relevant papers.
110 This section provides a graphical overview of how CBMC fits together.
111 CBMC takes C code or a goto-binary as input and tries to emit traces
112 of executions that lead to crashes or undefined behaviour. The diagram
113 below shows the intermediate steps in this process.
119 node [shape=box, fontcolor=blue];
128 5 -> 6 -> 7 -> 8 -> 9;
131 /* shift bottom subgraph over */
132 9 -> 1 [color=white];
136 1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
137 2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
138 3 [label="language\ntype-checking" URL="\ref type-checking"];
139 4 [label="goto\nconversion" URL="\ref goto-conversion"];
140 5 [label="instrumentation" URL="\ref instrumentation"];
141 6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
142 7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
143 8 [label="decision\nprocedure" URL="\ref decision-procedure"];
144 9 [label="counter example\nproduction" URL="\ref counter-example-production"];
148 The \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
149 perspective. Each node in the diagram above links to the appropriate
150 class or module documentation, describing that particular stage in the
152 CPROVER is structured in a similar fashion to a compiler. It has
153 language specific front-ends which perform limited syntactic analysis
154 and then convert to an intermediate format. The intermediate format can
155 be output to files (this is what `goto-cc` does) and are (informally)
156 referred to as “goto binaries” or “goto programs”. The back-end are
157 tools process this format, either directly from the front-end or from
158 it’s saved output. These include a wide range of analysis and
159 transformation tools (see \ref other-tools).
163 See `CODING_STANDARD.md` file in the root of the CBMC repository.
165 CPROVER is written in a fairly minimalist subset of C++; templates and
166 meta-programming are avoided except where necessary.
167 External library dependencies are avoided (only STL and a SAT solver
168 are required). Boost is not used. The `util` directory contains many
169 utilities that are not (yet) in the standard library.
171 Patches should be formatted so that code is indented with two space
172 characters, not tab and wrapped to 80 columns. Headers for doxygen
173 should be given (and preferably filled!) and the author will be the
174 person who first created the file. Add doxygen comments to
175 undocumented functions as you touch them. Coding standards
176 and doxygen comments are enforced by CI before a patch can be
177 merged by running `clang-format` and `cpplint`.
179 Identifiers should be lower case with underscores to separate words.
180 Types (classes, structures and typedefs) names must end with a `t`.
181 Types that model types (i.e. C types in the program that is being
182 interpreted) are named with `_typet`. For example `ui_message_handlert`
183 rather than `UI_message_handlert` or `UIMessageHandler` and
187 \section other-tools Other Tools
189 FIXME: The text in this section is a bit outdated.
191 The CPROVER subversion archive contains a number of separate programs.
192 Others are developed separately as patches or separate
193 branches.Interfaces are have been and are continuing to stablise but
194 older code may require work to compile and function correctly.
198 * `CBMC`: A bounded model checking tool for C and C++. See
201 * `goto-cc`: A drop-in, flag compatible replacement for GCC and other
202 compilers that produces goto-programs rather than executable binaries.
205 * `goto-instrument`: A collection of functions for instrumenting and
206 modifying goto-programs. See \ref goto-instrument.
208 Model checkers and similar tools:
210 * `SatABS`: A CEGAR model checker using predicate abstraction. Is
211 roughly 10,000 lines of code (on top of the CPROVER code base) and is
212 developed in its own subversion archive. It uses an external model
213 checker to find potentially feasible paths. Key limitations are
214 related to code with pointers and there is scope for significant
217 * `Scratch`: Alistair Donaldson’s k-induction based tool. The
218 front-end is in the old project CVS and some of the functionality is
219 in `goto-instrument`.
221 * `Wolverine`: An implementation of Ken McMillan’s IMPACT algorithm
222 for sequential programs. In the old project CVS.
224 * `C-Impact`: An implementation of Ken McMillan’s IMPACT algorithm for
225 parallel programs. In the old project CVS.
227 * `LoopFrog`: A loop summarisation tool.
229 * `TAN`: Christoph’s termination analyser.
231 Test case generation:
233 * `cover`: A basic test-input generation tool. In the old
236 * `FShell`: A test-input generation tool that allows the user to
237 specify the desired coverage using a custom language (which includes
238 regular expressions over paths). It uses incremental SAT and is thus
239 faster than the naïve “add assertions one at a time and use the
240 counter-examples” approach. Is developed in its own subversion.
242 Alternative front-ends and input translators:
244 * `Scoot`: A System-C to C translator. Probably in the old
247 * `???`: A Simulink to C translator. In the old project CVS.
249 * `???`: A Verilog front-end. In the old project CVS.
251 * `???`: A converter from Codewarrior project files to Makefiles. In
256 * `ai`: Leo’s hybrid abstract interpretation / CEGAR tool.
258 * `DeltaCheck?`: Ajitha’s slicing tool, aimed at locating changes and
259 differential verification. In the old project CVS.
261 There are tools based on the CPROVER framework from other research
262 groups which are not listed here.