cLARVA

Residual analysis for properties as symbolic automata

cLARVA (= clara + LARVA) is a tool aimed to reduce some of the overheads associated with runtime verifiying Java programs with Dynamic Automata with Events and Timers (DATEs), and variants thereof. The tool attempts to find parts of the program that can be ignored soundly for verification, and to remove transitions in a DATE that are not needed to identify a violation at runtime. Soot, a Java bytecode analyser, is used to support this analysis.

Limitations:

1. Only properties about sequential parts of the program will be analysed soundly. You can still analyse programs with threads, but the results will only apply intra-thread, and no guarantees are given for any interleaving behaviour.
2. Only LARVA scripts with one DATE will be processed.
3. Only control-flow static analysis is used, ignoring any data-oriented concerns of a DATE.
4. Tool is still under development. It has been manually verified to give correct results under some case studies, however this does not ensure that other bugs are not present.

Input:

1. mode of the analysis -- (a) fast: uses a Class Hierarchy Analysis (CHA) to create a more or less sound callgraph, while ignoring java., jdk., and sun.* packages, giving a quick (should take seconds) analysis; and (b) intensive uses SPARK, creating a more precise callgraph and pointer-analysis by considering also library files, leading to a longer processing time (should take some minutes);
2. filePath to DATE property --- an automata specifying the violating traces of the previous program (through AspectJ notions) with transitions over events (method calls) and conditions encoding data state (see Larva Manual for the syntax of DATEs).
3. root directory of compiled Java program (in eclipse, the bin directory); and
4. Canonical name of the Main class of program (of the form <package-name>.<class-name>).

Example call: -jar clarva.jar fast java "./date.lrv" "./bin" main.Main

Output:

1. A DATE that is a pruned version of Input (2), with which it is enough to monitor Input (3).
2. Class files of the program with some program statements modified to soundly avoid subsequent LARVA instrumentation.

Note that instrumentation is optimised by creating a new class with methods for each method call to be instrumented, and by instrumenting the bytecode of the original Java program by invoking these new methods for events that have been classed as needed to give the same results as the original instrumentation (modulo the input and output DATEs).

The output class files should then be weaved with the output DATE using the LARVA compiler.

Tips

1. One may wish to analyse a program with multiple entry-points. A way to do this would be to create a mock main class that can access each entry-point in a random manner, and use this as the main class for the analysis.

See technical report CS-2017-01 in this series for a detailed version of the theory behind this tool, which will be published in the proceedings of PrePost 2017, in the EPCTS series, and available on arXiv.