The more you know.

Documentation for various components of GameTime.

Project Configuration Files

The project configuration file is an XML file that allows you to configure a GameTime project. A sample project configuration file is provided in the sandbox directory of the GameTime distribution (and also available here). The schema of the project configuration file is described below. Click on the tags to expand or collapse their descriptions and their children tags.

<gametime-project>
Contains options to configure GameTime for a specific project.
<file>
Contains and maintains information about the function that is analyzed by GameTime.
<location>
Location of the C file that contains the function that is analyzed by GameTime. This location can be either absolute or relative: if relative, the location is resolved with respect to the directory that contains the project configuration XML file.
</location>
<analysis-function>
Name of the function that is analyzed by GameTime.
</analysis-function>
<start-label>
Label in the function where GameTime starts the analysis from. If left empty, GameTime will start the analysis of the function from its beginning.
</start-label>
<end-label>
Label in the function where GameTime ends its analysis at. If left empty, GameTime will end the analysis of the function at its end.
</end-label>
</file>
<preprocess>
Contains configuration options for preprocessing the file using source-to-source transformations before analysis.
<include>
Locations of directories that contain other files that need to be compiled and linked, but not preprocessed, with the file that contains the function to be analyzed, such as header files. More than one directory can be specified, and the names must be separated by either whitespaces or commas. The locations can be either absolute or relative: if relative, a location is resolved with respect to the directory that contains the project configuration XML file.
</include>
<merge>
Locations of other files to be merged and preprocessed with the file that contains the function to be analyzed. More than one file can be specified, and the names must be separated by either whitespaces or commas. Unix-style globs are also permitted. The locations can be either absolute or relative: if relative, a location is resolved with respect to the directory that contains the project configuration XML file.
</merge>
<inline>
Functions to inline, if any. More than one function can be specified, and the names must be separated by whitespaces or commas.
</inline>
<unroll-loops>
If added, this tag asks GameTime to unroll loops in the code. No content is required for this tag.
</unroll-loops>
</preprocess>
<analysis>
Contains configuration options for various features of the GameTime analysis.
<randomize-initial-basis>
If added, this tag asks GameTime to randomize the basis that it starts the analysis with. Without randomization, the initial basis is the standard basis. No content is required for this tag.
</randomize-initial-basis>
<determinant-threshold>
Threshold below which the determinant of the basis matrix is considered "too small". The default threshold is 0.001.
</determinant-threshold>
<max-infeasible-paths>
Maximum number of infeasible paths that can be explored before the row of a basis matrix is considered "bad". The default maximum number is 100.
</max-infeasible-paths>
<model-as-nested-arrays>
If added, this tag asks GameTime to model multi-dimensional arrays as nested arrays, or arrays whose elements can also be arrays, in an SMT query. If not added, a multi-dimensional array will be modeled as a one-dimensional array, and the indices of an access will be concatenated. No content is required for this tag.
</model-as-nested-arrays>
<prevent-basis-refinement>
If added, this tag prevents GameTime from refining the basis into a 2-barycentric spanner. No content is required for this tag.
</prevent-basis-refinement>
<ilp-solver>
Integer linear programming solver used to solve integer linear programs to generate candidate paths.
The following options are recognized:
  • cbc for CBC.
  • cbc-pulp for the version of CBC provided with the pulp Python package.
  • cplex for CPLEX.
  • glpk for GLPK.
  • gurobi for Gurobi.
  • xpress for Xpress.
If no solver is specified, the default solver of the pulp Python package will be used.
</ilp-solver>
<smt-solver>
SMT solver that GameTime uses to check the satisfiability of an SMT query.
The following options are recognized: An SMT solver must be specified.
</smt-solver>
<maximum-error-scale-factor>
Specifies the accuracy of the overcomplete basis. This parameter is used only when the --overcomplete_basis command line flag is used.
</maximum-error-scale-factor>
</analysis>
</gametime-project>

Sandbox Script

The sandbox script is a ready-made Python script located within the sandbox directory in the GameTime distribution: the directory is intended for user projects, although projects can be placed at any writable location in the filesystem. This script, available at sandbox/analyzeProject.py, uses the Python interface to the GameTime toolkit.

The GameTime distribution also contains a batch script, available at gametime.bat, which sets up a prompt and several environment variables needed for the functioning of GameTime. The batch script can be used to interact with the sandbox script: the command analyze, when used at the prompt, is an alias for the command python sandbox/analyzeProject.py.

The command-line arguments for the sandbox script, and thus for the command analyze, are described below, separated into sections according to their intended usages. Click on the section titles and the command-line arguments to expand or collapse their descriptions. For arguments that expect a location on the filesystem, the relative locations are resolved against the current working directory.

This documentation can also be obtained through either the command analyze --help or the command analyze -h.

