docs/user/config.md

   1 # Configuring JPF #
   2
   3 JPF configuration can be intimidating. It is worth to think about why we need such a heavy mechanism before we dive into its details. Little in JPF is hardwired. Since JPF is such an open system that can be parameterized and extended in a variety of ways, there is a strong need for a general, uniform configuration mechanism. The challenge for this mechanism is that many of the parts which are subject to parameterization are configured themselves (i.e. options for optional JPF components like listeners). This effectively prohibits the use of a configuration object that contains concrete fields to hold configuration data, since this class would be a central "design bottleneck" for a potentially open number of JPF components like Searches, Instruction sets and Listeners.
   4
   5 The goal is to have a configuration object that
   6
   7   * is based on string values
   8   * can be extended at will
   9   * is passed down in a hierarchical initialization process so that every component extracts only its own parameters
  10
  11 We achieve this by means of a central dictionary object (`gov.nasa.jpf.Config`) which is initialized through a hierarchical set of Java property files that target three different initialization layers:
  12
  13   1. site: optionally installed JPF components
  14   2. project: settings for each installed JPF module and (optionally) systems under test
  15   3. application: the class and program properties JPF should check (this is part of your system under test)
  16
  17 Initialization happens in a prioritized order, which means you can override anything from later configuration stages, all the way up to command line parameters. Actually, this can be even overridden by using the `Verify` API from system under test code, but this is a developer topic. Here is the blueprint, which we will examine in order of execution:
  18
  19 ![Figure: Configuring JPF](../graphics/properties.svg){align=center width=800}
  20
  21
  22 ## Property Types ##
  23
  24 Property specifications are processed in a hierarchical order: site properties, project properties, application properties and command line properties. Later stages can override previous stages. Each property is a `<key>=<value>` pair, but we do support some special notations (see below) for key/value expansion, value extension, and pseudo properties that act as directives.
  25
  26 ### Site Properties ###
  27 The site.properties file is machine specific and not part of any JPF project, which means you have to create a [ site.properties](wiki:install/site-properties) file as part of the install process. A sample site.properties might look like:
  28
  29 ~~~~~~~~
  30 jpf-core = ${user.home}/projects/jpf/jpf-core
  31 jpf-shell = ${user.home}/projects/jpf/jpf-shell
  32 jpf-awt = ${user.home}/projects/jpf/jpf-awt
  33 ...
  34 extensions=${jpf-core},${jpf-shell}
  35 ~~~~~~~~
  36
  37 Each module is listed as a `<name>=<directory>` pair, and optionally added to the comma separated list of `extensions`. The order in which modules are added to `extensions` does matter, since it will determine the order in which each of these components is initialized, which basically maps to an ordered list of classpath entries (both for the host VM and JPF itself - paths are kept separate).
  38
  39 Note that we do **not** require all modules being added to `extensions`, **but** jpf-core needs to be in there. Dependencies on modules not listed in `extensions` can be specified later-on with the `@using` directive. It is a good idea to keep the `extensions` list small to avoid conflicts, and to improve class load times (shorter classpaths).
  40
  41 Note also that the `extensions` entries are of the form `${<key>}`, which tells JPF to replace these expressions with the value that is associated to <key>.
  42
  43 Site properties have to be stored in the directory from where you start JPF, one of its parent directories, or a global `${user.home}/.jpf/site.properties`. We recommend a to keep it in a common root directory that contains all your JPF projects and modules.
  44
  45
  46 ### Project Properties ###
  47 Each JPF module contains a jpf.properties file in its root directory, no matter if this is the jpf-core or an extension. System under test projects can contain a jpf.properties file to factor out common settings (such as class paths) for all JPF applications within this project.
  48
  49 A project property file defines the JPF specific paths that need to be set for the module or system under test to work properly
  50
  51  1. `<module-name>.`**`native_classpath`**: the host VM classpath (i.e. the classes that constitute JPF itself)
  52  1. `<module-name>.`**`classpath`**: the classpath JPF uses to execute the system under test
  53  1. `<module-name>.`**`test_classpath`**: host VM and JPF classpath for regression tests
  54  1. `<module-name>.`**`sourcepath`**: the path entries JPF uses to locate sources in case it needs to create program traces
  55
  56 Additionally, `jpf.properties` should contain default values for all module or project specific settings (e.g. report options).
  57
  58 An example project properties file might look like:
  59
  60 ~~~~~~~~ {.bash}
  61 jpf-aprop = ${config_path}
  62
  63 #--- path specifications
  64 jpf-aprop.native_classpath = build/jpf-aprop.jar;lib/antlr-runtime-3.1.3.jar
  65 jpf-aprop.classpath = build/examples
  66 jpf-aprop.test_classpath = build/tests
  67 jpf-aprop.sourcepath = src/examples
  68
  69 #--- other project specific settings
  70 listener.autoload=${listener.autoload},javax.annotation.Nonnull,...
  71 listener.javax.annotation.Nonnull=gov.nasa.jpf.aprop.listener.NonnullChecker
  72 ...
  73 ~~~~~~~~
  74
  75
  76
  77 The first entry (`<module-name>=${config_path}`) in a jpf.properties should always define the module name. JPF automatically expands `${config_path}` with the pathname of the directory in which this jpf.properties file resides.
  78
  79 jpf.properties are executed in order of definition within site.properties, with one caveat: if you start JPF from within a directory  that contains a jpf.properties file, this one will always take precedence, i.e. will be loaded last (overriding previous settings except of the command line). This way, we ensure that JPF developers can enforce priority of the component they are working on.
  80
  81 Both site.properties and jpf.properties can define or override any key/value pairs they want, but keep in mind that you might end up with different system behavior depending on where you start JPF - avoid configuration force fights by keeping jpf.properties settings disjunct wherever you can.
  82
  83 Please note that site and project properties have to be consistent, i.e. the module names (e.g. jpf-awt) in site.properties and jpf.properties need to be the same. This is also true for the build.xml Ant project names.
  84
  85 It is perfectly fine to have a jpf.properties in a SUT that only uses JPF for verification. You need at least to set up the `classpath` so that JPF knows where to find the SUT classes.
  86
  87
  88 ### Application Properties ###
  89 In order to run JPF, you need to tell it what main class it should start to execute. This is the minimal purpose of the *.jpf application properties files, which are part of your systems under test (SUT). Besides the `target` setting that defines the main class of your SUT, you can also define a list of `target_args` and any number of JPF properties that define how you want your application to be checked (listeners, search policy, bytecode factories etc.). A typical example looks like
  90
  91 ~~~~~~~~ {.bash}
  92 #--- dependencies on other JPF modules
  93 @using = jpf-awt
  94 @using = jpf-shell
  95
  96 #--- what JPF should run
  97 target = RobotManager
  98
  99 #--- other stuff that defines how to run JPF
 100 listener+=,.listener.OverlappingMethodAnalyzer
 101
 102 shell=.shell.basicshell.BasicShell
 103 awt.script=${config_path}/RobotManager-thread.es
 104 cg.enumerate_random=true
 105 ...
 106 ~~~~~~~~
 107
 108 The `@using = <module-name>` directive tells JPF to load the `jpf.properties` of the specified projects (defined in `site.properties`). This is the way to ensure proper path initialization of projects that are not listed in `extensions`.
 109
 110 ### Command Line Properties ###
 111 Last not least, you can override or extend any of the previous settings by providing "**+**<key>=<value>" pairs as command line options. This is convenient for experiments if you have to determine the right settings values empirically
 112
 113
 114 ## Special Property Syntax ##
 115 JPF supports a number of special notations that are valid Java properties syntax, but are only processed by JPF (and - to a certain extend - by Ant):
 116
 117  * **`key=...${x}..`** - replaces `"${x}"` with whatever is currently stored under the key "`x`". This also works recursively, as in "`classpath = mypath;${classpath}`". Note that while Apache Ant does also support value expansion, but not recursively. In addition, JPF also supports expansion in the key part (i.e. left of the "`=`")
 118
 119  * **`key+=val`** - appends val to whatever is currently stored under "`key`". Note that there can be no blank between key and "`+=`", which would not be parsed by Java. This expansion only works in JPF
 120
 121  * **`+key=val`** - in a properties file adds "`val`" in front of what is currently stored under "`key`". Note that if you want to use this from the command line, you have to use two "`++`", since command line options start with "+"
 122
 123  * **`${config_path}`** - is automatically set to the directory pathname of the currently parsed property file. This can be useful to specify relative pathnames (e.g. input scripts for the jpf-awt extension)
 124
 125  * **`${config}`** - is set to the file pathname of the currently parsed file
 126
 127  * **`@requires=<key>`** - can be used to short-circuit loading of a properties file. This is a simple mechanism to control loading of jpf.properties file sections that are incompatible with other modules, and compares to `#ifdef` preprocessor directives. The respective keys are usually set from application properties (*.jpf) files.
 128 Note this does not throw an exception if the required key is not defined, it just bails out of loading the properties file that contains the @requires directive
 129
 130  * **`@include=<property-file>`** - recursively loads the properties file with the specified pathname. You can use the automatically defined `${config_path}` property to specify path names that are relative to where the file containing the `@include` directive is, or use `${<module-name>}` for paths that are relative to the specified module.
 131
 132  * **`@using=<module-name>`** - is similar to `@include`, but loads the jpf.properties of the specified module name (which has to be defined in site.properties). Note that there is no `${..}` around the module name - otherwise it would be replaced. The `@using` directive is the preferred way to specify dependencies on modules that are not in the `extensions` list (i.e. automatically initialized).
 133
 134  * **`@include_if = ?<key>?<properties-file>`** - is a conditional `@include` that only loads the properties file if the specified `<key>` is defined
 135
 136  * **`@include_unless = ?<key>?<properties-file>`** - likewise loads the file only if `<key>` is not defined. Both of these directives are used rarely.
 137
 138  * Omitting the "`=..`" part in command line settings defaults to a "`true`" value for the corresponding key
 139
 140  * Setting an empty value (`key=`) removes the key from the config dictionary
 141
 142 ## Debugging ##
 143 Depending on the number of installed and loaded projects, you can easily end up with hundreds of settings. There are two command line options you can use if you assume there is a configuration error:
 144
 145  * **`-show`** - prints all Config entries after the initialization is complete
 146
 147  * **`-log`** - lists the order in which properties files got loaded by JPF
 148
 149 ## Details on various options ##
 150
 151 * [Randomization](config/random)
 152
 153 * Error Reporting