Skip to content

User Guide

Jump to bottom
Petr Hudeček edited this page Jul 29, 2016 · 11 revisions

Welcome to JPF Inspector, the debugger designed for debugging applications run using Java Pathfinder!

JPF Inspector capabilities

If you use JPF with your application, as a model checker, verifier, or otherwise, your application runs under the JPF virtual machine which runs itself on top of the native virtual machine. This prevents normal debuggers from working at all.

JPF Inspector, however, is a fully featured GDB-like debugger for such applications. You may set breakpoints and step through your program, forwards and backwards, explore values of variables and fields, modify them and view call stacks. JPF Inspector goes beyond what GDB provides and also gives you additional debugging tools.

This user guide will get you started with basic capabilities of the Inspector. To understand more advanced features, check out the documentation page on commands, hit conditions and expressions or browse the table of contents.

JPF Inspector is platform-independent.

Launching JPF Inspector

First, download the jpf-inspector extension and the jpf-shell extension that the Inspector depends on (where are these repositories?).

In your site.properties file (see creating a site.properties file), add references to these extensions.

For example, your site.properties file could look like this:

jpf-base-dir =  /home/jancik/jpf
jpf-core =      ${jpf-base-dir}/jpf-core
jpf-shell =     ${jpf-base-dir}/jpf-shell
jpf-inspector = ${jpf-base-dir}/jpf-inspector

extensions=${jpf-core}

Then, in your application configuration file, add a reference to the Inspector and specify the shell that you want to use:

For example, your app.jpf file could look like this:

@using jpf-inspector
shell=.shell.basicshell.BasicShell
target=[your_application_main_class]

If you want to use the command-line shell and not the graphical shell, use instead:

@using jpf-inspector
shell=.inspector.frontends.cmd.CommandLineShell
target=[your_application_main_class]

Then don't forget to build all extensions by running ant build inside jpf-core, jpf-shell and finally jpf-inspector.

(Troubleshooting: It is possible you will encounter compile errors at this point. There are several common causes: your Java minor version might not be compatible with jpf-core; your site.properties file might be set incorrectly; a configuration file or extension is missing or cannot be found by Ant.)

Then, you can start up a debugging session by running a line such as this:

$ java -jar ./jpf-core/build/RunJPF.jar ./app.jpf

While setting up your configuration, ensure that your application source files are in a source_path property, or else JPF won't be able to find them and Inspector capabilities will be greatly reduced.

Using JPF Inspector panels

This user guide assumes you're using the graphical shell. For the command-line shell, see Commandline Shell.

Console

Your primary interface with JPF Inspector is the console:

Here, you can execute commands in a GDB-like fashion. The most common commands are:

You may look at the tutorial to see these commands in action.

The console, however, is not the only way you can interact with the Inspector.

Source view

If you set up your sourcepath correctly, JPF Inspector will also show you relevant source code in the source view panel:

The line with the current instruction is highlighted.

Quick toolbar commands

When stepping through your program, you might find it useful to look at the source view panel and use the quick stepping commands in the toolbar to avoid having to type commands.

You may also add your own favorite commands to the toolbar, see Quick Commands.

Explorer

There is also a graphical explorer of the program state where you can browse through all Java objects in the state.

Tab tearing

You can drag a tab from the shell out to create a new window. This way, you may have multiple panels side by side. For example, you might want to see the Explorer and the source view at the same time.

Setting breakpoints

Unlike traditional debuggers where you mostly set a breakpoint on a line of code and optionally add some conditions, in JPF Inspector, this kind of breakpoint is merely one of many possible [hit conditions](Hit Condition Expression Syntax).

To set up a breakpoint, use the command create breakpoint, for example:

create breakpoint position=myPackage.myClass:20

which breaks execution at the beginning of the 20th line of the file that contains myPackage.myClass.

You can print all breakpoints using show breakpoint or delete them using delete breakpoint.

Some more examples of hit conditions include:

  • local_write=val: breaks when an instruction writes into a local variable named val
  • method_invoke=*:factorial: breaks when a method named factorial is called
  • thread_scheduled=in:4: breaks when the thread number 4 is scheduled to run
  • see [the comprehensive list](Hit Condition Expression Syntax) or create your own

