cprover
/builddir/build/BUILD/cbmc-cbmc-5.9/doc/architectural/cprover-architecture-overview.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page cprover-architecture-overview CProver Architecture Overview
3 
4 \author Martin Brain, Peter Schrammel
5 
6 \section overview-dirs Overview of CPROVER Directories
7 
8 ## `src/`
9 
10 The source code is divided into a number of sub-directories, each
11 containing the code for a different part of the system.
12 
13 - GOTO-Programs
14 
15  * \ref goto-programs
16  * \ref linking
17 
18 - Symbolic Execution
19  * \ref goto-symex
20 
21 - Static Analyses
22 
23  * \ref analyses
24  * \ref pointer-analysis
25 
26 - Solvers
27  * \ref solvers
28 
29 - Language Front Ends
30 
31  * Language API: \ref langapi
32  * C: \ref ansi-c
33  * C++: \ref cpp
34  * Java: \ref java_bytecode
35  * JavaScript: \ref jsil
36 
37 - Tools
38 
39  * \ref cbmc
40  * \ref clobber
41  * \ref goto-analyzer
42  * \ref goto-instrument
43  * \ref goto-diff
44  * \ref memory-models
45  * \ref goto-cc
46  * \ref jbmc
47 
48 - Utilities
49 
50  * \ref big-int
51  * \ref json
52  * \ref xmllang
53  * \ref util
54  * \ref miniz
55  * \ref nonstd
56 
57 In the top level of `src` there are only a few files:
58 
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.
63 
64 * `Makefile`: The main systems Make file. Parallel builds are
65  supported and encouraged; please don’t break them!
66 
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 /
69  build environment.
70 
71 * `doxygen.cfg`: The config file for doxygen.cfg
72 
73 ## `doc/`
74 
75 Contains the CBMC man page. Doxygen HTML pages are generated
76 into the `doc/html` directory when running `doxygen` from `src`.
77 
78 ## `regression/`
79 
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:
86 
87  ../test.pl -c PATH_TO_CBMC
88 
89 The `–help` option gives instructions for use and the
90 format of the description files.
91 
92 
93 \section general-info General Information
94 
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.
98 
99 ## Documentation
100 
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.
107 
108 ## Architecture
109 
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.
114 
115 \dot
116 digraph G {
117 
118  rankdir="TB";
119  node [shape=box, fontcolor=blue];
120 
121  subgraph top {
122  rank=same;
123  1 -> 2 -> 3 -> 4;
124  }
125 
126  subgraph bottom {
127  rank=same;
128  5 -> 6 -> 7 -> 8 -> 9;
129  }
130 
131  /* shift bottom subgraph over */
132  9 -> 1 [color=white];
133 
134  4 -> 5;
135 
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"];
145 }
146 \enddot
147 
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
151 CBMC pipeline.
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).
160 
161 ## Coding Standards
162 
163 See `CODING_STANDARD.md` file in the root of the CBMC repository.
164 
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.
170 
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`.
178 
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
184 `union_typet`.
185 
186 
187 \section other-tools Other Tools
188 
189 FIXME: The text in this section is a bit outdated.
190 
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.
195 
196 In the main archive:
197 
198 * `CBMC`: A bounded model checking tool for C and C++. See
199  \ref cbmc.
200 
201 * `goto-cc`: A drop-in, flag compatible replacement for GCC and other
202  compilers that produces goto-programs rather than executable binaries.
203  See \ref goto-cc.
204 
205 * `goto-instrument`: A collection of functions for instrumenting and
206  modifying goto-programs. See \ref goto-instrument.
207 
208 Model checkers and similar tools:
209 
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
215  improvement.
216 
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`.
220 
221 * `Wolverine`: An implementation of Ken McMillan’s IMPACT algorithm
222  for sequential programs. In the old project CVS.
223 
224 * `C-Impact`: An implementation of Ken McMillan’s IMPACT algorithm for
225  parallel programs. In the old project CVS.
226 
227 * `LoopFrog`: A loop summarisation tool.
228 
229 * `TAN`: Christoph’s termination analyser.
230 
231 Test case generation:
232 
233 * `cover`: A basic test-input generation tool. In the old
234  project CVS.
235 
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.
241 
242 Alternative front-ends and input translators:
243 
244 * `Scoot`: A System-C to C translator. Probably in the old
245  project CVS.
246 
247 * `???`: A Simulink to C translator. In the old project CVS.
248 
249 * `???`: A Verilog front-end. In the old project CVS.
250 
251 * `???`: A converter from Codewarrior project files to Makefiles. In
252  the old project CVS.
253 
254 Other tools:
255 
256 * `ai`: Leo’s hybrid abstract interpretation / CEGAR tool.
257 
258 * `DeltaCheck?`: Ajitha’s slicing tool, aimed at locating changes and
259  differential verification. In the old project CVS.
260 
261 There are tools based on the CPROVER framework from other research
262 groups which are not listed here.