Tools overview #5792

TGWDB · 2021-01-29T15:40:36Z

[V ] 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.

codecov · 2021-01-29T16:17:17Z

Codecov Report

Merging #5792 (f7d1023) into develop (4cc9611) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5792   +/-   ##
========================================
  Coverage    69.54%   69.54%           
========================================
  Files         1243     1243           
  Lines       100701   100701           
========================================
  Hits         70037    70037           
  Misses       30664    30664

Flag	Coverage Δ
cproversmt2	`43.32% <ø> (ø)`
regression	`66.44% <ø> (ø)`
unit	`32.25% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out more.

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 4cc9611...f7d1023. Read the comment docs.

martin-cs

Basically yes but there are a few more bits and links that might be useful.

martin-cs · 2021-01-29T21:31:21Z

TOOLS_OVERVIEW.md

+- [others (converter, driver, file_converter, java-converter)](#others)
+
+The rest of this document provides a section on each of these tools in alphabetical order.
+Most links in this document are to the [CProver online documentation](http://cprover.diffblue.com/index.html).


I'm not quite sure how linking is done in the rest of the documentation but if there is an option to have these as local / relative links that would be great.

We should definitely use relative links.

There is no consistent way of linking.

I was working on another (draft, so very provisional) pull request (see #5781) and it was recommended to use links to the online documentation at diffblue.com.

Exact quote is:

README.md references http://cprover.diffblue.com/, so I'd go with that in top-level files (README.md, COMPILING.md, CODING_STANDARD.md, and possibly any files to be added at that level).

So should I document with:
A. Links to the local documentation path (e.g. doc/html/index.html)
B. Links to the absolute location (e.g. http://cprover.diffblue.com/index.html)
C. Something else? (E.g. relative html links, although these will not work when .md files are used like this one?)

I think the confusion is that the top-level .md files are currently not compiled into cprover.diffblue.com, but only those in doc and the README.md files in the source directories.

My rationale was that this is a top level .md file (similar to README.md) and so we should link to the diffblue.com URLs. Since this is not going to be compiled into the website, then I understand the current linking is correct?

The above said, if we wish to move this document to another location (or have another reason to change), let me know and I can redo the links as relative.

martin-cs · 2021-01-29T21:53:08Z

TOOLS_OVERVIEW.md

+
+## goto-analyzer
+
+This provides a way to access and invoke various forms of analysis on


It's a bit more detailed and restricted than that. goto-analyzer is a wrapper around the abstract interpretation ( http://cprover.diffblue.com/background-concepts.html#abstract_interpretation_section ) implementation ( well, implementations, see http://cprover.diffblue.com/group__analyses.html ) in CPROVER. It allows you to configure what abstractions are used and what is then done with them (verification, display, simplification, etc.). At the moment the best documentation is here : http://cprover.diffblue.com/goto__analyzer__parse__options_8h.html but I have writing a section for the manual on my TODO list.

Incorporated these comments into an updated version (some text taken almost directly).

Let me know if you want to coordinate on writing the section for the manual (I'd love to learn more about this, and help write the section if I can).

martin-cs · 2021-01-29T21:55:48Z

TOOLS_OVERVIEW.md

+## goto-cc
+
+This is a compiler that also adds goto program information to the compiled
+programs. Note that `goto-cc` is the compiler and linker while `goto-gcc` and


goto-cc is intended as a drop-in replacement for gcc so that you can re-use the same build infrastructure. The key difference is that it builds goto-modelts instead of executables ( somewhere @tautschnig had a patch to build both but it is not the default ). Really important is that depending on the same of the binary, you get emulation of different compilers, such as the Visual Studio one and the CodeWarrior one.

Pushed a rewrite that I hope reflects this.

martin-cs · 2021-01-29T21:56:28Z

TOOLS_OVERVIEW.md

+Provides a variety of difference checks between two goto programs (produced
+by `goto-cc`). This invokes some of the cbmc tools to convert the goto
+program and then determine which functions are added/removed/changed.
+


@peterschrammel ?

Essentially a diff tool for goto-programs.

Updated the text for this (and also jdiff).

martin-cs · 2021-01-29T21:58:24Z

TOOLS_OVERVIEW.md

+## janalyzer
+
+This provides a way to access and invoke various forms of analysis on
+Java programs.


Yes; janalyzer is a fork of goto-analyzer with the JVM front-end added.

Updated the text for this.

martin-cs · 2021-01-29T21:59:36Z

TOOLS_OVERVIEW.md

+
+This is the main analysis engine the performs the analysis
+of Java files using bounded model checking. This is a
+Java version of the `cbmc` tool (more documentation for


Pedantry perhaps but to me a "java version" implies it is written in Java. The point is that jbmc is an old fork of cbmc with the JVM front-end added.

Yes, it's a BMC tool for Java bytecode (similar to cbmc being a BMC tool for C).
It has been separated from CBMC in order to support separate compilation of C and Java frontends and tools. Also, JBMC's command line follows conventions of java so that programs can be analysed in the same way you would run them using the java executable. There also lots of additional options to support nondeterministic initialisation of variable size arrays, data structures and strings, control how to assert on exceptions etc.

Updated text for this (and added some clear phrases from Peter).

martin-cs · 2021-01-29T22:00:29Z

TOOLS_OVERVIEW.md

+Provides a variety of difference checks between two goto programs (produced
+by `goto-cc`). This invokes some of the `cbmc` tools to convert the goto
+program and then determine which functions are added/removed/changed.
+


Likewise, I believe (@peterschrammel ?) that jdiff is goto-diff forked and the JVM front-end added.

Yes, just a clone of goto-diff for use on Java bytecode input.

Updated text (and also on goto-diff)

martin-cs · 2021-01-29T22:01:50Z

TOOLS_OVERVIEW.md

+## memory-analyzer
+
+This is a wrapper program that provides a front end to `gdb` that adds some
+useful features related to the other goto utilities. Note that to use


It's a bit more than that. memory-analyzer allows you to run an compiled binary, using gdb and when you are at the right point, it will build a harness that allows you to analyze the program /from that state/.

Added text on this, hope it is clear(er) now.

martin-cs · 2021-01-29T22:02:42Z

TOOLS_OVERVIEW.md

+
+This is an (Satisfiability Modulo Theory) SMT solver that is shipped
+with CProver. The SMT solver here is built on top of a Satisfiability
+(SAT) solver. The `smt2_solver` is designer to work with files, and


It is basically an SMT interface to the CPROVER back-end prover.

@martin-cs Can you please clarify whether you are proposing a change to the text (and if so perhaps propose some new text), or whether you were making a comment to help us understand?

I think more of the later but let's try the former too...

smt2_solver is an SMT (Satisfiability Modulo Theory) solver. It parses SMT-LIB 2 format and uses CPROVER's internal bit-blasting solver (see solvers/) to resolve queries.

peterschrammel · 2021-01-30T14:46:43Z

TOOLS_OVERVIEW.md

+- [others (converter, driver, file_converter, java-converter)](#others)
+
+The rest of this document provides a section on each of these tools in alphabetical order.
+Most links in this document are to the [CProver online documentation](http://cprover.diffblue.com/index.html).


We should definitely use relative links.

peterschrammel · 2021-01-30T15:00:24Z

TOOLS_OVERVIEW.md

+
+This is the main analysis engine the performs the analysis
+of Java files using bounded model checking. This is a
+Java version of the `cbmc` tool (more documentation for


Yes, it's a BMC tool for Java bytecode (similar to cbmc being a BMC tool for C).
It has been separated from CBMC in order to support separate compilation of C and Java frontends and tools. Also, JBMC's command line follows conventions of java so that programs can be analysed in the same way you would run them using the java executable. There also lots of additional options to support nondeterministic initialisation of variable size arrays, data structures and strings, control how to assert on exceptions etc.

peterschrammel · 2021-01-30T15:01:09Z

TOOLS_OVERVIEW.md

+Provides a variety of difference checks between two goto programs (produced
+by `goto-cc`). This invokes some of the `cbmc` tools to convert the goto
+program and then determine which functions are added/removed/changed.
+


Yes, just a clone of goto-diff for use on Java bytecode input.

peterschrammel · 2021-01-30T15:01:34Z

TOOLS_OVERVIEW.md

+Provides a variety of difference checks between two goto programs (produced
+by `goto-cc`). This invokes some of the cbmc tools to convert the goto
+program and then determine which functions are added/removed/changed.
+


Essentially a diff tool for goto-programs.

peterschrammel · 2021-01-30T15:02:24Z

TOOLS_OVERVIEW.md

+janalyzer --help
+```
+
+## java-unit


