Add JBMC user manual

Author: Joel Allred

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

@@ -0,0 +1,229 @@
+\ingroup module_hidden
+\page jbmc-user-manual JBMC User Manual
+
+
+\section jbmc-manual-intro Introduction
+
+JBMC is a bounded model checking tool for the Java language. It follows the
+same principles as CBMC, thus the existing
+[documentation for CBMC](http://www.cprover.org/cprover-manual/cbmc.html)
+largely applies to JBMC.
+
+In brief, JBMC creates a model from Java Bytecode (given as input as .class
+files) 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.
+
+Using examples, the following section will guide you through the basic
+features of JBMC, and explore the most useful features.
+
+
+\section jbmc-tutorial JBMC tutorial
+
+\subsection jbmc-manual-auto-assert Automatic assertions
+
+Consider the following simplistic `Example.java` file which we have compiled
+into `Example.class` and which contains a utility method to query a given
+array at a given index:
+```java
+1  package core;
+2
+3  public class Example {
+4
+5      public static int query(int[] array, int index) {
+6          return array[index];
+7      }
+8  }
+```
+
+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
+```
+
+The output contains the following:
+```
+core/Example.java function java::core.Example.query:([II)I
+[java::core.Example.query:([II)I.null-pointer-exception.1] line 6 Null pointer check: FAILURE
+[java::core.Example.query:([II)I.array-index-out-of-bounds-low.1] line 6 Array index should be >= 0: FAILURE
+[java::core.Example.query:([II)I.array-index-out-of-bounds-high.1] line 6 Array index should be < length: FAILURE
+[java::core.Example.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+```
+Three reported failures spring up:
+1) there is no null pointer check on the array passed as argument
+2) there is no check that the index at which we access the array is non-negative
+3) there is no check that the index is within the length of the array.
+
+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) {
+6          if (array == null) {
+7              return -1;
+8          }
+9          if (index < 0 || index >= array.length) {
+10             return -1;
+11         }
+12         return array[index];
+13     }
+```
+
+then the JBMC automatic assertions become valid, meaning that there is no
+possible inputs (argument values) for which they can be violated:
+```
+core/Example.java function java::core.Example.query:([II)I
+[java::core.Example.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+[java::core.Example.query:([II)I.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
+[java::core.Example.query:([II)I.null-pointer-exception.2] line 12 Null pointer check: SUCCESS
+[java::core.Example.query:([II)I.array-index-out-of-bounds-low.1] line 12 Array index should be >= 0: SUCCESS
+[java::core.Example.query:([II)I.array-index-out-of-bounds-high.1] line 12 Array index should be < length: SUCCESS
+```
+
+\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
+unwind limit, JBMC will not terminate when analysing the following function
+whose state representation is theoretically unbounded (because of the for-loop
+whose number of iterations depends on an input):
+```java
+    public static boolean isPrime(int candidate) {
+        for (int div = 2; div <= candidate / 2; div++) {
+            if (candidate % div == 0) {
+                return false;
+            }
+        }
+        return candidate > 1;
+    }
+```
+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
+```
+will terminate (with `VERIFICATION SUCCESSFUL`).
+
+
+\subsection jbmc-manual-user-assert User assertions
+
+Elaborating on the example above, users may provide their own assertions, that
+ JBMC will try do refute. Consider the following class:
+ ```java
+1   package core;
+2
+3   public class Example {
+4
+5       public static void doSomething(int input) {
+6           if (input > 1 && input % 2 == 1) {
+7               assert isPrime(input);
+8               // do something
+9           }
+10      }
+11
+12      public static boolean isPrime(int candidate) {
+13          for (int div = 2; div * div <= candidate; div++) {
+14              if (candidate % div == 0) {
+15                  return false;
+16              }
+17          }
+18          return candidate > 1;
+19      }
+20
+21  }
+ ```
+
+On line 7, we check the assertion that all odd numbers greater than 1 are prime.
+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
+```
+and unsurprisingly JBMC doesn't agree, and prints an assertion failure
+(truncated here for readability):
+```
+ [...doSomething:(I)V.assertion.1] line 7 assertion at file core/Example.java: FAILURE
+```
+
+Rerunning the analysis with the `--trace` option, we can see find out which
+input value JBMC found to trigger the violation:
+```
+INPUT arg0i: 15
+```
+The value chosen by JBMC is arbitrary, and could as well be 9 or
+2084569161.
+
+\subsection jbmc-manual-library Java Library support
+
+The examples above only involve primitive types. In order to analyse code
+involving Java Library classes, the core models (located in the same
+repository) need to be added to the classpath:
+```
+--cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar
+
+```
+The core models library simulate the behaviour of the Java Library and
+contains some commonly used classes, such as Object, Class, String, Enum.
+Some JBMC-specific utilities reside in the `org.cprover` package.
+
+Using the models, JBMC can reason with a variety of the String operations
+from `java.lang.String`, e.g.
+
+```java
+5    public static void doSomething() {
+6        StringBuilder sb = new StringBuilder("abcd");
+7        StringBuilder sb2 = sb.insert(2, "$");
+8        assert sb2.toString().startsWith("abc");
+9    }
+
+```
+The following command line (note that the current directory is also added to
+the classpath):
+```
+jbmc Example.class --function core.Example.doSomething --cp
+<path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
+```
+will flag this violation (truncated):
+```
+[java::core.Example.doSomething:()V.assertion.1] line 8 assertion: FAILURE
+```
+Again, the trace shows the contradicting string:
+```
+  dynamic_object2={ 'a', 'b', '$', 'c', 'd' }
+```
+
+\subsections jbmc-manual-exceptions Exceptions
+
+In its analysis, JBMC can take into account exceptions thrown by user code or
+library classes, as well as runtime exceptions such as NullPointerException.
+To have JBMC reliably notify about all uncaught exceptions, the
+`--throw-runtime-exceptions` can be used.
+
+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.
+```java
+5     public static int exceptionHandling(String str) {
+6         int retval = 0;
+7         try {
+8              retval = str.length();
+9         } catch (NullPointerException except) {
+10            retval = -1;
+11            assert false;
+12        }
+13        return retval;
+14    }
+```
+
+To remove all the assertions checking for uncaught exceptions, the
+`--disable-uncaught-exception-check` can be used in combination with
+`--throw-runtime-exceptions`.
+
+\subsection jbmc-manual-further-doc Further documentation
+
+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:
+```
+jbmc --help
+```