Skip to content

Commit 6a36fa4

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide
Create structure for CBMC developer documentation
2 parents 61a8c30 + 612b4f8 commit 6a36fa4

14 files changed

+615
-266
lines changed

‎doc/architectural/background-concepts.md

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
\ingroup module_hidden
2+
\page background-concepts Background Concepts
3+
4+
\author Martin Brain, Peter Schrammel
5+
6+
# Representations #
7+
8+
## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
9+
10+
To be documented.
11+
12+
## CFG ##
13+
14+
To be documented.
15+
16+
### SSA ###
17+
18+
To be documented.
19+
20+
# Analysis techniques #
21+
22+
## Bounded model checking (from the CBMC manual) ##
23+
24+
To be documented.
25+
26+
## SAT and SMT ##
27+
28+
To be documented.
29+
30+
## Static analysis ##
31+
32+
To be documented.

‎doc/architectural/bmct-class.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
\ingroup module_hidden
2+
\page bmct-class Bmct class
3+
4+
\author
5+
6+
## equation ##
7+
8+
To be documented.

‎doc/architectural/cbmc-architecture.md

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
\ingroup module_hidden
2+
\page cbmc-architecture CBMC Architecture
3+
4+
\author Martin Brain, Peter Schrammel
5+
6+
This section provides a graphical overview of how CBMC fits together.
7+
CBMC takes C code or a goto-binary as input and tries to emit traces
8+
of executions that lead to crashes or undefined behaviour. The diagram
9+
below shows the intermediate steps in this process.
10+
11+
\dot
12+
digraph G {
13+
14+
rankdir="TB";
15+
node [shape=box, fontcolor=blue];
16+
17+
subgraph top {
18+
rank=same;
19+
1 -> 2 -> 3 -> 4;
20+
}
21+
22+
subgraph bottom {
23+
rank=same;
24+
5 -> 6 -> 7 -> 8 -> 9;
25+
}
26+
27+
/* shift bottom subgraph over */
28+
9 -> 1 [color=white];
29+
30+
4 -> 5;
31+
32+
1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
33+
2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
34+
3 [label="language\ntype-checking" URL="\ref type-checking"];
35+
4 [label="goto\nconversion" URL="\ref goto-conversion"];
36+
5 [label="instrumentation" URL="\ref instrumentation"];
37+
6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
38+
7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
39+
8 [label="decision\nprocedure" URL="\ref decision-procedure"];
40+
9 [label="counter example\nproduction" URL="\ref counter-example-production"];
41+
}
42+
\enddot
43+
44+
The \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
45+
perspective. Each node in the diagram above links to the appropriate
46+
class or module documentation, describing that particular stage in the
47+
CBMC pipeline.
48+
CPROVER is structured in a similar fashion to a compiler. It has
49+
language specific front-ends which perform limited syntactic analysis
50+
and then convert to an intermediate format. The intermediate format can
51+
be output to files (this is what `goto-cc` does) and are (informally)
52+
referred to as “goto binaries” or “goto programs”. The back-end are
53+
tools process this format, either directly from the front-end or from
54+
it’s saved output. These include a wide range of analysis and
55+
transformation tools (see \ref section-other-tools).
56+
57+
# Concepts #
58+
## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
59+
60+
To be documented.
61+
62+
## Instrumentation (for test gen & CBMC & ...): Goto functions -> goto functions ##
63+
64+
To be documented.
65+
66+
## Goto functions -> BMC -> Counterexample (trace) ##
67+
68+
To be documented.
69+
70+
## Trace -> interpreter -> memory map ##
71+
72+
To be documented.
73+
74+
## Goto functions -> abstract interpretation ##
75+
76+
To be documented.
77+
78+
## Executables (flow of transformations): ##
79+
80+
To be documented.
81+
82+
### goto-cc ###
83+
84+
To be documented.
85+
86+
### goto-instrument ###
87+
88+
To be documented.
89+
90+
### cbmc ###
91+
92+
To be documented.
93+
94+
### goto-analyzer ###
95+
96+
To be documented.

‎doc/architectural/compilation-and-development.md

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
\ingroup module_hidden
2+
\page compilation-and-development Compilation and Development
3+
4+
\author Martin Brain, Peter Schrammel
5+
6+
## Makefiles ##
7+
8+
First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
9+
how to get, build and use CBMC. This document covers the
10+
internals of the system and how to get started on development.
11+
12+
## CMake files ##
13+
14+
To be documented.
15+
16+
## Personal configuration: config.inc, macro DEBUG ##
17+
18+
To be documented.
19+
20+
## Documentation
21+
22+
Apart from the (user-orientated) CBMC user manual and this document, most
23+
of the rest of the documentation is inline in the code as `doxygen` and
24+
some comments. A man page for CBMC, goto-cc and goto-instrument is
25+
contained in the `doc/` directory and gives some options for these
26+
tools. All of these could be improved and patches are very welcome. In
27+
some cases the algorithms used are described in the relevant papers.
28+
29+
## Accessing doxygen documentation ##
30+
31+
The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
32+
To build it locally, run `doxygen` in `/src`. HTML output will be created in
33+
`/doc/html`. The index page is `/doc/html/index.html`.
34+
35+
## Coding standards ##
36+
37+
See <a
38+
href="https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD.md">
39+
`CODING_STANDARD.md`</a> file in the root of the CBMC repository.
40+
41+
CPROVER is written in a fairly minimalist subset of C++; templates and
42+
meta-programming are avoided except where necessary.
43+
External library dependencies are avoided (only STL and a SAT solver
44+
are required). Boost is not used. The `util` directory contains many
45+
utilities that are not (yet) in the standard library.
46+
47+
Patches should be formatted so that code is indented with two space
48+
characters, not tab and wrapped to 80 columns. Headers for doxygen
49+
should be given (and preferably filled!) and the author will be the
50+
person who first created the file. Add doxygen comments to
51+
undocumented functions as you touch them. Coding standards
52+
and doxygen comments are enforced by CI before a patch can be
53+
merged by running `clang-format` and `cpplint`.
54+
55+
Identifiers should be lower case with underscores to separate words.
56+
Types (classes, structures and typedefs) names must end with a `t`.
57+
Types that model types (i.e. C types in the program that is being
58+
interpreted) are named with `_typet`. For example `ui_message_handlert`
59+
rather than `UI_message_handlert` or `UIMessageHandler` and
60+
`union_typet`.

0 commit comments

Comments
 (0)