docs/testing.rst - external/github.com/stp/stp - Git at Google

 Introduction
 ============

 STP currently supports the following types of tests

 -  Tests that use query files (i.e. ``smt``, ``smt2`` and ``cvc`` files)
    to drive the ``stp`` binary and check the tool’s output. These are
    driven using the `lit <https://pypi.python.org/pypi/lit>`__ and
    `OutputCheck <https://github.com/stp/OutputCheck>`__ tools. We refer
    to these as query file tests.
 -  Tests that use STP’s API and are checked using the GoogleTest
    framework and driven using lit. We refer to these as unit tests.

 Getting started
 ===============

 We depend on various external tools to do testing. Firstly you should
 install python. Secondly you should initialise STP’s git submodules to
 get the GoogleTest and OutputCheck code.

 ::

     $ cd /path/stp/src
     $ git submodule init
     $ git submodule update

 Now you need to install the lit tool which is available from
 `PyPi <https://pypi.python.org/pypi>`__. An easy way to install the tool
 is using the ``pip`` tool.

 ::

     $ pip install lit

 Note that for Ubuntu 14.04 you need install the ``python-stdeb``
 package, fix the URL in ``/usr/bin/pypi-install`` to
 ``https://pypi.python.org/pypi`` and then execute
 ``sudo pypi-install lit``.

 Installing lit without root access
 ----------------------------------

 If you don’t have root access to your machine you can use the
 `virtualenv <http://www.virtualenv.org/en/latest/>`__ tool to install
 lit in a local python environment.

 ::

     $ cd /path/to/put/your/virtual_environment
     $ virtualenv venv
     Using base prefix '/usr'
     New python executable in venv/bin/python3
     Also creating executable in venv/bin/python
     Installing setuptools, pip...done.
     $ . venv/bin/activate
     (venv) $ pip install lit
     Downloading/unpacking lit
       Downloading lit-0.3.0.tar.gz (45kB): 45kB downloaded
     ...
     Successfully installed lit
     Cleaning up...
     (venv) $

 Note how the shell prompt changes when the ``venv/bin/activate`` script
 is executed from your shell. This is a hint that you are now using the
 python virtual environment named ``venv``

 Note if you do this you need to make sure CMake is aware that you want
 to use the python executable in your virtual environment and not the
 system python executable.

 If you have never executed CMake previously then if you run it from a
 shell where you have activated your virtual environemt (i.e.
 ``venv/bin/activate``) then when CMake is configuring it will detect
 your virtual environment python executable.

 If you have executed CMake previously (e.g. because you have already
 built STP perhaps with testing disabled) then in a shell with your
 python virtual environment enabled you should run ``make edit_cache``
 from the STP build directory root (``ninja edit_cache`` for ninja) and
 then do one of the following

 -  Delete the ``PYTHON_EXECUTABLE`` cache variable and then configure.
    If all goes well you will see the ``PYTHON_EXECUTABLE`` reappear set
    to the full path to your virtual environment python executable. Once
    you have configured successfully you should regenerate the build
    system (i.e. press the generate button).

 OR

 -  Set the ``PYTHON_EXECUTABLE`` cache variable manually to the path to
    your virtual environment python executable and then configure and
    generate.

 CMake options
 -------------

 There are various CMake options that allow control over testing. You can
 easily configure these by…

 -  When configuring for the first time use the ``cmake-gui`` or
    ``ccmake`` tool.
 -  If you’ve already configured/built previously by running
    ``make edit_cache`` or ``ninja edit_cache`` in the build directory
    (this assumes you used the ``cmake-gui`` or ``ccmake`` tool when you
    first built).

 At the time of writing the following options are available

 -  ``ENABLE_TESTING`` - If enabled other testing options will be
    available
 -  ``LIT_TOOL`` - Path to the ``lit`` executable (you shouldn’t need to
    modify this normally)
 -  ``PYTHON_EXECUTABLE`` - Path to the python executable to use for
    testing programs. If you used ``virtualenv`` to install ``lit`` you
    should ensure that this CMake variable is set to the path to the
    ``virtualenv`` python executable. This will happen automatically if
    you used the virtualenv ``activate`` script before configuring.
 -  ``TEST_APIS`` - If enabled the tests available under ``tests/api``
    will become available.
 -  ``TEST_C_API`` - If enabled the C API unit tests will be available
    for building/testing.
 -  ``TEST_QUERY_FILES`` - If enabled the query file tests will be
    available for testing.
 -  ``USE_VALGRIND`` - If enabled Valgrind will be used for unit tests.

 Running tests
 -------------

 To attempt to run all tests from the build directory (assuming you are
 using the Makefile generated build system) run

 ::

     $ make check

 Note if any tests fail other test suites will not execute (unless you
 pass the ``-i`` flag to make).

 Notes for Query file tests
 --------------------------

 When using the ``lit`` tool to run query file tests it is possible to
 pass various handy parameters.

 ::

     $ lit --param=solver=/path/to/solver .

 This will change the solver from STP to a solver of your choice

 ::

     $ lit --param=solver_params="-flag1 -flag2 -flag3" .

 This will pass additional flags to the solver ## Individual test suites

 Query file tests
 ~~~~~~~~~~~~~~~~

 To run the query file tests run

 ::

     $ make query-file-tests

 to run directly using ``lit`` run

 ::

     $ cd /path/to/stp/build/
     $ lit tests/query-files

 C API tests
 ~~~~~~~~~~~

 To run and build the C-api tests run

 ::

     $ make C-api-tests

 Individual tests
 ----------------

 .. _query-file-tests-1:

 Query file tests
 ~~~~~~~~~~~~~~~~

 When running the query file tests the lit tool gives you the ability to
 easily run a subset of tests. For example say you are in the
 ``tests/query-files`` directory. You can do the following

 ::

     $ lit -v misc-tests/ unit_test/alwaysTrue.smt2

 This will run all tests under the ``tests/misc-tests`` folder and run
 the ``unit_test/alwaysTrue.smt2`` test.

 Unit tests
 ~~~~~~~~~~

 The unit tests are built as standalone executables so individual tests
 can be executed by just running their executables.

 For example for the C API tests the built tests can be found in
 ``tests/api/C`` in the build directory.

 Writing tests
 -------------

 .. _query-file-tests-2:

 Query file tests
 ----------------

 You should take a look the existing tests and at the
 `lit <http://llvm.org/docs/CommandGuide/lit.html>`__, `LLVM
 testing <http://llvm.org/docs/TestingGuide.html#writing-new-regression-tests>`__
 and
 `OutputCheck <https://github.com/stp/OutputCheck/blob/master/README.md>`__
 documentation.

 .. _unit-tests-1:

 Unit tests
 ----------

 You should take a look at some existing testsand read the `GoogleTest
 documentation <https://code.google.com/p/googletest/wiki/Documentation>`__.
	Introduction
	============

	STP currently supports the following types of tests

	- Tests that use query files (i.e. ``smt``, ``smt2`` and ``cvc`` files)
	to drive the ``stp`` binary and check the tool’s output. These are
	driven using the `lit <https://pypi.python.org/pypi/lit>`__ and
	`OutputCheck <https://github.com/stp/OutputCheck>`__ tools. We refer
	to these as query file tests.
	- Tests that use STP’s API and are checked using the GoogleTest
	framework and driven using lit. We refer to these as unit tests.

	Getting started
	===============

	We depend on various external tools to do testing. Firstly you should
	install python. Secondly you should initialise STP’s git submodules to
	get the GoogleTest and OutputCheck code.

	::

	$ cd /path/stp/src
	$ git submodule init
	$ git submodule update

	Now you need to install the lit tool which is available from
	`PyPi <https://pypi.python.org/pypi>`__. An easy way to install the tool
	is using the ``pip`` tool.

	::

	$ pip install lit

	Note that for Ubuntu 14.04 you need install the ``python-stdeb``
	package, fix the URL in ``/usr/bin/pypi-install`` to
	``https://pypi.python.org/pypi`` and then execute
	``sudo pypi-install lit``.

	Installing lit without root access
	----------------------------------

	If you don’t have root access to your machine you can use the
	`virtualenv <http://www.virtualenv.org/en/latest/>`__ tool to install
	lit in a local python environment.

	::

	$ cd /path/to/put/your/virtual_environment
	$ virtualenv venv
	Using base prefix '/usr'
	New python executable in venv/bin/python3
	Also creating executable in venv/bin/python
	Installing setuptools, pip...done.
	$ . venv/bin/activate
	(venv) $ pip install lit
	Downloading/unpacking lit
	Downloading lit-0.3.0.tar.gz (45kB): 45kB downloaded
	...
	Successfully installed lit
	Cleaning up...
	(venv) $

	Note how the shell prompt changes when the ``venv/bin/activate`` script
	is executed from your shell. This is a hint that you are now using the
	python virtual environment named ``venv``

	Note if you do this you need to make sure CMake is aware that you want
	to use the python executable in your virtual environment and not the
	system python executable.

	If you have never executed CMake previously then if you run it from a
	shell where you have activated your virtual environemt (i.e.
	``venv/bin/activate``) then when CMake is configuring it will detect
	your virtual environment python executable.

	If you have executed CMake previously (e.g. because you have already
	built STP perhaps with testing disabled) then in a shell with your
	python virtual environment enabled you should run ``make edit_cache``
	from the STP build directory root (``ninja edit_cache`` for ninja) and
	then do one of the following

	- Delete the ``PYTHON_EXECUTABLE`` cache variable and then configure.
	If all goes well you will see the ``PYTHON_EXECUTABLE`` reappear set
	to the full path to your virtual environment python executable. Once
	you have configured successfully you should regenerate the build
	system (i.e. press the generate button).

	OR

	- Set the ``PYTHON_EXECUTABLE`` cache variable manually to the path to
	your virtual environment python executable and then configure and
	generate.

	CMake options
	-------------

	There are various CMake options that allow control over testing. You can
	easily configure these by…

	- When configuring for the first time use the ``cmake-gui`` or
	``ccmake`` tool.
	- If you’ve already configured/built previously by running
	``make edit_cache`` or ``ninja edit_cache`` in the build directory
	(this assumes you used the ``cmake-gui`` or ``ccmake`` tool when you
	first built).

	At the time of writing the following options are available

	- ``ENABLE_TESTING`` - If enabled other testing options will be
	available
	- ``LIT_TOOL`` - Path to the ``lit`` executable (you shouldn’t need to
	modify this normally)
	- ``PYTHON_EXECUTABLE`` - Path to the python executable to use for
	testing programs. If you used ``virtualenv`` to install ``lit`` you
	should ensure that this CMake variable is set to the path to the
	``virtualenv`` python executable. This will happen automatically if
	you used the virtualenv ``activate`` script before configuring.
	- ``TEST_APIS`` - If enabled the tests available under ``tests/api``
	will become available.
	- ``TEST_C_API`` - If enabled the C API unit tests will be available
	for building/testing.
	- ``TEST_QUERY_FILES`` - If enabled the query file tests will be
	available for testing.
	- ``USE_VALGRIND`` - If enabled Valgrind will be used for unit tests.

	Running tests
	-------------

	To attempt to run all tests from the build directory (assuming you are
	using the Makefile generated build system) run

	::

	$ make check

	Note if any tests fail other test suites will not execute (unless you
	pass the ``-i`` flag to make).

	Notes for Query file tests
	--------------------------

	When using the ``lit`` tool to run query file tests it is possible to
	pass various handy parameters.

	::

	$ lit --param=solver=/path/to/solver .

	This will change the solver from STP to a solver of your choice

	::

	$ lit --param=solver_params="-flag1 -flag2 -flag3" .

	This will pass additional flags to the solver ## Individual test suites

	Query file tests
	~~~~~~~~~~~~~~~~

	To run the query file tests run

	::

	$ make query-file-tests

	to run directly using ``lit`` run

	::

	$ cd /path/to/stp/build/
	$ lit tests/query-files

	C API tests
	~~~~~~~~~~~

	To run and build the C-api tests run

	::

	$ make C-api-tests

	Individual tests
	----------------

	.. _query-file-tests-1:

	Query file tests
	~~~~~~~~~~~~~~~~

	When running the query file tests the lit tool gives you the ability to
	easily run a subset of tests. For example say you are in the
	``tests/query-files`` directory. You can do the following

	::

	$ lit -v misc-tests/ unit_test/alwaysTrue.smt2

	This will run all tests under the ``tests/misc-tests`` folder and run
	the ``unit_test/alwaysTrue.smt2`` test.

	Unit tests
	~~~~~~~~~~

	The unit tests are built as standalone executables so individual tests
	can be executed by just running their executables.

	For example for the C API tests the built tests can be found in
	``tests/api/C`` in the build directory.

	Writing tests
	-------------

	.. _query-file-tests-2:

	Query file tests
	----------------

	You should take a look the existing tests and at the
	`lit <http://llvm.org/docs/CommandGuide/lit.html>`__, `LLVM
	testing <http://llvm.org/docs/TestingGuide.html#writing-new-regression-tests>`__
	and
	`OutputCheck <https://github.com/stp/OutputCheck/blob/master/README.md>`__
	documentation.

	.. _unit-tests-1:

	Unit tests
	----------

	You should take a look at some existing testsand read the `GoogleTest
	documentation <https://code.google.com/p/googletest/wiki/Documentation>`__.