Create CBMC developer guide documentation #2615
Conversation
owen-mc-diffblue
requested review from
chrisr-diffblue,
kroening,
smowton and
tautschnig
as code owners
|
|
||
| subgraph top { | ||
| rank=same; | ||
| 1 -> 2 -> 3 -> 4; |
There was a problem hiding this comment.
You can give these informative short names instead of 1, 2, 3, ...
There was a problem hiding this comment.
I didn't write this. It seems clear enough to me.
| 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 ## |
There was a problem hiding this comment.
Some ascii arrows, some unicode ones
|
|
||
| FIXME | ||
|
|
||
| ## Instrumentation (for test gen & CBMC & …): Goto functions -> goto functions ## |
There was a problem hiding this comment.
Similarly pick between ASCII and unicode ellipses
| @@ -70,12 +255,12 @@ In the top level of `src` there are only a few files: | |||
|
|
|||
| * `doxygen.cfg`: The config file for doxygen.cfg | |||
|
|
|||
| ## `doc/` | |||
| ## `doc/` ## | |||
There was a problem hiding this comment.
FWIW I think this is unnecessary in markdown
There was a problem hiding this comment.
Yeah, I discovered it yesterday and thought it might make the titles stand out more when looking at the source
| some cases the algorithms used are described in the relevant papers. | ||
| ## Strings: dstringt, the string_container and the ID_* ## | ||
| Within cbmc, strings are represented using irep_idt. By default this is | ||
| typedefed to dstringt, which stores a string as an index into a large |
There was a problem hiding this comment.
Probably use backticks for typenames etc
| 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. | ||
| ## Irept: a 4-triple (data, named-sub, comments-sub, sub) ## |
There was a problem hiding this comment.
Suggest put sub after data as the most-used part
There was a problem hiding this comment.
We should probably be consistent with the order they are listed in the documentation for irept (cf #2618), which is this order. It's also the order that they're listed in in irep.h.
|
|
||
| \dot | ||
| digraph G { | ||
| As that documentation says, irepts are generic tree nodes. You should |
There was a problem hiding this comment.
Mention that data is just a string (irep_idt)
| so a minus_exprt has ID_minus as its id(). This means that a | ||
| minus_exprt can be passed wherever an exprt is expected, and if you | ||
| want to check if the expression you are looking at is a minus | ||
| expression then you have to check its id(). |
There was a problem hiding this comment.
...or use can_cast_expr and cousins
| Many different kinds of statements inherit from codet, and they are | ||
| distinguished by their statement(). For example, a while loop would be | ||
| represented by a code_whilet, which has statement() ID_while. | ||
| Code_whilet has two operands in its sub, and helper functions to make |
There was a problem hiding this comment.
Don't capitalise types, even at start of sentence
| Code_whilet has two operands in its sub, and helper functions to make | ||
| it easier to use: cond() returns the first entry in its sub(), which | ||
| is the condition for the while loop, and body() returns the second | ||
| entry in its sub, which is the body of the while loop - this has to be |
There was a problem hiding this comment.
Worth defining and then using the terminology "first subexpression, second subexpression, ..." rather than "... in its sub"?
There was a problem hiding this comment.
Use backticks for code elements
| @@ -1,11 +1,196 @@ | |||
| \ingroup module_hidden | |||
| \page cprover-architecture-overview CProver Architecture Overview | |||
| \ingroup module_hidden | |||
There was a problem hiding this comment.
I'd split this into separate .md files. If you give them appropriate \page directives they will appear as pages within the CProver Developer Documentation section.
There was a problem hiding this comment.
Perhaps when this file starts getting too big I will split of large parts into their own pages and just link to them from this page. I like having the headings in this order, as I think this is roughly the order that a new developer would want to encounter the documentation.
| FIXME | ||
|
|
||
|
|
||
| \section section-folder-walkthrough Folder walkthrough |
There was a problem hiding this comment.
I'd appreciate if this was kept on top of one of the pages within CProver Developer Documentation as it is the most convenient entry point to access the module/directory documentation.
There was a problem hiding this comment.
I've moved it to a separate file.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 1bc437d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80002298
There was a problem hiding this comment.
Forgive me rambling but here is some context. I pushed Daniel to start the group wiki and got people to write some stuff for it (mostly still relevant but it was abandoned in the move to Diffblue). i also wrote the original internals documentation in a deal with @tautschnig . I got part way through writing the update but left it with @Charliemowood when I was reassigned. Some of it seems to have been committed by @peterschrammel but quite a bit appears to have been cut.
If this is the start of someone taking ownership of the documentation -- great. If it is an optimisitic "people will help out" ... it doesn't happen organically, or, at least, I never succeeded making it happen organically. I'd even be happy to help with the documentation push but I don't have time to lead a campaign.
|
|
||
| #### Martin #### | ||
|
|
||
| FIXME |
There was a problem hiding this comment.
Do I need to be fixed? :-(
There was a problem hiding this comment.
Ha. Yes, I think I failed to parse that properly. The outline came from Cesar and he presumably meant that you could fill in that section. I'll make that clearer.
There was a problem hiding this comment.
Probably what I meant was that Martin could help with the goto-analyzer section, or that I would ask him to complete the TOC of that section
|
|
||
| \author Martin Brain, Peter Schrammel |
There was a problem hiding this comment.
I was told not to remove authors.
There was a problem hiding this comment.
Oops. It wasn't my intention to remove authors. I deleted one file and moved most of its contents into a new file. Git has decided to represent this as moving the old file and adding a lot of things. I have reinstated them in the new file.
| 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 |
There was a problem hiding this comment.
Where does this text come from? It reminds me of some of my usual grammatical mistakes.
There was a problem hiding this comment.
Yes, I believe it is by you. It was in cprover-archicture-overview.md, which git has decided was renamed to CBMC-developer-guide.md in this PR. I think I moved it into a different section to match the order I was planning on.
@martin-cs, with Charlie I managed to get all the various sources of documentation integrated into http://cprover.diffblue.com. But we didn't get far in improving the structure and consolidating the texts back then. If you think that something is missing then please let me know. |
|
@martin-cs Thanks for your review. There is quite a lot of energy behind improving the documentation. The idea behind creating all the headers without most of the content is to say "This is the structure the documentation should take" so that people can work together to fill it in. I only really put the "FIXME" lines in to separate the headings and make it clearer what they were meant to be. I doubt that they will all be filled in in the next few months, but I believe that some of them will be. I've replaced them with "To be documented.", which I think better portrays my intent. |
|
@martin-cs I forgot to say that I have 1 day a week assigned to improving documentation and onboarding material for Diffblue, so I do intend to fill in some of the sections myself. (Or move documentation from other places to this document.) |
owen-mc-diffblue
force-pushed
the
doc/cbmc-developer-guide
branch
from
8d5ac3b to
a88f851
Compare
|
I believe I've addressed all review comments and this is ready for re-review. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 8d5ac3b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80117571
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a88f851).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80118390
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 70f0ad6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80121705
|
@peterschrammel @martin-cs Please re-review. |
|
|
||
| ### goto-analyzer ### | ||
|
|
||
| To be documented. (Martin?) |
There was a problem hiding this comment.
I don't mind being volunteered for things.
|
|
||
| ### cbmc ### | ||
|
|
||
| See <a href="https://github.com/diffblue/doc-diffblue-common/wiki/Talks#cbmc-for-coverage-test-generation-a-brief-tour"> |
There was a problem hiding this comment.
This link is useless because not publicly accessible.
| `union_typet`. | ||
|
|
||
|
|
||
| \section section-background-concepts Background Concepts |
There was a problem hiding this comment.
I'd put this section into a separate file
|
|
||
|
|
||
|
|
||
| \section section-other-tools Other Tools |
There was a problem hiding this comment.
Also, this section should probably become a separate file.
|
On Thu, 2018-07-26 at 06:55 -0700, owen-jones-diffblue wrote:
@martin-cs Thanks for your review. There is quite a lot of energy
behind improving the documentation.
Great! It's really important but so rarely are people willing to
commit time.
The idea behind creating all the headers without most of the content
is to say "This is the structure the documentation should take" so
that people can work together to fill it in.
From my experience, the best way of achieving this is to target
particular people and approach them directly.
I only really put the "FIXME" lines in to separate the headings and
make it clearer what they were meant to be. I doubt that they will
all be filled in in the next few months, but I believe that some of
them will be. I've replaced them with "To be documented.", which I
think better portrays my intent.
Fair. Target specific people. Trading time is always a good tactic,
as in "what can I do for an hour to give you time to write this
section".
@martin-cs I forgot to say that I have 1 day a week assigned to
improving documentation and onboarding material for Diffblue, so I do
intend to fill in some of the sections myself. (Or move documentation
from other places to this document.)
Brilliant! I'll dig out some notes to send to you.
|
|
|
||
| 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 |
There was a problem hiding this comment.
At one point we even used to have a link to the live doxygen on the web.
| 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. |
There was a problem hiding this comment.
Last few lines aren't about doxygen and should be in a separate section.
| interpreted) are named with `_typet`. For example `ui_message_handlert` | ||
| rather than `UI_message_handlert` or `UIMessageHandler` and | ||
| `union_typet`. | ||
|
|
There was a problem hiding this comment.
I'm unsure whether this should be here or in the coding style document itself. My feeling is that the coding style documents and the lint script that enforces them should be aligned.
There was a problem hiding this comment.
It should probably be in the coding standard. I'm going to leave it for now, to try and get this PR merged more quickly.
| ## Static analysis ## | ||
|
|
||
| To be documented. | ||
|
|
There was a problem hiding this comment.
This is quite a mix of representations and analysis techniques. I'd separate the two.
|
|
||
| \section section-cprover-architecture CPROVER Architecture | ||
|
|
||
| This section provides a graphical overview of how CBMC fits together. |
There was a problem hiding this comment.
CBMC \subseteq CPROVER This is the architecture of CBMC, not the architecture of CPROVER.
|
|
||
| \section section-folder-walkthrough Folder walkthrough | ||
|
|
||
| See [the folder walkthrough](\ref folder-walkthrough). |
There was a problem hiding this comment.
When explaining this, I try to work from the architecture diagram and then show how the architectural components map on to the directories.
There was a problem hiding this comment.
Yes, it isn't ideal having them on different pages. I'm going to leave it like this for now but it may well be changed in the future as more documentation is written.
| To be documented. | ||
|
|
||
|
|
||
| ## Examples: how to represent the AST of statements, focus on java ## |
There was a problem hiding this comment.
I've changed it to "how to represent the AST of statements, in C and in java"
| To be documented. | ||
|
|
||
| ## Generating doxygen documentation ## | ||
|
|
There was a problem hiding this comment.
If the latest version of this is going to be available in http://cprover.diffblue.com/ it should be worth mentioning it here.
Currently this is an outline - over time the various sections should be filled in. I have moved some of the existing documentation into it in the appropriate place.
The CBMC Developer Guide now contains a link to that file.
owen-mc-diffblue
force-pushed
the
doc/cbmc-developer-guide
branch
from
70f0ad6 to
612b4f8
Compare
|
I believe I've addressed most review comments. The ones I didn't address had merit but I will leave them for the future, in the hope of getting this PR merged sooner. @peterschrammel I have rearranged things so the major sections of the CBMC developer guide now appear as pages under "CProver Developer Documentation" (in the correct order), and there is no longer a page for the CBMC developer guide. |
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 612b4f8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80903005
|
@martin-cs Yes, if you have notes that you want turned into documentation then please send them to me and I'll give it a go. |
|
@owen-jones-diffblue : sent by e-mail |
|
@peterschrammel Would you like to look at this again or can I merge it? |
|
Nice to see this done. :) Edit: or shall we say living. |
4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration 01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor 9c3fd45 Add AWS CodeBuild badges 4261fd8 Remove appveyor badge fe23db7 Remove appveyor.yml 21857a7 Add support for getting components by name to `struct_exprt` 05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug 0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants 159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type 5ca6cd2 Restrict new clinit_wrapper calls to enum types 6e04213 Reformatting the structs to aid readability 0cfacb8 Add type2c conversion for specifying a type name c3fef70 Add a clean configuration for expr2c 3a40db1 Make expr2ct configurable in a number of ways 097cf71 Merge pull request diffblue#2731 from diffblue/increase-version 170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant c9e46ae Temporarily remove new UNREACHABLE statements 03e3877 Add tests for nondet initialization of enums 3e32140 CI lazy methods: load clinit for all param types 5542c54 Move nondet enum initialization to new function 6ecf4f9 Nondet-init enums by assigning them to a constant 6c84caa Refactor logic for generating a nondet int 07d1e44 Always run clinit_wrapper before nondet object init 3be826f Add some documentation to java_object_factory 5e80310 add invariant on parent-child class relationship 2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType c6acc9c increased version number in preparation for release 5.10 0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls 89048e6 Function-pointer remvoval: print human-friendly debug messages 1fc3118 Use pointer difference type when adding to pointer 072b592 Merge pull request diffblue#2726 from tautschnig/java-loc 4dca215 Goto program should not use java_method_typet 273fff4 Add can_cast_type and precondition. 6cb7e5d Reinstate require_code and add require_java_method 78f7cb7 Refactor constructors for java_method_typet 6cefc61 Unit tests conversion from code_typet to java_method_typet c3b8b5a Update tag in to_java_method_type 972315a Update docs on java_method_typet constructor 211931c Add tag for java_method_type 551df9c Update unit tests to use java_method_typet da18c9f Change variables named code_type to method_type f1bd41e Change code_typet to java_method_typet in jbmc be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id 03fa885 Replace function calls c4d79ab Java string preprocessing: use provided source location fb0c552 Java string preprocessing: use and document parameter function_id c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type 2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2 8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest 30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h 8c8801c List source files in goto-programs/Makefile in lexicographic order 40d28ae replace_symbolt: report replacements in code_typet::return_type 4b9df3b Revert "Ignore return value" e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe 424ab4f --stop-on-fail now stops on failed path 545bff8 Add clear() to path exploration worklist 95d8d0f Generalise option setting from strategy unit tests e85fb77 Cleanup constant_propagator_domaint::valuest 18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests 30d557a Constant propagation: Check type consistency before adding to replacement map a5ce621 Make unit tests quiet 61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names 7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm 3785941 Remove names of unused parameters af79cb9 add support for Visual Studio style inline assembler 254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix 26009a3 remove_asm now guarantees that functions called exist 9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue e247a29 CodeBuild: Remove empty artifact stanza 756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang 355fbd2 avoid assert() 6178908 bump goto binary version f93deec type symbols now use ID_symbol_type 22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation 5c06786 set mode for functions added by remove_asm ef53b65 Update description of regression test framework 312ca1d Add section to documentation about running tests d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location 119e88b Pass location around for nondet initialization 50660db Specify source location for nondet expressions d1f2ad9 Replace -> with → e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments 519370d State that identifiers should be good 30d29b9 Replace unicode arrows → with ascii ones -> 611374f Document classes and member variables unless obvious adb7ef0 Minor fixes to documentation outline fd4f563 Add side_effect_exprt constructor with location 98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions 6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide 61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes c0bcce7 use clang as native compiler for goto-clang 1f19e23 goto-cc: use result of our native compiler detection d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags f94d5e2 follow union, struct and enum tags 99e33bd fix typo in comments for struct_tag_typet 1f53246 expose remove_preconditions f212505 Avoids using expr.op0 when type is known 7b36ca2 Moves is_lvalue to expr_util.c 4782b48 Fix invariant regression tests efb1c40 Refactor invariant_failedt definition. 515f050 Pass the condition to the invariant_failedt constructor. bf6dd9e Added extra use-case hints to the already present invariant definitions. 612b4f8 Address review comments 7233f92 Rearrange everything into separate pages 1cb3cdd Move other tools into a separate file 82eefb7 Fix links between files d9e690b Move folder walkthrough to a separate file 2939db4 Address review comments 8d5cbcb Create CBMC developer guide documentation git-subtree-dir: cbmc git-subtree-split: 4f5e148
Currently this is an outline - over time the various sections should
be filled in. I have moved some of the existing documentation into it
in the appropriate place.