Not really an executable for users, but developers.

peterschrammel · 2021-01-30T15:03:10Z

TOOLS_OVERVIEW.md

+
+## symtab2gb
+
+This utility is to compile a cbmc symbols table (in JSON format) into a goto binary.


This is used to integrate external language frontends, e.g. https://github.com/diffblue/gnat2goto/

peterschrammel · 2021-01-30T15:03:29Z

TOOLS_OVERVIEW.md

+```
+
+
+## unit


Things below are for developers.

Added developer utilities section and listed the developer tools there.

tautschnig

Thank you for adding all this documentation! One overall comment: would be be worth merging the sections janalyzer/goto-analyzer, jdiff/goto-diff, jbmc/cbmc, java-unit/unit?

tautschnig · 2021-02-01T10:10:47Z

TOOLS_OVERVIEW.md

+- [Developer Utilities](#developer-utilities)
+    - [java-unit](#java-unit)
+    - [unit](#unit)
+    - [others (converter, driver, file_converter, java-converter)](#others)


This is great, and makes me wonder whether this should be linked (or included in?) the top-level README file so that people accessing the repository see it right away?

Added link in README.md

tautschnig · 2021-02-01T10:17:21Z

TOOLS_OVERVIEW.md

+in addition to the normal compiled program). Note that `goto-cc` is the
+compiler and linker while `goto-gcc` and `goto-ld` are symbolic links to
+`goto-cc`. The additional object code is used as the internal representation


I'm not sure the fact that these are symlinks matters the most to a user. Perhaps focus on the resulting behaviour? goto-cc behaves differently, depending on the file name: the command-line options (and ensuing behaviour) are modelled after the program that has the same name as the suffix, i.e., gcc, ld, etc. (we also support cl, link, bcc, as).

This has been updated now to clarify the role of the different files and de-emphasise the symlinks.

tautschnig · 2021-02-01T10:17:53Z

TOOLS_OVERVIEW.md

+Note that `goto-cc` can emulate GCC, Visual Studio, and CodeWarrior
+compilers.


Ah, see my notes about for symlinks.

tautschnig · 2021-02-01T10:18:55Z

TOOLS_OVERVIEW.md

+This invokes some of the cbmc tools to convert the goto
+program and then determine which functions are added/removed/changed.


I don't think that any other tools are being invoked?

tautschnig · 2021-02-01T10:20:17Z

TOOLS_OVERVIEW.md

+## goto-harness
+
+This is a tool for creating a harness around a (part of a) goto program that
+can then be analysed inside the harness. Harnesses can be either function


What does "inside the harness" mean?

tautschnig · 2021-02-01T10:21:52Z

TOOLS_OVERVIEW.md

+### others
+
+These (`converter`, `driver`, `file_converter`, `java-converter`)
+are build time utilities for other tools and not designed
+to be run independently.


I'm not sure these should even be mentioned?

Rationale was to have list of all binaries (built on Linux, so some on other platforms may be missing). Open to removing the section though.

Understood, but I fear this might cause more confusion than doing good. Not a blocker from my point of view, leaving it to you to decide.

This adds the TOOLS_OVERVIEW.md file (and links to it from README.md). The Tools Overview is an overview of all the tools that are part of the CProver package. Each overview includes main points on how to use the tool and what the tool is meant to do. Also further documentation links are provided to better understand the tool.

TGWDB requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners January 29, 2021 15:40

martin-cs approved these changes Jan 29, 2021

View reviewed changes

peterschrammel approved these changes Jan 30, 2021

View reviewed changes

tautschnig approved these changes Feb 1, 2021

View reviewed changes

TGWDB force-pushed the tools-overview branch from 2442e91 to f7d1023 Compare February 5, 2021 09:28

TGWDB merged commit 0dfbd1e into diffblue:develop Feb 5, 2021


		## goto-analyzer

		This provides a way to access and invoke various forms of analysis on


		## symtab2gb

		This utility is to compile a cbmc symbols table (in JSON format) into a goto binary.

		Note that `goto-cc` can emulate GCC, Visual Studio, and CodeWarrior
		compilers.

		This invokes some of the cbmc tools to convert the goto
		program and then determine which functions are added/removed/changed.

		```


		## unit

Tools overview #5792

Tools overview #5792

Uh oh!

Conversation

TGWDB commented Jan 29, 2021

Uh oh!

codecov bot commented Jan 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

TGWDB Feb 1, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

codecov bot commented Jan 29, 2021 •

edited

Loading

TGWDB Feb 1, 2021 •

edited

Loading