Breakpoints support more advanced features, see the documentation of create breakpoint for details and Breakpoints (advanced guide) for really advanced features.

Abbreviations & Help

Use the command help to print the syntax of all built-in commands and hit conditions.

All commands and many hit conditions have "abbreviated versions" to save you some typing. For example, instead of

create breakpoint position=myPackage.myClass:20

you can also type

cr bp pos=myPackage.myClass:20

The help command will print the abbreviated forms as well and the comprehensive list of commands also lists each command's abbreviated forms.

Exploring program state

When the debugged program is stopped, you may read the values of variables and fields using the command print or using the graphical explorer.

More information on the syntax of the command print and on possible expressions can be found in its documentation and the page Expression syntax.

Some examples:

  • print #thread[2] prints the thread with index 2
  • print #thread[2].#stackFrame[0] prints the top stack frame of thread 2
  • print #stackFrame prints the top stack frame of the active thread
  • print #thread.#stackFrame.var prints the value of the local variable var
  • print #heap[*] prints a list of all objects on the heap
  • print #heap[java.*] prints a list of all objects on the heap whose class is in the java package
  • print #heap[424] prints the object on the heap with index 424
  • print #heap[0xFF] prints the object on the heap with index 256
  • print #thread[2].#stackFrame[1].p2.left prints the value of the field left of the object in the local variable or parameter p2 on the second stack frame from the top on the thread with index 2
  • print local_array[4] prints the object at index 4 of the local variable local_array that is of an array type
  • print #this.#field[2] prints the value of the instance field with index 2 of the receiver object of the currently executed method

Modifying values

When the debugged program is stopped, you may also set new values for its variables and fields using the command set. To do this, execute set [name] = [value], where [name] is any assignable location. It could be the name of a local variable, or perhaps an expression such as #thread[2].#stackFrame[1].#stackSlot[4].

Here's some examples (for more, see Expression syntax).

  • set my_bool = true assigns true to a boolean variable.
  • set my_charArray[10] = 'A' assigns the character A to the character array at the index 10.
  • set my_byte = my_Integer assigns the current value of the existing variable my_Integer of the type java.lang.Integer to a byte variable.
  • set my_const_Object = null assigns the null value to the given reference variable (of any type).
  • set my_String = "Alf rules" assigns the given string constant to a string variable.
  • set #heap[10].float_val = 3.1415f assigns the Pi value defined as a float constant to the field float_val of the specified heap object.
  • set my_double = NaN - the user can assign special values NaN (not-a-number), -inf (negative_infinity), and +inf (positive_infinity) to floating point variables.

Example use:

cmd>print #this.field
	1 : field (int) = 5

cmd>set #this.field = -8
Value set successfully.

cmd>print #this.field
	1 : field (int) = -8

Stepping

Using JPF Inspector, you may step forward in the program, instruction by instruction, but not only that - JPF also permits us to support backwards stepping.

By forward stepping, we mean executing until we reach a specified point - the next instruction or the next line, for example - and then stopping.

By backwards stepping, we mean "undoing" recent instructions. Internally, what happens is that the Inspector forces JPF to backtrack the most recent transition (possibly multiple transitions) and then re-executes instruction up until the point towards which we want to backstep.

The following stepping commands exist:

  • step_instruction to move one instruction forwards
  • step_in to enter the next method call
  • step_over to move one line forwards
  • step_out to complete the current method
  • step_transition to complete the current transition
  • back_step_instruction to undo one instruction
  • back_step_in to return before the last return statement
  • back_step_over to undo one line
  • back_step_out to undo the current method
  • back_step_transition to undo the current transition
  • back_field_access to step back to where a field was accessed
  • back_breakpoint_hit to step back to where last a breakpoint was hit

All of these commands are described in more detail in a separate page and advanced information on stepping is also available.

Because backwards stepping may be complex to wrap one's head around, you might find it useful to first look at the tutorial.

Conclusion

This concludes the introductory user guide. In the table of contents at Home, you will find more documentation on various advanced features of JPF Inspector.

Some features you might be interested in are:

Clone this wiki locally