Add JBMC user manual [DOC-9] #3404

allredj · 2018-11-13T18:13:55Z

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.
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.

peterschrammel · 2018-11-13T18:17:55Z

doc/cprover-manual/jbmc-user-manual.md

+Now let's run the following command to let JBMC tell us about potential errors
+in our `query` method.
+```
+jbmc Example.class --function core.Example.query


That's a bit strange that you cd first into core and then run jbmc from there. I'd say jbmc core/Example.class ....
Side note: At some point that will actually change to running jbmc core.Example ... (akin to java core.Example).

Is core a good name? What about tutorial or examples?

Actually, about your first comment, I'm not cd-ing into anything. There is no core folder. I compiled the java file using javac, and it's not within a maven project, so the folder hierarchy doesn't follow the packages. Is that confusing? Should I remove the package from the examples?

peterschrammel · 2018-11-13T18:19:05Z

doc/cprover-manual/jbmc-user-manual.md

+
+\subsection jbmc-manual-unwind Loop unwinding
+
+As in CBMC, JBMC transforms the input program into a state representation,


As CBMC, JBMC

peterschrammel · 2018-11-13T18:19:20Z

doc/cprover-manual/jbmc-user-manual.md

+\subsection jbmc-manual-unwind Loop unwinding
+
+As in CBMC, JBMC transforms the input program into a state representation,
+and thus needs to unwind loops up to a given value. Without specifying a


peterschrammel · 2018-11-13T18:21:04Z

doc/cprover-manual/jbmc-user-manual.md

+To limit the number of times the for-loop is unwound, we use the `--unwind N`
+ options, in which case the following call to JBMC:
+```
+jbmc Example.class --function core.Example.isPrime --unwind 10


peterschrammel · 2018-11-13T18:21:13Z

doc/cprover-manual/jbmc-user-manual.md

