cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/cbmc-architecture.md
Go to the documentation of this file.
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 section-goto-transforms"];
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 [CPROVER User Manual](http://www.cprover.org/cprover-manual/) describes
45 CBMC from a user perspective. Each node in the diagram above links to the
46 appropriate class or module documentation, describing that particular stage
47 in the 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 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: 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 ### goto-cc ###
81 
82 To be documented.
83 
84 ### goto-instrument ###
85 
86 To be documented.
87 
88 ### cbmc ###
89 
90 To be documented.
91 
92 ### goto-analyzer ###
93 
94 To be documented.