First draft of background concepts section. #2806
Conversation
johanneskloos
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
|
||
| TODO: Explain that this means going from a more high-level | ||
| representation to a more low-level representation, with the goal of | ||
| enabling a different set of transformations, analyses or optimisations. |
There was a problem hiding this comment.
Optimizations (CODING_STANDARD.md mandates American English)
| declarations of `atoi` and `printf`, and the function definitions of | ||
| `factorial` and `main`). Let us start considering the specification of | ||
| `atoi`. This gives rise to a subtree modelling that we have a function | ||
| `atoi` with return type `int` and unnamed argument of type `const char `. |
There was a problem hiding this comment.
Unless that's GitHub acting up: * missing after "const char"
| derive simple information such as ''which functions are being defined?'', | ||
| ''what are the arguments to a given function'' and so on. | ||
|
|
||
| Nevertheless, for serious analysis, this representation needs to be |
There was a problem hiding this comment.
"serious" is dismissive - a lot of useful analysis can be done at syntax level.
| reason for this transformation is that interpreting a structured | ||
| program, as described by an AST, requires us to keep track of all the | ||
| blocks that we have entered so far, requiring us to do bookkeeping | ||
| whenever we enter or leave a block. |
There was a problem hiding this comment.
I disagree with this introduction. All the above steps are purely syntactic. The CFG is the first step that actually interprets the semantics of instructions. As such it isn't necessarily more (or less) low-level.
|
|
||
| A control flow graph, in contrast, reduces the amount of state we need | ||
| to keep; the cost we pay is that we lose the hierarchy imposed by the | ||
| structured programming constructs. |
There was a problem hiding this comment.
Really, it depends on what you want to analyse. Some analysis can be very costly when done on a CFG, while trivial on an AST.
| executes, right at the start. The conditional of the second basic block | ||
| is executed several times, so it cannot be part of the first basic | ||
| block. It cannot be part of the other basic blocks | ||
| loop body, there is a branch right after it (meaning that no other |
There was a problem hiding this comment.
Text needs reviewing here
There was a problem hiding this comment.
This sentence is a bit garbled.
There was a problem hiding this comment.
Can you use more specific references than 'other block'?
| } | ||
| \enddot | ||
| Depending on which path the execution takes, we have to return either | ||
| `x.1` or `x.2`! The default solution is to provide a ''magic'' function |
There was a problem hiding this comment.
Please reword. This is what Rosen, Wegman, Zadeck published in 1988. It's neither a "default" nor is magic involved.
| In CBMC, we use a slightly different solution. For each branch, we keep | ||
| track of which side of the branch was taken, and implement Φ using | ||
| this information. We also handle loops slightly differently than in the | ||
| default approach; this will be discussed in a later chapter. |
There was a problem hiding this comment.
I'm not sure what the "default" is?
| \author Martin Brain, Peter Schrammel | ||
| \author Martin Brain, Peter Schrammel, Johannes Kloos | ||
|
|
||
| TODO intro |
|
|
||
| \section representations_section Representations | ||
|
|
||
| \subsection AST_section AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables | ||
| One of the first questions we should be considering is how we represent programs | ||
| in such a way that we can easily analyze and reason about programs. |
There was a problem hiding this comment.
maybe: 'about them' or 'about their behaviour'?
| abstraction. These representations are designed in such a way that for | ||
| each analysis we want to perform, there is an appropriate | ||
| representation, and it is easy to go from representations that are | ||
| closed to the source code to representations that are better for deep |
| places where CBMC does things differently, attempting to give rationales | ||
| wherever possible. | ||
|
|
||
| More in-depth information can be found in ... |
| result of parsing the program in memory. | ||
|
|
||
| The key data structure that stores the result of this step is known as an | ||
| **Abstract Syntax Tree**, or **AST** for short. They are still relatively |
| ``` | ||
|
|
||
| This function | ||
| consists of four basic blocks: |
There was a problem hiding this comment.
Not sure the basic block discussion is required to understand CFGs. In the analyses that run on GOTO programs basic blocks have little significance.
There was a problem hiding this comment.
For example, we do do abstract interpretation by statement, not by basic block. The statements still form a cfg though.
There was a problem hiding this comment.
Not sure how things are done in CBMC, but at least the instrumentations I am using are usually done at the basic block level. I think they should be discussed somewhere, but I don't mind moving that part of the discussion elsewhere.
There was a problem hiding this comment.
When reading this proposed documentation I largely tried to ignore CBMC specifics, and I think @johanneskloos has done a good job of providing a general introduction to the topic. CFGs are fundamentally defined around basic blocks, so I thought this was fine. (As was not using CBMC's way of naming symbols and doing SSA indexing.) But I'm happy to stand corrected and would thus re-review with an adjusted mindset.
There was a problem hiding this comment.
I concur with @tautschnig - I tried to be somewhat technology-agnostic, while not straying from the way CBMC does things too much.
There was a problem hiding this comment.
Fully agreed with this part being language-agnostic. I'm just noting this to avoid confusing the reader with concepts that seem important and then it turns out that they actually "optional". A clarifying comment would be fine.
There was a problem hiding this comment.
Rewrote the introduction section about basic blocks: I now state that one may treat each instruction as basic block (as CBMC) does.
| `for` loop of `factorial` is transformed. We currently have: | ||
|
|
||
| ``` | ||
| expression: fac.1 *= i.1 |
There was a problem hiding this comment.
Maybe use the appropriate @#$ suffixes used by ssa_exprt
There was a problem hiding this comment.
Where can I find documentation on this?
There was a problem hiding this comment.
Ooh, I remember making a PR to add the documentation. https://github.com/diffblue/cbmc/pull/886/files
There was a problem hiding this comment.
Hm, this carries quite a bit of additional information - should we really introduce all of this here? Especially since this seems a bit like an implementation detail.
| } | ||
| \enddot | ||
|
|
||
| TODO: Point to some good discussion of SSA |
|
|
||
| \subsection Trace_section Trace | ||
|
|
||
| TODO: I am not quite sure what is supposed to go here. |
There was a problem hiding this comment.
I think this was intended to describe how a (counterexample) trace is represented.
There was a problem hiding this comment.
I think this section should become a subsection of Bounded Model Checking (below). It's relative to a technique, it's not a standard program representation. What to put here will be easier to find once you have described BMC.
|
|
||
| \section analysis_techniques_section Analysis techniques | ||
|
|
||
| \subsection BMC_section Bounded model checking | ||
|
|
||
| To be documented (can copy from the CBMC manual). | ||
|
|
||
| TODO: There seems to be no sufficiently comprehensive section in the |
| } | ||
| \enddot | ||
|
|
||
| In the end, we produce a sequence of graphs modeling each declaration |
There was a problem hiding this comment.
Graphs -> Trees. Trees are graphs of course, but we're still at AST level so we should stick with one term.
| ``` | ||
|
|
||
| This function | ||
| consists of four basic blocks: |
There was a problem hiding this comment.
For example, we do do abstract interpretation by statement, not by basic block. The statements still form a cfg though.
|
|
||
| In CBMC, we use a slightly different solution. For each branch, we keep | ||
| track of which side of the branch was taken, and implement Φ using | ||
| this information. There are also some differences in how loops are |
There was a problem hiding this comment.
Is this actually a different solution in practice then? I think all that you're saying here is that there's no explicit Φ expression here right?
There was a problem hiding this comment.
Just commenting on the CBMC angle: there is an explicit Φ node added during goto-symex, it's just a precise variant thereof. See goto_symext::phi_function.
| formulas and, essentially, running the program on sets of concrete | ||
| states, another approach to learn about a program is based on the idea | ||
| of interpreting an abstract version of the program. This is known | ||
| as **static analysis**, or, more precisely, **abstract interpretation**. |
There was a problem hiding this comment.
This makes it sound as if "static analysis" means "abstract interpretation", but in a sort of ambiguous and nebulous way. I think something like "This is known as abstract interpretation, a form of static analysis" would be more in line with what's intended here?
| \author Martin Brain, Peter Schrammel, Johannes Kloos | ||
|
|
||
| The purpose of this section is to explain several key concepts used throughout | ||
| CBMC on a high level, ignoring the details of the actual implementation. |
There was a problem hiding this comment.
CBMC -> the CPROVER framework.
The same comment applies elsewhere in your PR. Even though the Git repo is named 'cbmc', the contents of the repo correspond to the CPROVER framework, and this documentation is part of the CPROVER developer manual ;)
| close to the source code to representations that focus on specific | ||
| semantic aspects of the program. | ||
|
|
||
| The representations that CBMC uses mirror commonly-used representations |
There was a problem hiding this comment.
Double use of "use". Perhaps "representations employed in CPROVER mirror..." ?
| #TODO: Find a good online compiler construction course and reference | ||
| #here. | ||
| # TODO: There doesn't seem to be a good online course that covers | ||
| # all of these topics in one go. Maybe buy the Dragon Book? |
There was a problem hiding this comment.
To be fixed before you merge
|
|
||
| The first step in representing a program in memory is to parse the | ||
| program, at the same time checking for syntax errors, and store the | ||
| result of parsing the program in memory. |
There was a problem hiding this comment.
"result of parsing the program in memory" --> "parsing result in memory"
| result of parsing the program in memory. | ||
|
|
||
| The key data structure that stores the result of this step is known as an | ||
| **Abstract Syntax Tree**, or **AST** for short. ASTs are still relatively |
There was a problem hiding this comment.
AST --> link to wikipedia? https://en.wikipedia.org/wiki/Abstract_syntax_tree
| using such abstract values. Coming back to our running example, we wish | ||
| to prove that the factorial function never returns 0. | ||
|
|
||
| The first ingredient we need for abstract interpretation is the |
There was a problem hiding this comment.
For clarity, I would list here all the ingredients you will need:
- An abstract domain, abstracting away details in the data
- A transformer per statement
- A map associating pairs (location, variable) to values of the abstract domain
- An algorithm to compute the fixed point.
| - bottom is bottom, obviously. | ||
| It is easy but tedious to check that all conditions hold. | ||
|
|
||
| The domain allows us to express what we know about a given variable or |
There was a problem hiding this comment.
First intuition, then formalization.
Put this paragraph first. Use it to justify why you need the merge operator in the formalization. Then present the lattice.
| It is easy but tedious to check that all conditions hold. | ||
|
|
||
| The domain allows us to express what we know about a given variable or | ||
| value; in our example, whether it is zero or not. |
There was a problem hiding this comment.
about a given variable or value -> add at a given location.
|
|
||
| For instance, consider the `factorial` example again. After running the | ||
| first basic block, we know that `fac` and `i` both contain 1, so we have | ||
| a map to maps both `fac` and `i` to "not 0". |
There was a problem hiding this comment.
to maps --> that associates
| states, another approach to learn about a program is based on the idea | ||
| of interpreting an abstract version of the program. This is known | ||
| as **abstract interpretation**. Abstract interpretation is one of the | ||
| main methods in the area of **static analysis**. |
There was a problem hiding this comment.
| is achieved by executing the instrumented code or by just analyzing it in some | ||
| other way. | ||
|
|
||
| # Flattening and Lowering |
There was a problem hiding this comment.
Can we turn this (and probably others) into a doxygen \subsection so it can be referenced from else where
peterschrammel
assigned johanneskloos and unassigned johanneskloos, danpoe and hannes-steffenhagen-diffblue
To be replaced by diffblue#2806
|
Let's don't forget to introduce a link from https://github.com/diffblue/cbmc/pull/2792/files#diff-9c1ded90972faa6bdc815b782038ead3R14 to the corresponding section in this PR. |
|
There is still one big TODO in the BMC section. I would like to deal with this in the next documentation day, since I believe it warrants spending some more time on this. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 63347d5).
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).
|
|
||
| \section representations_section Representations | ||
|
|
||
| \subsection AST_section AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables | ||
| One of the first questions we should be considering is how we represent programs | ||
| in such a way that we can easily analyze and reason them. |
| (cf. [Wikipedia](https://en.wikipedia.org/wiki/Abstract_syntax_tree)). | ||
| ASTs are still relatively | ||
| close to the source code, and represent the structure of the source code | ||
| while abstracting away from irrelevant details, e.g., dropping |
There was a problem hiding this comment.
Don't use the term "irrelevant". You don't know what the reader may or may not consider relevant.
| grouping. | ||
|
|
||
| Considering the example of the C program given above, we first notice | ||
| that the program describes (in C terms) a single *compilation unit*, |
There was a problem hiding this comment.
I'm not sure what @cesaro meant to say, but afaik the correct term is "translation unit".
| the parameter list for each parameter, giving its type and name, if a | ||
| name is given. | ||
|
|
||
| More interestingly, we can represent the structure of the `factorial` |
There was a problem hiding this comment.
Don't presuppose what the reader may or may not find interesting.
|
|
||
| More interestingly, we can represent the structure of the `factorial` | ||
| function using ASTs. The idea here is that the code itself has a | ||
| hierarchical structure. In the case of C, this start with the block |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 1103480).
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).
|
|
||
| To instrument a piece of code means to modify it by (usually) inserting new | ||
| fragments of code that, when executed, tell us something useful about the code | ||
| being instrumented. |
There was a problem hiding this comment.
the code [that has] been instrumented.
|
|
||
| \subsection static_analysis_section Static analysis | ||
|
|
||
| To be documented. | ||
| While BMC analyses the program by transforming everything to logic |
|
|
||
| In the CPROVER framework, the term **verification condition** is used | ||
| in a somewhat non-standard way. Let a program and a set of assertions | ||
| be given. We transform the program into an SSA and turn it into a |
There was a problem hiding this comment.
(acyclic) SSA -- otherwise 'after' is not correct in the presence of loops.
|
Please squash the commits. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: a2b4c45).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84028057
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).
|
@cesaro Any further comments? |
|
Fine with me. |
|
I'm halfway through a review. |
| \author Martin Brain, Peter Schrammel, Johannes Kloos | ||
|
|
||
| The purpose of this section is to explain several key concepts used throughout | ||
| the CPROVER framework on a high level, ignoring the details of the actual implementation. |
There was a problem hiding this comment.
"on a high level" -> "at a high level"
| rationales wherever possible. | ||
|
|
||
| One in-depth resource for most of this section is the classic | ||
| (compiler construction text book)[https://en.wikipedia.org/wiki/Compilers:_Principles,_Techniques,_and_Tools] |
There was a problem hiding this comment.
It seems odd to me that you don't name the book, either by its official name or as the dragon book
| local declaration (similar to the global declarations above) of a | ||
| variable. | ||
|
|
||
| \dot "AST for unsigned long fac = 1" |
There was a problem hiding this comment.
Maybe use backticks around unsigned long fac = 1? You do it in other places like this.
| following structure (this is a simplified version of the tree that the CPROVER framework | ||
| uses internally): | ||
|
|
||
| \dot "AST for the atoi declaration" |
There was a problem hiding this comment.
Maybe use backticks around atoi? You do it in other places like this.
| important property: They must reflect the actual behavior of the | ||
| underlying program instructions. There is a formal description of this | ||
| property, using *Galois connections*; for the details, it is best to | ||
| look at the literature. |
There was a problem hiding this comment.
Link to https://en.wikipedia.org/wiki/Galois_connection (or another site if you prefer)
| } | ||
| \enddot | ||
|
|
||
| We provide an initial variable map: n is "could be 0" before BB1. |
There was a problem hiding this comment.
Put backticks around variable names from here to the end of the section
| that f(x) = x). | ||
|
|
||
| This overview only describes the most basic way of performing abstract | ||
| interpretation. For one, it only works on the procedure level (we speak of |
There was a problem hiding this comment.
"we speak of" -> "we say it is an" (I think this is clearer)
| what line is being visited. Finally we execute the instrumented version of | ||
| `aha` and collect the desired information from the log. | ||
|
|
||
| More generally speaking, and specially within the CPROVER code base, |
There was a problem hiding this comment.
"specially" -> "especially"
|
|
||
| One in-depth resource for most of this section is the classic | ||
| (compiler construction text book)[https://en.wikipedia.org/wiki/Compilers:_Principles,_Techniques,_and_Tools] | ||
| by Aho, Lam, Sethi and Ullman. |
There was a problem hiding this comment.
The link is not being rendered properly:
There was a problem hiding this comment.
The square brackets and the round brackets are the wrong way around
| condrhs [label="Expression: Variable n",shape=rectangle] | ||
| inc [label="Code\nExpression: ++ - postfix",shape=rectangle] | ||
| incarg [label="Expression: Variable i",shape=rectangle] | ||
| body [label="Code\nStatement: Block"] |
There was a problem hiding this comment.
Same comment as above. SHould the Statement: Block node be a rectancle like the others?
| All in all, the AST for the function body looks like this: | ||
|
|
||
| \dot "AST for the body of `factorial`" | ||
| digraph ast { |
There was a problem hiding this comment.
Same coment in this digraph about the two rounded nodes below:
| basic block, take one of the available outgoing edges to another basic block. | ||
| This makes this representation a prime candidate to implement a number | ||
| of static analyses, as described in sections @ref analyses-frameworks | ||
| and @ref analyses-specific-analyses. |
There was a problem hiding this comment.
@johanneskloos This has not been addressed. I propose to insert a new section exactly here on Intermediate Representations, with a FIXME and a list of items describing the contents that you think should be described.
|
|
||
| ''(*x* or *y*) and (*x* or not *y*) and *x* and *y*'' | ||
|
|
||
| We can represent this formula in the minisat input format as: |
There was a problem hiding this comment.
minisat input format -> DIMACS format (all modern solvers, including minisat, read this format). Give a link to e.g. these slides (using archive.org): https://www.cs.upc.edu/~erodri/webpage/cps/lab/sat/tutorial-sat-solvers-slides/slides.pdf
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 3e240b1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84417981
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).
| the current position to right after that instruction. At the end of a | ||
| basic block, take one of the available outgoing edges to another basic block. | ||
|
|
||
| In the CPROVER framework, we often not construct CFGs explicitly, but instead |
There was a problem hiding this comment.
"we often not construct" -> "we often do not construct"
| basic block, take one of the available outgoing edges to another basic block. | ||
|
|
||
| In the CPROVER framework, we often not construct CFGs explicitly, but instead | ||
| use an IR that is structed in a way very similar to CFGs, known as |
There was a problem hiding this comment.
"structed" -> "constructed"
| that f(x) = x). | ||
|
|
||
| This overview only describes the most basic way of performing abstract | ||
| interpretation. For one, it only works on the procedure level (we sat it is an |
There was a problem hiding this comment.
"we sat" -> "we say"
|
I believe all the remaining comments are now addressed. If there are no more remarks, I will squash the commits and ask for a merge. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 1a5ff93).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85590257
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).
|
I believe this PR is ready for merging. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 0fda003).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85710107
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).
This is a first, incomplete version of the background material section, as described in Jira ticket DOC-8 (cf. .
It adds documentation for the following:
Still missing are:
I have added stubs for the corresponding sections.
An additional pain point is that the formatting of inline GraphViz graphs by Doxygen is quite bad, often cutting of labels and making the bounding boxes to small. This will need to be fixed for a later version.
Since this PR only changes documentation, I will cancel the corresponding Travis run.