+To be sure that this always holds, we run JBMC on the example, with a
+reasonable `unwind` value:
+```
+jbmc Example.class --function core.Example.isPrime --unwind 10


peterschrammel · 2018-11-13T18:22:16Z

doc/cprover-manual/jbmc-user-manual.md

+If we make our code more robust by adding guards to make the array access
+safe as follows:
+```java
+5      public static int query(int[] array, int index) {


I suggest to make the examples complete classes with different names so that the user can easily copy paste the code and run.

peterschrammel · 2018-11-13T18:24:45Z

doc/cprover-manual/jbmc-user-manual.md

+```
+[java::core.Example.doSomething:()V.assertion.1] line 8 assertion: FAILURE
+```
+Again, the trace shows the contradicting string:


to be precise "the string violating the condition in the assertion"

peterschrammel · 2018-11-13T18:25:37Z

doc/cprover-manual/jbmc-user-manual.md

+
+JBMC has a wealth of other options that can either constrain the model (to
+cope with complexity issues), or output more relevant information. The list
+of all available options are printed by typing:


peterschrammel · 2018-11-13T18:28:54Z

doc/cprover-manual/jbmc-user-manual.md

+
+To remove all the assertions checking for uncaught exceptions, the
+`--disable-uncaught-exception-check` can be used in combination with
+`--throw-runtime-exceptions`.


It might be worth pointing out that in the JVM assert actually throws an AssertionError on violation. Thus it can be handled like any other 'exception' (Throwable, to be precise). This behaviour can be enabled with --throw-assertion-error. An assertion violation is then reported as an uncaught exception.

peterschrammel · 2018-11-13T18:29:38Z

doc/cprover-manual/jbmc-user-manual.md

+Rerunning the analysis with the `--trace` option, we can see find out which
+input value JBMC found to trigger the violation:
+```
+INPUT arg0i: 15


To getter better variable names, compile with -g and explain this.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a58697f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91258287

allredj · 2018-11-14T16:40:10Z

@peterschrammel this is ready for re-review.

Note for reviewers: since doc/cprover-manual is excluded from doxygen, if you want to see the html page, you must copy doc/cprover-manual/jbmc-user-manual.md into doc and generate the doxygen.

yumibagge · 2018-11-14T17:24:32Z

doc/cprover-manual/jbmc-user-manual.md

+```
+package tutorial;
+
+public class Example2


yumibagge · 2018-11-14T17:35:22Z

doc/cprover-manual/jbmc-user-manual.md

+Rerunning the analysis with the `--trace` option, we can see find out which
+input value JBMC found to trigger the violation:
+
+    INPUT inputVal: 15


When I run jbmc Example3.class --function tutorial.Example3.doSomething --unwind 10 --trace, I did not see INPUT inputVal: 15 but it shows me ```Violated property:
file tutorial/Example3.java function tutorial.Example3.doSomething(int) line 6 thread 0
assertion at file tutorial/Example3.java line 6 function java::tutorial.Example3.doSomething:(I)V bytecode-index 16
false

** 1 of 15 failed (2 iterations)
VERIFICATION FAILED

Don't you see something like this in the trace view? I rephrased the doc a bit to suggest that it needs a bit of searching.

Actually now I see INPUT inputVal: 15 (00000000 00000000 00000000 00001111), so now it is good.

yumibagge · 2018-11-14T17:39:42Z

doc/cprover-manual/jbmc-user-manual.md

+The value chosen by JBMC is arbitrary, and could as well be 9
+or 2084569161.
+Note that to see the original parameter names in the trace 
+output, the java source must be compiled in debug mode (`javac -g`).


I tried javac -g but but I could not find the original parameter names...

That's weird. I'll have a look at this on your machine.

This is also resolved.

yumibagge · 2018-11-14T17:53:23Z

doc/cprover-manual/jbmc-user-manual.md

+
+In the following code, only with `--throw-runtime-exceptions` will JBMC
+signal that the assertion on line 11 can be violated. Without that option,
+line 11 will be considered as unreachable, and hence the assertion to be valid.


It maybe nice to tell how jbmc thinks the line is unreachable from the log. Also without --throw-runtime-exception, I still get different Failure

You can't actually see that in the output. JBMC doesn't tell us which parts of the bytecode it managed to reach.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 479e45d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91407736
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 incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj · 2018-11-14T18:06:48Z

@yumibagge comments applied/responded to.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 7905eed).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91414593

allredj · 2018-11-15T10:06:43Z

@yumibagge from your offline comments:

Renamed the example files (instead of numbering them)
Modified the last sentence of the Unwind section to make it clearer
Added a side-note to the "Exceptions" section to prevent user from being confused by seeing an unrelated assertion failure in the output.
Hard-coded the line numbers (as the seem to not show automatically with the latest version of doxygen).

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: a197cd6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91499218
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 incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 41f3a43).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91507626

peterschrammel · 2018-11-15T15:15:59Z

doc/cprover-manual/jbmc-user-manual.md

+Now let's run the following command to let JBMC tell us about potential errors
+in our `query` method.
+
+    $ jbmc ExampleArray.class --function tutorial.ExampleArray.query


tutorial/ExampleArray.class

As mentioned in a previous comment, there is no tutorial folder. We're not in a Maven project. If you just use javac on a java file (which is the approach chosen in this tutorial), you get a class file in the same directory. 🔧

But this is not the way java works. You cannot run java ExampleArray, you must use java tutorial.ExampleArray. JBMC will work the same way soon. We can apply a simple 's#jbmc tutorial/ExampleArray.class#jbmc tutorial.ExampleArray' to this tutorial after this change.

OK, got it. That makes sense now. I now consider the class file to be in a folder named after the package.

peterschrammel · 2018-11-15T15:17:54Z

doc/cprover-manual/jbmc-user-manual.md

+In brief, JBMC creates a model from Java Bytecode (given as input as a .class
+file or a .jar) and performs static analysis and symbolic simulation which allow
+to prove or refute properties. These properties are either automatically
+generated, or provided by the user in the form of assertions.


automatically generated (runtime errors)

peterschrammel · 2018-11-15T15:19:19Z

doc/cprover-manual/jbmc-user-manual.md

+
+In brief, JBMC creates a model from Java Bytecode (given as input as a .class
+file or a .jar) and performs static analysis and symbolic simulation which allow
+to prove or refute properties. These properties are either automatically


allow us to prove

peterschrammel · 2018-11-15T15:19:36Z

doc/cprover-manual/jbmc-user-manual.md

+largely applies to JBMC.
+
+In brief, JBMC creates a model from Java Bytecode (given as input as a .class
+file or a .jar) and performs static analysis and symbolic simulation which allow


symbolic execution

I just re-used the wording from the CBMC tutorial. But will follow your suggestion.

Ah... I think execution is more common, though.

peterschrammel · 2018-11-15T15:22:45Z

doc/cprover-manual/jbmc-user-manual.md

+
+\subsection jbmc-manual-unwind Loop unwinding
+
+As CBMC, JBMC transforms the input program into a state representation,


I'm not sure 'state representation' is something intuitively understood by the reader.

removing this part of the sentence

peterschrammel · 2018-11-15T15:41:53Z

doc/cprover-manual/jbmc-user-manual.md

+
+\section jbmc-tutorial JBMC tutorial
+
+\subsection jbmc-manual-auto-assert Automatic assertions


Jbmc can detect two things: A. thrown exceptions/errors or B. uncaught exceptions/errors.

Orthogonally, there are 3 groups of errors that we want to detect:

Assertion violations

Runtime exceptions

Explicit throws

The question is how best to introduce it. B2, B3 are probably the concepts Java developers are most familiar with. A is a bit more for experts and probably best explained for 2 (as you do).
For people familiar with assertions starting with A1 would be doable. The difference between A1 and B1 is for practical purposes irrelevant (unless you catch AssertionError somewhere).

In the long term I'd like to make B the default behaviour.

What do you want me to do here? Shall I enumerate these groups in the introduction?

We have to restructure the sections a bit to start with familiar concepts and then go to less familiar ones. But we can do this in a second iteration.

peterschrammel · 2018-11-15T15:42:49Z

doc/cprover-manual/jbmc-user-manual.md

+To limit the number of times the for-loop is unwound, we use the `--unwind N`
+options, in which case the following call to JBMC:
+
+    $ jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10


tutorial/ExampleUnwind.class

peterschrammel · 2018-11-15T15:44:00Z

doc/cprover-manual/jbmc-user-manual.md

+ 2|
+ 3| public class ExampleArray {
+ 4|
+ 5|     public static int query(int[] array, int index) {


It might be worth changing this to static void main(String[]) to show also the case without --function option

I think it's slightly confusing to start with the example where the entry point is main, because the reader needs to understand that the entry point is always a function, and that main is only the default. So I change one of the later examples (the one with models). Furthermore, that example is better suited to be a main because we don't use any arguments.

It is very intuitive that the entry point is main because this is how you run a Java program. You can then explain that you can choose other methods entry point (which is unlike java).

That's right I'll try to start with an example with main as entry point then.

peterschrammel · 2018-11-15T15:44:40Z

doc/cprover-manual/jbmc-user-manual.md

+Rerunning the analysis with the `--trace` option, the following line appears
+somewhere in the trace output and tells us which input value JBMC found to
+trigger the violation (note that to see the original parameter names in the
+trace output, the java source must be compiled in debug mode: `javac -g`):


Java source

allredj · 2018-11-15T17:34:08Z

@peterschrammel changes applied. What would you like me to do about the 🔧 (folder of class files) issue? I could remove the package altogether, but I thought it would be good to show the syntax of --function with packages.
Alternatively I can actually put the class file inside a tutorial folder but it's difficult to explain why we would do this if we're not in a Maven project.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c7b714d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91561535

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c94494e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91640253

peterschrammel

Let's go with that

allredj · 2018-11-16T11:17:31Z

@peterschrammel I have made some improvements. Do you want to take a look?

peterschrammel · 2018-11-16T11:20:35Z

doc/cprover-manual/jbmc-user-manual.md

+[java::tutorial.ExampleExceptions.strLength:(Ljava/lang/String;)I.1] line 6 no uncaught exception: FAILURE
+```
+This could be fixed by adding a try-catch statement, or else checking that
+`str` is non-Null before accessing it.


⛏ non-null

peterschrammel · 2018-11-16T11:22:48Z

@allredj, please squash the commits

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: ab18976).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91656682
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 incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 00ac7b8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91657894

