Docs for incremental SMT backed

[esteffin]

Add documentation for the new incremental SMT backend.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

I'm not convinced the "CPROVER Manual" (rendered at https://www.cprover.org/cprover-manual/) is the right place for this: the level of abstraction of other information presented in there is quite a bit higher, and I am opposed to putting work-in-progress stuff in there. I think the CBMC man page is a good candidate, or else just a README.md file in the source directory.

[codecov]

Codecov Report

Merging #7005 (2610713) into develop (4d5d529) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #7005   +/-   ##
========================================
  Coverage    77.85%   77.85%           
========================================
  Files         1569     1569           
  Lines       180656   180656           
========================================
  Hits        140648   140648           
  Misses       40008    40008           

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 22fec4c...2610713. Read the comment docs.

[NlightNFotis]

Hi @tautschnig I don't believe the man page is the appropriate location for the sort of information we want to add (we can add things to the man page for sure, but I think that's orthogonal to the information we have here).

This is supposed to be the documentation that we have for final users of the new SMT backend. The decision for putting it there was made on the rationale that a user would look for supporting information on the tool's manual, which is represented by that directory.

Indeed, that directory also contains other files that have a mix of user documentation/architectural stuff, such as goto-cc.md and visual-studio.md. Now, of course, an argument could be made that we don't want to add more documents like that in that folder.

However, in that case, guidance should be given on where pieces of documentation like the one that we are adding now should go, given that the other folders under doc/ seem less appropriate for this piece of documentation (say, ADR/ which is for Architectural Decision Records, not user documentation, or architectural/ which is describing CBMC internals). It seems that the only other appropriate place is a new folder, which doesn't seem ideal.

[NlightNFotis]

We should mention that we support C integers via bit-vector arithmetic (bit-vectors are not a C level construct AFAIK)

[esteffin]

changed

[NlightNFotis]

We can remove the word requirement, or phrase it like:

Usage of the incremental SMT backend requires a SMT solver compatible with SMTlib v2.6 formatted input

[esteffin]

changed

[NlightNFotis]

I would phrase this as

Examples of invocations with various solvers

[esteffin]

changed

[NlightNFotis]

I believe this information is inaccurate - we do build an SMT2 solver with CBMC (you can find regression tests for that under regression/smt2_solver and the binary under <build>/bin/smt2_solver) but we are not targeting that as it's very primitive and its current level of SMTlib support is unknown.

I suggest we rephrase that as

The new incremental SMT backend has been designed to interoperate with external solvers

[esteffin]

changed

[NlightNFotis]

I would phrase that as

Due to lack of support for conversion of array_of expressions that are generated by CBMC in the new SMT backend, we currently have to supply an extra argument --slice-formula so that instances of arrayof_exprt are removed from the formula to be converted.

As we move forward with our array-support implementation, we anticipate that the need for this extra flag will be diminished.

[esteffin]

changed

[NlightNFotis]

We should probably refer to them as "major features" or just "features", not primitives, IMO.

[esteffin]

changed

[tautschnig]

Warning: I may end up hijacking this PR to discuss plans for documentation.

Hi @tautschnig I don't believe the man page is the appropriate location for the sort of information we want to add (we can add things to the man page for sure, but I think that's orthogonal to the information we have here).

I'm not sure why it is "orthogonal," but more on that below.

This is supposed to be the documentation that we have for final users of the new SMT backend. The decision for putting it there was made on the rationale that a user would look for supporting information on the tool's manual, which is represented by that directory.

Well, the man page is a place for "final users." The current CPROVER manual (i.e., any files under doc/cprover-manual) barely mentions SAT or SMT solvers, or indeed anything about solving back-ends. It's just not that level of abstraction that's being covered in here. So if we don't currently tell users about the back-end, we can't suddenly introduce a new chapter that specifically talks about one particular back-end.

