Create CBMC developer guide documentation

doc/architectural/background-concepts.md

@@ -0,0 +1,32 @@
+\ingroup module_hidden 
+\page background-concepts Background Concepts
+
+\author Martin Brain, Peter Schrammel
+
+# Representations #
+
+## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
+
+To be documented.
+
+## CFG ##
+
+To be documented.
+
+### SSA ###
+
+To be documented.
+
+# Analysis techniques #
+
+## Bounded model checking (from the CBMC manual) ##
+
+To be documented.
+
+## SAT and SMT ##
+
+To be documented.
+
+## Static analysis ##
+
+To be documented.

doc/architectural/bmct-class.md

@@ -0,0 +1,8 @@
+\ingroup module_hidden 
+\page bmct-class Bmct class
+
+\author
+
+## equation ##
+
+To be documented.

doc/architectural/cbmc-architecture.md

@@ -0,0 +1,96 @@
+\ingroup module_hidden 
+\page cbmc-architecture CBMC Architecture
+
+\author Martin Brain, Peter Schrammel
+
+This section provides a graphical overview of how CBMC fits together.
+CBMC takes C code or a goto-binary as input and tries to emit traces
+of executions that lead to crashes or undefined behaviour. The diagram
+below shows the intermediate steps in this process.
+
+\dot
+digraph G {
+
+  rankdir="TB";
+  node [shape=box, fontcolor=blue];
+
+  subgraph top {
+    rank=same;
+    1 -> 2 -> 3 -> 4;
+  }
+
+  subgraph bottom {
+    rank=same;
+    5 -> 6 -> 7 -> 8 -> 9;
+  }
+
+  /* shift bottom subgraph over */
+  9 -> 1 [color=white];
+
+  4 -> 5;
+
+  1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
+  2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
+  3 [label="language\ntype-checking" URL="\ref type-checking"];
+  4 [label="goto\nconversion" URL="\ref goto-conversion"];
+  5 [label="instrumentation" URL="\ref instrumentation"];
+  6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
+  7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
+  8 [label="decision\nprocedure" URL="\ref decision-procedure"];
+  9 [label="counter example\nproduction" URL="\ref counter-example-production"];
+}
+\enddot
+
+The \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
+perspective. Each node in the diagram above links to the appropriate
+class or module documentation, describing that particular stage in the
+CBMC pipeline.
+CPROVER is structured in a similar fashion to a compiler. It has
+language specific front-ends which perform limited syntactic analysis
+and then convert to an intermediate format. The intermediate format can
+be output to files (this is what `goto-cc` does) and are (informally)
+referred to as “goto binaries” or “goto programs”. The back-end are
+tools process this format, either directly from the front-end or from
+it’s saved output. These include a wide range of analysis and
+transformation tools (see \ref section-other-tools).
+
+# Concepts #
+## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
+
+To be documented.
+
+## Instrumentation (for test gen & CBMC & ...): Goto functions -> goto functions ##
+
+To be documented.
+
+## Goto functions -> BMC -> Counterexample (trace) ##
+
+To be documented.
+
+## Trace -> interpreter -> memory map ##
+
+To be documented.
+
+## Goto functions -> abstract interpretation ##
+
+To be documented.
+
+## Executables (flow of transformations): ##
+
+To be documented.
+
+### goto-cc ###
+
+To be documented.
+
+### goto-instrument ###
+
+To be documented.
+
+### cbmc ###
+
+To be documented.
+
+### goto-analyzer ###
+
+To be documented.

doc/architectural/compilation-and-development.md

@@ -0,0 +1,60 @@
+\ingroup module_hidden 
+\page compilation-and-development Compilation and Development
+
+\author Martin Brain, Peter Schrammel
+
+## Makefiles ##
+
+First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
+how to get, build and use CBMC. This document covers the
+internals of the system and how to get started on development.
+
+## CMake files ##
+
+To be documented.
+
+## Personal configuration: config.inc, macro DEBUG ##
+
+To be documented.
+
+## Documentation
+
+Apart from the (user-orientated) CBMC user manual and this document, most
+of the rest of the documentation is inline in the code as `doxygen` and
+some comments. A man page for CBMC, goto-cc and goto-instrument is
+contained in the `doc/` directory and gives some options for these
+tools. All of these could be improved and patches are very welcome. In
+some cases the algorithms used are described in the relevant papers.
+
+## Accessing doxygen documentation ##
+
+The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
+To build it locally, run `doxygen` in `/src`. HTML output will be created in
+`/doc/html`. The index page is `/doc/html/index.html`.
+
+## Coding standards ##
+
+See <a
+href="https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD.md">
+`CODING_STANDARD.md`</a> file in the root of the CBMC repository.
+
+CPROVER is written in a fairly minimalist subset of C++; templates and
+meta-programming are avoided except where necessary.
+External library dependencies are avoided (only STL and a SAT solver
+are required). Boost is not used. The `util` directory contains many
+utilities that are not (yet) in the standard library.
+
+Patches should be formatted so that code is indented with two space
+characters, not tab and wrapped to 80 columns. Headers for doxygen
+should be given (and preferably filled!) and the author will be the
+person who first created the file. Add doxygen comments to
+undocumented functions as you touch them. Coding standards
+and doxygen comments are enforced by CI before a patch can be
+merged by running `clang-format` and `cpplint`.
+
+Identifiers should be lower case with underscores to separate words.
+Types (classes, structures and typedefs) names must end with a `t`.
+Types that model types (i.e. C types in the program that is being
+interpreted) are named with `_typet`. For example `ui_message_handlert`
+rather than `UI_message_handlert` or `UIMessageHandler` and
+`union_typet`.