allredj self-assigned this Nov 13, 2018

allredj requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners November 13, 2018 18:13

allredj requested a review from romainbrenguier November 13, 2018 18:14

peterschrammel reviewed Nov 13, 2018

View reviewed changes

allredj commented Nov 13, 2018

View reviewed changes

peterschrammel added the documentation label Nov 13, 2018

allredj force-pushed the allredj/doc-jbmc-user-manual branch from a58697f to 479e45d Compare November 14, 2018 16:36

yumibagge reviewed Nov 14, 2018

View reviewed changes

allredj force-pushed the allredj/doc-jbmc-user-manual branch from 479e45d to 7905eed Compare November 14, 2018 18:01

allredj commented Nov 14, 2018

View reviewed changes

allredj force-pushed the allredj/doc-jbmc-user-manual branch from a197cd6 to 83c4929 Compare November 15, 2018 10:04

allredj force-pushed the allredj/doc-jbmc-user-manual branch from 83c4929 to 41f3a43 Compare November 15, 2018 10:39

allredj commented Nov 15, 2018

View reviewed changes

yumibagge approved these changes Nov 15, 2018

View reviewed changes

peterschrammel reviewed Nov 15, 2018

View reviewed changes

allredj commented Nov 15, 2018

View reviewed changes

allredj commented Nov 16, 2018

View reviewed changes

peterschrammel approved these changes Nov 16, 2018

View reviewed changes

allredj force-pushed the allredj/doc-jbmc-user-manual branch from c94494e to 63c944c Compare November 16, 2018 11:16

peterschrammel approved these changes Nov 16, 2018

View reviewed changes

Add JBMC user manual

00ac7b8

allredj force-pushed the allredj/doc-jbmc-user-manual branch from ab18976 to 00ac7b8 Compare November 16, 2018 11:25

allredj commented Nov 16, 2018

View reviewed changes

allredj merged commit 6953507 into develop Nov 16, 2018

allredj deleted the allredj/doc-jbmc-user-manual branch November 16, 2018 13:18


		\subsection jbmc-manual-unwind Loop unwinding

		As in CBMC, JBMC transforms the input program into a state representation,


		\subsection jbmc-manual-unwind Loop unwinding

		As CBMC, JBMC transforms the input program into a state representation,


		\section jbmc-tutorial JBMC tutorial

		\subsection jbmc-manual-auto-assert Automatic assertions

Add JBMC user manual [DOC-9] #3404

Add JBMC user manual [DOC-9] #3404

Uh oh!

Conversation

allredj commented Nov 13, 2018

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj commented Nov 14, 2018

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!

allredj Nov 14, 2018 • 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj commented Nov 14, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj commented Nov 15, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj Nov 14, 2018 •

edited

Loading

allredj Nov 15, 2018 •

edited

Loading

allredj Nov 15, 2018 •

edited

Loading