The man page, however, could be a place to document all command-line options (indeed my various recent PRs are an effort to ensure this is the case). The exception shall be options that we intentionally exclude from any kind of documentation (including --help output). That said, the man pages still are in need of love, and a lot more text is yet to be written. Only very few of them are in a shape that perhaps I'd like them to be in (#6938 is somewhat close to that, as is the goto-analyzer man page that's already merged).

My opinion (and I do by no means claim to be authoritative on this, just my own thoughts):

1. Users new to verification start with https://model-checking.github.io/cbmc-training/ (or perhaps https://www.cprover.org/cprover-manual/).
2. If you know what verification is about, but you better want to understand the workflow, https://model-checking.github.io/cbmc-training/ and https://www.cprover.org/cprover-manual/ remain the place to look for information.
3. If you know what tools you need to use, but need to understand all the options available with each tool, look at each tool's man page. (This is no longer an overview across tools, it's now very specific to a single tool.)
4. If you want to contribute to the development or understand some internals, go to http://cprover.diffblue.com/.

Indeed, that directory also contains other files that have a mix of user documentation/architectural stuff, such as goto-cc.md and visual-studio.md. Now, of course, an argument could be made that we don't want to add more documents like that in that folder.

I don't see the above examples as "architectural stuff" (or at least not in the way that I'd understand that phrase). If there is more cleanup in doc/cprover-manual to be done, then let's go for it. Let's please not clutter it any further, just because we think it's a mess already.

However, in that case, guidance should be given on where pieces of documentation like the one that we are adding now should go, given that the other folders under doc/ seem less appropriate for this piece of documentation (say, ADR/ which is for Architectural Decision Records, not user documentation, or architectural/ which is describing CBMC internals). It seems that the only other appropriate place is a new folder, which doesn't seem ideal.

I don't want us to start the discussion from where in the source tree a piece of documentation will go. I expect that discussion to start from the potential consumer of such documentation. When that is determined, we can find a suitable place in the source tree. If the audience (as I think is the case here) is a CBMC user (as opposed to a contributor/developer), then it needs to fit with the level of abstraction that is covered by a particular (collection of) document(s). If there is no so suitable collection, then perhaps we need to create a new one. But I want to make sure we don't just end up dumping text in the repository: we have a lot of documentation across the code base, but largely lack consistency. And we should aim to improve on this, not make it even worse just so that we can tick some "documentation" checkbox.

[NlightNFotis]

Hello @tautschnig, thank you for taking the time to share your thoughts.

I'm in agreement with a lot of what's written there, and I share the feeling that the CBMC documentation situation is unsatisfactory, and merits a lengthier conversation and plan to move it to a better place.

We also want to get this PR moving though (to get some user documentation about the new SMT backend so that you guys can start playing with it), so I propose the following two actions for now:

1. Could you please open an RFC issue re documentation and copy your post there? It contains a lot of useful information and thoughts that are to shape any future conversation and I wouldn't want it to be lost when this PR gets merged, nor does it seem great to hold up this PR to not lose that comment.
2. Would us moving the information here to the CBMC man page be an adequate solution for now, until we decide on a place/structure to host future documentation efforts?

Let me know your thoughts, and thanks again for starting this conversation.

[tautschnig]

1. Could you please open an RFC issue re documentation and copy your post there? It contains a lot of useful information and thoughts that are to shape any future conversation and I wouldn't want it to be lost when this PR gets merged, nor does it seem great to hold up this PR to not lose that comment.

Done: #7006

2. Would us moving the information here to the CBMC `man` page be an adequate solution for now, until we decide on a place/structure to host future documentation efforts?

In my opinion, yes, it would be a great fit. Feel free to use the existing man page to get this PR merged ASAP, and I'll rebase #6937 on top of it.

[tautschnig]

Left-over?

[tautschnig]

s/supoorted/supported/

[tautschnig]

Can safely be removed.

[tautschnig]

This would also be valuable information to copy into the man page.

[tautschnig]

Would also be nice to see in the man page.