Optional command-line arguments for GameTime analysis
Options to initialize and save the GameTime analysis.
-a LOCATION, --analyze LOCATION
Location of the XML file that configures a GameTime project. The location of a directory can also be provided, in which case the first XML file found in the directory will be used to configure a GameTime project. If this argument is not provided, the XML file located in the GameTime source distribution at demo/modexp_unrolled/projectConfig.xml will be used.
--analyzer-location LOCATION
Location where the analyzer is saved. If this argument is not provided, the analyzer is saved to a file called analyzer in a temporary directory called analysis, created within the directory that contains the code to analyze.

Optional command-line arguments for preprocessing
Options to preprocess the code to analyze.
--unroll-loops
Unrolls the loops in the code under analysis, using the bounds provided by the user in the loop configuration file generated during loop detection. The use of this option overrides the corresponding tag ( <unroll-loops> ) in the project configuration XML file.

Optional command-line arguments for feasible basis paths
Options to generate basis paths.
-b, --basis
Generates the basis paths of the code under analysis, and writes them to files in a temporary directory called analysis, created within the directory that contains the code to analyze.
--overcomplete_basis
Generates an overcomplete basis paths of the code under analysis. The accuracy of the overcomplete basis is specified by the parameter maximum-error-scale-factor. The paths are written to files in a temporary directory called analysis, created within the directory that contains the code to analyze. If this flag is used, then use the flag --ob_extraction to generate predictions of the lengest feasible paths.

Optional command-line arguments for other types of feasible paths
Options to generate other types of feasible paths, once the basis paths have been generated. All paths are also written to files in a temporary directory called analysis, created within the directory that contains the code to analyze, and the predicted values of these paths are also saved to a file whose name has the prefix predicted-.
--values FILE
Location of the file that contains the values to be associated with the basis paths. If this argument is not provided, this script assumes that this file is called measured-basis, located in the temporary directory called analysis.
-n NUM, --num-paths NUM
Upper bound on the number of paths to generate. This value is ignored if all feasible paths are being generated. The default value is 5.
-w, --worst-case
Generates the worst-case feasible paths of the code under analysis (paths with the largest values).
--ob_extraction
Generates the worst-case feasible paths of the code under analysis (paths with the largest values).
-v, --best-case
Generates the best-case feasible paths of the code under analysis (paths with the smallest values).
-r, --random
Generates random feasible paths of the code under analysis.
-d, --all-decreasing
Generates all feasible paths of the code under analysis (in decreasing order of value).
Warning: The total number of feasible paths can be very large.
-i, --all-increasing
Generates all feasible paths of the code under analysis (in increasing order of value).
Warning: The total number of feasible paths can be very large.
-l BOUND, --lower BOUND
Lower bound on the values of the feasible paths that are generated. If this argument is not provided, no lower bound is assumed.
-u BOUND, --upper BOUND
Upper bound on the values of the feasible paths that are generated. If this argument is not provided, no upper bound is assumed.

Optional command-line arguments for measurement of values of feasible paths
Options to measure the values of all types of feasible paths, including feasible basis paths. The files that store the measurements and predictions are located in the temporary directory called analysis.
-m, --measure-tests
Creates test cases for each feasible path generated, and measures the value of each test case on the specified simulator. This option can be used with any other option that generates feasible paths. The measurements are saved to a file whose name has the prefix measured-. If none of these other options are used, the test cases for the feasible basis paths are created and measured, and the measurements are saved to a file called measured-basis. However, this assumes that the feasible basis paths have already been generated.
-s {ptarm,simit-arm}, --simulator {ptarm,simit-arm}
Simulator to measure the cycle counts of the test case files on. The default simulator is ptarm.

Optional command-line arguments for creating histograms from the values of feasible paths
Options to create histograms computed from the values of all types of feasible paths, including feasible basis paths. The files that store the histograms are located in the temporary directory called analysis.
--histogram
Creates a histogram from the values of feasible paths. This option can be used with any other option that generates feasible paths.

The histogram created from the predicted values of these feasible paths is saved to a file whose name has the prefix histogram-predicted-. If the values of these feasible paths are also measured on a simulator, using the command-line options for measurement, a histogram is created from the measured values and saved to a file whose name has the prefix histogram-measured-. If, however, none of the other options to generate feasible paths are used, or if feasible basis paths are being generated (and optionally measured), a histogram is created from the values of the feasible basis paths and saved to a file called histogram-basis.
--hist-bins SIZE
Number of equally-sized bins in the histogram that is created. If not provided, the histogram will have 10 equally-sized bins. This command-line option can only be used along with the --histogram command-line option.
--hist-lower SIZE
Lower bound of the range of path values to be considered for histogram creation. If not provided, the lower bound is the smallest value of the paths that are considered for histogram creation. This command-line option can only be used along with the --histogram command-line option.
--hist-upper SIZE
Upper bound of the range of path values to be considered for histogram creation. If not provided, the upper bound is the greatest value of the paths that are considered for histogram creation. This command-line option can only be used along with the --histogram command-line option.