Skip to content

Commit

Permalink
Replace references to "llvm-lit" by "lit" in the documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
ccadar committed Feb 16, 2024
1 parent 5bf7941 commit 6ba37e9
Showing 1 changed file with 10 additions and 10 deletions.
20 changes: 10 additions & 10 deletions docs/developers-guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -174,16 +174,16 @@ This will generate the documentation in `path/to/build-dir/docs/doxygen/`.

KLEE uses LLVM's testing infrastructure for its regression tests. In KLEE these are...

* External tests executed by [llvm-lit](http://llvm.org/docs/CommandGuide/lit.html). These are the tests that are executed by the ``make check`` command. These test the KLEE tools externally.
* External tests executed by [lit](http://llvm.org/docs/CommandGuide/lit.html). These are the tests that are executed by the ``make check`` command. These test the KLEE tools externally.
* Internal tests that are driven using [GoogleTest](https://code.google.com/p/googletest/). These are the tests that are executed by the ``make unittests`` command. These test KLEE's internal APIs.

### External tests

``llvm-lit`` is used to test KLEE's tools by invoking them as shell commands.
``lit`` is used to test KLEE's tools by invoking them as shell commands.

KLEE's tests are currently divided into categories, each of which is a subdirectory in ``test/`` in the source tree (e.g. ``test/Feature``).

``llvm-lit`` is passed one or more paths to test files or directories which it will search recursively for tests. The ``llvm-lit`` tool needs to know what test-suite the tests belong to and how to run them. This information is in the ``lit.site.cfg`` (generated by the ``Makefile``). This file itself refers to ``lit.cfg`` which tells ``llvm-lit`` how to run the test suite. At the time of writing the ``lit.cfg`` instructs ``llvm-lit`` to treat files with the following file extensions as tests:`` .ll .c .cpp .kquery``.
``lit`` is passed one or more paths to test files or directories which it will search recursively for tests. The ``lit`` tool needs to know what test-suite the tests belong to and how to run them. This information is in the ``lit.site.cfg`` (generated by the ``Makefile``). This file itself refers to ``lit.cfg`` which tells ``lit`` how to run the test suite. At the time of writing the ``lit.cfg`` instructs ``lit`` to treat files with the following file extensions as tests:`` .ll .c .cpp .kquery``.

It is desirable to disable some tests (e.g. disable klee-uclibc tests if support was not compiled in) or change which file extensions to look for. This is done by adding a ``lit.local.cfg`` file to a directory which can be used to customise how tests in that directory are executed. For example to change the file extensions searched for to ``.cxx`` and ``.txt`` the following could be used in a ``lit.local.cfg`` file:

Expand All @@ -199,7 +199,7 @@ mark them as unsupported by placing the following inside a
if some_condition: config.unsupported = True
{% endhighlight %}

All ``llvm-lit`` configuration files are Python scripts loaded by ``llvm-lit`` so you have the full power of Python at your disposal.
All ``lit`` configuration files are Python scripts loaded by ``lit`` so you have the full power of Python at your disposal.

The actions performed in each test are specified by special comments in the file. For example, in ``test/Feature/ByteSwap.c`` the first two lines are:

Expand All @@ -224,18 +224,18 @@ $ cd path/to/klee/build/test
$ make check
{% endhighlight %}

or you can use ``llvm-lit`` directly
or you can use ``lit`` directly

{% highlight bash %}
$ cd path/to/klee/build/test
$ llvm-lit .
$ lit .
{% endhighlight %}

If you want to run a subset of the test suite simply pass the filenames of the tests or directories to search for tests to ``llvm-lit``. For example the commands below will execute the ``Feature/DoubleFree.c`` and ``CXX/ArrayNew.cpp`` test and all tests nested in the ``regression/`` folder.
If you want to run a subset of the test suite simply pass the filenames of the tests or directories to search for tests to ``lit``. For example the commands below will execute the ``Feature/DoubleFree.c`` and ``CXX/ArrayNew.cpp`` test and all tests nested in the ``regression/`` folder.

{% highlight bash %}
$ cd path/to/klee/build/test
$ llvm-lit Feature/DoubleFree.c CXX/ArrayNew.cpp regression/
$ lit Feature/DoubleFree.c CXX/ArrayNew.cpp regression/
{% endhighlight %}

Sometimes it can be useful to pass extra command line options to ``klee`` or ``kleaver`` when running tests. This could be used for example to quickly see if changing the default value for a command line option changes the passing/failing of a test. This is **not** a substitute for writing new tests for ``klee`` or ``kleaver``! If you add a new feature that is exposed by a new command line option a new test should be added that tests this behaviour.
Expand All @@ -244,12 +244,12 @@ Here is an example:

{% highlight bash %}
$ cd test/
$ llvm-lit --param klee_opts=-use-forked-solver=0 --param kleaver_opts="-use-forked-solver=0 -use-query-log=all:smt2" .
$ lit --param klee_opts=-use-forked-solver=0 --param kleaver_opts="-use-forked-solver=0 -use-query-log=all:smt2" .
{% endhighlight %}

In this example when running ``klee`` in tests an extra option ``-use-forked-solver=0`` is passed to ``klee`` and when running ``kleaver`` the ``-use-forked-solver=0`` and ``-use-query-log=all:smt2`` options will be passed to ``kleaver``. It is important to realise if the test already invokes ``klee`` or ``kleaver`` with a particular option you will not be able to override that option because the ``klee_opts`` and ``kleaver_opts`` are substituted just after the tool name so subsequent options used in the test will override these.

For more information on ``llvm-lit`` tests see [LLVM's testing infrastructure documentation](http://llvm.org/docs/TestingGuide.html#id1) and the [``llvm-lit`` tool documentation](http://llvm.org/docs/CommandGuide/lit.html).
For more information on ``lit`` tests see [LLVM's testing infrastructure documentation](http://llvm.org/docs/TestingGuide.html#id1) and the [``lit`` tool documentation](http://llvm.org/docs/CommandGuide/lit.html).

### Internal tests

Expand Down

0 comments on commit 6ba37e9

Please sign in to comment.